Compare commits
No commits in common. "master" and "ast2C_proposition" have entirely different histories.
master
...
ast2C_prop
8
TODO
Normal file
8
TODO
Normal 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
|
||||
|
||||
# ...
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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)
|
||||
|
||||
@ -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"
|
||||
|
||||
@ -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 =
|
||||
|
||||
21
src/main.ml
21
src/main.ml
@ -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
|
||||
|
||||
|
||||
@ -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 }
|
||||
;
|
||||
|
||||
667
src/passes.ml
667
src/passes.ml
@ -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
|
||||
|
||||
@ -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)
|
||||
|
||||
@ -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
|
||||
|
||||
|
||||
@ -1,4 +0,0 @@
|
||||
node main (i: int) returns (o: int);
|
||||
let
|
||||
o = 1 -> 2 -> 3;
|
||||
tel
|
||||
@ -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
|
||||
|
||||
@ -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;
|
||||
@ -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
21
tests/test.node
Normal 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
|
||||
|
||||
@ -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);
|
||||
@ -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
|
||||
@ -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
|
||||
Loading…
Reference in New Issue
Block a user