diff options
| -rw-r--r-- | backend/Selection.v | 9 | ||||
| -rw-r--r-- | cfrontend/C2C.ml | 9 | ||||
| -rw-r--r-- | test/monniaux/ternary_builtin/ternary_builtin.c | 12 |
3 files changed, 16 insertions, 14 deletions
diff --git a/backend/Selection.v b/backend/Selection.v index 05a06abf..27c5bd10 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -267,6 +267,11 @@ Definition sel_switch_long := (fun arg ofs => subl arg (longconst (Int64.repr ofs))) lowlong. +Definition sel_builtin optid ef args := + Sbuiltin (sel_builtin_res optid) ef + (sel_builtin_args args + (Machregs.builtin_constraints ef)). + (** Conversion from Cminor statements to Cminorsel statements. *) Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := @@ -278,9 +283,7 @@ Fixpoint sel_stmt (s: Cminor.stmt) : res stmt := OK (match classify_call fn with | Call_default => Scall optid sg (inl _ (sel_expr fn)) (sel_exprlist args) | Call_imm id => Scall optid sg (inr _ id) (sel_exprlist args) - | Call_builtin ef => Sbuiltin (sel_builtin_res optid) ef - (sel_builtin_args args - (Machregs.builtin_constraints ef)) + | Call_builtin ef => sel_builtin optid ef args end) | Cminor.Sbuiltin optid ef args => OK (Sbuiltin (sel_builtin_res optid) ef diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index bd9b7487..1ab38a2b 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -154,6 +154,10 @@ let ais_annot_functions = else [] +let builtin_ternary suffix typ = + ("__builtin_ternary_" ^ suffix), + (typ, [TInt(IInt, []); typ; typ], false);; + let builtins_generic = { Builtins.typedefs = []; Builtins.functions = @@ -180,7 +184,10 @@ let builtins_generic = { TPtr(TVoid [AConst], []); TInt(IULong, []); TInt(IULong, [])], - false); + false); + (* Ternary operator *) + builtin_ternary "uint" (TInt(IUInt, [])); + (* Annotations *) "__builtin_annot", (TVoid [], diff --git a/test/monniaux/ternary_builtin/ternary_builtin.c b/test/monniaux/ternary_builtin/ternary_builtin.c index caa1c4c7..8052da0f 100644 --- a/test/monniaux/ternary_builtin/ternary_builtin.c +++ b/test/monniaux/ternary_builtin/ternary_builtin.c @@ -1,11 +1,3 @@ -int ternary_signed(int x, int v0, int v1) { - return ((-(x==0)) & v0) | ((-(x!=0)) & v1); -} - -int ternary_unsigned(unsigned x, int v0, int v1) { - return ((-(x==0)) & v0) | ((-(x!=0)) & v1); -} - -long ternary_signedl(long x, long v0, long v1) { - return ((-(x==0)) & v0) | ((-(x!=0)) & v1); +int essai(int x, unsigned y, unsigned z) { + return __builtin_ternary_uint(x, y, z); } |