 Timestamp:
 Feb 22, 2013, 10:39:26 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2653 r2713 121 121  RET ⇒ inr … (RET ?) 122 122  RETI ⇒ inr … (RETI ?) 123  NOP ⇒ inr … (RealInstruction (NOP ?)) 123  NOP ⇒ inr … (NOP ?) 124  JMP dst ⇒ inr … (RealInstruction (JMP ? dst)) 124 125 ]. 125 126 … … 147 148 [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))] 148 149  Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr 150  Jnz acc dst1 dst2 ⇒ 151 [ RealInstruction (JNZ … (RELATIVE (bitvector_of_nat ? 3))); 152 LJMP (ADDR16 (zero ?)); 153 LJMP (ADDR16 (zero ?)) ] 154  MovSuccessor dst ws lbl ⇒ 155 let v ≝ DATA (zero …) in 156 match dst return λx. bool_to_Prop (is_in ? [[acc_a;direct;registr]] x) → ? with 157 [ ACC_A ⇒ λ_. 158 [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈 159 ACC_A, v〉))))))] 160  DIRECT b1 ⇒ λ_. 161 [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT b1, v〉)))))] 162  REGISTER r ⇒ λ_. 163 [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈 164 REGISTER r, v〉))))))] 165  _ ⇒ λK. match K in False with [ ] ] (subaddressing_modein … dst) 149 166  Jmp jmp ⇒ 150 167 match jmp_len with … … 587 604 @(subaddressing_mode_elim … a1) #w 588 605 #EQ normalize in EQ; destruct(EQ) 589 2,3,6: #x [3: #y] #H cases H 590 4,5: #id #_ cases a cases b #H try % normalize in H; destruct(H) 606 2,3,8: #x [3: #y] #H cases H 607 4,7: #id #_ cases a cases b #H try % normalize in H; destruct(H) 608 5,6: #x #y #z #H normalize in H; cases H 591 609 ] 592 610 qed. … … 595 613 instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i. 596 614 #a #b #i cases i 597 [2,3, 6: #x [3: #y] #H cases H598 4, 5: #id #_ cases a cases b @leb_true_to_le / by refl/615 [2,3,8: #x [3: #y] #H cases H 616 4,7: #id #_ cases a cases b @leb_true_to_le / by refl/ 599 617 1: #pi cases pi 600 618 try (#x #y #H) try (#x #H) try (#H) cases H … … 603 621 cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try % 604 622 @(subaddressing_mode_elim … a1) #w % 623 5,6: #x #y #z #H cases H 605 624 ] 606 625 qed. … … 640 659 try (#x #id #Hnth_eq #Hsafe) try (#id #Hnth_eq #Hsafe) try (#Hnth_eq #Hsafe) 641 660 try % lapply Hsafe Hsafe lapply Hnth_eq Hnth_eq lapply id id 642 2,3,6: #x [3: #y] normalize nodelta #Hnth_eq #_ %] 661 2,3,5,8: #x [3: #y #z  4: #y] normalize nodelta #_ #_ % 662 6: #x #y #z normalize nodelta #_ #_ @pair_elim #w1 #w2 #_ 663 @(subaddressing_mode_elim … x) try #k % ] 643 664 #id lapply (Hpc_equal i (le_S_to_le … Hi)) 644 665 lapply (Hpc_equal (S i) Hi) … … 751 772 ¬is_jump i → ∀j1,j2.instruction_size_jmplen j1 i = instruction_size_jmplen j2 i. 752 773 #i cases i 753 [2,3,6: #x [3: #y] #Hj #j1 #j2 % 754 4,5: #x #Hi cases Hi 774 [2,3,8: #x [3: #y] #Hj #j1 #j2 % 775 5,6: #x #y #z #_ #j1 #j2 % 776 4,7: #x #Hi cases Hi 755 777 1: #pi cases pi try (#x #y #Hj #j1 #j2) try (#y #Hj #j1 #j2) try (#Hj #j1 #j2) 756 778 try % cases Hj ]
Note: See TracChangeset
for help on using the changeset viewer.