Revision 8517c831
Added by PierreLoïc Garoche over 7 years ago
src/causality.ml  

114  114 
 _ > mems in 
115  115 
match_mem eq.eq_lhs eq.eq_rhs mems 
116  116  
117  
118 
let eqs_memory_variables eqs = 

119 
List.fold_left eq_memory_variables ISet.empty eqs 

120  
121 
(* computes the equivalence relation relating variables 

122 
in the same equation lhs, under the form of a table 

123 
of class representatives *) 

124 
let eqs_equiv eqs = 

125 
let eq_equiv = Hashtbl.create 23 in 

126 
List.iter (fun eq > 

127 
let first = List.hd eq.eq_lhs in 

128 
List.iter (fun v > Hashtbl.add eq_equiv v first) eq.eq_lhs 

129 
) 

130 
eqs; 

131 
eq_equiv 

132 


133  117 
let node_memory_variables nd = 
134  118 
List.fold_left eq_memory_variables ISet.empty nd.node_eqs 
135  119  
...  ...  
226  210 
mashup_appl_dependencies f e g 
227  211 
 Expr_appl (f, e, Some (r, _)) > 
228  212 
mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g) 
213 


229  214 
in 
230  215 
add_dep false eq.eq_lhs eq.eq_rhs (add_vertices eq.eq_lhs g, g') 
231  216 

232  217  
233  218 
(* Returns the dependence graph for node [n] *) 
234 
let dependence_graph mems non_inputs eqs =


219 
let dependence_graph mems non_inputs n =


235  220 
eq_var_cpt := 0; 
236  221 
instance_var_cpt := 0; 
237  222 
let g = new_graph (), new_graph () in 
238  223 
(* Basic dependencies *) 
239 
let g = List.fold_right (add_eq_dependencies mems non_inputs) eqs g in 

224 
let g = List.fold_right (add_eq_dependencies mems non_inputs) n.node_eqs g in


240  225 
g 
241  226  
242  227 
end 
...  ...  
328  313 
let mk_copy_var n id = 
329  314 
mk_new_name (node_vars n) id 
330  315  
331 
let mk_copy_eq vars var = 

332 
let var_decl = try List.find (fun v > v.var_id = var) vars with Not_found > ( 

333 
Format.eprintf "Causality: Impossible to find variable %s in vars [%a]@.@?" 

334 
var 

335 
(Utils.fprintf_list ~sep:", " Printers.pp_var) vars; 

336 
assert false 

337 
) in 

338 
let cp_var = mk_new_name vars var in 

316 
let mk_copy_eq n var = 

317 
let var_decl = node_var var n in 

318 
let cp_var = mk_copy_var n var in 

339  319 
let expr = 
340  320 
{ expr_tag = Utils.new_tag (); 
341  321 
expr_desc = Expr_ident var; 
...  ...  
391  371 
 a list of new equations 
392  372 
 a modified acyclic version of [g] 
393  373 
*) 
394 
let break_cycles vars eqs mems g =


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

374 
let break_cycles node mems g =


375 
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


396  376 
let rec break vdecls mem_eqs g = 
397  377 
let scc_l = Cycles.scc_list g in 
398  378 
let wrong = List.filter (wrong_partition g) scc_l in 
...  ...  
405  385 
end 
406  386 
 (head::part)::_ > 
407  387 
begin 
408 
let vdecl_cp_head, cp_eq = mk_copy_eq vars head in


388 
let vdecl_cp_head, cp_eq = mk_copy_eq node head in


409  389 
let pvar v = List.mem v part in 
410  390 
let fvar v = if v = head then vdecl_cp_head.var_id else v in 
411  391 
let mem_eqs' = List.map (eq_replace_rhs_var pvar fvar) mem_eqs in 
...  ...  
464  444 
IdentDepGraph.iter_vertex (fun v > IdentDepGraph.add_vertex g1 v) g2; 
465  445 
IdentDepGraph.iter_edges (fun s t > IdentDepGraph.add_edge g1 s t) g2 
466  446  
467  
468  447 
let global_dependency node = 
469  448 
let mems = ExprDep.node_memory_variables node in 
470  449 
let non_inputs = ExprDep.node_non_input_variables node in 
471 
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems non_inputs node.node_eqs in


450 
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems non_inputs node in 

472  451 
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; 
473  452 
Format.eprintf "g_mems: %a" pp_dep_graph g_mems;*) 
474  453 
CycleDetection.check_cycles g_non_mems; 
475 
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles (node_vars node) node.node_eqs mems g_mems in


454 
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in


476  455 
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) 
477  456 
merge_with g_non_mems g_mems'; 
478  457 
{ node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals }, 
479  458 
g_non_mems 
480  459  
481  460  
482  
483 
(* Il doit y avoir un pb: non_input dans la version trunk et input dans la branch spec *) 

484 
let global_dependency_eqs (inputs: var_decl list) vars eqs = 

485 


486 
(* Format.eprintf "@.%a@." (Utils.fprintf_list ~sep:"@." Printers.pp_node_eq) eqs; *) 

487 
(* Format.eprintf "inputs: %a@." (Utils.fprintf_list ~sep:"@." Printers.pp_var) inputs; *) 

488 
let mems = ExprDep.eqs_memory_variables eqs in 

489 
(* Format.eprintf "@.global dep; mems: %a@.@?" (Utils.fprintf_list ~sep:", " Format.pp_print_string) (ISet.elements mems); *) 

490 
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs eqs in 

491 
(* Format.eprintf "g_non_mems: %a@.@?" pp_dep_graph g_non_mems; *) 

492 
(* Format.eprintf "g_mems: %a@.@?" pp_dep_graph g_mems; *) 

493 
CycleDetection.check_cycles g_non_mems; 

494 
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles vars eqs mems g_mems in 

495 
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) 

496 
merge_with g_non_mems g_mems'; 

497 
eqs', vdecls', g_non_mems 

498  
499  
500  461 
(* Local Variables: *) 
501  462 
(* compilecommand:"make C .." *) 
502  463 
(* End: *) 
Also available in: Unified diff
Revert casality to r288