source: src/ERTLptr/ERTLptrToLTL.ma @ 2796

Last change on this file since 2796 was 2774, checked in by sacerdot, 8 years ago
  1. the compiler now outputs both the stack cost model and the max stack available
  2. hypothesis on initial status not failing removed from correctness.ma by using the low level definition
File size: 15.6 KB
RevLine 
[1084]1include "LTL/LTL.ma".
[2693]2include "ERTLptr/Interference.ma".
[1154]3include "ASM/Arithmetic.ma".
[2286]4include "joint/TranslateUtils.ma".
[1154]5
[2286]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.*)
[1160]10
[2286]11coercion Reg_to_dec : ∀r:Register.decision ≝ decision_colour on _r : Register to decision.
[1232]12
[2286]13inductive arg_decision : Type[0] ≝
14  | arg_decision_colour : Register → arg_decision
15  | arg_decision_spill : ℕ → arg_decision
[2490]16  | arg_decision_imm : Byte → arg_decision.
[1160]17
[2286]18coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision.
[1160]19
[2286]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 *)
[1154]24
[2286]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.
[1154]29
[2286]30(* for notation *)
31definition A ≝ it.
[1154]32
[2286]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
[1168]47definition get_stack:
[2286]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 ].
[1154]53
[2286]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 ].
[1154]60
[2286]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.
[1260]66
[2286]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 :
[2490]76  ∀globals.nat → Byte →  list (joint_seq LTL globals) ≝
[2286]77  λglobals,off,int.
78  set_dp_by_offset ? off @
79  [ A ← int
80  ; STORE … it it A ].
[1154]81
[2286]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 ⇒
[1154]87    match src with
[2286]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 ]
[1154]100    ]
[2286]101  | decision_spill dsto ⇒
[1154]102    match src with
[2286]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)
[1154]114    ]
115  ].
116
[2286]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 ].
[1154]121
[2286]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
[2443]131  ; RegisterSPH ← A
[2286]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
[2443]142  ; RegisterSPH ← A
[2286]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
[1154]260  else
[2286]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.
[1154]265
[2286]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 :
[2681]290  ∀globals.bool → ∀i.i ∈ globals → decision → decision →
[2286]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
[2694]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
[2286]318definition translate_step:
319  ∀globals.∀after : valuation register_lattice.
320  coloured_graph after →
[2693]321  ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝
[2286]322  λglobals,after,grph,stack_sz,lbl,s.
[2681]323  bret … (
[2286]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' ⇒
[2681]333    match s' return λ_.step_block LTL globals with
334    [ COMMENT c ⇒ [COMMENT … c]
[1282]335    | POP r ⇒
[2286]336      POP … A ::
337      move (lookup r) RegisterA
338    | PUSH a ⇒
339      move RegisterA (lookup_arg a) @
340      [ PUSH … A ]
[1282]341    | STORE addr1 addr2 srcr ⇒
[2286]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)
[2681]351    | CLEAR_CARRY ⇒ [CLEAR_CARRY ??]
352    | SET_CARRY ⇒ [CLEAR_CARRY ??]
[2286]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)
[1282]362    | MOVE pair_regs ⇒
[2286]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
[1282]374    | ADDRESS lbl prf dpl dph ⇒
[2286]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 ⇒
[1250]382      match ext with
[2693]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 ⇒
[2694]391           translate_low_address ? carry_lives_after (lookup r1) l
[2693]392        | HIGH_ADDRESS r1 l ⇒
[2694]393           translate_high_address ? carry_lives_after (lookup r1) l       
[2693]394        ]
[2681]395    ]
[2689]396  | COST_LABEL cost_lbl ⇒ 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉
[2681]397  | COND r ltrue ⇒
398    〈add_dummy_variance … (move RegisterA (lookup r)),λ_.COND … it ltrue, [ ]〉
399  | CALL f n_args _ ⇒
[2490]400      match f with
[2681]401      [ inl f ⇒
402        〈[ ],λ_.CALL LTL ? (inl … f) n_args it, [ ]〉
[2490]403      | inr dp ⇒
404        let 〈dpl, dph〉 ≝ dp in
[2681]405        〈add_dummy_variance … (move_to_dp … (lookup_arg dpl) (lookup_arg dph)),
406         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
[2490]407      ]
[2681]408  ]).
[1154]409
[2286]410definition translate_fin_step:
[2693]411  ∀globals.label → joint_fin_step ERTLptr → bind_fin_block LTL globals ≝
[2286]412  λglobals,lbl,s.
[2681]413  bret … (〈[ ],
414  match s with
[2286]415  [ RETURN ⇒ RETURN ?
416  | GOTO l ⇒ GOTO ? l
[2490]417  | TAILCALL abs _ _ ⇒ Ⓧabs
[2681]418  ]〉).
[1271]419
[2700]420definition translate_data :
421 fixpoint_computer → coloured_graph_computer →
422 ∀globals.
[2693]423  joint_closed_internal_function ERTLptr globals →
424  bind_new register (b_graph_translate_data ERTLptr LTL globals) ≝
[2700]425λthe_fixpoint,build,globals,int_fun.
[2681]426(* colour registers *)
[2700]427let after ≝ analyse_liveness the_fixpoint globals int_fun in
[2739]428let coloured_graph ≝ build … int_fun after in
[2681]429(* compute new stack size *)
430let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
431bret …
[2693]432  (mk_b_graph_translate_data ERTLptr LTL globals
[2681]433    (* init_ret ≝ *) it
434    (* init_params ≝ *) it
435    (* init_stack_size ≝ *) stack_sz
436    (* added_prologue ≝ *) [ ]
437    (* f_step ≝ *) (translate_step … coloured_graph stack_sz)
438    (* f_fin ≝ *) (translate_fin_step globals)
439    ???).
440@hide_prf
441[ #l #c % ]
442cases daemon (* TODO *)
443qed.
[1084]444
[2774]445definition first_free_stack_addr : ltl_program → nat ≝
446 λp.
447  let globals_addr_internal ≝
448   λoffset : nat.
449   λx_size: ident × region × nat.
450    let 〈x, region, size〉 ≝ x_size in
451     offset + size in
452 foldl … globals_addr_internal 0 (prog_vars … p).
453
[2700]454definition ertlptr_to_ltl:
[2774]455 fixpoint_computer → coloured_graph_computer → ertlptr_program →
456  ltl_program × stack_cost_model × nat ≝
457  λthe_fixpoint,build,pr.
458   let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in
459   〈ltlprog, stack_cost … ltlprog, 2^16 - first_free_stack_addr ltlprog〉.
Note: See TracBrowser for help on using the repository browser.