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