From bfca80bb8b6b13ddbfab29c151c5783aa1b94a28 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Thu, 15 Dec 2022 23:22:15 +0100 Subject: [PATCH 1/7] Avoid crashes that can occur `when` using when with a statement that may crash if the `when` condition doesn't hold For instance ``` node main () returns (o: int); var i: int; let i = 0; o = (1 / i) when false; tel ``` used to crash with for instance: ``` Floating point exception 136 ``` now returns `0` but in fact this value wouldn't be used in theory as the `when` condition doesn't hold. --- src/ast_to_c.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast_to_c.ml b/src/ast_to_c.ml index 52b439c..ff4e5f7 100644 --- a/src/ast_to_c.ml +++ b/src/ast_to_c.ml @@ -99,8 +99,8 @@ let pp_expression node_name = match expression with | EWhen (_, e1, e2) -> begin - (* as don't use a variable assigned when the condition holds, can define it even if the condition doesn't hold *) - Format.fprintf fmt "%a" + Format.fprintf fmt "%a ? %a : 0" + pp_expression_aux e2 pp_expression_aux e1 end | EReset (_, e1, e2) -> From de294df84ade5a0668986780f83fcbe2a131fa09 Mon Sep 17 00:00:00 2001 From: Antoine Grimod Date: Thu, 15 Dec 2022 23:32:36 +0100 Subject: [PATCH 2/7] Translation of automaton to lustre almost finished --- src/passes.ml | 166 +++++++++++++++++++++++++++++++++++++++----- src/passes_utils.ml | 5 ++ 2 files changed, 153 insertions(+), 18 deletions(-) diff --git a/src/passes.ml b/src/passes.ml index 9fdffda..e11b579 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -155,29 +155,29 @@ let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option in node_pass aux +let rec tpl debug ((pat, exp): t_equation) = + match exp with + | ETuple (_, hexps :: texps) -> + debug "An ETuple has been recognized, inlining..."; + let p1, p2 = + list_select + (List.length (type_exp hexps)) + (snd pat) in + let t1 = List.flatten (List.map type_var p1) in + let t2 = List.flatten (List.map type_var p2) in + ((t1, p1), hexps) + :: (tpl debug ((t2, p2), + ETuple (List.flatten (List.map type_exp texps), texps))) + | ETuple (_, []) -> [] + | _ -> [(pat, exp)] + let pass_linearization verbose debug main_fn = let node_lin (node: t_node): t_node option = - let rec tpl ((pat, exp): t_equation) = - match exp with - | ETuple (_, hexps :: texps) -> - debug "An ETuple has been recognized, inlining..."; - let p1, p2 = - list_select - (List.length (type_exp hexps)) - (snd pat) in - let t1 = List.flatten (List.map type_var p1) in - let t2 = List.flatten (List.map type_var p2) in - ((t1, p1), hexps) - :: (tpl ((t2, p2), - ETuple (List.flatten (List.map type_exp texps), texps))) - | ETuple (_, []) -> [] - | _ -> [(pat, exp)] - in let new_locvars = node.n_local_vars in let new_equations = List.flatten begin List.map - tpl + (tpl debug) node.n_equations end in Some @@ -185,7 +185,7 @@ let pass_linearization verbose debug main_fn = n_name = node.n_name; n_inputs = node.n_inputs; n_outputs = node.n_outputs; - n_local_vars = new_locvars; + n_local_vars = node.n_local_vars; n_equations = new_equations; n_automata = node.n_automata; } @@ -296,3 +296,133 @@ let pass_typing verbose debug main_fn ast = else None in aux ast +let check_automaton_branch_vars automaton = + let (init, states) = automaton in + let left_side = Hashtbl.create 10 in + + let rec init_left_side eqlist = match eqlist with + | [] -> () + | (varlist, exp)::q -> + begin + Hashtbl.add left_side varlist true; + init_left_side q; + end + in + let check_state s = match s with + | State(name, eqs, cond, next) -> + List.for_all (fun (varlist, exp) -> (Hashtbl.mem left_side varlist)) eqs + in + begin + match init with | State(name, eqs, cond, next) -> init_left_side eqs; + let validity = List.for_all (fun s -> (check_state s)) states in + if not validity then + failwith "Automaton branch has different variables assignment in different branches" + end + +let automaton_translation debug automaton = + let gathered = Hashtbl.create 10 in + let state_to_int = Hashtbl.create 10 in + let add_to_table var exp state = + if Hashtbl.mem gathered var then + let res = Hashtbl.find gathered var in + Hashtbl.replace gathered var ((state, exp)::res); + else + Hashtbl.replace gathered var ([(state, exp)]) + in + let rec init_state_translation states c = match states with + | [] -> () + | State(name, _, _, _)::q -> + Hashtbl.replace state_to_int name c; (init_state_translation q c) + in + + let rec find_state name = + match Hashtbl.find_opt state_to_int name with + | None -> failwith "Unknown state in automaton" + | Some v -> v + in + + let rec equation_pass state : t_eqlist -> unit = function + | [] -> () + | (vars, exp)::q -> begin + add_to_table vars exp state; + equation_pass state q + end + in + + let flatten_state state = match state with + | State(name, eq, cond, next) -> + let new_equations = List.flatten + begin + List.map + (tpl debug) + eq + end in + equation_pass name new_equations; + State(name, new_equations, cond, next) + in + + let rec transition_eq states s = + match states with + | [] -> EVar([TInt], IVar(s)) + | State(name, eqs, cond, next)::q -> + let name = find_state name + and next = find_state next in + ETriOp([TInt], TOp_if, + EBinOp([TBool], BOp_and, + EComp([TBool], COp_eq, + EVar([TInt], IVar(s)), + EConst([TInt], CInt(name)) + ), + cond + ), + EConst([TInt], CInt(next)), + transition_eq q s + ) + in + + let rec translate_var s v explist = match explist with + | [] -> EConst([TInt], CInt(0)) (* TODO *) + | (state, exp)::q -> + ETriOp(Utils.type_exp exp, TOp_if, + EComp([TBool], COp_eq, + EVar([TInt], IVar(s)), + EConst([TInt], CInt(Hashtbl.find state_to_int state)) + ), + exp, + translate_var s v q + ) + in + + let flatten_automaton automaton = + let (init, states) = automaton in + (flatten_state init, List.map flatten_state states) + in + let (init, states) = flatten_automaton automaton in + let s = create_automaton_name () in + init_state_translation states 1; + let exp_transition = transition_eq states s 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) + + +let automata_trans_pass debug (node:t_node) : t_node option= + + let rec aux automaton = match automaton with + | [] -> [], [] + | a::q -> + let eq, var = automaton_translation debug a + and tail_eq, tail_var = aux q in + eq@tail_eq, var::tail_var + in + + let eqs, vars = aux node.n_automata in + Some + { + n_name = node.n_name; + n_inputs = node.n_inputs; + n_outputs = node.n_outputs; + n_local_vars = vars@node.n_local_vars; + n_equations = eqs@new_equations; + n_automata = node.n_automata; + } + diff --git a/src/passes_utils.ml b/src/passes_utils.ml index 0e159d9..d7356a8 100644 --- a/src/passes_utils.ml +++ b/src/passes_utils.ml @@ -31,3 +31,8 @@ let expression_pass f: t_nodelist -> t_nodelist option = equation_pass aux exception PassExn of string + +let counter = ref 0 +let create_automaton_name : unit -> string = fun () -> + counter := !counter + 1; + Format.asprintf "_s%d" (!counter) From 21d2d0c9bba628f084956379001e8764601f1a67 Mon Sep 17 00:00:00 2001 From: Antoine Grimod Date: Thu, 15 Dec 2022 23:48:02 +0100 Subject: [PATCH 3/7] fix type error in code --- src/passes.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/passes.ml b/src/passes.ml index e11b579..f141130 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -408,21 +408,22 @@ let automaton_translation debug automaton = let automata_trans_pass debug (node:t_node) : t_node option= let rec aux automaton = match automaton with - | [] -> [], [] + | [] -> [], [], [] | a::q -> let eq, var = automaton_translation debug a - and tail_eq, tail_var = aux q in - eq@tail_eq, var::tail_var + and tail_eq, tail_var, tail_type = aux q in + eq@tail_eq, var::tail_var, TInt::tail_type in - let eqs, vars = aux node.n_automata in + let eqs, vars, new_ty = aux node.n_automata in + let ty, loc_vars = node.n_local_vars in Some { n_name = node.n_name; n_inputs = node.n_inputs; n_outputs = node.n_outputs; - n_local_vars = vars@node.n_local_vars; - n_equations = eqs@new_equations; + n_local_vars = (new_ty@ty, vars@loc_vars); + n_equations = eqs@node.n_equations; n_automata = node.n_automata; } From 0c8da12afe243ad92c9841cf1db6eaf4667396c4 Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Fri, 16 Dec 2022 00:00:11 +0100 Subject: [PATCH 4/7] Correct typo in verification that nodes always have arguments and make the `main` having such a verification too, as in Lustre --- src/parser.mly | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parser.mly b/src/parser.mly index c6a1305..134a77d 100644 --- a/src/parser.mly +++ b/src/parser.mly @@ -199,7 +199,7 @@ node_content: n_local_vars = $10; n_equations = eqs; n_automata = aut; } in - if List.length (snd $10) = 0 && node_name <> "main" + if List.length t_in = 0 then raise (MyParsingError (Format.asprintf "The node %s should have arguments." node_name, From b4ae058bf6e14e4176b79b8db682d8519d47374a Mon Sep 17 00:00:00 2001 From: Benjamin Loison Date: Fri, 16 Dec 2022 00:04:57 +0100 Subject: [PATCH 5/7] Remove unused variable `new_locvars` in `src/passes.ml` --- src/passes.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/passes.ml b/src/passes.ml index f141130..ad8ff30 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -173,7 +173,6 @@ let rec tpl debug ((pat, exp): t_equation) = let pass_linearization verbose debug main_fn = let node_lin (node: t_node): t_node option = - let new_locvars = node.n_local_vars in let new_equations = List.flatten begin List.map From 1b3af051b37285764731d2969369ffb95fcc53f4 Mon Sep 17 00:00:00 2001 From: Antoine Grimod Date: Fri, 16 Dec 2022 00:02:48 +0100 Subject: [PATCH 6/7] adding automaton translation pass to list of executed passes --- src/main.ml | 3 ++- src/passes.ml | 4 ++++ src/test.node | 1 - 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/src/main.ml b/src/main.ml index 450e81d..06434d7 100644 --- a/src/main.ml +++ b/src/main.ml @@ -25,7 +25,7 @@ let exec_passes ast main_fn verbose debug passes f = let _ = (** Usage and argument parsing. *) - let default_passes = ["pre2vars"; "linearization"; "equations_ordering"] in + let default_passes = ["pre2vars"; "automata_translation"; "linearization"; "equations_ordering"] in let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in let usage_msg = "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ @@ -67,6 +67,7 @@ let _ = [ ("pre2vars", Passes.pre2vars); ("chkvar_init_unicity", Passes.chkvar_init_unicity); + ("automata_translation", Passes.automata_translation_pass); ("linearization", Passes.pass_linearization); ("equations_ordering", Passes.pass_eq_reordering); ("check_typing", Passes.pass_typing); diff --git a/src/passes.ml b/src/passes.ml index ad8ff30..e711189 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -426,3 +426,7 @@ let automata_trans_pass debug (node:t_node) : t_node option= n_automata = node.n_automata; } +let automata_translation_pass verbose debug main_fn = + node_pass (automata_trans_pass debug) + + diff --git a/src/test.node b/src/test.node index ef459bb..5b65c18 100644 --- a/src/test.node +++ b/src/test.node @@ -1,5 +1,4 @@ node diagonal_int (i: int) returns (o1, o2 : int); -var i: int; let (o1, o2) = (i, i); tel From 6af9ddf394d1d74d0aac09fc102ca185f3e2f7e8 Mon Sep 17 00:00:00 2001 From: Antoine Grimod Date: Fri, 16 Dec 2022 01:04:09 +0100 Subject: [PATCH 7/7] added pass to check validity of automata and disable flattening of automaton branch because of incorrect code resulting from it --- src/main.ml | 3 ++- src/passes.ml | 61 +++++++++++++++++++++++++++++++-------------------- src/test.node | 5 +++-- 3 files changed, 42 insertions(+), 27 deletions(-) diff --git a/src/main.ml b/src/main.ml index 06434d7..e0c67f3 100644 --- a/src/main.ml +++ b/src/main.ml @@ -25,7 +25,7 @@ let exec_passes ast main_fn verbose debug passes f = let _ = (** Usage and argument parsing. *) - let default_passes = ["pre2vars"; "automata_translation"; "linearization"; "equations_ordering"] in + let default_passes = ["pre2vars"; "automata_validity" ;"automata_translation"; "linearization"; "equations_ordering"] in let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in let usage_msg = "Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \ @@ -68,6 +68,7 @@ let _ = ("pre2vars", Passes.pre2vars); ("chkvar_init_unicity", Passes.chkvar_init_unicity); ("automata_translation", Passes.automata_translation_pass); + ("automata_validity", Passes.check_automata_validity); ("linearization", Passes.pass_linearization); ("equations_ordering", Passes.pass_eq_reordering); ("check_typing", Passes.pass_typing); diff --git a/src/passes.ml b/src/passes.ml index e711189..6c721a3 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -295,28 +295,35 @@ let pass_typing verbose debug main_fn ast = else None in aux ast -let check_automaton_branch_vars automaton = - let (init, states) = automaton in - let left_side = Hashtbl.create 10 in +let check_automata_validity verbos debug main_fn = + let check_automaton_branch_vars automaton = + let (init, states) = automaton in + let left_side = Hashtbl.create 10 in - let rec init_left_side eqlist = match eqlist with - | [] -> () - | (varlist, exp)::q -> - begin - Hashtbl.add left_side varlist true; - init_left_side q; - end + let rec init_left_side eqlist = match eqlist with + | [] -> () + | (varlist, exp)::q -> + begin + Hashtbl.add left_side varlist true; + init_left_side q; + end + in + let check_state s = match s with + | State(name, eqs, cond, next) -> + List.for_all (fun (varlist, exp) -> (Hashtbl.mem left_side varlist)) eqs + in + begin + match init with | State(name, eqs, cond, next) -> init_left_side eqs; + let validity = List.for_all (fun s -> (check_state s)) states in + if not validity then + failwith "Automaton branch has different variables assignment in different branches" + end in - let check_state s = match s with - | State(name, eqs, cond, next) -> - List.for_all (fun (varlist, exp) -> (Hashtbl.mem left_side varlist)) eqs + let aux node = + List.iter check_automaton_branch_vars node.n_automata; + Some node in - begin - match init with | State(name, eqs, cond, next) -> init_left_side eqs; - let validity = List.for_all (fun s -> (check_state s)) states in - if not validity then - failwith "Automaton branch has different variables assignment in different branches" - end + node_pass aux let automaton_translation debug automaton = let gathered = Hashtbl.create 10 in @@ -331,7 +338,7 @@ let automaton_translation debug automaton = let rec init_state_translation states c = match states with | [] -> () | State(name, _, _, _)::q -> - Hashtbl.replace state_to_int name c; (init_state_translation q c) + Hashtbl.replace state_to_int name c; (init_state_translation q (c+1)) in let rec find_state name = @@ -350,14 +357,20 @@ let automaton_translation debug automaton = let flatten_state state = match state with | State(name, eq, cond, next) -> + (* Flattening is not possible + for example a branch where x,y = 1, 2 will be unpacked + when in another branch x, y = f(z) will not be unpacked + *) + (* let new_equations = List.flatten begin List.map (tpl debug) eq end in - equation_pass name new_equations; - State(name, new_equations, cond, next) + *) + equation_pass name eq; + State(name, eq, cond, next) in let rec transition_eq states s = @@ -399,7 +412,7 @@ let automaton_translation debug automaton = let (init, states) = flatten_automaton automaton in let s = create_automaton_name () in init_state_translation states 1; - let exp_transition = 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 Hashtbl.fold (fun var explist acc -> (var, translate_var s var explist)::acc) gathered new_equations, IVar(s) @@ -423,7 +436,7 @@ let automata_trans_pass debug (node:t_node) : t_node option= n_outputs = node.n_outputs; n_local_vars = (new_ty@ty, vars@loc_vars); n_equations = eqs@node.n_equations; - n_automata = node.n_automata; + n_automata = []; (* not needed anymore *) } let automata_translation_pass verbose debug main_fn = diff --git a/src/test.node b/src/test.node index 5b65c18..03d9db8 100644 --- a/src/test.node +++ b/src/test.node @@ -12,9 +12,10 @@ let tel node auto (i: int) returns (o : int); +var x, y:int; let automaton - | Incr -> do o = (pre o) + 1; done - | Decr -> do o = (pre o) - 1; done + | Incr -> do (o,x) = (0 fby o + 1, 2); done + | Decr -> do (o,x) = diagonal_int(0 fby o); done tel