IT COMPILES

7 files changed, 48 insertions, 45 deletions

diff --git a/common/Values.v b/common/Values.v
index ae8d31f3..837ed799 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -768,14 +768,14 @@ Definition rolml (v: val) (amount: int) (mask: int64): val :=
 
 
 Definition extfz stop start v :=
-  if (Int.cmp Cle start stop)
-       && (Int.cmp Cge start Int.zero)
-       && (Int.cmp Clt stop Int.iwordsize)
+  if (Z.leb start stop)
+       && (Z.geb start Z.zero)
+       && (Z.ltb stop Int.zwordsize)
   then
-    let stop' := Int.add stop Int.one in
+    let stop' := Z.add stop Z.one in
     match v with
     | Vint w =>
-      Vint (Int.shr (Int.shl w (Int.sub Int.iwordsize stop')) (Int.sub Int.iwordsize (Int.sub stop' start)))
+      Vint (Int.shr (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
     | _ => Vundef
     end
   else Vundef.
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 2c3eef1f..290691f4 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -130,7 +130,7 @@ Inductive instruction : Type :=
   | Psxwd   (rd rs: ireg)                           (**r Sign Extend Word to Double Word *)

   | Pzxwd   (rd rs: ireg)                           (**r Zero Extend Word to Double Word *)

 

-  | Pextfz  (rd : ireg) (rs : ireg) (stop : int) (start : int) (**r extract bitfields unsigned *)

+  | Pextfz  (rd : ireg) (rs : ireg) (stop : Z) (start : Z) (**r extract bitfields unsigned *)

   | Pfabsd  (rd rs: ireg)                           (**r float absolute double *)

   | Pfabsw  (rd rs: ireg)                           (**r float absolute word *)

   | Pfnegd  (rd rs: ireg)                           (**r float negate double *)

diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index a347b6fc..b39ebd0e 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -307,7 +307,7 @@ Inductive arith_name_rr : Type :=
   | Psxwd                                           (**r Sign Extend Word to Double Word *)
   | Pzxwd                                           (**r Zero Extend Word to Double Word *)
 (*  | Pextfs (stop : int) (start : int)               (**r extract bit field, signed *) *)
-  | Pextfz (stop : int) (start : int)               (**r extract bit field, unsigned *)
+  | Pextfz (stop : Z) (start : Z)               (**r extract bit field, unsigned *)
            
   | Pfabsd                                          (**r float absolute double *)
   | Pfabsw                                          (**r float absolute word *)
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 8180c43f..8293af1e 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -198,7 +198,7 @@ Inductive operation : Type :=
   | Oselectl (cond: condition0)   (**r [rd = if cond r3 then r2 else r1] *)
   | Oselectf (cond: condition0)   (**r [rd = if cond r3 then r2 else r1] *)
   | Oselectfs (cond: condition0) (**r [rd = if cond r3 then r2 else r1] *)
-  | Oextfz (stop : int) (start : int).
+  | Oextfz (stop : Z) (start : Z).
 
 (** Addressing modes.  [r1], [r2], etc, are the arguments to the
   addressing. *)
@@ -233,7 +233,7 @@ Defined.
 
 Definition eq_operation: forall (x y: operation), {x=y} + {x<>y}.
 Proof.
-  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0; intros.
+  generalize Int.eq_dec Int64.eq_dec Ptrofs.eq_dec Float.eq_dec Float32.eq_dec ident_eq eq_condition eq_condition0 Z.eq_dec; intros.
   decide equality.
 Defined.
 
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index 8f953425..3e36a51c 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -203,11 +203,11 @@ Nondetfunction shrimm (e1: expr) (n: int) :=
         then Eop (Oshrimm (Int.add n n1)) (t1:::Enil)
         else Eop (Oshrimm n) (e1:::Enil)
     | Eop (Oshlimm n1) (t1:::Enil) =>
-        let stop := Int.sub Int.iwordsize (Int.add n1 Int.one) in
-	let start := Int.sub (Int.add (Int.add n stop) Int.one) Int.iwordsize in
-	if (Int.cmp Cle start stop)
-         && (Int.cmp Cge start Int.zero)
-         && (Int.cmp Clt stop Int.iwordsize)
+        let stop := Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one) in
+	let start := Z.sub (Z.add (Z.add (Int.unsigned n) stop) Z.one) Int.zwordsize in
+	if (Z.leb start stop)
+         && (Z.geb start Z.zero)
+         && (Z.ltb stop Int.zwordsize)
         then Eop (Oextfz stop start) (t1:::Enil)
 	else Eop (Oshrimm n) (e1:::Enil)
     | _ =>
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 954ffba2..d072bb7b 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -321,7 +321,7 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero.
   intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto.
 
-  destruct (Int.ltu n Int.iwordsize) eqn:LT; simpl.
+  destruct (Int.ltu n Int.iwordsize) eqn:LT.
   destruct (shrimm_match a); intros; InvEval.
   - exists (Vint (Int.shr n1 n)); split. EvalOp.
     simpl. rewrite LT; auto.
@@ -335,34 +335,37 @@ Proof.
     subst. TrivialExists. econstructor. EvalOp. simpl; eauto. constructor.
     simpl. auto.
   - subst x.
+    simpl negb.
+    cbn iota.
     destruct (_ && _ && _) eqn:BOUNDS.
-    + exists (Val.extfz (Int.sub Int.iwordsize (Int.add n1 Int.one))
-            (Int.sub
-               (Int.add
-                  (Int.add n (Int.sub Int.iwordsize (Int.add n1 Int.one)))
-                  Int.one) Int.iwordsize) v1).
+    + exists (Val.extfz (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one))
+            (Z.sub
+               (Z.add
+                  (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
+                  Z.one) Int.zwordsize) v1).
       split.
       ++ EvalOp.
       ++ unfold Val.extfz.
-      * simpl. rewrite BOUNDS.
-        destruct v1; simpl; trivial.
-        destruct (Int.ltu n1 Int.iwordsize) eqn:Hltu_n1; simpl; trivial.
-        destruct (Int.ltu n Int.iwordsize) eqn:Hltu_n; simpl; trivial.
-        replace (Int.sub Int.iwordsize
-                         (Int.add (Int.sub Int.iwordsize (Int.add n1 Int.one)) Int.one)) with n1.
-        replace (Int.sub Int.iwordsize
-             (Int.sub
-                (Int.add (Int.sub Int.iwordsize (Int.add n1 Int.one)) Int.one)
-                (Int.sub
-                   (Int.add
-                      (Int.add n (Int.sub Int.iwordsize (Int.add n1 Int.one)))
-                      Int.one) Int.iwordsize))) with n.
-        constructor.
-        ** repeat (try rewrite Int.add_signed; try rewrite Int.sub_signed; try rewrite Int.signed_repr).
-           rewrite <- (Int.repr_signed n) at 1.
-           f_equal.
-           omega.
-           
+         rewrite BOUNDS.
+         destruct v1; try (simpl; apply Val.lessdef_undef).
+        replace (Z.sub Int.zwordsize
+                         (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)) with (Int.unsigned n1).
+        replace (Z.sub Int.zwordsize
+             (Z.sub
+                (Z.add (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)) Z.one)
+                (Z.sub
+                   (Z.add
+                      (Z.add (Int.unsigned n) (Z.sub Int.zwordsize (Z.add (Int.unsigned n1) Z.one)))
+                      Z.one) Int.zwordsize))) with (Int.unsigned n).
+        * rewrite Int.repr_unsigned.
+          rewrite Int.repr_unsigned.
+          simpl.
+          destruct (Int.ltu n1 Int.iwordsize) eqn:Hltu_n1; simpl; trivial.
+          simpl.
+          destruct (Int.ltu n Int.iwordsize) eqn:Hltu_n; simpl; trivial.
+        * omega.
+        * omega.
+    + TrivialExists. constructor. econstructor. constructor. eassumption. constructor. simpl. reflexivity. constructor. simpl. reflexivity.
   - TrivialExists.
   - intros; TrivialExists. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor.
     auto.
diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v
index 64002cef..e498d237 100644
--- a/mppa_k1c/ValueAOp.v
+++ b/mppa_k1c/ValueAOp.v
@@ -75,15 +75,15 @@ Definition eval_static_selectfs (cond : condition0) (v0 v1 vselect : aval) : ava
   end.
   
 
-Definition eval_static_extfz (stop : int) (start : int) (v : aval) :=
-  if (Int.cmp Cle start stop)
-       && (Int.cmp Cge start Int.zero)
-       && (Int.cmp Clt stop Int.iwordsize)
+Definition eval_static_extfz (stop : Z) (start : Z) (v : aval) :=
+  if (Z.leb start stop)
+       && (Z.geb start Z.zero)
+       && (Z.ltb stop Int.zwordsize)
   then
-    let stop' := Int.add stop Int.one in
+    let stop' := Z.add stop Z.one in
     match v with
     | I w =>
-      I (Int.shr (Int.shl w (Int.sub Int.iwordsize stop')) (Int.sub Int.iwordsize (Int.sub stop' start)))
+      I (Int.shr (Int.shl w (Int.repr (Z.sub Int.zwordsize stop'))) (Int.repr (Z.sub Int.zwordsize (Z.sub stop' start))))
     | _ => Vtop
     end
   else Vtop.