source: src/RTLabs/RTLabsToRTL.ma @ 2290

Last change on this file since 2290 was 2290, checked in by campbell, 7 years ago

Remove jump tables from RTLabs -> RTL.

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