source: src/ERTLptr/ERTLptrToLTL.ma @ 2694

Last change on this file since 2694 was 2694, checked in by tranquil, 8 years ago

completed ERTLptrToLTL

File size: 15.0 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.Register → nat → list (joint_seq LTL globals) ≝
49 λglobals,r,off.
50 set_dp_by_offset ? off @
51 [ LOAD … A it it ] @
52 if eq_Register r RegisterA then [ ] else [ r ← A ].
53
54definition set_stack_not_a :
55 ∀globals.nat → Register → list (joint_seq LTL globals) ≝
56 λglobals,off,r.
57 set_dp_by_offset ? off @
58 [ A ← r
59 ; STORE … it it A ].
60
61definition set_stack_a :
62 ∀globals.nat → list (joint_seq LTL globals) ≝
63 λglobals,off.
64 [ RegisterST1 ← A ] @
65 set_stack_not_a ? off RegisterST1.
66
67definition set_stack :
68 ∀globals.nat → Register → list (joint_seq LTL globals) ≝
69 λglobals,off,r.
70 if eq_Register r RegisterA then
71   set_stack_a ? off
72 else
73   set_stack_not_a ? off r.
74 
75definition set_stack_int :
76  ∀globals.nat → Byte →  list (joint_seq LTL globals) ≝
77  λglobals,off,int.
78  set_dp_by_offset ? off @
79  [ A ← int
80  ; STORE … it it A ].
81
82definition move :
83  ∀globals.bool → decision → arg_decision → list (joint_seq LTL globals) ≝
84  λglobals,carry_lives_after,dst,src.
85  match dst with
86  [ decision_colour dstr ⇒
87    match src with
88    [ arg_decision_colour srcr ⇒
89      if eq_Register dstr srcr then [ ] else
90      if eq_Register dstr RegisterA then [ A ← srcr ] else
91      if eq_Register srcr RegisterA then [ dstr ← A ] else
92      [ A ← srcr ; dstr ← A]
93    | arg_decision_spill srco ⇒
94      preserve_carry_bit ? carry_lives_after
95        (get_stack ? dstr srco)
96    | arg_decision_imm int ⇒
97      [ A ← int ] @
98      if eq_Register dstr RegisterA then [ ] else
99      [ dstr ← A ]
100    ]
101  | decision_spill dsto ⇒
102    match src with
103    [ arg_decision_colour srcr ⇒
104      preserve_carry_bit ? carry_lives_after
105        (set_stack ? dsto srcr)
106    | arg_decision_spill srco ⇒
107      if eqb srco dsto then [ ] else
108      preserve_carry_bit ? carry_lives_after
109        (get_stack ? RegisterA srco @
110         set_stack ? dsto RegisterA)
111    | arg_decision_imm int ⇒
112      preserve_carry_bit ? carry_lives_after
113        (set_stack_int ? dsto int)
114    ]
115  ].
116
117definition arg_is_spilled : arg_decision → bool ≝
118  λx.match x with [ arg_decision_spill _ ⇒ true | _ ⇒ false ].
119definition is_spilled : decision → bool ≝
120  λx.match x with [ decision_spill _ ⇒ true | _ ⇒ false ].
121
122definition newframe :
123  ∀globals.ℕ → list (joint_seq LTL globals) ≝
124  λglobals,stack_sz.
125  [ CLEAR_CARRY …
126  ; A ← RegisterSPL
127  ; A ← A .Sub. byte_of_nat stack_sz
128  ; RegisterSPL ← A
129  ; A ← RegisterSPH
130  ; A ← A .Sub. zero_byte
131  ; RegisterSPH ← A
132  ].
133
134definition delframe :
135  ∀globals.ℕ → list (joint_seq LTL globals) ≝
136  λglobals,stack_sz.
137  [ A ← RegisterSPL
138  ; A ← A .Add. byte_of_nat stack_sz
139  ; RegisterSPL ← A
140  ; A ← RegisterSPH
141  ; A ← A .Addc. zero_byte
142  ; RegisterSPH ← A
143  ].
144
145definition commutative : Op2 → bool ≝
146λop.match op with
147[ Add ⇒ true
148| Addc ⇒ true
149| Or ⇒ true
150| Xor ⇒ true
151| And ⇒ true
152| _ ⇒ false
153].
154
155definition uses_carry : Op2 → bool ≝
156λop.match op with
157[ Addc ⇒ true
158| Sub ⇒ true
159| _ ⇒ false
160].
161
162definition sets_carry : Op2 → bool ≝
163λop.match op with
164[ Add ⇒ true
165| Addc ⇒ true
166| Sub ⇒ true
167| _ ⇒ false
168].
169
170definition translate_op2 :
171  ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
172  λglobals,carry_lives_after,op,dst,arg1,arg2.
173  (* this won't preserve the carry bit if op does not set it: left to next function *)
174  (* if op uses carry bit (⇒ it sets it too) it must be preserved before the op *)
175  (preserve_carry_bit ?
176    (uses_carry op ∧ (arg_is_spilled arg1 ∨ arg_is_spilled arg2))
177    (move ? false RegisterB arg2 @
178     move ? false RegisterA arg1) @
179    [ A ← A .op. RegisterB ] @
180    (* it op sets the carry bit and it is needed afterwards it must be preserved here *)
181    move ? (sets_carry op ∧ carry_lives_after) dst RegisterA).
182
183definition translate_op2_smart :
184  ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
185  λglobals,carry_lives_after,op,dst,arg1,arg2.
186  (* if op does not set carry bit (⇒ it does not use it either) then it must be
187    preserved *)
188  preserve_carry_bit ?
189    (¬sets_carry op ∧ carry_lives_after ∧
190      (arg_is_spilled arg1 ∨ arg_is_spilled arg2 ∨ is_spilled dst))
191    (match arg2 with
192    [ arg_decision_colour arg2r ⇒
193      move ? (uses_carry op) RegisterA arg1 @
194      [ A ← A .op. arg2r ] @
195      move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
196    | arg_decision_imm arg2i ⇒
197      move ? (uses_carry op) RegisterA arg1 @
198      [ A ← A .op. arg2i ] @
199      move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
200    | _ ⇒
201      if commutative op then
202        match arg1 with
203        [ arg_decision_colour arg1r ⇒
204          move ? (uses_carry op) RegisterA arg2 @
205          [ A ← A .op. arg1r ] @
206          move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
207        | arg_decision_imm arg1i ⇒
208          move ? (uses_carry op) RegisterA arg2 @
209          [ A ← A .op. arg1i ] @
210          move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
211        | _ ⇒
212          translate_op2 ? carry_lives_after op dst arg1 arg2
213        ]
214      else
215        translate_op2 ? carry_lives_after op dst arg1 arg2
216    ]).
217
218definition dec_to_arg_dec : decision → arg_decision ≝
219  λd.match d with
220  [ decision_colour r ⇒ arg_decision_colour r
221  | decision_spill n ⇒ arg_decision_spill n
222  ].
223
224coercion dec_arg_dec : ∀d:decision.arg_decision ≝ dec_to_arg_dec on _d : decision to arg_decision.
225
226definition translate_op1 :
227  ∀globals.bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝
228  λglobals,carry_lives_after,op,dst,arg.
229  let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in
230  preserve_carry_bit ? preserve_carry
231    (move ? false RegisterA arg @
232     OP1 … op it it ::
233     move ? false dst RegisterA).
234
235definition translate_opaccs :
236  ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
237  λglobals,carry_lives_after,op,dst1,dst2,arg1,arg2.
238  (* OPACCS always has dead carry bit and sets it to zero *)
239  move ? false RegisterB arg2 @
240  move ? false RegisterA arg1 @
241  OPACCS … op it it it it ::
242  move ? false dst1 RegisterA @
243  move ? false dst2 RegisterB @
244  if carry_lives_after ∧ (is_spilled dst1 ∨ is_spilled dst2) then
245    [CLEAR_CARRY ??]
246  else [ ].
247
248(* does not preserve carry bit *)
249definition move_to_dp :
250  ∀globals.arg_decision → arg_decision → list (joint_seq LTL globals) ≝
251  λglobals,arg1,arg2.
252  if ¬arg_is_spilled arg1 then
253    move ? false RegisterDPH arg2 @
254    (* does not change dph because arg1 is not spilled *)
255    move ? false RegisterDPL arg1
256  else if ¬arg_is_spilled arg2 then
257    move ? false RegisterDPL arg1 @
258    (* does not change dpl because arg2 is not spilled *)
259    move ? false RegisterDPH arg2
260  else
261    (* using B as temporary, as moving spilled registers tampers with DPTR *)
262    move ? false RegisterB arg1 @
263    move ? false RegisterDPH arg2 @
264    move ? false RegisterDPL RegisterB.
265
266definition translate_store : 
267  ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
268  λglobals,carry_lives_after,addr1,addr2,src.
269  (* requires src != RegisterA and RegisterB *)
270  preserve_carry_bit ? (carry_lives_after ∧
271    (arg_is_spilled addr1 ∨ arg_is_spilled addr1 ∨ arg_is_spilled src))
272    (let move_to_dptr ≝ move_to_dp ? addr1 addr2 in
273     (if arg_is_spilled src then
274        move ? false RegisterST0 src @
275        move_to_dptr @
276        [ A ← RegisterST0]
277      else move_to_dptr) @
278     [STORE … it it A]).
279
280definition translate_load : 
281  ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
282  λglobals,carry_lives_after,dst,addr1,addr2.
283  preserve_carry_bit ? (carry_lives_after ∧
284    (is_spilled dst ∨ arg_is_spilled addr1 ∨ arg_is_spilled addr1))
285    (move_to_dp ? addr1 addr2 @
286     [ LOAD … A it it ] @
287     move ? false dst RegisterA).
288
289definition translate_address :
290  ∀globals.bool → ∀i.i ∈ globals → decision → decision →
291  list (joint_seq LTL globals) ≝
292  λglobals,carry_lives_after,id,prf,addr1,addr2.
293  preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2))
294    (ADDRESS LTL ? id prf it it ::
295     move ? false addr1 RegisterDPL @
296     move ? false addr2 RegisterDPH).
297
298definition translate_low_address :
299  ∀globals.bool → decision → label →
300  list (joint_seq LTL globals) ≝
301  λglobals,carry_lives_after,dst,lbl.
302  match dst return λ_.list (joint_seq LTL globals) with
303  [ decision_colour r ⇒ [LOW_ADDRESS r lbl]
304  | _ ⇒
305    LOW_ADDRESS RegisterA lbl :: move ? carry_lives_after dst RegisterA
306  ].
307
308definition translate_high_address :
309  ∀globals.bool → decision → label →
310  list (joint_seq LTL globals) ≝
311  λglobals,carry_lives_after,dst,lbl.
312  match dst return λ_.list (joint_seq LTL globals) with
313  [ decision_colour r ⇒ [HIGH_ADDRESS r lbl]
314  | _ ⇒
315    HIGH_ADDRESS RegisterA lbl :: move ? carry_lives_after dst RegisterA
316  ].
317
318definition translate_step:
319  ∀globals.∀after : valuation register_lattice.
320  coloured_graph after →
321  ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝
322  λglobals,after,grph,stack_sz,lbl,s.
323  bret … (
324  let lookup ≝ λr.colouring … grph (inl … r) in
325  let lookup_arg ≝ λa.match a with
326    [ Reg r ⇒ lookup r
327    | Imm b ⇒ arg_decision_imm b
328    ] in
329  let carry_lives_after ≝ hlives RegisterCarry (after lbl) in
330  let move ≝ move globals carry_lives_after in
331  match s with
332  [ step_seq s' ⇒
333    match s' return λ_.step_block LTL globals with
334    [ COMMENT c ⇒ [COMMENT … c]
335    | POP r ⇒
336      POP … A ::
337      move (lookup r) RegisterA
338    | PUSH a ⇒
339      move RegisterA (lookup_arg a) @
340      [ PUSH … A ]
341    | STORE addr1 addr2 srcr ⇒
342      translate_store ? carry_lives_after
343        (lookup_arg addr1)
344        (lookup_arg addr2)
345        (lookup_arg srcr)
346    | LOAD dstr addr1 addr2 ⇒
347      translate_load ? carry_lives_after
348        (lookup dstr)
349        (lookup_arg addr1)
350        (lookup_arg addr2)
351    | CLEAR_CARRY ⇒ [CLEAR_CARRY ??]
352    | SET_CARRY ⇒ [CLEAR_CARRY ??]
353    | OP2 op dst arg1 arg2 ⇒
354      translate_op2_smart ? carry_lives_after op
355        (lookup dst)
356        (lookup_arg arg1)
357        (lookup_arg arg2)
358    | OP1 op dst arg ⇒
359      translate_op1 ? carry_lives_after op
360        (lookup dst)
361        (lookup arg)
362    | MOVE pair_regs ⇒
363      let lookup_move_dst ≝ λx.match x return λ_.decision with
364        [ PSD r ⇒ lookup r
365        | HDW r ⇒ r
366        ] in
367      let dst ≝ lookup_move_dst (\fst pair_regs) in
368      let src ≝
369        match \snd pair_regs return λ_.arg_decision with
370        [ Reg r ⇒ lookup_move_dst r
371        | Imm b ⇒ arg_decision_imm b
372        ] in
373      move dst src
374    | ADDRESS lbl prf dpl dph ⇒
375      translate_address ? carry_lives_after
376        lbl prf (lookup dpl) (lookup dph)
377    | OPACCS op dst1 dst2 arg1 arg2 ⇒
378      translate_opaccs ? carry_lives_after op
379        (lookup dst1) (lookup dst2)
380        (lookup_arg arg1) (lookup_arg arg2)
381    | extension_seq ext ⇒
382      match ext with
383        [ ertlptr_ertl ext' ⇒
384          match ext' with
385          [ ertl_new_frame ⇒ newframe ? stack_sz
386          | ertl_del_frame ⇒ delframe ? stack_sz
387          | ertl_frame_size r ⇒
388            move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
389          ]
390        | LOW_ADDRESS r1 l ⇒
391           translate_low_address ? carry_lives_after (lookup r1) l
392        | HIGH_ADDRESS r1 l ⇒
393           translate_high_address ? carry_lives_after (lookup r1) l       
394        ]
395    ]
396  | COST_LABEL cost_lbl ⇒ 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉
397  | COND r ltrue ⇒
398    〈add_dummy_variance … (move RegisterA (lookup r)),λ_.COND … it ltrue, [ ]〉
399  | CALL f n_args _ ⇒
400      match f with
401      [ inl f ⇒
402        〈[ ],λ_.CALL LTL ? (inl … f) n_args it, [ ]〉
403      | inr dp ⇒
404        let 〈dpl, dph〉 ≝ dp in
405        〈add_dummy_variance … (move_to_dp … (lookup_arg dpl) (lookup_arg dph)),
406         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
407      ]
408  ]).
409
410definition translate_fin_step:
411  ∀globals.label → joint_fin_step ERTLptr → bind_fin_block LTL globals ≝
412  λglobals,lbl,s.
413  bret … (〈[ ],
414  match s with
415  [ RETURN ⇒ RETURN ?
416  | GOTO l ⇒ GOTO ? l
417  | TAILCALL abs _ _ ⇒ Ⓧabs
418  ]〉).
419
420definition translate_data : ∀globals.
421  joint_closed_internal_function ERTLptr globals →
422  bind_new register (b_graph_translate_data ERTLptr LTL globals) ≝
423λglobals,int_fun.
424(* colour registers *)
425let after ≝ analyse_liveness globals int_fun in
426let coloured_graph ≝ build after in
427(* compute new stack size *)
428let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
429bret …
430  (mk_b_graph_translate_data ERTLptr LTL globals
431    (* init_ret ≝ *) it
432    (* init_params ≝ *) it
433    (* init_stack_size ≝ *) stack_sz
434    (* added_prologue ≝ *) [ ]
435    (* f_step ≝ *) (translate_step … coloured_graph stack_sz)
436    (* f_fin ≝ *) (translate_fin_step globals)
437    ???).
438@hide_prf
439[ #l #c % ]
440cases daemon (* TODO *)
441qed.
442
443definition ertl_to_ltl: ertlptr_program → ltl_program ≝
444  b_graph_transform_program … translate_data.
Note: See TracBrowser for help on using the repository browser.