Revision 1eda3e78
Added by Xavier Thirioux almost 8 years ago
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 
Also available in: Unified diff
 work in progress for automata...