Changeset 2286 for src/RTLabs/RTLabsToRTL.ma
 Timestamp:
 Aug 2, 2012, 3:18:11 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL.ma
r2176 r2286 5 5 include "common/Graphs.ma". 6 6 include "joint/TranslateUtils.ma". 7 include "utilities/bindLists.ma". 7 8 include alias "ASM/BitVector.ma". 8 9 include alias "arithmetics/nat.ma". 9 10 10 let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝ 11 match n with 12 [ O ⇒ 〈[],runiverse〉 13  S n' ⇒ 14 let 〈r,runiverse〉 ≝ fresh … runiverse in 15 let 〈res,runiverse〉 ≝ register_freshes runiverse n' in 16 〈r::res,runiverse〉 ]. 17 18 definition complete_regs ≝ 19 λglobals. 20 λdef. 21 λsrcrs1. 22 λsrcrs2. 23 if leb (length … srcrs2) (length … srcrs1) then 24 let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs1) (length ? srcrs2)) in 25 〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉 26 else 27 let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs2) (length ? srcrs1)) in 28 〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉. 29 30 lemma complete_regs_length: 31 ∀globals,def,left,right. 32 \fst (\fst (complete_regs globals def left right)) = \snd (\fst (complete_regs globals def left right)). 33 #globals #def #left #right 34 whd in match complete_regs; normalize nodelta 35 @leb_elim normalize nodelta #H 36 [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right))); 37  generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)));] 38 cases (fresh_regs ????) #def' #fresh normalize >append_length 39 generalize in match H; H; 40 generalize in match (length … left); generalize in match (length … right); generalize in match (length … fresh); 41 [ /2/  #x #y #z #H generalize in match (not_le_to_lt … H); H #H #E >E >commutative_plus 42 <plus_minus_m_m /2/ ] 43 qed. 11 definition 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 17 definition 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〉. 44 22 45 23 definition size_of_sig_type ≝ … … 47 25 match sig with 48 26 [ ASTint isize sign ⇒ 49 let isize' ≝ match isize with [ I8 ⇒ 8  I16 ⇒ 16  I32 ⇒ 32 ] in 50 isize' ÷ (nat_of_bitvector ? int_size) 27 match isize with [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4 ] 51 28  ASTfloat _ ⇒ ? (* dpm: not implemented *) 52  ASTptr ⇒ nat_of_bitvector ? ptr_size53 ]. 54 cases not_implemented ;29  ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *) 30 ]. 31 cases not_implemented 55 32 qed. 56 33 … … 61 38 definition local_env ≝ identifier_map RegisterTag (list register). 62 39 63 definition mem_local_env : register → local_env → bool ≝ 64 λr,e. member … e r. 65 66 definition add_local_env : register → list register → local_env → local_env ≝ 67 λr,v,e. add … e r v. 68 69 definition find_local_env : register → local_env → list register ≝ 70 λr: register.λenv. lookup_def … env r []. 71 72 definition initialize_local_env_internal ≝ 73 λlenv_runiverse. 74 λr_sig. 75 let 〈lenv,runiverse〉 ≝ lenv_runiverse in 40 definition 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 46 definition find_local_env ≝ λr.λlenv : local_env. 47 λprf : r ∈ lenv.opt_safe … (lookup … lenv r) ?. 48 lapply (in_map_domain … lenv r) 49 >prf * #x #lookup_eq >lookup_eq % #ABS destruct(ABS) 50 qed. 51 52 lemma 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 55 change with (P (opt_safe ???)) 56 @opt_safe_elim assumption 57 qed. 58 59 definition find_local_env_arg : register → local_env → ? → list psd_argument ≝ 60 λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf). 61 62 definition 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 76 68 let 〈r, sig〉 ≝ r_sig in 77 69 let size ≝ size_of_sig_type sig in 78 let 〈rs,runiverse〉 ≝ register_freshes runiverse size in 79 〈add_local_env r rs lenv,runiverse〉. 80 81 definition initialize_local_env ≝ 82 λruniverse. 83 λregisters. 84 λresult. 85 let registers ≝ registers @ 86 match result with 87 [ None ⇒ [ ] 88  Some rt ⇒ [ rt ] 70 let 〈def,rs〉 ≝ repeat_fresh … (rtl_fresh_reg_no_local globals) size def in 71 〈def,add … lenv r rs〉. 72 73 include alias "common/Identifiers.ma". 74 let 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 82 definition 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 89 lemma 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 ] 105 qed. 106 107 example proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr. 108 // qed. 109 example proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr. 110 // qed. 111 112 definition 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; 89 144 ] 90 in91 foldl … initialize_local_env_internal 〈empty_map …,runiverse〉 registers.92 93 definition map_list_local_env_internal ≝ 94 λlenv,res,r. res @ (find_local_env r lenv).95 96 definition map_list_local_env ≝ 97 λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs.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 ] 152 qed. 98 153 99 154 definition make_addr ≝ 100 155 λA. 101 156 λlst: list A. 102 λprf: 2 = length A lst. 103 match lst return λx. 2 = x → A × A with 104 [ nil ⇒ λlst_nil_prf. ? 105  cons hd tl ⇒ λprf. 106 match tl return λx. 1 = x → A × A with 107 [ nil ⇒ λtl_nil_prf. ? 108  cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉 109 ] ? 110 ] prf. 111 [1: normalize in lst_nil_prf; 112 destruct(lst_nil_prf) 113 2: normalize in prf; 114 @injective_S 115 assumption 116 3: normalize in tl_nil_prf; 117 destruct(tl_nil_prf) 118 ] 119 qed. 157 λprf: 2 = length A lst.〈nth_safe … 0 lst ?, nth_safe … 1 lst ?〉. <prf // 158 qed. 120 159 121 160 definition find_and_addr ≝ 122 λr,lenv. make_addr ? (find_local_env r lenv). 123 124 definition rtl_args ≝ 125 λregs_list,lenv. flatten … (map … (λr. find_local_env r lenv) regs_list). 126 127 definition translate_cst_int_internal ≝ 128 λglobals,dest_lbl,r,i. sequential rtl_params_ globals (INT … r i) dest_lbl. 161 λr,lenv,prf. make_addr ? (find_local_env r lenv prf). 162 163 include alias "common/Identifiers.ma". 164 let 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 173 include alias "basics/lists/list.ma". 174 let 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. 129 183 130 184 definition split_into_bytes: 131 185 ∀size. ∀int: bvint size. Σbytes: list Byte. bytes = size_intsize size ≝ 132 λsize. 133 match size return λsize.∀int: bvint size. Σbytes. bytes = size_intsize size with 134 [ I8 ⇒ λint. ?  I16 ⇒ λint. ?  I32 ⇒ λint. ? ]. 135 [ %[@[int]] // 136  %[@(let 〈h,l〉 ≝ vsplit ? 8 … int in [l;h])] cases (vsplit ????) // 137  %[@(let 〈h1,l〉 ≝ vsplit ? 8 … int in 138 let 〈h2,l〉 ≝ vsplit ? 8 … l in 139 let 〈h3,l〉 ≝ vsplit ? 8 … l in 140 [l;h3;h2;h1])] 141 cases (vsplit ????) #h1 #l normalize 142 cases (vsplit ????) #h2 #l normalize 143 cases (vsplit ????) // ] 144 qed. 145 146 lemma eqb_implies_eq: 147 ∀m, n: nat. 148 eqb m n = true → m = n. 149 #M 150 elim M 151 [1: #N normalize 152 cases N 153 [1: normalize // 154 2: #M' normalize #HYP destruct(HYP) 155 ] 156 2: #M' #IND_HYP #N 157 normalize 158 cases N 159 [1: normalize #HYP destruct(HYP) 160 2: #M'' normalize #HYP 161 @eq_f @(IND_HYP M'') 162 assumption 163 ] 164 ] 165 qed. 166 167 definition translate_op: ∀globals. ? → list register → list register → list register → 168 label → label → rtl_internal_function globals → rtl_internal_function globals ≝ 186 λsize.vrsplit ? (size_intsize size) 8. 187 188 let rec list_inject_All_aux A P (l : list A) on l : All A P l → list (Σx.P x) ≝ 189 match 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] 193 qed. 194 195 include alias "basics/lists/list.ma". 196 definition 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 ≝ 169 204 λglobals: list ident. 170 205 λop. 171 λdestrs: list register. 172 λsrcrs1: list register. 173 λsrcrs2: list register. 174 λstart_lbl: label. 175 λdest_lbl: label. 176 λdef: rtl_internal_function globals. 177 match reduce_strong register register srcrs1 srcrs2 with 178 [ mk_Sig reduced first_reduced_proof ⇒ 179 let srcrsl_common ≝ \fst (\fst reduced) in 180 let srcrsr_common ≝ \fst (\snd reduced) in 181 let srcrsl_rest ≝ \snd (\fst reduced) in 182 let srcrsr_rest ≝ \snd (\snd reduced) in 183 let srcrs_rest ≝ srcrsl_rest @ srcrsr_rest in 184 match reduce_strong register register destrs srcrsl_common with 185 [ mk_Sig reduced second_reduced_proof ⇒ 186 let destrs_common ≝ \fst (\fst reduced) in 187 let destrs_rest ≝ \snd (\fst reduced) in 188 match reduce_strong register register destrs_rest srcrs_rest with 189 [ mk_Sig reduced third_reduced_proof ⇒ 190 let destrs_cted ≝ \fst (\fst reduced) in 191 let destrs_rest ≝ \snd (\fst reduced) in 192 let srcrs_cted ≝ \fst (\snd reduced) in 193 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 194 let insts_init ≝ [ 195 sequential … (CLEAR_CARRY …); 196 sequential … (INT rtl_params_ globals tmpr (zero …)) 197 ] in 198 let f_add ≝ λdestr. λsrcr1. λsrcr2. sequential … (OP2 rtl_params_ globals op destr srcr1 srcr2) in 199 let insts_add ≝ map3 ? ? ? ? f_add destrs_common srcrsl_common srcrsr_common ? ? in 200 let f_add_cted ≝ λdestr. λsrcr. sequential … (OP2 rtl_params_ globals op destr srcr tmpr) in 201 let insts_add_cted ≝ map2 … f_add_cted destrs_cted srcrs_cted ? in 202 let f_rest ≝ λdestr. sequential … (OP2 rtl_params_ globals op destr tmpr tmpr) in 203 let insts_rest ≝ map … f_rest destrs_rest in 204 adds_graph rtl_params1 globals (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def 205 ] 206 ] 207 ]. 208 [1: @third_reduced_proof 209 3: @first_reduced_proof 210 *: cases daemon (* XXX: some of these look like they may be false *) 211 ] 212 qed. 213 214 (* Type safety in RTLabs has broken this for the moment... 215 let rec translate_cst 216 (globals: list ident) (cst: constant) (destrs: list register) 217 (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals) 218 on cst: rtl_internal_function globals ≝ 219 match cst with 220 [ Ointconst size const ⇒ 221 match destrs with 222 [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def 223  _ ⇒ 224 let size' ≝ size_intsize size in 225 match eqb size' (destrs) return λx. (eqb size' (destrs)) = x → rtl_internal_function globals with 226 [ true ⇒ λgood_case. 227 match split_into_bytes size const with 228 [ mk_Sig bytes bytes_length_proof ⇒ 229 let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in 230 adds_graph rtl_params1 globals mapped start_lbl dest_lbl def 231 ] 232  false ⇒ λbad_case. ? 233 ] (refl … (eqb size' (destrs))) 234 ] 235  Ofloatconst float ⇒ ⊥ 236  Oaddrsymbol id offset ⇒ 237 let 〈r1, r2〉 ≝ make_addr … destrs ? in 238 let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def in 239 let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in 240 def 241  Oaddrstack offset ⇒ 242 let 〈r1, r2〉 ≝ make_addr … destrs ? in 243 let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (extension rtl_params_ globals (rtl_st_ext_stack_address r1 r2)) dest_lbl) def in 244 let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in 245 def 246 ]. 247 [1: >bytes_length_proof 248 cut(size' = destrs) 249 [1: @eqb_implies_eq 250 assumption 251 2: #EQ_HYP 252 <EQ_HYP % 253 ] 254 2: cases daemon (* XXX: bad case where destrs is of the wrong length *) 255 3: cases not_implemented (* XXX: float, error_float in o'caml *) 256 *: cases daemon (* XXX: various proofs to be filled in *) 257 ]. 258 qed. 259 260 definition translate_move_internal ≝ 261 λglobals. 262 λdestr: register. 263 λsrcr: register. 264 sequential rtl_params_ globals (MOVE … 〈destr,srcr〉). 265 266 definition translate_move ≝ 267 λglobals. 268 λdestrs: list register. 269 λsrcrs: list register. 270 λstart_lbl: label. 271 match reduce_strong register register destrs srcrs with 272 [ mk_Sig crl_crr len_proof ⇒ 273 let commonl ≝ \fst (\fst crl_crr) in 274 let commonr ≝ \fst (\snd crl_crr) in 275 let restl ≝ \snd (\fst crl_crr) in 276 let restr ≝ \snd (\snd crl_crr) in 277 let f_common ≝ translate_move_internal globals in 278 let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in 279 let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *) 280 add_translates … [ translate1 ; translate2 ] start_lbl 281 ]. 282 @len_proof 283 qed. 284 285 let rec make 286 (A: Type[0]) (elt: A) (n: nat) on n ≝ 287 match n with 288 [ O ⇒ [ ] 289  S n' ⇒ elt :: make A elt n' 290 ]. 291 292 lemma make_length: 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 217 definition 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 224 lemma length_make_list: 293 225 ∀A: Type[0]. 294 226 ∀elt: A. 295 227 ∀n: nat. 296 n = length ? (make A elt n).228 length ? (make_list A elt n) = n. 297 229 #A #ELT #N 298 elim N 299 [ normalize % 300  #N #IH 301 normalize <IH % 230 elim N normalize // qed. 231 232 lemma 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 ] 238 qed. 239 240 lemma length_cast_list : ∀A,dflt,n,l.cast_list A dflt n l = n. 241 #A #dflt #n #l 242 normalize @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 ] 249 qed. 250 251 definition 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 ] % 261 qed. 262 263 let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.l = size ≝ 264 match 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 270 definition 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 277 definition 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 283 definition 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 % 302 311 ] 303 312 qed. 304 305 definition translate_cast_unsigned ≝ 306 λglobals. 307 λdestrs. 308 λstart_lbl. 309 λdest_lbl. 310 λdef: joint_internal_function … (rtl_params globals). 311 let 〈def, tmp_zero〉 ≝ fresh_reg … def in 312 let zeros ≝ make … tmp_zero (length … destrs) in 313 add_translates … [ 314 adds_graph rtl_params1 … [ 315 sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) 316 ]; 317 translate_move globals destrs zeros 318 ] start_lbl dest_lbl def. 319 320 definition translate_cast_signed: 321 ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ 322 λglobals: list ident. 323 λdestrs. 324 λsrcr. 325 λstart_lbl. 326 λdest_lbl. 327 λdef. 328 let 〈def, tmp_128〉 ≝ fresh_reg … def in 329 let 〈def, tmp_255〉 ≝ fresh_reg … def in 330 let 〈def, tmpr〉 ≝ fresh_reg … def in 331 let 〈def, dummy〉 ≝ fresh_reg … def in 332 let insts ≝ [ 333 sequential … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128)); 334 sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr); 335 sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128); 336 sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255)); 337 sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255) 313 314 definition 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 322 definition 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 350 definition 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 360 definition 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 368 let rec last A (l : list A) on l : option A ≝ 369 match l with 370 [ nil ⇒ None ? 371  cons hd tl ⇒ 372 match tl with 373 [ nil ⇒ Some ? hd 374  _ ⇒ last A tl 338 375 ] 339 in 340 let srcrs ≝ make … tmpr (length … destrs) in 341 add_translates rtl_params1 globals [ 342 adds_graph rtl_params1 globals insts; 343 translate_move globals destrs srcrs 344 ] start_lbl dest_lbl def. 345 346 definition translate_cast ≝ 347 λglobals: list ident. 348 λsrc_size: nat. 349 λsrc_sign: signedness. 350 λdest_size: nat. 351 λdestrs: list register. 352 λsrcrs: list register. 353 match srcrs return λx. srcrs = x → ? with 354 [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ] 355  S n' ⇒ λsucc_prf. 356 if ltb dest_size src_size then 357 translate_move globals destrs srcrs 376 ]. 377 378 lemma 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) 386 qed. 387 388 definition 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 ] 358 404 else 359 match reduce_strong register register destrs srcrs with 360 [ mk_Sig crl len_proof ⇒ 361 let commonl ≝ \fst (\fst crl) in 362 let commonr ≝ \fst (\snd crl) in 363 let restl ≝ \snd (\fst crl) in 364 let restr ≝ \snd (\snd crl) in 365 let insts_common ≝ translate_move globals commonl commonr in 366 let sign_reg ≝ last_safe ? srcrs ? in 367 let insts_sign ≝ 368 match src_sign with 369 [ Unsigned ⇒ translate_cast_unsigned globals restl 370  Signed ⇒ translate_cast_signed globals restl sign_reg 371 ] 372 in 373 add_translates rtl_params1 globals [ insts_common; insts_sign ] 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) 374 419 ] 375 ] (refl ? (srcrs)). 376 >succ_prf // 377 qed. 378 379 definition translate_negint ≝ 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 ] 429 qed. 430 431 (* using size of lists as size of ints *) 432 definition 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 460 definition 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 468 definition translate_negint : ∀globals.? → ? → ? → bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 380 469 λglobals: list ident. 381 470 λdestrs: list register. 382 471 λsrcrs: list register. 383 λstart_lbl: label.384 λdest_lbl: label.385 λdef: rtl_internal_function globals.386 472 λprf: destrs = srcrs. (* assert in caml code *) 387 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 388 let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in 389 let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in 390 let insts_init ≝ [ 391 sequential … (SET_CARRY …); 392 sequential … (INT rtl_params_ globals tmpr (zero ?)) 393 ] in 394 let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in 395 let insts_add ≝ map … f_add destrs in 396 adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def. 397 398 definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ 399 λglobals: list ident. 400 λdestrs: list register. 401 λsrcrs: list register. 402 λstart_lbl: label. 403 λdest_lbl: label. 404 λdef: rtl_internal_function globals. 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 480 definition 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. 405 485 match destrs with 406 [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def 407  cons destr destrs ⇒ 408 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 409 let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in 410 let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in 411 let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in 412 let f ≝ λtmp_srcr. [ 413 sequential … (CLEAR_CARRY rtl_params_ globals); 414 sequential … (INT rtl_params_ globals tmpr (zero ?)); 415 sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr); 416 sequential … (INT rtl_params_ globals tmpr (zero ?)); 417 sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr); 418 sequential … (OP2 rtl_params_ globals Xor destr destr tmpr) 419 ] in 420 let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in 421 let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in 422 add_translates rtl_params1 globals [ 423 save_srcrs; adds_graph rtl_params1 globals insts; epilogue 424 ] start_lbl dest_lbl def 425 ]. 426 427 (* TODO: examine this properly. This is a change from the O'caml code due 428 to us dropping the explicit use of a cast destination size field. We 429 instead infer the size of the cast's destination from the context. Is 430 this correct? 431 *) 432 definition translate_op1 ≝ 433 λglobals: list ident. 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 nonnull iff srcrs was nonnull *) 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 nonnull *) 501 destr ← tmp .Addc. tmp] 502 ] 503 ]. 504 505 definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? → 506 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 507 λglobals. 434 508 λty, ty'. 435 509 λop1: unary_operation ty ty'. 436 510 λdestrs: list register. 437 511 λsrcrs: list register. 438 λprf: destrs = srcrs. 439 λstart_lbl: label. 440 λdest_lbl: label. 441 λdef: rtl_internal_function globals. 442 match op1 with 443 [ Ocastint src_size src_sign _ _ ⇒ 444 let dest_size ≝ destrs * 8 in 445 let src_size ≝ bitsize_of_intsize src_size in 446 translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def 447  Onegint _ _ ⇒ 448 translate_negint globals destrs srcrs start_lbl dest_lbl def prf 449  Onotbool _ _ _ _ ⇒ 450 translate_notbool globals destrs srcrs start_lbl dest_lbl def 451  Onotint _ _ ⇒ 452 let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in 453 let l ≝ map2 … f destrs srcrs prf in 454 adds_graph rtl_params1 globals l start_lbl dest_lbl def 455  Optrofint _ _ r ⇒ 456 translate_move globals destrs srcrs start_lbl dest_lbl def 457  Ointofptr _ _ r ⇒ 458 translate_move globals destrs srcrs start_lbl dest_lbl def 459  Oid _ ⇒ 460 translate_move globals destrs srcrs start_lbl dest_lbl def 461  _ ⇒ ? (* float operations implemented in runtime *) 462 ]. 463 cases not_implemented 464 qed. 465 466 let rec translate_mul1 467 (globals: list ident) (dummy: register) (tmpr: register) 468 (destrs: list register) (srcrs1: list register) (srcr2: register) 469 (start_lbl: label) 470 on srcrs1 ≝ 471 match destrs with 472 [ nil ⇒ adds_graph rtl_params1 globals [ GOTO … ] start_lbl 473  cons destr tl ⇒ 474 match tl with 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 ] 536 qed. 537 538 include alias "arithmetics/nat.ma". 539 540 let rec range_strong_internal (start : ℕ) (count : ℕ) 541 (* Paolo: no notation to avoid ambiguity *) 542 on count : list (Σn : ℕ.lt n (plus start count)) ≝ 543 match 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 …). 551 destruct(EQ) // qed. 552 553 definition range_strong : ∀end : ℕ. list (Σn.n<end) ≝ 554 λend.range_strong_internal 0 end. 555 556 definition 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[ki] 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 621 definition 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 kth position of the result *) 637 let 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 *) 647 translate_fill_with_zero … tmp_destrs @ 648 (* the main body, roughly: 649 for k in 0 ... n1 do 650 for i in 0 ... k do 651 translate_mul_i … k … i *) 652 foldr … translate_mul_k [ ] (range_strong (destrs)) @ 653 (* epilogue: saving the result *) 654 translate_move … destrs (map … (Reg ?) tmp_destrs) ?. 655 [ >length_map >tmp_destrs_prf // 656  >length_append <plus_n_Sm <plus_n_O // 657 ] 658 qed. 659 660 definition 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 475 673 [ nil ⇒ 476 match srcrs1 with 477 [ nil ⇒ 478 adds_graph rtl_params1 globals [ 479 sequential … (INT rtl_params_ globals tmpr (zero …)); 480 sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) 481 ] start_lbl 482  cons srcr1 tl' ⇒ 483 adds_graph rtl_params1 globals [ 484 sequential … (OPACCS rtl_params_ globals Mul tmpr dummy srcr2 srcr1); 485 sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) 486 ] start_lbl 487 ] 488  cons destr2 destrs ⇒ 489 match srcrs1 with 490 [ nil ⇒ 491 add_translates rtl_params1 globals [ 492 adds_graph rtl_params1 globals [ 493 sequential … (INT rtl_params_ globals tmpr (zero …)); 494 sequential … (OP2 rtl_params_ globals Addc destr destr tmpr); 495 sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr) 496 ]; 497 translate_cst globals (Ointconst I8 (zero …)) destrs 498 ] start_lbl 499  cons srcr1 srcrs1 ⇒ 500 match destrs with 501 [ nil ⇒ 502 add_translates rtl_params1 globals [ 503 adds_graph rtl_params1 globals [ 504 sequential … (INT rtl_params_ globals tmpr (zero …)); 505 sequential … (OP2 rtl_params_ globals Addc destr destr tmpr); 506 sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr) 507 ]; 508 translate_cst globals (Ointconst I8 (zero ?)) destrs 509 ] start_lbl 510  cons destr2 destrs ⇒ 511 add_translates rtl_params1 globals [ 512 adds_graph rtl_params1 globals [ 513 sequential … (OPACCS rtl_params_ globals Mul tmpr destr2 srcr2 srcr1); 514 sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) 515 ]; 516 translate_mul1 globals dummy tmpr (destr2 :: destrs) srcrs1 srcr2 517 ] start_lbl 518 ] 519 ] 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 *) 520 687 ] 521 ]. 522 523 definition translate_muli ≝ 524 λglobals: list ident. 525 λdummy: register. 526 λtmpr: register. 527 λdestrs: list register. 528 λtmp_destrs: list register. 529 λsrcrs1: list register. 530 λdummy_lbl: label. 531 λi: nat. 532 λi_prf: i ≤ tmp_destrs. 533 λtranslates: list ?. 534 λsrcr2i: register. 535 let 〈tmp_destrs1, tmp_destrs2〉 ≝ vsplit … tmp_destrs i i_prf in 536 let tmp_destrs2' ≝ 537 match tmp_destrs2 with 538 [ nil ⇒ [ ] 539  cons tmp_destr2 tmp_destrs2 ⇒ [ 540 adds_graph rtl_params1 globals [ 541 sequential rtl_params_ globals (CLEAR_CARRY …); 542 sequential … (INT rtl_params_ globals tmp_destr2 (zero …)) 543 ]; 544 translate_mul1 globals dummy tmpr tmp_destrs2 srcrs1 srcr2i; 545 translate_cst globals (Ointconst I8 (zero …)) tmp_destrs1; 546 adds_graph rtl_params1 globals [ 547 sequential rtl_params_ globals (CLEAR_CARRY …) 548 ]; 549 translate_op globals Addc destrs destrs tmp_destrs 550 ] 551 ] 552 in 553 translates @ tmp_destrs2'. 554 555 let rec remove_n_first_internal 556 (b: Type[0]) (n: nat) (the_list: list b) (i: nat) 557 on the_list ≝ 558 match the_list with 559 [ nil ⇒ [ ] 560  cons hd tl ⇒ 561 match eqb i n with 562 [ true ⇒ the_list 563  false ⇒ remove_n_first_internal b n tl (S i) 564 ] 565 ]. 566 567 definition remove_n_first ≝ 568 λb: Type[0]. 569 λn: nat. 570 λthe_list: list b. 571 remove_n_first_internal b n the_list 0. 572 573 axiom plus_m_n_eq_o_to_lt_m_o: 574 ∀m, n, o: nat. 575 m + n = o → m ≤ o. 576 577 include alias "arithmetics/nat.ma". 578 579 axiom minus_m_n_Sp_to_minus_m_Sn_p: 580 ∀m, n, p: nat. 581 minus m n = S p → minus m (S n) = p. 582 583 let rec foldi_strong_internal 584 (a: Type[0]) (b: Type[0]) (reference: nat) (the_list: list b) 585 (f: ∀j: nat. ∀proof: lt j (the_list). a → b → a) (seed: a) 586 (counter: nat) (counter_proof: minus reference counter = the_list) 587 on the_list: a ≝ 588 match the_list return λx. the_list = x → (minus reference counter = x) → a with 589 [ nil ⇒ λidentity. λbase_case. seed 590  cons hd tl ⇒ λidentity. λstep_case. 591 let f' ≝ λj: nat. λproof: j < tl. f j ? in 592 foldi_strong_internal a b reference tl f' (f counter ? seed hd) (S counter) ? 593 ] (refl … the_list) counter_proof. 594 [1: cases daemon (* XXX: to do *) 595 2: generalize in match counter_proof; 596 >identity 597 #HYP 598 normalize in HYP:(???%); 599 generalize in match (minus_m_n_Sp_to_minus_m_Sn_p reference counter (tl) HYP); 600 #ASSM assumption 601 3: >identity 602 normalize 603 normalize in proof; 604 generalize in match(le_S … proof); 605 #HYP assumption 606 ] 607 qed. 608 609 definition foldi_strong ≝ 610 λa: Type[0]. 611 λb: Type[0]. 612 λthe_list: list b. 613 λf: (∀i: nat. ∀proof: i < the_list. a → b → a). 614 λseed: a. 615 foldi_strong_internal a b (the_list) the_list f seed 0 ?. 616 // 617 qed. 618 619 definition translate_mul ≝ 688 ] (refl …). 689 [3: elim not_implemented] 690 destruct normalize in srcrs1_prf; normalize in srcrs2_prf; destruct qed. 691 692 (* Paolo: to be moved elsewhere *) 693 let 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 …). 704 destruct normalize in prf; [destruct//] 705 qed. 706 707 definition translate_ne: ∀globals: list ident.?→?→?→?→ 708 bind_new (localsT RTL) (list (joint_seq RTL globals)) ≝ 620 709 λglobals: list ident. 621 710 λdestrs: list register. 622 λsrcrs1: list register. 623 λsrcrs2: list register. 624 λregs_proof: destrs = srcrs2. 625 λstart_lbl: label. 626 λdest_lbl: label. 627 λdef: rtl_internal_function globals. 628 let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in 629 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 630 match fresh_regs_strong rtl_params0 globals def (destrs) with 631 [ mk_Sig def_tmp_destrs tmp_destrs_prf ⇒ 632 let def ≝ \fst def_tmp_destrs in 633 let tmp_destrs ≝ \snd def_tmp_destrs in 634 let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (srcrs1) in 635 let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (srcrs2) in 636 let insts_init ≝ [ 637 translate_move globals fresh_srcrs1 srcrs1; 638 translate_move globals fresh_srcrs2 srcrs2; 639 translate_cst globals (Ointconst I8 (zero …)) destrs 640 ] 641 in 642 let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in 643 let f' ≝ λi. λi_proof: i < srcrs2. f i ? in 644 let insts_mul ≝ foldi_strong … srcrs2 f' [ ] in 645 add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def 646 ]. 647 >tmp_destrs_prf 648 >regs_proof 649 /2/ 650 qed. 651 652 definition translate_divumodu8 ≝ 653 λglobals: list ident. 654 λorder: bool. 655 λdestrs: list register. 656 λsrcr1: register. 657 λsrcr2: register. 658 λstart_lbl: label. 659 λdest_lbl: label. 660 λdef: rtl_internal_function globals. 661 match destrs with 662 [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def 663  cons destr destrs ⇒ 664 let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in 665 let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉  _ ⇒ 〈dummy, destr〉 ] in 666 let inst_div ≝ adds_graph rtl_params1 globals [ 667 sequential rtl_params_ globals (OPACCS … DivuModu destr1 destr2 srcr1 srcr2) 668 ] 669 in 670 let insts_rest ≝ translate_cst globals (Ointconst I8 (zero ?)) destrs in 671 add_translates rtl_params1 globals [ inst_div; insts_rest ] start_lbl dest_lbl def 672 ]. 673 674 definition translate_ne: ∀globals: list ident. ? → ? → ? → ? → ? → ? → rtl_internal_function globals ≝ 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. *) 742 definition translate_toggle_bool : ∀globals.?→list (joint_seq RTL globals) ≝ 675 743 λglobals: list ident. 676 744 λdestrs: list register. 677 λsrcrs1: list register.678 λsrcrs2: list register.679 λstart_lbl: label.680 λdest_lbl: label.681 λdef: rtl_internal_function globals.682 745 match destrs with 683 [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def 684  cons destr destrs ⇒ 685 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 686 let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params0 globals def in 687 let 〈def, tmp_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (srcrs1) in 688 let save_srcrs1 ≝ translate_move globals tmp_srcrs1 srcrs1 in 689 let 〈def, tmp_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (srcrs2) in 690 let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in 691 match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with 692 [ mk_Sig crl their_proof ⇒ 693 let commonl ≝ \fst (\fst crl) in 694 let commonr ≝ \fst (\snd crl) in 695 let restl ≝ \snd (\snd crl) in 696 let restr ≝ \snd (\snd crl) in 697 let rest ≝ restl @ restr in 698 let inits ≝ [ 699 sequential … (INT rtl_params_ globals destr (zero …)); 700 sequential … (INT rtl_params_ globals tmp_zero (zero …)) 701 ] 702 in 703 let f_common ≝ λtmp_srcr1. λtmp_srcr2. [ 704 sequential … (CLEAR_CARRY …); 705 sequential … (OP2 rtl_params_ globals Sub tmpr tmp_srcr1 tmp_srcr2); 706 sequential … (OP2 rtl_params_ globals Or destr destr tmpr) 707 ] 708 in 709 let insts_common ≝ flatten … (map2 … f_common commonl commonr ?) in 710 let f_rest ≝ λtmp_srcr. [ 711 sequential … (CLEAR_CARRY …); 712 sequential … (OP2 rtl_params_ globals Sub tmpr tmp_zero tmp_srcr); 713 sequential … (OP2 rtl_params_ globals Or destr destr tmpr) 714 ] 715 in 716 let insts_rest ≝ flatten … (map … f_rest rest) in 717 let insts ≝ inits @ insts_common @ insts_rest in 718 let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in 719 add_translates rtl_params1 globals [ 720 save_srcrs1; save_srcrs2; adds_graph rtl_params1 globals insts; epilogue 721 ] start_lbl dest_lbl def 746 [ nil ⇒ [ ] 747  cons destr _ ⇒ [destr ← .Cmpl. destr] 748 ]. 749 750 definition 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 *) 771 let 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〉 722 784 ] 723 785 ]. 724 @their_proof 725 qed. 726 727 definition translate_eq_reg ≝ 728 λglobals: list ident. 729 λtmp_zero: register. 730 λtmp_one: register. 731 λtmpr1: register. 732 λtmpr2: register. 733 λdestr: register. 734 λdummy_lbl: label. 735 λsrcr12: register × register. 736 let 〈srcr1, srcr2〉 ≝ srcr12 in 737 [ sequential … (CLEAR_CARRY …); 738 sequential rtl_params_ globals (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2); 739 sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero); 740 sequential … (OP2 rtl_params_ globals Sub tmpr2 srcr2 srcr1); 741 sequential … (OP2 rtl_params_ globals Addc tmpr2 tmp_zero tmp_zero); 742 sequential … (OP2 rtl_params_ globals Or tmpr1 tmpr1 tmpr2); 743 sequential … (OP2 rtl_params_ globals Xor tmpr1 tmpr1 tmp_one); 744 sequential … (OP2 rtl_params_ globals And destr destr tmpr1) ]. 745 746 definition translate_eq_list ≝ 747 λglobals: list ident. 748 λtmp_zero: register. 749 λtmp_one: register. 750 λtmpr1: register. 751 λtmpr2: register. 752 λdestr: register. 753 λleq: list (register × register). 754 λdummy_lbl: label. 755 let f ≝ translate_eq_reg globals tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in 756 (sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1))) :: 757 flatten … (map … f leq). 758 759 definition translate_atom ≝ 760 λglobals: list ident. 761 λtmp_zero: register. 762 λtmp_one: register. 763 λtmpr1: register. 764 λtmpr2: register. 765 λtmpr3: register. 766 λdestr: register. 767 λdummy_lbl: label. 768 λleq: list (register × register). 769 λsrcr1: register. 770 λsrcr2: register. 771 translate_eq_list globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @ 772 [ sequential … (CLEAR_CARRY …); 773 sequential … (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2); 774 sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero); 775 sequential … (OP2 rtl_params_ globals And tmpr3 tmpr3 tmpr1); 776 sequential … (OP2 rtl_params_ globals Or destr destr tmpr3) ]. 777 778 definition translate_lt_main ≝ 779 λglobals: list ident. 780 λtmp_zero: register. 781 λtmp_one: register. 782 λtmpr1: register. 783 λtmpr2: register. 784 λtmpr3: register. 785 λdestr: register. 786 λdummy_lbl: label. 787 λsrcrs1: list register. 788 λsrcrs2: list register. 789 λproof: srcrs1 = srcrs2. 790 let f ≝ λinsts_leq. λsrcr1. λsrcr2. 791 let 〈insts, leq〉 ≝ insts_leq in 792 let added_insts ≝ translate_atom globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in 793 〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉 794 in 795 \fst (fold_left2 … f 〈[ ], [ ]〉 srcrs1 srcrs2 proof). 796 797 definition fresh_regs_strong: 798 ∀globals. rtl_internal_function globals → ∀n: nat. Σfresh: (rtl_internal_function globals) × (list register). \snd fresh = n ≝ 799 λglobals: list ident. 800 λdef. 801 λn. 802 fresh_regs rtl_params0 globals def n. 803 @fresh_regs_length 804 qed. 805 806 definition complete_regs_strong: 807 ∀globals: list ident. rtl_internal_function globals → list register → list register → Σcomplete: (list register) × (list register) × (list register). \fst (\fst complete) = \snd (\fst complete) ≝ 808 λglobals: list ident. 809 λdef. 810 λleft. 811 λright. 812 complete_regs globals def left right. 813 @complete_regs_length 814 qed. 815 816 definition translate_lt ≝ 817 λglobals: list ident. 818 λdestrs: list register. 819 λprf_destrs: 0 < destrs. 820 λsrcrs1: list register. 821 λsrcrs2: list register. 822 λstart_lbl: label. 823 λdest_lbl: label. 824 λdef: rtl_internal_function globals. 825 match destrs with 826 [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def 827  _ ⇒ 828 match fresh_regs_strong globals def (destrs) with 829 [ mk_Sig def_tmp_destrs tmp_destrs_proof ⇒ 830 let def ≝ \fst def_tmp_destrs in 831 let tmp_destrs ≝ \snd def_tmp_destrs in 832 let tmp_destr ≝ hd_safe ? tmp_destrs ? in 833 let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params1 globals def in 834 let 〈def, tmp_one〉 ≝ fresh_reg rtl_params1 globals def in 835 let 〈def, tmpr1〉 ≝ fresh_reg rtl_params1 globals def in 836 let 〈def, tmpr2〉 ≝ fresh_reg rtl_params1 globals def in 837 let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in 838 match complete_regs_strong globals def srcrs1 srcrs2 with 839 [ mk_Sig srcrs12_added srcrs12_proof ⇒ 840 let srcrs1 ≝ \fst (\fst srcrs12_added) in 841 let srcrs2 ≝ \snd (\fst srcrs12_added) in 842 let added ≝ \snd srcrs12_added in 843 let srcrs1' ≝ rev … srcrs1 in 844 let srcrs2' ≝ rev … srcrs2 in 845 let insts_init ≝ [ 846 translate_cst globals (Ointconst I8 (zero ?)) tmp_destrs; 847 translate_cst globals (Ointconst I8 (zero ?)) added; 848 adds_graph rtl_params1 globals [ 849 sequential rtl_params_ globals (INT rtl_params_ globals tmp_zero (zero …)); 850 sequential rtl_params_ globals (INT rtl_params_ globals tmp_one (bitvector_of_nat … 1)) 851 ] 852 ] 853 in 854 let insts_main ≝ 855 translate_lt_main globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in 856 let insts_main ≝ [ adds_graph rtl_params1 globals insts_main ] in 857 let insts_exit ≝ [ translate_move globals destrs tmp_destrs ] in 858 add_translates rtl_params1 globals (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def 859 ] 860 ] 861 ]. 862 [2: >tmp_destrs_proof @prf_destrs 863 1: normalize nodelta 864 generalize in match srcrs12_proof; 865 #HYP >rev_length >rev_length @HYP 866 ] 867 qed. 868 869 definition add_128_to_last ≝ 870 λglobals: list ident. 871 λtmp_128: register. 872 λrs. 873 λprf: 0 < rs. 874 λstart_lbl: label. 875 match rs with 876 [ nil ⇒ adds_graph rtl_params1 globals [ ] start_lbl 877  _ ⇒ 878 let r ≝ last_safe … rs prf in 879 adds_graph rtl_params1 globals [ 880 sequential rtl_params_ globals (OP2 rtl_params_ globals Add r r tmp_128) 881 ] start_lbl 882 ]. 883 884 definition translate_lts ≝ 885 λglobals: list ident. 886 λdestrs: list register. 887 λdestrs_prf: 0 < destrs. 888 λsrcrs1: list register. 889 λsrcrs2: list register. 890 λsrcrs1_lt_prf: 0 < srcrs1. 891 λsrcrs2_lt_prf: 0 < srcrs2. 892 λstart_lbl: label. 893 λdest_lbl: label. 894 λdef: rtl_internal_function globals. 895 match fresh_regs_strong globals def (srcrs1) with 896 [ mk_Sig def_tmp_srcrs1 srcrs1_prf ⇒ 897 let def ≝ \fst def_tmp_srcrs1 in 898 let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in 899 match fresh_regs_strong globals def (srcrs2) with 900 [ mk_Sig def_tmp_srcrs2 srcrs2_prf ⇒ 901 let def ≝ \fst def_tmp_srcrs2 in 902 let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in 903 let 〈def, tmp_128〉 ≝ fresh_reg rtl_params0 globals def in 904 add_translates rtl_params1 globals [ 905 translate_move globals tmp_srcrs1 srcrs1; 906 translate_move globals tmp_srcrs2 srcrs2; 907 adds_graph rtl_params1 globals [ 908 sequential rtl_params_ globals (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128)) 909 ]; 910 add_128_to_last globals tmp_128 tmp_srcrs1 ?; 911 add_128_to_last globals tmp_128 tmp_srcrs2 ?; 912 translate_lt globals destrs destrs_prf tmp_srcrs1 tmp_srcrs2 913 ] start_lbl dest_lbl def 914 ] 915 ]. 916 [1: >srcrs1_prf @srcrs1_lt_prf 917 2: >srcrs2_prf @srcrs2_lt_prf 918 ] 919 qed. 920 921 definition translate_op2 ≝ 922 λglobals: list ident. 923 λop2. 924 λdestrs: list register. 925 λdestrs_prf: 0 < destrs. 926 λsrcrs1: list register. 927 λsrcrs2: list register. 928 λsrcrs2_destrs_prf: srcrs2 = destrs. 929 λsrcrs1_destrs_prf: srcrs1 = destrs. 930 λstart_lbl: label. 931 λdest_lbl: label. 932 λdef: rtl_internal_function globals. 933 match op2 with 934 [ Oadd ⇒ 935 translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def 936  Oaddp ⇒ 937 translate_op globals Addc destrs srcrs1 srcrs2 start_lbl dest_lbl def 938  Osub ⇒ 939 translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 940  Osubpi ⇒ 941 translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 942  Osubpp sz ⇒ 943 translate_op globals Sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 944  Omul ⇒ 945 translate_mul globals destrs srcrs1 srcrs2 ? start_lbl dest_lbl def 946  Odivu ⇒ 947 match srcrs1 return λx. 0 < x → rtl_internal_function globals with 948 [ cons hd tl ⇒ λcons_prf. 949 match tl with 950 [ nil ⇒ translate_divumodu8 globals true destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def 951  _ ⇒ ? (* not implemented *) 952 ] 953  nil ⇒ λnil_absrd. ? 954 ] ? 955  Omodu ⇒ 956 match srcrs1 return λx. 0 < x → rtl_internal_function globals with 957 [ cons hd tl ⇒ λcons_prf. 958 match tl with 959 [ nil ⇒ translate_divumodu8 globals false destrs hd (hd_safe register srcrs2 ?) start_lbl dest_lbl def 960  _ ⇒ ? (* not implemented *) 961 ] 962  nil ⇒ λnil_absrd. ? 963 ] ? 964  Oand ⇒ 965 translate_op globals And destrs srcrs1 srcrs2 start_lbl dest_lbl def 966  Oor ⇒ 967 translate_op globals Or destrs srcrs1 srcrs2 start_lbl dest_lbl def 968  Oxor ⇒ 969 translate_op globals Xor destrs srcrs1 srcrs2 start_lbl dest_lbl def 970  Ocmp c ⇒ 971 match c with 972 [ Ceq ⇒ 973 add_translates rtl_params1 globals [ 974 translate_ne globals destrs srcrs1 srcrs2; 975 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (destrs)) 976 ] start_lbl dest_lbl def 977  Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def 978  Clt ⇒ translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ? start_lbl dest_lbl def 979  Cgt ⇒ translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ? start_lbl dest_lbl def 980  Cle ⇒ 981 add_translates rtl_params1 globals [ 982 translate_lts globals destrs destrs_prf srcrs2 srcrs1 ? ?; 983 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (destrs)) 984 ] start_lbl dest_lbl def 985  Cge ⇒ 986 add_translates rtl_params1 globals [ 987 translate_lts globals destrs destrs_prf srcrs1 srcrs2 ? ?; 988 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (destrs)) 989 ] start_lbl dest_lbl def 990 ] 991  Ocmpu c ⇒ 992 match c with 993 [ Ceq ⇒ 994 add_translates rtl_params1 globals [ 995 translate_ne globals destrs srcrs1 srcrs2; 996 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (destrs)) 997 ] start_lbl dest_lbl def 998  Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def 999  Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def 1000  Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def 1001  Cle ⇒ 1002 add_translates rtl_params1 globals [ 1003 translate_lt globals destrs destrs_prf srcrs2 srcrs1; 1004 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (destrs)) 1005 ] start_lbl dest_lbl def 1006  Cge ⇒ 1007 add_translates rtl_params1 globals [ 1008 translate_lt globals destrs destrs_prf srcrs1 srcrs2; 1009 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (destrs)) 1010 ] start_lbl dest_lbl def 1011 ] 1012  Ocmpp c ⇒ 1013 match c with 1014 [ Ceq ⇒ 1015 add_translates rtl_params1 globals [ 1016 translate_ne globals destrs srcrs1 srcrs2; 1017 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (destrs)) 1018 ] start_lbl dest_lbl def 1019  Cne ⇒ translate_ne globals destrs srcrs1 srcrs2 start_lbl dest_lbl def 1020  Clt ⇒ translate_lt globals destrs destrs_prf srcrs1 srcrs2 start_lbl dest_lbl def 1021  Cgt ⇒ translate_lt globals destrs destrs_prf srcrs2 srcrs1 start_lbl dest_lbl def 1022  Cle ⇒ 1023 add_translates rtl_params1 globals [ 1024 translate_lt globals destrs destrs_prf srcrs2 srcrs1; 1025 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (destrs)) 1026 ] start_lbl dest_lbl def 1027  Cge ⇒ 1028 add_translates rtl_params1 globals [ 1029 translate_lt globals destrs destrs_prf srcrs1 srcrs2; 1030 translate_op1 globals ?? (Onotbool (ASTint I8 Unsigned) I8 Unsigned I) destrs destrs (refl ? (destrs)) 1031 ] start_lbl dest_lbl def 1032 ] 1033  _ ⇒ ? (* assert false, implemented in run time or float op *) 1034 ]. 1035 [1: 1036 @sym_eq 1037 assumption 1038 3,8,19,22,24,25: 1039 >srcrs1_destrs_prf 1040 assumption 1041 4,9: 1042 normalize in nil_absrd; 1043 cases(not_le_Sn_O 0) 1044 #HYP cases(HYP nil_absrd) 1045 5,10,20,21,23,26: 1046 >srcrs2_destrs_prf 1047 assumption 1048 *: 1049 cases not_implemented (* XXX: yes, really *) 1050 ] 1051 qed. 1052 1053 definition translate_cond: ∀globals: list ident. list register → label → label → label → rtl_internal_function globals → rtl_internal_function globals ≝ 786 [1,2: % 787 *: cases re * #a #b >p1 normalize #EQ >EQ % 788 ] qed. 789 790 definition 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 ?. 808 whd in match new_srcrs1; whd in match new_srcrs2; 809 cases p1 810 cases p2 811 // 812 qed. 813 814 definition 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 821 definition 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 842 definition 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 887 definition translate_cond: ∀globals: list ident. list register → label → 888 bind_seq_block RTL globals (joint_step RTL globals) ≝ 1054 889 λglobals: list ident. 1055 890 λsrcrs: list register. 1056 λstart_lbl: label.1057 891 λlbl_true: label. 1058 λlbl_false: label. 1059 λdef: rtl_internal_function globals. 1060 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 1061 let 〈tmp_lbl, def〉 ≝ fresh_label rtl_params1 globals def in 1062 let init ≝ sequential rtl_params_ globals (INT rtl_params_ globals tmpr (zero …)) in 1063 let f ≝ λsrcr. sequential rtl_params_ globals (OP2 rtl_params_ globals Or tmpr tmpr srcr) in 1064 let def ≝ adds_graph rtl_params1 globals (init :: (map ? ? f srcrs)) start_lbl tmp_lbl def in 1065 add_graph rtl_params1 globals tmp_lbl (sequential rtl_params_ globals (COND rtl_params_ globals tmpr lbl_true) lbl_false) def. 1066 1067 definition translate_load ≝ 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) *) 903 definition translate_load : ∀globals.?→?→?→bind_new (localsT RTL) ? ≝ 1068 904 λglobals: list ident. 1069 λaddr .905 λaddr : list psd_argument. 1070 906 λaddr_prf: 2 = addr. 1071 907 λdestrs: list register. 1072 λstart_lbl: label. 1073 λdest_lbl: label. 1074 λdef: rtl_internal_function globals. 1075 match fresh_regs_strong rtl_params0 globals def (addr) with 1076 [ mk_Sig def_save_addr save_addr_prf ⇒ 1077 let def ≝ \fst def_save_addr in 1078 let save_addr ≝ \snd def_save_addr in 1079 match fresh_regs_strong rtl_params0 globals def (addr) with 1080 [ mk_Sig def_tmp_addr tmp_addr_prf ⇒ 1081 let def ≝ \fst def_tmp_addr in 1082 let tmp_addr ≝ \snd def_tmp_addr in 1083 let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in 1084 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 1085 let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in 1086 let insts_save_addr ≝ translate_move globals save_addr addr in 1087 let f ≝ λtranslates_off. λr. 1088 let 〈translates, off〉 ≝ translates_off in 1089 let translates ≝ translates @ [ 1090 adds_graph rtl_params1 globals [ 1091 sequential rtl_params_ globals (INT rtl_params_ globals tmpr off) 1092 ]; 1093 translate_op2 globals Oaddp tmp_addr ? save_addr [dummy; tmpr] ? ?; 1094 adds_graph rtl_params1 globals [ 1095 sequential rtl_params_ globals (LOAD rtl_params_ globals r tmp_addr1 tmp_addr2) 1096 ] 1097 ] 1098 in 1099 let 〈carry, result〉 ≝ half_add … off int_size in 1100 〈translates, result〉 1101 in 1102 let 〈translates, ignore〉 ≝ foldl … f 〈[ ], (zero ?)〉 destrs in 1103 add_translates rtl_params1 globals (insts_save_addr :: translates) start_lbl dest_lbl def 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 921 definition 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 938 lemma 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 945 elim (Exists_All … r_ok env_typed) 946 * #r' #ty' * #EQ destruct(EQ) * #rs * #EQ1 #EQ2 #prf 947 whd in match find_local_env; normalize nodelta 948 @opt_safe_elim #rs' >EQ1 #EQ' destruct assumption 949 qed. 950 951 lemma 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 958 whd in match find_local_env_arg; normalize nodelta 959 >length_map @lenv_typed_reg_typed_ok1 assumption 960 qed. 961 962 lemma 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 968 elim (Exists_All … r_ok env_typed) 969 * #r' #ty' * #EQ destruct(EQ) * #rs * #EQ1 #EQ2 970 whd in ⊢ (?%); 971 >EQ1 % 972 qed. 973 974 lemma cst_size_ok : ∀ty,cst.size_of_sig_type ty=size_of_cst ty cst. 975 #ty * ty [*] // 976 qed. 977 978 definition 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_jumptable r l ⇒ ⊥ (* assert false: not implemented yet *) 1028  St_return ⇒ λ_. ❬inr … (RETURN ?),it❭ 1029 ]. 1030 [ >(lenv_typed_reg_typed_ok1 … lenv_typed stmt_typed) 1031 @cst_size_ok 1032  @(lenv_typed_reg_typed_ok2 … lenv_typed stmt_typed) 1033  cases daemon (* needs more hypotheses *) 1034 4,5,6,7: cases stmt_typed #dstr_typed #srcr_typed 1035 [1,2: @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption 1036  @(lenv_typed_reg_typed_ok2 … lenv_typed srcr_typed) 1037  @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_typed) 1104 1038 ] 1105 ]. 1106 [1: >tmp_addr_prf >save_addr_prf % 1107 2: >save_addr_prf >tmp_addr_prf 1108 @addr_prf 1109 3: >tmp_addr_prf normalize 1110 <addr_prf // 1111 4: >tmp_addr_prf assumption 1112 ] 1113 qed. 1114 1115 definition translate_store ≝ 1116 λglobals: list ident. 1117 λaddr. 1118 λaddr_prf: 2 = addr. 1119 λsrcrs: list register. 1120 λstart_lbl: label. 1121 λdest_lbl: label. 1122 λdef: rtl_internal_function globals. 1123 match fresh_regs_strong rtl_params0 globals def (addr) with 1124 [ mk_Sig def_tmp_addr tmp_addr_prf ⇒ 1125 let def ≝ \fst def_tmp_addr in 1126 let tmp_addr ≝ \snd def_tmp_addr in 1127 let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in 1128 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 1129 let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in 1130 let f ≝ λtranslate_off. λsrcr. 1131 let 〈translates, off〉 ≝ translate_off in 1132 let translates ≝ translates @ [ 1133 adds_graph rtl_params1 globals [ 1134 sequential rtl_params_ globals (INT rtl_params_ globals tmpr off) 1135 ]; 1136 translate_op2 globals Oaddp tmp_addr … addr [dummy; tmpr] ? ?; 1137 adds_graph rtl_params1 globals [ 1138 sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr) 1139 ] 1140 ] 1141 in 1142 let 〈carry, result〉 ≝ half_add … off int_size in 1143 〈translates, result〉 1144 in 1145 let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero …〉 srcrs in 1146 add_translates rtl_params1 globals translates start_lbl dest_lbl def 1147 ]. 1148 [1: >tmp_addr_prf % 1149 2: >tmp_addr_prf normalize 1150 <addr_prf // 1151 3: >tmp_addr_prf <addr_prf // 1152 4: >tmp_addr_prf @addr_prf 1153 ] 1154 qed. 1155 1156 axiom fake_label: label. 1157 1158 (* XXX: following conversation with CSC about the mix up in extension statements 1159 and extension instructions in RTL, use fake_label in calls to 1160 tailcall_* instructions. *) 1161 definition translate_stmt ≝ 1162 λglobals: list ident. 1163 λlenv: local_env. 1164 λlbl: label. 1165 λstmt. 1166 λdef: rtl_internal_function globals. 1167 match stmt with 1168 [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def 1169  St_cost cost_lbl lbl' ⇒ add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (COST_LABEL rtl_params_ globals cost_lbl) lbl') def 1170  St_const destr cst lbl' ⇒ 1171 translate_cst globals cst (find_local_env destr lenv) lbl lbl' def 1172  St_op1 ty ty' op1 destr srcr lbl' ⇒ 1173 translate_op1 globals ty ty' op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def 1174  St_op2 op2 destr srcr1 srcr2 lbl' ⇒ 1175 translate_op2 globals op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def 1176 (* XXX: should we be ignoring this? *) 1177  St_load ignore addr destr lbl' ⇒ 1178 translate_load globals (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def 1179 (* XXX: should we be ignoring this? *) 1180  St_store ignore addr srcr lbl' ⇒ 1181 translate_store globals (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def 1182  St_call_id f args retr lbl' ⇒ 1183 match retr with 1184 [ Some retr ⇒ 1185 add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) (find_local_env retr lenv)) lbl') def 1186  None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) [ ]) lbl') def 1039 8,9,10,11,12,13: 1040 cases stmt_typed * #srcrs1_prf #srcrs2_prf #dstr_prf 1041 [1,2: @(lenv_typed_arg_typed_ok1 … lenv_typed) assumption 1042  @(lenv_typed_reg_typed_ok1 … lenv_typed) assumption 1043  @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs2_prf) 1044  @(lenv_typed_reg_typed_ok2 … lenv_typed srcrs1_prf) 1045  @(lenv_typed_reg_typed_ok2 … lenv_typed dstr_prf) 1187 1046 ] 1188  St_call_ptr f args retr lbl' ⇒ 1189 match retr with 1190 [ None ⇒ 1191 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in 1192 add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])) lbl') def 1193  Some retr ⇒ 1194 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in 1195 add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv))) lbl') def 1196 ] 1197  St_tailcall_id f args ⇒ 1198 add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params_ globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) fake_label) def 1199  St_tailcall_ptr f args ⇒ 1200 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in 1201 add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params1 globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) fake_label) def 1202  St_cond r lbl_true lbl_false ⇒ 1203 translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def 1204  St_jumptable r l ⇒ ? (* assert false: not implemented yet *) 1205  St_return ⇒ add_graph rtl_params1 globals lbl (RETURN …) def 1206 ]. 1207 [10: cases not_implemented (* jtable case *) 1208 *: cases daemon (* TODO: proofs regarding lengths of lists, examine! *) 1047 *: whd in stmt_typed; cases daemon (* TODO need more stringent statement_typed *) 1209 1048 ] 1210 1049 qed. … … 1217 1056 λglobals: list ident. 1218 1057 λdef. 1219 let runiverse ≝ f_reggen def in 1220 let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse 1221 (f_params def @ f_locals def) (f_result def) in 1222 let params ≝ map_list_local_env lenv (map … \fst (f_params def)) in 1223 let locals ≝ map_list_local_env lenv (map … \fst (f_locals def)) in 1224 let result ≝ 1225 match (f_result def) with 1226 [ None ⇒ [ ] 1227  Some r_typ ⇒ 1228 let 〈r, typ〉 ≝ r_typ in 1229 find_local_env r lenv 1230 ] 1231 in 1058 let runiverse' ≝ f_reggen def in 1232 1059 let luniverse' ≝ f_labgen def in 1233 let runiverse' ≝ runiverse in1234 let result' ≝ result in1235 let params' ≝ params in1236 let locals' ≝ locals in1237 1060 let stack_size' ≝ f_stacksize def in 1238 1061 let entry' ≝ f_entry def in 1239 1062 let exit' ≝ f_exit def in 1240 let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params_ globals entry') in 1241 let graph' ≝ add LabelTag ? graph' exit' (GOTO rtl_params_ globals exit') in 1242 let res ≝ 1243 mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params' 1244 locals' stack_size' graph' ? ? in 1245 foldi … (translate_stmt globals … lenv) (f_graph def) res. 1246 [ % [@entry'  @graph_add_lookup @graph_add] 1247  % [@exit'  @graph_add]] 1063 let init ≝ init_graph_if RTL globals luniverse' runiverse' [ ] [ ] 1064 [ ] stack_size' (pi1 … entry') (pi1 … exit') in 1065 let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals 1066 (f_locals def) (f_params def) (f_result def) init in 1067 let vars ≝ (f_locals def) @ (f_params def) @ 1068 match f_result def with [ Some x ⇒ [x]  _ ⇒ [ ] ] in 1069 let f_trans ≝ λlbl,stmt,def. 1070 let pr ≝ translate_statement … vars lenv ? stmt ? in 1071 b_adds_graph … (rtl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in 1072 foldi … f_trans (f_graph def) init'. (* TODO *) cases daemon 1248 1073 qed. 1249 1074 … … 1252 1077 definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝ 1253 1078 λp. transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)). 1254 1255 *)1256 axiom rtlabs_to_rtl: RTLabs_program → rtl_program.1257
Note: See TracChangeset
for help on using the changeset viewer.