source: src/ERTL/ERTLToLTL_paolo.ma @ 2208

Last change on this file since 2208 was 2208, checked in by tranquil, 8 years ago
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
File size: 14.7 KB
Line 
1include "LTL/LTL_paolo.ma".
2include "ERTL/Interference_paolo.ma".
3include "ASM/Arithmetic.ma".
4include "joint/TranslateUtils_paolo.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 : beval → arg_decision.
17
18coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision.
19
20definition stacksize :
21  ∀globals.ℕ → joint_internal_function globals ertl_params → ℕ ≝
22  λglobals.
23  λspilled_no.
24  λint_fun.
25  spilled_no + joint_if_stacksize … int_fun.
26
27(* Paolo: I'm changing the following: before, spilled registers were
28  assigned stack addresses going from SP + #frame_size - #stack_params
29  excluded down to SP included. I am turning it upside down, so that
30  the offset does not need the stack size to be computed *)
31
32definition preserve_carry_bit :
33  ∀globals.bool → list (joint_seq ltl_params globals) → list (joint_seq ltl_params globals) ≝
34  λglobals,do_it,steps.
35  if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.
36
37(* for notation *)
38definition A ≝ it.
39
40coercion beval_of_byte : ∀b : Byte.beval ≝ BVByte on _b : Byte to beval.
41
42(* spill should be byte-based from the start *)
43definition set_dp_by_offset :
44  ∀globals.nat → list (joint_seq ltl_params globals) ≝
45  λglobals,off.
46  [ A ← byte_of_nat off
47  ; A ← A .Add. RegisterSPL
48  ; RegisterDPL ← A
49  ; A ← zero_byte
50  ; A ← A .Addc. RegisterSPH
51  ; RegisterDPH ← A
52  ].
53
54definition get_stack:
55 ∀globals.Register → nat → list (joint_seq ltl_params globals) ≝
56 λglobals,r,off.
57 set_dp_by_offset ? off @
58 [ LOAD … A it it ] @
59 if eq_Register r RegisterA then [ ] else [ r ← A ].
60
61definition set_stack_not_a :
62 ∀globals.nat → Register → list (joint_seq ltl_params globals) ≝
63 λglobals,off,r.
64 set_dp_by_offset ? off @
65 [ A ← r
66 ; STORE … it it A ].
67
68definition set_stack_a :
69 ∀globals.nat → list (joint_seq ltl_params globals) ≝
70 λglobals,off.
71 [ RegisterST1 ← A ] @
72 set_stack_not_a ? off RegisterST1.
73
74definition set_stack :
75 ∀globals.nat → Register → list (joint_seq ltl_params globals) ≝
76 λglobals,off,r.
77 if eq_Register r RegisterA then
78   set_stack_a ? off
79 else
80   set_stack_not_a ? off r.
81 
82definition set_stack_int :
83  ∀globals.nat → beval →  list (joint_seq ltl_params globals) ≝
84  λglobals,off,int.
85  set_dp_by_offset ? off @
86  [ A ← int
87  ; STORE … it it A ].
88
89definition move :
90  ∀globals.bool → decision → arg_decision → list (joint_seq ltl_params globals) ≝
91  λglobals,carry_lives_after,dst,src.
92  match dst with
93  [ decision_colour dstr ⇒
94    match src with
95    [ arg_decision_colour srcr ⇒
96      if eq_Register dstr srcr then [ ] else
97      if eq_Register dstr RegisterA then [ A ← srcr ] else
98      if eq_Register srcr RegisterA then [ dstr ← A ] else
99      [ A ← srcr ; dstr ← A]
100    | arg_decision_spill srco ⇒
101      preserve_carry_bit ? carry_lives_after
102        (get_stack ? dstr srco)
103    | arg_decision_imm int ⇒
104      [ A ← int ] @
105      if eq_Register dstr RegisterA then [ ] else
106      [ dstr ← A ]
107    ]
108  | decision_spill dsto ⇒
109    match src with
110    [ arg_decision_colour srcr ⇒
111      preserve_carry_bit ? carry_lives_after
112        (set_stack ? dsto srcr)
113    | arg_decision_spill srco ⇒
114      if eqb srco dsto then [ ] else
115      preserve_carry_bit ? carry_lives_after
116        (get_stack ? RegisterA srco @
117         set_stack ? dsto RegisterA)
118    | arg_decision_imm int ⇒
119      preserve_carry_bit ? carry_lives_after
120        (set_stack_int ? dsto int)
121    ]
122  ].
123
124definition arg_is_spilled : arg_decision → bool ≝
125  λx.match x with [ arg_decision_spill _ ⇒ true | _ ⇒ false ].
126definition is_spilled : decision → bool ≝
127  λx.match x with [ decision_spill _ ⇒ true | _ ⇒ false ].
128
129definition newframe :
130  ∀globals.ℕ → list (joint_seq ltl_params globals) ≝
131  λglobals,stack_sz.
132  [ CLEAR_CARRY …
133  ; A ← RegisterSPL
134  ; A ← A .Sub. byte_of_nat stack_sz
135  ; RegisterSPL ← A
136  ; A ← RegisterSPH
137  ; A ← A .Sub. zero_byte
138  ; RegisterSPL ← A
139  ].
140
141definition delframe :
142  ∀globals.ℕ → list (joint_seq ltl_params globals) ≝
143  λglobals,stack_sz.
144  [ A ← RegisterSPL
145  ; A ← A .Add. byte_of_nat stack_sz
146  ; RegisterSPL ← A
147  ; A ← RegisterSPH
148  ; A ← A .Addc. zero_byte
149  ; RegisterSPL ← A
150  ].
151
152definition commutative : Op2 → bool ≝
153λop.match op with
154[ Add ⇒ true
155| Addc ⇒ true
156| Or ⇒ true
157| Xor ⇒ true
158| And ⇒ true
159| _ ⇒ false
160].
161
162definition uses_carry : Op2 → bool ≝
163λop.match op with
164[ Addc ⇒ true
165| Sub ⇒ true
166| _ ⇒ false
167].
168
169definition sets_carry : Op2 → bool ≝
170λop.match op with
171[ Add ⇒ true
172| Addc ⇒ true
173| Sub ⇒ true
174| _ ⇒ false
175].
176
177definition translate_op2 :
178  ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
179  λglobals,carry_lives_after,op,dst,arg1,arg2.
180  (* this won't preserve the carry bit if op does not set it: left to next function *)
181  (* if op uses carry bit (⇒ it sets it too) it must be preserved before the op *)
182  (preserve_carry_bit ?
183    (uses_carry op ∧ (arg_is_spilled arg1 ∨ arg_is_spilled arg2))
184    (move ? false RegisterB arg2 @
185     move ? false RegisterA arg1) @
186    [ A ← A .op. RegisterB ] @
187    (* it op sets the carry bit and it is needed afterwards it must be preserved here *)
188    move ? (sets_carry op ∧ carry_lives_after) dst RegisterA).
189
190definition translate_op2_smart :
191  ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
192  λglobals,carry_lives_after,op,dst,arg1,arg2.
193  (* if op does not set carry bit (⇒ it does not use it either) then it must be
194    preserved *)
195  preserve_carry_bit ?
196    (¬sets_carry op ∧ carry_lives_after ∧
197      (arg_is_spilled arg1 ∨ arg_is_spilled arg2 ∨ is_spilled dst))
198    (match arg2 with
199    [ arg_decision_colour arg2r ⇒
200      move ? (uses_carry op) RegisterA arg1 @
201      [ A ← A .op. arg2r ] @
202      move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
203    | arg_decision_imm arg2i ⇒
204      move ? (uses_carry op) RegisterA arg1 @
205      [ A ← A .op. arg2i ] @
206      move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
207    | _ ⇒
208      if commutative op then
209        match arg1 with
210        [ arg_decision_colour arg1r ⇒
211          move ? (uses_carry op) RegisterA arg2 @
212          [ A ← A .op. arg1r ] @
213          move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
214        | arg_decision_imm arg1i ⇒
215          move ? (uses_carry op) RegisterA arg2 @
216          [ A ← A .op. arg1i ] @
217          move ? (sets_carry op ∧ carry_lives_after) dst RegisterA
218        | _ ⇒
219          translate_op2 ? carry_lives_after op dst arg1 arg2
220        ]
221      else
222        translate_op2 ? carry_lives_after op dst arg1 arg2
223    ]).
224
225definition dec_to_arg_dec : decision → arg_decision ≝
226  λd.match d with
227  [ decision_colour r ⇒ arg_decision_colour r
228  | decision_spill n ⇒ arg_decision_spill n
229  ].
230
231coercion dec_arg_dec : ∀d:decision.arg_decision ≝ dec_to_arg_dec on _d : decision to arg_decision.
232
233definition translate_op1 :
234  ∀globals.bool → Op1 → decision → decision → list (joint_seq ltl_params globals) ≝
235  λglobals,carry_lives_after,op,dst,arg.
236  let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in
237  preserve_carry_bit ? preserve_carry
238    (move ? false RegisterA arg @
239     OP1 … op it it ::
240     move ? false dst RegisterA).
241
242definition translate_opaccs :
243  ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
244  λglobals,carry_lives_after,op,dst1,dst2,arg1,arg2.
245  (* OPACCS always has dead carry bit and sets it to zero *)
246  move ? false RegisterB arg2 @
247  move ? false RegisterA arg1 @
248  OPACCS … op it it it it ::
249  move ? false dst1 RegisterA @
250  move ? false dst2 RegisterB @
251  if carry_lives_after ∧ (is_spilled dst1 ∨ is_spilled dst2) then
252    [CLEAR_CARRY ??]
253  else [ ].
254
255(* does not preserve carry bit *)
256definition move_to_dp :
257  ∀globals.arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
258  λglobals,arg1,arg2.
259  if ¬arg_is_spilled arg1 then
260    move ? false RegisterDPH arg2 @
261    (* does not change dph because arg1 is not spilled *)
262    move ? false RegisterDPL arg1
263  else if ¬arg_is_spilled arg2 then
264    move ? false RegisterDPL arg1 @
265    (* does not change dpl because arg2 is not spilled *)
266    move ? false RegisterDPH arg2
267  else
268    (* using B as temporary, as moving spilled registers tampers with DPTR *)
269    move ? false RegisterB arg1 @
270    move ? false RegisterDPH arg2 @
271    move ? false RegisterDPL RegisterB.
272
273definition translate_store : 
274  ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
275  λglobals,carry_lives_after,addr1,addr2,src.
276  (* requires src != RegisterA and RegisterB *)
277  preserve_carry_bit ? (carry_lives_after ∧
278    (arg_is_spilled addr1 ∨ arg_is_spilled addr1 ∨ arg_is_spilled src))
279    (let move_to_dptr ≝ move_to_dp ? addr1 addr2 in
280     (if arg_is_spilled src then
281        move ? false RegisterST0 src @
282        move_to_dptr @
283        [ A ← RegisterST0]
284      else move_to_dptr) @
285     [STORE … it it A]).
286
287definition translate_load : 
288  ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
289  λglobals,carry_lives_after,dst,addr1,addr2.
290  preserve_carry_bit ? (carry_lives_after ∧
291    (is_spilled dst ∨ arg_is_spilled addr1 ∨ arg_is_spilled addr1))
292    (move_to_dp ? addr1 addr2 @
293     [ LOAD … A it it ] @
294     move ? false dst RegisterA).
295
296definition translate_address :
297  ∀globals.bool → ∀i.member i (eq_identifier ?) globals → decision → decision →
298  list (joint_seq ltl_params globals) ≝
299  λglobals,carry_lives_after,id,prf,addr1,addr2.
300  preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2))
301    (ADDRESS ltl_params ? id prf it it ::
302     move ? false addr1 RegisterDPL @
303     move ? false addr2 RegisterDPH).
304
305definition translate_step:
306  ∀globals.∀after : valuation register_lattice.
307  coloured_graph after →
308  ℕ → label → joint_step ertl_params globals → seq_block ltl_params globals (joint_step ltl_params globals) ≝
309  λglobals,after,grph,stack_sz,lbl,s.
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 ≝ hlives RegisterCarry (after lbl) in
316  let move ≝ move globals carry_lives_after in
317  match s with
318  [ step_seq s' ⇒
319    match s' return λ_.seq_block ltl_params globals (joint_step ltl_params globals) with
320    [ COMMENT c ⇒ COMMENT … c
321    | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl
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 ? carry_lives_after
330        (lookup_arg addr1)
331        (lookup_arg addr2)
332        (lookup_arg srcr)
333    | LOAD dstr addr1 addr2 ⇒
334      translate_load ? carry_lives_after
335        (lookup dstr)
336        (lookup_arg addr1)
337        (lookup_arg addr2)
338    | CLEAR_CARRY ⇒ CLEAR_CARRY …
339    | SET_CARRY ⇒ CLEAR_CARRY …
340    | OP2 op dst arg1 arg2 ⇒
341      translate_op2_smart ? carry_lives_after op
342        (lookup dst)
343        (lookup_arg arg1)
344        (lookup_arg arg2)
345    | OP1 op dst arg ⇒
346      translate_op1 ? 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 dpl dph ⇒
362      translate_address ? carry_lives_after
363        lbl prf (lookup dpl) (lookup dph)
364    | OPACCS op dst1 dst2 arg1 arg2 ⇒
365      translate_opaccs ? 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_new_frame ⇒ newframe ? stack_sz
371      | ertl_del_frame ⇒ delframe ? stack_sz
372      | ertl_frame_size r ⇒
373        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
374      ]
375    | CALL_ID f n_args _ ⇒ CALL_ID ltl_params ? f n_args it
376    | extension_call abs ⇒ match abs in void with [ ]
377    ]
378  | COND r ltrue ⇒
379    〈move RegisterA (lookup r),COND … it ltrue〉
380  ].
381
382definition translate_fin_step:
383  ∀globals.label → joint_fin_step ertl_params → seq_block ltl_params globals (joint_fin_step ltl_params) ≝
384  λglobals,lbl,s.
385  match s return λ_.seq_block ltl_params globals (joint_fin_step ltl_params) with
386  [ RETURN ⇒ RETURN ?
387  | GOTO l ⇒ GOTO ? l
388  | tailcall abs ⇒ match abs in void with [ ]
389  ].
390
391definition translate_internal: ∀globals: list ident.
392  joint_internal_function globals ertl_params →
393  joint_internal_function globals ltl_params ≝
394  λglobals: list ident.
395  λint_fun: joint_internal_function globals ertl_params.
396  (* initialize graph *)
397  let entry ≝ pi1 … (joint_if_entry … int_fun) in
398  let exit ≝ pi1 … (joint_if_exit … int_fun) in
399  let graph ≝ add ? ? (empty_map ? (joint_statement ??)) entry (GOTO … exit) in
400  let graph ≝ add ? ? graph exit (RETURN …) in
401  (* colour registers *)
402  let after ≝ analyse_liveness globals int_fun in
403  let coloured_graph ≝ build after in
404  (* compute new stack size *)
405  let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
406  (* initialize internal function *)
407  let init ≝ mk_joint_internal_function globals ltl_params
408    (joint_if_luniverse … int_fun)
409    (joint_if_runiverse … int_fun)
410    it it [ ] stack_sz graph entry exit in
411  graph_translate …
412    init
413    (translate_step … coloured_graph stack_sz)
414    (translate_fin_step …)
415    int_fun.
416>graph_code_has_point @map_mem_prop
417[@graph_add_lookup] @graph_add
418qed.
419
420definition ertl_to_ltl: ertl_program → ltl_program ≝
421  λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
Note: See TracBrowser for help on using the repository browser.