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