From 633e60ed36c07c4b6cb4b1dc93b9eea312882ceb Mon Sep 17 00:00:00 2001 From: Xavier Leroy 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. --- cfrontend/Csyntax.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'cfrontend/Csyntax.v') diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 00565309..c34a5e13 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -100,6 +100,18 @@ Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) := Eassignop (match id with Incr => Oadd | Decr => Osub end) l (Eval (Vint Int.one) type_int32s) (typeconv ty) ty. +(** Selection is a conditional expression that always evaluates both arms + and can be implemented by "conditional move" instructions. + It is expressed as an invocation of a builtin function. *) + +Definition Eselection (r1 r2 r3: expr) (ty: type) := + let t := typ_of_type ty in + let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in + Ebuiltin (EF_builtin "__builtin_sel"%string sg) + (Tcons type_bool (Tcons ty (Tcons ty Tnil))) + (Econs r1 (Econs r2 (Econs r3 Enil))) + ty. + (** Extract the type part of a type-annotated expression. *) Definition typeof (a: expr) : type := -- cgit