diff options
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 2 | ||||
| -rw-r--r-- | mppa_k1c/Asmblockgenproof1.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 2 | ||||
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 9 | ||||
| -rw-r--r-- | test/monniaux/bitsliced-aes/bs.c | 4 | ||||
| -rw-r--r-- | test/monniaux/bitsliced-tea/bstea.h | 12 | ||||
| -rw-r--r-- | test/monniaux/bitsliced-tea/bstea_wordsize.h | 2 |
7 files changed, 14 insertions, 21 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 6315192c..a7e3c8ef 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -741,7 +741,7 @@ Definition transl_op do r0 <- ireg_of a0; do r1 <- ireg_of a1; do rS <- ireg_of aS; - OK (Pcmove BTdnez r0 rS r1 ::i k) + OK (Pcmove BTwnez r0 rS r1 ::i k) | _, _ => Error(msg "Asmgenblock.transl_op") diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index d90b73e2..99ab1b91 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1661,8 +1661,8 @@ Opaque Int.eq. destruct (rs x) eqn:eqX; try constructor. destruct (rs x0) eqn:eqX0; try constructor. simpl. - rewrite int64_eq_comm. - destruct (Int64.eq i Int64.zero); simpl; rewrite Pregmap.gss; constructor. + rewrite int_eq_comm. + destruct (Int.eq i Int.zero); simpl; rewrite Pregmap.gss; constructor. * intros. rewrite Pregmap.gso; congruence. Qed. diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 7fefe594..f8f5bf3b 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -286,6 +286,7 @@ Nondetfunction orl (e1: expr) (e2: expr) := | t1, Eop (Olongconst n2) Enil => orlimm n2 t1 | (Eop Onotl (t1:::Enil)), t2 => Eop Oornl (t1:::t2:::Enil) | t1, (Eop Onotl (t2:::Enil)) => Eop Oornl (t2:::t1:::Enil) + | _, _ => Eop Oorl (e1:::e2:::Enil) end. (* @@ -300,7 +301,6 @@ 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) *) Nondetfunction xorlimm (n1: int64) (e2: expr) := diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index de2fd422..da108ada 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -53,8 +53,8 @@ Definition select (v0 v1 vselect : aval) : aval := Definition selectl (v0 v1 vselect : aval) : aval := match vselect with - | L iselect => - if Int64.eq Int64.zero iselect + | I iselect => + if Int.eq Int.zero iselect then binop_long (fun x0 x1 => x0) v0 v1 else binop_long (fun x0 x1 => x1) v0 v1 | _ => Vtop @@ -274,8 +274,9 @@ Proof. (* selectl *) - inv H2; simpl; try constructor. + destruct (Int.eq _ _); apply binop_long_sound; trivial. - + destruct (Int.eq _ _); - destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. Qed. End SOUNDNESS. diff --git a/test/monniaux/bitsliced-aes/bs.c b/test/monniaux/bitsliced-aes/bs.c index 9a24643c..929fd24d 100644 --- a/test/monniaux/bitsliced-aes/bs.c +++ b/test/monniaux/bitsliced-aes/bs.c @@ -2,8 +2,8 @@ #include <string.h> #include "bs.h" -#if defined(__K1C__) -#define TERNARY(x, v0, v1) __builtin_ternary_ulong((x), (v1), (v0)) +#if defined(__K1C__) && defined(__COMPCERT__) +#define TERNARY(x, v0, v1) __builtin_ternary_ulong((x)!=0, (v1), (v0)) #else #define TERNARY(x, v0, v1) ((x) ? (v1) : (v0)) #endif diff --git a/test/monniaux/bitsliced-tea/bstea.h b/test/monniaux/bitsliced-tea/bstea.h index fa767996..793f29ff 100644 --- a/test/monniaux/bitsliced-tea/bstea.h +++ b/test/monniaux/bitsliced-tea/bstea.h @@ -6,16 +6,8 @@ #include "bstea_wordsize.h" -static inline long compcert_ternary_signedl(long x, long v0, long v1) { - return ((-(x==0)) & v0) | ((-(x!=0)) & v1); -} - -static inline uint32_t compcert_ternary(uint32_t x, uint32_t v0, uint32_t v1) { - return compcert_ternary_signedl(x, v0, v1); -} - -#if defined(__K1C__) -#define TERNARY(x, v1, v0) compcert_ternary((x), (v0), (v1)) +#if defined(__K1C__) && defined(__COMPCERT__) +#define TERNARY(x, v1, v0) __builtin_ternary_ulong((x)!=0, (v1), (v0)) #else #define TERNARY(x, v1, v0) ((x) ? (v1) : (v0)) #endif diff --git a/test/monniaux/bitsliced-tea/bstea_wordsize.h b/test/monniaux/bitsliced-tea/bstea_wordsize.h index 5381e17c..b4e2e823 100644 --- a/test/monniaux/bitsliced-tea/bstea_wordsize.h +++ b/test/monniaux/bitsliced-tea/bstea_wordsize.h @@ -6,7 +6,7 @@ #if defined __x86_64__ || defined __amd64__ || defined __x86_64 || \ defined __amd64 || defined _M_X64 || defined __ia64__ || \ defined __ia64__ || defined __IA64__ || defined __ia64 || \ - defined _M_IA64 + defined _M_IA64 || defined __K1C__ # define __BSTEA_WORDSIZE 64 #else # define __BSTEA_WORDSIZE 32 |