Compare commits
15 Commits
a0383dbf13
...
73b753bec2
Author | SHA1 | Date | |
---|---|---|---|
73b753bec2 | |||
530f6ddf51 | |||
|
57dd9c1aa4 | ||
21414e6461 | |||
c37e819f1a | |||
ea94bb84dd | |||
|
3fa0f92233 | ||
|
3417d75620 | ||
7c2c43fe24 | |||
|
c7a97f3305 | ||
|
8d6349dd3f | ||
|
d7f0f148e9 | ||
|
9987922e0f | ||
|
6af9ddf394 | ||
|
1b3af051b3 |
@ -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:
|
\end{frame}
|
||||||
|
|
||||||
|
\section{Tests}
|
||||||
|
\begin{frame}{Tests}
|
||||||
|
\begin{block}{testing methods}
|
||||||
|
We thought of three testing methods:
|
||||||
\begin{itemize}
|
\begin{itemize}
|
||||||
\item those checking the program validity
|
\item manual testing of our functionalities
|
||||||
\item those modifying the AST of the program
|
\item run the sanity-checks-passes after any AST-altering pass
|
||||||
|
\item simulation of the nodes (aborted)
|
||||||
\end{itemize}
|
\end{itemize}
|
||||||
\end{block}
|
\end{block}
|
||||||
\end{frame}
|
\end{frame}
|
||||||
|
|
||||||
\begin{frame}{Implemented passes}
|
\section{Possible improvements}
|
||||||
\begin{block}{\texttt{pre}-propagation to leaves}
|
\begin{frame}{Improvements}
|
||||||
\end{block}
|
\begin{itemize}
|
||||||
\begin{block}{Check: unique initialization for variables}
|
\item Increase the expressivity of the accepted programs
|
||||||
\end{block}
|
\item Improve the complexity of the different passes
|
||||||
\begin{block}{Linearization of the equations}
|
\begin{itemize}
|
||||||
\end{block}
|
\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}
|
||||||
|
@ -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);
|
||||||
|
125
src/passes.ml
125
src/passes.ml
@ -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 new_equations = List.flatten
|
let rec pre_aux_expression vars expr: t_eqlist * t_varlist * t_expression =
|
||||||
|
match expr with
|
||||||
|
| EVar _ -> [], vars, expr
|
||||||
|
| EMonOp (t, op, e) ->
|
||||||
begin
|
begin
|
||||||
List.map
|
match op with
|
||||||
(tpl debug)
|
| MOp_pre ->
|
||||||
node.n_equations
|
let eqs, vars, e = pre_aux_expression vars e in
|
||||||
end 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
|
||||||
|
(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
|
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,7 +377,8 @@ 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 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
|
||||||
|
|
||||||
@ -317,6 +400,12 @@ let check_automaton_branch_vars automaton =
|
|||||||
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
|
||||||
@ -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)
|
||||||
|
|
||||||
|
|
||||||
|
@ -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
|
||||||
|
|
||||||
|
@ -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
|
||||||
|
Loading…
Reference in New Issue
Block a user