source: src/ERTL/ERTLToLTL.ma @ 3263

Last change on this file since 3263 was 3263, checked in by tranquil, 6 years ago

moved callee saved saving and restoring to ERTL -> LTL pass (untrusted
colourer and interference graph creator still need to be updated)
joint now has the stack size split in three (referenced locals, params
and spilled)

File size: 16.7 KB
Line 
1include "LTL/LTL.ma".
2include "ERTL/Interference.ma".
3include "ASM/Arithmetic.ma".
4include "joint/TranslateUtils.ma".
5include "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
12coercion Reg_to_dec : ∀r:Register.decision ≝ decision_colour on _r : Register to decision.
13
14inductive 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
19coercion 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
26definition 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 *)
32definition A ≝ it.
33
34coercion beval_of_byte : ∀b : Byte.beval ≝ BVByte on _b : Byte to beval.
35
36(* spill should be byte-based from the start *)
37definition 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
48definition 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
56definition 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
64definition 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
70definition 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 
78definition 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
86definition 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
121definition arg_is_spilled : arg_decision → bool ≝
122  λx.match x with [ arg_decision_spill _ ⇒ true | _ ⇒ false ].
123definition is_spilled : decision → bool ≝
124  λx.match x with [ decision_spill _ ⇒ true | _ ⇒ false ].
125
126definition 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
138definition 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
149definition 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
159definition uses_carry : Op2 → bool ≝
160λop.match op with
161[ Addc ⇒ true
162| Sub ⇒ true
163| _ ⇒ false
164].
165
166definition sets_carry : Op2 → bool ≝
167λop.match op with
168[ Add ⇒ true
169| Addc ⇒ true
170| Sub ⇒ true
171| _ ⇒ false
172].
173
174definition 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
187definition 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
222definition 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
228coercion dec_arg_dec : ∀d:decision.arg_decision ≝ dec_to_arg_dec on _d : decision to arg_decision.
229
230definition 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
239definition 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 *)
253definition 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
270definition 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
286definition 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
295definition 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
304definition 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
394definition translate_fin_step:
395  ∀globals.list (joint_seq LTL globals) →
396  label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
397  λglobals,epilogue,lbl,s.
398  bret … (match s with
399  [ RETURN ⇒ 〈epilogue, RETURN ?〉
400  | GOTO l ⇒ 〈[ ], GOTO ? l〉
401  | TAILCALL abs _ _ ⇒ Ⓧabs
402  ]).
403
404definition translate_data :
405 fixpoint_computer → coloured_graph_computer →
406 ∀globals.
407  joint_closed_internal_function ERTL globals →
408  bind_new register (b_graph_translate_data ERTL LTL globals) ≝
409λthe_fixpoint,build,globals,int_fun.
410νν |RegisterCalleeSaved| as callee_saved_store in
411(* colour registers *)
412let after ≝ analyse_liveness the_fixpoint globals int_fun callee_saved_store in
413let coloured_graph ≝ build … int_fun after callee_saved_store in
414let callee_saved_pairs ≝ zip_pottier … RegisterCalleeSaved callee_saved_store in
415let localss ≝ joint_if_local_stacksize ?? int_fun in
416let save ≝ \fold[append ?, nil ?]_{R_r ∈ callee_saved_pairs}
417  (move ? localss false
418    (colouring … coloured_graph (inl … (\snd R_r)))
419    (decision_colour (\fst R_r))) in
420let restore ≝ \fold[append ?, nil ?]_{R_r ∈ callee_saved_pairs}
421  (move ? localss false
422    (decision_colour (\fst R_r))
423    (colouring … coloured_graph (inl … (\snd R_r)))) in
424let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
425bret …
426  (mk_b_graph_translate_data ERTL LTL globals
427    (* init_ret ≝ *) it
428    (* init_params ≝ *) it
429    (* added_local_stacksize ≝ *) 0
430    (* added_params_stacksize ≝ *) 0
431    (* added_spilled_stacksize ≝ *) (spilled_no … coloured_graph)
432    (* added_prologue ≝ *) (newframe ? stack_sz @ save)
433    (* new_regs ≝ *) callee_saved_store
434    (* f_step ≝ *) (translate_step ? int_fun localss … coloured_graph stack_sz)
435    (* f_fin ≝ *) (translate_fin_step globals (restore @ delframe ? stack_sz))
436    ????).
437@hide_prf
438[3: #l #c % ]
439cases daemon (* TODO *)
440qed.
441
442(* Paolo: does it really have sense to do here the first stack address computation,
443   when it is an info easily available from any program in the back end?
444   Also, is it really 2^16 - |globals|, or should there also be a -1? *)
445definition ertl_to_ltl:
446 fixpoint_computer → coloured_graph_computer → ertl_program →
447  ltl_program × stack_cost_model × nat ≝
448  λthe_fixpoint,build,pr.
449   let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in
450   〈ltlprog, stack_cost … ltlprog, 2^16 - globals_stacksize … ltlprog〉.
451#r0 #r1 #r2 #r3 #r4 #r5 #r6 #r7 %
452qed.
453
454lemma ERTLToLTL_monotone_stacksizes :
455∀fix,col.
456∀p_in.
457let cost_m ≝ \snd (\fst (ertl_to_ltl fix col p_in)) in
458stack_cost_model_le (stack_cost ? p_in) cost_m ≝
459λfix,col.joint_transform_monotone_stacksizes ….
Note: See TracBrowser for help on using the repository browser.