diff options
| -rw-r--r-- | backend/Selection.v | 18 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 1 | ||||
| -rw-r--r-- | mppa_k1c/Op.v | 6 | ||||
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 8 | ||||
| -rw-r--r-- | mppa_k1c/SelectLongproof.v | 3 | ||||
| -rw-r--r-- | mppa_k1c/ValueAOp.v | 4 | ||||
| -rw-r--r-- | test/monniaux/bitsliced-aes/bs.c | 11 | ||||
| -rw-r--r-- | test/monniaux/ternary_builtin/ternary_builtin.c | 8 |
8 files changed, 37 insertions, 22 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index 5e45dde3..5cfa3dcb 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -286,10 +286,26 @@ Definition sel_builtin optid ef args := ((sel_expr a3)::: (sel_expr a2)::: (sel_expr a1):::Enil))) + | _ => Error (msg "__builtin_ternary_ulong: arguments") + end + end + else + if String.string_dec name "__builtin_ternary_ulong" + then + match optid with + | None => OK Sskip + | Some id => + match args with + | a1::a2::a3::nil => + OK (Sassign id (Eop Oselectl + ((sel_expr a3)::: + (sel_expr a2)::: + (sel_expr a1):::Enil))) | _ => Error (msg "__builtin_ternary_uint: arguments") end end - else sel_builtin_default optid ef args) + else + sel_builtin_default optid ef args) | _ => sel_builtin_default optid ef args end. diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 1ab38a2b..c17ce75a 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -187,6 +187,7 @@ let builtins_generic = { false); (* Ternary operator *) builtin_ternary "uint" (TInt(IUInt, [])); + builtin_ternary "ulong" (TInt(IULong, [])); (* Annotations *) "__builtin_annot", diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 10e4a350..74788387 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -272,12 +272,12 @@ Definition select (v0 : val) (v1 : val) (vselect : val) : val := Definition selectl (v0 : val) (v1 : val) (vselect : val) : val := match vselect with - | Vlong iselect => + | Vint iselect => match v0 with | Vlong i0 => match v1 with | Vlong i1 => - Vlong (if Int64.cmp Ceq Int64.zero iselect + Vlong (if Int.cmp Ceq Int.zero iselect then i0 else i1) | _ => Vundef @@ -607,7 +607,7 @@ Definition type_of_operation (op: operation) : list typ * typ := | Ocmp c => (type_of_condition c, Tint) | Oselect => (Tint :: Tint :: Tint :: nil, Tint) - | Oselectl => (Tlong :: Tlong :: Tlong :: nil, Tlong) + | Oselectl => (Tlong :: Tlong :: Tint :: nil, Tlong) end. Definition type_of_addressing (addr: addressing) : list typ := diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index 60b8f094..7fefe594 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -285,7 +285,10 @@ Nondetfunction orl (e1: expr) (e2: expr) := | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2 | 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) + | t1, (Eop Onotl (t2:::Enil)) => Eop Oornl (t2:::t1:::Enil) + end. + + (* | (Eop Oandl ((Eop Ocast32signed ((Eop Oneg ((Eop (Ocmp (Ccomplimm Ceq zero0)) (y0:::Enil)):::Enil)):::Enil)):::v0:::Enil)), @@ -298,8 +301,7 @@ Nondetfunction orl (e1: expr) (e2: expr) := then Eop Oselectl (v0:::v1:::y0:::Enil) else Eop Oorl (e1:::e2:::Enil) | _, _ => Eop Oorl (e1:::e2:::Enil) - end. - + *) 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 11804d2e..e18de2ee 100644 --- a/mppa_k1c/SelectLongproof.v +++ b/mppa_k1c/SelectLongproof.v @@ -452,6 +452,7 @@ Proof. - InvEval. apply eval_orlimm; auto. - (*orn*) InvEval. TrivialExists; simpl; congruence. - (*orn reversed*) InvEval. rewrite Val.orl_commut. TrivialExists; simpl; congruence. + (* - (* selectl *) destruct (same_expr_pure y0 y1) eqn:PURE; simpl; try TrivialExists. predSpec Int64.eq Int64.eq_spec zero0 Int64.zero; simpl; try TrivialExists. @@ -525,7 +526,7 @@ Proof. rewrite Int64.and_mone. rewrite Int64.and_zero. rewrite Int64.or_zero. - reflexivity. + reflexivity. *) - TrivialExists. Qed. diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index 9c851573..de2fd422 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -273,8 +273,8 @@ Proof. destruct a1; destruct a0; eauto; constructor. (* selectl *) - inv H2; simpl; try constructor. - + destruct (Int64.eq _ _); apply binop_long_sound; trivial. - + destruct (Int64.eq _ _); + + destruct (Int.eq _ _); apply binop_long_sound; trivial. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. Qed. diff --git a/test/monniaux/bitsliced-aes/bs.c b/test/monniaux/bitsliced-aes/bs.c index 063f36f5..9a24643c 100644 --- a/test/monniaux/bitsliced-aes/bs.c +++ b/test/monniaux/bitsliced-aes/bs.c @@ -2,17 +2,8 @@ #include <string.h> #include "bs.h" - -static inline long compcert_ternary_signedl(long x, long v0, long v1) { - return ((-(x==0)) & v0) | ((-(x!=0)) & v1); -} - -static inline word_t compcert_ternary(word_t x, word_t v0, word_t v1) { - return compcert_ternary_signedl(x, v0, v1); -} - #if defined(__K1C__) -#define TERNARY(x, v0, v1) compcert_ternary((x), (v0), (v1)) +#define TERNARY(x, v0, v1) __builtin_ternary_ulong((x), (v1), (v0)) #else #define TERNARY(x, v0, v1) ((x) ? (v1) : (v0)) #endif diff --git a/test/monniaux/ternary_builtin/ternary_builtin.c b/test/monniaux/ternary_builtin/ternary_builtin.c index 98497387..1295581c 100644 --- a/test/monniaux/ternary_builtin/ternary_builtin.c +++ b/test/monniaux/ternary_builtin/ternary_builtin.c @@ -1,10 +1,14 @@ #include <stdio.h> -int essai(int x, unsigned y, unsigned z) { +unsigned essai(int x, unsigned y, unsigned z) { return __builtin_ternary_uint(x, y, z); } +unsigned long essai2(int x, unsigned long y, unsigned long z) { + return __builtin_ternary_ulong(x, y, z); +} + int main() { - printf("%d\n", essai(0, 42, 69)); + printf("%ld\n", essai2(0, 42, 69)); return 0; } |