| 1 | (* Pasted from Pottier's PP compiler *) |
|---|
| 2 | |
|---|
| 3 | open LTL |
|---|
| 4 | |
|---|
| 5 | let 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_ind_0 (i, l) -> |
|---|
| 55 | LTL.St_ind_0 (i, rep l) |
|---|
| 56 | | LTL.St_ind_inc (i, l) -> |
|---|
| 57 | LTL.St_ind_inc (i, rep l) |
|---|
| 58 | | LTL.St_int (r, i, l) -> |
|---|
| 59 | LTL.St_int (r, i, rep l) |
|---|
| 60 | | LTL.St_addr (x, l) -> |
|---|
| 61 | LTL.St_addr (x, rep l) |
|---|
| 62 | | LTL.St_pop l -> |
|---|
| 63 | LTL.St_pop (rep l) |
|---|
| 64 | | LTL.St_push l -> |
|---|
| 65 | LTL.St_push (rep l) |
|---|
| 66 | | LTL.St_clear_carry l -> |
|---|
| 67 | LTL.St_clear_carry (rep l) |
|---|
| 68 | | LTL.St_set_carry l -> |
|---|
| 69 | LTL.St_set_carry (rep l) |
|---|
| 70 | | LTL.St_from_acc (r, l) -> |
|---|
| 71 | LTL.St_from_acc (r, rep l) |
|---|
| 72 | | LTL.St_to_acc (r, l) -> |
|---|
| 73 | LTL.St_to_acc (r, rep l) |
|---|
| 74 | | LTL.St_opaccs (opaccs, l) -> |
|---|
| 75 | LTL.St_opaccs (opaccs, rep l) |
|---|
| 76 | | LTL.St_op1 (op1, l) -> |
|---|
| 77 | LTL.St_op1 (op1, rep l) |
|---|
| 78 | | LTL.St_op2 (op2, r, l) -> |
|---|
| 79 | LTL.St_op2 (op2, r, rep l) |
|---|
| 80 | | LTL.St_load l -> |
|---|
| 81 | LTL.St_load (rep l) |
|---|
| 82 | | LTL.St_store l -> |
|---|
| 83 | LTL.St_store (rep l) |
|---|
| 84 | | LTL.St_call_id (f, l) -> |
|---|
| 85 | LTL.St_call_id (f, rep l) |
|---|
| 86 | | LTL.St_call_ptr l -> |
|---|
| 87 | LTL.St_call_ptr (rep l) |
|---|
| 88 | | LTL.St_condacc (lbl_true, lbl_false) -> |
|---|
| 89 | LTL.St_condacc (rep lbl_true, rep lbl_false) |
|---|
| 90 | | LTL.St_return -> |
|---|
| 91 | LTL.St_return |
|---|
| 92 | ) graph |
|---|
