1 (* Pasted from Pottier's PP compiler *)
4 open Untrusted_interference
6 let build globals int_fun uses liveafter =
8 (* Create an interference graph whose vertices are the procedure's
9 pseudo-registers. This graph initially has no edges. *)
12 Identifiers.foldi PreIdentifiers.RegisterTag
13 (fun id _ map -> Pset.add id map
16 let graph = create f_locals in
18 (* Every pseudo register interferes with special forbidden registers. *)
20 let graph = mkiph graph f_locals
21 (Untrusted_interference.hwregisterset_of_list I8051.registersForbidden) in
23 (* Iterate over all statements in the control flow graph and populate the
24 interference graph with interference and preference edges. *)
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
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. *)
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
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).
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. *)
69 let defined = Liveness.defined globals stmt in
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)
83 mki graph (Obj.magic (Liveness.rl_diff live exceptions))
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. *)
94 | St_addr (r1, r2, _, _) ->
95 mki graph (Liveness.L.psingleton r1) (Liveness.L.psingleton r2)
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
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)} ->
112 | {Types.fst = ERTL.PSD r1 ; snd = Joint.Reg (ERTL.HDW r2)}
113 | {Types.fst = ERTL.HDW r2 ; snd = Joint.Reg (ERTL.PSD r1)} ->
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. *)
126 mkiph graph (Zero.nonzeroable i) (MIPS.RegisterSet.singleton MIPS.zero)
131 ) (Obj.magic int_fun.Joint.joint_if_code) graph