source: src/ERTLptr/ERTLptrToLTL.ma @ 2818

Last change on this file since 2818 was 2818, checked in by sacerdot, 8 years ago

"Repaired", using non computational daemons.

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