source: src/RTLabs/RTLabsToRTL.ma @ 3004

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

fixed a bug where when doing an asymetrical op, cast initialization was inserted also when sizes matched

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