Revision 333e3a25
Added by PierreLoïc Garoche over 5 years ago
src/causality.ml  

88  88 
let new_graph () = 
89  89 
IdentDepGraph.create () 
90  90  
91 


91  92 
module ExprDep = struct 
92  
93 
let get_node_eqs nd = 

94 
let eqs, auts = get_node_eqs nd in 

95 
if auts != [] then assert false (* No call on causality on a Lustre model 

96 
with automaton. They should be expanded by now. *); 

97 
eqs 

98 


93  99 
let instance_var_cpt = ref 0 
94  100  
95  101 
(* read vars represent input/mem readonly vars, 
...  ...  
317  323 
 Expr_appl (id, args, _) > Some (id, expr_list_of_expr args) 
318  324 
 _ > None 
319  325  
320 
let get_calls prednode eqs = 

321 
let deps = 

322 
List.fold_left 

323 
(fun accu eq > ESet.union accu (get_expr_calls prednode eq.eq_rhs)) 

324 
ESet.empty 

325 
eqs in 

326 
let get_calls prednode nd = 

327 
let accu f init objl = List.fold_left (fun accu o > ESet.union accu (f o)) init objl in 

328 
let get_eq_calls eq = get_expr_calls prednode eq.eq_rhs in 

329 
let rec get_stmt_calls s = 

330 
match s with Eq eq > get_eq_calls eq  Aut aut > get_aut_calls aut 

331 
and get_aut_calls aut = 

332 
let get_handler_calls h = 

333 
let get_cond_calls c = accu (fun (_,e,_,_) > get_expr_calls prednode e) ESet.empty c in 

334 
let until = get_cond_calls h.hand_until in 

335 
let unless = get_cond_calls h.hand_unless in 

336 
let calls = ESet.union until unless in 

337 
let calls = accu get_stmt_calls calls h.hand_stmts in 

338 
let calls = accu (fun a > get_expr_calls prednode a.assert_expr) calls h.hand_asserts in 

339 
(* let calls = accu xx calls h.hand_annots in *) (* TODO: search for calls in eexpr *) 

340 
calls 

341 
in 

342 
accu get_handler_calls ESet.empty aut.aut_handlers 

343 
in 

344 
let eqs, auts = get_node_eqs nd in 

345 
let deps = accu get_eq_calls ESet.empty eqs in 

346 
let deps = accu get_aut_calls deps auts in 

326  347 
ESet.elements deps 
327  348  
328  349 
let dependence_graph prog = 
...  ...  
335  356 
let accu = add_vertices [nd.node_id] accu in 
336  357 
let deps = List.map 
337  358 
(fun e > fst (desome (get_callee e))) 
338 
(get_calls (fun _ > true) (get_node_eqs nd))


359 
(get_calls (fun _ > true) nd)


339  360 
in 
340  361 
(* Adding assert expressions deps *) 
341  362 
let deps_asserts = 
...  ...  
378  399 
match td.top_decl_desc with 
379  400 
 Node nd > 
380  401 
let prednode n = is_generic_node (Hashtbl.find node_table n) in 
381 
nd.node_gencalls < get_calls prednode (get_node_eqs nd)


402 
nd.node_gencalls < get_calls prednode nd


382  403 
 _ > () 
383  404 

384  405 
) prog 
...  ...  
459  480 
 a modified acyclic version of [g] 
460  481 
*) 
461  482 
let break_cycles node mems g = 
462 
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 

483 
let eqs , auts = get_node_eqs node in 

484 
assert (auts = []); (* TODO: check: For the moment we assume that auts are expanded by now *) 

485 
let (mem_eqs, non_mem_eqs) = List.partition (fun eq > List.exists (fun v > ISet.mem v mems) eq.eq_lhs) eqs in 

463  486 
let rec break vdecls mem_eqs g = 
464  487 
let scc_l = Cycles.scc_list g in 
465  488 
let wrong = List.filter (wrong_partition g) scc_l in 
Also available in: Unified diff
[general] Refactor get_node_eqs to produce (eqs, auts) with automatons