src/ERTL/liveness.ml

   1 (* Pasted from Pottier's PP compiler *)
   2
   3 open ERTL
   4
   5 (* In the following, a ``variable'' means a pseudo-register or an
   6    allocatable hardware register. *)
   7
   8 (* These functions allow turning an [ERTL] control flow graph into an
   9    explicit graph, that is, making successor edges explicit. This is
  10    useful in itself and facilitates the computation of predecessor
  11    edges. *)
  12
  13 let statement_successors (stmt : statement) =
  14   match stmt with
  15   | St_return _ ->
  16     Label.Set.empty
  17   | St_skip l
  18   | St_comment (_, l)
  19   | St_cost (_, l)
  20   | St_set_hdw (_, _, l)
  21   | St_get_hdw (_, _, l)
  22   | St_hdw_to_hdw (_, _, l)
  23   | St_newframe l
  24   | St_delframe l
  25   | St_framesize (_, l)
  26   | St_push (_, l)
  27   | St_pop (_, l)
  28   | St_addrH (_, _, l)
  29   | St_addrL (_, _, l)
  30   | St_int (_, _, l)
  31   | St_move (_, _, l)
  32   | St_opaccsA (_, _, _, _, l)
  33   | St_opaccsB (_, _, _, _, l)
  34   | St_op1 (_, _, _, l)
  35   | St_op2 (_, _, _, _, l)
  36   | St_clear_carry l
  37   | St_set_carry l
  38   | St_load (_, _, _, l)
  39   | St_store (_, _, _, l)
  40   | St_call_id (_, _, l)
  41   | St_call_ptr (_, _, _, l) ->
  42     Label.Set.singleton l
  43   | St_cond (_, l1, l2) ->
  44     Label.Set.add l1 (Label.Set.singleton l2)
  45
  46 (* The analysis uses the lattice of sets of variables. The lattice's
  47    join operation is pointwise set union, which reflects the fact that
  48    a variable is deemed live at a program point if and only if it is
  49    live at any of the successors of that program point. *)
  50
  51 module L = struct
  52
  53   (* A set of variable is represented as a pair of a set of
  54      pseudo-registers and a set of hardware registers. *)
  55
  56   type t =
  57       Register.Set.t * I8051.RegisterSet.t
  58
  59   type property =
  60       t
  61
  62   let bottom =
  63     Register.Set.empty, I8051.RegisterSet.empty
  64
  65   let psingleton r =
  66     Register.Set.singleton r, I8051.RegisterSet.empty
  67
  68   let hsingleton hwr =
  69     Register.Set.empty, I8051.RegisterSet.singleton hwr
  70
  71   let join (rset1, hwrset1) (rset2, hwrset2) =
  72     (Register.Set.union rset1 rset2, I8051.RegisterSet.union hwrset1 hwrset2)
  73
  74   let diff (rset1, hwrset1) (rset2, hwrset2) =
  75     (Register.Set.diff rset1 rset2, I8051.RegisterSet.diff hwrset1 hwrset2)
  76
  77   let equal (rset1, hwrset1) (rset2, hwrset2) =
  78     Register.Set.equal rset1 rset2 && I8051.RegisterSet.equal hwrset1 hwrset2
  79
  80   let is_maximal _ =
  81     false
  82
  83 end
  84
  85 module Label_ImperativeMap = struct
  86
  87   type key =
  88       Label.Map.key
  89
  90   type 'data t =
  91       'data Label.Map.t ref
  92
  93   let create () =
  94     ref Label.Map.empty
  95
  96   let clear t =
  97     t := Label.Map.empty
  98
  99   let add k d t =
 100     t := Label.Map.add k d !t
 101
 102   let find k t =
 103     Label.Map.find k !t
 104
 105   let iter f t =
 106     Label.Map.iter f !t
 107
 108 end
 109
 110 module F = Fix.Make (Label_ImperativeMap) (L)
 111
 112 (* These are the sets of variables defined at (written by) a statement. *)
 113
 114 let defined (stmt : statement) : L.t =
 115   match stmt with
 116   | St_skip _
 117   | St_comment _
 118   | St_cost _
 119   | St_push _
 120   | St_store _
 121   | St_cond _
 122   | St_return _ ->
 123     L.bottom
 124   | St_clear_carry _
 125   | St_set_carry _ ->
 126     Register.Set.empty, I8051.RegisterSet.singleton I8051.carry
 127   | St_op2 (I8051.Add, r, _, _, _)
 128   | St_op2 (I8051.Addc, r, _, _, _)
 129   | St_op2 (I8051.Sub, r, _, _, _) ->
 130     L.join (L.hsingleton I8051.carry) (L.psingleton r)
 131   | St_op1 (I8051.Inc, r, _, _)
 132   | St_get_hdw (r, _, _)
 133   | St_framesize (r, _)
 134   | St_pop (r, _)
 135   | St_int (r, _, _)
 136   | St_addrH (r, _, _)
 137   | St_addrL (r, _, _)
 138   | St_move (r, _, _)
 139   | St_opaccsA (_, r, _, _, _)
 140   | St_opaccsB (_, r, _, _, _)
 141   | St_op1 (_, r, _, _)
 142   | St_op2 (_, r, _, _, _)
 143   | St_load (r, _, _, _) ->
 144     L.psingleton r
 145   | St_set_hdw (r, _, _)
 146   | St_hdw_to_hdw (r, _, _) ->
 147     L.hsingleton r
 148   | St_call_id _ | St_call_ptr _  ->
 149       (* Potentially destroys all caller-save hardware registers. *)
 150     Register.Set.empty, I8051.caller_saved
 151   | St_newframe _
 152   | St_delframe _ ->
 153     L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
 154
 155 let set_of_list rl =
 156   List.fold_right I8051.RegisterSet.add rl I8051.RegisterSet.empty
 157
 158 (* This is the set of variables used at (read by) a statement. *)
 159
 160 let set_of_list =
 161   let f set r = I8051.RegisterSet.add r set in
 162   List.fold_left f I8051.RegisterSet.empty
 163
 164 let ret_regs = set_of_list I8051.rets
 165
 166 let used (stmt : statement) : L.t =
 167   match stmt with
 168   | St_skip _
 169   | St_comment _
 170   | St_cost _
 171   | St_framesize _
 172   | St_pop _
 173   | St_addrH _
 174   | St_addrL _
 175   | St_int _
 176   | St_clear_carry _
 177   | St_set_carry _ ->
 178     L.bottom
 179   | St_call_id (_, nparams, _) ->
 180     (* Reads the hardware registers that are used to pass parameters. *)
 181     Register.Set.empty,
 182     set_of_list (MiscPottier.prefix nparams I8051.parameters)
 183   | St_call_ptr (r1, r2, nparams, _) ->
 184     (* Reads the hardware registers that are used to pass parameters. *)
 185     Register.Set.of_list [r1 ; r2],
 186     set_of_list (MiscPottier.prefix nparams I8051.parameters)
 187   | St_get_hdw (_, r, _)
 188   | St_hdw_to_hdw (_, r, _) ->
 189     L.hsingleton r
 190   | St_set_hdw (_, r, _)
 191   | St_push (r, _)
 192   | St_move (_, r, _)
 193   | St_op1 (_, _, r, _)
 194   | St_cond (r, _, _) ->
 195     L.psingleton r
 196   | St_op2 (I8051.Addc, _, r1, r2, _) ->
 197     L.join (L.join (L.psingleton r1) (L.psingleton r2))
 198       (L.hsingleton I8051.carry)
 199   | St_opaccsA (_, _, r1, r2, _)
 200   | St_opaccsB (_, _, r1, r2, _)
 201   | St_op2 (_, _, r1, r2, _)
 202   | St_load (_, r1, r2, _) ->
 203     L.join (L.psingleton r1) (L.psingleton r2)
 204   | St_store (r1, r2, r3, _) ->
 205     L.join (L.join (L.psingleton r1) (L.psingleton r2)) (L.psingleton r3)
 206   | St_newframe _
 207   | St_delframe _ ->
 208     L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
 209   | St_return _ ->
 210     Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved ret_regs
 211
 212 (* A statement is considered pure if it has no side effect, that is, if
 213    its only effect is to write a value to its destination variable.
 214
 215    A pure statement whose destination is dead after the statement will
 216    be eliminated during the translation of [ERTL] to [LTL]. This is done by
 217    replacing the statement with an [St_skip] statement.
 218
 219    [eliminable liveafter stmt] returns [Some l], where [l] is [stmt]'s single
 220    successor, if statement [stmt] is eliminable. Otherwise, it returns
 221    [None]. The parameter [liveafter] is the set of variables that are live
 222    after the statement. *)
 223
 224 let eliminable ((pliveafter, hliveafter) : L.t) (stmt : statement) =
 225   match stmt with
 226   | St_skip _
 227   | St_comment _
 228   | St_cost _
 229   | St_newframe _
 230   | St_delframe _
 231   | St_pop _
 232   | St_push _
 233   | St_clear_carry _
 234   | St_set_carry _
 235   | St_store _
 236   | St_call_id _
 237   | St_call_ptr _
 238   | St_cond _
 239   | St_return _ ->
 240     None
 241   | St_get_hdw (r, _, l)
 242   | St_framesize (r, l)
 243   | St_int (r, _, l)
 244   | St_addrH (r, _, l)
 245   | St_addrL (r, _, l)
 246   | St_move (r, _, l)
 247   | St_opaccsA (_, r, _, _, l)
 248   | St_opaccsB (_, r, _, _, l)
 249   | St_op1 (_, r, _, l)
 250   | St_op2 (_, r, _, _, l)
 251   | St_load (r, _, _, l) ->
 252     if (Register.Set.mem r pliveafter) ||
 253        (I8051.RegisterSet.mem I8051.carry hliveafter) then None else Some l
 254   | St_set_hdw (r, _, l)
 255   | St_hdw_to_hdw (r, _, l) ->
 256     if I8051.RegisterSet.mem r hliveafter then None else Some l
 257
 258 (* This is the abstract semantics of instructions. It defines the
 259    variables that are live before the instruction in terms of
 260    those that are live after the instruction. *)
 261
 262 (* The standard definition is: a variable is considered live
 263    before the instruction if either (1) it is used by the instruction,
 264    or (2) it is live after the instruction and not defined by the
 265    instruction.
 266
 267    As an exception to this rule, if the instruction is eliminable,
 268    then a variable is considered live before the instruction
 269    if and only if it is live after the instruction. This anticipates
 270    on the instruction's elimination.
 271
 272    This exception means that the source variables of a pure
 273    instruction need not be considered live if the instruction's result
 274    is unused. This allows a sequence of pure instructions whose end
 275    result is dead to be considered entirely dead.
 276
 277    It is a simple, but not entirely trivial, exercise to check that
 278    this transfer function is monotone. *)
 279
 280 let statement_semantics (stmt : statement) (liveafter : L.t) : L.t =
 281   match eliminable liveafter stmt with
 282   | None ->
 283       L.join (L.diff liveafter (defined stmt)) (used stmt)
 284   | Some _ ->
 285       liveafter
 286
 287 (* A valuation is a function that maps a program point (a control flow
 288    graph label) to the set of variables that are live after that
 289    point. *)
 290
 291 type valuation =
 292     Label.t -> L.t
 293
 294 (* This is how we turn an [ERTL] procedure into a liveness analysis
 295    problem and solve it. *)
 296
 297 let analyze (int_fun : internal_function) : valuation =
 298
 299   (* Formulate the problem. Construct a system (recursive) equations
 300      that describe the live variables before and after each
 301      instruction. *)
 302
 303   (* The following two functions, [livebefore] and [liveafter],
 304      define these equations. Both use an oracle, a valuation --
 305      also called [liveafter] -- which is supposed to tell us
 306      which variables are live after each label. *)
 307
 308   (* The live variables before an instruction are computed, using the
 309      instruction's semantics, in terms of the live variables after the
 310      instruction -- which are given by the oracle. *)
 311
 312   let livebefore label (liveafter : valuation) : L.t =
 313     let stmt : statement = Label.Map.find label int_fun.f_graph in
 314     statement_semantics stmt (liveafter label)
 315   in
 316
 317   (* The live variables after an instruction are the union of the live
 318      variables before each of the instruction's successors. *)
 319
 320   let liveafter label (liveafter : valuation) : L.t =
 321     let stmt : statement = Label.Map.find label int_fun.f_graph in
 322     Label.Set.fold (fun successor accu ->
 323       L.join (livebefore successor liveafter) accu
 324     ) (statement_successors stmt) L.bottom
 325   in
 326
 327   (* Compute the least fixed point of these recursive equations. *)
 328
 329   F.lfp liveafter