Benjamin_Loison/Synchronous_reactive_systems
1
0
Fork 0
Code Issues 7 Pull Requests Packages Projects Releases Wiki Activity

[passes] linearization of tuple-equations + deletion of unused pass

Browse Source
This commit is contained in:
Arnaud DABY-SEESARAM 2022-12-18 19:00:24 +01:00
parent aa7f7514d3
commit c344f125e5
3 changed files with 42 additions and 119 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/main.ml
View File

@ -9,12 +9,12 @@ let print_debug d s =
let print_verbose v s =
if v then Format.printf "\x1b[33;01;04mStatus:\x1b[0m %s\n" s else ()
let exec_passes ast main_fn verbose debug passes f =
let exec_passes ast verbose debug passes f =
let rec aux ast = function
| [] -> f ast
| (n, p) :: passes ->
verbose (Format.asprintf "Executing pass %s:\n" n);
match p verbose debug main_fn ast with
match p verbose debug ast with
| None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0)
| Some ast -> (
debug (Format.asprintf "Current AST (after %s):\n%a\n" n Lustre_pp.pp_ast ast);
@ -25,7 +25,7 @@ let exec_passes ast main_fn verbose debug passes f =
let _ =
(** Usage and argument parsing. *)
let default_passes = [] in
let default_passes = ["linearization_tuples"; "linearization"] in
let sanity_passes = ["chkvar_init_unicity"; "check_typing"] in
let usage_msg =
"Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
@ -57,13 +57,12 @@ let _ =
if !passes = [] then passes := default_passes;
let print_verbose = print_verbose !verbose in
let print_debug = print_debug !debug in
let main_fn = "main" in
(** Definition of the passes table *)
let passes_table = Hashtbl.create 100 in
List.iter (fun (s, k) -> Hashtbl.add passes_table s k)
[
("pre2vars", Passes.pre2vars);
("linearization_tuples", Passes.pass_linearization_tuples);
("chkvar_init_unicity", Passes.chkvar_init_unicity);
("automata_translation", Passes.automata_translation_pass);
("automata_validity", Passes.check_automata_validity);
@ -120,7 +119,7 @@ let _ =
print_debug (Format.asprintf "Initial AST (before executing any passes):\n%a"
Lustre_pp.pp_ast ast) ;
exec_passes ast main_fn print_verbose print_debug passes
exec_passes ast print_verbose print_debug passes
begin
if !ppast
then (Format.printf "%a" Lustre_pp.pp_ast)

132
src/passes.ml
View File

@ -4,88 +4,29 @@ open Ast
open Passes_utils
open Utils
let pre2vars verbose debug main_fn =
let rec all_pre expr =
let rec split_tuple (eq: t_equation): t_eqlist =
let patt, expr = eq in
match expr with
| EMonOp (ty, MOp_pre, expr) -> all_pre expr
| EMonOp _ -> false
| EVar _ -> true
| _ -> false
in
let rec pre_push expr : t_expression =
match expr with
| EVar _ -> EMonOp (type_exp expr, MOp_pre, expr)
| EConst _ -> expr (** pre(c) = c for any constant c *)
| EMonOp (ty, mop, expr) ->
| ETuple (_, expr_h :: expr_t) ->
begin
match mop with
| MOp_pre ->
if all_pre expr
then EMonOp (ty, mop, EMonOp (ty, mop, expr))
else pre_push (pre_push expr)
| _ -> EMonOp (ty, mop, pre_push expr)
let t_l = type_exp expr_h in
let patt_l, patt_r = list_select (List.length t_l) (snd patt) in
let t_r = List.flatten (List.map type_var patt_r) in
((t_l, patt_l), expr_h) ::
split_tuple ((t_r, patt_r), ETuple (t_r, expr_t))
end
| EBinOp (ty, bop, expr, expr') ->
let expr = pre_push expr in let expr' = pre_push expr' in
EBinOp (ty, bop, expr, expr')
| ETriOp (ty, top, expr, expr', expr'') ->
let expr = pre_push expr in let expr' = pre_push expr' in
let expr'' = pre_push expr'' in
ETriOp (ty, top, expr, expr', expr'')
| EComp (ty, cop, expr, expr') ->
let expr = pre_push expr in let expr' = pre_push expr' in
EComp (ty, cop, expr, expr')
| EWhen (ty, expr, expr') ->
let expr = pre_push expr in let expr' = pre_push expr' in
EWhen (ty, expr, expr')
| EReset (ty, expr, expr') ->
let expr = pre_push expr in let expr' = pre_push expr' in
EReset (ty, expr, expr')
| ETuple (ty, elist) ->
let elist =
List.fold_right (fun expr acc -> (pre_push expr) :: acc) elist [] in
ETuple (ty, elist)
| EApp (ty, node, arg) ->
let arg = pre_push arg in
EApp (ty, node, arg)
in
let rec aux (expr: t_expression) =
match expr with
| EVar _ -> expr
| EMonOp (ty, mop, expr) ->
begin
match mop with
| MOp_pre -> pre_push expr
| _ -> let expr = aux expr in EMonOp (ty, mop, expr)
end
| EBinOp (ty, bop, expr, expr') ->
let expr = aux expr in let expr' = aux expr' in
EBinOp (ty, bop, expr, expr')
| ETriOp (ty, top, expr, expr', expr'') ->
let expr = aux expr in let expr' = aux expr' in
let expr'' = aux expr'' in
ETriOp (ty, top, expr, expr', expr'')
| EComp (ty, cop, expr, expr') ->
let expr = aux expr in let expr' = aux expr' in
EComp (ty, cop, expr, expr')
| EWhen (ty, expr, expr') ->
let expr = aux expr in let expr' = aux expr' in
EWhen (ty, expr, expr')
| EReset (ty, expr, expr') ->
let expr = aux expr in let expr' = aux expr' in
EReset (ty, expr, expr')
| EConst (ty, c) -> EConst (ty, c)
| ETuple (ty, elist) ->
let elist =
List.fold_right (fun expr acc -> (aux expr) :: acc) elist [] in
ETuple (ty, elist)
| EApp (ty, node, arg) ->
let arg = aux arg in
EApp (ty, node, arg)
in
expression_pass (somify aux)
| ETuple (_, []) -> []
| _ -> [eq]
let chkvar_init_unicity verbose debug main_fn : t_nodelist -> t_nodelist option =
let pass_linearization_tuples verbose debug =
let aux_linearization_tuples node =
let new_equations = List.flatten (List.map split_tuple node.n_equations) in
Some { node with n_equations = new_equations }
in
node_pass aux_linearization_tuples
let chkvar_init_unicity verbose debug : t_nodelist -> t_nodelist option =
let aux (node: t_node) : t_node option =
let incr_aux h n =
match Hashtbl.find_opt h n with
@ -171,7 +112,7 @@ let rec tpl debug ((pat, exp): t_equation) =
| ETuple (_, []) -> []
| _ -> [(pat, exp)]
let pass_linearization verbose debug main_fn =
let pass_linearization verbose debug =
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
@ -237,34 +178,13 @@ let pass_linearization verbose debug main_fn =
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, vs)
([], node.n_local_vars)
new_equations
node.n_equations
in
Some
{
@ -278,7 +198,7 @@ let pass_linearization verbose debug main_fn =
in
node_pass node_lin
let pass_eq_reordering verbose debug main_fn ast =
let pass_eq_reordering verbose debug ast =
let rec pick_equations init_vars eqs remaining_equations =
match remaining_equations with
| [] -> Some eqs
@ -312,7 +232,7 @@ let pass_eq_reordering verbose debug main_fn ast =
in
node_pass node_eq_reorganising ast
let pass_typing verbose debug main_fn ast =
let pass_typing verbose debug ast =
let htbl = Hashtbl.create (List.length ast) in
let () = debug "[typing verification]" in
let () = List.iter
@ -382,7 +302,7 @@ let pass_typing verbose debug main_fn ast =
else None
in aux ast
let check_automata_validity verbos debug main_fn =
let check_automata_validity verbos debug =
let check_automaton_branch_vars automaton =
let (init, states) = automaton in
let left_side = Hashtbl.create 10 in
@ -539,10 +459,10 @@ let automata_trans_pass debug (node:t_node) : t_node option=
n_automata = []; (* not needed anymore *)
}
let automata_translation_pass verbose debug main_fn =
let automata_translation_pass verbose debug =
node_pass (automata_trans_pass debug)
let clock_unification_pass verbose debug main_fn ast =
let clock_unification_pass verbose debug ast =
let failure str = raise (PassExn ("Failed to unify clocks: "^str)) in

12
src/test.node
View File

@ -1,6 +1,10 @@
node n (i: int) returns (o: int);
var v: int;
node my_and (a, b: bool) returns (o: bool);
let
o = 1;
v = pre o;
o = a and b;
tel
node n (i: int) returns (o: int);
var v: bool;
let
(o, v) = (1, my_and (pre o = 8, pre v));
tel