Compare commits

..

No commits in common. "530f6ddf518418e785ae10cbb0afdc210895ddcd" and "21414e6461c85ea20a9cf0d19bb2c5b3e4a989e9" have entirely different histories.

5 changed files with 61 additions and 180 deletions

View File

@ -6,13 +6,6 @@
\begin{document} \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} \section{Structure of the compiler}
\begin{frame}{Main ideas} \begin{frame}{Main ideas}
\begin{figure} \begin{figure}
@ -104,49 +97,35 @@
\section{Passes} \section{Passes}
\begin{frame}{Passes} \begin{frame}{Passes}
\begin{block}{Sanity checks} \begin{block}{Classification}
The passes of our compiler are functions of taking a program and either:
\begin{itemize} \begin{itemize}
\item Check the well-typedness of a program \item returning a program if the pass succeeded
\item Check that there are no assignment conflicts in a programs \item returns nothing otherwise
\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} \end{itemize}
We only have one language in our compiler: no intermediary language.
\end{block} \end{block}
\end{frame} \end{frame}
\section{Translation to C} \subsection{Check}
\begin{frame} \begin{frame}
\centerline{\Huge TODO $\boxed{\ddot\smile}$} \begin{block}{Passes}
\end{frame} The passes can be split into:
\section{Tests}
\begin{frame}{Tests}
\begin{block}{testing methods}
We thought of three testing methods:
\begin{itemize} \begin{itemize}
\item manual testing of our functionalities \item those checking the program validity
\item run the sanity-checks-passes after any AST-altering pass \item those modifying the AST of the program
\item simulation of the nodes (aborted)
\end{itemize} \end{itemize}
\end{block} \end{block}
\end{frame} \end{frame}
\section{Possible improvements} \begin{frame}{Implemented passes}
\begin{frame}{Improvements} \begin{block}{\texttt{pre}-propagation to leaves}
\begin{itemize} \end{block}
\item Increase the expressivity of the accepted programs \begin{block}{Check: unique initialization for variables}
\item Improve the complexity of the different passes \end{block}
\begin{itemize} \begin{block}{Linearization of the equations}
\item Group neighbour passes of the same type (node-, expression or \end{block}
equation-pass).
\end{itemize}
\item \dots{}
\end{itemize}
\end{frame} \end{frame}
\end{document} \end{document}

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 = ["pre2vars"; "linearization"; "equations_ordering"] 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] \
@ -67,8 +67,6 @@ let _ =
[ [
("pre2vars", Passes.pre2vars); ("pre2vars", Passes.pre2vars);
("chkvar_init_unicity", Passes.chkvar_init_unicity); ("chkvar_init_unicity", Passes.chkvar_init_unicity);
("automata_translation", Passes.automata_translation_pass);
("automata_validity", Passes.check_automata_validity);
("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);

View File

@ -137,9 +137,9 @@ let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option
in in
let add_var_in = add_var 1 in let add_var_in = add_var 1 in
let add_var_loc = add_var 0 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_outputs);
List.iter add_var_loc (snd node.n_local_vars); List.iter add_var_loc (snd node.n_local_vars);
List.iter add_var_in (snd node.n_inputs);
(** Usual Equations *) (** Usual Equations *)
incr_eqlist h node.n_equations; incr_eqlist h node.n_equations;
if check_now h = false if check_now h = false
@ -173,100 +173,18 @@ let rec tpl debug ((pat, exp): t_equation) =
let pass_linearization verbose debug main_fn = let pass_linearization verbose debug main_fn =
let node_lin (node: t_node): t_node option = 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 let new_equations = List.flatten
(List.map begin
tpl List.map
node.n_equations) (tpl debug)
in node.n_equations
let new_equations, new_locvars = end in
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 Some
{ {
n_name = node.n_name; n_name = node.n_name;
n_inputs = node.n_inputs; n_inputs = node.n_inputs;
n_outputs = node.n_outputs; n_outputs = node.n_outputs;
n_local_vars = new_locvars; n_local_vars = node.n_local_vars;
n_equations = new_equations; n_equations = new_equations;
n_automata = node.n_automata; n_automata = node.n_automata;
} }
@ -377,7 +295,6 @@ let pass_typing verbose debug main_fn ast =
else None else None
in aux ast in aux ast
let check_automata_validity verbos debug main_fn =
let check_automaton_branch_vars automaton = let check_automaton_branch_vars automaton =
let (init, states) = automaton in let (init, states) = automaton in
let left_side = Hashtbl.create 10 in let left_side = Hashtbl.create 10 in
@ -400,12 +317,6 @@ let check_automata_validity verbos debug main_fn =
if not validity then if not validity then
failwith "Automaton branch has different variables assignment in different branches" failwith "Automaton branch has different variables assignment in different branches"
end end
in
let aux node =
List.iter check_automaton_branch_vars node.n_automata;
Some node
in
node_pass aux
let automaton_translation debug automaton = let automaton_translation debug automaton =
let gathered = Hashtbl.create 10 in let gathered = Hashtbl.create 10 in
@ -420,7 +331,7 @@ let automaton_translation debug automaton =
let rec init_state_translation states c = match states with let rec init_state_translation states c = match states with
| [] -> () | [] -> ()
| State(name, _, _, _)::q -> | State(name, _, _, _)::q ->
Hashtbl.replace state_to_int name c; (init_state_translation q (c+1)) Hashtbl.replace state_to_int name c; (init_state_translation q c)
in in
let rec find_state name = let rec find_state name =
@ -439,20 +350,14 @@ let automaton_translation debug automaton =
let flatten_state state = match state with let flatten_state state = match state with
| State(name, eq, cond, next) -> | 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 let new_equations = List.flatten
begin begin
List.map List.map
(tpl debug) (tpl debug)
eq eq
end in end in
*) equation_pass name new_equations;
equation_pass name eq; State(name, new_equations, cond, next)
State(name, eq, cond, next)
in in
let rec transition_eq states s = let rec transition_eq states s =
@ -494,7 +399,7 @@ let automaton_translation debug automaton =
let (init, states) = flatten_automaton automaton in let (init, states) = flatten_automaton automaton in
let s = create_automaton_name () in let s = create_automaton_name () in
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 = 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)::acc) gathered new_equations, IVar(s)
@ -518,10 +423,6 @@ let automata_trans_pass debug (node:t_node) : t_node option=
n_outputs = node.n_outputs; n_outputs = node.n_outputs;
n_local_vars = (new_ty@ty, vars@loc_vars); n_local_vars = (new_ty@ty, vars@loc_vars);
n_equations = eqs@node.n_equations; n_equations = eqs@node.n_equations;
n_automata = []; (* not needed anymore *) n_automata = node.n_automata;
} }
let automata_translation_pass verbose debug main_fn =
node_pass (automata_trans_pass debug)

View File

@ -1,4 +1,5 @@
node diagonal_int (i: int) returns (o1, o2 : int); node diagonal_int (i: int) returns (o1, o2 : int);
var i: int;
let let
(o1, o2) = (i, i); (o1, o2) = (i, i);
tel tel
@ -12,10 +13,9 @@ let
tel tel
node auto (i: int) returns (o : int); node auto (i: int) returns (o : int);
var x, y:int;
let let
automaton automaton
| Incr -> do (o,x) = (0 fby o + 1, 2); done | Incr -> do o = (pre o) + 1; done
| Decr -> do (o,x) = diagonal_int(0 fby o); done | Decr -> do o = (pre o) - 1; done
tel tel

View File

@ -1,4 +1,7 @@
node main (i: int) returns (o1: int); node diagonal_int (i: int) returns (o1, o2 : int);
var y: int;
let let
o1 = 10 -> pre (20 -> 30); o2 = y;
y = i;
o1 = i;
tel tel