 Timestamp:
 Nov 22, 2011, 11:58:43 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r1493 r1528 5 5 include "ASM/Status.ma". 6 6 include alias "basics/logic.ma". 7 include alias "arithmetics/nat.ma". 7 8 8 9 definition assembly_preinstruction ≝ … … 545 546 qed. 546 547 547 (* label_ trie: identifier ↦ 〈instruction number, address〉 *)548 definition label_ trie ≝ BitVectorTrie (nat × nat) 16.548 (* label_map: identifier ↦ 〈instruction number, address〉 *) 549 definition label_map ≝ identifier_map ASMTag (nat × nat). 549 550 550 551 definition add_instruction_size: ℕ → jump_length → pseudo_instruction → ℕ ≝ … … 572 573 [ #i >nth_nil #H @⊥ @H 573 574  #h #t #IH #i cases i i 574 [ cases h #hi #hp cases hi normalize 575 [ #H @⊥ @H 576  #l' #Heq change in match (eq_v ??? l' l) with (eq_bv ? l' l) 577 >(eq_eq_bv … Heq) // 575 [ cases h #hi #hp cases hi 576 [ normalize #H @⊥ @H 577  #l' #Heq whd in ⊢ (??%?); change with (eq_identifier ? l' l) in match (instruction_matches_identifier ??); 578 whd in Heq; >Heq 579 >eq_identifier_refl // 578 580 ] 579  #i #H whd in match (does_not_occur ??) 580 whd in match (instruction_matches_identifier ??) 581 cases h #hi #hp cases hi normalize 581  #i #H whd in match (does_not_occur ??); 582 whd in match (instruction_matches_identifier ??); 583 cases h #hi #hp cases hi normalize nodelta 582 584 [ @(IH i) @H 583  #l' cases (eq_v ??? l' l)585  #l' @eq_identifier_elim 584 586 [ normalize // 585  normalize @(IH i) @H587  normalize #_ @(IH i) @H 586 588 ] 587 589 ] … … 603 605 coercion coerc_pair_sigma:∀A,B,P. ∀p:A × B. P (\snd p) → A × (Σx:B.P x) 604 606 ≝ coerc_pair_sigma on p: (? × ?) to (? × (Sig ??)). 605 606 let rec create_label_ trie(program: list labelled_instruction)607 608 let rec create_label_map (program: list labelled_instruction) 607 609 (policy: jump_expansion_policy): 608 (Σlabels:label_ trie.609 ∀i:ℕ. i < program→610 (Σlabels:label_map. 611 ∀i:ℕ.lt i (program) (* XXX using < causes (false?) ambiguity *) → 610 612 ∀l.occurs_exactly_once l program → 611 613 is_label (nth i ? program 〈None ?, Comment [ ]〉) l → 612 ∃a.lookup _opt … l labels= Some ? 〈i,a〉614 ∃a.lookup … labels l = Some ? 〈i,a〉 613 615 ) ≝ 614 616 let 〈final_pc, final_labels〉 ≝ … … 618 620 ∀l.occurs_exactly_once l prefix → 619 621 is_label (nth i ? prefix 〈None ?, Comment [ ]〉) l → 620 ∃a.lookup _opt … l labels= Some ? 〈i,a〉)622 ∃a.lookup … labels l = Some ? 〈i,a〉) 621 623 ) 622 624 program … … 627 629 match label with 628 630 [ None ⇒ labels 629  Some l ⇒ insert … l 〈prefix, pc〉 labels631  Some l ⇒ add … labels l 〈prefix, pc〉 630 632 ] in 631 let jmp_len ≝ \snd ( lookup …(bitvector_of_nat 16 (prefix)) policy 〈pc, long_jump〉) in633 let jmp_len ≝ \snd (bvt_lookup ?? (bitvector_of_nat 16 (prefix)) policy 〈pc, long_jump〉) in 632 634 〈add_instruction_size pc jmp_len instr, new_labels〉 633 ) 〈0, Stub ? ?〉 in635 ) 〈0, empty_map …〉 in 634 636 final_labels. 635 [ #i >append_length <commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi;637 [ #i >append_length >commutative_plus #Hi normalize in Hi; cases (le_to_or_lt_eq … Hi) Hi; 636 638 [ #Hi #l normalize nodelta; cases label normalize nodelta 637 639 [ >occurs_exactly_once_None #Hocc >(nth_append_first ? ? prefix ? ? (le_S_S_to_le ? ? Hi)) #Hl 638 640 lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc Hl) #addr #Haddr 639 641 % [ @addr  @Haddr ] 640  #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) Hocc; #Hocc641 lapply (refl ? (eq_bv 16 l' l)) cases (eq_bv ? l' l) in ⊢ (???% → %) #Heq642 [ >Heq in Hocc; #Hoccnormalize in Hocc;642  #l' #Hocc #Hl lapply (occurs_exactly_once_Some_stronger … Hocc) Hocc; 643 @eq_identifier_elim #Heq #Hocc 644 [ normalize in Hocc; 643 645 >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; #Hl 644 646 @⊥ @(absurd … Hocc) 645  >Heq in Hocc; normalize nodelta #Hocclapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?)646 [ #addr #Haddr % [ @addr  <Haddr @lookup_ opt_insert_miss >eq_bv_sym >Heq // ]647  normalize nodelta lapply (sig2 … labels) #Hacc elim (Hacc i (le_S_S_to_le … Hi) l Hocc ?) 648 [ #addr #Haddr % [ @addr  <Haddr @lookup_add_miss /2/ ] 647 649  >(nth_append_first ? ? prefix ? ? (le_S_S_to_le … Hi)) in Hl; // 648 650 ] … … 653 655 [ <minus_n_n #Hl normalize in Hl; normalize nodelta cases label in Hl; 654 656 [ normalize nodelta #H @⊥ @H 655  #l' normalize nodelta #Heq % [ @pc  <Heq normalize nodelta @lookup_ opt_insert_hit ]657  #l' normalize nodelta #Heq % [ @pc  <Heq normalize nodelta @lookup_add_hit ] 656 658 ] 657 659  @le_n … … 662 664 qed. 663 665 664 definition select_reljump_length: label_ trie→ ℕ → Identifier → jump_length ≝666 definition select_reljump_length: label_map → ℕ → Identifier → jump_length ≝ 665 667 λlabels.λpc.λlbl. 666 let 〈n, addr〉 ≝ lookup … lbl labels〈0, pc〉 in668 let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in 667 669 if leb pc addr (* forward jump *) 668 670 then if leb (addr  pc) 126 … … 673 675 else long_jump. 674 676 675 definition select_call_length: label_ trie→ ℕ → Identifier → jump_length ≝677 definition select_call_length: label_map → ℕ → Identifier → jump_length ≝ 676 678 λlabels.λpc_nat.λlbl. 677 679 let pc ≝ bitvector_of_nat 16 pc_nat in 678 let addr ≝ bitvector_of_nat 16 (\snd (lookup ? ? lbl labels〈0, pc_nat〉)) in680 let addr ≝ bitvector_of_nat 16 (\snd (lookup_def ? ? labels lbl 〈0, pc_nat〉)) in 679 681 let 〈fst_5_addr, rest_addr〉 ≝ split ? 5 11 addr in 680 682 let 〈fst_5_pc, rest_pc〉 ≝ split ? 5 11 pc in … … 683 685 else long_jump. 684 686 685 definition select_jump_length: label_ trie→ ℕ → Identifier → jump_length ≝687 definition select_jump_length: label_map → ℕ → Identifier → jump_length ≝ 686 688 λlabels.λpc.λlbl. 687 let 〈n, addr〉 ≝ lookup … lbl labels〈0, pc〉 in689 let 〈n, addr〉 ≝ lookup_def … labels lbl 〈0, pc〉 in 688 690 if leb pc addr 689 691 then if leb (addr  pc) 126 … … 694 696 else select_call_length labels pc lbl. 695 697 696 definition jump_expansion_step_instruction: label_ trie→ ℕ →698 definition jump_expansion_step_instruction: label_map → ℕ → 697 699 preinstruction Identifier → option jump_length ≝ 698 700 λlabels.λpc.λi. … … 830 832 (old_policy: Σpolicy.jump_in_policy program policy): 831 833 (Σpolicy. 832 jump_in_policy program policy ∧834 And (jump_in_policy program policy) (* XXX ∧ causes ambiguity *) 833 835 (jump_in_policy program policy → 834 (∀i. i < program→ is_jump (nth i ? program 〈None ?, Comment []〉) →836 (∀i.lt i (program) (* XXX < causes ambiguity *) → is_jump (nth i ? program 〈None ?, Comment []〉) → 835 837 jmpleq 836 838 (\snd (lookup … (bitvector_of_nat 16 i) old_policy 〈0,short_jump〉)) … … 838 840 ) 839 841 ) ≝ 840 let labels ≝ create_label_ trieprogram old_policy in842 let labels ≝ create_label_map program old_policy in 841 843 let 〈final_pc, final_policy〉 ≝ 842 844 foldl_strong (option Identifier × pseudo_instruction) … … 902 904 % [1,3,5,7: @pc 903 905 2,4,6,8: lapply (refl ? (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉)) 904 cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) in ⊢ (???% → %) 906 cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) in ⊢ (???% → %); 905 907 #x #y #Hl normalize nodelta 906 % [1,3,5,7: @(max_length y (select_reljump_length (create_label_ trieprogram old_policy) pc j))908 % [1,3,5,7: @(max_length y (select_reljump_length (create_label_map program old_policy) pc j)) 907 909 2,4,6,8: @lookup_opt_insert_hit 908 910 ] ] … … 910 912 % [1,3,5,7,9: @pc 911 913 2,4,6,8,10: lapply (refl ? (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉)) 912 cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) in ⊢ (???% → %) 914 cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) in ⊢ (???% → %); 913 915 #x #y #Hl normalize nodelta 914 % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_ trieprogram old_policy) pc j))916 % [1,3,5,7,9: @(max_length y (select_reljump_length (create_label_map program old_policy) pc j)) 915 917 2,4,6,8,10: @lookup_opt_insert_hit 916 918 ] ] … … 920 922 2,4: cases (lookup … (bitvector_of_nat ? (prefix)) old_policy 〈0,short_jump〉) 921 923 #x #y normalize nodelta 922 % [1: @(max_length y (select_jump_length (create_label_ trieprogram old_policy) pc j))923 3: @(max_length y (select_call_length (create_label_ trieprogram old_policy) pc j))924 % [1: @(max_length y (select_jump_length (create_label_map program old_policy) pc j)) 925 3: @(max_length y (select_call_length (create_label_map program old_policy) pc j)) 924 926 2,4: @lookup_opt_insert_hit 925 927 ] … … 940 942 [ @(proj2 ? ? Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 941 943  #z normalize nodelta 942 whd in match (snd ℕ jump_expansion_policy ?) >lookup_insert_miss944 whd in match (snd ℕ jump_expansion_policy ?); >lookup_insert_miss 943 945 [ @(proj2 … Hpolicy (proj1 ? ? Hpolicy) ? (le_S_S_to_le … Hi) Hj) 944 946  @bitvector_of_nat_abs @(lt_to_not_eq i (prefix)) @(le_S_S_to_le … Hi) … … 961 963 9,10,14,15: #j normalize nodelta #_ 962 964 cases (lookup ???? 〈0,short_jump〉) #x #y 963 whd in match (snd ℕ jump_expansion_policy ?) 965 whd in match (snd ℕ jump_expansion_policy ?); 964 966 >lookup_insert_hit normalize @jmpleq_max_length 965 967 11,12,13,16,17: #z #j normalize nodelta #_ 966 968 cases (lookup ???? 〈0,short_jump〉) #x #y 967 whd in match (snd ℕ jump_expansion_policy ?) 969 whd in match (snd ℕ jump_expansion_policy ?); 968 970 >lookup_insert_hit normalize @jmpleq_max_length 969 971 ] 970 972 4,5: #id #_ cases (lookup ???? 〈0,short_jump〉) #x #y 971 whd in match (snd ℕ jump_expansion_policy ?) 973 whd in match (snd ℕ jump_expansion_policy ?); 972 974 >lookup_insert_hit normalize @jmpleq_max_length 973 975 ] … … 1027 1029 λpseudo_program_counter: nat. 1028 1030 λprogram_counter: nat. 1029 λcosts: BitVectorTrie Word16.1031 λcosts: BitVectorTrie costlabel 16. 1030 1032 λi. 1031 1033 match i with … … 1148 1150 sigma00 program pol prefix (Some … 〈0, 〈0, Stub …〉〉) ≠ None …. 1149 1151 * #preamble #instr_list #pol #suffix #prefix #prf whd in prf:(???%); 1150 generalize in match (sig2 ?? pol) whd in prf:(???%)<prf in pol; #pol1151 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0 1152 generalize in match (sig2 ?? pol); whd in prf:(???%); <prf in pol; #pol 1153 whd in match policy_ok; whd in match sigma_safe; whd in match sigma0; 1152 1154 normalize nodelta >sigma00_append 1153 1155 cases (sigma00 ?? prefix ?) … … 1166 1168 * #preamble #instr_list #pol #suffix #hd #prefix #ppc_pc_map #EQ1 #EQ2 1167 1169 generalize in match (policy_ok_prefix_ok 〈preamble,instr_list〉 pol suffix 1168 (prefix@[hd]) EQ1) in ⊢ ? >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?)1170 (prefix@[hd]) EQ1) in ⊢ ?; >sigma00_append <EQ2 whd in ⊢ (?(??%?) → ?); 1169 1171 @pair_elim' #ppc #pc_map #EQ3 normalize nodelta 1170 1172 @pair_elim' #pc #map #EQ4 normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.