This commit is contained in:
Benjamin Loison 2022-12-16 04:47:05 +01:00
commit ea94bb84dd
5 changed files with 173 additions and 61 deletions

View File

@ -97,35 +97,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, ((fst vs) @ (fst vars), (snd vs) @ (snd 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