source: src/RTLabs/RTLabsToRTL.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

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