1 | include "LTL/LTL.ma". |
---|
2 | include "ERTL/Interference.ma". |
---|
3 | include "ASM/Arithmetic.ma". |
---|
4 | include "joint/TranslateUtils.ma". |
---|
5 | include "joint/joint_stacksizes.ma". |
---|
6 | |
---|
7 | (* Note: translation is complicated by having to preserve the carry bit and |
---|
8 | wanting to do it with as less boilerplate as possible. It could be somewhat |
---|
9 | simplified if constant and copy propagation was to be done after this pass: |
---|
10 | those optimisations would take care of the boilerplate for us.*) |
---|
11 | |
---|
12 | coercion Reg_to_dec : ∀r:Register.decision ≝ decision_colour on _r : Register to decision. |
---|
13 | |
---|
14 | inductive arg_decision : Type[0] ≝ |
---|
15 | | arg_decision_colour : Register → arg_decision |
---|
16 | | arg_decision_spill : ℕ → arg_decision |
---|
17 | | arg_decision_imm : Byte → arg_decision. |
---|
18 | |
---|
19 | coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision. |
---|
20 | |
---|
21 | (* Paolo: I'm changing the following: before, spilled registers were |
---|
22 | assigned stack addresses going from SP + #frame_size - #stack_params |
---|
23 | excluded down to SP included. I am turning it upside down, so that |
---|
24 | the offset does not need the stack size to be computed *) |
---|
25 | |
---|
26 | definition preserve_carry_bit : |
---|
27 | ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝ |
---|
28 | λglobals,do_it,steps. |
---|
29 | if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps. |
---|
30 | |
---|
31 | (* for notation *) |
---|
32 | definition A ≝ it. |
---|
33 | |
---|
34 | coercion beval_of_byte : ∀b : Byte.beval ≝ BVByte on _b : Byte to beval. |
---|
35 | |
---|
36 | (* spill should be byte-based from the start *) |
---|
37 | definition set_dp_by_offset : |
---|
38 | ∀globals.nat → list (joint_seq LTL globals) ≝ |
---|
39 | λglobals,off. |
---|
40 | [ A ← byte_of_nat off |
---|
41 | ; A ← A .Add. RegisterSPL |
---|
42 | ; RegisterDPL ← A |
---|
43 | ; A ← zero_byte |
---|
44 | ; A ← A .Addc. RegisterSPH |
---|
45 | ; RegisterDPH ← A |
---|
46 | ]. |
---|
47 | |
---|
48 | definition get_stack: |
---|
49 | ∀globals.nat → Register → nat → list (joint_seq LTL globals) ≝ |
---|
50 | λglobals,localss,r,off. |
---|
51 | let off ≝ localss + off in |
---|
52 | set_dp_by_offset ? off @ |
---|
53 | [ LOAD … A it it ] @ |
---|
54 | if eq_Register r RegisterA then [ ] else [ r ← A ]. |
---|
55 | |
---|
56 | definition set_stack_not_a : |
---|
57 | ∀globals.nat → nat → Register → list (joint_seq LTL globals) ≝ |
---|
58 | λglobals,localss,off,r. |
---|
59 | let off ≝ localss + off in |
---|
60 | set_dp_by_offset ? off @ |
---|
61 | [ A ← r |
---|
62 | ; STORE … it it A ]. |
---|
63 | |
---|
64 | definition set_stack_a : |
---|
65 | ∀globals.nat → nat → list (joint_seq LTL globals) ≝ |
---|
66 | λglobals,localss,off. |
---|
67 | [ RegisterST1 ← A ] @ |
---|
68 | set_stack_not_a ? localss off RegisterST1. |
---|
69 | |
---|
70 | definition set_stack : |
---|
71 | ∀globals.nat → nat → Register → list (joint_seq LTL globals) ≝ |
---|
72 | λglobals,localss,off,r. |
---|
73 | if eq_Register r RegisterA then |
---|
74 | set_stack_a ? localss off |
---|
75 | else |
---|
76 | set_stack_not_a ? localss off r. |
---|
77 | |
---|
78 | definition set_stack_int : |
---|
79 | ∀globals.nat → nat → Byte → list (joint_seq LTL globals) ≝ |
---|
80 | λglobals,localss,off,int. |
---|
81 | let off ≝ localss + off in |
---|
82 | set_dp_by_offset ? off @ |
---|
83 | [ A ← int |
---|
84 | ; STORE … it it A ]. |
---|
85 | |
---|
86 | definition move : |
---|
87 | ∀globals.nat → bool → decision → arg_decision → list (joint_seq LTL globals) ≝ |
---|
88 | λglobals,localss,carry_lives_after,dst,src. |
---|
89 | match dst with |
---|
90 | [ decision_colour dstr ⇒ |
---|
91 | match src with |
---|
92 | [ arg_decision_colour srcr ⇒ |
---|
93 | if eq_Register dstr srcr then [ ] else |
---|
94 | if eq_Register dstr RegisterA then [ A ← srcr ] else |
---|
95 | if eq_Register srcr RegisterA then [ dstr ← A ] else |
---|
96 | [ A ← srcr ; dstr ← A] |
---|
97 | | arg_decision_spill srco ⇒ |
---|
98 | preserve_carry_bit ? carry_lives_after |
---|
99 | (get_stack ? localss dstr srco) |
---|
100 | | arg_decision_imm int ⇒ |
---|
101 | [ A ← int ] @ |
---|
102 | if eq_Register dstr RegisterA then [ ] else |
---|
103 | [ dstr ← A ] |
---|
104 | ] |
---|
105 | | decision_spill dsto ⇒ |
---|
106 | match src with |
---|
107 | [ arg_decision_colour srcr ⇒ |
---|
108 | preserve_carry_bit ? carry_lives_after |
---|
109 | (set_stack ? localss dsto srcr) |
---|
110 | | arg_decision_spill srco ⇒ |
---|
111 | if eqb srco dsto then [ ] else |
---|
112 | preserve_carry_bit ? carry_lives_after |
---|
113 | (get_stack ? localss RegisterA srco @ |
---|
114 | set_stack ? localss dsto RegisterA) |
---|
115 | | arg_decision_imm int ⇒ |
---|
116 | preserve_carry_bit ? carry_lives_after |
---|
117 | (set_stack_int ? localss dsto int) |
---|
118 | ] |
---|
119 | ]. |
---|
120 | |
---|
121 | definition arg_is_spilled : arg_decision → bool ≝ |
---|
122 | λx.match x with [ arg_decision_spill _ ⇒ true | _ ⇒ false ]. |
---|
123 | definition is_spilled : decision → bool ≝ |
---|
124 | λx.match x with [ decision_spill _ ⇒ true | _ ⇒ false ]. |
---|
125 | |
---|
126 | definition newframe : |
---|
127 | ∀globals.ℕ → list (joint_seq LTL globals) ≝ |
---|
128 | λglobals,stack_sz. |
---|
129 | [ CLEAR_CARRY … |
---|
130 | ; A ← RegisterSPL |
---|
131 | ; A ← A .Sub. byte_of_nat stack_sz |
---|
132 | ; RegisterSPL ← A |
---|
133 | ; A ← RegisterSPH |
---|
134 | ; A ← A .Sub. zero_byte |
---|
135 | ; RegisterSPH ← A |
---|
136 | ]. |
---|
137 | |
---|
138 | definition delframe : |
---|
139 | ∀globals.ℕ → list (joint_seq LTL globals) ≝ |
---|
140 | λglobals,stack_sz. |
---|
141 | [ A ← RegisterSPL |
---|
142 | ; A ← A .Add. byte_of_nat stack_sz |
---|
143 | ; RegisterSPL ← A |
---|
144 | ; A ← RegisterSPH |
---|
145 | ; A ← A .Addc. zero_byte |
---|
146 | ; RegisterSPH ← A |
---|
147 | ]. |
---|
148 | |
---|
149 | definition commutative : Op2 → bool ≝ |
---|
150 | λop.match op with |
---|
151 | [ Add ⇒ true |
---|
152 | | Addc ⇒ true |
---|
153 | | Or ⇒ true |
---|
154 | | Xor ⇒ true |
---|
155 | | And ⇒ true |
---|
156 | | _ ⇒ false |
---|
157 | ]. |
---|
158 | |
---|
159 | definition uses_carry : Op2 → bool ≝ |
---|
160 | λop.match op with |
---|
161 | [ Addc ⇒ true |
---|
162 | | Sub ⇒ true |
---|
163 | | _ ⇒ false |
---|
164 | ]. |
---|
165 | |
---|
166 | definition sets_carry : Op2 → bool ≝ |
---|
167 | λop.match op with |
---|
168 | [ Add ⇒ true |
---|
169 | | Addc ⇒ true |
---|
170 | | Sub ⇒ true |
---|
171 | | _ ⇒ false |
---|
172 | ]. |
---|
173 | |
---|
174 | definition translate_op2 : |
---|
175 | ∀globals.nat → bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ |
---|
176 | λglobals,localss,carry_lives_after,op,dst,arg1,arg2. |
---|
177 | (* this won't preserve the carry bit if op does not set it: left to next function *) |
---|
178 | (* if op uses carry bit (⇒ it sets it too) it must be preserved before the op *) |
---|
179 | (preserve_carry_bit ? |
---|
180 | (uses_carry op ∧ (arg_is_spilled arg1 ∨ arg_is_spilled arg2)) |
---|
181 | (move ? localss false RegisterB arg2 @ |
---|
182 | move ? localss false RegisterA arg1) @ |
---|
183 | [ A ← A .op. RegisterB ] @ |
---|
184 | (* it op sets the carry bit and it is needed afterwards it must be preserved here *) |
---|
185 | move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA). |
---|
186 | |
---|
187 | definition translate_op2_smart : |
---|
188 | ∀globals.nat → bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ |
---|
189 | λglobals,localss,carry_lives_after,op,dst,arg1,arg2. |
---|
190 | (* if op does not set carry bit (⇒ it does not use it either) then it must be |
---|
191 | preserved *) |
---|
192 | preserve_carry_bit ? |
---|
193 | (¬sets_carry op ∧ carry_lives_after ∧ |
---|
194 | (arg_is_spilled arg1 ∨ arg_is_spilled arg2 ∨ is_spilled dst)) |
---|
195 | (match arg2 with |
---|
196 | [ arg_decision_colour arg2r ⇒ |
---|
197 | move ? localss (uses_carry op) RegisterA arg1 @ |
---|
198 | [ A ← A .op. arg2r ] @ |
---|
199 | move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA |
---|
200 | | arg_decision_imm arg2i ⇒ |
---|
201 | move ? localss (uses_carry op) RegisterA arg1 @ |
---|
202 | [ A ← A .op. arg2i ] @ |
---|
203 | move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA |
---|
204 | | _ ⇒ |
---|
205 | if commutative op then |
---|
206 | match arg1 with |
---|
207 | [ arg_decision_colour arg1r ⇒ |
---|
208 | move ? localss (uses_carry op) RegisterA arg2 @ |
---|
209 | [ A ← A .op. arg1r ] @ |
---|
210 | move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA |
---|
211 | | arg_decision_imm arg1i ⇒ |
---|
212 | move ? localss (uses_carry op) RegisterA arg2 @ |
---|
213 | [ A ← A .op. arg1i ] @ |
---|
214 | move ? localss (sets_carry op ∧ carry_lives_after) dst RegisterA |
---|
215 | | _ ⇒ |
---|
216 | translate_op2 ? localss carry_lives_after op dst arg1 arg2 |
---|
217 | ] |
---|
218 | else |
---|
219 | translate_op2 ? localss carry_lives_after op dst arg1 arg2 |
---|
220 | ]). |
---|
221 | |
---|
222 | definition dec_to_arg_dec : decision → arg_decision ≝ |
---|
223 | λd.match d with |
---|
224 | [ decision_colour r ⇒ arg_decision_colour r |
---|
225 | | decision_spill n ⇒ arg_decision_spill n |
---|
226 | ]. |
---|
227 | |
---|
228 | coercion dec_arg_dec : ∀d:decision.arg_decision ≝ dec_to_arg_dec on _d : decision to arg_decision. |
---|
229 | |
---|
230 | definition translate_op1 : |
---|
231 | ∀globals.nat → bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝ |
---|
232 | λglobals,localss,carry_lives_after,op,dst,arg. |
---|
233 | let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in |
---|
234 | preserve_carry_bit ? preserve_carry |
---|
235 | (move ? localss false RegisterA arg @ |
---|
236 | OP1 … op it it :: |
---|
237 | move ? localss false dst RegisterA). |
---|
238 | |
---|
239 | definition translate_opaccs : |
---|
240 | ∀globals.nat → bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ |
---|
241 | λglobals,localss,carry_lives_after,op,dst1,dst2,arg1,arg2. |
---|
242 | (* OPACCS always has dead carry bit and sets it to zero *) |
---|
243 | move ? localss false RegisterB arg2 @ |
---|
244 | move ? localss false RegisterA arg1 @ |
---|
245 | OPACCS … op it it it it :: |
---|
246 | move ? localss false dst1 RegisterA @ |
---|
247 | move ? localss false dst2 RegisterB @ |
---|
248 | if carry_lives_after ∧ (is_spilled dst1 ∨ is_spilled dst2) then |
---|
249 | [CLEAR_CARRY ??] |
---|
250 | else [ ]. |
---|
251 | |
---|
252 | (* does not preserve carry bit *) |
---|
253 | definition move_to_dp : |
---|
254 | ∀globals.nat → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ |
---|
255 | λglobals,localss,arg1,arg2. |
---|
256 | if ¬arg_is_spilled arg1 then |
---|
257 | move ? localss false RegisterDPH arg2 @ |
---|
258 | (* does not change dph because arg1 is not spilled *) |
---|
259 | move ? localss false RegisterDPL arg1 |
---|
260 | else if ¬arg_is_spilled arg2 then |
---|
261 | move ? localss false RegisterDPL arg1 @ |
---|
262 | (* does not change dpl because arg2 is not spilled *) |
---|
263 | move ? localss false RegisterDPH arg2 |
---|
264 | else |
---|
265 | (* using B as temporary, as moving spilled registers tampers with DPTR *) |
---|
266 | move ? localss false RegisterB arg1 @ |
---|
267 | move ? localss false RegisterDPH arg2 @ |
---|
268 | move ? localss false RegisterDPL RegisterB. |
---|
269 | |
---|
270 | definition translate_store : |
---|
271 | ∀globals.nat → bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ |
---|
272 | λglobals,localss,carry_lives_after,addr1,addr2,src. |
---|
273 | (* requires src != RegisterA and RegisterB *) |
---|
274 | preserve_carry_bit ? (carry_lives_after ∧ |
---|
275 | (arg_is_spilled addr1 ∨ arg_is_spilled addr1 ∨ arg_is_spilled src)) |
---|
276 | (let move_to_dptr ≝ move_to_dp ? localss addr1 addr2 in |
---|
277 | (if arg_is_spilled src then |
---|
278 | move ? localss false RegisterST0 src @ |
---|
279 | move_to_dptr @ |
---|
280 | [ A ← RegisterST0] |
---|
281 | else |
---|
282 | move_to_dptr @ |
---|
283 | move ? localss false RegisterA src) @ |
---|
284 | [STORE … it it A]). |
---|
285 | |
---|
286 | definition translate_load : |
---|
287 | ∀globals.nat → bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝ |
---|
288 | λglobals,localss,carry_lives_after,dst,addr1,addr2. |
---|
289 | preserve_carry_bit ? (carry_lives_after ∧ |
---|
290 | (is_spilled dst ∨ arg_is_spilled addr1 ∨ arg_is_spilled addr1)) |
---|
291 | (move_to_dp ? localss addr1 addr2 @ |
---|
292 | [ LOAD … A it it ] @ |
---|
293 | move ? localss false dst RegisterA). |
---|
294 | |
---|
295 | definition translate_address : |
---|
296 | ∀globals.nat → bool → ∀i.i ∈ globals → Word → decision → decision → |
---|
297 | list (joint_seq LTL globals) ≝ |
---|
298 | λglobals,localss,carry_lives_after,id,prf,off,addr1,addr2. |
---|
299 | preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2)) |
---|
300 | (ADDRESS LTL ? id prf off it it :: |
---|
301 | move ? localss false addr1 RegisterDPL @ |
---|
302 | move ? localss false addr2 RegisterDPH). |
---|
303 | |
---|
304 | definition translate_step: |
---|
305 | ∀globals,fn.nat → ∀after : valuation register_lattice. |
---|
306 | coloured_graph (interferes globals fn after) → |
---|
307 | ℕ → label → joint_step ERTL globals → bind_step_block LTL globals ≝ |
---|
308 | λglobals,fn,localss,after,grph,stack_sz,lbl,s. |
---|
309 | bret … ( |
---|
310 | let lookup ≝ λr.colouring … grph (inl … r) in |
---|
311 | let lookup_arg ≝ λa.match a with |
---|
312 | [ Reg r ⇒ lookup r |
---|
313 | | Imm b ⇒ arg_decision_imm b |
---|
314 | ] in |
---|
315 | let carry_lives_after ≝ h_in_lattice RegisterCarry (after lbl) in |
---|
316 | let move ≝ move globals localss carry_lives_after in |
---|
317 | if eliminable_step … (after lbl) s then ([ ] : step_block LTL globals) else |
---|
318 | match s with |
---|
319 | [ step_seq s' ⇒ |
---|
320 | match s' return λ_.step_block LTL globals with |
---|
321 | [ COMMENT c ⇒ [COMMENT … c] |
---|
322 | | POP r ⇒ |
---|
323 | POP … A :: |
---|
324 | move (lookup r) RegisterA |
---|
325 | | PUSH a ⇒ |
---|
326 | move RegisterA (lookup_arg a) @ |
---|
327 | [ PUSH … A ] |
---|
328 | | STORE addr1 addr2 srcr ⇒ |
---|
329 | translate_store ? localss carry_lives_after |
---|
330 | (lookup_arg addr1) |
---|
331 | (lookup_arg addr2) |
---|
332 | (lookup_arg srcr) |
---|
333 | | LOAD dstr addr1 addr2 ⇒ |
---|
334 | translate_load ? localss carry_lives_after |
---|
335 | (lookup dstr) |
---|
336 | (lookup_arg addr1) |
---|
337 | (lookup_arg addr2) |
---|
338 | | CLEAR_CARRY ⇒ [CLEAR_CARRY ??] |
---|
339 | | SET_CARRY ⇒ [SET_CARRY ??] |
---|
340 | | OP2 op dst arg1 arg2 ⇒ |
---|
341 | translate_op2_smart ? localss carry_lives_after op |
---|
342 | (lookup dst) |
---|
343 | (lookup_arg arg1) |
---|
344 | (lookup_arg arg2) |
---|
345 | | OP1 op dst arg ⇒ |
---|
346 | translate_op1 ? localss carry_lives_after op |
---|
347 | (lookup dst) |
---|
348 | (lookup arg) |
---|
349 | | MOVE pair_regs ⇒ |
---|
350 | let lookup_move_dst ≝ λx.match x return λ_.decision with |
---|
351 | [ PSD r ⇒ lookup r |
---|
352 | | HDW r ⇒ r |
---|
353 | ] in |
---|
354 | let dst ≝ lookup_move_dst (\fst pair_regs) in |
---|
355 | let src ≝ |
---|
356 | match \snd pair_regs return λ_.arg_decision with |
---|
357 | [ Reg r ⇒ lookup_move_dst r |
---|
358 | | Imm b ⇒ arg_decision_imm b |
---|
359 | ] in |
---|
360 | move dst src |
---|
361 | | ADDRESS lbl prf off dpl dph ⇒ |
---|
362 | translate_address ? localss carry_lives_after |
---|
363 | lbl prf off (lookup dpl) (lookup dph) |
---|
364 | | OPACCS op dst1 dst2 arg1 arg2 ⇒ |
---|
365 | translate_opaccs ? localss carry_lives_after op |
---|
366 | (lookup dst1) (lookup dst2) |
---|
367 | (lookup_arg arg1) (lookup_arg arg2) |
---|
368 | | extension_seq ext ⇒ |
---|
369 | match ext with |
---|
370 | [ ertl_frame_size r ⇒ |
---|
371 | move (lookup r) (arg_decision_imm (byte_of_nat stack_sz)) |
---|
372 | ] |
---|
373 | ] |
---|
374 | | COST_LABEL cost_lbl ⇒ 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉 |
---|
375 | | COND r ltrue ⇒ |
---|
376 | 〈add_dummy_variance … (move RegisterA (lookup r)),λ_.COND … it ltrue, [ ]〉 |
---|
377 | | CALL f n_args _ ⇒ |
---|
378 | match f with |
---|
379 | [ inl f ⇒ |
---|
380 | 〈[ ],λ_.CALL LTL ? (inl … f) n_args it, [ ]〉 |
---|
381 | | inr dp ⇒ |
---|
382 | let 〈dpl, dph〉 ≝ dp in |
---|
383 | 〈add_dummy_variance … (move_to_dp ? localss (lookup_arg dpl) (lookup_arg dph)) @ |
---|
384 | [λl.(LOW_ADDRESS l : joint_seq ??); |
---|
385 | λ_.PUSH LTL ? it; |
---|
386 | λl.HIGH_ADDRESS l; |
---|
387 | λ_.PUSH LTL ? it ; |
---|
388 | (* necessary as ptr CALL will be JMP A+DPTR *) |
---|
389 | λ_.A ← zero_byte ], |
---|
390 | λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉 |
---|
391 | ] |
---|
392 | ]). |
---|
393 | |
---|
394 | definition translate_fin_step: |
---|
395 | ∀globals.ℕ → label → joint_fin_step ERTL → bind_fin_block LTL globals ≝ |
---|
396 | λglobals,stack_sz,lbl,s. |
---|
397 | bret … (match s with |
---|
398 | [ RETURN ⇒ 〈delframe ? stack_sz, RETURN ?〉 |
---|
399 | | GOTO l ⇒ 〈[ ], GOTO ? l〉 |
---|
400 | | TAILCALL abs _ _ ⇒ Ⓧabs |
---|
401 | ]). |
---|
402 | |
---|
403 | definition translate_data : |
---|
404 | fixpoint_computer → coloured_graph_computer → |
---|
405 | ∀globals. |
---|
406 | joint_closed_internal_function ERTL globals → |
---|
407 | bind_new register (b_graph_translate_data ERTL LTL globals) ≝ |
---|
408 | λthe_fixpoint,build,globals,int_fun. |
---|
409 | (* colour registers *) |
---|
410 | let after ≝ analyse_liveness the_fixpoint globals int_fun in |
---|
411 | let coloured_graph ≝ build … int_fun after in |
---|
412 | (* compute new stack size *) |
---|
413 | let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in |
---|
414 | bret … |
---|
415 | (mk_b_graph_translate_data ERTL LTL globals |
---|
416 | (* init_ret ≝ *) it |
---|
417 | (* init_params ≝ *) it |
---|
418 | (* init_stack_size ≝ *) stack_sz |
---|
419 | (* added_prologue ≝ *) (newframe ? stack_sz) |
---|
420 | (* new_regs ≝ *) [ ] |
---|
421 | (* f_step ≝ *) (translate_step ? int_fun (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz) |
---|
422 | (* f_fin ≝ *) (translate_fin_step globals stack_sz) |
---|
423 | ????). |
---|
424 | @hide_prf |
---|
425 | [ |
---|
426 | | #l #c % ] |
---|
427 | cases daemon (* TODO *) |
---|
428 | qed. |
---|
429 | |
---|
430 | (* Paolo: does it really have sense to do here the first stack address computation, |
---|
431 | when it is an info easily available from any program in the back end? |
---|
432 | Also, is it really 2^16 - |globals|, or should there also be a -1? *) |
---|
433 | definition ertl_to_ltl: |
---|
434 | fixpoint_computer → coloured_graph_computer → ertl_program → |
---|
435 | ltl_program × stack_cost_model × nat ≝ |
---|
436 | λthe_fixpoint,build,pr. |
---|
437 | let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in |
---|
438 | 〈ltlprog, stack_cost … ltlprog, 2^16 - globals_stacksize … ltlprog〉. |
---|
439 | % |
---|
440 | qed. |
---|
441 | |
---|
442 | lemma ERTLToLTL_monotone_stacksizes : |
---|
443 | ∀fix,col. |
---|
444 | ∀p_in. |
---|
445 | let cost_m ≝ \snd (\fst (ertl_to_ltl fix col p_in)) in |
---|
446 | stack_cost_model_le (stack_cost ? p_in) cost_m. |
---|
447 | #fix #col #p_in whd |
---|
448 | @list_map_opt_All2 |
---|
449 | [ @(λid_def1,id_def2. |
---|
450 | match \snd id_def1 with |
---|
451 | [ Internal f1 ⇒ |
---|
452 | match \snd id_def2 with |
---|
453 | [ Internal f2 ⇒ |
---|
454 | \fst id_def1 = \fst id_def2 ∧ |
---|
455 | le (joint_if_stacksize … f1) (joint_if_stacksize … f2) |
---|
456 | | _ ⇒ False |
---|
457 | ] |
---|
458 | | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ] |
---|
459 | ]) |
---|
460 | | * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %] |
---|
461 | ** #H %{H} % ] |
---|
462 | @All2_of_map * #id * #f normalize nodelta [2: %] |
---|
463 | % [%] |
---|
464 | cases (b_graph_translate ?????) #f_out * #data ** |
---|
465 | [2: #hd #tl ] * #f_lbls * #f_regs * [*] whd in ⊢ (%→?); #EQ_data |
---|
466 | #props >(ss_def_out_eq … props) >EQ_data |
---|
467 | generalize in match (joint_if_stacksize ???); generalize in match (spilled_no ??); |
---|
468 | -p_in // |
---|
469 | qed. |
---|
470 | |
---|