source: src/ERTL/ERTLToLTL.ma @ 3371

Last change on this file since 3371 was 3371, checked in by piccolo, 6 years ago

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

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