source: src/ERTLptr/ERTLptrToLTL.ma @ 2883

Last change on this file since 2883 was 2883, checked in by piccolo, 7 years ago

partial commit

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