source: src/RTLabs/RTLabsToRTL.ma @ 3096

Last change on this file since 3096 was 3037, checked in by tranquil, 7 years ago
  • ADDRESS joint instruction now has also an offset
  • corrected call to pointer (needed to clear the accumulator)
  • now we make sure globals contain also function names

LINToASM will be fixed in an upcoming commit

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    let off ≝ bitvector_of_nat 16 offset in
330    [ ADDRESS RTL globals id ? off r1 r2 ]
331  | Oaddrstack offset ⇒ λcst_prf,prf.
332    let 〈r1, r2〉 ≝ make_addr … destrs ? in
333    (rtl_stack_address r1 r2 : joint_seq RTL globals) ::
334    if eqb offset 0 then [ ] else
335    translate_op … Add
336      [r1 ; r2 ] [ r1 ; r2 ] [ byte_of_nat … offset ; zero_byte ]
337      (refl …) (refl …)
338  ] (pi2 … cst_sig).
339  @hide_prf
340  [ cases (split_into_bytes ??) #lst
341    #EQ >EQ >prf whd in ⊢ (??%?); cases size %
342  | @cst_prf
343  |*: >prf %
344  ]
345qed.
346 
347definition translate_move :
348  ∀globals.
349  ∀destrs: list register.
350  ∀srcrs: list psd_argument.
351  |destrs| = |srcrs| → list (joint_seq RTL globals) ≝
352  λglobals,destrs,srcrs,length_eq.
353  map2 … (λdst,src.dst ← src) destrs srcrs length_eq.
354
355definition sign_mask : ∀globals.register → psd_argument →
356  list (joint_seq RTL globals) ≝
357    (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that:
358       byte in destr if srcr is: neg   |  pos
359       destr ← srcr | 127       11...1 | 01...1
360       destr ← destr <rot< 1    1...11 | 1...10
361       destr ← INC destr        0....0 | 1....1
362       destr ← CPL destr        1....1 | 0....0
363     *)
364  λglobals,destr,srca.
365  match srca with
366  [ Reg srcr ⇒
367    let byte_127 : Byte ≝ false ::: maximum ? in
368    [destr ← srcr .Or. byte_127 ;
369     destr ← .Rl. destr ;
370     destr ← .Inc. destr ;
371     destr ← .Cmpl. destr ]
372  | Imm b ⇒
373    if sign_bit … b then
374      [ destr ← (maximum … : Byte) ]
375    else
376      [ destr ← zero_byte ]
377  ].
378
379definition translate_cast_signed :
380  ∀globals : list ident.
381  list register → psd_argument →
382  bind_new register (list (joint_seq RTL globals)) ≝
383  λglobals,destrs,srca.
384  ν tmp in
385  (sign_mask ? tmp srca @
386  translate_move ? destrs (make_list ? (Reg ? tmp) (|destrs|)) ?).
387 >length_make_list % qed.
388
389definition translate_fill_with_zero :
390  ∀globals : list ident.
391  list register → list (joint_seq RTL globals) ≝
392  λglobals,destrs.
393  translate_move ? destrs (zero_args (|destrs|)) ?.
394  @sym_eq @pi2 qed.
395
396let rec last A (l : list A) on l : option A ≝
397match l with
398[ nil ⇒ None ?
399| cons hd tl ⇒
400  match tl with
401  [ nil ⇒ Some ? hd
402  | _ ⇒ last A tl
403  ]
404].
405
406lemma last_def : ∀A,hd,tl.last A (hd @ [tl]) = Some ? tl.
407#A #hd elim hd -hd [ #tl % ] #hd * [ #_ #last % ] #hd' #tl #IH #last
408@IH qed.
409
410lemma last_not_empty : ∀A,l.not_empty A l →
411  match last A l with
412  [ None ⇒ False
413  | _ ⇒ True ].
414#A @list_elim_left [*] #pref #last #_ #_ >last_def % qed.
415
416definition translate_op_asym_signed :
417  (* first argument will dictate size, second will be casted signedly *)
418  ∀globals.Op2 → list register → list psd_argument → list psd_argument →
419  bind_new register (list (joint_seq RTL globals)) ≝
420  λglobals,op,destrs,srcrs1,srcrs2.
421  νtmp1,tmp2 in
422  let l ≝ |destrs| in
423  let cast_srcrs ≝ λsrcrs,tmp.
424    let srcrs_l ≝ |srcrs| in
425    if leb (S srcrs_l) l then
426      match last ? srcrs with
427      [ Some last ⇒
428        〈srcrs @ make_list … (Reg ? tmp) (l - srcrs_l),
429         sign_mask … tmp last〉
430      | None ⇒
431        〈make_list … (zero_byte : psd_argument) l, [ ]〉
432      ]
433    else
434      〈lhd … srcrs l, [ ]〉 in
435  let prf : ∀srcrs,tmp.|destrs| = |\fst (cast_srcrs srcrs tmp)| ≝ ? in
436  let srcrs1init ≝ cast_srcrs srcrs1 tmp1 in
437  let srcrs2init ≝ cast_srcrs srcrs2 tmp2 in
438  \snd srcrs1init @@ \snd srcrs2init @@
439  translate_op globals op destrs (\fst srcrs1init) (\fst srcrs2init) ??.
440  @hide_prf
441  [ @prf | <prf @prf ]
442  #srcrs #tmp normalize nodelta
443  @leb_elim #H normalize nodelta
444  [ cases (last ??) normalize nodelta
445    [ >length_make_list %
446    | #_ >length_append >length_make_list
447      @minus_to_plus [ @(transitive_le … H) ] //
448    ]
449  | >length_lhd lapply (le_S_S_to_le … (not_le_to_lt … H))
450    lapply (|destrs|) lapply (|srcrs|) -destrs
451    #n #m * -n [2: #n #H] whd in ⊢ (???%); [2: @if_elim #_ % ]
452    >not_le_to_leb_false [%] @lt_to_not_le @le_S_S assumption
453  ]
454qed.
455
456(* using size of lists as size of ints *)
457definition translate_cast :
458  ∀globals: list ident.
459  signedness → list register → list register →
460    bind_new register (list (joint_seq RTL globals)) ≝
461  λglobals,src_sign,destrs,srcrs.
462  match reduce_strong ?? srcrs destrs with
463  [ mk_Sig t prf ⇒
464    let src_common ≝ \fst (\fst t) in
465    let src_rest   ≝ \snd (\fst t) in
466    let dst_common ≝ \fst (\snd t) in
467    let dst_rest   ≝ \snd (\snd t) in
468    (* first, move the common part *)
469    translate_move ? dst_common (map … (Reg ?) src_common) ? @@
470    match src_rest return λ_.bind_new ?? with
471    [ nil ⇒ (* upcast *)
472      match src_sign return λ_.bind_new ?? with
473      [ Unsigned ⇒ translate_fill_with_zero ? dst_rest
474      | Signed ⇒
475        match last … srcrs (* = src_common *) with
476        [ Some src_last ⇒ translate_cast_signed ? dst_rest src_last
477        | None ⇒ (* srcrs is empty *) translate_fill_with_zero ? dst_rest
478        ]
479      ]
480    | _ ⇒ (* downcast, nothing else to do *) [ ]
481    ]
482  ].
483  >length_map >prf % qed.
484 
485definition translate_notint :
486  ∀globals : list ident.
487  ∀destrs : list register.
488  ∀srcrs_arg : list register.
489  |destrs| = |srcrs_arg| → list (joint_seq RTL globals) ≝
490  λglobals, destrs, srcrs, prf.
491  map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf.
492
493definition translate_negint : ∀globals.? → ? → ? → list (joint_seq RTL globals) ≝
494  λglobals: list ident.
495  λdestrs: list register.
496  λsrcrs: list register.
497  λprf: |destrs| = |srcrs|. (* assert in caml code *)
498  translate_notint … destrs srcrs prf @
499  translate_op ? Add destrs (map … (Reg ?) destrs) (one_args (|destrs|)) ??.
500@hide_prf
501>length_map [ @sym_eq @pi2 | % ] qed.
502
503definition translate_notbool:
504  ∀globals : list ident.
505  list register → list register →
506    bind_new register (list (joint_seq RTL globals)) ≝
507  λglobals,destrs,srcrs.
508  match destrs with
509  [ nil ⇒ [ ]
510  | cons destr destrs' ⇒
511    translate_fill_with_zero ? destrs' @@
512    match srcrs return λ_.bind_new ?? with
513    [ nil ⇒ [destr ← zero_byte]
514    | cons srcr srcrs' ⇒
515      (destr ← srcr) :::
516      map register (joint_seq RTL globals) (λr. destr ← destr .Or. r) srcrs' @@
517      (* now destr is non-null iff srcrs was non-null *)
518      CLEAR_CARRY ?? :::
519      (* many uses of 0, better not use immediates *)
520      ν tmp in
521      [tmp ← zero_byte ;
522       destr ← tmp .Sub. tmp ;
523       (* now carry bit is set iff destr was non-null *)
524       destr ← tmp .Addc. tmp]
525     ]
526   ].
527
528definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? →
529  bind_new register (list (joint_seq RTL globals)) ≝
530  λglobals.
531  λty, ty'.
532  λop1: unary_operation ty ty'.
533  λdestrs: list register.
534  λsrcrs: list register.
535  λprf1: |destrs| = size_of_sig_type ty'.
536  λprf2: |srcrs| = size_of_sig_type ty.
537  match op1
538  return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' →
539    bind_new register (list (joint_seq RTL globals)) with
540  [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2.
541    translate_cast globals src_sign destrs srcrs
542  | Onegint sz sg ⇒ λeq1,eq2.
543    translate_negint globals destrs srcrs ?
544  | Onotbool _ _ _ _ ⇒ λeq1,eq2.
545    translate_notbool globals destrs srcrs
546  | Onotint sz sg ⇒ λeq1,eq2.
547    translate_notint globals destrs srcrs ?
548  | Optrofint sz sg ⇒ λeq1,eq2.
549    translate_cast globals Unsigned destrs srcrs
550  | Ointofptr sz sg ⇒ λeq1,eq2.
551    translate_cast globals Unsigned destrs srcrs
552  | Oid t ⇒ λeq1,eq2.
553      translate_move globals destrs (map … (Reg ?) srcrs) ?
554  | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *)
555  ] (refl …) (refl …).
556  @hide_prf
557  destruct >prf1 >prf2 [3: >length_map ] //
558qed.
559
560include alias "arithmetics/nat.ma".
561
562definition translate_mul_i :
563  ∀globals.
564  register → register →
565  (* size of destination and sources *)
566  ∀n : ℕ.
567  (* the temporary destination, with a dummy register at the end *)
568  ∀tmp_destrs_dummy : list register.
569  ∀srcrs1,srcrs2 : list psd_argument.
570  |tmp_destrs_dummy| = S n →
571  n = |srcrs1| →
572  |srcrs1| = |srcrs2| →
573  (* the position of the least significant byte of the result we compute at
574     this stage (goes from 0 to n in the main function) *)
575  ∀k : ℕ.
576  lt k n →
577  (* the position of the byte in the first source we will use in this stage.
578     the position in the other source will be k - i *)
579  (Σi.i<S k) →
580  (* the accumulator *)
581  list (joint_seq RTL globals) →
582    list (joint_seq RTL globals) ≝
583  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
584    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
585  (* the following will expand to
586     a, b ← srcrs1[i] * srcrs2[k-i]
587     tmp_destrs_dummy[k]   ← tmp_destrs_dummy[k] + a
588     tmp_destrs_dummy[k+1] ← tmp_destrs_dummy[k+1] + b + C
589     tmp_destrs_dummy[k+2] ← tmp_destrs_dummy[k+2] + 0 + C
590     ...
591     tmp_destrs_dummy[n]   ← tmp_destrs_dummy[n] + 0 + C
592     ( all calculations on tmp_destrs_dummy[n] will be eliminated with
593     liveness analysis) *)
594  match i_sig with
595    [ mk_Sig i i_prf ⇒
596      (* we pad the result of a byte multiplication with zeros in order
597         for the bit to be carried. Redundant calculations will be eliminated
598         by constant propagation. *)
599      let args : list psd_argument ≝
600        [Reg ? a;Reg ? b] @ make_list ? (zero_byte : psd_argument) (n - 1 - k) in
601      let tmp_destrs_view : list register ≝
602        ltl ? tmp_destrs_dummy k in
603      [❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?)] @
604      translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @
605      acc
606    ].
607@hide_prf
608[ <srcrs1_prf
609  @(transitive_le … i_prf k_prf)
610| @lt_plus_to_minus [ @le_S_S_to_le assumption | <srcrs2_prf <srcrs1_prf
611  whd >(plus_n_O (S k)) @le_plus // ]
612| >length_map %
613| >length_map
614  >length_ltl
615  >tmp_destrs_dummy_prf >length_append
616  >length_make_list
617  normalize in ⊢ (???(?%?));
618  cases n in k_prf; [ #ABS cases (absurd ? ABS ?) /2 by le_to_not_lt/ ]
619  #n' #k_prf >minus_S_S <minus_n_O
620  >plus_minus_commutative [%] @le_S_S_to_le assumption
621] qed.
622
623definition translate_mul : ∀globals.?→?→?→?→?→bind_new register (list (joint_seq RTL globals)) ≝
624λglobals : list ident.
625λdestrs : list register.
626λsrcrs1 : list psd_argument.
627λsrcrs2 : list psd_argument.
628λsrcrs1_prf : |destrs| = |srcrs1|.
629λsrcrs2_prf : |srcrs1| = |srcrs2|.
630(* needed fresh registers *)
631νa in
632νb in
633(* temporary registers for the result are created, so to avoid overwriting
634   sources *)
635νν |destrs| as tmp_destrs with tmp_destrs_prf in
636νdummy in
637(dummy ← byte_of_nat 0) :::
638(* the step calculating all products with least significant byte going in the
639   k-th position of the result *)
640let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq RTL globals) →
641  list (joint_seq RTL globals) ≝
642  λk_sig,acc.match k_sig with
643  [ mk_Sig k k_prf ⇒
644    foldr … (translate_mul_i ? a b (|destrs|)
645      (tmp_destrs @ [dummy]) srcrs1 srcrs2
646      ? srcrs1_prf srcrs2_prf k k_prf) acc (range_strong (S k))
647  ] in
648(* initializing tmp_destrs to zero
649   dummy is intentionally uninitialized *)
650translate_fill_with_zero … tmp_destrs @
651(* the main body, roughly:
652   for k in 0 ... n-1 do
653     for i in 0 ... k do
654       translate_mul_i … k … i *)
655foldr … translate_mul_k [ ] (range_strong (|destrs|)) @
656(* epilogue: saving the result *)
657translate_move … destrs (map … (Reg ?) tmp_destrs) ?.
658@hide_prf
659[ >length_append  <plus_n_Sm <plus_n_O //
660| >length_map >tmp_destrs_prf //
661]
662qed.
663
664definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→
665    bind_new register (list (joint_seq RTL globals)) ≝
666  λglobals: list ident.
667  λdiv_not_mod: bool.
668  λdestrs: list register.
669  λsrcrs1: list psd_argument.
670  λsrcrs2: list psd_argument.
671  λsrcrs1_prf : |destrs| = |srcrs1|.
672  λsrcrs2_prf : |srcrs1| = |srcrs2|.
673  match destrs return λx.x = destrs → bind_new ?? with
674  [ nil ⇒ λ_.[ ]
675  | cons destr destrs' ⇒ λeq_destrs.
676    match destrs' with
677    [ nil ⇒
678      match srcrs1 return λx.x = srcrs1 → bind_new ??  with
679      [ nil ⇒ λeq_srcrs1.⊥
680      | cons srcr1 srcrs1' ⇒ λeq_srcrs1.
681        match srcrs2 return λx.x = srcrs2 → bind_new ??  with
682        [ nil ⇒ λeq_srcrs2.⊥
683        | cons srcr2 srcrs2' ⇒ λeq_srcrs2.
684          νdummy in
685          let 〈destr1, destr2〉 ≝
686            if div_not_mod then 〈destr, dummy〉 else 〈dummy, destr〉 in
687          [❮destr1, destr2❯ ← srcr1 .DivuModu. srcr2]
688        ] (refl …)
689      ] (refl …)
690    | _ ⇒ ? (* not implemented *)
691    ]
692  ] (refl …).
693[3: elim not_implemented]
694@hide_prf
695destruct normalize in srcrs1_prf srcrs2_prf; destruct qed.
696
697(* Paolo: to be moved elsewhere *)
698let rec foldr2 (A : Type[0]) (B : Type[0]) (C : Type[0]) (f : A→B→C→C) (init : C) (l1 : list A) (l2 : list B)
699  (prf : |l1| = |l2|) on l1 : C ≝
700  match l1 return λx.x = l1 → C with 
701  [ nil ⇒ λ_.init
702  | cons a l1' ⇒ λeq_l1.
703    match l2 return λy.y = l2 → C with
704    [ nil ⇒ λeq_l2.⊥
705    | cons b l2' ⇒ λeq_l2.
706      f a b (foldr2 A B C f init l1' l2' ?)
707    ] (refl …)
708  ] (refl …).
709@hide_prf
710destruct normalize in prf;  [destruct|//]
711qed.
712
713definition translate_ne: ∀globals: list ident.?→?→?→?→
714  bind_new register (list (joint_seq RTL globals)) ≝
715  λglobals: list ident.
716  λdestrs: list register.
717  λsrcrs1: list psd_argument.
718  λsrcrs2: list psd_argument.
719  match destrs return λ_.|srcrs1| = |srcrs2| → bind_new ?? with
720  [ nil ⇒ λ_.[ ]
721  | cons destr destrs' ⇒ λEQ.
722    translate_fill_with_zero … destrs' @@
723    match srcrs1 return λx.|x| = |srcrs2| → bind_new ?? with
724    [ nil ⇒ λ_.[destr ← zero_byte]
725    | cons srcr1 srcrs1' ⇒
726      match srcrs2 return λx.S (|srcrs1'|) = |x| → bind_new ?? with
727      [ nil ⇒ λEQ.⊥
728      | cons srcr2 srcrs2' ⇒ λEQ.
729        νtmpr in
730        let f : psd_argument → psd_argument → list (joint_seq RTL globals) → list (joint_seq RTL globals) ≝
731          λs1,s2,acc.
732          tmpr  ← s1 .Xor. s2 ::
733          destr ← destr .Or. tmpr ::
734          acc in
735        let epilogue : list (joint_seq RTL globals) ≝
736          [ CLEAR_CARRY ?? ;
737            tmpr ← zero_byte .Sub. destr ;
738            (* now carry bit is 1 iff destrs != 0 *)
739            destr ← zero_byte .Addc. zero_byte ] in
740         destr ← srcr1 .Xor. srcr2 ::
741         foldr2 ??? f epilogue srcrs1' srcrs2' ?
742       ]
743     ] EQ
744   ].
745@hide_prf normalize in EQ; destruct(EQ) assumption qed.
746
747(* if destrs is 0 or 1, it inverses it. To be used after operations that
748   ensure this. *)
749definition translate_toggle_bool : ∀globals.?→bind_new register (list (joint_seq RTL globals)) ≝
750  λglobals: list ident.
751  λdestrs: list register.
752  match destrs with
753  [ nil ⇒ [ ]
754  | cons destr _ ⇒ [destr ← destr .Xor. byte_of_nat 1]
755  ].
756 
757definition translate_lt_unsigned :
758  ∀globals.
759  ∀destrs: list register.
760  ∀srcrs1: list psd_argument.
761  ∀srcrs2: list psd_argument.
762  |srcrs1| = |srcrs2| →
763  bind_new register (list (joint_seq RTL globals)) ≝
764  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
765  match destrs with
766  [ nil ⇒ [ ]
767  | cons destr destrs' ⇒
768    ν tmpr in
769    (translate_fill_with_zero … destrs' @@
770    (* I perform a subtraction, but the only interest is in the carry bit *)
771    translate_op ? Sub (make_list … tmpr (|srcrs1|)) srcrs1 srcrs2 ? srcrs_prf @@
772    [ destr ← zero_byte .Addc. zero_byte ])
773  ].
774@hide_prf
775>length_make_list % qed.
776
777(* shifts signed integers by adding 128 to the most significant byte
778   it replaces it with a fresh register which must be provided *)
779let rec shift_signed globals
780  (tmp : register)
781  (srcrs : list psd_argument) on srcrs :
782  Σt : (list psd_argument) × (list (joint_seq RTL globals)).|\fst t| = |srcrs| ≝
783  let byte_128 : Byte ≝ true ::: bv_zero ? in
784  match srcrs with
785  [ nil ⇒ 〈[ ],[ ]〉
786  | cons srcr srcrs' ⇒
787    match srcrs' with
788    [ nil ⇒ 〈[ Reg ? tmp ], [ tmp ← srcr .Add. byte_128 ]〉
789    | _ ⇒
790      let re ≝ shift_signed globals tmp srcrs' in
791      〈srcr :: \fst re, \snd re〉
792    ]
793  ].
794@hide_prf
795[1,2: %
796|*: cases re * #a #b >p1 normalize #EQ >EQ %
797] qed.
798
799definition translate_lt_signed :
800  ∀globals.
801  ∀destrs: list register.
802  ∀srcrs1: list psd_argument.
803  ∀srcrs2: list psd_argument.
804  |srcrs1| = |srcrs2| →
805  bind_new register (list (joint_seq RTL globals)) ≝
806  λglobals,destrs,srcrs1,srcrs2,srcrs_prf.
807  νtmp_last_s1 in
808  νtmp_last_s2 in
809  let p1 ≝ shift_signed globals tmp_last_s1 srcrs1 in
810  let new_srcrs1 ≝ \fst p1 in
811  let shift_srcrs1 ≝ \snd p1 in
812  let p2 ≝ shift_signed globals tmp_last_s2 srcrs2 in
813  let new_srcrs2 ≝ \fst p2 in
814  let shift_srcrs2 ≝ \snd p2 in
815  shift_srcrs1 @@ shift_srcrs2 @@
816  translate_lt_unsigned globals destrs new_srcrs1 new_srcrs2 ?.
817@hide_prf
818whd in match new_srcrs1; whd in match new_srcrs2;
819cases p1
820cases p2
821//
822qed.
823
824definition translate_lt : bool→∀globals.?→?→?→?→bind_new register (list (joint_seq RTL globals)) ≝
825  λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs_prf.
826  if is_unsigned then
827    translate_lt_unsigned globals destrs srcrs1 srcrs2 srcrs_prf
828  else
829    translate_lt_signed globals destrs srcrs1 srcrs2 srcrs_prf.
830
831definition translate_cmp ≝
832  λis_unsigned,globals,cmp,destrs,srcrs1,srcrs2,srcrs_prf.
833  match cmp with
834  [ Ceq ⇒
835    translate_ne globals destrs srcrs1 srcrs2 srcrs_prf @@
836    translate_toggle_bool globals destrs
837  | Cne ⇒
838    translate_ne globals destrs srcrs1 srcrs2 srcrs_prf
839  | Clt ⇒
840    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf
841  | Cgt ⇒
842    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ?
843  | Cle ⇒
844    translate_lt is_unsigned globals destrs srcrs2 srcrs1 ? @@
845    translate_toggle_bool globals destrs
846  | Cge ⇒
847    translate_lt is_unsigned globals destrs srcrs1 srcrs2 srcrs_prf @@
848    translate_toggle_bool globals destrs
849  ]. @sym_eq assumption qed.
850
851definition translate_op2 :
852  ∀globals.∀ty1,ty2,ty3.∀op : binary_operation ty1 ty2 ty3.
853  ∀destrs : list register.
854  ∀srcrs1,srcrs2 : list psd_argument.
855  |destrs| = size_of_sig_type ty3 →
856  |srcrs1| = size_of_sig_type ty1 →
857  |srcrs2| = size_of_sig_type ty2 →
858  bind_new register (list (joint_seq RTL globals)) ≝
859  λglobals,ty1,ty2,ty3,op2,destrs,srcrs1,srcrs2.
860  match op2 return λty1,ty2,ty3.λx : binary_operation ty1 ty2 ty3.
861    ? = size_of_sig_type ty3 → ? = size_of_sig_type ty1 → ? = size_of_sig_type ty2 →
862    bind_new ?? with
863  [ Oadd sz sg ⇒ λprf1,prf2,prf3.
864    translate_op globals Add destrs srcrs1 srcrs2 ??
865  | Oaddpi sz ⇒ λprf1,prf2,prf3.
866    translate_op_asym_signed globals Add destrs srcrs1 srcrs2
867  | Oaddip sz ⇒ λprf1,prf2,prf3.
868    translate_op_asym_signed globals Add destrs srcrs2 srcrs1
869  | Osub sz sg ⇒ λprf1,prf2,prf2.
870    translate_op globals Sub destrs srcrs1 srcrs2 ??
871  | Osubpi sz ⇒ λprf1,prf2,prf3.
872    translate_op_asym_signed globals Add destrs srcrs1 srcrs2
873  | Osubpp sz ⇒ λprf1,prf2,prf3.
874    translate_op_asym_unsigned globals Sub destrs srcrs1 srcrs2
875  | Omul sz sg ⇒ λprf1,prf2,prf3.
876    translate_mul globals destrs srcrs1 srcrs2 ??
877  | Odivu sz ⇒ λprf1,prf2,prf3.
878    translate_divumodu8 globals true destrs srcrs1 srcrs2 ??
879  | Omodu sz ⇒ λprf1,prf2,prf3.
880    translate_divumodu8 globals false destrs srcrs1 srcrs2 ??
881  | Oand sz sg ⇒ λprf1,prf2,prf3.
882    translate_op globals And destrs srcrs1 srcrs2 ??
883  | Oor sz sg ⇒ λprf1,prf2,prf3.
884    translate_op globals Or destrs srcrs1 srcrs2 ??
885  | Oxor sz sg ⇒ λprf1,prf2,prf3.
886    translate_op globals Xor destrs srcrs1 srcrs2 ??
887  | Ocmp sz sg1 sg2 c ⇒ λprf1,prf2,prf3.
888    translate_cmp false globals c destrs srcrs1 srcrs2 ?
889  | Ocmpu sz sg c ⇒ λprf1,prf2,prf3.
890    translate_cmp true globals c destrs srcrs1 srcrs2 ?
891  | Ocmpp sg c ⇒ λprf1,prf2,prf3.
892    translate_cmp true globals c destrs srcrs1 srcrs2 ?
893  | _ ⇒ ⊥ (* assert false, implemented in run time or float op *)
894  ]. try @not_implemented @hide_prf //
895  qed.
896
897definition translate_cond: ∀globals: list ident. list register → label →
898  bind_step_block RTL globals ≝
899  λglobals: list ident.
900  λsrcrs: list register.
901  λlbl_true: label.
902  match srcrs return λ_.bind_step_block RTL ? with
903  [ nil ⇒ bret … [ ]
904  | cons srcr srcrs' ⇒
905    ν tmpr in
906    let f : register → label → joint_seq RTL globals ≝
907      λr.λ_. tmpr ← tmpr .Or. r in
908    bret …
909    〈(λ_.MOVE RTL globals 〈tmpr,srcr〉) ::
910     map ?? f srcrs',
911     λ_.COND … tmpr lbl_true, [ ]〉
912  ].
913
914(* Paolo: to be controlled (original seemed overly complex) *)
915definition translate_load : ∀globals.?→?→?→bind_new register ? ≝
916  λglobals: list ident.
917  λaddr : list psd_argument.
918  λaddr_prf: 2 = |addr|.
919  λdestrs: list register.
920  ν tmp_addr_l in
921  ν tmp_addr_h in
922  (translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
923  let f ≝ λdestr : register.λacc : bind_new register (list (joint_seq RTL globals)).
924    [LOAD RTL globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h)] @@
925    translate_op ? Add
926      [tmp_addr_l ; tmp_addr_h]
927      [tmp_addr_l ; tmp_addr_h]
928      [(int_size : Byte) ; zero_byte ] ? ? @@ acc in
929  foldr … f [ ] destrs).
930@hide_prf
931[ <addr_prf ] % qed.
932 
933definition translate_store : ∀globals.?→?→?→bind_new register ? ≝
934  λglobals: list ident.
935  λaddr : list psd_argument.
936  λaddr_prf: 2 = |addr|.
937  λsrcrs: list psd_argument.
938  ν tmp_addr_l in
939  ν tmp_addr_h in
940  (translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
941  let f ≝ λsrcr : psd_argument.λacc : bind_new register (list (joint_seq RTL globals)).
942    [STORE RTL globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr] @@
943    translate_op … Add
944      [tmp_addr_l ; tmp_addr_h]
945      [tmp_addr_l ; tmp_addr_h]
946      [(int_size : Byte) ; zero_byte ] ? ? @@ acc in
947  foldr … f [ ] srcrs).
948@hide_prf [ <addr_prf ] % qed.
949
950lemma lenv_typed_reg_typed_ok1 :
951  ∀locals,env,r,ty.
952  local_env_typed locals env →
953  Exists ? (λx:register×typ.〈r,ty〉=x) locals →
954  ∀prf.
955  |find_local_env r env prf| = size_of_sig_type ty.
956#locals #env #r #ty #env_typed #r_ok
957elim (Exists_All … r_ok env_typed)
958* #r' #ty' * #EQ destruct(EQ) * #rs * #EQ1 #EQ2 #prf
959whd in match find_local_env; normalize nodelta
960@opt_safe_elim #rs' >EQ1 #EQ' destruct assumption
961qed.
962
963lemma lenv_typed_arg_typed_ok1 :
964  ∀locals,env,r,ty.
965  local_env_typed locals env →
966  Exists ? (λx:register×typ.〈r,ty〉=x) locals →
967  ∀prf.
968  |find_local_env_arg r env prf| = size_of_sig_type ty.
969#locals #env #r #ty #env_typed #r_ok #prf
970whd in match find_local_env_arg; normalize nodelta
971>length_map @lenv_typed_reg_typed_ok1 assumption
972qed.
973
974lemma lenv_typed_reg_typed_ok2 :
975  ∀locals,env,r,ty.
976  local_env_typed locals env →
977  Exists ? (λx:register×typ.〈r,ty〉=x) locals →
978  r ∈ env.
979#locals #env #r #ty #env_typed #r_ok
980elim (Exists_All … r_ok env_typed)
981* #r' #ty' * #EQ destruct(EQ) * #rs * #EQ1 #EQ2
982whd in ⊢ (?%);
983>EQ1 %
984qed.
985
986lemma cst_size_ok : ∀ty,cst.size_of_sig_type ty=size_of_cst ty cst.
987#ty * -ty [*] //
988qed.
989
990(* TODO: move it *)
991definition ensure_bind_step_block : ∀p : params.∀g.
992  bind_new register (list (joint_seq p g)) → bind_step_block p g ≝
993  λp,g,b.! l ← b; bret ? (step_block p g) l.
994
995coercion bind_step_block_from_bind_list nocomposites :
996  ∀p : params.∀g.
997  ∀b : bind_new register (list (joint_seq p g)).bind_step_block p g ≝
998  ensure_bind_step_block on _b : bind_new register (list (joint_seq ??)) to
999  bind_step_block ??.
1000
1001definition translate_statement : ∀globals, locals.∀env.
1002  local_env_typed locals env →
1003  ∀stmt : statement.statement_typed locals stmt →
1004  𝚺b :
1005  bind_step_block RTL globals +
1006  bind_fin_block RTL globals.
1007  match b with [ inl _ ⇒ label | _ ⇒ unit] ≝
1008  λglobals,locals,lenv,lenv_typed,stmt.
1009  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
1010  [ St_skip lbl' ⇒ λstmt_typed.
1011    ❬inl … (bret … [ ]), lbl'❭
1012  | St_cost cost_lbl lbl' ⇒ λstmt_typed.
1013    ❬inl … (bret … 〈[ ], λ_.COST_LABEL … cost_lbl, [ ]〉), lbl'❭
1014  | St_const ty destr cst lbl' ⇒ λstmt_typed.
1015    ❬inl … (translate_cst ty globals cst (find_local_env destr lenv ?) ?), lbl'❭
1016  | St_op1 ty ty' op1 destr srcr lbl' ⇒ λstmt_typed.
1017    ❬inl … (translate_op1 globals ty' ty op1
1018      (find_local_env destr lenv ?)
1019      (find_local_env srcr lenv ?) ??), lbl'❭
1020  | St_op2 ty1 ty2 ty3 op2 destr srcr1 srcr2 lbl' ⇒ λstmt_typed.
1021    ❬inl … (translate_op2 globals … op2
1022      (find_local_env destr lenv ?)
1023      (find_local_env_arg srcr1 lenv ?)
1024      (find_local_env_arg srcr2 lenv ?) ???), lbl'❭
1025    (* XXX: should we be ignoring this? *)
1026  | St_load ignore addr destr lbl' ⇒ λstmt_typed.
1027    ❬inl … (translate_load globals
1028      (find_local_env_arg addr lenv ?) ? (find_local_env destr lenv ?)), lbl'❭
1029    (* XXX: should we be ignoring this? *)
1030  | St_store ignore addr srcr lbl' ⇒ λstmt_typed.
1031    ❬inl … (translate_store globals (find_local_env_arg addr lenv ?) ?
1032      (find_local_env_arg srcr lenv ?)), lbl'❭
1033  | St_call_id f args retr lbl' ⇒ λstmt_typed.
1034    ❬inl … (bret …
1035      〈[ ],λ_.CALL RTL ? (inl ?? f) (rtl_args args lenv ?)
1036        (match retr with
1037         [ Some retr ⇒
1038           find_local_env retr lenv ?
1039         | None ⇒ [ ]
1040         ]), [ ]〉), lbl'❭
1041  | St_call_ptr f args retr lbl' ⇒ λstmt_typed.
1042    let fs ≝ find_and_addr_arg f lenv ?? in
1043    ❬inl … (bret …
1044      〈[ ],λ_.CALL RTL ? (inr ?? fs) (rtl_args args lenv ?)
1045        (match retr with
1046         [ Some retr ⇒
1047           find_local_env retr lenv ?
1048         | None ⇒ [ ]
1049         ]), [ ]〉), lbl'❭
1050  | St_cond r lbl_true lbl_false ⇒ λstmt_typed.
1051    ❬inl … (translate_cond globals (find_local_env r lenv ?) lbl_true), lbl_false❭
1052  | St_return ⇒ λ_. ❬inr … (bret … 〈[ ], RETURN ?〉),it❭
1053  ].
1054  @hide_prf
1055  [ cases daemon (* needs more hypotheses *)
1056  | @(lenv_typed_reg_typed_ok2 … lenv_typed stmt_typed)
1057  | >(lenv_typed_reg_typed_ok1 … lenv_typed stmt_typed)
1058    @cst_size_ok
1059  |4,5,6,7: cases stmt_typed #dstr_typed #srcr_typed
1060    [3,4: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption
1061    |2: @(lenv_typed_reg_typed_ok2 … lenv_typed srcr_typed)
1062    |1: @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_typed)
1063    ]
1064  |8,9,10,11,12,13:
1065    cases stmt_typed * #srcrs1_prf #srcrs2_prf #dstr_prf
1066    [5,6: @(lenv_typed_arg_typed_ok1 … lenv_typed) assumption
1067    |4: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption
1068    |3: @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs2_prf)
1069    |2: @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs1_prf)
1070    |1: @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_prf)
1071    ]
1072  |*: cases daemon (* TODO  *)
1073  ]
1074qed.
1075
1076definition translate_internal :
1077  ∀globals.internal_function → (* insert here more properties *)
1078  joint_closed_internal_function RTL globals ≝
1079  λglobals: list ident.
1080  λdef.
1081  let runiverse' ≝ f_reggen def in
1082  let luniverse' ≝ f_labgen def in
1083  let stack_size' ≝ f_stacksize def in
1084  let entry' ≝ pi1 … (f_entry def) in
1085  let init ≝ mk_joint_internal_function RTL globals
1086    luniverse' runiverse' [ ] [ ] stack_size' stack_size'
1087    (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) entry' in
1088  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
1089    (f_locals def) (f_params def) (f_result def) init in
1090  let vars ≝ (f_locals def) @ (f_params def) @
1091    match f_result def with [ Some x ⇒ [x] | _ ⇒ [ ] ] in
1092  let f_trans ≝ λlbl,stmt,def.
1093    let pr ≝ translate_statement … vars lenv ? stmt ? in
1094    match dpi1 … pr return λx.match x with [ inl _ ⇒ label | _ ⇒ unit ] → ? with
1095    [ inl instrs ⇒ λlbl'.b_adds_graph … instrs lbl lbl' def
1096    | inr instrs ⇒ λ_.b_fin_adds_graph … instrs lbl def
1097    ] (dpi2 … pr) in
1098  foldi … f_trans (f_graph def) init'.
1099(* TODO *) cases daemon
1100qed.
1101
1102(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
1103  because of CompCert heritage *)
1104definition rtlabs_to_rtl: (* initialization cost label *) costlabel →
1105  RTLabs_program → rtl_program ≝
1106 λinit_cost, p.
1107  mk_joint_program …
1108    (prog_funct_names \ldots p)
1109    (transform_program … p (λvarnames. transf_fundef … (translate_internal ?)))
1110    init_cost
1111    ?.
1112@hide_prf @transform_prog_funct_names qed.
Note: See TracBrowser for help on using the repository browser.