This commit is contained in:
Benjamin Loison 2022-12-16 05:55:15 +01:00
commit 530f6ddf51
5 changed files with 180 additions and 61 deletions

View File

@ -6,6 +6,13 @@
\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}
@ -97,35 +104,49 @@
\section{Passes} \section{Passes}
\begin{frame}{Passes} \begin{frame}{Passes}
\begin{block}{Classification} \begin{block}{Sanity checks}
The passes of our compiler are functions of taking a program and either:
\begin{itemize} \begin{itemize}
\item returning a program if the pass succeeded \item Check the well-typedness of a program
\item returns nothing otherwise \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} \end{itemize}
We only have one language in our compiler: no intermediary language.
\end{block} \end{block}
\end{frame} \end{frame}
\subsection{Check} \section{Translation to C}
\begin{frame} \begin{frame}
\begin{block}{Passes} \centerline{\Huge TODO $\boxed{\ddot\smile}$}
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}
\end{frame} \end{frame}
\begin{frame}{Implemented passes} \section{Tests}
\begin{block}{\texttt{pre}-propagation to leaves} \begin{frame}{Tests}
\end{block} \begin{block}{testing methods}
\begin{block}{Check: unique initialization for variables} We thought of three testing methods:
\end{block} \begin{itemize}
\begin{block}{Linearization of the equations} \item manual testing of our functionalities
\end{block} \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{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 = ["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 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,6 +67,8 @@ 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,18 +173,100 @@ 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
begin (List.map
List.map tpl
(tpl debug) node.n_equations)
node.n_equations in
end 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 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 = node.n_local_vars; n_local_vars = new_locvars;
n_equations = new_equations; n_equations = new_equations;
n_automata = node.n_automata; n_automata = node.n_automata;
} }
@ -295,28 +377,35 @@ let pass_typing verbose debug main_fn ast =
else None else None
in aux ast in aux ast
let check_automaton_branch_vars automaton = let check_automata_validity verbos debug main_fn =
let (init, states) = automaton in let check_automaton_branch_vars automaton =
let left_side = Hashtbl.create 10 in let (init, states) = automaton in
let left_side = Hashtbl.create 10 in
let rec init_left_side eqlist = match eqlist with let rec init_left_side eqlist = match eqlist with
| [] -> () | [] -> ()
| (varlist, exp)::q -> | (varlist, exp)::q ->
begin begin
Hashtbl.add left_side varlist true; Hashtbl.add left_side varlist true;
init_left_side q; init_left_side q;
end 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 in
let check_state s = match s with let aux node =
| State(name, eqs, cond, next) -> List.iter check_automaton_branch_vars node.n_automata;
List.for_all (fun (varlist, exp) -> (Hashtbl.mem left_side varlist)) eqs Some node
in in
begin node_pass aux
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 automaton_translation debug automaton =
let gathered = Hashtbl.create 10 in 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 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) Hashtbl.replace state_to_int name c; (init_state_translation q (c+1))
in in
let rec find_state name = let rec find_state name =
@ -350,14 +439,20 @@ 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; *)
State(name, new_equations, cond, next) equation_pass name eq;
State(name, eq, cond, next)
in in
let rec transition_eq states s = let rec transition_eq states s =
@ -399,7 +494,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 = 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)::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_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 = node.n_automata; n_automata = []; (* not needed anymore *)
} }
let automata_translation_pass verbose debug main_fn =
node_pass (automata_trans_pass debug)

View File

@ -1,5 +1,4 @@
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
@ -13,9 +12,10 @@ 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 = (pre o) + 1; done | Incr -> do (o,x) = (0 fby o + 1, 2); done
| Decr -> do o = (pre o) - 1; done | Decr -> do (o,x) = diagonal_int(0 fby o); done
tel tel

View File

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