source: src/RTLabs/RTLabsToRTL.ma @ 2774

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