Changeset 1393 for src/ASM/Assembly.ma
- Timestamp:
- Oct 17, 2011, 3:50:50 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Assembly.ma
r1363 r1393 414 414 415 415 (* jump_expansion_policy: instruction number ↦ 〈pc, jump_length〉 *) 416 definition jump_expansion_policy ≝ BitVectorTrie ( Word× jump_length) 16.416 definition jump_expansion_policy ≝ BitVectorTrie (ℕ × jump_length) 16. 417 417 418 418 definition expand_relative_jump_internal: … … 545 545 546 546 (* label_trie: identifier ↦ 〈instruction number, address〉 *) 547 definition label_trie ≝ BitVectorTrie (nat × Word) 16.548 549 definition add_instruction_size: Word → jump_length → pseudo_instruction → Word≝547 definition label_trie ≝ BitVectorTrie (nat × nat) 16. 548 549 definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝ 550 550 λpc.λjmp_len.λinstr. 551 let ilist ≝ expand_pseudo_instruction_safe (λx.pc) (λx.pc) pc jmp_len instr in 551 let bv_pc ≝ bitvector_of_nat 16 pc in 552 let ilist ≝ expand_pseudo_instruction_safe (λx.bv_pc) (λx.bv_pc) bv_pc jmp_len instr in 552 553 let bv: list (BitVector 8) ≝ match ilist with 553 554 [ None ⇒ (* hmm, this shouldn't happen *) [ ] 554 555 | Some l ⇒ flatten … (map … assembly1 l) 555 556 ] in 556 let 〈new_pc, carry〉 ≝ add_16_with_carry pc (bitvector_of_nat 16 (|bv|)) false in 557 new_pc. 558 557 pc + (|bv|). 558 559 559 definition is_label ≝ 560 560 λx:labelled_instruction.λl:Identifier. … … 631 631 ] 632 632 qed. 633 634 lemma coerc_pair_sigma: 635 ∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x). 636 #A #B #P * #a #b #p % [@a | /2/] 637 qed. 638 coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x) 639 ≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)). 633 640 634 definition create_label_trie: list labelled_instruction → jump_expansion_policy → 635 label_trie ≝ 636 λprogram.λpolicy. 641 let rec create_label_trie (program: list labelled_instruction) 642 (policy: jump_expansion_policy): 643 (Σlabels:label_trie. 644 ∀i:ℕ.i < |program| → 645 ∀l.occurs_exactly_once l program → 646 is_label (nth i ? program 〈None ?, Comment [ ]〉) l → 647 ∃a.lookup_opt … l labels = Some ? 〈i,a〉 648 ) ≝ 637 649 let 〈final_pc, final_labels〉 ≝ 638 650 foldl_strong (option Identifier × pseudo_instruction) 639 (λprefix.Σres. 640 let 〈pc,labels〉 ≝ res in 651 (λprefix.ℕ × (Σlabels. 641 652 ∀i:ℕ.i < |prefix| → 642 ∀l.occurs_exactly_once l prefix ->653 ∀l.occurs_exactly_once l prefix → 643 654 is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l → 644 ∃a.lookup_opt … l labels = Some ? 〈i,a〉 655 ∃a.lookup_opt … l labels = Some ? 〈i,a〉) 645 656 ) 646 657 program … … 648 659 let 〈pc,labels〉 ≝ acc in 649 660 let 〈label,instr〉 ≝ x in 650 let new_labels ≝ 651 match label with 652 [ None ⇒ labels 653 | Some l ⇒ insert … l 〈|prefix|, pc〉 labels 654 ] in 655 let 〈ignore,jmp_len〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉 in 656 let new_pc ≝ add_instruction_size pc jmp_len instr in 657 〈new_pc, new_labels〉 658 ) 〈zero ?, Stub ? ?〉 in 661 let new_labels ≝ 662 match label with 663 [ None ⇒ labels 664 | Some l ⇒ insert … l 〈|prefix|, pc〉 labels 665 ] in 666 let jmp_len ≝ \snd (lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, long_jump〉) in 667 〈add_instruction_size pc jmp_len instr, new_labels〉 668 ) 〈0, Stub ? ?〉 in 659 669 final_labels. 660 [ lapply (sig2 … acc) >p >p1 normalize nodelta #Hacc #i >append_length 661 <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi; 662 [ #Hi #l cases label 670 [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi; 671 [ #Hi #l normalize nodelta; cases label normalize nodelta 663 672 [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl 664 lapply ( Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #Ha elim Ha; -Ha; #addr #Haddr673 lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 665 674 % [ @addr | @Haddr ] 666 675 | #l' #Hocc #Hl lapply (oeo_Some_Stronger … Hocc) -Hocc; #Hocc … … 669 678 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 670 679 @⊥ @(absurd … Hocc) 671 | >Heq in Hocc; normalize nodelta #Hocc lapply (Hacc i (le_S_S_to_le … Hi) l ? ?) 672 [ >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; // 673 | @Hocc 674 | #H elim H #addr #Haddr % [ @addr | <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ] 680 | >Heq in Hocc; normalize nodelta #Hocc lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?) 681 [ #addr #Haddr % [ @addr | <Haddr @lookup_opt_insert_miss >eq_bv_sym >Heq // ] 682 | >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; // 675 683 ] 676 684 ] … … 678 686 ] 679 687 | #Hi #l #Hocc >(injective_S … Hi) >nth_append_second 680 [ <minus_n_n #Hl normalize in Hl; cases label in Hl;688 [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl; 681 689 [ normalize nodelta #H @⊥ @H 682 | #l' normalize nodelta #Heq % [ @pc | <Heq @lookup_opt_insert_hit ]690 | #l' normalize nodelta #Heq % [ @pc | <Heq normalize nodelta @lookup_opt_insert_hit ] 683 691 ] 684 692 | @le_n … … 689 697 qed. 690 698 691 definition select_reljump_length: label_trie → Word→ Identifier → jump_length ≝699 definition select_reljump_length: label_trie → ℕ → Identifier → jump_length ≝ 692 700 λlabels.λpc.λlbl. 693 701 let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in 694 if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT pending lookup of right condition *) 695 then short_jump 696 else long_jump. 697 698 definition select_call_length: label_trie → Word → Identifier → jump_length ≝ 699 λlabels.λpc.λlbl. 700 let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in 702 if leb pc addr (* forward jump *) 703 then if leb (addr - pc) 126 704 then short_jump 705 else long_jump 706 else if leb (pc - addr) 129 707 then short_jump 708 else long_jump. 709 710 definition select_call_length: label_trie → ℕ → Identifier → jump_length ≝ 711 λlabels.λpc_nat.λlbl. 712 let pc ≝ bitvector_of_nat 16 pc_nat in 713 let addr ≝ bitvector_of_nat 16 (\snd (lookup ? ? lbl labels 〈0, pc_nat〉)) in 701 714 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in 702 715 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in … … 705 718 else long_jump. 706 719 707 definition select_jump_length: label_trie → Word→ Identifier → jump_length ≝720 definition select_jump_length: label_trie → ℕ → Identifier → jump_length ≝ 708 721 λlabels.λpc.λlbl. 709 722 let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in 710 if (gt_s ? pc addr) (* REMOVE BEFORE FLIGHT *) 711 then short_jump 712 else 713 let 〈n, addr〉 ≝ lookup … lbl labels 〈0, pc〉 in 714 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in 715 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in 716 if eq_bv ? fst_5_addr fst_5_pc 717 then medium_jump 718 else long_jump. 723 if leb pc addr 724 then if leb (addr - pc) 126 725 then short_jump 726 else select_call_length labels pc lbl 727 else if leb (pc - addr) 129 728 then short_jump 729 else select_call_length labels pc lbl. 719 730 720 definition jump_expansion_step_instruction: label_trie → Word→731 definition jump_expansion_step_instruction: label_trie → ℕ → 721 732 preinstruction Identifier → option jump_length ≝ 722 733 λlabels.λpc.λi. … … 745 756 | short_jump ⇒ j2 746 757 ]. 747 748 definition jump_expansion_step: list labelled_instruction → 749 jump_expansion_policy → jump_expansion_policy ≝ 750 λprogram.λpolicy. 751 let labels ≝ create_label_trie program policy in 752 let 〈final_n, final_pc, final_policy〉 ≝ 758 759 definition jmpleq: jump_length → jump_length → Prop ≝ 760 λj1.λj2. 761 match j1 with 762 [ short_jump ⇒ True 763 | medium_jump ⇒ 764 match j2 with 765 [ short_jump ⇒ False 766 | _ ⇒ True 767 ] 768 | long_jump ⇒ 769 match j2 with 770 [ long_jump ⇒ True 771 | _ ⇒ False 772 ] 773 ]. 774 775 definition is_jump' ≝ 776 λx:preinstruction Identifier. 777 match x with 778 [ JC _ ⇒ True 779 | JNC _ ⇒ True 780 | JZ _ ⇒ True 781 | JNZ _ ⇒ True 782 | JB _ _ ⇒ True 783 | JNB _ _ ⇒ True 784 | JBC _ _ ⇒ True 785 | CJNE _ _ ⇒ True 786 | DJNZ _ _ ⇒ True 787 | _ ⇒ False 788 ]. 789 790 definition is_jump ≝ 791 λx:labelled_instruction. 792 let 〈label,instr〉 ≝ x in 793 match instr with 794 [ Instruction i ⇒ is_jump' i 795 | Call _ ⇒ True 796 | Jmp _ ⇒ True 797 | _ ⇒ False 798 ]. 799 800 axiom bitvector_of_nat_ok: 801 ∀x,y,n.bitvector_of_nat (S n) x = bitvector_of_nat (S n) y → x = y. 802 803 let rec jump_expansion_step (program: list labelled_instruction) 804 (old_policy: jump_expansion_policy): 805 (Σpolicy.∀i:ℕ.i < |program| → 806 is_jump (nth i ? program 〈None ?, Comment [ ]〉) → 807 ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉 808 ) ≝ 809 let labels ≝ create_label_trie program old_policy in 810 let 〈final_pc, final_policy〉 ≝ 753 811 foldl_strong (option Identifier × pseudo_instruction) 754 (λprefix.Σres.True) 812 (λprefix.ℕ × Σpolicy.∀i:ℕ.i < |prefix| → 813 is_jump (nth i ? prefix 〈None ?, Comment [ ]〉) → 814 ∃p,j.lookup_opt … (bitvector_of_nat 16 i) policy = Some ? 〈p,j〉 815 ) 755 816 program 756 817 (λprefix.λx.λtl.λprf.λacc. 757 let 〈 n,pc, policy〉 ≝ acc in818 let 〈pc, policy〉 ≝ acc in 758 819 let 〈label,instr〉 ≝ x in 759 let old_jump_length ≝ lookup_opt … (bitvector_of_nat 16 n) policy in820 let old_jump_length ≝ lookup_opt ? ? (bitvector_of_nat 16 (|prefix|)) policy in 760 821 let add_instr ≝ 761 822 match instr with … … 766 827 ] in 767 828 let 〈new_pc, new_policy〉 ≝ 768 let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 n) policy 〈pc, short_jump〉 in829 let 〈ignore,old_length〉 ≝ lookup … (bitvector_of_nat 16 (|prefix|)) policy 〈pc, short_jump〉 in 769 830 match add_instr with 770 831 [ None ⇒ (* i.e. it's not a jump *) … … 772 833 | Some ai ⇒ 773 834 let new_length ≝ max_length old_length ai in 774 〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 n) 〈pc, new_length〉 policy〉835 〈add_instruction_size pc new_length instr, insert … (bitvector_of_nat 16 (|prefix|)) 〈pc, new_length〉 policy〉 775 836 ] in 776 〈 S n,new_pc, new_policy〉777 ) 〈0, zero ?,Stub ? ?〉 in837 〈new_pc, new_policy〉 838 ) 〈0, Stub ? ?〉 in 778 839 final_policy. 779 @I 840 [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) -Hi; 841 [ #Hi; >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) #Hj 842 lapply (sig2 … policy) #Hacc elim (Hacc i (le_S_S_to_le … Hi) Hj) #henk #ingrid elim ingrid 843 -ingrid #ingrid #Hingrid 844 % [ @henk | % [ @ingrid | normalize nodelta cases instr normalize nodelta 845 [2,3: #x cases (lookup ??? policy ?) #y #z @Hingrid 846 |6: #x #y cases (lookup ??? policy ?) #w #z @Hingrid 847 |1: #pi cases (lookup ??? policy ?) #x #y cases (jump_expansion_step_instruction ???) 848 [ @Hingrid 849 | #z normalize nodelta <Hingrid @lookup_opt_insert_miss 850 @notb_elim >eq_bv_false [ // | @nmk #H @(absurd (i = (|prefix|))) 851 [ @(bitvector_of_nat_ok … H) 852 | @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi) 853 ] ] 854 ] 855 |4,5: #id cases (lookup ??? policy ?) #x #y normalize nodelta <Hingrid 856 @lookup_opt_insert_miss @notb_elim >eq_bv_false 857 [1,3: // 858 |2,4: @nmk #H @(absurd (i = (|prefix|))) 859 [1,3: @(bitvector_of_nat_ok … H) 860 |2,4: @(lt_to_not_eq i (|prefix|)) @(le_S_S_to_le … Hi) 861 ] ] 862 ] ] ] 863 | #Hi >nth_append_second >(injective_S … Hi) 864 [ <minus_n_n #Hj normalize in Hj; normalize nodelta cases instr in Hj; 865 [2,3: #x #Hj @⊥ @Hj 866 |6: #x #y #Hj @⊥ @Hj 867 |1: #pi cases pi 868 [35,36,37: #Hj @⊥ @Hj 869 |4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: #x #Hj @⊥ @Hj 870 |1,2,3,6,7,33,34: #x #y #Hj @⊥ @Hj 871 |9,10,14,15: #j normalize nodelta #_ 872 % [1,3,5,7: @pc 873 |2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉)) 874 cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %) 875 #x #y #Hl normalize nodelta 876 % [1,3,5,7: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j)) 877 |2,4,6,8: @lookup_opt_insert_hit 878 ] ] 879 |11,12,13,16,17: #x #j normalize nodelta #_ 880 % [1,3,5,7,9: @pc 881 |2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉)) 882 cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) in ⊢ (???% → %) 883 #x #y #Hl normalize nodelta 884 % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_trie program old_policy) pc j)) 885 |2,4,6,8,10: @lookup_opt_insert_hit 886 ] ] 887 ] 888 |4,5: #j normalize nodelta #_ 889 % [1,3: @pc 890 |2,4: cases (lookup … (bitvector_of_nat ? (|prefix|)) policy 〈pc,short_jump〉) 891 #x #y normalize nodelta 892 % [1: @(max_length y (select_jump_length (create_label_trie program old_policy) pc j)) 893 |3: @(max_length y (select_call_length (create_label_trie program old_policy) pc j)) 894 |2,4: @lookup_opt_insert_hit 895 ] 896 ] 897 ] 898 | @le_n 899 ] 900 ] 901 | #i #Hi @⊥ @(absurd (i<0)) [ @Hi | @(not_le_Sn_O) ] 902 ] 780 903 qed. 781 904 … … 791 914 λprogram.λpc. 792 915 let policy ≝ jump_expansion_internal (\snd program) in 793 let 〈n,j〉 ≝ lookup ? ? pc policy 〈 zero ?, long_jump〉 in916 let 〈n,j〉 ≝ lookup ? ? pc policy 〈0, long_jump〉 in 794 917 j. 795 918
Note: See TracChangeset
for help on using the changeset viewer.