Compare commits

..

No commits in common. "master" and "ast2C_proposition" have entirely different histories.

19 changed files with 287 additions and 627 deletions

8
TODO Normal file
View File

@ -0,0 +1,8 @@
# Parseur
- tests divers et variés
- support pour un point-virgule optionel en fin de nœud
- ajout des flottants (= réels)
- ajout de pre, ->, fby, automates
# ...

View File

@ -1,12 +1,12 @@
node auto (i: int) returns (o : int);
var x, y: int;
var x, y:int;
let
automaton
| Incr -> do (o,x) = (0 fby o + 1, 2); until o < 5 then Decr
| Decr -> do (o,x) = diagonal_int(0 fby o); until o > 3 then Incr
tel
node auto (i: int) returns (o : int);
node auto (i: int) returns (o: int);
var x, y: int;
let
_s1 = 1 -> (if _s = 1 and o < 5 then 2 else if _s = 2 and o > then 1 else 1);
@ -14,7 +14,7 @@ let
tel
node auto (i: int) returns (o : int);
var x, y: int;
var x, y:int;
let
automaton
| Incr -> do (o,x) = (0 fby o + 1, 2); until o < 5 then Decr

View File

@ -55,7 +55,7 @@ and t_equation = t_varlist * t_expression
and t_eqlist = t_equation list
and t_state = | State of ident * t_eqlist * (t_expression list) * (ident list)
and t_state = | State of ident * t_eqlist * t_expression * ident
and t_automaton = t_state * t_state list
@ -77,4 +77,3 @@ type t_ck = base_ck list
and base_ck =
| Base
| On of base_ck * t_expression
| Unknown

View File

@ -215,11 +215,11 @@ let cp_prevars fmt (node, h) =
match Hashtbl.find_opt node_st.nt_map (v, false) with
| Some (src_array, src_idx) ->
let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
Format.fprintf fmt "\t_state->%s[%d] = _state->%s[%d];\n"
Format.fprintf fmt "\tstate->%s[%d] = state->%s[%d];\n"
dst_array dst_idx src_array src_idx
| None ->
let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in
Format.fprintf fmt "\t_state->%s[%d] = %s;\n"
Format.fprintf fmt "\tstate->%s[%d] = %s;\n"
dst_array dst_idx v
)
(List.map Utils.name_of_var l)
@ -236,11 +236,11 @@ let cp_init_aux_nodes fmt (node, h) =
| None -> () (** All auxiliary nodes have been initialized *)
| Some n ->
begin
Format.fprintf fmt "%a\t\tif(!_state->is_reset) {\n\
\t\t\t_state->aux_states[%d] = calloc (1, sizeof (%s));\n\
Format.fprintf fmt "%a\t\tif(!state->is_reset) {\n\
\t\t\tstate->aux_states[%d] = calloc (1, sizeof (%s));\n\
\t\t}\n\
\t\t((%s*)(_state->aux_states[%d]))->is_init = true;\n\
\t\t((%s*)(_state->aux_states[%d]))->is_reset = _state->is_reset;\n"
\t\t((%s*)(state->aux_states[%d]))->is_init = true;\n\
\t\t((%s*)(state->aux_states[%d]))->is_reset = state->is_reset;\n"
aux (node, nst, i-1)
(i-1) (Format.asprintf "t_state_%s" n.n_name)
(Format.asprintf "t_state_%s" n.n_name) (i-1)
@ -252,7 +252,7 @@ let cp_init_aux_nodes fmt (node, h) =
then ()
else begin
Format.fprintf fmt "\t/* Initialize the auxiliary nodes */\n\
\tif (_state->is_init) {\n%a\t}\n\n\n"
\tif (state->is_init) {\n%a\t}\n\n\n"
aux (node, nst, nst.nt_count_app)
end
@ -270,12 +270,12 @@ let cp_equations fmt (eqs, hloc, h) =
List.map (fun eq -> equation_to_expression (hloc, h, eq)) eqs in
let main_block = remove_ifnot main_block in
let main_block = merge_neighbour_ifs main_block in
Format.fprintf fmt "\t/*Main code:*/\n%a"
Format.fprintf fmt "\t/*Main code :*/\n%a"
cp_block (main_block, hloc.nt_map)
(** [cp_node] prints a single node *)
let cp_node fmt (node, h) =
Format.fprintf fmt "%a\n{\n%a%a\n\n\t_state->is_init = false;\n%a}\n"
Format.fprintf fmt "%a\n{\n%a%a\n\n\tstate->is_init = false;\n%a}\n"
cp_prototype (node, h)
cp_init_aux_nodes (node, h)
cp_equations (node.in_equations, Hashtbl.find h node.in_name, h)
@ -310,12 +310,12 @@ let dump_var_locations fmt (st: node_states) =
(** main function that prints a C-code from a term of type [t_nodelist]. *)
let ast_to_c fmt verbose debug prog =
let ast_to_c verbose debug prog =
verbose "Computation of the node_states";
let prog_st_types = make_state_types prog in
debug (Format.asprintf "%a" dump_var_locations prog_st_types);
let iprog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in
Format.fprintf fmt "%a\n\n#define BUFFER_SIZE 1024\n\n%a\n\n%a\n\n/* Nodes: */\n%a%a\n"
Format.printf "%a\n\n%a\n\n%a\n\n/* Nodes: */\n%a%a\n"
cp_includes (Config.c_includes)
cp_state_types prog_st_types
cp_state_frees (iprog, prog_st_types)

View File

@ -95,7 +95,7 @@ let cp_state_frees fmt (iprog, sts) =
then
Format.fprintf fmt "\tif (st->aux_states[%d]) {\n\
\t\tfree_state_%s((t_state_%s*)(st->aux_states[%d]));\n\
\t\tfree (st->aux_states[%d]);\n\t}\n%a"
\t\tfree (st->aux_state[%d]);\n\t}\n%a"
idx callee_name callee_name idx
idx cp_free_aux (i+1, caller_name)
else Format.fprintf fmt "\tif (st->aux_states[%d])\n\
@ -124,7 +124,7 @@ let cp_state_frees fmt (iprog, sts) =
let cp_var' fmt = function
| CVStored (arr, idx) -> Format.fprintf fmt "_state->%s[%d]" arr idx
| CVStored (arr, idx) -> Format.fprintf fmt "state->%s[%d]" arr idx
| CVInput s -> Format.fprintf fmt "%s" s
let cp_var fmt = function
@ -170,7 +170,7 @@ let cp_prototype fmt (node, h): unit =
| None -> failwith "This should not happened!"
| Some nst ->
begin
Format.fprintf fmt "void fn_%s (%s *_state, %a)"
Format.fprintf fmt "void fn_%s (%s *state, %a)"
node.in_name
nst.nt_name
cp_varlist node.in_inputs
@ -211,7 +211,7 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) =
in
match value with
| CVariable (CVInput s) -> Format.fprintf fmt "%s" s
| CVariable (CVStored (arr, idx)) -> Format.fprintf fmt "_state->%s[%d]" arr idx
| CVariable (CVStored (arr, idx)) -> Format.fprintf fmt "state->%s[%d]" arr idx
| CConst (CInt i) -> Format.fprintf fmt "%d" i
| CConst (CBool b) -> Format.fprintf fmt "%s" (Bool.to_string b)
| CConst (CReal r) -> Format.fprintf fmt "%f" r
@ -227,9 +227,9 @@ let rec cp_value fmt (value, (hloc: (ident * bool, string * int) Hashtbl.t)) =
end
| CVInput n -> n) in
let (arr, idx) = Hashtbl.find hloc (varname, true) in
Format.fprintf fmt "_state->%s[%d]" arr idx
Format.fprintf fmt "state->%s[%d]" arr idx
| CBinOp (BOp_arrow, v, v') ->
Format.fprintf fmt "(_state->is_init ? (%a) : (%a))"
Format.fprintf fmt "(state->is_init ? (%a) : (%a))"
cp_value (v, hloc) cp_value (v', hloc)
| CBinOp (op, v, v') ->
Format.fprintf fmt "(%a) %s (%a)"
@ -256,7 +256,7 @@ and cp_expression fmt (expr, hloc) =
match expr with
| CAssign (CVStored (arr, idx), value) ->
begin
Format.fprintf fmt "%s_state->%s[%d] = %a;\n"
Format.fprintf fmt "%sstate->%s[%d] = %a;\n"
prefix arr idx cp_value (value, hloc)
end
| CAssign (CVInput _, _) -> failwith "never assign an input."
@ -270,14 +270,14 @@ and cp_expression fmt (expr, hloc) =
let h_out = aux_node_st.nt_output_map in
Format.fprintf fmt "%sfn_%s(%s, %a);\n"
prefix fn
(Format.asprintf "_state->aux_states[%d]" (nb-1))
(Format.asprintf "state->aux_states[%d]" (nb-1))
cp_varlist' argl;
let _ = List.fold_left
(fun i var ->
match var with
| CVStored (arr, idx) ->
let (arr', idx') = Hashtbl.find h_out i in
Format.fprintf fmt "%s_state->%s[%d] = ((%s*)(_state->aux_states[%d]))->%s[%d];\n"
Format.fprintf fmt "%sstate->%s[%d] = ((%s*)(state->aux_states[%d]))->%s[%d];\n"
prefix arr idx
aux_node_st.nt_name (nb-1)
arr' idx';
@ -288,8 +288,8 @@ and cp_expression fmt (expr, hloc) =
| CReset (node_name, i, v, b) ->
begin
Format.fprintf fmt "\tif (%a) {\n\
\t\t((t_state_%s*)(_state->aux_states[%d]))->is_init = true;\n\
\t\t((t_state_%s*)(_state->aux_states[%d]))->is_reset = true;\n\
\t\t((t_state_%s*)(state->aux_states[%d]))->is_init = true;\n\
\t\t((t_state_%s*)(state->aux_states[%d]))->is_reset = true;\n\
\t}\n\
%a\n"
cp_value (v, hloc)
@ -389,7 +389,7 @@ let cp_main_fn fmt (prog, sts) =
else Format.fprintf fmt "%s%a")
(match h with
| IVar _ -> "%d"
| BVar _ -> "%hd"
| BVar _ -> "%c"
| RVar _ -> "%f")
cp_printf_str (true, t)
in
@ -397,7 +397,7 @@ let cp_main_fn fmt (prog, sts) =
match Hashtbl.find_opt h i with
| None -> ()
| Some (s, i) ->
Format.fprintf fmt ", _state.%s[%d]%a"
Format.fprintf fmt ", state.%s[%d]%a"
s i cp_printf_arg (h, i+1)
in
Format.fprintf fmt "\"%a\\n\"%a"
@ -417,31 +417,23 @@ let cp_main_fn fmt (prog, sts) =
let main_st = Hashtbl.find sts "main" in
if main_st.nt_count_app = 0
then ()
else Format.fprintf fmt "\tfree_state_main(&_state);\n"
else Format.fprintf fmt "\tfree_state_main(&state);\n"
in
match List.find_opt (fun n -> n.n_name = "main") prog with
| None -> ()
| Some node ->
Format.fprintf fmt "int main (int argc, char **argv)\n\
{\n%a\n\
\tchar buffer[BUFFER_SIZE];\n\
\tt_state_main _state;\n\
\t_state.is_init = true;\n\
\t_state.is_reset = false;\n\
\tchar _buffer[1024];\n\
\tt_state_main state;\n\
\tstate.is_init = true;\n\
\tstate.is_reset = false;\n\
\twhile(true) {\n\
\t\tprintf(\"input: \");\n\
\t\tfor(unsigned short idx = 0; idx < BUFFER_SIZE; idx++) {\n\
\t\t\tif(idx == (BUFFER_SIZE - 1) || (buffer[idx] = getchar()) == '\\n') {\n\
\t\t\t\tbuffer[idx] = '\\0';\n\
\t\t\t\tbreak;\n\
\t\t\t}\n\
\t\t}\n\
\t\tif(!strcmp(buffer, \"exit\")) { break; }\n\
\t\tsscanf(buffer, %a);\n%a\
\t\tfn_main(&_state, %a);\n\
\t\tprintf(\"output: \");\n\
\t\tscanf(\"%%s\", _buffer);\n\
\t\tif(!strcmp(_buffer, \"exit\")) { break; }\n\
\t\tsscanf(_buffer, %a);\n%a\
\t\tfn_main(&state, %a);\n\
\t\tprintf(%a);\n\
\t\tprintf(\"\\n\");\n\
\t}\n\
%a\treturn EXIT_SUCCESS;\n\
}\n"

View File

@ -153,22 +153,14 @@ let rec pp_automata fmt: t_automaton list -> unit = function
pp_translist trans
pp_automata tail
and pp_nexts fmt: t_expression list * string list -> unit = function
| [], [] -> ()
| e::exprs, n::nexts ->
Format.fprintf fmt "if %a then %s else %a"
pp_expression e
n
pp_nexts (exprs, nexts)
| _, _ -> () (*This should never happen*)
and pp_translist fmt: t_state list -> unit = function
| [] -> ()
| State(name, eqs, cond, next)::q ->
Format.fprintf fmt "\t\t\t|%s -> do\n%a\n\t\t\tdone until %a \n%a"
Format.fprintf fmt "\t\t\t|%s -> do\n%a\n\t\t\tdone until %a \t\t\tthen %s\n%a"
name
pp_equations eqs
pp_nexts (cond, next)
pp_expression cond
next
pp_translist q
let pp_node fmt node =

View File

@ -25,6 +25,8 @@ let exec_passes ast verbose debug passes f =
| [] -> f ast
| (n, p) :: passes ->
verbose (Format.asprintf "Executing pass %s:\n" n);
try
begin
match p verbose debug ast with
| None -> (exit_error ("Error while in the pass "^n^".\n"); exit 0)
| Some ast -> (
@ -32,6 +34,8 @@ let exec_passes ast verbose debug passes f =
(Format.asprintf
"Current AST (after %s):\n%a\n" n Lustre_pp.pp_ast ast);
aux ast passes)
end with
| _ -> failwith ("The pass "^n^" should have caught me!")
in
aux ast passes
@ -40,12 +44,10 @@ let exec_passes ast verbose debug passes f =
let _ =
(** Usage and argument parsing. *)
let default_passes =
["linearization_reset"; "automata_translation"; "remove_if";
"linearization_merge"; "linearization_when";
["linearization_reset"; "remove_if";
"linearization_pre"; "linearization_tuples"; "linearization_app";
"ensure_assign_val";
"equations_ordering";
"clock_unification"] in
"equations_ordering"] in
let sanity_passes = ["sanity_pass_assignment_unicity"; "check_typing"] in
let usage_msg =
"Usage: main [-passes p1,...,pn] [-ast] [-verbose] [-debug] \
@ -83,8 +85,6 @@ let _ =
List.iter (fun (s, k) -> Hashtbl.add passes_table s k)
[
("remove_if", Passes.pass_if_removal);
("linearization_merge", Passes.pass_merge_lin);
("linearization_when", Passes.pass_when_lin);
("linearization_tuples", Passes.pass_linearization_tuples);
("linearization_app", Passes.pass_linearization_app);
("linearization_pre", Passes.pass_linearization_pre);
@ -157,13 +157,6 @@ let _ =
else (
if !nopopt
then (fun _ -> ())
else
(
let oc = open_out !output_file in
let fmt = Format.make_formatter
(Stdlib.output_substring oc)
(fun () -> Stdlib.flush oc) in
Ast_to_c.ast_to_c fmt print_verbose print_debug);
)
else Ast_to_c.ast_to_c print_verbose print_debug)
end

View File

@ -436,10 +436,9 @@ ident_comma_list:
transition:
| CASE IDENT BO_arrow DO equations DONE {
State($2, $5, [EConst([TBool], CBool(true))], [$2]) }
| CASE IDENT BO_arrow DO equations UNTIL next_list {
let (exprs, outs) = $7 in
State($2, $5, exprs, outs)}
State($2, $5, EConst([TBool], CBool(true)), $2) }
| CASE IDENT BO_arrow DO equations UNTIL expr THEN IDENT {
State($2, $5, $7, $9)}
;
transition_list:
@ -447,8 +446,3 @@ transition_list:
| transition transition_list { $1 :: $2 }
| /* empty */ {raise(MyParsingError("Empty automaton", current_location()))}
;
next_list:
| expr THEN IDENT { [$1], [$3] }
| next_list ELSE IF expr THEN IDENT { let (exprs, outs) = $1 in $4::exprs, $6::outs }
;

View File

@ -6,183 +6,6 @@ open Utils
(** [pass_when_lin] linearizes the when construct so that it only appears as
* main construction of right members of equations. *)
let pass_when_lin verbose debug =
(* prefix of the fresh variables to use and counter to make them unique. *)
let varname_prefix = "_whenlin" in
let count = ref 0 in
(** Auxiliary function that linearizes an expression. *)
let rec aux_expr vars expr toplevel conds =
match expr with
| EVar _ | EConst _ -> [], vars, expr
| EMonOp (t, op, e) ->
let eqs, vars, e = aux_expr vars e false conds in
eqs, vars, EMonOp (t, op, e)
| EBinOp (t, op, e, e') ->
let eqs, vars, e = aux_expr vars e false conds in
let eqs', vars, e' = aux_expr vars e' false conds in
eqs'@eqs, vars, EBinOp (t, op, e, e')
| EComp (t, op, e, e') ->
let eqs, vars, e = aux_expr vars e false conds in
let eqs', vars, e' = aux_expr vars e' false conds in
eqs'@eqs, vars, EComp (t, op, e, e')
| EReset (t, e, e') ->
let eqs, vars, e = aux_expr vars e false conds in
let eqs', vars, e' = aux_expr vars e' false conds in
eqs'@eqs, vars, EReset (t, e, e')
| ETuple (t, l) ->
let eqs, vars, l = List.fold_right
(fun e (eqs, vars, l) ->
let eqs', vars, e = aux_expr vars e false conds in
eqs' @ eqs, vars, (e :: l))
l ([], vars, []) in
eqs, vars, ETuple (t, l)
| EApp (t, n, e) ->
let eqs, vars, e = aux_expr vars e false conds in
eqs, vars, EApp (t, n, e)
| ETriOp (t, op, e, e', e'') ->
let eqs, vars, e = aux_expr vars e false conds in
let eqs', vars, e' = aux_expr vars e' false conds in
let eqs'', vars, e'' = aux_expr vars e'' false conds in
eqs''@eqs'@eqs, vars, ETriOp (t, op, e, e', e'')
| EWhen (t, e, e') ->
let eqs, vars, e = aux_expr vars e false conds in
let eqs', vars, e' = aux_expr vars e' false (e :: conds) in
let e =
List.fold_left
(fun e e' -> EBinOp ([TBool], BOp_and, e,e'))
e conds
in
if toplevel
then
eqs'@eqs, vars, EWhen (t, e, e')
else
begin
if List.length t = 1
then
begin
let newvar = Format.sprintf "%s%d" varname_prefix !count in
let newvar =
match List.hd t with
| TInt -> IVar newvar
| TBool -> BVar newvar
| TReal -> RVar newvar
in
let () = incr count in
let vars = (t @ (fst vars), newvar :: (snd vars)) in
((t, [newvar]), EWhen (t, e, e')) :: eqs'@eqs, vars, EVar (t, newvar)
end
else
raise (PassExn "When should only happen on unary expressions.")
end
in
(** For each node: *)
let aux_when_lin node =
(** Loop on equations to get additional equations and variables. *)
let eqs, vars =
List.fold_left
(fun (eqs, vars) (patt, expr) ->
let eqs', vars, expr = aux_expr vars expr true [] in
(patt, expr) :: eqs' @ eqs, vars)
([], node.n_local_vars) node.n_equations
in
Some { node with n_local_vars = vars; n_equations = eqs }
in
node_pass aux_when_lin
(** [pass_merge_lin] linearizes the merges so that they only appear as main
* construct of right sides of equations.
* This simplifies their handling in next passes and in the C printer. *)
let pass_merge_lin verbose debug =
(* prefix of the fresh variables to use and counter to make them unique. *)
let varname_prefix = "_mergelin" in
let count = ref 0 in
(** Auxiliary function that linearizes an expression. *)
let rec aux_expr vars expr toplevel =
match expr with
| EVar _ | EConst _ -> [], vars, expr
| EMonOp (t, op, e) ->
let eqs, vars, e = aux_expr vars e false in
eqs, vars, EMonOp (t, op, e)
| EBinOp (t, op, e, e') ->
let eqs, vars, e = aux_expr vars e false in
let eqs', vars, e' = aux_expr vars e' false in
eqs'@eqs, vars, EBinOp (t, op, e, e')
| EComp (t, op, e, e') ->
let eqs, vars, e = aux_expr vars e false in
let eqs', vars, e' = aux_expr vars e' false in
eqs'@eqs, vars, EComp (t, op, e, e')
| EReset (t, e, e') ->
let eqs, vars, e = aux_expr vars e false in
let eqs', vars, e' = aux_expr vars e' false in
eqs'@eqs, vars, EReset (t, e, e')
| ETuple (t, l) ->
let eqs, vars, l = List.fold_right
(fun e (eqs, vars, l) ->
let eqs', vars, e = aux_expr vars e false in
eqs' @ eqs, vars, (e :: l))
l ([], vars, []) in
eqs, vars, ETuple (t, l)
| EApp (t, n, e) ->
let eqs, vars, e = aux_expr vars e false in
eqs, vars, EApp (t, n, e)
| ETriOp (_, TOp_if, _, _, _) ->
raise (PassExn "There should no longer be any condition.")
| EWhen (t, e, e') ->
let eqs, vars, e = aux_expr vars e false in
let eqs', vars, e' = aux_expr vars e' false in
eqs @ eqs', vars, EWhen (t, e, e')
| ETriOp (t, TOp_merge, c, e, e') ->
begin
if toplevel
then
begin
let eqs, vars, c = aux_expr vars c false in
let eqs', vars, e = aux_expr vars e false in
let eqs'', vars, e' = aux_expr vars e' false in
eqs@eqs'@eqs'', vars, ETriOp (t, TOp_merge, c, e, e')
end
else
begin
if List.length t = 1
then
let newvar = Format.sprintf "%s%d" varname_prefix !count in
let newvar =
match List.hd t with
| TInt -> IVar newvar
| TBool -> BVar newvar
| TReal -> RVar newvar
in
let () = incr count in
let vars = (t @ (fst vars), newvar :: (snd vars)) in
let eqs, vars, c = aux_expr vars c false in
let eqs', vars, e = aux_expr vars e false in
let eqs'', vars, e' = aux_expr vars e' false in
((t, [newvar]), ETriOp (t, TOp_merge, c, e, e')) :: eqs @ eqs' @ eqs'', vars, EVar (t, newvar)
else
raise (PassExn "Merges should only happen on unary expressions.")
end
end
in
(** For each node: *)
let aux_merge_lin node =
(** Loop on equations to get additional equations and variables. *)
let eqs, vars =
List.fold_left
(fun (eqs, vars) (patt, expr) ->
let eqs', vars, expr = aux_expr vars expr true in
(patt, expr) :: eqs' @ eqs, vars)
([], node.n_local_vars) node.n_equations
in
Some { node with n_local_vars = vars; n_equations = eqs }
in
node_pass aux_merge_lin
(** [pass_if_removal] replaces the `if` construct with `when` and `merge` ones.
*
* [x1, ..., xn = if c then e_l else e_r;]
@ -324,7 +147,6 @@ let pass_if_removal verbose debug =
node_pass aux_if_removal
(** [pass_linearization_reset] makes sure that all reset constructs in the program
* are applied to functions.
* This is required, since the reset construct is translated into resetting the
@ -393,7 +215,6 @@ let pass_linearization_reset verbose debug =
node_pass node_lin
(** [pass_linearization_pre] makes sure that all pre constructs in the program
* are applied to variables.
* This is required, since the pre construct is translated into a variable in
@ -421,7 +242,7 @@ let pass_linearization_pre verbose debug =
| [TInt] -> IVar nvar
| [TBool] -> BVar nvar
| [TReal] -> RVar nvar
| _ -> failwith "Should not happened. (pass_linearization_pre)" in
| _ -> 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
@ -802,45 +623,28 @@ let rec tpl debug ((pat, exp): t_equation) =
| ETuple (_, []) -> []
| _ -> [(pat, exp)]
(** [pass_eq_reordering] orders the equation such that an equation should not
* appear before all equations defining the variables it depends on are. *)
let pass_eq_reordering verbose debug ast =
(** [pick_equations] takes a list of equations and initialized variables.
* it either returns:
* - a list of equations in a correct order
* - nothing *)
let rec pick_equations init_vars eqs remaining_equations =
match remaining_equations with
| [] -> (* There are no equations left to order: we are done. *) Some eqs
| [] -> Some eqs
| _ ->
begin
(** The filter below provides the equations whose dependencies have
* already been defined *)
match List.filter
(fun (patt, expr) ->
List.for_all
(fun v -> List.mem v init_vars)
(vars_of_expr expr))
remaining_equations with
| [] -> (** There are remaining equations to order, but none whose all
* dependencies have already been defined yet.*)
raise (PassExn "[equation ordering] The equations cannot be ordered.")
| h :: t -> (** [h :: t] is a list of equations whose dependencies have
* all already been defined. *)
let init_vars = (* new set of initialized variables *)
| [] -> raise (PassExn "[equation ordering] The equations cannot be ordered.")
| h :: t ->
let init_vars =
List.fold_left
(fun acc vs ->
(vars_of_patt (fst vs)) @ acc) init_vars (h :: t) in
(** The filter below removes the equation of [h :: t] to those to
* the list of equations to be ordered *)
pick_equations init_vars (eqs @ (h :: t))
(List.filter
(fun eq -> List.for_all (fun e -> eq <> e) (h :: t)) remaining_equations)
acc @ (vars_of_patt (fst vs))) init_vars (h :: t) in
pick_equations init_vars (eqs@(h :: t))
(List.filter (fun eq -> List.for_all (fun e -> eq <> e) (h :: t)) remaining_equations)
end
in
(* main function of the (node-)pass. *)
in
let node_eq_reorganising (node: t_node): t_node option =
let init_vars = List.map name_of_var (snd node.n_inputs) in
try
@ -851,11 +655,8 @@ let pass_eq_reordering verbose debug ast =
end
with PassExn err -> (verbose err; None)
in
(** iterate the pass over the nodes of the program. *)
node_pass node_eq_reorganising ast
let pass_typing verbose debug ast =
let htbl = Hashtbl.create (List.length ast) in
let () = debug "[typing verification]" in
@ -926,7 +727,7 @@ let pass_typing verbose debug ast =
else None
in aux ast
let check_automata_validity verbose debug =
let check_automata_validity verbos debug =
let check_automaton_branch_vars automaton =
let (init, states) = automaton in
let left_side = Hashtbl.create 10 in
@ -951,22 +752,78 @@ let check_automata_validity verbose debug =
end
in
let aux node =
try
List.iter check_automaton_branch_vars node.n_automata;
Some node
with
| PassExn err -> (verbose err; None)
in
node_pass aux
let automaton_translation debug automaton =
let automaton_translation debug automaton =
let gathered = Hashtbl.create 10 in
let state_to_int = Hashtbl.create 10 in
let add_to_table var exp state =
if Hashtbl.mem gathered var then
let res = Hashtbl.find gathered var in
Hashtbl.replace gathered var ((state, exp)::res);
else
Hashtbl.replace gathered var ([(state, exp)])
in
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+1))
in
let rec find_state name =
match Hashtbl.find_opt state_to_int name with
| None -> failwith "Unknown state in automaton"
| Some v -> v
in
let rec equation_pass state : t_eqlist -> unit = function
| [] -> ()
| (vars, exp)::q -> begin
add_to_table vars exp state;
equation_pass state q
end
in
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 eq;
State(name, eq, cond, next)
in
let rec transition_eq states s =
match states with
| [] -> EVar([TInt], IVar(s))
| State(name, eqs, cond, next)::q ->
let name = find_state name
and next = find_state next in
ETriOp([TInt], TOp_if,
EBinOp([TBool], BOp_and,
EComp([TBool], COp_eq,
EVar([TInt], IVar(s)),
EConst([TInt], CInt(name))
),
cond
),
EConst([TInt], CInt(next)),
transition_eq q s
)
in
let id = create_automaton_id () in
let automat_name = create_automaton_name id in
let new_vars = Hashtbl.create Config.maxvar in
let var_seen = Hashtbl.create Config.maxvar in
let var_merged = Hashtbl.create Config.maxvar in
let state_to_int = Hashtbl.create Config.maxvar in
let default_constant ty =
let defaults ty = match ty with
| TInt -> EConst([ty], CInt(0))
@ -979,273 +836,157 @@ let automaton_translation debug automaton =
| [TReal] -> EConst(ty, CReal(0.0))
| _ -> ETuple(ty, List.map defaults ty)
in
let get_branch_var var branch =
Format.asprintf "_%s_%s_%d" var branch id in
let create_var_name var branch ty =
let s = get_branch_var var branch in
Hashtbl.replace new_vars s (var, branch, ty);
Hashtbl.add var_seen var (s, branch, ty);
s
in
let get_branch_bool branch =
Format.asprintf "_b_%s_%d" branch id in
let create_branch_name branch =
let s = get_branch_bool branch in
Hashtbl.replace new_vars s ("", branch, TBool);
s
in
let create_merge_var varname branch ty =
let s = Format.asprintf "_%s_%s_merge_%d" varname branch id in
Hashtbl.replace new_vars s (varname, branch, ty);
s
in
let create_next_var branch =
let s = Format.asprintf "_next_%s_%d" branch id in
Hashtbl.replace new_vars s ("", branch, TInt);
s
in
let create_type_var_name var branch = match var with
| BVar(name) -> create_var_name name branch TBool
| IVar(name) -> create_var_name name branch TInt
| RVar(name) -> create_var_name name branch TReal
in
let to_var varname ty = match ty with
| TInt -> IVar(varname)
| TBool -> BVar(varname)
| TReal -> RVar(varname)
in
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+1))
in
let rec find_state name =
match Hashtbl.find_opt state_to_int name with
| None -> failwith "Unknown state in automaton"
| Some v -> v
in
let translate_eqlist eqlist branch =
let aux eq =
let ((ty, vlist), expr ) = eq in
((ty, List.map2 (fun l ty -> to_var (create_type_var_name l branch) ty ) vlist ty ),
EWhen(type_exp expr, expr, EVar([TBool], to_var (get_branch_bool branch) TBool )))
in
List.map aux eqlist
in
let rec next_construct exprs nexts = match exprs, nexts with
| [], [] -> EConst([TInt], CInt(1))
| e::exprs, n::nexts -> ETriOp([TInt], TOp_if, e, EConst([TInt], CInt(find_state n)), next_construct exprs nexts)
| _, _ -> failwith "Automata translation: next construct: should not happen"
in
let state_translation state =
match state with
| State( name, equations, expr, next ) ->
let b = create_branch_name name in
let eqs = translate_eqlist equations name in
let bool_expr = EComp([TBool], COp_eq, EVar([TInt], to_var automat_name TInt), EConst([TInt], CInt(find_state name))) in
let next_expr = EWhen([TInt], next_construct expr next, EVar([TBool], to_var (get_branch_bool name) TBool)) in
(([TBool], [to_var b TBool]), bool_expr)::(([TInt], [to_var (create_next_var name) TInt]), next_expr)::eqs
in
let rec iter_states states =
match states with
| [] -> []
| s::q -> (state_translation s) @ (iter_states q)
in
let combine_one_var varname ty =
let default = default_constant [ty] in
let rec merge_branches previous branchlist = match branchlist with
| [] -> Hashtbl.replace var_merged varname true ; [(([ty], [to_var varname ty]), previous)]
| (var, branch, ty2)::q ->
let merge_var = create_merge_var varname branch ty in
(([ty], [to_var merge_var ty]),
ETriOp([ty], TOp_merge, EVar([TBool], to_var (get_branch_bool branch) TBool), EVar([ty], to_var var ty),
EWhen([ty], previous, EMonOp([TBool], MOp_not, EVar([TBool], to_var (get_branch_bool branch) TBool)))))
:: ( merge_branches (EVar([ty], to_var merge_var ty2)) q )
in
let l = Hashtbl.find_all var_seen varname in
merge_branches default l
in
let combine_var varname =
if Hashtbl.mem var_merged varname then []
else let (_, _, ty) = Hashtbl.find var_seen varname in combine_one_var varname ty
in
let rec merge_state states = match states with
| [] -> EConst([TInt], CInt(1))
| State(name, _, _, _)::q ->
let end_state = merge_state q in
let bool_var = EVar([TBool], to_var (get_branch_bool name) TBool) in
ETriOp([TInt], TOp_merge, bool_var, EVar([TInt], to_var (create_next_var name) TInt),
EWhen([TInt], end_state, EMonOp([TBool], MOp_not, bool_var)))
in
let extract_new_var (varname, (_, _, ty)) = to_var varname ty in
let rec build_type varlist = match varlist with
|IVar(_)::q -> TInt::build_type q
|BVar(_)::q -> TBool::build_type q
|RVar(_)::q -> TReal::build_type q
|[] -> []
let rec translate_var s v explist ty = match explist with
| [] -> default_constant ty
| (state, exp)::q ->
ETriOp(Utils.type_exp exp, TOp_if,
EComp([TBool], COp_eq,
EVar([TInt], IVar(s)),
EConst([TInt], CInt(Hashtbl.find state_to_int state))
),
exp,
translate_var s v q ty
)
in
let init, states = automaton in
let flatten_automaton automaton =
let (init, states) = automaton in
(flatten_state init, List.map flatten_state states)
in
let (init, states) = flatten_automaton automaton in
let s = create_automaton_name () in
init_state_translation states 1;
let transition_eq = (([TInt], [IVar(automat_name)]), EBinOp([TInt], BOp_arrow, EConst([TInt], CInt(1)), EMonOp([TInt], MOp_pre, merge_state states))) in
let state_eqs = (iter_states states) in
let new_eqs = state_eqs @ (List.flatten (List.map combine_var (List.of_seq (Hashtbl.to_seq_keys var_seen)))) in
let new_vars = List.map extract_new_var (List.of_seq (Hashtbl.to_seq new_vars)) in
(transition_eq)::new_eqs, (TInt::(build_type new_vars), IVar(automat_name)::new_vars)
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 (fst var))::acc) gathered new_equations, IVar(s)
let automata_trans_pass debug (node:t_node) : t_node option=
let rec aux automaton = match automaton with
| [] -> [], [], []
| a::q ->
let eq, var = automaton_translation debug a
and tail_eq, tail_var, tail_type = aux q in
eq@tail_eq, var::tail_var, TInt::tail_type
in
let eqs, vars, new_ty = aux node.n_automata in
let ty, loc_vars = node.n_local_vars in
Some
{
n_name = node.n_name;
n_inputs = node.n_inputs;
n_outputs = node.n_outputs;
n_local_vars = (new_ty@ty, vars@loc_vars);
n_equations = eqs@node.n_equations;
n_automata = []; (* not needed anymore *)
}
let automata_translation_pass verbose debug =
let rec iter_automata autolist = match autolist with
| [] -> [], ([], [])
| a::q -> let (eqs, (ty, vars)) = automaton_translation debug a in
let (eqs_end, (ty_end, vars_end)) = iter_automata q in
eqs@eqs_end, (ty@ty_end, vars@vars_end)
in
let aux node =
try
let eqs, (ty, vars) = iter_automata node.n_automata in
let (ty_old, vars_old) = node.n_local_vars in
Some { node with n_local_vars = (ty@ty_old, vars@vars_old); n_equations = node.n_equations@eqs; n_automata = []}
with
|PassExn err -> (verbose err; None)
in
node_pass aux
node_pass (automata_trans_pass debug)
let clock_unification_pass verbose debug ast =
let failure str = raise (PassExn ("Failed to unify clocks: "^str)) in
let known_clocks = Hashtbl.create 100 in
let used = Hashtbl.create 100 in (*keep track of variables that appear on right side of equation*)
let changed = ref false in
let rec count_not e acc = match e with
| EVar([TBool], var) -> acc, e
| EConst([TBool], cons) -> acc, e
| EMonOp([TBool], MOp_not, e) -> count_not e (acc + 1)
| _ -> acc, e
let find_clock_var var =
match Hashtbl.find_opt known_clocks var with
| None ->
begin
match var with
| BVar(name)
| IVar(name)
| RVar(name) -> raise (PassExn ("Cannot find clock of variable "^name) )
end
| Some c -> c
in
let verify_when e1 e2 =
let n1, var1 = count_not e1 0
and n2, var2 = count_not e2 0 in
if n1 mod 2 <> n2 mod 2 || var1 <> var2 then
raise (PassExn "verify_when failure")
in
let get_var_name var = match var with
| RVar(name)
| BVar(name)
| IVar(name) -> name
in
let rec clk_to_string clk = match clk with
| Base -> "Base"
| Unknown -> "Unknown"
| On(clk, exp) ->
let n, var = count_not exp 0 in
let s = if n mod 2 = 1 then "not " else "" in
let v = match var with |EVar(_, var) -> get_var_name var | EConst(_, CBool(false)) -> "false" |_ -> "true" in
(clk_to_string clk) ^ " on " ^ s ^ v
in
let add_clock var clock =
match Hashtbl.find known_clocks var with
| Unknown -> changed := true; (debug ("Found clock for "^(get_var_name var)^": "^(clk_to_string clock))); Hashtbl.replace known_clocks var clock
| c when c = clock -> ()
| c -> raise (PassExn ("Clock conflict "^(get_var_name var) ^" "^(clk_to_string c) ^ " " ^ (clk_to_string clock)))
in
let rec update_clock exp clk = match exp with
| EConst(_, _) -> ()
| EVar(_, var) -> add_clock var clk; Hashtbl.replace used var var
| EMonOp(_, _, e) -> update_clock e clk
let rec compute_clock_exp exp = match exp with
| EConst(_, _) -> [Base]
| EVar(_, var) -> find_clock_var var
| EMonOp(_, MOp_pre, _) -> [Base]
| EMonOp(_, _, e) -> compute_clock_exp e
| EComp(_, _, e1, e2)
| EReset(_, e1, e2)
| EBinOp(_, _, e1, e2) -> update_clock e1 clk; update_clock e2 clk
| ETriOp(_, TOp_merge, e1, e2, e3) ->
update_clock e1 clk;
update_clock e2 (On(clk, e1));
update_clock e3 (On(clk, EMonOp([TBool], MOp_not, e1)))
| ETriOp(_, TOp_if, e1, e2, e3) ->
(* The 3 expressions should have the same clock *)
begin
update_clock e1 clk;
update_clock e2 clk;
update_clock e3 clk
end
| ETuple(_, explist) -> List.iter (fun e -> update_clock e clk) explist
| EApp(_, node, e) -> update_clock e clk
| EBinOp(_, _, e1, e2) ->
begin
let c1 = compute_clock_exp e1
and c2 = compute_clock_exp e2 in
if c1 <> c2 then
failure "Binop"
else
c1
end
| EWhen(_, e1, e2) ->
match clk with
| On(clk2, e) -> verify_when e e2; update_clock e1 clk2
| _ -> raise (PassExn "Clock unification failure: when")
begin
match compute_clock_exp e1 with
| [c1] -> [On (c1, e2)]
| _ -> failure "When"
end
| ETriOp(_, TOp_merge, e1, e2, e3) ->
begin
let c1 = compute_clock_exp e1
and c2 = compute_clock_exp e2
and c3 = compute_clock_exp e3 in
match c1, c2, c3 with
| [c1], [On(cl2, e2)], [On(cl3, e3)] ->
begin
if cl2 <> c1 || cl3 <> c1 then
failure "Triop clocks"
else match e2, e3 with
| EMonOp(_, MOp_not, e), _ when e = e3 -> [c1]
| _, EMonOp(_, MOp_not, e) when e = e2 -> [c1]
| _ -> failure "Triop condition"
end
| _ -> failure ("Merge format")
end
| ETriOp(_, TOp_if, e1, e2, e3) ->
let (* Unused: c1 = compute_clock_exp e1
and*) c2 = compute_clock_exp e2
and c3 = compute_clock_exp e3 in
if c2 <> c3 then
failure "If clocks"
else c2
| ETuple(_, explist) -> List.concat_map compute_clock_exp explist
| EApp(_, node, e) ->
let rec aux_app clk_list = match clk_list with
| [] -> raise (PassExn "Node called with no argument provided")
| [cl] -> cl
| t::q -> if t = (aux_app q) then t else failure "App diff clocks"
and mult_clk cl out_list = match out_list with
| [] -> []
| t::q -> cl::(mult_clk cl q)
in
mult_clk (aux_app (compute_clock_exp e)) (snd node.n_outputs)
in
let rec propagate_clock eqs =
let rec step ((ty, vars), exp)= match vars with
| [] -> ()
| v::t -> let clk = Hashtbl.find known_clocks v in
begin
if clk <> Unknown then update_clock exp clk
else ();
step ((ty, t), exp)
end
let rec compute_eq_clock eq =
let rec step vars clks = match vars, clks with
| [], [] -> ()
| [], c::q -> raise (PassExn "Mismatch between clock size")
| v::t, c::q -> Hashtbl.replace known_clocks v [c]; step t q
| l, [] -> raise (PassExn "Mismatch between clock size")
in
List.iter step eqs
let (_, vars), exp = eq in
let clk = compute_clock_exp exp in
step vars clk
in
let rec iter_til_stable eqs =
changed := false;
propagate_clock eqs;
if !changed then
iter_til_stable eqs
in
let check_unification node =
let (_, node_inputs) = node.n_inputs in
let rec check_vars_aux acc = match acc with
| [(v, c)] -> if c = Unknown && (Hashtbl.mem used v) then raise (PassExn ("Clock unification failure: Unkwown clock for "^(get_var_name v))) else c
| (v, t)::q -> let c = check_vars_aux q in
if c <> t then raise (PassExn "Clock unification failure: Non homogeneous equation") else c
| [] -> raise (PassExn "Clock unification failure: empty equation")
in
let rec check_vars ((ty, vars), exp) acc = match vars with
| [] -> let _ = check_vars_aux acc in ()
| v::t -> check_vars ((ty, t), exp) ((v, Hashtbl.find known_clocks v)::acc)
in
let rec check_inputs inputs = match inputs with
| [] -> ()
| i::q -> let c = Hashtbl.find known_clocks i in
match c with
| On(_, e) -> let _, var = count_not e 0 in
begin
match var with
| EConst(_, _) -> ()
| EVar(_, var) -> if not (List.mem var node_inputs) then raise (PassExn "Clock unification failure: input clock depends on non input clock")
else check_inputs q
| _ -> failwith "Should not happen. (clock_unification)"
end
| _ -> check_inputs q
in
(*Check that all variables used have a clock
and that inputs clocks do not depend on local vars or outputs*)
List.iter (fun eq -> check_vars eq []) node.n_equations;
check_inputs node_inputs;
in
let compute_clock_node n =
begin
Hashtbl.clear known_clocks;
List.iter (fun v -> Hashtbl.replace known_clocks v Unknown) (
snd n.n_inputs); (* Initializing inputs to Unknown clock *)
List.iter (fun v -> Hashtbl.replace known_clocks v Unknown) (
snd n.n_local_vars); (* Initializing local variables to Unknown clock *)
List.iter (fun v -> Hashtbl.replace known_clocks v Base) (
snd n.n_outputs); (* Initializing outputs to base clock *)
iter_til_stable n.n_equations;
(* catch potential errors and test for unification *)
check_unification n;
Some n
List.iter (fun v -> Hashtbl.replace known_clocks v [Base]) (
snd n.n_inputs); (* Initializing inputs to base clock *)
List.iter compute_eq_clock n.n_equations;
if not (List.for_all (fun v -> (Hashtbl.find known_clocks v) = [Base]) (
snd n.n_outputs)) then failure "Outputs" (*Checking that the node's output are on base clock *)
else
Some n
end
in node_pass compute_clock_node ast

View File

@ -33,9 +33,6 @@ let expression_pass f: t_nodelist -> t_nodelist option =
exception PassExn of string
let counter = ref 0
let create_automaton_id : unit -> int = fun () ->
let create_automaton_name : unit -> string = fun () ->
counter := !counter + 1;
!counter
let create_automaton_name id =
Format.asprintf "_s%d" (id)
Format.asprintf "_s%d" (!counter)

View File

@ -16,10 +16,3 @@ let
tmp = aux (a+b, i);
tel
node test (u, v: int; c: bool) returns (o: int);
var x, y: int; b: bool;
let
x = merge c u v;
o = 2 * x;
tel

View File

@ -1,4 +0,0 @@
node main (i: int) returns (o: int);
let
o = 1 -> 2 -> 3;
tel

View File

@ -1,22 +0,0 @@
node diagonal_int (i: int) returns (o1, o2 : int);
let
(o1, o2) = (i, i);
tel
node undiag_test (i: int) returns (o : bool);
var l1, l2: int; l3: int;
let
l3 = (pre (1)) -> 0;
(l1, l2) = diagonal_int(i);
o = (not (not (l1 = l2))) and (l1 = l2) and true;
tel
node main (i: int) returns (o : int);
var x, y:int;
let
automaton
| Incr -> do (o,x) = (0 fby o + 1, 2); until x > 0 then Decr else if x = o then Done
| Decr -> do (o,x) = diagonal_int(0 fby o); until x < o then Incr
| Done -> do o = pre o; done
tel

View File

@ -1,16 +0,0 @@
-- count the number of top between two tick
node counting (tick:bool; top:bool)
returns (o: int);
var v, o1: int;
let o = if tick then v else 0 -> (pre o) + v;
v = if top then 1 else 0
tel;
node main (i: int)
returns (o: int);
let
-- 0 means no `tick` and no `top`
-- 1 means `tick`
-- 2 means `top`
o = counting(i = 1, i = 2)
tel;

View File

@ -1,15 +0,0 @@
-- counter of `top`s until `reset` condition holds
node counting (tick: bool) returns (o: int);
var v: int;
let
o = v -> (pre o) + v;
v = if tick then 1 else 0
tel
node main (i: int) returns (o: int);
let
-- 0 means no `top` and no `reset`
-- 1 means `top`
-- 2 means `reset`
o = reset counting(i = 1) every (i = 2);
tel

21
tests/test.node Normal file
View File

@ -0,0 +1,21 @@
node diagonal_int (i: int) returns (o1, o2 : int);
let
(o1, o2) = (i, i);
tel
node undiag_test (i: int) returns (o : bool);
var l1, l2: int; l3: int;
let
l3 = (pre (1)) -> 0;
(l1, l2) = diagonal_int(i);
o = (not (not (l1 = l2))) and (l1 = l2) and true;
tel
node auto (i: int) returns (o : int);
var x, y:int;
let
automaton
| Incr -> do (o,x) = (0 fby o + 1, 2); done
| Decr -> do (o,x) = diagonal_int(0 fby o); done
tel

View File

@ -1,6 +1,6 @@
node diagonal_int (i: int) returns (o1, o2 : int);
let
(o1, o2) = (i, i);
(o1, o2) = (i, i);
tel
node main (i: int) returns (o1, o2, o3, o4: int);

View File

@ -1,4 +1,4 @@
node main (i: int) returns (o: bool);
node n2 (i: int) returns (o: bool);
let
o = pre (true and pre( i = pre(pre(i))));
tel

View File

@ -1,13 +0,0 @@
node test (i: real) returns (o: real);
var x, y: real;
let
x = (1.0 / i) when (i <> 0.0);
y = 0.0 when (not (i <> 0.0));
o = merge (i <> 0.0) x y;
tel
node main (i: real) returns (o: real);
let
-- The idea is to pass `0.0` as the input to acknowledge that the division by zero isn't computed.
o = test(i);
tel