source: src/RTLabs/RTLabsToRTL.ma @ 2917

Last change on this file since 2917 was 2917, checked in by tranquil, 7 years ago

made it so that a 0 offset does not generate adding ops when accessing global and stack addresses.

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