source: Deliverables/D2.2/8051/src/LTL/branch.ml @ 486

Last change on this file since 486 was 486, checked in by ayache, 8 years ago

Deliverable D2.2

File size: 2.2 KB
Line 
1(* Pasted from Pottier's PP compiler *)
2
3open LTL
4
5let compress entry graph =
6
7  (* Build a table that maps every graph label to a distinct ``point''
8     in the sense of [UnionFind]. *)
9
10  let points =
11    Label.Map.mapi (fun label _ ->
12      UnionFind.fresh label
13    ) graph
14  in
15
16  let lookup label =
17    try
18      Label.Map.find label points
19    with Not_found ->
20      assert false
21  in
22
23  (* For every [St_skip] statement, make the source label an alias for
24     the target label, unless the former is already an alias for the
25     latter (which means that the graph contains a cycle of [St_skip]
26     statements). *)
27
28  Label.Map.iter (fun src stmt ->
29    let source = lookup src in
30    match stmt with
31    | St_skip trgt ->
32        let target = lookup trgt in
33        if UnionFind.equivalent source target then
34          assert false (* can happen if the program contains an empty infinite loop, but let's ignore that *)
35        else
36          UnionFind.union source target
37    | _ ->
38        ()
39  ) graph;
40
41  (* Transform the graph by replacing every label with its representative. *)
42
43  let rep label =
44    UnionFind.find (lookup label)
45  in
46
47  rep entry, Label.Map.map (function
48    | LTL.St_skip l ->
49      LTL.St_skip (rep l) (* statement will be unreachable *)
50    | LTL.St_comment (s, l) ->
51      LTL.St_comment (s, rep l)
52    | LTL.St_cost (lbl, l) ->
53      LTL.St_cost (lbl, rep l)
54    | LTL.St_int (r, i, l) ->
55      LTL.St_int (r, i, rep l)
56    | LTL.St_addr (x, l) ->
57      LTL.St_addr (x, rep l)
58    | LTL.St_pop l ->
59      LTL.St_pop (rep l)
60    | LTL.St_push l ->
61      LTL.St_push (rep l)
62    | LTL.St_clear_carry l ->
63      LTL.St_clear_carry (rep l)
64    | LTL.St_from_acc (r, l) ->
65      LTL.St_from_acc (r, rep l)
66    | LTL.St_to_acc (r, l) ->
67      LTL.St_to_acc (r, rep l)
68    | LTL.St_opaccs (opaccs, l) ->
69      LTL.St_opaccs (opaccs, rep l)
70    | LTL.St_op1 (op1, l) ->
71      LTL.St_op1 (op1, rep l)
72    | LTL.St_op2 (op2, r, l) ->
73      LTL.St_op2 (op2, r, rep l)
74    | LTL.St_load l ->
75      LTL.St_load (rep l)
76    | LTL.St_store l ->
77      LTL.St_store (rep l)
78    | LTL.St_call_id (f, l) ->
79      LTL.St_call_id (f, rep l)
80    | LTL.St_condacc (lbl_true, lbl_false) ->
81      LTL.St_condacc (rep lbl_true, rep lbl_false)
82    | LTL.St_return ->
83      LTL.St_return
84  ) graph
Note: See TracBrowser for help on using the repository browser.