Compare commits

..

15 Commits

Author SHA1 Message Date
73b753bec2 Merge branch 'master' of https://gitea.lemnoslife.com/Benjamin_Loison/Synchronous_reactive_systems 2022-12-16 05:57:55 +01:00
530f6ddf51 Merge branch 'master' of https://gitea.lemnoslife.com/Benjamin_Loison/Synchronous_reactive_systems 2022-12-16 05:55:15 +01:00
Arnaud DABY-SEESARAM
57dd9c1aa4 [passes] linearozation: avoir duplication of variables 2022-12-16 14:16:13 +01:00
21414e6461 Make last equation of a node potentially not ending with a semi column
Otherwise the following code:

```
-- count the number of top between two tick
node counting (tick:bool; top:bool)
returns (o: bool);
	var v: int;
	let o = if tick then v else 0 -> pre o + v;
		v = if top then 1 else 0
	tel;
```

was involving the following error:

```
Syntax error at <line 1: -- count the number of top between two tick >
```
2022-12-16 05:54:41 +01:00
c37e819f1a Add a title frame to the beamer 2022-12-16 05:06:27 +01:00
ea94bb84dd Merge branch 'master' of https://gitea.lemnoslife.com/Benjamin_Loison/Synchronous_reactive_systems 2022-12-16 04:47:05 +01:00
Arnaud DABY-SEESARAM
3fa0f92233 [beamer] A few straight forward slides added 2022-12-16 10:45:20 +01:00
Arnaud DABY-SEESARAM
3417d75620 [passes] linearisation: correction (10 -> pre (20 -> 30)) works 2022-12-16 09:44:50 +01:00
7c2c43fe24 Precise to what extent considering integers work fine with working with floats instead 2022-12-16 01:20:42 +01:00
Arnaud DABY-SEESARAM
c7a97f3305 [passes] linearization: merge fix 2022-12-16 09:00:03 +01:00
Arnaud DABY-SEESARAM
8d6349dd3f Merge remote-tracking branch 'origin/master' into wip 2022-12-16 08:53:55 +01:00
Arnaud DABY-SEESARAM
d7f0f148e9 [pre linearization] done, not tested 2022-12-16 08:52:48 +01:00
dsac
9987922e0f [passes] linearization of pre (wip) 2022-12-16 07:47:20 +01:00
Antoine Grimod
6af9ddf394 added pass to check validity of automata and disable flattening of automaton branch because of incorrect code resulting from it 2022-12-16 01:04:09 +01:00
Antoine Grimod
1b3af051b3 adding automaton translation pass to list of executed passes 2022-12-16 00:06:51 +01:00
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: \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}

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 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)

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