Changeset 2225 for src/ASM/PolicyFront.ma
 Timestamp:
 Jul 20, 2012, 6:15:40 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2222 r2225 22 22 λx:preinstruction Identifier. 23 23 match x with 24 [ JC _ ⇒ True25  JNC _ ⇒ True26  JZ _ ⇒ True27  JNZ _ ⇒ True28  JB _ _ ⇒ True29  JNB _ _ ⇒ True30  JBC _ _ ⇒ True31  CJNE _ _ ⇒ True32  DJNZ _ _ ⇒ True33  _ ⇒ False24 [ JC _ ⇒ true 25  JNC _ ⇒ true 26  JZ _ ⇒ true 27  JNZ _ ⇒ true 28  JB _ _ ⇒ true 29  JNB _ _ ⇒ true 30  JBC _ _ ⇒ true 31  CJNE _ _ ⇒ true 32  DJNZ _ _ ⇒ true 33  _ ⇒ false 34 34 ]. 35 35 … … 38 38 match instr with 39 39 [ Instruction i ⇒ is_jump' i 40  _ ⇒ False40  _ ⇒ false 41 41 ]. 42 42 … … 45 45 match instr with 46 46 [ Instruction i ⇒ is_jump' i 47  Call _ ⇒ True48  Jmp _ ⇒ True49  _ ⇒ False47  Call _ ⇒ true 48  Jmp _ ⇒ true 49  _ ⇒ false 50 50 ]. 51 51 … … 53 53 λinstr:pseudo_instruction. 54 54 match instr with 55 [ Call _ ⇒ True56  _ ⇒ False55 [ Call _ ⇒ true 56  _ ⇒ false 57 57 ]. 58 58 … … 258 258 match j with 259 259 [ short_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = true ∧ 260 ¬is_call instr260 bool_to_Prop (¬is_call instr) 261 261  absolute_jump ⇒ \fst (absolute_jump_cond pc_plus_jmp_length addr) = true ∧ 262 262 \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ 263 ¬is_relative_jump instr263 bool_to_Prop (¬is_relative_jump instr) 264 264  long_jump ⇒ \fst (short_jump_cond pc_plus_jmp_length addr) = false ∧ 265 265 \fst (absolute_jump_cond pc_plus_jmp_length addr) = false … … 360 360 then short_jump 361 361 else select_call_length labels old_sigma inc_sigma added ppc lbl. 362 362 363 definition destination_of: preinstruction Identifier → option Identifier ≝ 364 λi. 365 match i with 366 [ JC j ⇒ Some ? j 367  JNC j ⇒ Some ? j 368  JZ j ⇒ Some ? j 369  JNZ j ⇒ Some ? j 370  JB _ j ⇒ Some ? j 371  JBC _ j ⇒ Some ? j 372  JNB _ j ⇒ Some ? j 373  CJNE _ j ⇒ Some ? j 374  DJNZ _ j ⇒ Some ? j 375  _ ⇒ None ? 376 ]. 377 363 378 definition jump_expansion_step_instruction: label_map → ppc_pc_map → ppc_pc_map → 364 379 ℕ → ℕ → preinstruction Identifier → option jump_length ≝ 365 380 λlabels.λold_sigma.λinc_sigma.λadded.λppc.λi. 366 match i with 367 [ JC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 368  JNC j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 369  JZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 370  JNZ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 371  JB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 372  JBC _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 373  JNB _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 374  CJNE _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 375  DJNZ _ j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 376  _ ⇒ None ? 377 ]. 378 379 lemma dec_is_jump: ∀x.Sum (is_jump x) (¬is_jump x). 380 #i cases i 381 [#id cases id 382 [1,2,3,6,7,33,34: 383 #x #y %2 whd in match (is_jump ?); /2 by nmk/ 384 4,5,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32: 385 #x %2 whd in match (is_jump ?); /2 by nmk/ 386 35,36,37: %2 whd in match (is_jump ?); /2 by nmk/ 387 9,10,14,15: #x %1 / by I/ 388 11,12,13,16,17: #x #y %1 / by I/ 389 ] 390 2,3: #x %2 /2 by nmk/ 391 4,5: #x %1 / by I/ 392 6: #x #y %2 /2 by nmk/ 393 ] 394 qed. 381 match destination_of i with 382 [ Some j ⇒ Some ? (select_reljump_length labels old_sigma inc_sigma added ppc j) 383  None ⇒ None ? 384 ]. 395 385 396 386 (* The first step of the jump expansion: everything to short. *) … … 599 589 #a #b #i cases i 600 590 [1: #pi cases pi 601 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 602 try (#x #y #H #_) try (#x #H #_) try (#H #_) cases H 603 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] #_ try (#_ %) 604 try (#abs normalize in abs; destruct (abs) @I) 605 cases a; cases b; try (#_ %) try (#abs normalize in abs; destruct(abs) @I) 606 try (@(subaddressing_mode_elim … x) #w #abs normalize in abs; destruct (abs) @I) 607 cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w 608 try ( #abs normalize in abs; destruct (abs) @I) 609 @(subaddressing_mode_elim … a1) #w2 #abs normalize in abs; destruct (abs) 610 ] 591 try (#x #y #H #EQ) try (#x #H #EQ) try (#H #EQ) cases H 592 cases a in EQ; cases b #EQ try % 593 try (normalize in EQ; destruct(EQ) @False) 594 try (lapply EQ @(subaddressing_mode_elim … x) #w #EQ normalize in EQ; destruct(EQ) @False) 595 lapply EQ EQ cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w 596 try (#EQ normalize in EQ; destruct(EQ) @False) 597 @(subaddressing_mode_elim … a1) #w 598 #EQ normalize in EQ; destruct(EQ) 611 599 2,3,6: #x [3: #y] #H cases H 612 4,5: #id #_ cases a cases b 613 [2,3,4,6,11,12,13,15: normalize #H destruct (H) 614 1,5,7,8,9,10,14,16,17,18: #H / by refl/ 615 ] 616 ] 600 4,5: #id #_ cases a cases b #H try % normalize in H; destruct(H) 601 ] 617 602 qed. 618 603 … … 623 608 4,5: #id #_ cases a cases b / by le_n/ 624 609 1: #pi cases pi 625 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 626 try (#x #y #H) try (#x #H) try (#H) cases H 627 9,10,11,12,13,14,15,16,17: #x [3,4,5,8,9: #y] 628 #_ cases a cases b 629 [1,4,5,6,7,8,9: / by le_n/ 630 10,13,14,15,16,17,18: / by le_n/ 631 19,22,23,24,25,26,27: / by le_n/ 632 28,31,32,33,34,35,36: / by le_n/ 633 37,40,41,42,43,44,45: / by le_n/ 634 46,47,48,49,50,51,52,53,54: / by le_n/ 635 55,56,57,58,59,60,61,62,63: / by le_n/ 636 64,65,66,67,68,69,70,71,72: / by le_n/ 637 73,74,75,76,77,78,79,80,81: / by le_n/ 638 ] 639 try (@(subaddressing_mode_elim … x) #w normalize @le_S @le_S @le_S @le_S @le_S @le_n) 640 cases x * #ad 641 try (@(subaddressing_mode_elim … ad) #w #z normalize @le_S @le_S @le_S @le_S @le_S @le_n) 642 #z @(subaddressing_mode_elim … z) #w normalize / by / 643 ] 610 try (#x #y #H) try (#x #H) try (#H) cases H 611 H cases a cases b @leb_true_to_le try % 612 try (@(subaddressing_mode_elim … x) #w % @False) 613 cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try % 614 @(subaddressing_mode_elim … a1) #w % 644 615 ] 645 616 qed. … … 701 672 cases (vsplit bool 9 7 result) #upper #lower normalize nodelta 702 673 cases (get_index' bool 2 0 flags) normalize nodelta 703 [3,4: #H @⊥ @(absurd ?? (proj2 ?? H)) / by I/674 [3,4: #H cases (proj2 ?? H) 704 675 1,2: cases (eq_bv 9 upper ?) 705 676 [2,4: #H lapply (proj1 ?? H) #H3 destruct (H3) … … 761 732 ] 762 733 ] 763 1: #pi cases pi 764 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 765 [1,2,3,6,7,24,25: #x #y 766 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 767 normalize nodelta #H #Heq @refl 768 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x 3,4,5,8,9: #y #x] 769 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) 770 #Hj #Heq lapply (Hj x (refl ? x)) Hj 734 1: cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) 735 [#A #B * / by refl/] #fst_foo 736 cut (∀x. 737 instruction_has_label x (\snd (nth i labelled_instruction program 〈None (identifier ASMTag),Comment []〉)) → 738 lookup_def ?? (create_label_map program) x 0 ≤ (program)) 739 [#x #Heq cases (create_label_map program) #clm #Hclm 740 @le_S_to_le @(proj2 ?? (Hclm x ?)) 741 @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??) 742 [ >nat_of_bitvector_bitvector_of_nat_inverse 743 [2: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 744  whd in match fetch_pseudo_instruction; normalize nodelta 745 >nth_safe_nth 746 [ >nat_of_bitvector_bitvector_of_nat_inverse 747 [ @pair_elim // ] 748 @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi ] 749  assumption ]] #lookup_in_program 750 H #pi cases pi 751 try (#y #x #H #Heq) try (#x #H #Heq) try (#H #Heq) try % 752 normalize nodelta >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in H; 753 #Hj lapply (Hj x (refl ? x)) Hj 771 754 whd in match expand_relative_jump; normalize nodelta 772 755 whd in match expand_relative_jump_internal; normalize nodelta … … 776 759 <(plus_n_Sm i 0) <plus_n_O <plus_n_O cases x2 normalize nodelta 777 760 [1,4,7,10,13,16,19,22,25: 778 cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) 779 [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ] 780 #fst_foo >fst_foo @pair_elim #sj_possible #disp #H #H2 761 >fst_foo @pair_elim #sj_possible #disp #H #H2 781 762 @(pair_replace ?????????? (eq_to_jmeq … H)) 782 [1,3,5,7,9,11,13,15,17: 783 cut (lookup_def ?? (create_label_map program) x 0 ≤ (program)) 784 [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm 785 @le_S_to_le @(proj2 ?? (Hclm x ?)) 786 @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??) 787 [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse 788 [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 789 2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta 790 >nth_safe_nth 791 [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse 792 [1,3,5,7,9,11,13,15,17: >Heq %] 793 @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 794 ] 795 ] 796 >Heq / by / 797 ] 798 #X >(le_to_leb_true … X) @refl 799 ] 763 [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …)) 764 try % >Heq % ] 800 765 >(proj1 ?? H2) try (@refl) normalize nodelta 801 766 [1,2,3,5: @(subaddressing_mode_elim … y) #w % … … 803 768 @(subaddressing_mode_elim … sth2) #x [3,4: #x2] % 804 769 ] 805 2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs #abs2 @⊥ @abs2 / by I/770 2,5,8,11,14,17,20,23,26: ** #_ #_ #abs cases abs 806 771 ] 807 cut (∀A,B,ab.fst A B ab = (let 〈a,b〉 ≝ ab in a)) 808 [1,3,5,7,9,11,13,15,17: #A #B * / by refl/ ] 809 #fst_foo * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H 772 * #H #_ >fst_foo in H; @pair_elim #sj_possible #disp #H 810 773 @(pair_replace ?????????? (eq_to_jmeq … H)) 811 [1,3,5,7,9,11,13,15,17: 812 cut (lookup_def ?? (create_label_map program) x 0 ≤ (program)) 813 [1,3,5,7,9,11,13,15,17: cases (create_label_map program) #clm #Hclm 814 @le_S_to_le @(proj2 ?? (Hclm x ?)) 815 @(proj2 ?? Hprogram x (bitvector_of_nat ? i) ? (\snd (nth i ? program 〈None ?, Comment []〉)) ??) 816 [1,4,7,10,13,16,19,22,25: >nat_of_bitvector_bitvector_of_nat_inverse 817 [2,4,6,8,10,12,14,16,18: @(transitive_lt … (proj1 ?? Hprogram)) @le_S] @Hi 818 2,5,8,11,14,17,20,23,26: whd in match fetch_pseudo_instruction; normalize nodelta 819 >nth_safe_nth 820 [1,3,5,7,9,11,13,15,17: >nat_of_bitvector_bitvector_of_nat_inverse 821 [1,3,5,7,9,11,13,15,17: >Heq %] 822 @(transitive_lt … (proj1 ?? Hprogram)) @le_S @Hi 823 ] 824 ] 825 >Heq / by / 826 ] 827 #X >(le_to_leb_true … X) @refl 828 ] 774 [1,3,5,7,9,11,13,15,17: >(le_to_leb_true … (lookup_in_program …)) 775 try % >Heq % ] 829 776 #H2 >H2 try (@refl) normalize nodelta 830 777 [1,2,3,5: @(subaddressing_mode_elim … y) #w % … … 832 779 [1,2: %] whd in match (map ????); whd in match (flatten ??); 833 780 whd in match (map ????) in ⊢ (???%); whd in match (flatten ??) in ⊢ (???%); 834 >length_append >length_append @eq_f2 % 835 ] 836 ] 837 ] 838 ] 839 ] 840 ] 781 >length_append >length_append %]]]]] 841 782 qed. 842 783 … … 845 786 #i cases i 846 787 [2,3,6: #x [3: #y] #Hj #j1 #j2 % 847 4,5: #x #Hi cases Hi #abs @⊥ @abs @I 848 1: #pi cases pi 849 [1,2,3,4,5,6,7,8,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37: 850 [1,2,3,6,7,24,25: #x #y 851 4,5,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23: #x] 852 #Hj #j1 #j2 % 853 9,10,11,12,13,14,15,16,17: [1,2,6,7: #x 3,4,5,8,9: #y #x] 854 #Hi cases Hi #abs @⊥ @abs @I 855 ] 856 ] 857 qed. 788 4,5: #x #Hi cases Hi 789 1: #pi cases pi try (#x #y #Hj #j1 #j2) try (#y #Hj #j1 #j2) try (#Hj #j1 #j2) 790 try % cases Hj ] 791 qed.
Note: See TracChangeset
for help on using the changeset viewer.