Revision 01f1a1f4 src/causality.ml
| src/causality.ml | ||
|---|---|---|
| 470 | 470 |
(map : disjoint_map) |
| 471 | 471 |
end |
| 472 | 472 |
|
| 473 |
(* replace variable [v] by [v'] in disjunction [map]. Then:
|
|
| 473 |
(* merge variables [v] and [v'] in disjunction [map]. Then:
|
|
| 474 | 474 |
- the mapping v' becomes v' |-> (map v) inter (map v') |
| 475 | 475 |
- the mapping v |-> ... then disappears |
| 476 | 476 |
- other mappings become x |-> (map x) \ (if v in x then v else v') |
| 477 | 477 |
*) |
| 478 |
let replace_in_disjoint_map map v v' =
|
|
| 478 |
let merge_in_disjoint_map map v v' =
|
|
| 479 | 479 |
begin |
| 480 | 480 |
Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id)); |
| 481 | 481 |
Hashtbl.remove map v.var_id; |
| 482 | 482 |
Hashtbl.iter (fun x map_x -> Hashtbl.replace map x (CISet.remove (if CISet.mem v map_x then v else v') map_x)) map; |
| 483 | 483 |
end |
| 484 | 484 |
|
| 485 |
(* replace variable [v] by [v'] in disjunction [map]. |
|
| 486 |
[v'] is a dead variable. Then: |
|
| 487 |
- the mapping v' becomes v' |-> (map v) |
|
| 488 |
- the mapping v |-> ... then disappears |
|
| 489 |
- all mappings become x |-> ((map x) \ { v}) union ({v'} if v in map x)
|
|
| 490 |
*) |
|
| 491 |
let replace_in_disjoint_map map v v' = |
|
| 492 |
begin |
|
| 493 |
Hashtbl.replace map v'.var_id (Hashtbl.find map v.var_id); |
|
| 494 |
Hashtbl.remove map v.var_id; |
|
| 495 |
Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (if CISet.mem v mapx then CISet.add v' (CISet.remove v mapx) else CISet.remove v' mapx)) map; |
|
| 496 |
end |
|
| 497 |
|
|
| 498 |
(* remove variable [v] in disjunction [map]. Then: |
|
| 499 |
- the mapping v |-> ... then disappears |
|
| 500 |
- all mappings become x |-> (map x) \ { v}
|
|
| 501 |
*) |
|
| 502 |
let remove_in_disjoint_map map v = |
|
| 503 |
begin |
|
| 504 |
Hashtbl.remove map v.var_id; |
|
| 505 |
Hashtbl.iter (fun x mapx -> Hashtbl.replace map x (CISet.remove v mapx)) map; |
|
| 506 |
end |
|
| 507 |
|
|
| 485 | 508 |
let pp_disjoint_map fmt map = |
| 486 | 509 |
begin |
| 487 | 510 |
Format.fprintf fmt "{ /* disjoint map */@.";
|
| ... | ... | |
| 503 | 526 |
|
| 504 | 527 |
(* Merges elements of graph [g2] into graph [g1] *) |
| 505 | 528 |
let merge_with g1 g2 = |
| 529 |
begin |
|
| 506 | 530 |
IdentDepGraph.iter_vertex (fun v -> IdentDepGraph.add_vertex g1 v) g2; |
| 507 | 531 |
IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2 |
| 532 |
end |
|
| 533 |
|
|
| 534 |
let add_external_dependency outputs mems g = |
|
| 535 |
let caller ="!_world" in |
|
| 536 |
begin |
|
| 537 |
IdentDepGraph.add_vertex g caller; |
|
| 538 |
ISet.iter (fun o -> IdentDepGraph.add_edge g caller o) outputs; |
|
| 539 |
ISet.iter (fun m -> IdentDepGraph.add_edge g caller m) mems; |
|
| 540 |
end |
|
| 508 | 541 |
|
| 509 | 542 |
let global_dependency node = |
| 510 | 543 |
let mems = ExprDep.node_memory_variables node in |
| 511 | 544 |
let inputs = ExprDep.node_input_variables node in |
| 545 |
let outputs = ExprDep.node_output_variables node in |
|
| 512 | 546 |
let node_vars = ExprDep.node_variables node in |
| 513 | 547 |
let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in |
| 514 | 548 |
(*Format.eprintf "g_non_mems: %a" pp_dep_graph g_non_mems; |
| ... | ... | |
| 516 | 550 |
CycleDetection.check_cycles g_non_mems; |
| 517 | 551 |
let (vdecls', eqs', g_mems') = CycleDetection.break_cycles node mems g_mems in |
| 518 | 552 |
(*Format.eprintf "g_mems': %a" pp_dep_graph g_mems';*) |
| 519 |
merge_with g_non_mems g_mems'; |
|
| 520 |
{ node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals },
|
|
| 521 |
g_non_mems |
|
| 522 |
|
|
| 553 |
begin |
|
| 554 |
merge_with g_non_mems g_mems'; |
|
| 555 |
add_external_dependency outputs mems g_non_mems; |
|
| 556 |
{ node with node_eqs = eqs'; node_locals = vdecls'@node.node_locals },
|
|
| 557 |
g_non_mems |
|
| 558 |
end |
|
| 523 | 559 |
|
| 524 | 560 |
(* Local Variables: *) |
| 525 | 561 |
(* compile-command:"make -C .." *) |
Also available in: Unified diff