source: src/ERTLptr/ERTLptrToLTL.ma @ 2944

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

Many changes:

  1. Coloured graphs are now specified in terms of livebefore
  2. Type of livebefore changed so that it is now a valuation transformer
  3. Several axioms can now be inhabited in ERTLptrToLTLProof

Problems:
ERTLtoERTLptrOK is broken beyond my understanding. This pass should have
been unaffected by the changes, but it is not so. Why?

File size: 16.5 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,fn.nat → ∀after : valuation register_lattice.
323  coloured_graph (livebefore globals fn after) →
324  ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝
325  λglobals,fn,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  if eliminable_step … (after lbl) s then ([ ] : step_block LTL globals) else
335  match s with
336  [ step_seq s' ⇒
337    match s' return λ_.step_block LTL globals with
338    [ COMMENT c ⇒ [COMMENT … c]
339    | POP r ⇒
340      POP … A ::
341      move (lookup r) RegisterA
342    | PUSH a ⇒
343      move RegisterA (lookup_arg a) @
344      [ PUSH … A ]
345    | STORE addr1 addr2 srcr ⇒
346      translate_store ? localss carry_lives_after
347        (lookup_arg addr1)
348        (lookup_arg addr2)
349        (lookup_arg srcr)
350    | LOAD dstr addr1 addr2 ⇒
351      translate_load ? localss carry_lives_after
352        (lookup dstr)
353        (lookup_arg addr1)
354        (lookup_arg addr2)
355    | CLEAR_CARRY ⇒ [CLEAR_CARRY ??]
356    | SET_CARRY ⇒ [SET_CARRY ??]
357    | OP2 op dst arg1 arg2 ⇒
358      translate_op2_smart ? localss carry_lives_after op
359        (lookup dst)
360        (lookup_arg arg1)
361        (lookup_arg arg2)
362    | OP1 op dst arg ⇒
363      translate_op1 ? localss carry_lives_after op
364        (lookup dst)
365        (lookup arg)
366    | MOVE pair_regs ⇒
367      let lookup_move_dst ≝ λx.match x return λ_.decision with
368        [ PSD r ⇒ lookup r
369        | HDW r ⇒ r
370        ] in
371      let dst ≝ lookup_move_dst (\fst pair_regs) in
372      let src ≝
373        match \snd pair_regs return λ_.arg_decision with
374        [ Reg r ⇒ lookup_move_dst r
375        | Imm b ⇒ arg_decision_imm b
376        ] in
377      move dst src
378    | ADDRESS lbl prf dpl dph ⇒
379      translate_address ? localss carry_lives_after
380        lbl prf (lookup dpl) (lookup dph)
381    | OPACCS op dst1 dst2 arg1 arg2 ⇒
382      translate_opaccs ? localss carry_lives_after op
383        (lookup dst1) (lookup dst2)
384        (lookup_arg arg1) (lookup_arg arg2)
385    | extension_seq ext ⇒
386      match ext with
387        [ ertlptr_ertl ext' ⇒
388          match ext' with
389          [ ertl_new_frame ⇒ newframe ? stack_sz
390          | ertl_del_frame ⇒ delframe ? stack_sz
391          | ertl_frame_size r ⇒
392            move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
393          ]
394        | LOW_ADDRESS r1 l ⇒
395           translate_low_address ? localss carry_lives_after (lookup r1) l
396        | HIGH_ADDRESS r1 l ⇒
397           translate_high_address ? localss carry_lives_after (lookup r1) l       
398        ]
399    ]
400  | COST_LABEL cost_lbl ⇒ 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉
401  | COND r ltrue ⇒
402    〈add_dummy_variance … (move RegisterA (lookup r)),λ_.COND … it ltrue, [ ]〉
403  | CALL f n_args _ ⇒
404      match f with
405      [ inl f ⇒
406        〈[ ],λ_.CALL LTL ? (inl … f) n_args it, [ ]〉
407      | inr dp ⇒
408        let 〈dpl, dph〉 ≝ dp in
409        〈add_dummy_variance … (move_to_dp ? localss (lookup_arg dpl) (lookup_arg dph)),
410         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
411      ]
412  ]).
413
414definition translate_fin_step:
415  ∀globals.label → joint_fin_step ERTLptr → bind_fin_block LTL globals ≝
416  λglobals,lbl,s.
417  bret … (〈[ ],
418  match s with
419  [ RETURN ⇒ RETURN ?
420  | GOTO l ⇒ GOTO ? l
421  | TAILCALL abs _ _ ⇒ Ⓧabs
422  ]〉).
423
424definition translate_data :
425 fixpoint_computer → coloured_graph_computer →
426 ∀globals.
427  joint_closed_internal_function ERTLptr globals →
428  bind_new register (b_graph_translate_data ERTLptr LTL globals) ≝
429λthe_fixpoint,build,globals,int_fun.
430(* colour registers *)
431let after ≝ analyse_liveness the_fixpoint globals int_fun in
432let coloured_graph ≝ build … int_fun after in
433(* compute new stack size *)
434let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
435bret …
436  (mk_b_graph_translate_data ERTLptr LTL globals
437    (* init_ret ≝ *) it
438    (* init_params ≝ *) it
439    (* init_stack_size ≝ *) stack_sz
440    (* added_prologue ≝ *) [ ]
441    (* new_regs ≝ *) [ ]
442    (* f_step ≝ *) (translate_step ? int_fun (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz)
443    (* f_fin ≝ *) (translate_fin_step globals)
444    ????).
445@hide_prf
446[
447| #l #c % ]
448cases daemon (* TODO *)
449qed.
450
451(* Paolo: does it really have sense to do here the first stack address computation,
452   when it is an info easily available from any program in the back end?
453   Also, is it really 2^16 - |globals|, or should there also be a -1? *)
454definition ertlptr_to_ltl:
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 - globals_stacksize … ltlprog〉.
460%
461qed.
Note: See TracBrowser for help on using the repository browser.