Compare commits

..

2 Commits

Author SHA1 Message Date
Antoine Grimod
aa84a07902 testing clock unification 2022-12-16 14:51:41 +01:00
Antoine Grimod
ed54fd0114 clock unification added 2022-12-16 14:51:41 +01:00
4 changed files with 137 additions and 8 deletions

View File

@ -73,3 +73,7 @@ and t_node =
type t_nodelist = t_node list type t_nodelist = t_node list
type t_ck = base_ck list
and base_ck =
| Base
| On of base_ck * t_expression

View File

@ -25,7 +25,7 @@ let exec_passes ast main_fn verbose debug passes f =
let _ = let _ =
(** Usage and argument parsing. *) (** Usage and argument parsing. *)
let default_passes = ["automata_validity" ;"automata_translation"; "linearization"; "pre2vars"; "equations_ordering"] in let default_passes = ["automata_validity" ;"automata_translation"; "linearization"; "pre2vars"; "equations_ordering"; "clock_unification"] in
let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in
let usage_msg = let usage_msg =
"Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
@ -72,6 +72,7 @@ let _ =
("linearization", Passes.pass_linearization); ("linearization", Passes.pass_linearization);
("equations_ordering", Passes.pass_eq_reordering); ("equations_ordering", Passes.pass_eq_reordering);
("check_typing", Passes.pass_typing); ("check_typing", Passes.pass_typing);
("clock_unification", Passes.clock_unification_pass);
]; ];
(** Main functionality below *) (** Main functionality below *)

View File

@ -89,7 +89,7 @@ let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option
let aux (node: t_node) : t_node option = let aux (node: t_node) : t_node option =
let incr_aux h n = let incr_aux h n =
match Hashtbl.find_opt h n with match Hashtbl.find_opt h n with
| None -> failwith "todo, should not happened." | None -> raise (PassExn "todo, should not happened.")
| Some num -> Hashtbl.replace h n (num + 1) | Some num -> Hashtbl.replace h n (num + 1)
in in
let incr_eq h (((_, patt), _): t_equation) = let incr_eq h (((_, patt), _): t_equation) =
@ -403,7 +403,7 @@ let check_automata_validity verbos debug main_fn =
match init with | State(name, eqs, cond, next) -> init_left_side eqs; match init with | State(name, eqs, cond, next) -> init_left_side eqs;
let validity = List.for_all (fun s -> (check_state s)) states in let validity = List.for_all (fun s -> (check_state s)) states in
if not validity then if not validity then
failwith "Automaton branch has different variables assignment in different branches" raise (PassExn "Automaton branch has different variables assignment in different branches")
end end
in in
let aux node = let aux node =
@ -479,8 +479,21 @@ let automaton_translation debug automaton =
) )
in in
let rec translate_var s v explist = match explist with let default_constant ty =
| [] -> EConst([TInt], CInt(0)) (* TODO *) let defaults ty = match ty with
| TInt -> EConst([ty], CInt(0))
| TBool -> EConst([ty], CBool(false))
| TReal -> EConst([ty], CReal(0.0))
in
match ty with
| [TInt] -> EConst(ty, CInt(0))
| [TBool] -> EConst(ty, CBool(false))
| [TReal] -> EConst(ty, CReal(0.0))
| _ -> ETuple(ty, List.map defaults ty)
in
let rec translate_var s v explist ty = match explist with
| [] -> default_constant ty (* TODO *)
| (state, exp)::q -> | (state, exp)::q ->
ETriOp(Utils.type_exp exp, TOp_if, ETriOp(Utils.type_exp exp, TOp_if,
EComp([TBool], COp_eq, EComp([TBool], COp_eq,
@ -488,7 +501,7 @@ let automaton_translation debug automaton =
EConst([TInt], CInt(Hashtbl.find state_to_int state)) EConst([TInt], CInt(Hashtbl.find state_to_int state))
), ),
exp, exp,
translate_var s v q translate_var s v q ty
) )
in in
@ -501,7 +514,7 @@ let automaton_translation debug automaton =
init_state_translation states 1; init_state_translation states 1;
let exp_transition = EBinOp([TInt], BOp_arrow, EConst([TInt], CInt(1)), EMonOp([TInt], MOp_pre, transition_eq states s)) in let exp_transition = EBinOp([TInt], BOp_arrow, EConst([TInt], CInt(1)), EMonOp([TInt], MOp_pre, transition_eq states s)) in
let new_equations = [(([TInt], [IVar(s)]), exp_transition)] in let new_equations = [(([TInt], [IVar(s)]), exp_transition)] in
Hashtbl.fold (fun var explist acc -> (var, translate_var s var explist)::acc) gathered new_equations, IVar(s) Hashtbl.fold (fun var explist acc -> (var, translate_var s var explist (fst var))::acc) gathered new_equations, IVar(s)
let automata_trans_pass debug (node:t_node) : t_node option= let automata_trans_pass debug (node:t_node) : t_node option=
@ -529,4 +542,106 @@ let automata_trans_pass debug (node:t_node) : t_node option=
let automata_translation_pass verbose debug main_fn = let automata_translation_pass verbose debug main_fn =
node_pass (automata_trans_pass debug) node_pass (automata_trans_pass debug)
let clock_unification_pass verbose debug main_fn ast =
let failure str = raise (PassExn ("Failed to unify clocks: "^str)) in
let known_clocks = Hashtbl.create 100 in
let find_clock_var var =
match Hashtbl.find_opt known_clocks var with
| None ->
begin
match var with
| BVar(name)
| IVar(name)
| RVar(name) -> raise (PassExn ("Cannot find clock of variable "^name) )
end
| Some c -> c
in
let rec compute_clock_exp exp = match exp with
| EConst(_, _) -> [Base]
| EVar(_, var) -> find_clock_var var
| EMonOp(_, MOp_pre, _) -> [Base]
| EMonOp(_, _, e) -> compute_clock_exp e
| EComp(_, _, e1, e2)
| EReset(_, e1, e2)
| EBinOp(_, _, e1, e2) ->
begin
let c1 = compute_clock_exp e1
and c2 = compute_clock_exp e2 in
if c1 <> c2 then
failure "Binop"
else
c1
end
| EWhen(_, e1, e2) ->
begin
match compute_clock_exp e1 with
| [c1] -> [On (c1, e2)]
| _ -> failure "When"
end
| ETriOp(_, TOp_merge, e1, e2, e3) ->
begin
let c1 = compute_clock_exp e1
and c2 = compute_clock_exp e2
and c3 = compute_clock_exp e3 in
match c1, c2, c3 with
| [c1], [On(cl2, e2)], [On(cl3, e3)] ->
begin
if cl2 <> c1 || cl3 <> c1 then
failure "Triop clocks"
else match e2, e3 with
| EMonOp(_, MOp_not, e), _ when e = e3 -> [c1]
| _, EMonOp(_, MOp_not, e) when e = e2 -> [c1]
| _ -> failure "Triop condition"
end
| _ -> failure ("Merge format")
end
| ETriOp(_, TOp_if, e1, e2, e3) ->
let c1 = compute_clock_exp e1
and c2 = compute_clock_exp e2
and c3 = compute_clock_exp e3 in
if c2 <> c3 then
failure "If clocks"
else c2
| ETuple(_, explist) -> List.concat_map compute_clock_exp explist
| EApp(_, node, e) ->
let rec aux_app clk_list = match clk_list with
| [] -> raise (PassExn "Node called with no argument provided")
| [cl] -> cl
| t::q -> if t = (aux_app q) then t else failure "App diff clocks"
and mult_clk cl out_list = match out_list with
| [] -> []
| t::q -> cl::(mult_clk cl q)
in
mult_clk (aux_app (compute_clock_exp e)) (snd node.n_outputs)
in
let rec compute_eq_clock eq =
let rec step vars clks = match vars, clks with
| [], [] -> ()
| [], c::q -> raise (PassExn "Mismatch between clock size")
| v::t, c::q -> Hashtbl.replace known_clocks v [c]; step t q
| l, [] -> raise (PassExn "Mismatch between clock size")
in
let (_, vars), exp = eq in
let clk = compute_clock_exp exp in
step vars clk
in
let compute_clock_node n =
begin
Hashtbl.clear known_clocks;
List.iter (fun v -> Hashtbl.replace known_clocks v [Base]) (
snd n.n_inputs); (* Initializing inputs to base clock *)
List.iter compute_eq_clock n.n_equations;
if not (List.for_all (fun v -> (Hashtbl.find known_clocks v) = [Base]) (
snd n.n_outputs)) then failure "Outputs" (*Checking that the node's output are on base clock *)
else
Some n
end
in node_pass compute_clock_node ast

View File

@ -2,3 +2,12 @@ node main (i: int) returns (o1: int);
let let
o1 = 10 -> pre (20 -> 30); o1 = 10 -> pre (20 -> 30);
tel tel
node flipflop(i: int) returns (z: int);
var x, y: int; c: bool;
let
c = true fby (not c);
x = 1 on c;
y = 2 on (not c);
z = merge c x y;
tel