source: src/ERTL/ERTLToLTL_paolo.ma @ 2174

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