match some 'and'

4 files changed, 50 insertions, 14 deletions

diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 26ae55f6..9bf35581 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -258,7 +258,13 @@ Nondetfunction andl (e1: expr) (e2: expr) :=
   | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2
   | t1, Eop (Olongconst n2) Enil => andlimm n2 t1
   | (Eop Onotl (t1:::Enil)), t2 => Eop Oandnl (t1:::t2:::Enil) 
-  | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil) 
+  | t1, (Eop Onotl (t2:::Enil)) => Eop Oandnl (t2:::t1:::Enil)
+  | (Eop Ocast32signed
+         ((Eop Oneg ((Eop (Ocmp (Ccomplimm Cne zero1))
+        (y1:::Enil)):::Enil)):::Enil)), v1 =>
+     	if Int64.eq zero1 Int64.zero                 
+	then Eop Oselectl ((Eop (Olongconst Int64.zero) Enil):::v1:::y1:::Enil)
+	else Eop Oandl (e1:::e2:::Enil)
   | _, _ => Eop Oandl (e1:::e2:::Enil)
   end.
 
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 09a7cfff..49abc7c7 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -390,6 +390,15 @@ Proof.
 - TrivialExists.
 Qed.
 
+Lemma int64_eq_commut: forall x y : int64,
+    (Int64.eq x y) = (Int64.eq y x).
+Proof.
+  intros.
+  predSpec Int64.eq Int64.eq_spec x y;
+    predSpec Int64.eq Int64.eq_spec y x;
+    congruence.
+Qed.
+
 Theorem eval_andl: binary_constructor_sound andl Val.andl.
 Proof.
   unfold andl; destruct Archi.splitlong. apply SplitLongproof.eval_andl.
@@ -398,6 +407,24 @@ Proof.
 - InvEval. apply eval_andlimm; auto.
 - (*andn*) InvEval. TrivialExists. simpl. congruence.
 - (*andn reverse*) InvEval. rewrite Val.andl_commut. TrivialExists; simpl. congruence.
+- (* selectl *)
+  InvEval.
+  predSpec Int64.eq Int64.eq_spec zero1 Int64.zero; simpl; TrivialExists.
+  + constructor. econstructor; constructor.
+  constructor; try constructor; try constructor; try eassumption.
+  + simpl in *. f_equal. inv H6.
+    unfold selectl.
+    simpl.
+    destruct v3; simpl; trivial.
+    rewrite int64_eq_commut.
+    destruct (Int64.eq i Int64.zero); simpl.
+    * replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
+      destruct y; simpl; trivial.
+    * replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
+      destruct y; simpl; trivial.
+      rewrite Int64.and_commut. rewrite Int64.and_mone. reflexivity.
+  + constructor. econstructor. constructor. econstructor. constructor. econstructor. constructor. eassumption. constructor. simpl. f_equal. constructor. simpl. f_equal. constructor. simpl. f_equal. constructor. eassumption. constructor.
+  + simpl in *. congruence.
 - TrivialExists.
 Qed.
 
@@ -415,15 +442,6 @@ Proof.
 Qed.
 
 
-Lemma int64_eq_commut: forall x y : int64,
-    (Int64.eq x y) = (Int64.eq y x).
-Proof.
-  intros.
-  predSpec Int64.eq Int64.eq_spec x y;
-    predSpec Int64.eq Int64.eq_spec y x;
-    congruence.
-Qed.
-
 Theorem eval_orl: binary_constructor_sound orl Val.orl.
 Proof.
   unfold orl; destruct Archi.splitlong. apply SplitLongproof.eval_orl.
diff --git a/test/monniaux/bitsliced-aes/bs.c b/test/monniaux/bitsliced-aes/bs.c
index 949d2a8a..5fd7450a 100644
--- a/test/monniaux/bitsliced-aes/bs.c
+++ b/test/monniaux/bitsliced-aes/bs.c
@@ -16,13 +16,12 @@ static inline word_t compcert_ternary(word_t x, word_t v0, word_t v1) {
 /* with bitmask
 #define TERNARY0(cmp,v1) (-(cmp != 0) & (v1))
 */
-/* with function call to ternary */
+/* with function call to ternary 
 #define TERNARY0(cmp,v1) compcert_ternary(cmp, 0, v1)
-
-/*
-#define TERNARY0(x, v1) ((unsigned long) (((-(((long) (x))==0)) & (0)) | ((-(((long) (x))!=0)) & (v1))))
 */
 
+#define TERNARY0(x, v1) ((unsigned long) ((long) (-(((long) (x))!=0)) & (v1)))
+
 #if (defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__) ||\
         defined(__amd64__) || defined(__amd32__)|| defined(__amd16__)
 #define bs2le(x) (x)
diff --git a/test/monniaux/bitsliced-aes/notes.txt b/test/monniaux/bitsliced-aes/notes.txt
index e9be8b42..815d5931 100644
--- a/test/monniaux/bitsliced-aes/notes.txt
+++ b/test/monniaux/bitsliced-aes/notes.txt
@@ -36,3 +36,16 @@ cycles: 2916854
 
 ==> test.gcc.k1c.out <==
 cycles: 5646730
+
+* cmove via match du and
+==> test.ccomp.host.out <==
+cycles: 2553732
+
+==> test.ccomp.k1c.out <==
+cycles: 7208629
+
+==> test.gcc.host.out <==
+cycles: 1849125
+
+==> test.gcc.k1c.out <==
+cycles: 5255763