src/LTL/branch.ml

   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_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_set_carry l ->
  65       LTL.St_set_carry (rep l)
  66     | LTL.St_from_acc (r, l) ->
  67       LTL.St_from_acc (r, rep l)
  68     | LTL.St_to_acc (r, l) ->
  69       LTL.St_to_acc (r, rep l)
  70     | LTL.St_opaccs (opaccs, l) ->
  71       LTL.St_opaccs (opaccs, rep l)
  72     | LTL.St_op1 (op1, l) ->
  73       LTL.St_op1 (op1, rep l)
  74     | LTL.St_op2 (op2, r, l) ->
  75       LTL.St_op2 (op2, r, rep l)
  76     | LTL.St_load l ->
  77       LTL.St_load (rep l)
  78     | LTL.St_store l ->
  79       LTL.St_store (rep l)
  80     | LTL.St_call_id (f, l) ->
  81       LTL.St_call_id (f, rep l)
  82     | LTL.St_call_ptr l ->
  83       LTL.St_call_ptr (rep l)
  84     | LTL.St_condacc (lbl_true, lbl_false) ->
  85       LTL.St_condacc (rep lbl_true, rep lbl_false)
  86     | LTL.St_return ->
  87       LTL.St_return
  88   ) graph