diff --git a/beamer/beamer.tex b/beamer/beamer.tex index 445a780..7606b00 100644 --- a/beamer/beamer.tex +++ b/beamer/beamer.tex @@ -6,6 +6,13 @@ \begin{document} +\title{Presentation of our Lustre-to-C compiler} +%\subtitle{} +\date{16 December 2022} +\author{Benjamin Loison, Arnaud Daby-Seesaram, Antoine Grimod} + +\frame{\titlepage} + \section{Structure of the compiler} \begin{frame}{Main ideas} \begin{figure} @@ -97,35 +104,49 @@ \section{Passes} \begin{frame}{Passes} - \begin{block}{Classification} - The passes of our compiler are functions of taking a program and either: + \begin{block}{Sanity checks} \begin{itemize} - \item returning a program if the pass succeeded - \item returns nothing otherwise + \item Check the well-typedness of a program + \item Check that there are no assignment conflicts in a programs + \end{itemize} + \end{block} + \begin{block}{AST modification} + \begin{itemize} + \item Rewrite automata into \texttt{if-then-else} constructs + \item Linearization of the equations + \item (no longer required) Push the \texttt{pre} to variables \end{itemize} - - We only have one language in our compiler: no intermediary language. \end{block} \end{frame} -\subsection{Check} +\section{Translation to C} \begin{frame} - \begin{block}{Passes} - The passes can be split into: - \begin{itemize} - \item those checking the program validity - \item those modifying the AST of the program - \end{itemize} - \end{block} + \centerline{\Huge TODO $\boxed{\ddot\smile}$} \end{frame} -\begin{frame}{Implemented passes} - \begin{block}{\texttt{pre}-propagation to leaves} - \end{block} - \begin{block}{Check: unique initialization for variables} - \end{block} - \begin{block}{Linearization of the equations} - \end{block} +\section{Tests} +\begin{frame}{Tests} + \begin{block}{testing methods} + We thought of three testing methods: + \begin{itemize} + \item manual testing of our functionalities + \item run the sanity-checks-passes after any AST-altering pass + \item simulation of the nodes (aborted) + \end{itemize} + \end{block} +\end{frame} + +\section{Possible improvements} +\begin{frame}{Improvements} + \begin{itemize} + \item Increase the expressivity of the accepted programs + \item Improve the complexity of the different passes + \begin{itemize} + \item Group neighbour passes of the same type (node-, expression or + equation-pass). + \end{itemize} + \item \dots{} + \end{itemize} \end{frame} \end{document} diff --git a/src/main.ml b/src/main.ml index 450e81d..3652564 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 = ["automata_validity" ;"automata_translation"; "linearization"; "pre2vars"; "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,8 @@ 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 ad8ff30..2918d32 100644 --- a/src/passes.ml +++ b/src/passes.ml @@ -137,9 +137,9 @@ let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option in let add_var_in = add_var 1 in let add_var_loc = add_var 0 in - List.iter add_var_in (snd node.n_inputs); List.iter add_var_loc (snd node.n_outputs); List.iter add_var_loc (snd node.n_local_vars); + List.iter add_var_in (snd node.n_inputs); (** Usual Equations *) incr_eqlist h node.n_equations; if check_now h = false @@ -173,18 +173,100 @@ 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 rec pre_aux_expression vars expr: t_eqlist * t_varlist * t_expression = + match expr with + | EVar _ -> [], vars, expr + | EMonOp (t, op, e) -> + begin + match op with + | MOp_pre -> + let eqs, vars, e = pre_aux_expression vars e in + let nvar: string = fresh_var_name vars 6 in + let nvar = match t with + | [TInt] -> IVar nvar + | [TBool] -> BVar nvar + | [TReal] -> RVar nvar + | _ -> failwith "Should not happened." in + let neq_patt: t_varlist = (t, [nvar]) in + let neq_expr: t_expression = e in + let vars = varlist_concat (t, [nvar]) vars in + (neq_patt, neq_expr) :: eqs, vars, EMonOp (t, MOp_pre, EVar (t, nvar)) + | _ -> + let eqs, vars, e = pre_aux_expression vars e in + eqs, vars, EMonOp (t, op, e) + end + | EBinOp (t, op, e, e') -> + let eqs, vars, e = pre_aux_expression vars e in + let eqs', vars, e' = pre_aux_expression vars e' in + eqs @ eqs', vars, EBinOp (t, op, e, e') + | ETriOp (t, op, e, e', e'') -> + let eqs, vars, e = pre_aux_expression vars e in + let eqs', vars, e' = pre_aux_expression vars e' in + let eqs'', vars, e'' = pre_aux_expression vars e'' in + eqs @ eqs' @ eqs'', vars, ETriOp (t, op, e, e', e'') + | EComp (t, op, e, e') -> + let eqs, vars, e = pre_aux_expression vars e in + let eqs', vars, e' = pre_aux_expression vars e' in + eqs @ eqs', vars, EComp (t, op, e, e') + | EWhen (t, e, e') -> + let eqs, vars, e = pre_aux_expression vars e in + let eqs', vars, e' = pre_aux_expression vars e' in + eqs @ eqs', vars, EWhen (t, e, e') + | EReset (t, e, e') -> + let eqs, vars, e = pre_aux_expression vars e in + let eqs', vars, e' = pre_aux_expression vars e' in + eqs @ eqs', vars, EReset (t, e, e') + | EConst _ -> [], vars, expr + | ETuple (t, l) -> + let eqs, vars, l = List.fold_right + (fun e (eqs, vars, l) -> + let eqs', vars, e = pre_aux_expression vars e in + eqs' @ eqs, vars, (e :: l)) + l ([], vars, []) in + eqs, vars, ETuple (t, l) + | EApp (t, n, e) -> + let eqs, vars, e = pre_aux_expression vars e in + eqs, vars, EApp (t, n, e) + in + let rec pre_aux_equation (vars: t_varlist) ((patt, expr): t_equation) = + let eqs, vars, expr = pre_aux_expression vars expr in + (patt, expr)::eqs, vars + in + 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_equations = List.flatten - begin - List.map - (tpl debug) - node.n_equations - end in + (List.map + tpl + node.n_equations) + in + let new_equations, new_locvars = + List.fold_left + (fun (eqs, vars) eq -> + let es, vs = pre_aux_equation vars eq in + es @ eqs, vars) + ([], node.n_local_vars) + new_equations + in Some { n_name = node.n_name; n_inputs = node.n_inputs; n_outputs = node.n_outputs; - n_local_vars = node.n_local_vars; + n_local_vars = new_locvars; n_equations = new_equations; n_automata = node.n_automata; } @@ -295,28 +377,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 +420,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 +439,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 +494,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,6 +518,10 @@ 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 = + node_pass (automata_trans_pass debug) + + diff --git a/src/test.node b/src/test.node index ef459bb..03d9db8 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 @@ -13,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 diff --git a/src/test2.node b/src/test2.node index 36209a1..2116ba7 100644 --- a/src/test2.node +++ b/src/test2.node @@ -1,7 +1,4 @@ -node diagonal_int (i: int) returns (o1, o2 : int); -var y: int; +node main (i: int) returns (o1: int); let - o2 = y; - y = i; - o1 = i; + o1 = 10 -> pre (20 -> 30); tel