Revision 54d032f5
src/automata.ml | ||
---|---|---|
22 | 22 |
let mkfby loc e1 e2 = |
23 | 23 |
mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2))) |
24 | 24 |
|
25 |
let init loc restart state =
|
|
25 |
let mkidentpair loc restart state =
|
|
26 | 26 |
mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state]) |
27 | 27 |
|
28 | 28 |
let add_branch (loc, expr, restart, st) cont = |
... | ... | |
61 | 61 |
| Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts |
62 | 62 |
in ISet.diff allvars locals |
63 | 63 |
|
64 |
let node_of_handler nused node aut_id handler = |
|
65 |
let inputs = handler_read ISet.empty handler in |
|
64 |
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name) |
|
65 |
|
|
66 |
let rec rename_stmts_outputs frename stmts = |
|
67 |
match stmts with |
|
68 |
| [] -> [] |
|
69 |
| (Eq eq) :: q -> let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in |
|
70 |
eq' :: rename_stmts_outputs frename q |
|
71 |
| (Aut aut) :: q -> let handlers' = List.map (fun h -> { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts}) aut.aut_handlers in |
|
72 |
let aut' = Aut { aut with aut_handlers = handlers' } in |
|
73 |
aut' :: rename_stmts_outputs frename q |
|
74 |
|
|
75 |
let mk_frename used outputs = |
|
76 |
let table = ISet.fold (fun name table -> IMap.add name (rename_output used name) table) outputs IMap.empty in |
|
77 |
(fun name -> try IMap.find name table with Not_found -> name) |
|
78 |
|
|
79 |
let node_of_handler nused used node aut_id handler = |
|
66 | 80 |
let outputs = handler_write ISet.empty handler in |
81 |
let (new_locals, inputs) = ISet.partition (fun v -> ISet.mem v outputs) (handler_read ISet.empty handler) in |
|
82 |
let frename = mk_frename used outputs in |
|
83 |
let var_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs) in |
|
84 |
let new_var_locals = List.map (fun v -> get_node_var v node) (ISet.elements new_locals) in |
|
85 |
let var_outputs = List.map (fun v -> get_node_var v node) (ISet.elements outputs) in |
|
86 |
let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in |
|
87 |
let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in |
|
88 |
var_outputs, |
|
67 | 89 |
{ |
68 | 90 |
node_id = mk_new_name nused (Format.sprintf "%s_%s_handler" aut_id handler.hand_state); |
69 | 91 |
node_type = Types.new_var (); |
70 | 92 |
node_clock = Clocks.new_var true; |
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);
|
|
73 |
node_locals = handler.hand_locals; |
|
93 |
node_inputs = var_inputs;
|
|
94 |
node_outputs = new_var_outputs;
|
|
95 |
node_locals = new_var_locals @ handler.hand_locals;
|
|
74 | 96 |
node_gencalls = []; |
75 | 97 |
node_checks = []; |
76 | 98 |
node_asserts = handler.hand_asserts; |
77 |
node_stmts = handler.hand_stmts; |
|
99 |
node_stmts = new_output_eqs @ handler.hand_stmts;
|
|
78 | 100 |
node_dec_stateless = false; |
79 | 101 |
node_stateless = None; |
80 | 102 |
node_spec = None; |
... | ... | |
82 | 104 |
} |
83 | 105 |
|
84 | 106 |
let expr_of_exit loc restart state conds tag = |
85 |
mkexpr loc (Expr_when (List.fold_right add_branch conds (init loc restart state), state, tag))
|
|
107 |
mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag))
|
|
86 | 108 |
|
87 | 109 |
let expr_of_handler loc restart state node tag = |
88 |
let arg = mkexpr loc (Expr_tuple (List.map (fun v -> mkident loc v.var_id) node.node_inputs)) in |
|
89 |
mkexpr loc (Expr_when (mkexpr loc (Expr_appl (node.node_id, arg, Some (restart, tag_true))), state, tag)) |
|
110 |
let args = List.map (fun v -> mkexpr loc (Expr_when (mkident loc v.var_id, state, tag))) node.node_inputs in |
|
111 |
let arg = mkexpr loc (Expr_tuple args) in |
|
112 |
let reset = Some (mkident loc restart) in |
|
113 |
mkexpr loc (Expr_appl (node.node_id, arg, reset)) |
|
90 | 114 |
|
91 | 115 |
let assign_aut_handlers loc actual_r actual_s hnodes = |
92 |
let outputs = (snd (List.hd hnodes)).node_outputs in
|
|
93 |
let assign_handlers = List.map (fun (hs, n) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in
|
|
116 |
let outputs = fst (snd (List.hd hnodes)) in
|
|
117 |
let assign_handlers = List.map (fun (hs, (_, n)) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in
|
|
94 | 118 |
let assign_expr = mkexpr loc (Expr_merge (actual_s, assign_handlers)) in |
95 | 119 |
let assign_eq = mkeq loc (List.map (fun v -> v.var_id) outputs, assign_expr) in |
96 | 120 |
assign_eq |
... | ... | |
100 | 124 |
{ tydef_id = tname; |
101 | 125 |
tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers) |
102 | 126 |
} |
127 |
(* |
|
128 |
let expand_automata nused used owner typedef node aut = |
|
129 |
let initial = (List.hd aut.aut_handlers).hand_state in |
|
130 |
let incoming_r = mk_new_name used (aut.aut_id ^ "__restart_in") in |
|
131 |
let incoming_s = mk_new_name used (aut.aut_id ^ "__state_in") in |
|
132 |
let actual_r = mk_new_name used (aut.aut_id ^ "__restart_act") in |
|
133 |
let actual_s = mk_new_name used (aut.aut_id ^ "__state_act") in |
|
134 |
let next_incoming_r = mk_new_name used (aut.aut_id ^ "__next_restart_in") in |
|
135 |
let next_incoming_s = mk_new_name used (aut.aut_id ^ "__next_state_in") in |
|
136 |
(* merge on incoming_s gives actual_s by the unless equations *) |
|
137 |
let actual_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc incoming_r incoming_s h.hand_unless h.hand_state)) aut.aut_handlers in |
|
138 |
let actual_expr = mkexpr aut.aut_loc (Expr_merge (incoming_s, unless_handlers)) in |
|
139 |
let actual_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in |
|
140 |
(* next_incoming_s and initial conditions gives incoming_s *) |
|
141 |
let incoming_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) (mkidentpair aut.aut_loc next_incoming_r next_incoming_s) in |
|
142 |
let incoming_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], incoming_expr) in |
|
143 |
(* merge on actual_s gives handler assigned variables and next_incoming_s by the until equations *) |
|
144 |
let until_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc actual_r actual_s h.hand_until h.hand_state)) aut.aut_handlers in |
|
145 |
let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in |
|
146 |
let fby_until_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) until_expr in |
|
147 |
let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in |
|
148 |
let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused used node aut.aut_id h)) aut.aut_handlers in |
|
149 |
let outputs = fst (snd (List.hd hnodes)) in |
|
150 |
let next_incoming_and_assigned_vars = next_incoming_r :: next_incoming_s :: List.map (fun v -> v.var_id) outputs in |
|
151 |
let next_incoming_and_assigned_handlers = |
|
152 |
List.map (fun h -> ) aut.aut_handlers in |
|
153 |
let next_incoming_and_assigned_expr = mkexpr loc (Expr_merge (actual_s, next_incoming_and_assigned_handlers) in |
|
154 |
let next_incoming_and_assigned_eq = mkeq aut.aut_loc (next_incoming_and_assigned_vars, next_incoming_and_assigned_expr) in |
|
155 |
(* declaration of new local variables, equations and handler nodes *) |
|
156 |
let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in |
|
157 |
let tydec_state id = { ty_dec_desc = Tydec_clock (Tydec_const id); ty_dec_loc = aut.aut_loc } in |
|
158 |
let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in |
|
159 |
let locals' = [mkvar_decl aut.aut_loc (incoming_r, tydec_bool, ckdec_any, false); |
|
160 |
mkvar_decl aut.aut_loc (actual_r , tydec_bool, ckdec_any, false); |
|
161 |
mkvar_decl aut.aut_loc (next_incoming_r , tydec_bool, ckdec_any, false); |
|
162 |
mkvar_decl aut.aut_loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false); |
|
163 |
mkvar_decl aut.aut_loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false); |
|
164 |
mkvar_decl aut.aut_loc (next_incoming_s, tydec_state typedef.tydef_id, ckdec_any, false)] in |
|
165 |
let eqs' = [Eq actual_eq; Eq next_incoming_and_assigned_eq; Eq incoming_eq] in |
|
166 |
(List.map2 (fun h (hs, (_, n)) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes, |
|
167 |
locals', |
|
168 |
eqs') |
|
169 |
*) |
|
103 | 170 |
|
104 | 171 |
let expand_automata nused used owner typedef node aut = |
105 | 172 |
let initial = (List.hd aut.aut_handlers).hand_state in |
... | ... | |
112 | 179 |
let unless_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in |
113 | 180 |
let until_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc actual_r actual_s h.hand_until h.hand_state)) aut.aut_handlers in |
114 | 181 |
let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in |
115 |
let fby_until_expr = mkfby aut.aut_loc (init aut.aut_loc tag_false initial) until_expr in
|
|
182 |
let fby_until_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) until_expr in
|
|
116 | 183 |
let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in |
117 |
let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused node aut.aut_id h)) aut.aut_handlers in |
|
184 |
let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused used node aut.aut_id h)) aut.aut_handlers in
|
|
118 | 185 |
let assign_eq = assign_aut_handlers aut.aut_loc actual_r actual_s hnodes in |
119 | 186 |
let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in |
120 |
let tydec_const id = { ty_dec_desc = Tydec_const id; ty_dec_loc = aut.aut_loc } in
|
|
187 |
let tydec_state id = { ty_dec_desc = Tydec_clock (Tydec_const id); ty_dec_loc = aut.aut_loc } in
|
|
121 | 188 |
let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in |
122 | 189 |
let locals' = [mkvar_decl aut.aut_loc (incoming_r, tydec_bool, ckdec_any, false); |
123 | 190 |
mkvar_decl aut.aut_loc (actual_r , tydec_bool, ckdec_any, false); |
124 |
mkvar_decl aut.aut_loc (incoming_s, tydec_const typedef.tydef_id, ckdec_any, false);
|
|
125 |
mkvar_decl aut.aut_loc (actual_s , tydec_const typedef.tydef_id, ckdec_any, false)] in
|
|
191 |
mkvar_decl aut.aut_loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false);
|
|
192 |
mkvar_decl aut.aut_loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false)] in
|
|
126 | 193 |
let eqs' = [Eq unless_eq; Eq assign_eq; Eq until_eq] in |
127 |
(List.map2 (fun h (hs, n) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,
|
|
194 |
(List.map2 (fun h (hs, (_, n)) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,
|
|
128 | 195 |
locals', |
129 | 196 |
eqs') |
130 | 197 |
|
src/backends/C/c_backend_common.ml | ||
---|---|---|
47 | 47 |
|
48 | 48 |
let mk_call_var_decl loc id = |
49 | 49 |
{ var_id = id; |
50 |
var_orig = false; |
|
50 | 51 |
var_dec_type = mktyp Location.dummy_loc Tydec_any; |
51 | 52 |
var_dec_clock = mkclock Location.dummy_loc Ckdec_any; |
52 | 53 |
var_dec_const = false; |
src/causality.ml | ||
---|---|---|
109 | 109 |
assert (is_read_var id); |
110 | 110 |
String.sub id 1 (String.length id - 1) |
111 | 111 |
|
112 |
let undo_instance_var id = |
|
113 |
assert (is_instance_var id); |
|
114 |
String.sub id 1 (String.length id - 1) |
|
115 |
|
|
112 | 116 |
let eq_memory_variables mems eq = |
113 | 117 |
let rec match_mem lhs rhs mems = |
114 | 118 |
match rhs.expr_desc with |
... | ... | |
241 | 245 |
(* mashed up dependency for user-defined operators *) |
242 | 246 |
else |
243 | 247 |
mashup_appl_dependencies f e g |
244 |
| Expr_appl (f, e, Some (r, _)) ->
|
|
245 |
mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g)
|
|
248 |
| Expr_appl (f, e, Some c) ->
|
|
249 |
mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
|
|
246 | 250 |
in |
247 | 251 |
let g = |
248 | 252 |
List.fold_left |
... | ... | |
362 | 366 |
expr_delay = Delay.new_var (); |
363 | 367 |
expr_annot = None; |
364 | 368 |
expr_loc = var_decl.var_loc } in |
365 |
{ var_decl with var_id = cp_var }, |
|
369 |
{ var_decl with var_id = cp_var; var_orig = false },
|
|
366 | 370 |
mkeq var_decl.var_loc ([cp_var], expr) |
367 | 371 |
|
368 | 372 |
let wrong_partition g partition = |
... | ... | |
526 | 530 |
|
527 | 531 |
let pp_error fmt trace = |
528 | 532 |
fprintf fmt "@.Causality error, cyclic data dependencies: %a@." |
529 |
(fprintf_list ~sep:"->" pp_print_string) trace
|
|
533 |
(fprintf_list ~sep:", " pp_print_string) trace
|
|
530 | 534 |
|
531 | 535 |
(* Merges elements of graph [g2] into graph [g1] *) |
532 | 536 |
let merge_with g1 g2 = |
src/clock_calculus.ml | ||
---|---|---|
441 | 441 |
(Const_int i) -> i |
442 | 442 |
| _ -> failwith "Internal error: int_factor_of_expr" |
443 | 443 |
|
444 |
(** [clock_uncarry ck] drops the possible carrier name from clock [ck] *)
|
|
445 |
let clock_uncarry ck = |
|
444 |
(** [clock_uncarry ck] drops the possible carrier(s) name(s) from clock [ck] *)
|
|
445 |
let rec clock_uncarry ck =
|
|
446 | 446 |
let ck = repr ck in |
447 | 447 |
match ck.cdesc with |
448 | 448 |
| Ccarrying (_, ck') -> ck' |
449 |
| Con(ck', cr, l) -> clock_on (clock_uncarry ck') cr l |
|
450 |
| Ctuple ckl -> clock_of_clock_list (List.map clock_uncarry ckl) |
|
449 | 451 |
| _ -> ck |
450 | 452 |
|
451 | 453 |
let try_unify ck1 ck2 loc = |
... | ... | |
557 | 559 |
in |
558 | 560 |
aux ck |
559 | 561 |
|
562 |
(* Computes the root clock of a tuple or a node clock, |
|
563 |
which is not the same as the base clock. |
|
564 |
Root clock will be used as the call clock |
|
565 |
of a given node instance *) |
|
566 |
let compute_root_clock ck = |
|
567 |
let root = Clocks.root ck in |
|
568 |
let branch = ref None in |
|
569 |
let rec aux ck = |
|
570 |
match (repr ck).cdesc with |
|
571 |
| Ctuple cl -> |
|
572 |
List.iter aux cl |
|
573 |
| Carrow (ck1,ck2) -> |
|
574 |
aux ck1; aux ck2 |
|
575 |
| _ -> |
|
576 |
begin |
|
577 |
match !branch with |
|
578 |
| None -> |
|
579 |
branch := Some (Clocks.branch ck) |
|
580 |
| Some br -> |
|
581 |
(* cannot fail *) |
|
582 |
branch := Some (Clocks.common_prefix br (Clocks.branch ck)) |
|
583 |
end |
|
584 |
in |
|
585 |
begin |
|
586 |
aux ck; |
|
587 |
Clocks.clock_of_root_branch root (Utils.desome !branch) |
|
588 |
end |
|
589 |
|
|
560 | 590 |
(* Clocks a list of arguments of Lustre builtin operators: |
561 | 591 |
- type each expression, remove carriers of clocks as |
562 | 592 |
carriers may only denote variables, not arbitrary expr. |
... | ... | |
658 | 688 |
let cr = |
659 | 689 |
match r with |
660 | 690 |
| None -> new_var true |
661 |
| Some (x, _) -> let loc_r = loc_of_cond expr.expr_loc x in |
|
662 |
let expr_r = expr_of_ident x loc_r in |
|
663 |
clock_expr env expr_r in |
|
691 |
| Some c -> clock_standard_args env [c] in |
|
664 | 692 |
let couts = clock_appl env id args cr expr.expr_loc in |
665 | 693 |
expr.expr_clock <- couts; |
666 | 694 |
couts |
... | ... | |
690 | 718 |
| Expr_merge (c,hl) -> |
691 | 719 |
let cvar = new_var true in |
692 | 720 |
let crvar = new_carrier Carry_name true in |
693 |
List.iter (fun (t, h) -> let ckh = clock_expr env h in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;
|
|
721 |
List.iter (fun (t, h) -> let ckh = clock_uncarry (clock_expr env h) in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;
|
|
694 | 722 |
let cr = clock_carrier env c expr.expr_loc cvar in |
695 | 723 |
try_unify_carrier cr crvar expr.expr_loc; |
696 |
expr.expr_clock <- cvar; |
|
697 |
cvar |
|
724 |
let cres = clock_current ((snd (List.hd hl)).expr_clock) in |
|
725 |
expr.expr_clock <- cres; |
|
726 |
cres |
|
698 | 727 |
in |
699 | 728 |
Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck); |
700 | 729 |
resulting_ck |
src/clocks.ml | ||
---|---|---|
164 | 164 |
let clock_on ck cr l = |
165 | 165 |
clock_of_clock_list (List.map (fun ck -> new_ck (Con (ck,cr,l)) true) (clock_list_of_clock ck)) |
166 | 166 |
|
167 |
let clock_current ck = |
|
168 |
clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with Con(ck',_,_) -> ck' | _ -> assert false) (clock_list_of_clock ck)) |
|
169 |
|
|
167 | 170 |
let clock_of_impnode_clock ck = |
168 | 171 |
let ck = repr ck in |
169 | 172 |
match ck.cdesc with |
... | ... | |
378 | 381 |
| _ -> acc |
379 | 382 |
in branch ck [];; |
380 | 383 |
|
384 |
let clock_of_root_branch r br = |
|
385 |
List.fold_left (fun ck (cr,l) -> new_ck (Con (ck, cr, l)) true) r br |
|
386 |
|
|
387 |
(* Computes the (longest) common prefix of two branches *) |
|
388 |
let rec common_prefix br1 br2 = |
|
389 |
match br1, br2 with |
|
390 |
| [] , _ |
|
391 |
| _ , [] -> [] |
|
392 |
| (cr1,l1)::q1, (cr2,l2)::q2 -> |
|
393 |
if eq_carrier cr1 cr2 && (l1 = l2) |
|
394 |
then (cr1, l1) :: common_prefix q1 q2 |
|
395 |
else [] |
|
396 |
|
|
381 | 397 |
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *) |
382 | 398 |
let rec disjoint_branches br1 br2 = |
383 | 399 |
match br1, br2 with |
src/compiler_common.ml | ||
---|---|---|
39 | 39 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. parsing header file %s@ " filename); |
40 | 40 |
try |
41 | 41 |
let header = Parse.header Parser_lustre.header Lexer_lustre.token lexbuf in |
42 |
ignore (Modules.load_header ISet.empty header);
|
|
42 |
(*ignore (Modules.load_header ISet.empty header);*)
|
|
43 | 43 |
close_in h_in; |
44 | 44 |
header |
45 | 45 |
with |
... | ... | |
65 | 65 |
(fun fmt -> fprintf fmt ".. parsing source file %s@," source_name); |
66 | 66 |
try |
67 | 67 |
let prog = Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf in |
68 |
ignore (Modules.load_program ISet.empty prog);
|
|
68 |
(*ignore (Modules.load_program ISet.empty prog);*)
|
|
69 | 69 |
close_in s_in; |
70 | 70 |
prog |
71 | 71 |
with |
src/corelang.ml | ||
---|---|---|
41 | 41 |
let mkclock loc d = |
42 | 42 |
{ ck_dec_desc = d; ck_dec_loc = loc } |
43 | 43 |
|
44 |
let mkvar_decl loc (id, ty_dec, ck_dec, is_const) = |
|
44 |
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const) =
|
|
45 | 45 |
{ var_id = id; |
46 |
var_orig = orig; |
|
46 | 47 |
var_dec_type = ty_dec; |
47 | 48 |
var_dec_clock = ck_dec; |
48 | 49 |
var_dec_const = is_const; |
... | ... | |
61 | 62 |
|
62 | 63 |
let var_decl_of_const c = |
63 | 64 |
{ var_id = c.const_id; |
65 |
var_orig = true; |
|
64 | 66 |
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any }; |
65 | 67 |
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any }; |
66 | 68 |
var_dec_const = true; |
... | ... | |
572 | 574 |
| Expr_pre e' -> Expr_pre (expr_replace_var fvar e') |
573 | 575 |
| Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l) |
574 | 576 |
| Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl) |
575 |
| Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) -> fvar x, l) i')
|
|
577 |
| Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i')
|
|
576 | 578 |
|
577 | 579 |
(* Applies the renaming function [fvar] to every rhs |
578 | 580 |
only when the corresponding lhs satisfies predicate [pvar] *) |
... | ... | |
631 | 633 |
| Expr_merge (i, hl) -> |
632 | 634 |
Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl) |
633 | 635 |
| Expr_appl (i, e', i') -> |
634 |
Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i')
|
|
636 |
Expr_appl (f_node i, re e', Utils.option_map re i')
|
|
635 | 637 |
|
636 | 638 |
let rename_node_annot f_node f_var f_const expr = |
637 | 639 |
expr |
... | ... | |
929 | 931 |
| Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2] |
930 | 932 |
| Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl |
931 | 933 |
| Expr_appl (_, arg, None) -> get_expr_vars vars arg |
932 |
| Expr_appl (_, arg, Some (r,_)) -> get_expr_vars (Utils.ISet.add r vars) arg
|
|
934 |
| Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]
|
|
933 | 935 |
|
934 | 936 |
|
935 | 937 |
let rec expr_has_arrows e = |
src/corelang.mli | ||
---|---|---|
19 | 19 |
|
20 | 20 |
val mktyp: Location.t -> type_dec_desc -> type_dec |
21 | 21 |
val mkclock: Location.t -> clock_dec_desc -> clock_dec |
22 |
val mkvar_decl: Location.t -> ident * type_dec * clock_dec * bool (* is const *) -> var_decl |
|
22 |
val mkvar_decl: Location.t -> ?orig:bool -> ident * type_dec * clock_dec * bool (* is const *) -> var_decl
|
|
23 | 23 |
val var_decl_of_const: const_desc -> var_decl |
24 | 24 |
val mkexpr: Location.t -> expr_desc -> expr |
25 | 25 |
val mkeq: Location.t -> ident list * expr -> eq |
... | ... | |
83 | 83 |
val expr_of_ident : ident -> Location.t -> expr |
84 | 84 |
val expr_list_of_expr : expr -> expr list |
85 | 85 |
val expr_of_expr_list : Location.t -> expr list -> expr |
86 |
val call_of_expr: expr -> (ident * expr list * (ident * label) option)
|
|
86 |
val call_of_expr: expr -> (ident * expr list * expr option)
|
|
87 | 87 |
val expr_of_dimension: Dimension.dim_expr -> expr |
88 | 88 |
val dimension_of_expr: expr -> Dimension.dim_expr |
89 | 89 |
val dimension_of_const: Location.t -> constant -> Dimension.dim_expr |
src/expand.ml | ||
---|---|---|
73 | 73 |
let ty_dec = {ty_dec_desc = Tydec_any; ty_dec_loc = vloc} in (* dummy *) |
74 | 74 |
let ck_dec = {ck_dec_desc = Ckdec_any; ck_dec_loc = vloc} in (* dummy *) |
75 | 75 |
{var_id = vid; |
76 |
var_orig = false; |
|
76 | 77 |
var_dec_type = ty_dec; |
77 | 78 |
var_dec_clock = ck_dec; |
78 | 79 |
var_dec_deadline = vdd; |
src/lustreSpec.ml | ||
---|---|---|
50 | 50 |
|
51 | 51 |
type var_decl = |
52 | 52 |
{var_id: ident; |
53 |
var_orig:bool; |
|
53 | 54 |
var_dec_type: type_dec; |
54 | 55 |
var_dec_clock: clock_dec; |
55 | 56 |
var_dec_const: bool; |
... | ... | |
102 | 103 |
| Expr_merge of ident * (label * expr) list |
103 | 104 |
| Expr_appl of call_t |
104 | 105 |
|
105 |
and call_t = ident * expr * (ident * label) option
|
|
106 |
(* The third part denotes the reseting clock label and value *)
|
|
106 |
and call_t = ident * expr * expr option
|
|
107 |
(* The third part denotes the boolean condition for resetting *)
|
|
107 | 108 |
|
108 | 109 |
and eq = |
109 | 110 |
{eq_lhs: ident list; |
src/machine_code.ml | ||
---|---|---|
133 | 133 |
let dummy_var_decl name typ = |
134 | 134 |
{ |
135 | 135 |
var_id = name; |
136 |
var_orig = false; |
|
136 | 137 |
var_dec_type = dummy_type_dec; |
137 | 138 |
var_dec_clock = dummy_clock_dec; |
138 | 139 |
var_dec_const = false; |
... | ... | |
327 | 328 |
let reset_instance node args i r c = |
328 | 329 |
match r with |
329 | 330 |
| None -> [] |
330 |
| Some (x, l) -> [control_on_clock node args c (MBranch (translate_ident node args x, [l, [MReset i]]))] |
|
331 |
| Some r -> let g = translate_guard node args r in |
|
332 |
[control_on_clock node args c (conditional g [MReset i] [])] |
|
331 | 333 |
|
332 | 334 |
let translate_eq node ((m, si, j, d, s) as args) eq = |
333 | 335 |
(*Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;*) |
... | ... | |
366 | 368 |
node_f, |
367 | 369 |
NodeDep.filter_static_inputs (node_inputs node_f) el in |
368 | 370 |
let o = new_instance node node_f eq.eq_rhs.expr_tag in |
369 |
let call_ck = Clocks.new_var true in |
|
371 |
let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in |
|
372 |
let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in |
|
373 |
(*Clocks.new_var true in |
|
370 | 374 |
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; |
375 |
Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*) |
|
371 | 376 |
(m, |
372 | 377 |
(if Stateless.check_node node_f then si else MReset o :: si), |
373 | 378 |
Utils.IMap.add o call_f j, |
src/main_lustre_compiler.ml | ||
---|---|---|
12 | 12 |
open Format |
13 | 13 |
open Log |
14 | 14 |
|
15 |
open Utils |
|
15 | 16 |
open LustreSpec |
16 | 17 |
open Compiler_common |
17 | 18 |
|
... | ... | |
38 | 39 |
begin |
39 | 40 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>"); |
40 | 41 |
let header = parse_header true header_name in |
42 |
ignore (Modules.load_header ISet.empty header); |
|
41 | 43 |
ignore (check_top_decls header); |
42 | 44 |
create_dest_dir (); |
43 | 45 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," header_name); |
... | ... | |
85 | 87 |
|
86 | 88 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>"); |
87 | 89 |
|
90 |
(* Parsing source *) |
|
88 | 91 |
let prog = parse_source source_name in |
89 | 92 |
|
93 |
(* Removing automata *) |
|
94 |
let prog = Automata.expand_decls prog in |
|
95 |
|
|
96 |
(* Importing source *) |
|
97 |
let _ = Modules.load_program ISet.empty prog in |
|
98 |
|
|
90 | 99 |
(* Extracting dependencies *) |
91 | 100 |
let dependencies, type_env, clock_env = import_dependencies prog in |
92 | 101 |
|
93 |
(* Removing automata *) |
|
94 |
(*let prog = Automata.expand_decls prog in*) |
|
95 |
|
|
96 |
(*Printers.pp_prog Format.std_formatter prog;*) |
|
97 | 102 |
(* Sorting nodes *) |
98 | 103 |
let prog = SortProg.sort prog in |
99 | 104 |
|
src/modules.ml | ||
---|---|---|
82 | 82 |
in import ((typedef_of_top tydef).tydef_desc) |
83 | 83 |
|
84 | 84 |
let add_type itf name value = |
85 |
(*Format.eprintf "add_type %B %s %a (owner=%s)@." itf name Printers.pp_typedef (typedef_of_top value) value.top_decl_owner;*) |
|
85 |
(*Format.eprintf "Modules.add_type %B %s %a (owner=%s)@." itf name Printers.pp_typedef (typedef_of_top value) value.top_decl_owner;*)
|
|
86 | 86 |
try |
87 | 87 |
let value' = Hashtbl.find type_table (Tydec_const name) in |
88 | 88 |
let owner' = value'.top_decl_owner in |
src/normalization.ml | ||
---|---|---|
65 | 65 |
if List.exists (fun v -> v.var_id = s) vars then aux () else |
66 | 66 |
{ |
67 | 67 |
var_id = s; |
68 |
var_orig = false; |
|
68 | 69 |
var_dec_type = dummy_type_dec; |
69 | 70 |
var_dec_clock = dummy_clock_dec; |
70 | 71 |
var_dec_const = false; |
... | ... | |
371 | 372 |
- compute the associated expression without aliases |
372 | 373 |
*) |
373 | 374 |
let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in |
375 |
let split_defs = Splitting.tuple_split_eq_list defs in |
|
374 | 376 |
let norm_traceability = { |
375 |
annots = |
|
376 |
List.map |
|
377 |
(fun v -> |
|
378 |
let expr = substitute_expr diff_vars defs ( |
|
379 |
let eq = try |
|
380 |
List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs |
|
381 |
with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in |
|
382 |
eq.eq_rhs) in |
|
383 |
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in |
|
384 |
["horn_backend";"trace"], pair |
|
385 |
) |
|
386 |
diff_vars ; |
|
377 |
annots = List.map (fun v -> |
|
378 |
let eq = |
|
379 |
try |
|
380 |
List.find (fun eq -> eq.eq_lhs = [v.var_id]) split_defs |
|
381 |
with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in |
|
382 |
let expr = substitute_expr diff_vars split_defs eq.eq_rhs in |
|
383 |
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in |
|
384 |
(["horn_backend";"trace"], pair) |
|
385 |
) diff_vars; |
|
387 | 386 |
annot_loc = Location.dummy_loc |
388 | 387 |
} |
389 | 388 |
|
src/optimize_machine.ml | ||
---|---|---|
40 | 40 |
| Cst _ | StateVar _ -> expr |
41 | 41 |
|
42 | 42 |
(* see if elim has to take in account the provided instr: |
43 |
if so, upodate elim and return the remove flag,
|
|
43 |
if so, update elim and return the remove flag, |
|
44 | 44 |
otherwise, the expression should be kept and elim is left untouched *) |
45 | 45 |
let update_elim outputs elim instr = |
46 | 46 |
(* Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*) |
src/parser_lustre.mly | ||
---|---|---|
20 | 20 |
|
21 | 21 |
let mktyp x = mktyp (get_loc ()) x |
22 | 22 |
let mkclock x = mkclock (get_loc ()) x |
23 |
let mkvar_decl x = mkvar_decl (get_loc ()) x |
|
23 |
let mkvar_decl x = mkvar_decl (get_loc ()) ~orig:true x
|
|
24 | 24 |
let mkexpr x = mkexpr (get_loc ()) x |
25 | 25 |
let mkeexpr x = mkeexpr (get_loc ()) x |
26 | 26 |
let mkeq x = mkeq (get_loc ()) x |
... | ... | |
266 | 266 |
| handler handler_list { $1::$2 } |
267 | 267 |
|
268 | 268 |
handler: |
269 |
STATE UIDENT ARROW unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
|
|
269 |
STATE UIDENT COL 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 |
{ [] } |
... | ... | |
381 | 381 |
/* Applications */ |
382 | 382 |
| node_ident LPAR expr RPAR |
383 | 383 |
{mkexpr (Expr_appl ($1, $3, None))} |
384 |
| node_ident LPAR expr RPAR EVERY vdecl_ident |
|
385 |
{mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))} |
|
386 |
| node_ident LPAR expr RPAR EVERY tag_ident LPAR vdecl_ident RPAR |
|
387 |
{mkexpr (Expr_appl ($1, $3, Some ($8, $6))) } |
|
384 |
| node_ident LPAR expr RPAR EVERY expr |
|
385 |
{mkexpr (Expr_appl ($1, $3, Some $6))} |
|
388 | 386 |
| node_ident LPAR tuple_expr RPAR |
389 | 387 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))} |
390 |
| node_ident LPAR tuple_expr RPAR EVERY vdecl_ident |
|
391 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) } |
|
392 |
| node_ident LPAR tuple_expr RPAR EVERY tag_ident LPAR vdecl_ident RPAR |
|
393 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) } |
|
388 |
| node_ident LPAR tuple_expr RPAR EVERY expr |
|
389 |
{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some $6)) } |
|
394 | 390 |
|
395 | 391 |
/* Boolean expr */ |
396 | 392 |
| expr AND expr |
... | ... | |
527 | 523 |
|
528 | 524 |
vdecl: |
529 | 525 |
/* Useless no ?*/ ident_list |
530 |
{List.map mkvar_decl |
|
531 |
(List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)} |
|
526 |
{ List.map (fun id -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1 } |
|
532 | 527 |
|
533 | 528 |
| ident_list COL typeconst clock |
534 |
{List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)}
|
|
529 |
{ List.map (fun id -> mkvar_decl (id, mktyp $3, $4, false)) $1 }
|
|
535 | 530 |
| CONST ident_list COL typeconst /* static parameters don't have clocks */ |
536 |
{List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)}
|
|
531 |
{ List.map (fun id -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true)) $2 }
|
|
537 | 532 |
|
538 | 533 |
cdecl_list: |
539 | 534 |
cdecl SCOL { (fun itf -> [$1 itf]) } |
src/printers.ml | ||
---|---|---|
86 | 86 |
and pp_app fmt id e r = |
87 | 87 |
match r with |
88 | 88 |
| None -> pp_call fmt id e |
89 |
| Some (x, l) -> fprintf fmt "%t every %s(%s)" (fun fmt -> pp_call fmt id e) l x
|
|
89 |
| Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c
|
|
90 | 90 |
|
91 | 91 |
and pp_call fmt id e = |
92 | 92 |
match id, e.expr_desc with |
... | ... | |
135 | 135 |
Format.fprintf fmt "%s" (if restart then "restart" else "resume") |
136 | 136 |
|
137 | 137 |
let pp_unless fmt (_, expr, restart, st) = |
138 |
Format.fprintf fmt "unless %a %a %s" |
|
138 |
Format.fprintf fmt "unless %a %a %s@ "
|
|
139 | 139 |
pp_expr expr |
140 | 140 |
pp_restart restart |
141 | 141 |
st |
142 | 142 |
|
143 | 143 |
let pp_until fmt (_, expr, restart, st) = |
144 |
Format.fprintf fmt "until %a %a %s" |
|
144 |
Format.fprintf fmt "until %a %a %s@ "
|
|
145 | 145 |
pp_expr expr |
146 | 146 |
pp_restart restart |
147 | 147 |
st |
148 | 148 |
|
149 | 149 |
let rec pp_handler fmt handler = |
150 |
Format.fprintf fmt "state %s -> %a %a let %a tel %a"
|
|
150 |
Format.fprintf fmt "state %s ->@ @[<v 2> %a%alet@,@[<v 2> %a@]@,tel%a@]"
|
|
151 | 151 |
handler.hand_state |
152 |
(Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
|
|
152 |
(Utils.fprintf_list ~sep:"@," pp_unless) handler.hand_unless
|
|
153 | 153 |
(fun fmt locals -> |
154 | 154 |
match locals with [] -> () | _ -> |
155 | 155 |
Format.fprintf fmt "@[<v 4>var %a@]@ " |
... | ... | |
158 | 158 |
locals) |
159 | 159 |
handler.hand_locals |
160 | 160 |
pp_node_stmts handler.hand_stmts |
161 |
(Utils.fprintf_list ~sep:"@ " pp_until) handler.hand_until
|
|
161 |
(Utils.fprintf_list ~sep:"@," pp_until) handler.hand_until
|
|
162 | 162 |
|
163 | 163 |
and pp_node_stmt fmt stmt = |
164 | 164 |
match stmt with |
... | ... | |
168 | 168 |
and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts |
169 | 169 |
|
170 | 170 |
and pp_node_aut fmt aut = |
171 |
Format.fprintf fmt "automaton %s %a"
|
|
171 |
Format.fprintf fmt "@[<v 0>automaton %s@,%a@]"
|
|
172 | 172 |
aut.aut_id |
173 | 173 |
(Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers |
174 | 174 |
|
src/scheduling.ml | ||
---|---|---|
116 | 116 |
!sorted |
117 | 117 |
end |
118 | 118 |
|
119 |
(* Filters out normalization variables and renames instance variables to keep things readable, |
|
120 |
in a case of a dependency error *) |
|
121 |
let filter_original n vl = |
|
122 |
List.fold_right (fun v res -> |
|
123 |
if ExprDep.is_instance_var v then Format.sprintf "node %s" (ExprDep.undo_instance_var v) :: res else |
|
124 |
let vdecl = get_node_var v n in |
|
125 |
if vdecl.var_orig then v :: res else res) vl [] |
|
126 |
|
|
119 | 127 |
let schedule_node n = |
128 |
let node_vars = get_node_vars n in |
|
120 | 129 |
try |
121 | 130 |
let eq_equiv = ExprDep.node_eq_equiv n in |
122 | 131 |
let eq_equiv v1 v2 = |
... | ... | |
143 | 152 |
let sort = topological_sort eq_equiv g in |
144 | 153 |
let unused = Liveness.compute_unused_variables n gg in |
145 | 154 |
let fanin = Liveness.compute_fanin n gg in |
146 |
|
|
147 |
let disjoint = Disjunction.clock_disjoint_map (get_node_vars n) in
|
|
155 |
|
|
156 |
let disjoint = Disjunction.clock_disjoint_map node_vars in
|
|
148 | 157 |
|
149 | 158 |
Log.report ~level:2 |
150 | 159 |
(fun fmt -> |
... | ... | |
164 | 173 |
); |
165 | 174 |
|
166 | 175 |
n', { schedule = sort; unused_vars = unused; fanin_table = fanin; reuse_table = reuse } |
167 |
with (Causality.Cycle v) as exc -> |
|
168 |
pp_error Format.err_formatter v; |
|
176 |
with (Causality.Cycle vl) as exc -> |
|
177 |
let vl = filter_original n vl in |
|
178 |
pp_error Format.err_formatter vl; |
|
169 | 179 |
raise exc |
170 | 180 |
|
171 | 181 |
let schedule_prog prog = |
src/typing.ml | ||
---|---|---|
444 | 444 |
expression *) |
445 | 445 |
(match r with |
446 | 446 |
| None -> () |
447 |
| Some (x, l) -> |
|
448 |
check_constant expr.expr_loc const false; |
|
449 |
let expr_x = expr_of_ident x expr.expr_loc in |
|
450 |
let typ_l = |
|
451 |
Type_predef.type_clock |
|
452 |
(type_const expr.expr_loc (Const_tag l)) in |
|
453 |
type_subtyping_arg env in_main ~sub:false const expr_x typ_l); |
|
447 |
| Some c -> |
|
448 |
check_constant expr.expr_loc const false; |
|
449 |
type_subtyping_arg env in_main const c Type_predef.type_bool); |
|
454 | 450 |
let touts = type_appl env in_main expr.expr_loc const id (expr_list_of_expr args) in |
455 | 451 |
expr.expr_type <- touts; |
456 | 452 |
touts |
test/tests_ok.list | ||
---|---|---|
908 | 908 |
./tests/lusic/test1.lusi |
909 | 909 |
./tests/lusic/test1.lus,as_soon_as |
910 | 910 |
./tests/lusic/test2.lus |
911 |
./tests/automata/aut1.lus |
|
911 | 912 |
./tests/linear_ctl/ex8sat.lus,top |
912 | 913 |
./tests/linear_ctl/ex2reset.lus,top |
913 | 914 |
./tests/linear_ctl/lp_iir_9600_2.lus,top |
Also available in: Unified diff