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