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