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