source: src/RTLabs/RTLabsToRTL.ma

Last change on this file was 3263, checked in by tranquil, 6 years ago

moved callee saved saving and restoring to ERTL -> LTL pass (untrusted
colourer and interference graph creator still need to be updated)
joint now has the stack size split in three (referenced locals, params
and spilled)

File size: 39.9 KB
Line 
1include "RTLabs/RTLabs_syntax.ma".
2include "RTL/RTL.ma".
3include "common/FrontEndOps.ma".
4include "common/Graphs.ma".
5include "joint/TranslateUtils.ma".
6include "joint/joint_stacksizes.ma".
7include alias "ASM/BitVector.ma".
8include alias "arithmetics/nat.ma".
9
10definition size_of_sig_type ≝
11  λsig.
12  match sig with
13  [ ASTint isize sign ⇒
14    match isize with [ I8 ⇒ 1 | I16 ⇒ 2 | I32 ⇒ 4 ]
15  | ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *)
16  ].
17
18definition sign_of_sig_type ≝
19  λsig.
20  match sig with
21  [ ASTint _ sign ⇒ sign
22  | ASTptr ⇒ Unsigned
23  ].
24
25inductive register_type: Type[0] ≝
26  | register_int: register → register_type
27  | register_ptr: register → register → register_type.
28
29definition local_env ≝ identifier_map RegisterTag (list register).
30
31definition local_env_typed :
32  list (register × typ) → local_env → Prop ≝
33  λl,env.All ?
34    (λp.let 〈r, ty〉 ≝ p in ∃regs.lookup … env r = Some ? regs ∧
35                                 |regs| = size_of_sig_type ty) l.
36
37definition find_local_env ≝ λr.λlenv : local_env.
38  λprf : r ∈ lenv.opt_safe … (lookup … lenv r) ?.
39lapply (in_map_domain … lenv r)
40>prf * #x #lookup_eq >lookup_eq % #ABS destruct(ABS)
41qed.
42
43lemma find_local_env_elim : ∀P : list register → Prop.∀r. ∀lenv: local_env.∀prf.
44  (∀x.lookup … lenv r = Some ? x → P x) → P (find_local_env r lenv prf).
45#P#r#lenv#prf #H
46change with (P (opt_safe ???))
47@opt_safe_elim assumption
48qed.
49
50definition find_local_env_arg : register → local_env → ? → list psd_argument ≝
51  λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf).
52
53(* move *)
54let rec m_iter (M : Monad) X (f : X → M X) (n : ℕ) (m : M X) on n : M X ≝
55match n with
56[ O ⇒ m
57| S k ⇒
58  ! v ← m ;
59  m_iter … f k (f v)
60].
61
62definition fresh_registers : ∀p,g.ℕ → state_monad (joint_internal_function p g) (list register) ≝
63λp,g,n.
64  let f ≝ λacc.! m ← fresh_register … ; return (m :: acc) in
65  m_iter … f n (return [ ]).
66
67include alias "common/Identifiers.ma".
68let rec map_list_local_env
69  lenv (regs : list (register×typ)) on regs :
70  All ? (λpr.bool_to_Prop (\fst pr ∈ lenv)) regs → list register ≝
71  match regs return λx.All ?? x → ? with
72  [ nil ⇒ λ_.[ ]
73  | cons hd tl ⇒ λprf.find_local_env (\fst hd) lenv ? @ map_list_local_env lenv tl ?
74  ].cases prf #A #B assumption qed.
75
76definition initialize_local_env :
77  ∀globals.
78  list (register×typ) →
79  state_monad (joint_internal_function RTL globals) local_env ≝
80  λglobals,registers.
81  let f ≝
82    λr_sig,lenv.
83    let 〈r, sig〉 ≝ r_sig in
84    let size ≝ size_of_sig_type sig in
85    ! regs ← fresh_registers … size ;
86    return add … lenv r regs in
87  m_fold … f registers (empty_map …).
88
89lemma initialize_local_env_in : ∀globals,l,def,r.
90  Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env globals l def).
91whd in match initialize_local_env; normalize nodelta #globals
92cut (∀l,init,def,r.(Exists  ? (λx.\fst x = r) l ∨ bool_to_Prop (r ∈ init)) →
93     r ∈ \snd (m_fold (state_monad ?) ??? l init def))
94[7: #aux #l #def #r #H @aux %1{H} |*:]
95#l elim l -l
96[ #init #def #r * [*] #H @H ]
97* #hd #sig #tl #IH #init #def #r #H
98whd in ⊢ (?(???(???%)?)); normalize nodelta
99whd in ⊢ (?(???(???(match % with [ _ ⇒ ?]))?));
100inversion (fresh_registers ????) #def' #regs #EQfresh normalize nodelta
101@IH cases H -H [*] #H
102[ destruct %2 @mem_set_add_id
103| %1{H}
104| %2 >mem_set_add @orb_Prop_r @H
105]
106qed.
107
108example proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr.
109// qed-.
110example proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr.
111// qed-.
112
113definition initialize_locals_params_ret :
114  ∀globals.
115  (* locals *) list (register×typ) →
116  (* params *) list (register×typ) →
117  (* return *) option (register×typ) →
118  state_monad (joint_internal_function RTL globals) local_env ≝
119  λglobals,locals,params,ret,def.
120  let 〈def',lenv〉 as EQ ≝
121    initialize_local_env globals
122    ((match ret with
123     [ Some r_sig ⇒ [r_sig]
124     | None ⇒ [ ]
125     ]) @ locals @ params) def in
126  let params' ≝ map_list_local_env lenv params ? in
127  let ret' ≝ match ret return λx.ret = x → ? with
128    [ Some r_sig ⇒ λprf.find_local_env (\fst r_sig) lenv ?
129    | None ⇒ λ_.[ ]
130    ] (refl …) in
131  let def'' ≝
132    mk_joint_internal_function RTL globals
133      (joint_if_luniverse … def') (joint_if_runiverse … def') ret'
134      params' (joint_if_stacksize … def') (joint_if_local_stacksize … def') 0
135      (joint_if_code … def') (joint_if_entry … def') in
136   〈def'', lenv〉. @hide_prf
137[ >(proj2_rewrite ????? EQ)
138  @initialize_local_env_in >prf %1 %
139|*: >(proj2_rewrite ????? EQ)
140  @(All_mp ??? (λpr.initialize_local_env_in ??? (\fst pr)))
141  @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params))
142  [ #a #H @Exists_append_r @Exists_append_r @H
143  | elim params [%] #hd #tl #IH % [ %1 % ] @(All_mp … IH) #x #G %2{G}
144  ]
145]
146qed.
147
148definition make_addr ≝
149  λA.
150  λlst: list A.
151  λprf: 2 = length A lst.〈nth_safe … 0 lst ?, nth_safe … 1 lst ?〉. <prf [%2] %1
152  qed.
153
154definition find_and_addr ≝
155  λr,lenv,prf. make_addr ? (find_local_env r lenv prf).
156
157definition find_and_addr_arg ≝
158  λr,lenv,prf. make_addr ? (find_local_env_arg r lenv prf).
159
160(*include alias "common/Identifiers.ma".*)
161let rec rtl_args (args : list register) (env : local_env) on args :
162  All ? (λr.bool_to_Prop (r∈env)) args → list psd_argument ≝
163  match args return λx.All ?? x → ? with
164  [ nil ⇒ λ_.[ ]
165  | cons hd tl ⇒ λprf.find_local_env_arg hd env ? @ rtl_args tl env ?
166  ].
167  cases prf #H #G assumption
168  qed.
169
170include alias "basics/lists/list.ma".
171let rec vrsplit A (m,n : nat)
172  on m : Vector A (m*n) → Σs : list (Vector A n).|s| = m ≝
173  match m return λx.Vector A (x*n) → Sig (list ?) ? with
174  [ O ⇒ λv.[ ]
175  | S k ⇒ λv.let spl ≝ vsplit ? n … v in \fst spl :: vrsplit ? k n (\snd spl)
176  ].
177  [ %
178  | cases (vrsplit ????) #lst #EQ normalize >EQ %
179  ] qed.
180
181definition split_into_bytes:
182  ∀size. ∀int: bvint size. Σbytes: list Byte. |bytes| = size_intsize size ≝
183λsize,int.reverse … (vrsplit ? (size_intsize size) 8 int).
184>length_reverse @pi2 qed.
185
186let rec list_inject_All_aux A P (l : list A) on l : All A P l → list (Σx.P x) ≝
187match l return λx.All A P x → list (Σx.P x) with
188[ nil ⇒ λ_.[ ]
189| cons hd tl ⇒ λprf.«hd, proj1 … prf» :: list_inject_All_aux A P tl (proj2 … prf)
190].
191
192definition translate_op_aux:
193  ∀globals. Op2 →
194  ∀dests : list register.
195  ∀srcrs1 : list psd_argument.
196  ∀srcrs2 : list psd_argument.
197  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
198  list (joint_seq RTL globals)
199  ≝
200  λglobals: list ident.
201  λop.
202  λdestrs.
203  λsrcrs1.
204  λsrcrs2.
205  λprf1,prf2.
206  (* first, clear carry if op relies on it *)
207  map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2.
208
209definition translate_op:
210  ∀globals. Op2 →
211  ∀dests : list register.
212  ∀srcrs1 : list psd_argument.
213  ∀srcrs2 : list psd_argument.
214  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
215  list (joint_seq RTL globals)
216  ≝
217  λglobals: list ident.
218  λop.
219  λdestrs.
220  λsrcrs1.
221  λsrcrs2.
222  match op with
223  [ Add ⇒
224    match destrs return λdestrs.|destrs| = |srcrs1| → |srcrs1| = |srcrs2| → ? with
225    [ nil ⇒ λ_.λ_.[ ]
226    | cons destr destrs' ⇒
227      match srcrs1 return λsrcrs1.S(|destrs'|) = |srcrs1| → |srcrs1| = |srcrs2| → ? with
228      [ nil ⇒ λprf1.⊥
229      | cons srcr1 srcrs1' ⇒
230        λprf1.
231        match srcrs2 return λsrcrs2.S(|srcrs1'|) = |srcrs2| → ? with
232        [ nil ⇒ λprf2.⊥
233        | cons srcr2 srcrs2' ⇒
234          λprf2.OP2 ?? Add destr srcr1 srcr2 :: translate_op_aux … Addc destrs' srcrs1' srcrs2' ??
235        ]
236      ]
237    ]
238  | Sub ⇒ λprf1,prf2.[ CLEAR_CARRY ?? ] @ translate_op_aux … Sub … prf1 prf2
239  | Addc ⇒ λprf1,prf2.[ CLEAR_CARRY ?? ] @ translate_op_aux … Addc … prf1 prf2
240  | _ ⇒ translate_op_aux … op destrs srcrs1 srcrs2
241  ].
242  normalize in prf1 prf2; destruct assumption qed.
243
244definition cast_list : ∀A.A → ℕ → list A → list A ≝
245λA,deflt,new_length,l.
246  if leb (|l|) new_length then
247    l @ make_list ? deflt (new_length - |l|)
248  else
249    lhd … l new_length.
250
251lemma length_make_list:
252  ∀A: Type[0].
253  ∀elt: A.
254  ∀n: nat.
255    length ? (make_list A elt n) = n.
256  #A #ELT #N
257  elim N normalize // qed.
258
259lemma length_lhd : ∀A,l,n.|lhd A l n| = min (|l|) n.
260#A #l elim l -l
261[ * //
262| #hd #tl #IH * normalize [%]
263  #n >IH normalize elim (leb ??) %
264]
265qed.
266
267lemma length_cast_list : ∀A,dflt,n,l.|cast_list A dflt n l| = n.
268#A #dflt #n #l
269normalize @leb_elim #H normalize
270[ >length_append >length_make_list
271  @sym_eq @minus_to_plus //
272| >length_lhd normalize @leb_elim
273  [ #abs elim (absurd ? abs H) ]
274  #_ %
275]
276qed.
277
278definition translate_op_asym_unsigned :
279  ∀globals.Op2 → list register → list psd_argument → list psd_argument →
280  list (joint_seq RTL globals) ≝
281  λglobals,op,destrs,srcrs1,srcrs2.
282  let l ≝ |destrs| in
283  let srcrs1' ≝ cast_list ? (zero_byte : psd_argument) l srcrs1 in
284  let srcrs2' ≝ cast_list ? (zero_byte : psd_argument) l srcrs2 in
285  translate_op globals op destrs srcrs1' srcrs2' ??.
286  @hide_prf
287  normalize nodelta
288  >length_cast_list [2: >length_cast_list ] %
289qed.
290
291definition zero_args : ∀size.Σl : list psd_argument.|l| = size ≝
292λsize.
293«make_list psd_argument (zero_byte) size, length_make_list …».
294
295definition one_args : ∀size.Σl : list psd_argument.|l| = size ≝
296λsize.match size return λsize.Σl : list psd_argument.|l| = size with
297[ O ⇒ «[ ], refl …»
298| S k ⇒ (byte_of_nat 1 : psd_argument) :: zero_args k
299].
300whd in ⊢ (??%?); @eq_f @pi2 qed.
301
302definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with
303  [ Ointconst size _ _ ⇒ size_intsize size
304  | _ ⇒ 2
305  ].
306
307definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst.
308  match cst with
309  [ Oaddrsymbol id _ ⇒ bool_to_Prop (id ∈ globals)
310  | _ ⇒ True
311  ].
312
313definition translate_cst :
314  ∀ty.
315  ∀globals: list ident.
316  ∀cst_sig: Σcst : constant ty.cst_well_defd ty globals cst.
317  ∀destrs: list register.
318  |destrs| = size_of_cst ? cst_sig →
319  bind_new register (list (joint_seq RTL globals))
320 ≝
321  λty,globals,cst_sig,destrs.
322  match pi1 … cst_sig in constant return λty'.λx : constant ty'.
323      cst_well_defd ty' ? x → |destrs| = size_of_cst ty' x → ?
324  with
325  [ Ointconst size sign const ⇒ λcst_prf,prf.
326      map2 … (λr.λb : Byte.r ← b) destrs
327        (split_into_bytes size const) ?
328  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
329    let 〈r1, r2〉 ≝ make_addr … destrs ? in
330    let off ≝ bitvector_of_nat 16 offset in
331    [ ADDRESS RTL globals id ? off r1 r2 ]
332  | Oaddrstack offset ⇒ λcst_prf,prf.
333    let 〈r1, r2〉 ≝ make_addr … destrs ? in
334    (rtl_stack_address r1 r2 : joint_seq RTL globals) ::
335    if eqb offset 0 then [ ] else
336    translate_op … Add
337      [r1 ; r2 ] [ r1 ; r2 ] [ byte_of_nat … offset ; zero_byte ]
338      (refl …) (refl …)
339  ] (pi2 … cst_sig).
340  @hide_prf
341  [ cases (split_into_bytes ??) #lst
342    #EQ >EQ >prf whd in ⊢ (??%?); cases size %
343  | @cst_prf
344  |*: >prf %
345  ]
346qed.
347 
348definition translate_move :
349  ∀globals.
350  ∀destrs: list register.
351  ∀srcrs: list psd_argument.
352  |destrs| = |srcrs| → list (joint_seq RTL globals) ≝
353  λglobals,destrs,srcrs,length_eq.
354  map2 … (λdst,src.dst ← src) destrs srcrs length_eq.
355
356definition sign_mask : ∀globals.register → psd_argument →
357  list (joint_seq RTL globals) ≝
358    (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that:
359       byte in destr if srcr is: neg   |  pos
360       destr ← srcr | 127       11...1 | 01...1
361       destr ← destr <rot< 1    1...11 | 1...10
362       destr ← INC destr        0....0 | 1....1
363       destr ← CPL destr        1....1 | 0....0
364     *)
365  λglobals,destr,srca.
366  match srca with
367  [ Reg srcr ⇒
368    let byte_127 : Byte ≝ false ::: maximum ? in
369    [destr ← srcr .Or. byte_127 ;
370     destr ← .Rl. destr ;
371     destr ← .Inc. destr ;
372     destr ← .Cmpl. destr ]
373  | Imm b ⇒
374    if sign_bit … b then
375      [ destr ← (maximum … : Byte) ]
376    else
377      [ destr ← zero_byte ]
378  ].
379
380definition translate_cast_signed :
381  ∀globals : list ident.
382  list register → psd_argument →
383  bind_new register (list (joint_seq RTL globals)) ≝
384  λglobals,destrs,srca.
385  ν tmp in
386  (sign_mask ? tmp srca @
387  translate_move ? destrs (make_list ? (Reg ? tmp) (|destrs|)) ?).
388 >length_make_list % qed.
389
390definition translate_fill_with_zero :
391  ∀globals : list ident.
392  list register → list (joint_seq RTL globals) ≝
393  λglobals,destrs.
394  translate_move ? destrs (zero_args (|destrs|)) ?.
395  @sym_eq @pi2 qed.
396
397let rec last A (l : list A) on l : option A ≝
398match l with
399[ nil ⇒ None ?
400| cons hd tl ⇒
401  match tl with
402  [ nil ⇒ Some ? hd
403  | _ ⇒ last A tl
404  ]
405].
406
407lemma last_def : ∀A,hd,tl.last A (hd @ [tl]) = Some ? tl.
408#A #hd elim hd -hd [ #tl % ] #hd * [ #_ #last % ] #hd' #tl #IH #last
409@IH qed.
410
411lemma last_not_empty : ∀A,l.not_empty A l →
412  match last A l with
413  [ None ⇒ False
414  | _ ⇒ True ].
415#A @list_elim_left [*] #pref #last #_ #_ >last_def % qed.
416
417definition translate_op_asym_signed :
418  (* first argument will dictate size, second will be casted signedly *)
419  ∀globals.Op2 → list register → list psd_argument → list psd_argument →
420  bind_new register (list (joint_seq RTL globals)) ≝
421  λglobals,op,destrs,srcrs1,srcrs2.
422  νtmp1,tmp2 in
423  let l ≝ |destrs| in
424  let cast_srcrs ≝ λsrcrs,tmp.
425    let srcrs_l ≝ |srcrs| in
426    if leb (S srcrs_l) l then
427      match last ? srcrs with
428      [ Some last ⇒
429        〈srcrs @ make_list … (Reg ? tmp) (l - srcrs_l),
430         sign_mask … tmp last〉
431      | None ⇒
432        〈make_list … (zero_byte : psd_argument) l, [ ]〉
433      ]
434    else
435      〈lhd … srcrs l, [ ]〉 in
436  let prf : ∀srcrs,tmp.|destrs| = |\fst (cast_srcrs srcrs tmp)| ≝ ? in
437  let srcrs1init ≝ cast_srcrs srcrs1 tmp1 in
438  let srcrs2init ≝ cast_srcrs srcrs2 tmp2 in
439  \snd srcrs1init @@ \snd srcrs2init @@
440  translate_op globals op destrs (\fst srcrs1init) (\fst srcrs2init) ??.
441  @hide_prf
442  [ @prf | <prf @prf ]
443  #srcrs #tmp normalize nodelta
444  @leb_elim #H normalize nodelta
445  [ cases (last ??) normalize nodelta
446    [ >length_make_list %
447    | #_ >length_append >length_make_list
448      @minus_to_plus [ @(transitive_le … H) ] //
449    ]
450  | >length_lhd lapply (le_S_S_to_le … (not_le_to_lt … H))
451    lapply (|destrs|) lapply (|srcrs|) -destrs
452    #n #m * -n [2: #n #H] whd in ⊢ (???%); [2: @if_elim #_ % ]
453    >not_le_to_leb_false [%] @lt_to_not_le @le_S_S assumption
454  ]
455qed.
456
457(* using size of lists as size of ints *)
458definition translate_cast :
459  ∀globals: list ident.
460  signedness → list register → list register →
461    bind_new register (list (joint_seq RTL globals)) ≝
462  λglobals,src_sign,destrs,srcrs.
463  match reduce_strong ?? srcrs destrs with
464  [ mk_Sig t prf ⇒
465    let src_common ≝ \fst (\fst t) in
466    let src_rest   ≝ \snd (\fst t) in
467    let dst_common ≝ \fst (\snd t) in
468    let dst_rest   ≝ \snd (\snd t) in
469    (* first, move the common part *)
470    translate_move ? dst_common (map … (Reg ?) src_common) ? @@
471    match src_rest return λ_.bind_new ?? with
472    [ nil ⇒ (* upcast *)
473      match src_sign return λ_.bind_new ?? with
474      [ Unsigned ⇒ translate_fill_with_zero ? dst_rest
475      | Signed ⇒
476        match last … srcrs (* = src_common *) with
477        [ Some src_last ⇒ translate_cast_signed ? dst_rest src_last
478        | None ⇒ (* srcrs is empty *) translate_fill_with_zero ? dst_rest
479        ]
480      ]
481    | _ ⇒ (* downcast, nothing else to do *) [ ]
482    ]
483  ].
484  >length_map >prf % qed.
485 
486definition translate_notint :
487  ∀globals : list ident.
488  ∀destrs : list register.
489  ∀srcrs_arg : list register.
490  |destrs| = |srcrs_arg| → list (joint_seq RTL globals) ≝
491  λglobals, destrs, srcrs, prf.
492  map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf.
493
494definition translate_negint : ∀globals.? → ? → ? → list (joint_seq RTL globals) ≝
495  λglobals: list ident.
496  λdestrs: list register.
497  λsrcrs: list register.
498  λprf: |destrs| = |srcrs|. (* assert in caml code *)
499  translate_notint … destrs srcrs prf @
500  translate_op ? Add destrs (map … (Reg ?) destrs) (one_args (|destrs|)) ??.
501@hide_prf
502>length_map [ @sym_eq @pi2 | % ] qed.
503
504definition translate_notbool:
505  ∀globals : list ident.
506  list register → list register →
507    bind_new register (list (joint_seq RTL globals)) ≝
508  λglobals,destrs,srcrs.
509  match destrs with
510  [ nil ⇒ [ ]
511  | cons destr destrs' ⇒
512    translate_fill_with_zero ? destrs' @@
513    match srcrs return λ_.bind_new ?? with
514    [ nil ⇒ [destr ← zero_byte]
515    | cons srcr srcrs' ⇒
516      (destr ← srcr) :::
517      map register (joint_seq RTL globals) (λr. destr ← destr .Or. r) srcrs' @@
518      (* now destr is non-null iff srcrs was non-null *)
519      CLEAR_CARRY ?? :::
520      (* many uses of 0, better not use immediates *)
521      ν tmp in
522      [tmp ← zero_byte ;
523       destr ← tmp .Sub. tmp ;
524       (* now carry bit is set iff destr was non-null *)
525       destr ← tmp .Addc. tmp]
526     ]
527   ].
528
529definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? →
530  bind_new register (list (joint_seq RTL globals)) ≝
531  λglobals.
532  λty, ty'.
533  λop1: unary_operation ty ty'.
534  λdestrs: list register.
535  λsrcrs: list register.
536  λprf1: |destrs| = size_of_sig_type ty'.
537  λprf2: |srcrs| = size_of_sig_type ty.
538  match op1
539  return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' →
540    bind_new register (list (joint_seq RTL globals)) with
541  [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2.
542    translate_cast globals src_sign destrs srcrs
543  | Onegint sz sg ⇒ λeq1,eq2.
544    translate_negint globals destrs srcrs ?
545  | Onotbool _ _ _ _ ⇒ λeq1,eq2.
546    translate_notbool globals destrs srcrs
547  | Onotint sz sg ⇒ λeq1,eq2.
548    translate_notint globals destrs srcrs ?
549  | Optrofint sz sg ⇒ λeq1,eq2.
550    translate_cast globals Unsigned destrs srcrs
551  | Ointofptr sz sg ⇒ λeq1,eq2.
552    translate_cast globals Unsigned destrs srcrs
553  | Oid t ⇒ λeq1,eq2.
554      translate_move globals destrs (map … (Reg ?) srcrs) ?
555  | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *)
556  ] (refl …) (refl …).
557  @hide_prf
558  destruct >prf1 >prf2 [3: >length_map ] //
559qed.
560
561include alias "arithmetics/nat.ma".
562
563definition translate_mul_i :
564  ∀globals.
565  register → register →
566  (* size of destination and sources *)
567  ∀n : ℕ.
568  (* the temporary destination, with a dummy register at the end *)
569  ∀tmp_destrs_dummy : list register.
570  ∀srcrs1,srcrs2 : list psd_argument.
571  |tmp_destrs_dummy| = S n →
572  n = |srcrs1| →
573  |srcrs1| = |srcrs2| →
574  (* the position of the least significant byte of the result we compute at
575     this stage (goes from 0 to n in the main function) *)
576  ∀k : ℕ.
577  lt k n →
578  (* the position of the byte in the first source we will use in this stage.
579     the position in the other source will be k - i *)
580  (Σi.i<S k) →
581  (* the accumulator *)
582  list (joint_seq RTL globals) →
583    list (joint_seq RTL globals) ≝
584  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
585    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
586  (* the following will expand to
587     a, b ← srcrs1[i] * srcrs2[k-i]
588     tmp_destrs_dummy[k]   ← tmp_destrs_dummy[k] + a
589     tmp_destrs_dummy[k+1] ← tmp_destrs_dummy[k+1] + b + C
590     tmp_destrs_dummy[k+2] ← tmp_destrs_dummy[k+2] + 0 + C
591     ...
592     tmp_destrs_dummy[n]   ← tmp_destrs_dummy[n] + 0 + C
593     ( all calculations on tmp_destrs_dummy[n] will be eliminated with
594     liveness analysis) *)
595  match i_sig with
596    [ mk_Sig i i_prf ⇒
597      (* we pad the result of a byte multiplication with zeros in order
598         for the bit to be carried. Redundant calculations will be eliminated
599         by constant propagation. *)
600      let args : list psd_argument ≝
601        [Reg ? a;Reg ? b] @ make_list ? (zero_byte : psd_argument) (n - 1 - k) in
602      let tmp_destrs_view : list register ≝
603        ltl ? tmp_destrs_dummy k in
604      [❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?)] @
605      translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @
606      acc
607    ].
608@hide_prf
609[ <srcrs1_prf
610  @(transitive_le … i_prf k_prf)
611| @lt_plus_to_minus [ @le_S_S_to_le assumption | <srcrs2_prf <srcrs1_prf
612  whd >(plus_n_O (S k)) @le_plus // ]
613| >length_map %
614| >length_map
615  >length_ltl
616  >tmp_destrs_dummy_prf >length_append
617  >length_make_list
618  normalize in ⊢ (???(?%?));
619  cases n in k_prf; [ #ABS cases (absurd ? ABS ?) /2 by le_to_not_lt/ ]
620  #n' #k_prf >minus_S_S <minus_n_O
621  >plus_minus_commutative [%] @le_S_S_to_le assumption
622] qed.
623
624definition translate_mul : ∀globals.?→?→?→?→?→bind_new register (list (joint_seq RTL globals)) ≝
625λglobals : list ident.
626λdestrs : list register.
627λsrcrs1 : list psd_argument.
628λsrcrs2 : list psd_argument.
629λsrcrs1_prf : |destrs| = |srcrs1|.
630λsrcrs2_prf : |srcrs1| = |srcrs2|.
631(* needed fresh registers *)
632νa in
633νb in
634(* temporary registers for the result are created, so to avoid overwriting
635   sources *)
636νν |destrs| as tmp_destrs with tmp_destrs_prf in
637νdummy in
638(dummy ← byte_of_nat 0) :::
639(* the step calculating all products with least significant byte going in the
640   k-th position of the result *)
641let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq RTL globals) →
642  list (joint_seq RTL globals) ≝
643  λk_sig,acc.match k_sig with
644  [ mk_Sig k k_prf ⇒
645    foldr … (translate_mul_i ? a b (|destrs|)
646      (tmp_destrs @ [dummy]) srcrs1 srcrs2
647      ? srcrs1_prf srcrs2_prf k k_prf) acc (range_strong (S k))
648  ] in
649(* initializing tmp_destrs to zero
650   dummy is intentionally uninitialized *)
651translate_fill_with_zero … tmp_destrs @
652(* the main body, roughly:
653   for k in 0 ... n-1 do
654     for i in 0 ... k do
655       translate_mul_i … k … i *)
656foldr … translate_mul_k [ ] (range_strong (|destrs|)) @
657(* epilogue: saving the result *)
658translate_move … destrs (map … (Reg ?) tmp_destrs) ?.
659@hide_prf
660[ >length_append  <plus_n_Sm <plus_n_O //
661| >length_map >tmp_destrs_prf //
662]
663qed.
664
665definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→
666    bind_new register (list (joint_seq RTL globals)) ≝
667  λglobals: list ident.
668  λdiv_not_mod: bool.
669  λdestrs: list register.
670  λsrcrs1: list psd_argument.
671  λsrcrs2: list psd_argument.
672  λsrcrs1_prf : |destrs| = |srcrs1|.
673  λsrcrs2_prf : |srcrs1| = |srcrs2|.
674  match destrs return λx.x = destrs → bind_new ?? with
675  [ nil ⇒ λ_.[ ]
676  | cons destr destrs' ⇒ λeq_destrs.
677    match destrs' with
678    [ nil ⇒
679      match srcrs1 return λx.x = srcrs1 → bind_new ??  with
680      [ nil ⇒ λeq_srcrs1.⊥
681      | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
682        match srcrs2 return λx.x = srcrs2 → bind_new ??  with
683        [ nil ⇒ λeq_srcrs2.⊥
684        | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
685          νdummy in
686          let 〈destr1, destr2〉 ≝
687            if div_not_mod then 〈destr, dummy〉 else 〈dummy, destr〉 in
688          [❮destr1, destr2❯ ← srcr1 .DivuModu. srcr2]
689        ] (refl …)
690      ] (refl …)
691    | _ ⇒ ? (* not implemented *)
692    ]
693  ] (refl …).
694[3: elim not_implemented]
695@hide_prf
696destruct normalize in srcrs1_prf srcrs2_prf; destruct qed.
697
698(* Paolo: to be moved elsewhere *)
699let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (f : A→B→C→C) (init : C) (l1 : list A) (l2 : list B)
700  (prf : |l1| = |l2|) on l1 : C ≝
701  match l1 return λx.x = l1 → C with 
702  [ nil ⇒ λ_.init
703  | cons a l1' ⇒ λeq_l1.
704    match l2 return λy.y = l2 → C with
705    [ nil ⇒ λeq_l2.⊥
706    | cons b l2' ⇒ λeq_l2.
707      f a b (foldr2 A B C f init l1' l2' ?)
708    ] (refl …)
709  ] (refl …).
710@hide_prf
711destruct normalize in prf;  [destruct|//]
712qed.
713
714definition translate_ne: ∀globals: list ident.?→?→?→?→
715  bind_new register (list (joint_seq RTL globals)) ≝
716  λglobals: list ident.
717  λdestrs: list register.
718  λsrcrs1: list psd_argument.
719  λsrcrs2: list psd_argument.
720  match destrs return λ_.|srcrs1| = |srcrs2| → bind_new ?? with
721  [ nil ⇒ λ_.[ ]
722  | cons destr destrs' ⇒ λEQ.
723    translate_fill_with_zero … destrs' @@
724    match srcrs1 return λx.|x| = |srcrs2| → bind_new ?? with
725    [ nil ⇒ λ_.[destr ← zero_byte]
726    | cons srcr1 srcrs1' ⇒
727      match srcrs2 return λx.S (|srcrs1'|) = |x| → bind_new ?? with
728      [ nil ⇒ λEQ.⊥
729      | cons srcr2 srcrs2' ⇒ λEQ.
730        νtmpr in
731        let f : psd_argument → psd_argument → list (joint_seq RTL globals) → list (joint_seq RTL globals) ≝
732          λs1,s2,acc.
733          tmpr  ← s1 .Xor. s2 ::
734          destr ← destr .Or. tmpr ::
735          acc in
736        let epilogue : list (joint_seq RTL globals) ≝
737          [ CLEAR_CARRY ?? ;
738            tmpr ← zero_byte .Sub. destr ;
739            (* now carry bit is 1 iff destrs != 0 *)
740            destr ← zero_byte .Addc. zero_byte ] in
741         destr ← srcr1 .Xor. srcr2 ::
742         foldr2 ??? f epilogue srcrs1' srcrs2' ?
743       ]
744     ] EQ
745   ].
746@hide_prf normalize in EQ; destruct(EQ) assumption qed.
747
748(* if destrs is 0 or 1, it inverses it. To be used after operations that
749   ensure this. *)
750definition translate_toggle_bool : ∀globals.?→bind_new register (list (joint_seq RTL globals)) ≝
751  λglobals: list ident.
752  λdestrs: list register.
753  match destrs with
754  [ nil ⇒ [ ]
755  | cons destr _ ⇒ [destr ← destr .Xor. byte_of_nat 1]
756  ].
757 
758definition translate_lt_unsigned :
759  ∀globals.
760  ∀destrs: list register.
761  ∀srcrs1: list psd_argument.
762  ∀srcrs2: list psd_argument.
763  |srcrs1| = |srcrs2| →
764  bind_new register (list (joint_seq RTL globals)) ≝
765  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
766  match destrs with
767  [ nil ⇒ [ ]
768  | cons destr destrs' ⇒
769    ν tmpr in
770    (translate_fill_with_zero … destrs' @@
771    (* I perform a subtraction, but the only interest is in the carry bit *)
772    translate_op ? Sub (make_list … tmpr (|srcrs1|)) srcrs1 srcrs2 ? srcrs_prf @@
773    [ destr ← zero_byte .Addc. zero_byte ])
774  ].
775@hide_prf
776>length_make_list % qed.
777
778(* shifts signed integers by adding 128 to the most significant byte
779   it replaces it with a fresh register which must be provided *)
780let rec shift_signed globals
781  (tmp : register)
782  (srcrs : list psd_argument) on srcrs :
783  Σt : (list psd_argument) × (list (joint_seq RTL globals)).|\fst t| = |srcrs| ≝
784  let byte_128 : Byte ≝ true ::: bv_zero ? in
785  match srcrs with
786  [ nil ⇒ 〈[ ],[ ]〉
787  | cons srcr srcrs' ⇒
788    match srcrs' with
789    [ nil ⇒ 〈[ Reg ? tmp ], [ tmp ← srcr .Add. byte_128 ]〉
790    | _ ⇒
791      let re ≝ shift_signed globals tmp srcrs' in
792      〈srcr :: \fst re, \snd re〉
793    ]
794  ].
795@hide_prf
796[1,2: %
797|*: cases re * #a #b >p1 normalize #EQ >EQ %
798] qed.
799
800definition translate_lt_signed :
801  ∀globals.
802  ∀destrs: list register.
803  ∀srcrs1: list psd_argument.
804  ∀srcrs2: list psd_argument.
805  |srcrs1| = |srcrs2| →
806  bind_new register (list (joint_seq RTL globals)) ≝
807  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
808  νtmp_last_s1 in
809  νtmp_last_s2 in
810  let p1 ≝ shift_signed globals tmp_last_s1 srcrs1 in
811  let new_srcrs1 ≝ \fst p1 in
812  let shift_srcrs1 ≝ \snd p1 in
813  let p2 ≝ shift_signed globals tmp_last_s2 srcrs2 in
814  let new_srcrs2 ≝ \fst p2 in
815  let shift_srcrs2 ≝ \snd p2 in
816  shift_srcrs1 @@ shift_srcrs2 @@
817  translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ?.
818@hide_prf
819whd in match new_srcrs1; whd in match new_srcrs2;
820cases p1
821cases p2
822//
823qed.
824
825definition translate_lt : bool→∀globals.?→?→?→?→bind_new register (list (joint_seq RTL globals)) ≝
826  λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf.
827  if is_unsigned then
828    translate_lt_unsigned globals destrs srcrs1 srcrs2 srcrs_prf
829  else
830    translate_lt_signed globals destrs srcrs1 srcrs2 srcrs_prf.
831
832definition translate_cmp ≝
833  λis_unsigned,globals,cmp,destrs,srcrs1,srcrs2,srcrs_prf.
834  match cmp with
835  [ Ceq ⇒
836    translate_ne globals destrs srcrs1 srcrs2 srcrs_prf @@
837    translate_toggle_bool globals destrs
838  | Cne ⇒
839    translate_ne globals destrs srcrs1 srcrs2 srcrs_prf
840  | Clt ⇒
841    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf
842  | Cgt ⇒
843    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ?
844  | Cle ⇒
845    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? @@
846    translate_toggle_bool globals destrs
847  | Cge ⇒
848    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf @@
849    translate_toggle_bool globals destrs
850  ]. @sym_eq assumption qed.
851
852definition translate_op2 :
853  ∀globals.∀ty1,ty2,ty3.∀op : binary_operation ty1 ty2 ty3.
854  ∀destrs : list register.
855  ∀srcrs1,srcrs2 : list psd_argument.
856  |destrs| = size_of_sig_type ty3 →
857  |srcrs1| = size_of_sig_type ty1 →
858  |srcrs2| = size_of_sig_type ty2 →
859  bind_new register (list (joint_seq RTL globals)) ≝
860  λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2.
861  match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3.
862    ? = size_of_sig_type ty3 → ? = size_of_sig_type ty1 → ? = size_of_sig_type ty2 →
863    bind_new ?? with
864  [ Oadd sz sg ⇒ λprf1,prf2,prf3.
865    translate_op globals Add destrs srcrs1 srcrs2 ??
866  | Oaddpi sz ⇒ λprf1,prf2,prf3.
867    translate_op_asym_signed globals Add destrs srcrs1 srcrs2
868  | Oaddip sz ⇒ λprf1,prf2,prf3.
869    translate_op_asym_signed globals Add destrs srcrs2 srcrs1
870  | Osub sz sg ⇒ λprf1,prf2,prf2.
871    translate_op globals Sub destrs srcrs1 srcrs2 ??
872  | Osubpi sz ⇒ λprf1,prf2,prf3.
873    translate_op_asym_signed globals Add destrs srcrs1 srcrs2
874  | Osubpp sz ⇒ λprf1,prf2,prf3.
875    translate_op_asym_unsigned globals Sub destrs srcrs1 srcrs2
876  | Omul sz sg ⇒ λprf1,prf2,prf3.
877    translate_mul globals destrs srcrs1 srcrs2 ??
878  | Odivu sz ⇒ λprf1,prf2,prf3.
879    translate_divumodu8 globals true destrs srcrs1 srcrs2 ??
880  | Omodu sz ⇒ λprf1,prf2,prf3.
881    translate_divumodu8 globals false destrs srcrs1 srcrs2 ??
882  | Oand sz sg ⇒ λprf1,prf2,prf3.
883    translate_op globals And destrs srcrs1 srcrs2 ??
884  | Oor sz sg ⇒ λprf1,prf2,prf3.
885    translate_op globals Or destrs srcrs1 srcrs2 ??
886  | Oxor sz sg ⇒ λprf1,prf2,prf3.
887    translate_op globals Xor destrs srcrs1 srcrs2 ??
888  | Ocmp sz sg1 sg2 c ⇒ λprf1,prf2,prf3.
889    translate_cmp false globals c destrs srcrs1 srcrs2 ?
890  | Ocmpu sz sg c ⇒ λprf1,prf2,prf3.
891    translate_cmp true globals c destrs srcrs1 srcrs2 ?
892  | Ocmpp sg c ⇒ λprf1,prf2,prf3.
893    translate_cmp true globals c destrs srcrs1 srcrs2 ?
894  | _ ⇒ ⊥ (* assert false, implemented in run time or float op *)
895  ]. try @not_implemented @hide_prf //
896  qed.
897
898definition translate_cond: ∀globals: list ident. list register → label →
899  bind_step_block RTL globals ≝
900  λglobals: list ident.
901  λsrcrs: list register.
902  λlbl_true: label.
903  match srcrs return λ_.bind_step_block RTL ? with
904  [ nil ⇒ bret … [ ]
905  | cons srcr srcrs' ⇒
906    ν tmpr in
907    let f : register → label → joint_seq RTL globals ≝
908      λr.λ_. tmpr ← tmpr .Or. r in
909    bret …
910    〈(λ_.MOVE RTL globals 〈tmpr,srcr〉) ::
911     map ?? f srcrs',
912     λ_.COND … tmpr lbl_true, [ ]〉
913  ].
914
915(* Paolo: to be controlled (original seemed overly complex) *)
916definition translate_load : ∀globals.?→?→?→bind_new register ? ≝
917  λglobals: list ident.
918  λaddr : list psd_argument.
919  λaddr_prf: 2 = |addr|.
920  λdestrs: list register.
921  ν tmp_addr_l in
922  ν tmp_addr_h in
923  (translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
924  let f ≝ λdestr : register.λacc : bind_new register (list (joint_seq RTL globals)).
925    [LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h)] @@
926    translate_op ? Add
927      [tmp_addr_l ; tmp_addr_h]
928      [tmp_addr_l ; tmp_addr_h]
929      [(int_size : Byte) ; zero_byte ] ? ? @@ acc in
930  foldr … f [ ] destrs).
931@hide_prf
932[ <addr_prf ] % qed.
933 
934definition translate_store : ∀globals.?→?→?→bind_new register ? ≝
935  λglobals: list ident.
936  λaddr : list psd_argument.
937  λaddr_prf: 2 = |addr|.
938  λsrcrs: list psd_argument.
939  ν tmp_addr_l in
940  ν tmp_addr_h in
941  (translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
942  let f ≝ λsrcr : psd_argument.λacc : bind_new register (list (joint_seq RTL globals)).
943    [STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr] @@
944    translate_op … Add
945      [tmp_addr_l ; tmp_addr_h]
946      [tmp_addr_l ; tmp_addr_h]
947      [(int_size : Byte) ; zero_byte ] ? ? @@ acc in
948  foldr … f [ ] srcrs).
949@hide_prf [ <addr_prf ] % qed.
950
951lemma lenv_typed_reg_typed_ok1 :
952  ∀locals,env,r,ty.
953  local_env_typed locals env →
954  Exists ? (λx:register×typ.〈r,ty〉=x) locals →
955  ∀prf.
956  |find_local_env r env prf| = size_of_sig_type ty.
957#locals #env #r #ty #env_typed #r_ok
958elim (Exists_All … r_ok env_typed)
959* #r' #ty' * #EQ destruct(EQ) * #rs * #EQ1 #EQ2 #prf
960whd in match find_local_env; normalize nodelta
961@opt_safe_elim #rs' >EQ1 #EQ' destruct assumption
962qed.
963
964lemma lenv_typed_arg_typed_ok1 :
965  ∀locals,env,r,ty.
966  local_env_typed locals env →
967  Exists ? (λx:register×typ.〈r,ty〉=x) locals →
968  ∀prf.
969  |find_local_env_arg r env prf| = size_of_sig_type ty.
970#locals #env #r #ty #env_typed #r_ok #prf
971whd in match find_local_env_arg; normalize nodelta
972>length_map @lenv_typed_reg_typed_ok1 assumption
973qed.
974
975lemma lenv_typed_reg_typed_ok2 :
976  ∀locals,env,r,ty.
977  local_env_typed locals env →
978  Exists ? (λx:register×typ.〈r,ty〉=x) locals →
979  r ∈ env.
980#locals #env #r #ty #env_typed #r_ok
981elim (Exists_All … r_ok env_typed)
982* #r' #ty' * #EQ destruct(EQ) * #rs * #EQ1 #EQ2
983whd in ⊢ (?%);
984>EQ1 %
985qed.
986
987lemma cst_size_ok : ∀ty,cst.size_of_sig_type ty=size_of_cst ty cst.
988#ty * -ty [*] //
989qed.
990
991(* TODO: move it *)
992definition ensure_bind_step_block : ∀p : params.∀g.
993  bind_new register (list (joint_seq p g)) → bind_step_block p g ≝
994  λp,g,b.! l ← b; bret ? (step_block p g) l.
995
996coercion bind_step_block_from_bind_list nocomposites :
997  ∀p : params.∀g.
998  ∀b : bind_new register (list (joint_seq p g)).bind_step_block p g ≝
999  ensure_bind_step_block on _b : bind_new register (list (joint_seq ??)) to
1000  bind_step_block ??.
1001
1002definition translate_statement : ∀globals, locals.∀env.
1003  local_env_typed locals env →
1004  ∀stmt : statement.statement_typed locals stmt →
1005  𝚺b :
1006  bind_step_block RTL globals +
1007  bind_fin_block RTL globals.
1008  match b with [ inl _ ⇒ label | _ ⇒ unit] ≝
1009  λglobals,locals,lenv,lenv_typed,stmt.
1010  match stmt return λstmt.statement_typed locals stmt → 𝚺b: bind_step_block RTL globals ⊎ bind_fin_block RTL globals.match b with [ inl _ ⇒ label | _ ⇒ unit ] with
1011  [ St_skip lbl' ⇒ λstmt_typed.
1012    ❬inl … (bret … [ ]), lbl'❭
1013  | St_cost cost_lbl lbl' ⇒ λstmt_typed.
1014    ❬inl … (bret … 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉), lbl'❭
1015  | St_const ty destr cst lbl' ⇒ λstmt_typed.
1016    ❬inl … (translate_cst ty globals cst (find_local_env destr lenv ?) ?), lbl'❭
1017  | St_op1 ty ty' op1 destr srcr lbl' ⇒ λstmt_typed.
1018    ❬inl … (translate_op1 globals ty' ty op1
1019      (find_local_env destr lenv ?)
1020      (find_local_env srcr lenv ?) ??), lbl'❭
1021  | St_op2 ty1 ty2 ty3 op2 destr srcr1 srcr2 lbl' ⇒ λstmt_typed.
1022    ❬inl … (translate_op2 globals … op2
1023      (find_local_env destr lenv ?)
1024      (find_local_env_arg srcr1 lenv ?)
1025      (find_local_env_arg srcr2 lenv ?) ???), lbl'❭
1026    (* XXX: should we be ignoring this? *)
1027  | St_load ignore addr destr lbl' ⇒ λstmt_typed.
1028    ❬inl … (translate_load globals
1029      (find_local_env_arg addr lenv ?) ? (find_local_env destr lenv ?)), lbl'❭
1030    (* XXX: should we be ignoring this? *)
1031  | St_store ignore addr srcr lbl' ⇒ λstmt_typed.
1032    ❬inl … (translate_store globals (find_local_env_arg addr lenv ?) ?
1033      (find_local_env_arg srcr lenv ?)), lbl'❭
1034  | St_call_id f args retr lbl' ⇒ λstmt_typed.
1035    ❬inl … (bret …
1036      〈[ ],λ_.CALL RTL ? (inl ?? f) (rtl_args args lenv ?)
1037        (match retr with
1038         [ Some retr ⇒
1039           find_local_env retr lenv ?
1040         | None ⇒ [ ]
1041         ]), [ ]〉), lbl'❭
1042  | St_call_ptr f args retr lbl' ⇒ λstmt_typed.
1043    let fs ≝ find_and_addr_arg f lenv ?? in
1044    ❬inl … (bret …
1045      〈[ ],λ_.CALL RTL ? (inr ?? fs) (rtl_args args lenv ?)
1046        (match retr with
1047         [ Some retr ⇒
1048           find_local_env retr lenv ?
1049         | None ⇒ [ ]
1050         ]), [ ]〉), lbl'❭
1051  | St_cond r lbl_true lbl_false ⇒ λstmt_typed.
1052    ❬inl … (translate_cond globals (find_local_env r lenv ?) lbl_true), lbl_false❭
1053  | St_return ⇒ λ_. ❬inr … (bret … 〈[ ], RETURN ?〉),it❭
1054  ].
1055  @hide_prf
1056  [ cases daemon (* needs more hypotheses *)
1057  | @(lenv_typed_reg_typed_ok2 … lenv_typed stmt_typed)
1058  | >(lenv_typed_reg_typed_ok1 … lenv_typed stmt_typed)
1059    @cst_size_ok
1060  |4,5,6,7: cases stmt_typed #dstr_typed #srcr_typed
1061    [3,4: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption
1062    |2: @(lenv_typed_reg_typed_ok2 … lenv_typed srcr_typed)
1063    |1: @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_typed)
1064    ]
1065  |8,9,10,11,12,13:
1066    cases stmt_typed * #srcrs1_prf #srcrs2_prf #dstr_prf
1067    [5,6: @(lenv_typed_arg_typed_ok1 … lenv_typed) assumption
1068    |4: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption
1069    |3: @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs2_prf)
1070    |2: @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs1_prf)
1071    |1: @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_prf)
1072    ]
1073  |*: cases daemon (* TODO  *)
1074  ]
1075qed.
1076
1077definition translate_internal :
1078  ∀globals.internal_function → (* insert here more properties *)
1079  joint_closed_internal_function RTL globals ≝
1080  λglobals: list ident.
1081  λdef.
1082  let runiverse' ≝ f_reggen def in
1083  let luniverse' ≝ f_labgen def in
1084  let stack_size' ≝ f_stacksize def in
1085  let entry' ≝ pi1 … (f_entry def) in
1086  let init ≝ mk_joint_internal_function RTL globals
1087    luniverse' runiverse' [ ] [ ] 0 0 0
1088    (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) entry' in
1089  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
1090    (f_locals def) (f_params def) (f_result def) init in
1091  let vars ≝ (f_locals def) @ (f_params def) @
1092    match f_result def with [ Some x ⇒ [x] | _ ⇒ [ ] ] in
1093  let f_trans ≝ λlbl,stmt,def.
1094    let pr ≝ translate_statement … vars lenv ? stmt ? in
1095    match dpi1 … pr return λx.match x with [ inl _ ⇒ label | _ ⇒ unit ] → ? with
1096    [ inl instrs ⇒ λlbl'.b_adds_graph … instrs lbl lbl' def
1097    | inr instrs ⇒ λ_.b_fin_adds_graph … instrs lbl def
1098    ] (dpi2 … pr) in
1099  let def ≝ foldi … f_trans (f_graph def) init' in
1100  mk_joint_internal_function ??
1101    (joint_if_luniverse … def)
1102    (joint_if_runiverse … def)
1103    (joint_if_result … def)
1104    (joint_if_params … def)
1105    stack_size' 0 0
1106    (joint_if_code … def)
1107    (joint_if_entry … def).
1108(* TODO *) cases daemon
1109qed.
1110
1111(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
1112  because of CompCert heritage *)
1113definition rtlabs_to_rtl: (* initialization cost label *) costlabel →
1114  RTLabs_program → rtl_program ≝
1115 λinit_cost, p.
1116  mk_joint_program …
1117    (prog_funct_names \ldots p)
1118    (transform_program … p (λvarnames. transf_fundef … (translate_internal ?)))
1119    init_cost
1120    ?.
1121@hide_prf @transform_prog_funct_names qed.
1122
1123definition rtlabs_stack_cost : RTLabs_program → stack_cost_model ≝
1124λp.list_map_opt … (λi_f.
1125  match \snd i_f with [ Internal def ⇒ Some ? 〈\fst i_f, f_stacksize def〉
1126                      | External _ ⇒ None ?]) (prog_funct … p).
1127
1128lemma RTLabsToRTL_monotone_stacksizes :
1129∀cost,p_in.let p_out ≝ rtlabs_to_rtl cost p_in in
1130stack_cost_model_le (rtlabs_stack_cost p_in) (stack_cost ? p_out).
1131#cost #p_in whd
1132@list_map_opt_All2
1133[ @(λid_def1,id_def2.
1134   match \snd id_def1 with
1135   [ Internal f1 ⇒
1136     match \snd id_def2 with
1137     [ Internal f2 ⇒
1138       \fst id_def1 = \fst id_def2 ∧
1139       le (f_stacksize … f1) (joint_if_stacksize … f2)
1140     | _ ⇒ False
1141     ]
1142   | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ]
1143   ])
1144| * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %]
1145  ** #H %{H} % ]
1146@All2_of_map * #id * #f normalize nodelta [2: %]
1147% [%] whd in match translate_internal; whd in match joint_if_stacksize;
1148normalize nodelta
1149cases (initialize_locals_params_ret ?????) normalize nodelta #a #b %1
1150qed.
Note: See TracBrowser for help on using the repository browser.