Revision b08ffca7
src/access.ml | ||
---|---|---|
80 | 80 |
let checks = |
81 | 81 |
List.fold_left check_var_decl checks (get_node_vars nd) in |
82 | 82 |
let checks = |
83 |
List.fold_left (fun checks eq -> check_expr checks eq.eq_rhs) checks nd.node_eqs in
|
|
83 |
List.fold_left (fun checks eq -> check_expr checks eq.eq_rhs) checks (get_node_eqs nd) in
|
|
84 | 84 |
nd.node_checks <- CSet.elements checks |
85 | 85 |
|
86 | 86 |
let check_top_decl decl = |
src/automata.ml | ||
---|---|---|
13 | 13 |
open LustreSpec |
14 | 14 |
open Corelang |
15 | 15 |
|
16 |
let pp_restart fmt restart = |
|
17 |
Format.fprintf fmt "%s" (if restart then "restart" else "resume") |
|
18 |
|
|
19 |
let pp_unless fmt (_, expr, restart, st) = |
|
20 |
Format.fprintf fmt "unless %a %a %s" |
|
21 |
Printers.pp_expr expr |
|
22 |
pp_restart restart |
|
23 |
st |
|
24 |
|
|
25 |
let pp_until fmt (_, expr, restart, st) = |
|
26 |
Format.fprintf fmt "until %a %a %s" |
|
27 |
Printers.pp_expr expr |
|
28 |
pp_restart restart |
|
29 |
st |
|
30 |
|
|
31 |
let pp_handler fmt handler = |
|
32 |
Format.fprintf fmt "state %s -> %a %a let %a tel %a" |
|
33 |
handler.hand_state |
|
34 |
(Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless |
|
35 |
(fun fmt locals -> |
|
36 |
match locals with [] -> () | _ -> |
|
37 |
Format.fprintf fmt "@[<v 4>var %a@]@ " |
|
38 |
(Utils.fprintf_list ~sep:"@ " |
|
39 |
(fun fmt v -> Format.fprintf fmt "%a;" Printers.pp_node_var v)) |
|
40 |
locals) |
|
41 |
handler.hand_locals |
|
42 |
Printers.pp_node_eqs handler.hand_eqs |
|
43 |
(Utils.fprintf_list ~sep:"@ " pp_until) handler.hand_until |
|
44 |
|
|
45 |
let pp_automata fmt aut = |
|
46 |
Format.fprintf fmt "automaton %s %a" |
|
47 |
aut.aut_id |
|
48 |
(Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers |
|
49 |
|
|
50 | 16 |
let mkbool loc b = |
51 | 17 |
mkexpr loc (Expr_const (const_of_bool b)) |
52 | 18 |
|
... | ... | |
62 | 28 |
let add_branch (loc, expr, restart, st) cont = |
63 | 29 |
mkexpr loc (Expr_ite (expr, mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st]), cont)) |
64 | 30 |
|
65 |
let mkhandler loc st unless until locals (eqs, asserts, annots) =
|
|
31 |
let mkhandler loc st unless until locals (stmts, asserts, annots) =
|
|
66 | 32 |
{hand_state = st; |
67 | 33 |
hand_unless = unless; |
68 | 34 |
hand_until = until; |
69 | 35 |
hand_locals = locals; |
70 |
hand_eqs = eqs;
|
|
36 |
hand_stmts = stmts;
|
|
71 | 37 |
hand_asserts = asserts; |
72 | 38 |
hand_annots = annots; |
73 | 39 |
hand_loc = loc} |
... | ... | |
77 | 43 |
aut_handlers = handlers; |
78 | 44 |
aut_loc = loc} |
79 | 45 |
|
80 |
let handler_read handler = |
|
81 |
List.fold_left (fun read eq -> get_expr_vars read eq.eq_rhs) ISet.empty handler.hand_eqs |
|
82 |
|
|
83 |
let handler_write handler = |
|
84 |
List.fold_left (fun write eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs) ISet.empty handler.hand_eqs |
|
46 |
let rec handler_read reads handler = |
|
47 |
let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in |
|
48 |
let allvars = |
|
49 |
List.fold_left (fun read stmt -> |
|
50 |
match stmt with |
|
51 |
| Eq eq -> get_expr_vars read eq.eq_rhs |
|
52 |
| Aut aut -> List.fold_left handler_read read aut.aut_handlers ) reads handler.hand_stmts |
|
53 |
in ISet.diff allvars locals |
|
54 |
|
|
55 |
let rec handler_write writes handler = |
|
56 |
let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in |
|
57 |
let allvars = |
|
58 |
List.fold_left (fun write stmt -> |
|
59 |
match stmt with |
|
60 |
| Eq eq -> List.fold_left (fun write v -> ISet.add v write) write eq.eq_lhs |
|
61 |
| Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts |
|
62 |
in ISet.diff allvars locals |
|
85 | 63 |
|
86 | 64 |
let node_of_handler node aut_id handler = |
87 |
let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in |
|
88 |
let inputs = handler_read handler in |
|
89 |
let outputs = handler_write handler in |
|
65 |
let inputs = handler_read ISet.empty handler in |
|
66 |
let outputs = handler_write ISet.empty handler in |
|
90 | 67 |
{ |
91 | 68 |
node_id = Format.sprintf "%s_%s_handler" aut_id handler.hand_state; |
92 | 69 |
node_type = Types.new_var (); |
93 | 70 |
node_clock = Clocks.new_var true; |
94 |
node_inputs = List.map (fun v -> get_node_var v node) (ISet.elements (ISet.diff inputs locals));
|
|
95 |
node_outputs = List.map (fun v -> get_node_var v node) (ISet.elements (ISet.diff outputs locals));
|
|
71 |
node_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs);
|
|
72 |
node_outputs = List.map (fun v -> get_node_var v node) (ISet.elements outputs);
|
|
96 | 73 |
node_locals = handler.hand_locals; |
97 | 74 |
node_gencalls = []; |
98 | 75 |
node_checks = []; |
99 | 76 |
node_asserts = handler.hand_asserts; |
100 |
node_eqs = handler.hand_eqs;
|
|
77 |
node_stmts = handler.hand_stmts;
|
|
101 | 78 |
node_dec_stateless = false; |
102 | 79 |
node_stateless = None; |
103 | 80 |
node_spec = None; |
... | ... | |
111 | 88 |
let arg = mkexpr loc (Expr_tuple (List.map (fun v -> mkident loc v.var_id) node.node_inputs)) in |
112 | 89 |
mkexpr loc (Expr_when (mkexpr loc (Expr_appl (node.node_id, arg, Some (restart, tag_true))), state, tag)) |
113 | 90 |
|
114 |
let assign_aut_handlers loc node actual_r actual_s hnodes =
|
|
91 |
let assign_aut_handlers loc actual_r actual_s hnodes = |
|
115 | 92 |
let outputs = (snd (List.hd hnodes)).node_outputs in |
116 | 93 |
let assign_handlers = List.map (fun (hs, n) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in |
117 | 94 |
let assign_expr = mkexpr loc (Expr_merge (actual_s, assign_handlers)) in |
... | ... | |
123 | 100 |
{ tydef_id = tname; |
124 | 101 |
tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers) |
125 | 102 |
} |
103 |
(* |
|
104 |
let expand_automata_stmt (top_decls, locals, eqs) stmt = |
|
105 |
match stmt with |
|
106 |
| Eq eq -> (top_decls, locals, eq::eqs) |
|
107 |
| Aut aut -> |
|
108 |
|
|
126 | 109 |
|
127 | 110 |
let expand_automata top_node aut = |
128 | 111 |
let node = node_of_top top_node in |
... | ... | |
141 | 124 |
let fby_until_expr = mkfby aut.aut_loc (init aut.aut_loc tag_false initial) until_expr in |
142 | 125 |
let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in |
143 | 126 |
let hnodes = List.map (fun h -> (h.hand_state, node_of_handler node aut.aut_id h)) aut.aut_handlers in |
144 |
let assign_eq = assign_aut_handlers aut.aut_loc node actual_r actual_s hnodes in
|
|
127 |
let assign_eq = assign_aut_handlers aut.aut_loc actual_r actual_s hnodes in |
|
145 | 128 |
let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in |
146 | 129 |
let tydec_const id = { ty_dec_desc = Tydec_const id; ty_dec_loc = aut.aut_loc } in |
147 | 130 |
let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in |
... | ... | |
149 | 132 |
mkvar_decl aut.aut_loc (actual_r , tydec_bool, ckdec_any, false); |
150 | 133 |
mkvar_decl aut.aut_loc (incoming_s, tydec_const typedef.tydef_id, ckdec_any, false); |
151 | 134 |
mkvar_decl aut.aut_loc (actual_s , tydec_const typedef.tydef_id, ckdec_any, false)] in |
152 |
let eqs' = [unless_eq; assign_eq; until_eq] in
|
|
153 |
let node' = { node with node_locals = locals'@node.node_locals; node_eqs = eqs'@node.node_eqs } in
|
|
135 |
let eqs' = [Eq unless_eq; Eq assign_eq; Eq until_eq] in
|
|
136 |
let node' = { node with node_locals = locals'@node.node_locals; node_stmts = eqs'@node.node_stmts } in
|
|
154 | 137 |
(mktop_decl aut.aut_loc owner false (TypeDef typedef)) :: |
155 | 138 |
{ top_node with top_decl_desc = Node node' } :: |
156 | 139 |
(List.map2 (fun h (hs, n) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes) |
157 |
|
|
158 |
let node_extract_automata top_decl = |
|
140 |
*) |
|
141 |
let rec node_extract_automata top_decl =
|
|
159 | 142 |
match top_decl.top_decl_desc with |
160 |
| Node nd -> [top_decl]
|
|
143 |
| Node nd -> [] |
|
161 | 144 |
| _ -> [top_decl] |
162 | 145 |
(* |
163 | 146 |
let extract_automata top_decls = |
src/backends/C/c_backend_common.ml | ||
---|---|---|
24 | 24 |
|
25 | 25 |
(* Generation of a non-clashing name for the self memory variable (for step and reset functions) *) |
26 | 26 |
let mk_self m = |
27 |
mk_new_name (m.mstep.step_inputs@m.mstep.step_outputs@m.mstep.step_locals@m.mmemory) "self" |
|
27 |
let used name = |
|
28 |
(List.exists (fun v -> v.var_id = name) m.mstep.step_inputs) |
|
29 |
|| (List.exists (fun v -> v.var_id = name) m.mstep.step_outputs) |
|
30 |
|| (List.exists (fun v -> v.var_id = name) m.mstep.step_locals) |
|
31 |
|| (List.exists (fun v -> v.var_id = name) m.mmemory) in |
|
32 |
mk_new_name used "self" |
|
28 | 33 |
|
29 | 34 |
(* Generation of a non-clashing name for the instance variable of static allocation macro *) |
30 | 35 |
let mk_instance m = |
31 |
mk_new_name (m.mstep.step_inputs@m.mmemory) "inst" |
|
36 |
let used name = |
|
37 |
(List.exists (fun v -> v.var_id = name) m.mstep.step_inputs) |
|
38 |
|| (List.exists (fun v -> v.var_id = name) m.mmemory) in |
|
39 |
mk_new_name used "inst" |
|
32 | 40 |
|
33 | 41 |
(* Generation of a non-clashing name for the attribute variable of static allocation macro *) |
34 | 42 |
let mk_attribute m = |
35 |
mk_new_name (m.mstep.step_inputs@m.mmemory) "attr" |
|
43 |
let used name = |
|
44 |
(List.exists (fun v -> v.var_id = name) m.mstep.step_inputs) |
|
45 |
|| (List.exists (fun v -> v.var_id = name) m.mmemory) in |
|
46 |
mk_new_name used "attr" |
|
36 | 47 |
|
37 | 48 |
let mk_call_var_decl loc id = |
38 | 49 |
{ var_id = id; |
src/backends/C/c_backend_header.ml | ||
---|---|---|
172 | 172 |
else |
173 | 173 |
begin |
174 | 174 |
let static_inputs = List.filter (fun v -> v.var_dec_const) inode.nodei_inputs in |
175 |
let self = mk_new_name (inode.nodei_inputs@inode.nodei_outputs) "self" in |
|
175 |
let used name = |
|
176 |
(List.exists (fun v -> v.var_id = name) inode.nodei_inputs) |
|
177 |
|| (List.exists (fun v -> v.var_id = name) inode.nodei_outputs) in |
|
178 |
let self = mk_new_name used "self" in |
|
176 | 179 |
fprintf fmt "extern %a;@.@." |
177 | 180 |
(print_reset_prototype self) (inode.nodei_id, static_inputs); |
178 | 181 |
|
src/causality.ml | ||
---|---|---|
121 | 121 |
match_mem eq.eq_lhs eq.eq_rhs mems |
122 | 122 |
|
123 | 123 |
let node_memory_variables nd = |
124 |
List.fold_left eq_memory_variables ISet.empty nd.node_eqs
|
|
124 |
List.fold_left eq_memory_variables ISet.empty (get_node_eqs nd)
|
|
125 | 125 |
|
126 | 126 |
let node_input_variables nd = |
127 | 127 |
List.fold_left (fun inputs v -> ISet.add v.var_id inputs) ISet.empty nd.node_inputs |
... | ... | |
149 | 149 |
let first = List.hd eq.eq_lhs in |
150 | 150 |
List.iter (fun v -> Hashtbl.add eq_equiv v first) eq.eq_lhs |
151 | 151 |
) |
152 |
nd.node_eqs;
|
|
152 |
(get_node_eqs nd);
|
|
153 | 153 |
eq_equiv |
154 | 154 |
|
155 | 155 |
(* Create a tuple of right dimension, according to [expr] type, *) |
... | ... | |
255 | 255 |
instance_var_cpt := 0; |
256 | 256 |
let g = new_graph (), new_graph () in |
257 | 257 |
(* Basic dependencies *) |
258 |
let g = List.fold_right (add_eq_dependencies mems inputs node_vars) n.node_eqs g in
|
|
258 |
let g = List.fold_right (add_eq_dependencies mems inputs node_vars) (get_node_eqs n) g in
|
|
259 | 259 |
g |
260 | 260 |
|
261 | 261 |
end |
... | ... | |
312 | 312 |
| Node nd -> |
313 | 313 |
(*Format.eprintf "Computing deps of node %s@.@?" nd.node_id; *) |
314 | 314 |
let accu = add_vertices [nd.node_id] accu in |
315 |
let deps = List.map (fun e -> fst (desome (get_callee e))) (get_calls (fun _ -> true) nd.node_eqs) in
|
|
315 |
let deps = List.map (fun e -> fst (desome (get_callee e))) (get_calls (fun _ -> true) (get_node_eqs nd)) in
|
|
316 | 316 |
(*Format.eprintf "%a@.@?" (Utils.fprintf_list ~sep:"@." Format.pp_print_string) deps; *) |
317 | 317 |
add_edges [nd.node_id] deps accu |
318 | 318 |
| _ -> assert false (* should not happen *) |
... | ... | |
332 | 332 |
match td.top_decl_desc with |
333 | 333 |
| Node nd -> |
334 | 334 |
let prednode n = is_generic_node (Hashtbl.find node_table n) in |
335 |
nd.node_gencalls <- get_calls prednode nd.node_eqs
|
|
335 |
nd.node_gencalls <- get_calls prednode (get_node_eqs nd)
|
|
336 | 336 |
| _ -> () |
337 | 337 |
|
338 | 338 |
) prog |
... | ... | |
345 | 345 |
module Cycles = Graph.Components.Make (IdentDepGraph) |
346 | 346 |
|
347 | 347 |
let mk_copy_var n id = |
348 |
mk_new_name (get_node_vars n) id |
|
348 |
let used name = |
|
349 |
(List.exists (fun v -> v.var_id = name) n.node_locals) |
|
350 |
|| (List.exists (fun v -> v.var_id = name) n.node_inputs) |
|
351 |
|| (List.exists (fun v -> v.var_id = name) n.node_outputs) |
|
352 |
in mk_new_name used id |
|
349 | 353 |
|
350 | 354 |
let mk_copy_eq n var = |
351 | 355 |
let var_decl = get_node_var var n in |
... | ... | |
407 | 411 |
- a modified acyclic version of [g] |
408 | 412 |
*) |
409 | 413 |
let break_cycles node mems g = |
410 |
let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) node.node_eqs in
|
|
414 |
let (mem_eqs, non_mem_eqs) = List.partition (fun eq -> List.exists (fun v -> ISet.mem v mems) eq.eq_lhs) (get_node_eqs node) in
|
|
411 | 415 |
let rec break vdecls mem_eqs g = |
412 | 416 |
let scc_l = Cycles.scc_list g in |
413 | 417 |
let wrong = List.filter (wrong_partition g) scc_l in |
... | ... | |
553 | 557 |
begin |
554 | 558 |
merge_with g_non_mems g_mems'; |
555 | 559 |
add_external_dependency outputs mems g_non_mems; |
556 |
{ node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals },
|
|
560 |
{ node with node_stmts = List.map (fun eq -> Eq eq) eqs'; node_locals = vdecls'@node.node_locals },
|
|
557 | 561 |
g_non_mems |
558 | 562 |
end |
559 | 563 |
|
src/clock_calculus.ml | ||
---|---|---|
771 | 771 |
let new_env = clock_var_decl_list env false nd.node_inputs in |
772 | 772 |
let new_env = clock_var_decl_list new_env true nd.node_outputs in |
773 | 773 |
let new_env = clock_var_decl_list new_env true nd.node_locals in |
774 |
List.iter (clock_eq new_env) nd.node_eqs;
|
|
774 |
List.iter (clock_eq new_env) (get_node_eqs nd);
|
|
775 | 775 |
let ck_ins = clock_of_vlist nd.node_inputs in |
776 | 776 |
let ck_outs = clock_of_vlist nd.node_outputs in |
777 | 777 |
let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in |
src/corelang.ml | ||
---|---|---|
68 | 68 |
var_clock = Clocks.new_var false; |
69 | 69 |
var_loc = c.const_loc } |
70 | 70 |
|
71 |
let mk_new_name vdecl_list id =
|
|
71 |
let mk_new_name used id =
|
|
72 | 72 |
let rec new_name name cpt = |
73 |
if List.exists (fun v -> v.var_id = name) vdecl_list
|
|
73 |
if used name
|
|
74 | 74 |
then new_name (sprintf "_%s_%i" id cpt) (cpt+1) |
75 | 75 |
else name |
76 | 76 |
in new_name id 1 |
... | ... | |
475 | 475 |
|
476 | 476 |
let get_node_var id node = get_var id (get_node_vars node) |
477 | 477 |
|
478 |
let get_node_eqs = |
|
479 |
let get_eqs stmts = |
|
480 |
List.fold_right |
|
481 |
(fun stmt res -> |
|
482 |
match stmt with |
|
483 |
| Eq eq -> eq :: res |
|
484 |
| Aut _ -> assert false) |
|
485 |
stmts |
|
486 |
[] in |
|
487 |
let table_eqs = Hashtbl.create 23 in |
|
488 |
(fun nd -> |
|
489 |
try |
|
490 |
let (old, res) = Hashtbl.find table_eqs nd.node_id |
|
491 |
in if old == nd.node_stmts then res else raise Not_found |
|
492 |
with Not_found -> |
|
493 |
let res = get_eqs nd.node_stmts in |
|
494 |
begin |
|
495 |
Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res); |
|
496 |
res |
|
497 |
end) |
|
498 |
|
|
478 | 499 |
let get_node_eq id node = |
479 |
List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
|
|
500 |
List.find (fun eq -> List.mem id eq.eq_lhs) (get_node_eqs node)
|
|
480 | 501 |
|
481 | 502 |
let get_nodes prog = |
482 | 503 |
List.fold_left ( |
... | ... | |
639 | 660 |
rename_expr f_node f_var f_const expr}) |
640 | 661 |
nd.node_asserts |
641 | 662 |
in |
642 |
let eqs = List.map rename_eq nd.node_eqs in
|
|
663 |
let node_stmts = List.map (fun eq -> Eq (rename_eq eq)) (get_node_eqs nd) in
|
|
643 | 664 |
let spec = |
644 | 665 |
Utils.option_map |
645 | 666 |
(fun s -> rename_node_annot f_node f_var f_const s) |
... | ... | |
660 | 681 |
node_gencalls = gen_calls; |
661 | 682 |
node_checks = node_checks; |
662 | 683 |
node_asserts = node_asserts; |
663 |
node_eqs = eqs;
|
|
684 |
node_stmts = node_stmts;
|
|
664 | 685 |
node_dec_stateless = nd.node_dec_stateless; |
665 | 686 |
node_stateless = nd.node_stateless; |
666 | 687 |
node_spec = spec; |
... | ... | |
889 | 910 |
and get_eq_calls nodes eq = |
890 | 911 |
get_expr_calls nodes eq.eq_rhs |
891 | 912 |
and get_node_calls nodes node = |
892 |
List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs
|
|
913 |
List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node)
|
|
893 | 914 |
|
894 | 915 |
let rec get_expr_vars vars e = |
895 | 916 |
get_expr_desc_vars vars e.expr_desc |
... | ... | |
932 | 953 |
and eq_has_arrows eq = |
933 | 954 |
expr_has_arrows eq.eq_rhs |
934 | 955 |
and node_has_arrows node = |
935 |
List.exists (fun eq -> eq_has_arrows eq) node.node_eqs
|
|
956 |
List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node)
|
|
936 | 957 |
|
937 | 958 |
(* Local Variables: *) |
938 | 959 |
(* compile-command:"make -C .." *) |
src/corelang.mli | ||
---|---|---|
26 | 26 |
val mkassert: Location.t -> expr -> assert_t |
27 | 27 |
val mktop_decl: Location.t -> ident -> bool -> top_decl_desc -> top_decl |
28 | 28 |
val mkpredef_call: Location.t -> ident -> expr list -> expr |
29 |
val mk_new_name: var_decl list -> ident -> ident
|
|
29 |
val mk_new_name: (ident -> bool) -> ident -> ident
|
|
30 | 30 |
|
31 | 31 |
|
32 | 32 |
val node_table : (ident, top_decl) Hashtbl.t |
... | ... | |
65 | 65 |
|
66 | 66 |
val get_node_vars: node_desc -> var_decl list |
67 | 67 |
val get_node_var: ident -> node_desc -> var_decl |
68 |
val get_node_eqs: node_desc -> eq list |
|
68 | 69 |
val get_node_eq: ident -> node_desc -> eq |
69 | 70 |
val get_node_interface: node_desc -> imported_node_desc |
70 | 71 |
|
src/inliner.ml | ||
---|---|---|
46 | 46 |
node.node_id uid v; |
47 | 47 |
Format.flush_str_formatter ()) |
48 | 48 |
in |
49 |
let eqs' = List.map (rename_eq rename) node.node_eqs
|
|
49 |
let eqs' = List.map (rename_eq rename) (get_node_eqs node)
|
|
50 | 50 |
in |
51 | 51 |
let rename_var v = { v with var_id = rename v.var_id } in |
52 | 52 |
let inputs' = List.map rename_var node.node_inputs in |
... | ... | |
171 | 171 |
inline_expr eq.eq_rhs locals nodes |
172 | 172 |
in |
173 | 173 |
locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts |
174 |
) (nd.node_locals, [], nd.node_asserts) nd.node_eqs
|
|
174 |
) (nd.node_locals, [], nd.node_asserts) (get_node_eqs nd)
|
|
175 | 175 |
in |
176 | 176 |
{ nd with |
177 | 177 |
node_locals = new_locals; |
178 |
node_eqs = eqs;
|
|
178 |
node_stmts = List.map (fun eq -> Eq eq) eqs;
|
|
179 | 179 |
node_asserts = asserts; |
180 | 180 |
} |
181 | 181 |
|
... | ... | |
241 | 241 |
|
242 | 242 |
(* Building main node *) |
243 | 243 |
|
244 |
let ok_i_eq = |
|
245 |
{ eq_loc = loc; |
|
246 |
eq_lhs = List.map (fun v -> v.var_id) ok_i; |
|
247 |
eq_rhs = |
|
248 |
let inputs = expr_of_expr_list loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in |
|
249 |
let call_orig = |
|
250 |
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in |
|
251 |
let call_inlined = |
|
252 |
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in |
|
253 |
let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in |
|
254 |
mkexpr loc (Expr_appl ("=", args, None)) |
|
255 |
} in |
|
256 |
let ok_eq = |
|
257 |
{ eq_loc = loc; |
|
258 |
eq_lhs = [ok_ident]; |
|
259 |
eq_rhs = main_ok_expr; |
|
260 |
} in |
|
244 | 261 |
let main_node = { |
245 | 262 |
node_id = "check"; |
246 | 263 |
node_type = Types.new_var (); |
... | ... | |
251 | 268 |
node_gencalls = []; |
252 | 269 |
node_checks = []; |
253 | 270 |
node_asserts = []; |
254 |
node_eqs = [ |
|
255 |
{ eq_loc = loc; |
|
256 |
eq_lhs = List.map (fun v -> v.var_id) ok_i; |
|
257 |
eq_rhs = |
|
258 |
let inputs = expr_of_expr_list loc (List.map (fun v -> mkexpr loc (Expr_ident v.var_id)) main_orig_node.node_inputs) in |
|
259 |
let call_orig = |
|
260 |
mkexpr loc (Expr_appl ("orig_" ^ main_name, inputs, None)) in |
|
261 |
let call_inlined = |
|
262 |
mkexpr loc (Expr_appl ("inlined_" ^ main_name, inputs, None)) in |
|
263 |
let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in |
|
264 |
mkexpr loc (Expr_appl ("=", args, None)) |
|
265 |
}; |
|
266 |
{ eq_loc = loc; |
|
267 |
eq_lhs = [ok_ident]; |
|
268 |
eq_rhs = main_ok_expr; |
|
269 |
} |
|
270 |
]; |
|
271 |
node_stmts = [Eq ok_i_eq; Eq ok_eq]; |
|
271 | 272 |
node_dec_stateless = false; |
272 | 273 |
node_stateless = None; |
273 | 274 |
node_spec = Some |
src/lustreSpec.ml | ||
---|---|---|
135 | 135 |
{ |
136 | 136 |
assert_expr: expr; |
137 | 137 |
assert_loc: Location.t; |
138 |
} |
|
138 |
} |
|
139 |
|
|
140 |
type statement = |
|
141 |
| Eq of eq |
|
142 |
| Aut of automata_desc |
|
139 | 143 |
|
140 |
type automata_desc =
|
|
144 |
and automata_desc =
|
|
141 | 145 |
{aut_id : ident; |
142 | 146 |
aut_handlers: handler_desc list; |
143 | 147 |
aut_loc: Location.t} |
... | ... | |
147 | 151 |
hand_unless: (Location.t * expr * bool * ident) list; |
148 | 152 |
hand_until: (Location.t * expr * bool * ident) list; |
149 | 153 |
hand_locals: var_decl list; |
150 |
hand_eqs: eq list;
|
|
154 |
hand_stmts: statement list;
|
|
151 | 155 |
hand_asserts: assert_t list; |
152 | 156 |
hand_annots: expr_annot list; |
153 | 157 |
hand_loc: Location.t} |
154 | 158 |
|
155 |
type statement = |
|
156 |
| Eq of eq |
|
157 |
| Aut of automata_desc |
|
158 |
|
|
159 | 159 |
type node_desc = |
160 | 160 |
{node_id: ident; |
161 | 161 |
mutable node_type: Types.type_expr; |
... | ... | |
166 | 166 |
mutable node_gencalls: expr list; |
167 | 167 |
mutable node_checks: Dimension.dim_expr list; |
168 | 168 |
node_asserts: assert_t list; |
169 |
node_eqs: eq list;
|
|
169 |
node_stmts: statement list;
|
|
170 | 170 |
mutable node_dec_stateless: bool; |
171 | 171 |
mutable node_stateless: bool option; |
172 | 172 |
node_spec: node_annot option; |
src/machine_code.ml | ||
---|---|---|
156 | 156 |
node_gencalls = []; |
157 | 157 |
node_checks = []; |
158 | 158 |
node_asserts = []; |
159 |
node_eqs= [];
|
|
159 |
node_stmts= [];
|
|
160 | 160 |
node_dec_stateless = false; |
161 | 161 |
node_stateless = Some false; |
162 | 162 |
node_spec = None; |
... | ... | |
428 | 428 |
(* Format.eprintf "%s schedule: %a@." |
429 | 429 |
nd.node_id |
430 | 430 |
(Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*) |
431 |
let split_eqs = Splitting.tuple_split_eq_list nd.node_eqs in
|
|
431 |
let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in
|
|
432 | 432 |
let eqs_rev, remainder = |
433 | 433 |
List.fold_left |
434 | 434 |
(fun (accu, node_eqs_remainder) vl -> |
... | ... | |
446 | 446 |
if List.length remainder > 0 then ( |
447 | 447 |
Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?" |
448 | 448 |
Printers.pp_node_eqs remainder |
449 |
Printers.pp_node_eqs nd.node_eqs;
|
|
449 |
Printers.pp_node_eqs (get_node_eqs nd);
|
|
450 | 450 |
assert false); |
451 | 451 |
List.rev eqs_rev |
452 | 452 |
end |
src/normalization.ml | ||
---|---|---|
349 | 349 |
List.for_all ((!=) v) inputs_outputs in |
350 | 350 |
let orig_vars = inputs_outputs@node.node_locals in |
351 | 351 |
let defs, vars = |
352 |
List.fold_left (normalize_eq node) ([], orig_vars) node.node_eqs in
|
|
352 |
List.fold_left (normalize_eq node) ([], orig_vars) (get_node_eqs node) in
|
|
353 | 353 |
(* Normalize the asserts *) |
354 | 354 |
let vars, assert_defs, asserts = |
355 | 355 |
List.fold_left ( |
... | ... | |
391 | 391 |
let node = |
392 | 392 |
{ node with |
393 | 393 |
node_locals = new_locals; |
394 |
node_eqs = defs @ assert_defs;
|
|
394 |
node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
|
|
395 | 395 |
node_asserts = asserts; |
396 | 396 |
node_annot = norm_traceability::node.node_annot; |
397 | 397 |
} |
src/optimize_prog.ml | ||
---|---|---|
46 | 46 |
{ eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs } |
47 | 47 |
|
48 | 48 |
let node_unfold_consts consts node = |
49 |
{ node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs }
|
|
49 |
{ node with node_stmts = List.map (fun eq -> Eq (eq_unfold_consts consts eq)) (get_node_eqs node) }
|
|
50 | 50 |
|
51 | 51 |
let prog_unfold_consts prog = |
52 | 52 |
let consts = List.map const_of_top (get_consts prog) in |
... | ... | |
89 | 89 |
{ eq with eq_rhs = expr_distribute_when eq.eq_rhs } |
90 | 90 |
|
91 | 91 |
let node_distribute_when node = |
92 |
{ node with node_eqs = List.map eq_distribute_when node.node_eqs }
|
|
92 |
{ node with node_stmts = List.map (fun eq -> Eq (eq_distribute_when eq)) (get_node_eqs node) }
|
|
93 | 93 |
|
94 | 94 |
let prog_distribute_when prog = |
95 | 95 |
List.map ( |
src/parser_lustre.mly | ||
---|---|---|
188 | 188 |
|
189 | 189 |
top_decl: |
190 | 190 |
| CONST cdecl_list { List.rev ($2 false) } |
191 |
| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL
|
|
192 |
{let eqs, asserts, annots = $16 in
|
|
191 |
| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL
|
|
192 |
{let stmts, asserts, annots = $16 in
|
|
193 | 193 |
let nd = mktop_decl false (Node |
194 | 194 |
{node_id = $3; |
195 | 195 |
node_type = Types.new_var (); |
... | ... | |
200 | 200 |
node_gencalls = []; |
201 | 201 |
node_checks = []; |
202 | 202 |
node_asserts = asserts; |
203 |
node_eqs = eqs;
|
|
203 |
node_stmts = stmts;
|
|
204 | 204 |
node_dec_stateless = $2; |
205 | 205 |
node_stateless = None; |
206 | 206 |
node_spec = $1; |
... | ... | |
251 | 251 |
field_list: { [] } |
252 | 252 |
| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 } |
253 | 253 |
|
254 |
eq_list:
|
|
254 |
stmt_list:
|
|
255 | 255 |
{ [], [], [] } |
256 |
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
|
|
257 |
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
|
|
258 |
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
|
|
259 |
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
|
|
256 |
| eq stmt_list {let eql, assertl, annotl = $2 in ((Eq $1)::eql), assertl, annotl}
|
|
257 |
| assert_ stmt_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
|
|
258 |
| ANNOT stmt_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
|
|
259 |
| automaton stmt_list {let eql, assertl, annotl = $2 in ((Aut $1)::eql), assertl, annotl}
|
|
260 | 260 |
|
261 | 261 |
automaton: |
262 | 262 |
AUTOMATON type_ident handler_list { (Automata.mkautomata (get_loc ()) $2 $3); failwith "not implemented" } |
... | ... | |
266 | 266 |
| handler handler_list { $1::$2 } |
267 | 267 |
|
268 | 268 |
handler: |
269 |
STATE UIDENT ARROW unless_list locals LET eq_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
|
|
269 |
STATE UIDENT ARROW unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
|
|
270 | 270 |
|
271 | 271 |
unless_list: |
272 | 272 |
{ [] } |
src/printers.ml | ||
---|---|---|
131 | 131 |
pp_eq_lhs eq.eq_lhs |
132 | 132 |
pp_expr eq.eq_rhs |
133 | 133 |
|
134 |
let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq |
|
134 |
let pp_restart fmt restart = |
|
135 |
Format.fprintf fmt "%s" (if restart then "restart" else "resume") |
|
136 |
|
|
137 |
let pp_unless fmt (_, expr, restart, st) = |
|
138 |
Format.fprintf fmt "unless %a %a %s" |
|
139 |
pp_expr expr |
|
140 |
pp_restart restart |
|
141 |
st |
|
142 |
|
|
143 |
let pp_until fmt (_, expr, restart, st) = |
|
144 |
Format.fprintf fmt "until %a %a %s" |
|
145 |
pp_expr expr |
|
146 |
pp_restart restart |
|
147 |
st |
|
148 |
|
|
149 |
let rec pp_handler fmt handler = |
|
150 |
Format.fprintf fmt "state %s -> %a %a let %a tel %a" |
|
151 |
handler.hand_state |
|
152 |
(Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless |
|
153 |
(fun fmt locals -> |
|
154 |
match locals with [] -> () | _ -> |
|
155 |
Format.fprintf fmt "@[<v 4>var %a@]@ " |
|
156 |
(Utils.fprintf_list ~sep:"@ " |
|
157 |
(fun fmt v -> Format.fprintf fmt "%a;" pp_node_var v)) |
|
158 |
locals) |
|
159 |
handler.hand_locals |
|
160 |
pp_node_stmts handler.hand_stmts |
|
161 |
(Utils.fprintf_list ~sep:"@ " pp_until) handler.hand_until |
|
162 |
|
|
163 |
and pp_node_stmt fmt stmt = |
|
164 |
match stmt with |
|
165 |
| Eq eq -> pp_node_eq fmt eq |
|
166 |
| Aut aut -> pp_node_aut fmt aut |
|
167 |
|
|
168 |
and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts |
|
169 |
|
|
170 |
and pp_node_aut fmt aut = |
|
171 |
Format.fprintf fmt "automaton %s %a" |
|
172 |
aut.aut_id |
|
173 |
(Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers |
|
174 |
|
|
175 |
and pp_node_eqs fmt eqs = fprintf_list ~sep:"@ " pp_node_eq fmt eqs |
|
135 | 176 |
|
136 | 177 |
let rec pp_var_struct_type_field fmt (label, tdesc) = |
137 | 178 |
fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc |
... | ... | |
217 | 258 |
checks |
218 | 259 |
) nd.node_checks |
219 | 260 |
(fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot |
220 |
pp_node_eqs nd.node_eqs
|
|
261 |
pp_node_stmts nd.node_stmts
|
|
221 | 262 |
pp_asserts nd.node_asserts |
222 | 263 |
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*) |
223 | 264 |
|
src/stateless.ml | ||
---|---|---|
36 | 36 |
check_expr e' && |
37 | 37 |
(Basic_library.is_internal_fun i || check_node (node_from_name i)) |
38 | 38 |
and compute_node nd = |
39 |
List.for_all (fun eq -> check_expr eq.eq_rhs) nd.node_eqs
|
|
39 |
List.for_all (fun eq -> check_expr eq.eq_rhs) (get_node_eqs nd)
|
|
40 | 40 |
and check_node td = |
41 | 41 |
match td.top_decl_desc with |
42 | 42 |
| Node nd -> ( |
src/typing.ml | ||
---|---|---|
619 | 619 |
(fun uvs v -> IMap.add v.var_id () uvs) |
620 | 620 |
IMap.empty vd_env_ol in |
621 | 621 |
let undefined_vars = |
622 |
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init nd.node_eqs
|
|
622 |
List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init (get_node_eqs nd)
|
|
623 | 623 |
in |
624 | 624 |
(* Typing asserts *) |
625 | 625 |
List.iter (fun assert_ -> |
Also available in: Unified diff