source: src/ERTL/ERTLToLTL.ma @ 2490

Last change on this file since 2490 was 2490, checked in by tranquil, 7 years ago

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

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