source: src/ERTL/ERTLToLTL_paolo.ma @ 2175

Last change on this file since 2175 was 2175, checked in by tranquil, 8 years ago

corrected small bug

File size: 14.5 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 : Byte → 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
37definition set_dp_by_offset :
38  ∀globals.Byte → list (joint_seq ltl_params globals) ≝
39  λglobals,off.
40  [ 𝐀 ← off
41  ; 𝐀 ← 𝐀 .Add. RegisterSPL
42  ; RegisterDPL ← 𝐀
43  ; 𝐀 ← 0
44  ; 𝐀 ← 𝐀 .Addc. RegisterSPH
45  ; RegisterDPH ← 𝐀
46  ].
47
48definition get_stack:
49 ∀globals.Register → Byte → list (joint_seq ltl_params globals) ≝
50 λglobals,r,off.
51 set_dp_by_offset ? off @
52 [ LOAD … it it it ] @
53 if eq_Register r RegisterA then [ ] else [ r ← 𝐀 ].
54
55definition set_stack_not_a :
56 ∀globals.Byte → Register → list (joint_seq ltl_params globals) ≝
57 λglobals,off,r.
58 set_dp_by_offset ? off @
59 [ 𝐀 ← r
60 ; STORE … it it it ].
61
62definition set_stack_a :
63 ∀globals.Byte → list (joint_seq ltl_params globals) ≝
64 λglobals,off.
65 [ RegisterST1 ← 𝐀 ] @
66 set_stack_not_a ? off RegisterST1.
67
68definition set_stack :
69 ∀globals.Byte → Register → list (joint_seq ltl_params 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.Byte → Byte →  list (joint_seq ltl_params globals) ≝
78  λglobals,off,int.
79  set_dp_by_offset ? off @
80  [ 𝐀 ← int
81  ; STORE … it it it ].
82
83definition move :
84  ∀globals.bool → decision → arg_decision → list (joint_seq ltl_params 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 [ 𝐀 ← srcr ] else
92      if eq_Register srcr RegisterA then [ dstr ← 𝐀 ] else
93      [ 𝐀 ← srcr ; dstr ← 𝐀]
94    | arg_decision_spill srco ⇒
95      preserve_carry_bit ? carry_lives_after
96        (get_stack ? dstr srco)
97    | arg_decision_imm int ⇒
98      [ 𝐀 ← int ] @
99      if eq_Register dstr RegisterA then [ ] else
100      [ dstr ← 𝐀 ]
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_params globals) ≝
125  λglobals,stack_sz.
126  [ CLEAR_CARRY …
127  ; 𝐀 ← RegisterSPL
128  ; 𝐀 ← 𝐀 .Sub. stack_sz
129  ; RegisterSPL ← 𝐀
130  ; 𝐀 ← RegisterSPH
131  ; 𝐀 ← 𝐀 .Sub. 0
132  ; RegisterSPL ← 𝐀
133  ].
134
135definition delframe :
136  ∀globals.ℕ → list (joint_seq ltl_params globals) ≝
137  λglobals,stack_sz.
138  [ 𝐀 ← RegisterSPL
139  ; 𝐀 ← 𝐀 .Add. stack_sz
140  ; RegisterSPL ← 𝐀
141  ; 𝐀 ← RegisterSPH
142  ; 𝐀 ← 𝐀 .Addc. 0
143  ; RegisterSPL ← 𝐀
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_params 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    [ 𝐀 ← 𝐀 .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_params 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      [ 𝐀 ← 𝐀 .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      [ 𝐀 ← 𝐀 .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          [ 𝐀 ← 𝐀 .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          [ 𝐀 ← 𝐀 .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_params 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_params 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_params 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_params 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        [ 𝐀 ← RegisterST0]
278      else move_to_dptr) @
279     [STORE … it it it]).
280
281definition translate_load : 
282  ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq ltl_params 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 … it it it ] @
288     move ? false dst RegisterA).
289
290definition translate_address :
291  ∀globals.bool → ∀i.member i (eq_identifier ?) globals → decision → decision →
292  list (joint_seq ltl_params 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_params ? 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_params globals → seq_block ltl_params globals (joint_step ltl_params 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_params globals (joint_step ltl_params globals) with
314    [ COMMENT c ⇒ COMMENT … c
315    | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl
316    | POP r ⇒
317      POP … it ::
318      move (lookup r) RegisterA
319    | PUSH a ⇒
320      move RegisterA (lookup_arg a) @
321      [ PUSH … it ]
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        | INT 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 stack_sz)
368      ]
369    | CALL_ID f n_args _ ⇒ CALL_ID ltl_params ? f n_args it
370    | extension_call abs ⇒ match abs in void with [ ]
371    ]
372  | COND r ltrue ⇒
373    〈move RegisterA (lookup r),COND … it ltrue〉
374  ].
375
376definition translate_fin_step:
377  ∀globals.label → joint_fin_step ertl_params → seq_block ltl_params globals (joint_fin_step ltl_params) ≝
378  λglobals,lbl,s.
379  match s return λ_.seq_block ltl_params globals (joint_fin_step ltl_params) with
380  [ RETURN ⇒ RETURN ?
381  | GOTO l ⇒ GOTO ? l
382  | tailcall abs ⇒ match abs in void with [ ]
383  ].
384
385definition translate_internal: ∀globals: list ident.
386  ertl_internal_function globals → joint_internal_function globals ltl_params ≝
387  λglobals: list ident.
388  λint_fun: ertl_internal_function globals.
389  (* initialize graph *)
390  let entry ≝ pi1 … (joint_if_entry … int_fun) in
391  let exit ≝ pi1 … (joint_if_exit … int_fun) in
392  let graph ≝ add ? ? (empty_map ? (joint_statement ??)) entry (GOTO … exit) in
393  let graph ≝ add ? ? graph exit (RETURN …) in
394  (* colour registers *)
395  let after ≝ analyse_liveness globals int_fun in
396  let coloured_graph ≝ build after in
397  (* compute new stack size *)
398  let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
399  (* initialize internal function *)
400  let init ≝ mk_joint_internal_function globals ltl_params
401    (joint_if_luniverse … int_fun)
402    (joint_if_runiverse … int_fun)
403    it it [ ] stack_sz graph entry exit in
404  graph_translate …
405    init
406    (translate_step … coloured_graph stack_sz)
407    (translate_fin_step …)
408    int_fun.
409>graph_code_has_point @map_mem_prop
410[@graph_add_lookup] @graph_add
411qed.
412
413definition ertl_to_ltl: ertl_program → ltl_program ≝
414  λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
Note: See TracBrowser for help on using the repository browser.