 Timestamp:
 Aug 5, 2011, 1:47:34 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1054 r1103 441 441 let 〈p1, p2〉 ≝ split ? 5 11 pc in 442 442 if eq_bv ? a1 p1 then (* we're in the same segment *) 443 〈 3, 2, address, Some ? medium_jump〉443 〈2, 2, address, Some ? medium_jump〉 444 444 else 445 〈 3, 3, address, Some ? long_jump〉.445 〈2, 3, address, Some ? long_jump〉. 446 446 447 lemma frc_ok:447 (* lemma frc_ok: 448 448 ∀pc.∀j_addr. 449 449 let 〈i1,i2,addr,jl〉 ≝ find_right_call pc j_addr in … … 462 462 [ %1 [ @refl  @(eq_bv_eq … H) ] 463 463  %1 [ @refl  // ] ] 464 qed. 464 qed. *) 465 465 466 466 definition distance ≝ … … 474 474 let pa ≝ nat_of_bitvector ? address in 475 475 if ltb (distance pn pa) 127 then 476 〈2, 3, address, Some ? short_jump〉476 〈2, 2, address, Some ? short_jump〉 477 477 else 478 478 find_right_call pc address. 479 479 480 lemma frj_ok:480 (* lemma frj_ok: 481 481 ∀pc.∀j_addr. 482 482 let 〈i1,i2,addr,jl〉 ≝ find_right_jump pc j_addr in … … 502 502 ] 503 503 ] 504 qed. 504 qed. *) 505 505 506 506 definition find_right_relative_jump: Word → (BitVectorTrie (Word × Identifier) 16) → … … 508 508 λpc.λlabels.λjmp. 509 509 match lookup_opt ? ? jmp labels with 510 [ None ⇒ 〈 3, 3, pc, Some ? long_jump〉510 [ None ⇒ 〈2, 2, pc, Some ? short_jump〉 511 511  Some x ⇒ let 〈ignore, a〉 ≝ x in find_right_jump pc a ]. 512 512 513 lemma frrj_ok:513 (* lemma frrj_ok: 514 514 ∀pc.∀labels.∀j_id. 515 515 let 〈i1,i2,addr,jl〉 ≝ find_right_relative_jump pc labels j_id in … … 536 536 ] 537 537 ] 538 qed. 538 qed. *) 539 539 540 540 definition jep_relative: Word → (BitVectorTrie (Word × Identifier) 16) → preinstruction Identifier → ? ≝ … … 553 553 〈l, l, pc, None …〉 ]. 554 554 555 definition jgeq_opt ≝556 λa:jump_length.λb:option (Word × jump_length).557 match a with558 [ short_jump ⇒ match b with559 [ None ⇒ (* XXX *) False560  Some x ⇒ let 〈ignore,j〉 ≝ x in j = short_jump561 ]562  medium_jump ⇒ match b with563 [ None ⇒ (* XXX *) False564  Some x ⇒ let 〈ignore,j〉 ≝ x in j = short_jump ∨ j = medium_jump ]565  long_jump ⇒ True566 ].567 568 555 definition is_long_jump ≝ 569 556 λj.match j with … … 573 560 574 561 definition policy_safe ≝ 575 λp:BitVectorTrie (Word × Word × jump_length) 16. 576 forall ? ? p (λ_.λx.let 〈pc,addr,j〉 ≝ x in 562 (λ_:Word.λx:Word×Word×jump_length.let 〈pc,addr,j〉 ≝ x in 577 563 match j with 578 564 [ short_jump ⇒ distance (nat_of_bitvector ? pc) (nat_of_bitvector ? addr) < 127 … … 583 569 584 570 definition jump_expansion_policy ≝ 585 Σpolicy:BitVectorTrie (Word × Word × jump_length) 16.policy_safe policy. 571 Σpolicy:BitVectorTrie (Word × Word × jump_length) 16. 572 forall ? ? policy policy_safe. 586 573 587 574 definition inject_jump_expansion_policy: 588 ∀ x:BitVectorTrie (Word × Word × jump_length) 16.589 policy_safe x→ jump_expansion_policy ≝ inject ….575 ∀p:BitVectorTrie (Word × Word × jump_length) 16. 576 forall ? ? p policy_safe → jump_expansion_policy ≝ inject …. 590 577 591 578 coercion inject_jump_expansion_policy: 592 ∀x:BitVectorTrie (Word × Word × jump_length) 16. 593 policy_safe x → jump_expansion_policy ≝ inject_jump_expansion_policy 594 on x:(BitVectorTrie (Word × Word × jump_length) 16) to jump_expansion_policy. 579 ∀p:BitVectorTrie (Word × Word × jump_length) 16. 580 forall ? ? p policy_safe → jump_expansion_policy ≝ inject_jump_expansion_policy 581 on p:(BitVectorTrie (Word × Word × jump_length) 16) to jump_expansion_policy. 582 583 (* the jump length in a is greater than or equal to the jump length in b *) 584 definition jump_length_decrease ≝ 585 λa:jump_length.λb:jump_length. 586 match a with 587 [ short_jump ⇒ b = short_jump 588  medium_jump ⇒ b = short_jump ∨ b = medium_jump 589  long_jump ⇒ True 590 ]. 595 591 596 592 definition jump_expansion_policy_internal: pseudo_assembly_program → 597 593 (BitVectorTrie (Word × Identifier) 16) → jump_expansion_policy → 598 594 Σres:(BitVectorTrie (Word × Identifier) 16) × (BitVectorTrie (Word × Word × jump_length) 16). 599 let 〈x,p〉 ≝ res in policy_safe p ≝ 595 let 〈x,p〉 ≝ res in 596 True ≝ 600 597 λprogram.λold_labels.λold_policy. 601 598 let res ≝ 602 599 foldl_strong (option Identifier × pseudo_instruction) 603 (λprefix.Σresult:(Word × Word) × ((BitVectorTrie (Word × Identifier) 16) × 604 (BitVectorTrie (Word × Word × jump_length) 16)). 605 let 〈x,y,z,p〉 ≝ result in policy_safe p 606 ) 600 (λprefix.Σres.True) 607 601 (\snd program) 608 602 (λprefix.λi.λtl.λprf.λacc. … … 616 610 [ Call c ⇒ 617 611 match lookup_opt ? ? c new_labels with 618 [ None ⇒ 〈 3, 3, pc, Some ? long_jump〉612 [ None ⇒ 〈2, 2, pc, Some ? short_jump〉 619 613  Some x ⇒ let 〈ignore,c_addr〉 ≝ x in find_right_call pc c_addr ] 620 614  Jmp j ⇒ 621 615 match lookup_opt ? ? j new_labels with 622 [ None ⇒ 〈 3, 3, pc, Some ? long_jump〉616 [ None ⇒ 〈2, 2, pc, Some ? short_jump〉 623 617  Some x ⇒ let 〈ignore,j_addr〉 ≝ x in find_right_jump pc j_addr ] 624 618  Instruction i ⇒ jep_relative pc new_labels i … … 636 630 let 〈npc, norig_pc, nlabels, npolicy〉 ≝ res in 637 631 〈nlabels, npolicy〉. 638 [ cases res in p res; #res >p1 >p2 normalize nodelta #Ha #Hb normalize in Hb; 632 //. 633 (* [ cases res in p res; #res >p1 >p2 normalize nodelta #Ha #Hb normalize in Hb; 639 634 >Hb in Ha; normalize nodelta #H @H 640 635  generalize in match (sig2 … acc) >p1 >p2 >p3 #H … … 715 710 @H 716 711  generalize in match (sig2 … old_policy) #H @H 717 ] 718 qed. 719 712 ] *) 713 qed. 714 715 (* lemma short_jumps_ok: 716 ∀program.∀l:BitVectorTrie (Word×Identifier) 16.∀p:jump_expansion_policy. 717 forall (Word×Word×jump_length) 16 (\snd (jump_expansion_policy_internal program l p)) 718 (λk.λx.let 〈pc,addr,j〉 ≝ x in 719 j = short_jump → 720 distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 addr) < 127). 721 #program #l #p @lookup_forall 722 #x #b cases x x #x cases x #pc #addr #j #Hl normalize nodelta 723 cases j in Hl; #Hl #Hj 724 [2,3: destruct (Hj) 725 Hj; cases (jump_expansion_policy_internal program l p) in Hl; 726 #res cases res res #r #res normalize nodelta #Hf #Hl 727 normalize in Hl; lapply (forall_lookup ? 16 res ? Hf ? ? Hl) 728 normalize #H @H 729 ] 730 qed. *) 731 732 (* lemma medium_jumps_ok: 733 ∀program.∀l:BitVectorTrie (Word×Identifier) 16.∀p:jump_expansion_policy. 734 forall (Word×Word×jump_length) 16 (\snd (jump_expansion_policy_internal program l p)) 735 (λk.λx.let 〈pc,addr,j〉 ≝ x in 736 j = medium_jump → 737 distance (nat_of_bitvector 16 pc) (nat_of_bitvector 16 addr) < 127). 738 #program #l #p @lookup_forall 739 #x #b cases x x #x cases x #pc #addr #j #Hl normalize nodelta 740 cases j in Hl; #Hl #Hj 741 [2,3: destruct (Hj) 742 Hj; cases (jump_expansion_policy_internal program l p) in Hl; 743 #res cases res res #r #res normalize nodelta #Hf #Hl 744 normalize in Hl; lapply (forall_lookup ? 16 res ? Hf ? ? Hl) 745 normalize #H @H 746 ] 747 qed. *) 748 720 749 definition expand_relative_jump_internal: 721 750 (Identifier → Word) → jump_length → Identifier → Word → ([[relative]] → preinstruction [[relative]]) → … … 848 877 let rec jump_expansion_internal (n: nat) (program: pseudo_assembly_program) 849 878 (old_labels: BitVectorTrie (Word × Identifier) 16) 850 (old_policy: Σbla:BitVectorTrie (Word × Word × jump_length) 16.policy_safe bla) 879 (old_policy: Σbla:BitVectorTrie (Word × Word × jump_length) 16. 880 forall ? ? bla policy_safe) 851 881 on n: BitVectorTrie jump_length 16 ≝ 852 882 match n with … … 855 885 old_policy (Stub ? ?) 856 886  S n' ⇒ 857 (* let 〈x,y〉 ≝ jump_expansion_policy_internal program old_labels old_policy in *) 858 jump_expansion_internal n' program (* x y *) 887 jump_expansion_internal n' program 859 888 (\fst (jump_expansion_policy_internal program old_labels old_policy)) 860 889 (\snd (jump_expansion_policy_internal program old_labels old_policy)) … … 864 893 #a cases a #xx #pp normalize nodelta 865 894 #H #H2 normalize nodelta @H2 866 qed. 867 895 qed. 896 897 898 899 868 900 (**************************************** START OF POLICY ABSTRACTION ********************) 869 901
Note: See TracChangeset
for help on using the changeset viewer.