Changeset 1882 for src/RTLabs/RTLabsToRTL_paolo.ma
 Timestamp:
 Apr 6, 2012, 8:02:10 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL_paolo.ma
r1644 r1882 28 28 definition local_env ≝ identifier_map RegisterTag (list register). 29 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 []. 30 definition local_env_typed : 31 list (register × typ) → local_env → Prop ≝ 32 λl,env.All ? 33 (λp.let 〈r, ty〉 ≝ p in ∃regs.lookup … env r = Some ? regs ∧ 34 regs = size_of_sig_type ty) l. 35 36 definition find_local_env ≝ λr.λlenv : local_env. 37 λprf : r ∈ lenv.opt_safe … (lookup … lenv r) ?. 38 lapply (in_map_domain … lenv r) 39 >prf * #x #lookup_eq >lookup_eq % #ABS destruct(ABS) 40 qed. 41 42 lemma find_local_env_elim : ∀P : list register → Prop.∀r. ∀lenv: local_env.∀prf. 43 (∀x.lookup … lenv r = Some ? x → P x) → P (find_local_env r lenv prf). 44 #P#r#lenv#prf #H 45 change with (P (opt_safe ???)) 46 @opt_safe_elim assumption 47 qed. 38 48 39 49 definition find_local_env_arg ≝ 40 λr,lenv . map … Reg (find_local_env r lenv).50 λr,lenv,prf. map … Reg (find_local_env r lenv prf). 41 51 42 52 let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝ … … 49 59 50 60 definition initialize_local_env_internal ≝ 51 λlenv_runiverse .61 λlenv_runiverse : local_env × ?. 52 62 λr_sig. 53 63 let 〈lenv,runiverse〉 ≝ lenv_runiverse in … … 55 65 let size ≝ size_of_sig_type sig in 56 66 let 〈rs,runiverse〉 ≝ register_freshes runiverse size in 57 〈add _local_env r rs lenv,runiverse〉.67 〈add … lenv r rs,runiverse〉. 58 68 59 69 definition initialize_local_env ≝ … … 70 80 71 81 definition map_list_local_env_internal ≝ 72 λlenv,res,r . res @ (find_local_env r lenv).82 λlenv,res,r_sig. res @ (find_local_env (pi1 … r_sig) lenv (pi2 … r_sig)). 73 83 74 84 definition map_list_local_env ≝ … … 80 90 λprf: 2 = length A lst. 81 91 match lst return λx. 2 = x → A × A with 82 [ nil ⇒ λlst_nil_prf. ?92 [ nil ⇒ λlst_nil_prf. ⊥ 83 93  cons hd tl ⇒ λprf. 84 94 match tl return λx. 1 = x → A × A with 85 [ nil ⇒ λtl_nil_prf. ?95 [ nil ⇒ λtl_nil_prf. ⊥ 86 96  cons hd' tl' ⇒ λtl_cons_prf. 〈hd, hd'〉 87 97 ] ? … … 98 108 99 109 definition find_and_addr ≝ 100 λr,lenv . make_addr ? (find_local_env r lenv).110 λr,lenv,prf. make_addr ? (find_local_env r lenv prf). 101 111 102 112 definition rtl_args ≝ 103 λ regs_list,lenv. flatten … (map … (λr.find_local_env_arg r lenv) regs_list).113 λlenv,regs_list. flatten … (map … (λr.find_local_env_arg (pi1 … r) lenv (pi2 … r)) regs_list). 104 114 105 115 definition split_into_bytes: … … 119 129 qed. 120 130 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.126 127 131 definition translate_op: 128 132 ∀globals. Op2 → … … 131 135 ∀srcrs2 : list rtl_argument. 132 136 dests = srcrs1 → srcrs1 = srcrs2 → 133 list (rtl_ instructionglobals)137 list (rtl_step globals) 134 138 ≝ 135 139 λglobals: list ident. … … 140 144 λprf1,prf2. 141 145 let f_add ≝ OP2 rtl_params globals in 142 let res : list (rtl_ instructionglobals) ≝146 let res : list (rtl_step globals) ≝ 143 147 map3 ???? (f_add op) destrs srcrs1 srcrs2 ?? in 144 148 (* first, clear carry if op relies on it *) … … 151 155 (* if adding, we use a first Add op, that clear the carry, and then Addc's *) 152 156 [ Add ⇒ 153 match destrs return λx.destrs = x → list (rtl_ instructionglobals) with157 match destrs return λx.destrs = x → list (rtl_step globals) with 154 158 [ nil ⇒ λeq_destrs.[ ] 155 159  cons destr destrs' ⇒ λeq_destrs. 156 match srcrs1 return λy.srcrs1 = y → list (rtl_ instructionglobals) with160 match srcrs1 return λy.srcrs1 = y → list (rtl_step globals) with 157 161 [ nil ⇒ λeq_srcrs1.⊥ 158 162  cons srcr1 srcrs1' ⇒ λeq_srcrs1. 159 match srcrs2 return λz.srcrs2 = z → list (rtl_ instructionglobals) with163 match srcrs2 return λz.srcrs2 = z → list (rtl_step globals) with 160 164 [ nil ⇒ λeq_srcrs2.⊥ 161 165  cons srcr2 srcrs2' ⇒ λeq_srcrs2. … … 196 200  _ ⇒ True 197 201 ]. 202 198 203 definition translate_cst : 199 204 ∀globals: list ident. 200 205 ∀cst_sig: Σcst : constant.cst_well_defd globals cst. 201 206 ∀destrs: list register. 202 destrs = size_of_cst cst_sig → list (rtl_ instructionglobals)207 destrs = size_of_cst cst_sig → list (rtl_step globals) 203 208 ≝ 204 209 λglobals,cst_sig,destrs,prf. 205 match cst_sig return λy.cst_sig = y → list (rtl_ instructionglobals) with210 match cst_sig return λy.cst_sig = y → list (rtl_step globals) with 206 211 [ mk_Sig cst cst_good ⇒ λeqcst_sig. 207 match cst return λx.cst = x → list (rtl_ instructionglobals)212 match cst return λx.cst = x → list (rtl_step globals) 208 213 with 209 214 [ Ointconst size const ⇒ λeqcst. … … 218 223  Oaddrstack offset ⇒ λeqcst. 219 224 let 〈r1, r2〉 ≝ make_addr … destrs ? in 220 [(rtl_st_ext_stack_address r1 r2 : rtl_ instructionglobals)]225 [(rtl_st_ext_stack_address r1 r2 : rtl_step globals)] 221 226 ] (refl …) 222 227 ] (refl …). … … 235 240 ∀destrs: list register. 236 241 ∀srcrs: list rtl_argument. 237 destrs = srcrs → list (rtl_ instructionglobals) ≝242 destrs = srcrs → list (rtl_step globals) ≝ 238 243 λglobals,destrs,srcrs,length_eq. 239 244 map2 … (λdst,src.dst ← src) destrs srcrs length_eq. … … 259 264 qed. 260 265 261 definition sign_mask : ∀globals.register → register → list (rtl_ instructionglobals) ≝266 definition sign_mask : ∀globals.register → register → list (rtl_step globals) ≝ 262 267 (* this sets destr to 0xFF if s is neg, 0x00 o.w. Done like that: 263 268 byte in destr if srcr is: neg  pos … … 275 280 definition translate_cast_signed : 276 281 ∀globals : list ident. 277 list register → register → bind_list register unit (rtl_instructionglobals) ≝282 list register → register → bind_list register (rtl_step globals) ≝ 278 283 λglobals,destrs,srcr. 279 284 ν tmp in … … 283 288 definition translate_cast_unsigned : 284 289 ∀globals : list ident. 285 list register → list (rtl_ instructionglobals) ≝290 list register → list (rtl_step globals) ≝ 286 291 λglobals,destrs. 287 292 match nat_to_args (destrs) 0 with … … 296 301 ∀globals: list ident. 297 302 signedness → list register → list register → 298 bind_list register unit (rtl_instructionglobals) ≝303 bind_list register (rtl_step globals) ≝ 299 304 λglobals,src_sign,destrs,srcrs. 300 305 match srcrs 301 return λy. y = srcrs → bind_list register unit (rtl_instructionglobals)306 return λy. y = srcrs → bind_list register (rtl_step globals) 302 307 with 303 308 [ nil ⇒ λ_.translate_cast_unsigned ? destrs (* srcrs = [ ] ⇒ we fill with 0 *) … … 306 311 [ mk_Sig crl len_proof ⇒ 307 312 (* move prefix of srcrs in destrs *) 308 translate_move ? (\fst (\fst crl)) (map … Reg (\fst (\snd crl))) ? @ 309 match \snd (\snd crl) with313 translate_move ? (\fst (\fst crl)) (map … Reg (\fst (\snd crl))) ? @@ 314 match \snd (\snd crl) return λ_.bind_list ?? with 310 315 [ nil ⇒ 311 match src_sign return λ_.bind_list register unit (rtl_instructionglobals) with316 match src_sign return λ_.bind_list register (rtl_step globals) with 312 317 [ Unsigned ⇒ translate_cast_unsigned ? (\snd (\fst crl)) 313 318  Signed ⇒ … … 326 331 ∀destrs : list register. 327 332 ∀srcrs_arg : list register. 328 destrs = srcrs_arg → list (rtl_ instructionglobals) ≝333 destrs = srcrs_arg → list (rtl_step globals) ≝ 329 334 λglobals, destrs, srcrs, prf. 330 335 map2 ??? (OP1 rtl_params globals Cmpl) destrs srcrs prf. 331 336 332 333 definition translate_negint : ∀globals.? → ? → ? → bind_list register unit (rtl_instruction globals) ≝ 337 definition translate_negint : ∀globals.? → ? → ? → bind_list register (rtl_step globals) ≝ 334 338 λglobals: list ident. 335 339 λdestrs: list register. … … 346 350 ∀globals : list ident. 347 351 list register → list register → 348 bind_list register unit (rtl_instructionglobals) ≝352 bind_list register (rtl_step globals) ≝ 349 353 λglobals,destrs,srcrs. 350 354 match destrs with 351 355 [ nil ⇒ [ ] 352 356  cons destr destrs' ⇒ 353 translate_cast_unsigned ? destrs' @ (* fill destrs' with 0 *)357 translate_cast_unsigned ? destrs' @@ (* fill destrs' with 0 *) 354 358 match srcrs with 355 359 [ nil ⇒ [destr ← 0] 356 360  cons srcr srcrs' ⇒ 357 let f : register → rtl_ instructionglobals ≝361 let f : register → rtl_step globals ≝ 358 362 λr. destr ← destr .Or. r in 359 MOVE rtl_params globals 〈destr,srcr〉 ::360 map … f srcrs'@363 (destr ← srcr) ::: ? ]]. 364 map ?? f srcrs' @@ 361 365 (* now destr is nonnull iff srcrs was nonnull *) 362 366 CLEAR_CARRY ? ? :: … … 371 375 372 376 definition translate_op1 : ∀globals.? → ? → ? → ? → ? → ? → ? → 373 bind_list register unit (rtl_ instructionglobals) ≝377 bind_list register unit (rtl_step globals) ≝ 374 378 λglobals. 375 379 λty, ty'. … … 381 385 match op1 382 386 return λty'',ty'''.λx : unary_operation ty'' ty'''.ty'' = ty → ty''' = ty' → 383 bind_list register unit (rtl_ instructionglobals) with387 bind_list register unit (rtl_step globals) with 384 388 [ Ocastint _ src_sign _ _ ⇒ λeq1,eq2. 385 389 translate_cast globals src_sign destrs srcrs … … 440 444 (Σi.i<S k) → 441 445 (* the accumulator *) 442 list (rtl_ instructionglobals) →443 list (rtl_ instructionglobals) ≝446 list (rtl_step globals) → 447 list (rtl_step globals) ≝ 444 448 λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2, 445 449 tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc. … … 488 492 ] qed. 489 493 490 definition translate_mul : ∀globals.?→?→?→?→?→bind_list register unit (rtl_ instructionglobals) ≝494 definition translate_mul : ∀globals.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝ 491 495 λglobals : list ident. 492 496 λdestrs : list register. … … 504 508 (* the step calculating all products with least significant byte going in the 505 509 kth position of the result *) 506 let translate_mul_k : (Σk.k<destrs) → list (rtl_ instructionglobals) →507 list (rtl_ instructionglobals) ≝510 let translate_mul_k : (Σk.k<destrs) → list (rtl_step globals) → 511 list (rtl_step globals) ≝ 508 512 λk_sig,acc.match k_sig with 509 513 [ mk_Sig k k_prf ⇒ … … 528 532 529 533 definition translate_divumodu8 : ∀globals.?→?→?→?→?→?→ 530 bind_list register unit (rtl_ instructionglobals) ≝534 bind_list register unit (rtl_step globals) ≝ 531 535 λglobals: list ident. 532 536 λdiv_not_mod: bool. … … 536 540 λsrcrs1_prf : destrs = srcrs1. 537 541 λsrcrs2_prf : srcrs1 = srcrs2. 538 let return_type ≝ bind_list register unit (rtl_ instructionglobals) in542 let return_type ≝ bind_list register unit (rtl_step globals) in 539 543 match destrs return λx.x = destrs → return_type with 540 544 [ nil ⇒ λ_.[ ] … … 575 579 qed. 576 580 577 definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_ instructionglobals) ≝581 definition translate_ne: ∀globals: list ident.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝ 578 582 λglobals: list ident. 579 583 λdestrs: list register. … … 582 586 λsrcrs1_prf : destrs = srcrs1. 583 587 λsrcrs2_prf : srcrs1 = srcrs2. 584 let return_type ≝ bind_list register unit (rtl_ instructionglobals) in588 let return_type ≝ bind_list register unit (rtl_step globals) in 585 589 match destrs return λx.x = destrs → return_type with 586 590 [ nil ⇒ λ_.[ ] … … 593 597  cons srcr2 srcrs2' ⇒ λeq_srcrs2. 594 598 νtmpr in 595 let f : rtl_argument → rtl_argument → list (rtl_ instruction globals) → list (rtl_instructionglobals) ≝599 let f : rtl_argument → rtl_argument → list (rtl_step globals) → list (rtl_step globals) ≝ 596 600 λs1,s2,acc. 597 601 tmpr ← s1 .Xor. s2 :: 598 602 destr ← destr .Or. tmpr :: 599 603 acc in 600 let epilogue : list (rtl_ instructionglobals) ≝604 let epilogue : list (rtl_step globals) ≝ 601 605 [ CLEAR_CARRY … ; 602 606 tmpr ← 0 .Sub. destr ; … … 613 617 (* if destrs is 0 or 1, it inverses it. To be used after operations that 614 618 ensure this. *) 615 definition translate_toggle_bool : ∀globals.?→list (rtl_ instructionglobals) ≝619 definition translate_toggle_bool : ∀globals.?→list (rtl_step globals) ≝ 616 620 λglobals: list ident. 617 621 λdestrs: list register. … … 628 632 destrs = srcrs1 → 629 633 srcrs1 = srcrs2 → 630 list (rtl_ instructionglobals) ≝634 list (rtl_step globals) ≝ 631 635 λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf. 632 636 match destrs with … … 645 649 (tmp : register) 646 650 (srcrs : list rtl_argument) on srcrs : 647 (list rtl_argument) × (list (rtl_ instructionglobals)) ≝651 (list rtl_argument) × (list (rtl_step globals)) ≝ 648 652 match srcrs with 649 653 [ nil ⇒ 〈[ ],[ ]〉 … … 674 678 destrs = srcrs1 → 675 679 srcrs1 = srcrs2 → 676 bind_list register unit (rtl_ instructionglobals) ≝680 bind_list register unit (rtl_step globals) ≝ 677 681 λglobals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf. 678 682 νtmp_last_s1 in … … 688 692 >shift_signed_length [2: >shift_signed_length] assumption qed. 689 693 690 definition translate_lt : bool→∀globals.?→?→?→?→?→bind_list register unit (rtl_ instructionglobals) ≝694 definition translate_lt : bool→∀globals.?→?→?→?→?→bind_list register unit (rtl_step globals) ≝ 691 695 λis_unsigned,globals,destrs,srcrs1,srcrs2,srcrs1_prf,srcrs2_prf. 692 696 if is_unsigned then … … 717 721 718 722 definition translate_op2 : 719 ∀globals.?→?→?→?→?→?→bind_list register unit (rtl_ instructionglobals) ≝723 ∀globals.?→?→?→?→?→?→bind_list register unit (rtl_step globals) ≝ 720 724 λglobals: list ident. 721 725 λop2. … … 758 762 cases not_implemented (* XXX: yes, really *) qed. 759 763 760 definition translate_cond: ∀globals: list ident. list register → label → bind_list register unit (rtl_ instructionglobals) ≝764 definition translate_cond: ∀globals: list ident. list register → label → bind_list register unit (rtl_step globals) ≝ 761 765 λglobals: list ident. 762 766 λsrcrs: list register. … … 766 770  cons srcr srcrs' ⇒ 767 771 ν tmpr in 768 let f : register → rtl_ instructionglobals ≝772 let f : register → rtl_step globals ≝ 769 773 λr. tmpr ← tmpr .Or. r in 770 774 MOVE rtl_params globals 〈tmpr,srcr〉 :: … … 781 785 ν tmp_addr_l in 782 786 ν tmp_addr_h in 783 let f ≝ λdestr : register.λacc : list (rtl_ instructionglobals).787 let f ≝ λdestr : register.λacc : list (rtl_step globals). 784 788 LOAD rtl_params globals destr (Reg tmp_addr_l) (Reg tmp_addr_h) :: 785 789 translate_op … Add … … 798 802 ν tmp_addr_l in 799 803 ν tmp_addr_h in 800 let f ≝ λsrcr : rtl_argument.λacc : list (rtl_ instructionglobals).804 let f ≝ λsrcr : rtl_argument.λacc : list (rtl_step globals). 801 805 STORE rtl_params globals (Reg tmp_addr_l) (Reg tmp_addr_h) srcr :: 802 806 translate_op … Add … … 822 826 823 827 definition translate_inst : ∀globals.?→?→?→ 824 (bind_list register unit (rtl_ instructionglobals)) × label ≝828 (bind_list register unit (rtl_step globals)) × label ≝ 825 829 λglobals: list ident. 826 830 λlenv: local_env. 827 831 λstmt. 832 λstmt_typed : 828 833 λstmt_prf : stmt_not_final stmt. 829 834 match stmt return λx.stmt = x → 830 (bind_list register unit (rtl_ instructionglobals)) × label with835 (bind_list register unit (rtl_step globals)) × label with 831 836 [ St_skip lbl' ⇒ λ_. 832 837 〈[ ], lbl'〉 … … 865 870 (* Paolo: no notation to avoid ambiguity *) 866 871 〈bcons … ( 867 match retr return λ_.rtl_ instructionglobals with872 match retr return λ_.rtl_step globals with 868 873 [ Some retr ⇒ 869 874 rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv)
Note: See TracChangeset
for help on using the changeset viewer.