Changeset 2713 for src/ASM/PolicyFront.ma
- 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.