extracted/untrusted/build.ml

   1 (* Pasted from Pottier's PP compiler *)
   2
   3 open ERTL
   4 open Untrusted_interference
   5
   6 let build globals int_fun uses liveafter =
   7
   8   (* Create an interference graph whose vertices are the procedure's
   9      pseudo-registers. This graph initially has no edges. *)
  10
  11   let f_locals =
  12    Identifiers.foldi PreIdentifiers.RegisterTag
  13     (fun id _ map -> Pset.add id map
  14     ) uses Pset.empty in
  15
  16   let graph = create f_locals in
  17
  18   (* Every pseudo register interferes with special forbidden registers. *)
  19
  20   let graph = mkiph graph f_locals
  21    (Untrusted_interference.hwregisterset_of_list I8051.registersForbidden) in
  22
  23   (* Iterate over all statements in the control flow graph and populate the
  24      interference graph with interference and preference edges. *)
  25
  26   let graph =
  27     Identifiers.foldi PreIdentifiers.LabelTag (fun label stmt graph ->
  28       let live = liveafter label in
  29       if Liveness.eliminable globals live stmt = Bool.True then
  30
  31           (* This statement is eliminable and should be ignored. Eliminable
  32              statements have not been eliminated yet, because we are still
  33              in between ERTL and LTL. They *will* be eliminated soon, though,
  34              so there is no reason to take them into account while building
  35              the interference graph. *)
  36
  37           graph
  38
  39       else
  40
  41           (* Create interference edges. The general rule is, every
  42              pseudo-register or hardware register that is defined (written) by
  43              a statement interferes with every pseudo-register or hardware
  44              register (other than itself) that is live immediately after the
  45              statement executes.
  46
  47              An exception to the general rule can be made for move
  48              statements. In a move statement, we do not need the source
  49              and destination pseudo-registers to be assigned distinct hardware
  50              registers, since they contain the same value -- in fact, we would
  51              like them to be assigned the same hardware register. So, for a
  52              move statement, we let the register that is defined (written)
  53              interfere with every pseudo-register, other than itself *and
  54              other than the source pseudo-register*, that is live immediately
  55              after the statement executes. This optimization is explained in
  56              Chapter 10 of Appel's book (p. 221).
  57
  58              This special case is only a hack that works in many cases. There
  59              are cases where it doesn't suffice. For instance, if two
  60              successive move statements have the same source [r0], then
  61              their destinations [r1] and [r2] *will* be considered as
  62              interfering, even though it would in fact be correct and
  63              desirable to map both of them to the same hardware register. A
  64              more general solution would be to perform a static analysis that
  65              determines, for every program point, which pseudo-registers
  66              definitely hold the same value, and to exploit this information
  67              to build fewer interference edges. *)
  68
  69           let defined = Liveness.defined globals stmt in
  70           let exceptions =
  71             match stmt with
  72             | Joint.Sequential (Joint.Step_seq (Joint.MOVE arg),_) ->
  73                (match Obj.magic arg with
  74                   {Types.snd = Joint.Reg (ERTL.PSD sourcer)} ->
  75                    Liveness.rl_psingleton sourcer
  76                 | {Types.snd = Joint.Reg (ERTL.HDW sourcehwr)} ->
  77                    Liveness.rl_hsingleton sourcehwr
  78                 | _ -> Liveness.rl_bottom)
  79             | _ ->
  80                 Liveness.rl_bottom
  81           in
  82           let graph =
  83             mki graph (Obj.magic (Liveness.rl_diff live exceptions))
  84              (Obj.magic defined)
  85           in
  86
  87 (*
  88           (* Two registers written at the same time are interfering (they
  89              obviously should not be associated the same address).
  90              Only happens with St_addr. *)
  91
  92           let graph =
  93             match stmt with
  94               | St_addr (r1, r2, _, _) ->
  95                 mki graph (Liveness.L.psingleton r1) (Liveness.L.psingleton r2)
  96               | _ ->
  97                 graph
  98           in
  99 *)
 100
 101           (* Create preference edges between pseudo-registers. Two registers
 102              should preferably be assigned the same color when they are
 103              related by a move statement, so that the move statement can
 104              be eliminated. *)
 105
 106           let graph =
 107             match stmt with
 108             | Joint.Sequential (Joint.Step_seq (Joint.MOVE arg),_) ->
 109                (match Obj.magic arg with
 110                   {Types.fst = ERTL.PSD r1 ; snd = Joint.Reg (ERTL.PSD r2)} ->
 111                     mkppp graph r1 r2
 112                 | {Types.fst = ERTL.PSD r1 ; snd = Joint.Reg (ERTL.HDW r2)}
 113                 | {Types.fst = ERTL.HDW r2 ; snd = Joint.Reg (ERTL.PSD r1)} ->
 114                     mkpph graph r1 r2
 115                 | _ -> graph)
 116             | _ ->
 117                 graph
 118           in
 119   (*
 120
 121           (* Add interference edges between the hardware register [$zero]
 122              and every pseudo-register that the statement renders
 123              nonzeroable. See [Zero] for an explanation. *)
 124
 125           let graph =
 126             mkiph graph (Zero.nonzeroable i) (MIPS.RegisterSet.singleton MIPS.zero)
 127           in
 128   *)
 129           graph
 130
 131     ) (Obj.magic int_fun.Joint.joint_if_code) graph
 132   in
 133
 134   (* Done. *)
 135
 136   graph
 137