From 633e60ed36c07c4b6cb4b1dc93b9eea312882ceb Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Thu, 4 Jul 2019 17:49:11 +0200
Subject: Make __builtin_sel available from C source code

It is type-checked like a conditional expression then translated to
a call to the known builtin function.
---
 cparser/Elab.ml | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

(limited to 'cparser')

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index eea60127..3797164d 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1802,6 +1802,42 @@ let elab_expr ctx loc env a =
           (print_typ env) ty (print_typ env) ty'  (print_typ env) ty'  (print_typ env) ty;
       { edesc = ECall(ident, [b2; b3]); etyp = ty },env
 
+  | CALL((VARIABLE "__builtin_sel" as a0), al) ->
+      begin match al with
+      | [a1; a2; a3] ->
+          let b0,env = elab env a0 in
+          let b1,env = elab env a1 in
+          let b2,env = elab env a2 in
+          let b3,env = elab env a3 in
+          if not (is_scalar_type env b1.etyp) then
+            error "first argument of '__builtin_sel' is not a scalar type (invalid %a)"
+               (print_typ env) b1.etyp;
+          let tyres =
+            match pointer_decay env b2.etyp, pointer_decay env b3.etyp with
+            | (TInt _ | TFloat _ | TEnum _), (TInt _ | TFloat _ | TEnum _) ->
+                binary_conversion env b2.etyp b3.etyp
+            | (TPtr(ty1, a1) as pty1), (TPtr(ty2, a2)  as pty2) ->
+                if is_void_type env ty1 || is_void_type env ty2 then
+                  TPtr(TVoid (add_attributes a1 a2), [])
+                else begin
+                  match combine_types AttrIgnoreAll env pty1 pty2 with
+                  | None ->
+                      warning Pointer_type_mismatch "the second and third arguments of '__builtin_sel' have incompatible pointer types (%a and %a)"
+                     (print_typ env) pty1  (print_typ env) pty2;
+                     (* tolerance *)
+                     TPtr(TVoid (add_attributes a1 a2), [])
+                  | Some ty -> ty
+                end
+            | _, _ ->
+                fatal_error "wrong types (%a and %a) for the second and third arguments of '__builtin_sel'"
+                  (print_typ env) b2.etyp (print_typ env) b3.etyp
+
+            in
+          { edesc = ECall(b0, [b1; b2; b3]); etyp = tyres }, env
+      | _ ->
+          fatal_error "'__builtin_sel' expect 3 arguments"
+      end
+
   | CALL(a1, al) ->
       let b1,env =
         (* Catch the old-style usage of calling a function without
-- 
cgit