prepare for conditions in cmove

4 files changed, 34 insertions, 19 deletions

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index f75f0bd3..698d64d6 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1642,7 +1642,7 @@ Opaque Int.eq.
   + eapply exec_straight_one.
     simpl; reflexivity.
   + split.
-    * unfold select.
+    * unfold eval_select.
       destruct (rs x1) eqn:eqX1; try constructor.
       destruct (rs x) eqn:eqX; try constructor.
       destruct (rs x0) eqn:eqX0; try constructor.
@@ -1656,7 +1656,7 @@ Opaque Int.eq.
   + eapply exec_straight_one.
     simpl; reflexivity.
   + split.
-    * unfold selectl.
+    * unfold eval_selectl.
       destruct (rs x1) eqn:eqX1; try constructor.
       destruct (rs x) eqn:eqX; try constructor.
       destruct (rs x0) eqn:eqX0; try constructor.
@@ -1670,7 +1670,7 @@ Opaque Int.eq.
   + eapply exec_straight_one.
     simpl; reflexivity.
   + split.
-    * unfold selectl.
+    * unfold eval_selectf.
       destruct (rs x1) eqn:eqX1; try constructor.
       destruct (rs x) eqn:eqX; try constructor.
       destruct (rs x0) eqn:eqX0; try constructor.
@@ -1684,7 +1684,7 @@ Opaque Int.eq.
   + eapply exec_straight_one.
     simpl; reflexivity.
   + split.
-    * unfold selectl.
+    * unfold eval_selectfs.
       destruct (rs x1) eqn:eqX1; try constructor.
       destruct (rs x) eqn:eqX; try constructor.
       destruct (rs x0) eqn:eqX0; try constructor.
diff --git a/mppa_k1c/NeedOp.v b/mppa_k1c/NeedOp.v
index f3ce8361..ee3c4e27 100644
--- a/mppa_k1c/NeedOp.v
+++ b/mppa_k1c/NeedOp.v
@@ -192,7 +192,7 @@ Lemma select_sound:
     vagree v0 w0 (default x) ->
     vagree v1 w1 (default x) ->
     vagree v2 w2 (default x) ->
-    vagree (select v0 v1 v2) (select w0 w1 w2) x.
+    vagree (eval_select v0 v1 v2) (eval_select w0 w1 w2) x.
 Proof.
   unfold default; intros.
   destruct x; trivial.
@@ -213,7 +213,7 @@ Lemma selectl_sound:
     vagree v0 w0 (default x) ->
     vagree v1 w1 (default x) ->
     vagree v2 w2 (default x) ->
-    vagree (selectl v0 v1 v2) (selectl w0 w1 w2) x.
+    vagree (eval_selectl v0 v1 v2) (eval_selectl w0 w1 w2) x.
 Proof.
   unfold default; intros.
   destruct x; trivial.
@@ -232,7 +232,7 @@ Lemma selectf_sound:
     vagree v0 w0 (default x) ->
     vagree v1 w1 (default x) ->
     vagree v2 w2 (default x) ->
-    vagree (selectf v0 v1 v2) (selectf w0 w1 w2) x.
+    vagree (eval_selectf v0 v1 v2) (eval_selectf w0 w1 w2) x.
 Proof.
   unfold default; intros.
   destruct x; trivial.
@@ -251,7 +251,7 @@ Lemma selectfs_sound:
     vagree v0 w0 (default x) ->
     vagree v1 w1 (default x) ->
     vagree v2 w2 (default x) ->
-    vagree (selectfs v0 v1 v2) (selectfs w0 w1 w2) x.
+    vagree (eval_selectfs v0 v1 v2) (eval_selectfs w0 w1 w2) x.
 Proof.
   unfold default; intros.
   destruct x; trivial.
diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v
index 5afd0cb9..551d2dfb 100644
--- a/mppa_k1c/Op.v
+++ b/mppa_k1c/Op.v
@@ -51,6 +51,12 @@ Inductive condition : Type :=
   | Ccompfs (c: comparison)     (**r 32-bit floating-point comparison *)
   | Cnotcompfs (c: comparison). (**r negation of a floating-point comparison *)
 
+Inductive condition0 : Type :=
+  | Ccomp0 (c: comparison) (**r signed integer comparison with 0 *)
+  | Ccompu0 (c: comparison) (**r unsigned integer comparison with 0 *)
+  | Ccompl0 (c: comparison) (**r signed 64-bit integer comparison with 0 *)
+  | Ccomplu0 (c: comparison). (**r unsigned 64-bit integer comparison with 0 *)
+
 (** Arithmetic and logical operations.  In the descriptions, [rd] is the
   result of the operation and [r1], [r2], etc, are the arguments. *)
 
@@ -237,7 +243,7 @@ Global Opaque eq_condition eq_addressing eq_operation.
   to lists of values.  Return [None] when the computation can trigger an
   error, e.g. integer division by zero.  [eval_condition] returns a boolean,
   [eval_operation] and [eval_addressing] return a value. *)
-
+ 
 Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool :=
   match cond, vl with
   | Ccomp c, v1 :: v2 :: nil => Val.cmp_bool c v1 v2
@@ -254,8 +260,17 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool
   | Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2)
   | _, _ => None
   end.
+ 
+Definition eval_condition0 (cond: condition0) (vl: list val) (m: mem): option bool :=
+  match cond, vl with
+  | Ccomp0 c, v1 :: nil => Val.cmp_bool c v1 (Vint Int.zero)
+  | Ccompu0 c, v1 :: nil => Val.cmpu_bool (Mem.valid_pointer m) c v1 (Vint Int.zero)
+  | Ccompl0 c, v1 :: nil => Val.cmpl_bool c v1 (Vlong Int64.zero)
+  | Ccomplu0 c, v1 :: nil => Val.cmplu_bool (Mem.valid_pointer m) c v1 (Vlong Int64.zero)
+  | _, _ => None
+  end.
 
-Definition select (v0 : val) (v1 : val) (vselect : val) : val :=
+Definition eval_select (v0 : val) (v1 : val) (vselect : val) : val :=
   match vselect with
   | Vint iselect =>
     match v0 with
@@ -272,7 +287,7 @@ Definition select (v0 : val) (v1 : val) (vselect : val) : val :=
   | _ => Vundef
   end.
 
-Definition selectl (v0 : val) (v1 : val) (vselect : val) : val :=
+Definition eval_selectl (v0 : val) (v1 : val) (vselect : val) : val :=
   match vselect with
   | Vint iselect =>
     match v0 with
@@ -289,7 +304,7 @@ Definition selectl (v0 : val) (v1 : val) (vselect : val) : val :=
   | _ => Vundef
   end.
 
-Definition selectf (v0 : val) (v1 : val) (vselect : val) : val :=
+Definition eval_selectf (v0 : val) (v1 : val) (vselect : val) : val :=
   match vselect with
   | Vint iselect =>
     match v0 with
@@ -306,7 +321,7 @@ Definition selectf (v0 : val) (v1 : val) (vselect : val) : val :=
   | _ => Vundef
   end.
 
-Definition selectfs (v0 : val) (v1 : val) (vselect : val) : val :=
+Definition eval_selectfs (v0 : val) (v1 : val) (vselect : val) : val :=
   match vselect with
   | Vint iselect =>
     match v0 with
@@ -451,10 +466,10 @@ Definition eval_operation
   | Osingleoflong, v1::nil => Val.singleoflong v1
   | Osingleoflongu, v1::nil => Val.singleoflongu v1
   | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
-  | Oselect, v0::v1::vselect::nil => Some (select v0 v1 vselect)
-  | Oselectl, v0::v1::vselect::nil => Some (selectl v0 v1 vselect)
-  | Oselectf, v0::v1::vselect::nil => Some (selectf v0 v1 vselect)
-  | Oselectfs, v0::v1::vselect::nil => Some (selectfs v0 v1 vselect)
+  | Oselect, v0::v1::vselect::nil => Some (eval_select v0 v1 vselect)
+  | Oselectl, v0::v1::vselect::nil => Some (eval_selectl v0 v1 vselect)
+  | Oselectf, v0::v1::vselect::nil => Some (eval_selectf v0 v1 vselect)
+  | Oselectfs, v0::v1::vselect::nil => Some (eval_selectfs v0 v1 vselect)
   | _, _ => None
   end.
 
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index 5a19510a..20ba74a1 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -568,7 +568,7 @@ Proof.
     predSpec Int.eq Int.eq_spec zero1 Int.zero; simpl; try exact DEFAULT.
     TrivialExists.
     simpl in *.
-    unfold select.
+    unfold eval_select.
     f_equal.
     inv H6.
     inv H7.
@@ -606,7 +606,7 @@ Proof.
     predSpec Int.eq Int.eq_spec zero1 Int.zero; simpl; try exact DEFAULT.
     TrivialExists.
     simpl in *.
-    unfold select.
+    unfold eval_select.
     f_equal.
     inv H6.
     inv H7.