improvements on cmoved etc.

3 files changed, 18 insertions, 97 deletions

diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp
index 9bf35581..6c34de19 100644
--- a/mppa_k1c/SelectLong.vp
+++ b/mppa_k1c/SelectLong.vp
@@ -259,14 +259,16 @@ Nondetfunction andl (e1: expr) (e2: expr) :=
   | 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)
+  | _, _ => Eop Oandl (e1:::e2:::Enil)
+  end.
+(*
   | (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.
+*)
 
 Nondetfunction orlimm (n1: int64) (e2: expr) :=
   if Int64.eq n1 Int64.zero then e2 else
@@ -295,22 +297,9 @@ Nondetfunction orl (e1: expr) (e2: expr) :=
      && Int64.eq zero1 Int64.zero                 
      then Eop Oselectl (v0:::v1:::y0:::Enil)
      else Eop Oorl (e1:::e2:::Enil)
-     
   | _, _ => Eop Oorl (e1:::e2:::Enil)
   end.
-
-(*
-  |  (Eop Oandl ((Eop Ocast32signed
-         ((Eop Oneg ((Eop (Ocmp (Ccompluimm Ceq zero0))
-        (y0:::Enil)):::Enil)):::Enil)):::v0:::Enil)),
-     (Eop Oandl ((Eop Ocast32signed
-         ((Eop Oneg ((Eop (Ocmp (Ccompluimm Cne zero1))
-        (y1:::Enil)):::Enil)):::Enil)):::v1:::Enil)) =>
-     if same_expr_pure y0 y1
-     && Int64.eq zero0 Int64.zero
-     && Int64.eq zero1 Int64.zero                 
-     then Eop Oselectl (v0:::v1:::y0:::Enil)
-     else Eop Oorl (e1:::e2:::Enil) *)
+     
 
 Nondetfunction xorlimm (n1: int64) (e2: expr) :=
   if Int64.eq n1 Int64.zero then e2 else
diff --git a/mppa_k1c/SelectLongproof.v b/mppa_k1c/SelectLongproof.v
index 49abc7c7..dd4cfa69 100644
--- a/mppa_k1c/SelectLongproof.v
+++ b/mppa_k1c/SelectLongproof.v
@@ -407,6 +407,7 @@ 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.
@@ -424,7 +425,7 @@ Proof.
       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.
+  + simpl in *. congruence. *)
 - TrivialExists.
 Qed.
 
@@ -525,82 +526,6 @@ Proof.
       rewrite Int64.and_zero.
       rewrite Int64.or_zero.
       reflexivity.
-      (*
-  - (* selectl unsigned *)
-    destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try TrivialExists.
-    predSpec Int64.eq Int64.eq_spec zero0 Int64.zero; simpl; try TrivialExists.
-    predSpec Int64.eq Int64.eq_spec zero1 Int64.zero; simpl; [ | TrivialExists].
-    inv H.
-    inv H0.
-    inv H6.
-    inv H3.
-    inv H2.
-    inv H7.
-    inv H4.
-    inv H3.
-    inv H6.
-    inv H4.
-    inv H3.
-    inv H14.
-    inv H13.
-    inv H6.
-    inv H4.
-    inv H13.
-    inv H14.
-    inv H9.
-    inv H11.
-    inv H13.
-    inv H3.
-    inv H6.
-    inv H7.
-    inv H3.
-    inv H14.
-    inv H17.
-    simpl in *.
-    inv H8.
-    inv H5.
-    inv H10.
-    inv H12.
-    inv H15.
-    inv H16.
-    inv H11.
-    inv H13.
-    unfold same_expr_pure in PURE.
-    destruct y0; try congruence.
-    destruct y1; try congruence.
-    destruct (ident_eq i i0); try congruence; clear PURE.
-    rewrite <- e0 in *; clear e0.
-    inv H6.
-    inv H7.
-    rename v10 into vtest.
-    replace v11 with vtest in * by congruence.
-    TrivialExists.
-    simpl.
-    f_equal.
-    unfold selectl.
-    destruct vtest; simpl; trivial.
-    rewrite Val.andl_commut.
-    destruct v4; simpl; trivial.
-    rewrite Val.andl_commut.
-    rewrite Val.orl_commut.
-    destruct v9; simpl; trivial.
-    rewrite int64_eq_commut.
-    destruct (Int64.eq i1 Int64.zero); simpl.
-    
-    + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
-      replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
-      rewrite Int64.and_mone.
-      rewrite Int64.and_zero.
-      rewrite Int64.or_commut.
-      rewrite Int64.or_zero.
-      reflexivity.
-   + replace (Int64.repr (Int.signed (Int.neg Int.one))) with Int64.mone by Int64.bit_solve.
-      replace (Int64.repr (Int.signed (Int.neg Int.zero))) with Int64.zero by Int64.bit_solve.
-      rewrite Int64.and_mone.
-      rewrite Int64.and_zero.
-      rewrite Int64.or_zero.
-      reflexivity.
-   +  *)
 - TrivialExists.
 Qed.
 
diff --git a/test/monniaux/bitsliced-aes/bs.c b/test/monniaux/bitsliced-aes/bs.c
index 6c68e496..1fc046d1 100644
--- a/test/monniaux/bitsliced-aes/bs.c
+++ b/test/monniaux/bitsliced-aes/bs.c
@@ -19,8 +19,13 @@ static inline word_t compcert_ternary(word_t x, word_t v0, word_t v1) {
 /* with function call to ternary 
 #define TERNARY0(cmp,v1) compcert_ternary(cmp, 0, v1)
 */
-
+/*
 #define TERNARY0(x, v1) ((unsigned long) ((long) (-(((long) (x))!=0)) & (v1)))
+#define TERNARY(x, v0, v1) \
+  (((long) (-(((long) (x))==0)) & ((long) (v0))) |	\
+   ((long) (-(((long) (x))!=0)) & ((long) (v1))))
+*/
+#define TERNARY(x, v0, v1) compcert_ternary((x), (v0), (v1))
 
 #if (defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__) ||\
         defined(__amd64__) || defined(__amd32__)|| defined(__amd16__)
@@ -415,7 +420,9 @@ void bs_transpose_dst(word_t * transpose, word_t * blocks)
             for(j=0; j < WORD_SIZE; j++)
             {
                 // TODO make const time
-	      *(transptr++) |= TERNARY0((w & bitmask), bitpos);
+	      word_t old = *transptr;
+	      /* *(transptr++) = old | TERNARY0((w & bitmask), bitpos); */
+	      *(transptr++) = TERNARY(w & bitmask, old, old|bitpos);
 	      bitmask <<= 1;
             }
 #else
@@ -514,8 +521,8 @@ void bs_transpose_rev(word_t * blocks)
 	word_t bitmask = ONE;
         for(j=0; j < WORD_SIZE; j++)
         {
-	  word_t bit = TERNARY0(w & bitmask, bitpos);
-	  *transptr |= bit;
+	  word_t old = *transptr;
+	  *transptr = TERNARY(w & bitmask, old, old | bitpos);
 	  transptr += WORDS_PER_BLOCK;
 	  bitmask <<= 1;
         }