source: src/RTLabs/RTLabsToRTL.ma @ 2916

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

corrected yet another endianness bug in load and store

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