source: src/RTLabs/RTLabsToRTL.ma @ 2823

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