1 | include "ASM/Util.ma". |
---|
2 | include "ERTL/ERTL.ma". |
---|
3 | |
---|
4 | definition list_set_union ≝ |
---|
5 | λA: Type[0]. |
---|
6 | λeq_a: A → A → bool. |
---|
7 | λl: list A. |
---|
8 | λr: list A. |
---|
9 | nub_by A eq_a (l @ r). |
---|
10 | |
---|
11 | definition list_set_add ≝ |
---|
12 | λA: Type[0]. |
---|
13 | λeq_a: A → A → bool. |
---|
14 | λa: A. |
---|
15 | λs: list A. |
---|
16 | nub_by A eq_a (a :: s). |
---|
17 | |
---|
18 | definition list_set_diff ≝ |
---|
19 | λA: Type[0]. |
---|
20 | λeq_a: A → A → bool. |
---|
21 | λl: list A. |
---|
22 | λr: list A. |
---|
23 | filter A (λx. member A eq_a x r) l. |
---|
24 | |
---|
25 | definition list_set_equal ≝ |
---|
26 | λA: Type[0]. |
---|
27 | λeq_a: A → A → bool. |
---|
28 | λl: list A. |
---|
29 | λr: list A. |
---|
30 | foldr ? ? andb true (map ? ? (λx. member A eq_a x r) l). |
---|
31 | |
---|
32 | definition list_set_member ≝ member. |
---|
33 | |
---|
34 | definition list_set_fold ≝ foldr. |
---|
35 | |
---|
36 | definition statement_successors ≝ |
---|
37 | λglobals: list ident. |
---|
38 | λs: ertl_statement globals. |
---|
39 | match s with |
---|
40 | [ joint_st_sequential seq l ⇒ |
---|
41 | match seq with |
---|
42 | [ joint_instr_cond acc_a_reg lbl_true ⇒ |
---|
43 | list_set_add ? (eq_identifier ?) lbl_true [ l ] |
---|
44 | | _ ⇒ [ l ] |
---|
45 | ] |
---|
46 | | joint_st_extension ext ⇒ |
---|
47 | match ext with |
---|
48 | [ ertl_st_ext_new_frame l ⇒ [ l ] |
---|
49 | | ertl_st_ext_del_frame l ⇒ [ l ] |
---|
50 | | ertl_st_ext_frame_size r l ⇒ [ l ] |
---|
51 | ] |
---|
52 | | joint_st_goto l ⇒ [ l ] |
---|
53 | | joint_st_return ⇒ [ ] |
---|
54 | ]. |
---|
55 | |
---|
56 | definition register_lattice ≝ (list register) × (list Register). |
---|
57 | definition lattice_property ≝ register_lattice. |
---|
58 | definition lattice_bottom: register_lattice ≝ 〈[ ], [ ]〉. |
---|
59 | definition lattice_psingleton: register → register_lattice ≝ |
---|
60 | λr. |
---|
61 | 〈[ r ], [ ]〉. |
---|
62 | definition lattice_hsingleton: Register → register_lattice ≝ |
---|
63 | λr. |
---|
64 | 〈[ ], [ r ]〉. |
---|
65 | |
---|
66 | definition lattice_join: register_lattice → register_lattice → register_lattice ≝ |
---|
67 | λleft. |
---|
68 | λright. |
---|
69 | let 〈lp, lh〉 ≝ left in |
---|
70 | let 〈rp, rh〉 ≝ right in |
---|
71 | 〈list_set_union ? (eq_identifier ?) lp rp, list_set_union ? eq_Register lh rh〉. |
---|
72 | |
---|
73 | definition lattice_diff: register_lattice → register_lattice → register_lattice ≝ |
---|
74 | λleft. |
---|
75 | λright. |
---|
76 | let 〈lp, lh〉 ≝ left in |
---|
77 | let 〈rp, rh〉 ≝ right in |
---|
78 | 〈list_set_diff ? (eq_identifier ?) lp rp, list_set_diff ? eq_Register lh rh〉. |
---|
79 | |
---|
80 | definition lattice_equal: register_lattice → register_lattice → bool ≝ |
---|
81 | λleft. |
---|
82 | λright. |
---|
83 | let 〈lp, lh〉 ≝ left in |
---|
84 | let 〈rp, rh〉 ≝ right in |
---|
85 | andb (list_set_equal ? (eq_identifier ?) lp rp) (list_set_equal ? eq_Register lh rh). |
---|
86 | |
---|
87 | definition lattice_is_maximal: register_lattice → bool ≝ λl. false. |
---|
88 | |
---|
89 | record lattice_property_sig: Type[1] ≝ |
---|
90 | { |
---|
91 | lp_type : Type[0]; |
---|
92 | lp_property : Type[0]; |
---|
93 | lp_bottom : lp_type; |
---|
94 | lp_psingleton: register → lp_type; |
---|
95 | lp_hsingleton: Register → lp_type; |
---|
96 | lp_join : lp_type → lp_type → lp_type; |
---|
97 | lp_diff : lp_type → lp_type → lp_type; |
---|
98 | lp_equal : lp_type → lp_type → bool; |
---|
99 | lp_is_maximal: lp_type → bool |
---|
100 | }. |
---|
101 | |
---|
102 | definition property ≝ |
---|
103 | mk_lattice_property_sig |
---|
104 | ((list register) × (list Register)) |
---|
105 | lattice_property |
---|
106 | lattice_bottom |
---|
107 | lattice_psingleton |
---|
108 | lattice_hsingleton |
---|
109 | lattice_join |
---|
110 | lattice_diff |
---|
111 | lattice_equal |
---|
112 | lattice_is_maximal. |
---|
113 | |
---|
114 | definition defined ≝ |
---|
115 | λglobals: list ident. |
---|
116 | λs: ertl_statement globals. |
---|
117 | match s with |
---|
118 | [ joint_st_sequential seq l ⇒ |
---|
119 | match seq with |
---|
120 | [ joint_instr_op2 op2 r _ ⇒ |
---|
121 | match op2 with |
---|
122 | [ Add ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) |
---|
123 | | Addc ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) |
---|
124 | | Sub ⇒ lattice_join (lattice_hsingleton RegisterCarry) (lattice_psingleton r) |
---|
125 | | _ ⇒ lattice_psingleton r |
---|
126 | ] |
---|
127 | | joint_instr_clear_carry ⇒ lattice_hsingleton RegisterCarry |
---|
128 | | joint_instr_set_carry ⇒ lattice_hsingleton RegisterCarry |
---|
129 | | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) |
---|
130 | | joint_instr_op1 op1 r ⇒ lattice_psingleton r |
---|
131 | | joint_instr_pop r ⇒ lattice_psingleton r |
---|
132 | | joint_instr_int r _ ⇒ lattice_psingleton r |
---|
133 | | joint_instr_address _ _ r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) |
---|
134 | | joint_instr_load r _ _ ⇒ lattice_psingleton r |
---|
135 | (* Potentially destroys all caller-save hardware registers. *) |
---|
136 | | joint_instr_call_id _ _ ⇒ 〈[ ], RegisterCallerSaved〉 |
---|
137 | | joint_instr_comment c ⇒ lattice_bottom |
---|
138 | | joint_instr_cond r lbl_true ⇒ lattice_bottom |
---|
139 | | joint_instr_store acc_a dpl dph ⇒ lattice_bottom |
---|
140 | | joint_instr_cost_label clabel ⇒ lattice_bottom |
---|
141 | | joint_instr_push r ⇒ lattice_bottom |
---|
142 | | joint_instr_move pair_reg ⇒ |
---|
143 | (* first register relevant only *) |
---|
144 | let r1 ≝ \fst pair_reg in |
---|
145 | match r1 with |
---|
146 | [ pseudo p ⇒ lattice_psingleton p |
---|
147 | | hardware h ⇒ lattice_hsingleton h |
---|
148 | ] |
---|
149 | ] |
---|
150 | | joint_st_return ⇒ lattice_bottom |
---|
151 | | joint_st_extension ext ⇒ |
---|
152 | match ext with |
---|
153 | [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) |
---|
154 | | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) |
---|
155 | | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r |
---|
156 | ] |
---|
157 | | joint_st_goto l ⇒ lattice_bottom |
---|
158 | ]. |
---|
159 | |
---|
160 | definition list_set_of_list ≝ |
---|
161 | λrl. |
---|
162 | foldr ? ? (list_set_add Register eq_Register) rl [ ]. |
---|
163 | |
---|
164 | definition list_set_of_list2 ≝ |
---|
165 | let f ≝ λset. λr. list_set_add Register eq_Register r set in |
---|
166 | foldl ? ? f [ ]. |
---|
167 | |
---|
168 | definition ret_regs ≝ list_set_of_list RegisterRets. |
---|
169 | |
---|
170 | definition used ≝ |
---|
171 | λglobals: list ident. |
---|
172 | λs: ertl_statement globals. |
---|
173 | match s with |
---|
174 | [ joint_st_sequential seq l ⇒ |
---|
175 | match seq with |
---|
176 | [ joint_instr_op2 op2 acc_a r ⇒ |
---|
177 | match op2 with |
---|
178 | [ Addc ⇒ |
---|
179 | lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton r)) (lattice_hsingleton RegisterCarry) |
---|
180 | | _ ⇒ lattice_join (lattice_psingleton acc_a) (lattice_psingleton r) |
---|
181 | ] |
---|
182 | | joint_instr_clear_carry ⇒ lattice_bottom |
---|
183 | | joint_instr_set_carry ⇒ lattice_bottom |
---|
184 | (* acc_a and acc_b *) |
---|
185 | | joint_instr_opaccs opaccs r1 r2 ⇒ lattice_join (lattice_psingleton r1) (lattice_psingleton r2) |
---|
186 | | joint_instr_op1 op1 r ⇒ lattice_psingleton r |
---|
187 | | joint_instr_pop r ⇒ lattice_bottom |
---|
188 | | joint_instr_int r _ ⇒ lattice_bottom |
---|
189 | | joint_instr_address _ _ r1 r2 ⇒ lattice_bottom |
---|
190 | | joint_instr_load acc_a dpl dph ⇒ lattice_join (lattice_psingleton dpl) (lattice_psingleton dph) |
---|
191 | (* Reads the hardware registers that are used to pass parameters. *) |
---|
192 | | joint_instr_call_id _ nparams ⇒ 〈[ ], list_set_of_list (prefix ? nparams RegisterParams)〉 |
---|
193 | | joint_instr_comment c ⇒ lattice_bottom |
---|
194 | | joint_instr_cond r lbl_true ⇒ lattice_psingleton r |
---|
195 | | joint_instr_store acc_a dpl dph ⇒ |
---|
196 | lattice_join (lattice_join (lattice_psingleton acc_a) (lattice_psingleton dpl)) (lattice_psingleton dph) |
---|
197 | | joint_instr_cost_label clabel ⇒ lattice_bottom |
---|
198 | | joint_instr_push r ⇒ lattice_psingleton r |
---|
199 | | joint_instr_move pair_reg ⇒ |
---|
200 | (* only second reg in pair relevant *) |
---|
201 | let r2 ≝ \snd pair_reg in |
---|
202 | match r2 with |
---|
203 | [ pseudo p ⇒ lattice_psingleton p |
---|
204 | | hardware h ⇒ lattice_hsingleton h |
---|
205 | ] |
---|
206 | ] |
---|
207 | | joint_st_return ⇒ 〈[ ], list_set_union ? eq_Register RegisterCalleeSaved ret_regs〉 |
---|
208 | | joint_st_goto l ⇒ lattice_bottom |
---|
209 | | joint_st_extension ext ⇒ |
---|
210 | match ext with |
---|
211 | [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) |
---|
212 | | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH) |
---|
213 | | ertl_st_ext_frame_size r l ⇒ lattice_bottom |
---|
214 | ] |
---|
215 | ]. |
---|
216 | |
---|
217 | definition eliminable ≝ |
---|
218 | λglobals: list ident. |
---|
219 | λl: register_lattice. |
---|
220 | λs: ertl_statement globals. |
---|
221 | let 〈pliveafter, hliveafter〉 ≝ l in |
---|
222 | match s with |
---|
223 | [ joint_st_sequential seq l ⇒ |
---|
224 | match seq with |
---|
225 | [ joint_instr_op2 op2 acc_a r ⇒ |
---|
226 | if list_set_member register (eq_identifier ?) acc_a pliveafter ∨ |
---|
227 | list_set_member Register eq_Register RegisterCarry hliveafter then |
---|
228 | None ? |
---|
229 | else |
---|
230 | Some ? l |
---|
231 | | joint_instr_clear_carry ⇒ None ? |
---|
232 | | joint_instr_set_carry ⇒ None ? |
---|
233 | | joint_instr_opaccs opaccs r1 r2 ⇒ |
---|
234 | if list_set_member register (eq_identifier ?) r1 pliveafter ∨ |
---|
235 | list_set_member register (eq_identifier ?) r2 pliveafter ∨ |
---|
236 | list_set_member Register eq_Register RegisterCarry hliveafter then |
---|
237 | None ? |
---|
238 | else |
---|
239 | Some ? l |
---|
240 | | joint_instr_op1 op1 r ⇒ |
---|
241 | if list_set_member register (eq_identifier ?) r pliveafter ∨ |
---|
242 | list_set_member Register eq_Register RegisterCarry hliveafter then |
---|
243 | None ? |
---|
244 | else |
---|
245 | Some ? l |
---|
246 | | joint_instr_pop r ⇒ None ? |
---|
247 | | joint_instr_int r _ ⇒ |
---|
248 | if list_set_member register (eq_identifier ?) r pliveafter ∨ |
---|
249 | list_set_member Register eq_Register RegisterCarry hliveafter then |
---|
250 | None ? |
---|
251 | else |
---|
252 | Some ? l |
---|
253 | | joint_instr_address _ _ r1 r2 ⇒ |
---|
254 | if list_set_member register (eq_identifier ?) r1 pliveafter ∨ |
---|
255 | list_set_member register (eq_identifier ?) r2 pliveafter ∨ |
---|
256 | list_set_member Register eq_Register RegisterCarry hliveafter then |
---|
257 | None ? |
---|
258 | else |
---|
259 | Some ? l |
---|
260 | | joint_instr_load acc_a dpl dph ⇒ |
---|
261 | if list_set_member register (eq_identifier ?) acc_a pliveafter ∨ |
---|
262 | list_set_member Register eq_Register RegisterCarry hliveafter then |
---|
263 | None ? |
---|
264 | else |
---|
265 | Some ? l |
---|
266 | | joint_instr_call_id _ nparams ⇒ None ? |
---|
267 | | joint_instr_comment c ⇒ None ? |
---|
268 | | joint_instr_cond r lbl_true ⇒ None ? |
---|
269 | | joint_instr_store acc_a dpl dph ⇒ None ? |
---|
270 | | joint_instr_cost_label clabel ⇒ None ? |
---|
271 | | joint_instr_push r ⇒ None ? |
---|
272 | | joint_instr_move pair_reg ⇒ |
---|
273 | let r1 ≝ \fst pair_reg in |
---|
274 | let r2 ≝ \snd pair_reg in |
---|
275 | match r1 with |
---|
276 | [ pseudo p1 ⇒ |
---|
277 | if list_set_member register (eq_identifier ?) p1 pliveafter ∨ |
---|
278 | list_set_member Register eq_Register RegisterCarry hliveafter then |
---|
279 | None ? |
---|
280 | else |
---|
281 | Some ? l |
---|
282 | | hardware h1 ⇒ |
---|
283 | if list_set_member Register eq_Register h1 hliveafter then |
---|
284 | None ? |
---|
285 | else |
---|
286 | Some ? l |
---|
287 | ] |
---|
288 | ] |
---|
289 | | joint_st_goto l ⇒ None ? |
---|
290 | | joint_st_return ⇒ None ? |
---|
291 | | joint_st_extension ext ⇒ |
---|
292 | match ext with |
---|
293 | [ ertl_st_ext_new_frame l ⇒ None ? |
---|
294 | | ertl_st_ext_del_frame l ⇒ None ? |
---|
295 | | ertl_st_ext_frame_size r l ⇒ |
---|
296 | if list_set_member register (eq_identifier ?) r pliveafter ∨ |
---|
297 | list_set_member Register eq_Register RegisterCarry hliveafter then |
---|
298 | None ? |
---|
299 | else |
---|
300 | Some ? l |
---|
301 | ] |
---|
302 | ]. |
---|
303 | |
---|
304 | definition statement_semantics: ∀globals: list ident. ertl_statement globals → register_lattice → register_lattice ≝ |
---|
305 | λglobals. |
---|
306 | λstmt. |
---|
307 | λliveafter. |
---|
308 | match eliminable globals liveafter stmt with |
---|
309 | [ None ⇒ lattice_join (lattice_diff liveafter (defined globals stmt)) (used globals stmt) |
---|
310 | | Some l ⇒ liveafter |
---|
311 | ]. |
---|
312 | |
---|
313 | definition valuation ≝ label → register_lattice. |
---|
314 | definition rhs ≝ valuation → lattice_property. |
---|
315 | definition equations ≝ label → rhs. |
---|
316 | |
---|
317 | axiom fix_lfp: equations → valuation. |
---|
318 | |
---|
319 | definition livebefore ≝ |
---|
320 | λglobals: list ident. |
---|
321 | λint_fun. |
---|
322 | λlabel. |
---|
323 | λliveafter: valuation. |
---|
324 | match lookup ? ? (ertl_if_graph globals int_fun) label with |
---|
325 | [ None ⇒ ? |
---|
326 | | Some stmt ⇒ statement_semantics globals stmt (liveafter label) |
---|
327 | ]. |
---|
328 | cases not_implemented (* XXX *) |
---|
329 | qed. |
---|
330 | |
---|
331 | definition liveafter ≝ |
---|
332 | λglobals. |
---|
333 | λint_fun. |
---|
334 | λlivebefore. |
---|
335 | λlabel. |
---|
336 | λliveafter: valuation. |
---|
337 | match lookup … (ertl_if_graph globals int_fun) label with |
---|
338 | [ None ⇒ ? |
---|
339 | | Some stmt ⇒ list_set_fold … (λsuccessor. λaccu: register_lattice. |
---|
340 | lattice_join (livebefore successor liveafter) accu) |
---|
341 | lattice_bottom (statement_successors globals stmt) |
---|
342 | ]. |
---|
343 | cases not_implemented (* XXX *) |
---|
344 | qed. |
---|
345 | |
---|
346 | definition analyse ≝ |
---|
347 | λglobals. |
---|
348 | λint_fun. |
---|
349 | fix_lfp (liveafter globals int_fun (livebefore globals int_fun)). |
---|