source: src/ERTL/ERTLToLTL.ma @ 3014

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

ERTL to ERTLptr pass suppressed (it introduced a bug in the later ERTLptr to LTL), and integrated in a single ERTToLTL pass like before

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