diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-07-04 17:49:11 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-07-17 09:17:28 +0200 |
| commit | 633e60ed36c07c4b6cb4b1dc93b9eea312882ceb (patch) | |
| tree | 22feeaf195a61a3ffecf280717ddbde60987a5c7 /cfrontend/Csyntax.v | |
| parent | 10aa130361a5a673a14a7b38ed9c077103f9155f (diff) | |
| download | compcert-kvx-633e60ed36c07c4b6cb4b1dc93b9eea312882ceb.tar.gz compcert-kvx-633e60ed36c07c4b6cb4b1dc93b9eea312882ceb.zip | |
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.
Diffstat (limited to 'cfrontend/Csyntax.v')
| -rw-r--r-- | cfrontend/Csyntax.v | 12 |
1 files changed, 12 insertions, 0 deletions
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 := |