Changeset 2713 for src/ASM/PolicyFront.ma

Timestamp:

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

Author:

sacerdot

Message:

PolicyFront?.ma repaired

File:

• src/ASM/PolicyFront.ma (modified) (7 diffs)

src/ASM/PolicyFront.ma

@@ -121 +121 @@
   | RET ⇒ inr … (RET ?)
   | RETI ⇒ inr … (RETI ?)
-  | NOP ⇒ inr … (RealInstruction (NOP ?))
+  | NOP ⇒ inr … (NOP ?)
+  | JMP dst ⇒ inr … (RealInstruction (JMP ? dst))
   ].
 
@@ -147 +148 @@
      [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inr ? ? 〈DPTR, DATA16 (zero 16)〉))))]
   | Instruction instr ⇒ expand_relative_jump_unsafe jmp_len instr
+  | Jnz acc dst1 dst2 ⇒
+      [ RealInstruction (JNZ … (RELATIVE (bitvector_of_nat ? 3)));
+        LJMP (ADDR16 (zero ?));
+        LJMP (ADDR16 (zero ?)) ]
+  | MovSuccessor dst ws lbl ⇒
+     let v ≝ DATA (zero …) in
+     match dst return λx. bool_to_Prop (is_in ? [[acc_a;direct;registr]] x) → ? with
+     [ ACC_A ⇒ λ_.
+        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈
+ACC_A, v〉))))))]
+     | DIRECT b1 ⇒ λ_.
+        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT b1, v〉)))))]
+     | REGISTER r ⇒ λ_.
+        [ RealInstruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈
+REGISTER r, v〉))))))]
+     | _ ⇒ λK. match K in False with [ ] ] (subaddressing_modein … dst)
   | Jmp jmp ⇒
     match jmp_len with
@@ -587 +604 @@
    @(subaddressing_mode_elim … a1) #w
    #EQ normalize in EQ; destruct(EQ)
-  |2,3,6: #x [3: #y] #H cases H
-  |4,5: #id #_ cases a cases b #H try % normalize in H; destruct(H)
+  |2,3,8: #x [3: #y] #H cases H
+  |4,7: #id #_ cases a cases b #H try % normalize in H; destruct(H)
+  |5,6: #x #y #z #H normalize in H; cases H
  ]
 qed.
@@ -595 +613 @@
   instruction_size_jmplen a i ≤ instruction_size_jmplen (max_length a b) i.
  #a #b #i cases i
- [2,3,6: #x [3: #y] #H cases H
- |4,5: #id #_ cases a cases b @leb_true_to_le / by refl/
+ [2,3,8: #x [3: #y] #H cases H
+ |4,7: #id #_ cases a cases b @leb_true_to_le / by refl/
  |1: #pi cases pi
     try (#x #y #H) try (#x #H) try (#H) cases H
@@ -603 +621 @@
     cases x * #a1 #a2 @(subaddressing_mode_elim … a2) #w try %
     @(subaddressing_mode_elim … a1) #w %
+ |5,6: #x #y #z #H cases H
  ]
 qed.
@@ -640 +659 @@
               try (#x #id #Hnth_eq #Hsafe) try (#id #Hnth_eq #Hsafe) try (#Hnth_eq #Hsafe)
               try % lapply Hsafe -Hsafe lapply Hnth_eq -Hnth_eq lapply id -id
-          |2,3,6: #x [3: #y] normalize nodelta #Hnth_eq #_ %]
+          |2,3,5,8: #x [3: #y #z | 4: #y] normalize nodelta #_ #_ %
+          |6: #x #y #z normalize nodelta #_ #_ @pair_elim #w1 #w2 #_
+              @(subaddressing_mode_elim … x) try #k % ]
             #id lapply (Hpc_equal i (le_S_to_le … Hi))
             lapply (Hpc_equal (S i) Hi)
@@ -751 +772 @@
   ¬is_jump i → ∀j1,j2.instruction_size_jmplen j1 i = instruction_size_jmplen j2 i.
  #i cases i 
- [2,3,6: #x [3: #y] #Hj #j1 #j2 %
- |4,5: #x #Hi cases Hi
+ [2,3,8: #x [3: #y] #Hj #j1 #j2 %
+ |5,6: #x #y #z #_ #j1 #j2 %
+ |4,7: #x #Hi cases Hi
  |1: #pi cases pi try (#x #y #Hj #j1 #j2) try (#y #Hj #j1 #j2) try (#Hj #j1 #j2)
      try % cases Hj ]