From 86d7e48d92d602e2349032883b7b753bbea81a3c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 27 Mar 2019 09:47:32 +0100 Subject: improvements on cmoved etc. --- mppa_k1c/SelectLong.vp | 21 +++-------- mppa_k1c/SelectLongproof.v | 79 +--------------------------------------- test/monniaux/bitsliced-aes/bs.c | 15 ++++++-- 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; } -- cgit