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); node auto (i: int) returns (o : int);
var x, y: int; var x, y:int;
let let
automaton automaton
| Incr -> do (o,x) = (0 fby o + 1, 2); until o < 5 then Decr | 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 | Decr -> do (o,x) = diagonal_int(0 fby o); until o > 3 then Incr
tel tel
node auto (i: int) returns (o : int); node auto (i: int) returns (o: int);
var x, y: int; var x, y: int;
let let
_s1 = 1 -> (if _s = 1 and o < 5 then 2 else if _s = 2 and o > then 1 else 1); _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 tel
node auto (i: int) returns (o : int); node auto (i: int) returns (o : int);
var x, y: int; var x, y:int;
let let
automaton automaton
| Incr -> do (o,x) = (0 fby o + 1, 2); until o < 5 then Decr | 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_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 and t_automaton = t_state * t_state list
@ -77,4 +77,3 @@ type t_ck = base_ck list
and base_ck = and base_ck =
| Base | Base
| On of base_ck * t_expression | 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 match Hashtbl.find_opt node_st.nt_map (v, false) with
| Some (src_array, src_idx) -> | Some (src_array, src_idx) ->
let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in 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 dst_array dst_idx src_array src_idx
| None -> | None ->
let (dst_array, dst_idx) = Hashtbl.find node_st.nt_map (v, true) in 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 dst_array dst_idx v
) )
(List.map Utils.name_of_var l) (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 *) | None -> () (** All auxiliary nodes have been initialized *)
| Some n -> | Some n ->
begin begin
Format.fprintf fmt "%a\t\tif(!_state->is_reset) {\n\ Format.fprintf fmt "%a\t\tif(!state->is_reset) {\n\
\t\t\t_state->aux_states[%d] = calloc (1, sizeof (%s));\n\ \t\t\tstate->aux_states[%d] = calloc (1, sizeof (%s));\n\
\t\t}\n\ \t\t}\n\
\t\t((%s*)(_state->aux_states[%d]))->is_init = true;\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_reset = state->is_reset;\n"
aux (node, nst, i-1) aux (node, nst, i-1)
(i-1) (Format.asprintf "t_state_%s" n.n_name) (i-1) (Format.asprintf "t_state_%s" n.n_name)
(Format.asprintf "t_state_%s" n.n_name) (i-1) (Format.asprintf "t_state_%s" n.n_name) (i-1)
@ -252,7 +252,7 @@ let cp_init_aux_nodes fmt (node, h) =
then () then ()
else begin else begin
Format.fprintf fmt "\t/* Initialize the auxiliary nodes */\n\ 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) aux (node, nst, nst.nt_count_app)
end end
@ -270,12 +270,12 @@ let cp_equations fmt (eqs, hloc, h) =
List.map (fun eq -> equation_to_expression (hloc, h, eq)) eqs in List.map (fun eq -> equation_to_expression (hloc, h, eq)) eqs in
let main_block = remove_ifnot main_block in let main_block = remove_ifnot main_block in
let main_block = merge_neighbour_ifs 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_block (main_block, hloc.nt_map)
(** [cp_node] prints a single node *) (** [cp_node] prints a single node *)
let cp_node fmt (node, h) = 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_prototype (node, h)
cp_init_aux_nodes (node, h) cp_init_aux_nodes (node, h)
cp_equations (node.in_equations, Hashtbl.find h node.in_name, 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]. *) (** 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"; verbose "Computation of the node_states";
let prog_st_types = make_state_types prog in let prog_st_types = make_state_types prog in
debug (Format.asprintf "%a" dump_var_locations prog_st_types); debug (Format.asprintf "%a" dump_var_locations prog_st_types);
let iprog: i_nodelist = ast_to_intermediate_ast prog prog_st_types in 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_includes (Config.c_includes)
cp_state_types prog_st_types cp_state_types prog_st_types
cp_state_frees (iprog, prog_st_types) cp_state_frees (iprog, prog_st_types)

View File

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

View File

@ -153,22 +153,14 @@ let rec pp_automata fmt: t_automaton list -> unit = function
pp_translist trans pp_translist trans
pp_automata tail 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 and pp_translist fmt: t_state list -> unit = function
| [] -> () | [] -> ()
| State(name, eqs, cond, next)::q -> | 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 name
pp_equations eqs pp_equations eqs
pp_nexts (cond, next) pp_expression cond
next
pp_translist q pp_translist q
let pp_node fmt node = let pp_node fmt node =

View File

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

View File

@ -436,10 +436,9 @@ ident_comma_list:
transition: transition:
| CASE IDENT BO_arrow DO equations DONE { | CASE IDENT BO_arrow DO equations DONE {
State($2, $5, [EConst([TBool], CBool(true))], [$2]) } State($2, $5, EConst([TBool], CBool(true)), $2) }
| CASE IDENT BO_arrow DO equations UNTIL next_list { | CASE IDENT BO_arrow DO equations UNTIL expr THEN IDENT {
let (exprs, outs) = $7 in State($2, $5, $7, $9)}
State($2, $5, exprs, outs)}
; ;
transition_list: transition_list:
@ -447,8 +446,3 @@ transition_list:
| transition transition_list { $1 :: $2 } | transition transition_list { $1 :: $2 }
| /* empty */ {raise(MyParsingError("Empty automaton", current_location()))} | /* 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. (** [pass_if_removal] replaces the `if` construct with `when` and `merge` ones.
* *
* [x1, ..., xn = if c then e_l else e_r;] * [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 node_pass aux_if_removal
(** [pass_linearization_reset] makes sure that all reset constructs in the program (** [pass_linearization_reset] makes sure that all reset constructs in the program
* are applied to functions. * are applied to functions.
* This is required, since the reset construct is translated into resetting the * 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 node_pass node_lin
(** [pass_linearization_pre] makes sure that all pre constructs in the program (** [pass_linearization_pre] makes sure that all pre constructs in the program
* are applied to variables. * are applied to variables.
* This is required, since the pre construct is translated into a variable in * 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 | [TInt] -> IVar nvar
| [TBool] -> BVar nvar | [TBool] -> BVar nvar
| [TReal] -> RVar 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_patt: t_varlist = (t, [nvar]) in
let neq_expr: t_expression = e in let neq_expr: t_expression = e in
let vars = varlist_concat (t, [nvar]) vars in let vars = varlist_concat (t, [nvar]) vars in
@ -802,45 +623,28 @@ let rec tpl debug ((pat, exp): t_equation) =
| ETuple (_, []) -> [] | ETuple (_, []) -> []
| _ -> [(pat, exp)] | _ -> [(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 = 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 = let rec pick_equations init_vars eqs remaining_equations =
match remaining_equations with match remaining_equations with
| [] -> (* There are no equations left to order: we are done. *) Some eqs | [] -> Some eqs
| _ -> | _ ->
begin begin
(** The filter below provides the equations whose dependencies have
* already been defined *)
match List.filter match List.filter
(fun (patt, expr) -> (fun (patt, expr) ->
List.for_all List.for_all
(fun v -> List.mem v init_vars) (fun v -> List.mem v init_vars)
(vars_of_expr expr)) (vars_of_expr expr))
remaining_equations with remaining_equations with
| [] -> (** There are remaining equations to order, but none whose all | [] -> raise (PassExn "[equation ordering] The equations cannot be ordered.")
* dependencies have already been defined yet.*) | h :: t ->
raise (PassExn "[equation ordering] The equations cannot be ordered.") let init_vars =
| h :: t -> (** [h :: t] is a list of equations whose dependencies have
* all already been defined. *)
let init_vars = (* new set of initialized variables *)
List.fold_left List.fold_left
(fun acc vs -> (fun acc vs ->
(vars_of_patt (fst vs)) @ acc) init_vars (h :: t) in acc @ (vars_of_patt (fst vs))) init_vars (h :: t) in
(** The filter below removes the equation of [h :: t] to those to pick_equations init_vars (eqs@(h :: t))
* the list of equations to be ordered *) (List.filter (fun eq -> List.for_all (fun e -> eq <> e) (h :: t)) remaining_equations)
pick_equations init_vars (eqs @ (h :: t))
(List.filter
(fun eq -> List.for_all (fun e -> eq <> e) (h :: t)) remaining_equations)
end end
in in
(* main function of the (node-)pass. *)
let node_eq_reorganising (node: t_node): t_node option = let node_eq_reorganising (node: t_node): t_node option =
let init_vars = List.map name_of_var (snd node.n_inputs) in let init_vars = List.map name_of_var (snd node.n_inputs) in
try try
@ -851,11 +655,8 @@ let pass_eq_reordering verbose debug ast =
end end
with PassExn err -> (verbose err; None) with PassExn err -> (verbose err; None)
in in
(** iterate the pass over the nodes of the program. *)
node_pass node_eq_reorganising ast node_pass node_eq_reorganising ast
let pass_typing verbose debug ast = let pass_typing verbose debug ast =
let htbl = Hashtbl.create (List.length ast) in let htbl = Hashtbl.create (List.length ast) in
let () = debug "[typing verification]" in let () = debug "[typing verification]" in
@ -926,7 +727,7 @@ let pass_typing verbose debug ast =
else None else None
in aux ast in aux ast
let check_automata_validity verbose debug = let check_automata_validity verbos debug =
let check_automaton_branch_vars automaton = 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
@ -951,22 +752,78 @@ let check_automata_validity verbose debug =
end end
in in
let aux node = let aux node =
try
List.iter check_automaton_branch_vars node.n_automata; List.iter check_automaton_branch_vars node.n_automata;
Some node Some node
with
| PassExn err -> (verbose err; None)
in in
node_pass aux 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 default_constant ty =
let defaults ty = match ty with let defaults ty = match ty with
| TInt -> EConst([ty], CInt(0)) | TInt -> EConst([ty], CInt(0))
@ -979,273 +836,157 @@ let automaton_translation debug automaton =
| [TReal] -> EConst(ty, CReal(0.0)) | [TReal] -> EConst(ty, CReal(0.0))
| _ -> ETuple(ty, List.map defaults ty) | _ -> ETuple(ty, List.map defaults ty)
in in
let get_branch_var var branch =
Format.asprintf "_%s_%s_%d" var branch id in let rec translate_var s v explist ty = match explist with
let create_var_name var branch ty = | [] -> default_constant ty
let s = get_branch_var var branch in | (state, exp)::q ->
Hashtbl.replace new_vars s (var, branch, ty); ETriOp(Utils.type_exp exp, TOp_if,
Hashtbl.add var_seen var (s, branch, ty); EComp([TBool], COp_eq,
s EVar([TInt], IVar(s)),
in EConst([TInt], CInt(Hashtbl.find state_to_int state))
let get_branch_bool branch = ),
Format.asprintf "_b_%s_%d" branch id in exp,
let create_branch_name branch = translate_var s v q ty
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
|[] -> []
in 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; 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 exp_transition = EBinOp([TInt], BOp_arrow, EConst([TInt], CInt(1)), EMonOp([TInt], MOp_pre, transition_eq states s)) in
let state_eqs = (iter_states states) in let new_equations = [(([TInt], [IVar(s)]), exp_transition)] in
let new_eqs = state_eqs @ (List.flatten (List.map combine_var (List.of_seq (Hashtbl.to_seq_keys var_seen)))) in Hashtbl.fold (fun var explist acc -> (var, translate_var s var explist (fst var))::acc) gathered new_equations, IVar(s)
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 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 automata_translation_pass verbose debug =
let rec iter_automata autolist = match autolist with node_pass (automata_trans_pass debug)
| [] -> [], ([], [])
| 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
let clock_unification_pass verbose debug ast = 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 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 let find_clock_var var =
| EVar([TBool], var) -> acc, e match Hashtbl.find_opt known_clocks var with
| EConst([TBool], cons) -> acc, e | None ->
| EMonOp([TBool], MOp_not, e) -> count_not e (acc + 1) begin
| _ -> acc, e match var with
| BVar(name)
| IVar(name)
| RVar(name) -> raise (PassExn ("Cannot find clock of variable "^name) )
end
| Some c -> c
in in
let verify_when e1 e2 = let rec compute_clock_exp exp = match exp with
let n1, var1 = count_not e1 0 | EConst(_, _) -> [Base]
and n2, var2 = count_not e2 0 in | EVar(_, var) -> find_clock_var var
if n1 mod 2 <> n2 mod 2 || var1 <> var2 then | EMonOp(_, MOp_pre, _) -> [Base]
raise (PassExn "verify_when failure") | EMonOp(_, _, e) -> compute_clock_exp e
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
| EComp(_, _, e1, e2) | EComp(_, _, e1, e2)
| EReset(_, e1, e2) | EReset(_, e1, e2)
| EBinOp(_, _, e1, e2) -> update_clock e1 clk; update_clock e2 clk | EBinOp(_, _, e1, e2) ->
| ETriOp(_, TOp_merge, e1, e2, e3) -> begin
update_clock e1 clk; let c1 = compute_clock_exp e1
update_clock e2 (On(clk, e1)); and c2 = compute_clock_exp e2 in
update_clock e3 (On(clk, EMonOp([TBool], MOp_not, e1))) if c1 <> c2 then
| ETriOp(_, TOp_if, e1, e2, e3) -> failure "Binop"
(* The 3 expressions should have the same clock *) else
begin c1
update_clock e1 clk; end
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
| EWhen(_, e1, e2) -> | EWhen(_, e1, e2) ->
match clk with begin
| On(clk2, e) -> verify_when e e2; update_clock e1 clk2 match compute_clock_exp e1 with
| _ -> raise (PassExn "Clock unification failure: when") | [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 in
let rec propagate_clock eqs = let rec compute_eq_clock eq =
let rec step ((ty, vars), exp)= match vars with let rec step vars clks = match vars, clks with
| [] -> () | [], [] -> ()
| v::t -> let clk = Hashtbl.find known_clocks v in | [], c::q -> raise (PassExn "Mismatch between clock size")
begin | v::t, c::q -> Hashtbl.replace known_clocks v [c]; step t q
if clk <> Unknown then update_clock exp clk | l, [] -> raise (PassExn "Mismatch between clock size")
else ();
step ((ty, t), exp)
end
in in
List.iter step eqs let (_, vars), exp = eq in
let clk = compute_clock_exp exp in
step vars clk
in 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 = let compute_clock_node n =
begin begin
Hashtbl.clear known_clocks; Hashtbl.clear known_clocks;
List.iter (fun v -> Hashtbl.replace known_clocks v Unknown) ( List.iter (fun v -> Hashtbl.replace known_clocks v [Base]) (
snd n.n_inputs); (* Initializing inputs to Unknown clock *) snd n.n_inputs); (* Initializing inputs to base clock *)
List.iter (fun v -> Hashtbl.replace known_clocks v Unknown) ( List.iter compute_eq_clock n.n_equations;
snd n.n_local_vars); (* Initializing local variables to Unknown clock *) if not (List.for_all (fun v -> (Hashtbl.find known_clocks v) = [Base]) (
List.iter (fun v -> Hashtbl.replace known_clocks v Base) ( snd n.n_outputs)) then failure "Outputs" (*Checking that the node's output are on base clock *)
snd n.n_outputs); (* Initializing outputs to base clock *) else
iter_til_stable n.n_equations; Some n
(* catch potential errors and test for unification *)
check_unification n;
Some n
end end
in node_pass compute_clock_node ast 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 exception PassExn of string
let counter = ref 0 let counter = ref 0
let create_automaton_id : unit -> int = fun () -> let create_automaton_name : unit -> string = fun () ->
counter := !counter + 1; counter := !counter + 1;
!counter Format.asprintf "_s%d" (!counter)
let create_automaton_name id =
Format.asprintf "_s%d" (id)

View File

@ -16,10 +16,3 @@ let
tmp = aux (a+b, i); tmp = aux (a+b, i);
tel 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); node diagonal_int (i: int) returns (o1, o2 : int);
let let
(o1, o2) = (i, i); (o1, o2) = (i, i);
tel tel
node main (i: int) returns (o1, o2, o3, o4: int); 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 let
o = pre (true and pre( i = pre(pre(i)))); o = pre (true and pre( i = pre(pre(i))));
tel 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