diff options
-rw-r--r-- | mppa_k1c/SelectLong.vp | 8 | ||||
-rw-r--r-- | mppa_k1c/SelectLongproof.v | 36 | ||||
-rw-r--r-- | test/monniaux/bitsliced-aes/bs.c | 7 | ||||
-rw-r--r-- | test/monniaux/bitsliced-aes/notes.txt | 13 |
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 |