shortcuts for cmove

3 files changed, 41 insertions, 21 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 72d7394b..04ce13e7 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -342,8 +342,8 @@ Definition btest_for_cmpuwz (c: comparison) :=
   | Ceq => OK BTweqz
   | Clt => Error (msg "btest_for_compuwz: Clt")
   | Cge => Error (msg "btest_for_compuwz: Cge")
-  | Cle => Error (msg "btest_for_compuwz: Cle")
-  | Cgt => Error (msg "btest_for_compuwz: Cgt")
+  | Cle => OK BTweqz
+  | Cgt => OK BTwnez
   end.
 
 (* CoMPare Unsigned Words to Zero *)
@@ -353,8 +353,8 @@ Definition btest_for_cmpudz (c: comparison) :=
   | Ceq => OK BTdeqz
   | Clt => Error (msg "btest_for_compudz: Clt")
   | Cge => Error (msg "btest_for_compudz: Cge")
-  | Cle => Error (msg "btest_for_compudz: Cle")
-  | Cgt => Error (msg "btest_for_compudz: Cgt")
+  | Cle => OK BTdeqz
+  | Cgt => OK BTdnez
   end.
 
 Definition conditional_move (cond0 : condition0) (rc rd rs : ireg) :
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 86e640c9..1ed584e8 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -1668,6 +1668,30 @@ Proof.
   destruct a; reflexivity.
 Qed.
 
+Lemma int_ltu_to_neq:
+  forall x,
+    Int.ltu Int.zero x = negb (Int.eq x Int.zero).
+Proof.
+  intros.
+  unfold Int.ltu, Int.eq.
+  change (Int.unsigned Int.zero) with 0.
+  pose proof (Int.unsigned_range x) as RANGE.
+  unfold zlt, zeq.
+  destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; omega.
+Qed.
+
+Lemma int64_ltu_to_neq:
+  forall x,
+    Int64.ltu Int64.zero x = negb (Int64.eq x Int64.zero).
+Proof.
+  intros.
+  unfold Int64.ltu, Int64.eq.
+  change (Int64.unsigned Int64.zero) with 0.
+  pose proof (Int64.unsigned_range x) as RANGE.
+  unfold zlt, zeq.
+  destruct (Z_lt_dec _ _); destruct (Z.eq_dec _ _); trivial; omega.
+Qed.
+
 Lemma transl_op_correct:
   forall op args res k (rs: regset) m v c,
   transl_op op args res k = OK c ->
@@ -1754,28 +1778,24 @@ Opaque Int.eq.
   }
 
   destruct c0; simpl in *.
-  1, 2, 3:
-    destruct c; simpl in *; inv EQ2;
-    econstructor; split; try (apply exec_straight_one; constructor);
-    split; try (simpl; intros; rewrite Pregmap.gso; trivial; assumption);
-    unfold Val.select; simpl;
-    rewrite Pregmap.gss;
-    destruct (rs x1); simpl; trivial;
-    rewrite if_neg;
-    apply Val.lessdef_normalize.
-  
+
+  all:
     destruct c; simpl in *; inv EQ2;
     econstructor; split; try (apply exec_straight_one; constructor);
     split; try (simpl; intros; rewrite Pregmap.gso; trivial; assumption);
     unfold Val.select; simpl;
     rewrite Pregmap.gss;
     destruct (rs x1); simpl; trivial;
-    rewrite if_neg;
-    try apply Val.lessdef_normalize;
-    
-    destruct Archi.ptr64; simpl; replace (Int64.eq Int64.zero Int64.zero) with true by reflexivity; simpl; trivial;
-    destruct (_ || _); trivial;
-    apply Val.lessdef_normalize.
+    try rewrite int_ltu_to_neq;
+    try rewrite int64_ltu_to_neq;
+    try change (Int64.eq Int64.zero Int64.zero) with true;
+    try destruct Archi.ptr64;
+    repeat rewrite if_neg;
+    simpl;
+    trivial;
+    try destruct (_ || _);
+    trivial;
+    try apply Val.lessdef_normalize.
 Qed.
 
 (** Memory accesses *)
diff --git a/test/monniaux/picosat-965/Makefile b/test/monniaux/picosat-965/Makefile
index e13087de..991278ff 100644
--- a/test/monniaux/picosat-965/Makefile
+++ b/test/monniaux/picosat-965/Makefile
@@ -7,7 +7,7 @@ ALL_CFLAGS = -DNALARM -DNZIP -DNGETRUSAGE -DNDEBUG
 K1C_CFLAGS += $(EMBEDDED_CFLAGS)
 K1C_CCOMPFLAGS += $(EMBEDDED_CFLAGS)
 CCOMPFLAGS += -fbitfields
-K1C_CCOMPFLAGS += -fbitfields -fno-if-conversion
+K1C_CCOMPFLAGS += -fbitfields # -fno-if-conversion
 
 K1C_CFLAGS += $(ALL_CFLAGS)
 K1C_CCOMPFLAGS += $(ALL_CFLAGS)