detect insf case, begin

3 files changed, 16 insertions, 4 deletions

diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v
index 2faa6b0a..fe8ce203 100644
--- a/mppa_k1c/ExtValues.v
+++ b/mppa_k1c/ExtValues.v
@@ -83,12 +83,19 @@ Definition insfl stop start prev fld :=
             (Val.andl (Val.shll fld (Vint (Int.repr start))) mask)
   else Vundef.
 
-Fixpoint highest_bit (x : Z) (n : nat) : N :=
+Fixpoint highest_bit (x : Z) (n : nat) : Z :=
   match n with
-  | O => 0%N
+  | O => 0
   | S n1 =>
-    let n' := N_of_nat n in
-    if Z.testbit x (Z.of_N n')
+    let n' := Z.of_N (N_of_nat n) in
+    if Z.testbit x n'
     then n'
     else highest_bit x n1
   end.
+
+Definition int_highest_bit (x : int) : Z :=
+  highest_bit (Int.unsigned x) (31%nat).
+
+
+Definition int64_highest_bit (x : int64) : Z :=
+  highest_bit (Int64.unsigned x) (63%nat).
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index aad6249a..bdceced8 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -336,6 +336,10 @@ Nondetfunction or (e1: expr) (e2: expr) :=
      && Int.eq zero1 Int.zero                 
      then select_base v0 v1 y0
      else Eop Oor (e1:::e2:::Enil)
+  | (Eop (Oandimm nmask) (prev:::Enil)),
+    (Eop (Oandimm mask)
+      ((Eop (Oshlimm start) (fld:::Enil)):::Enil)) =>
+      Eop Oor (e1:::e2:::Enil)
   | _, _ => Eop Oor (e1:::e2:::Enil)
   end.
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index cc362eb7..dc8f16ab 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -701,6 +701,7 @@ Proof.
       rewrite Int.or_zero.
       reflexivity.
   - apply DEFAULT.
+  - apply DEFAULT.
 Qed.
 
 Theorem eval_xorimm: