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}
\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}

View File

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

View File

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

View File

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

View File

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