aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2017-09-26 10:51:00 +0200
committerBernhard Schommer <bernhardschommer@gmail.com>2017-09-26 10:51:00 +0200
commitc42707362b99da19cc7a3f2496d9620dcc0dfa62 (patch)
tree51482a67e86f3130b1cb3067c34c7b5cf31d91c1
parent0c36ecaed8fc861cb3e14b1396b0b6b6e754c199 (diff)
downloadcompcert-kvx-c42707362b99da19cc7a3f2496d9620dcc0dfa62.tar.gz
compcert-kvx-c42707362b99da19cc7a3f2496d9620dcc0dfa62.zip
Moved common buitlins to C2C gernic_builtins.
-rw-r--r--arm/CBuiltins.ml9
-rw-r--r--cfrontend/C2C.ml12
-rw-r--r--powerpc/CBuiltins.ml8
-rw-r--r--riscV/CBuiltins.ml8
-rw-r--r--x86/CBuiltins.ml8
5 files changed, 11 insertions, 34 deletions
diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml
index 2015607a..ec4f4aaa 100644
--- a/arm/CBuiltins.ml
+++ b/arm/CBuiltins.ml
@@ -23,12 +23,6 @@ let builtins = {
];
Builtins.functions = [
(* Integer arithmetic *)
- "__builtin_bswap",
- (TInt(IUInt, []), [TInt(IUInt, [])], false);
- "__builtin_bswap32",
- (TInt(IUInt, []), [TInt(IUInt, [])], false);
- "__builtin_bswap16",
- (TInt(IUShort, []), [TInt(IUShort, [])], false);
"__builtin_clz",
(TInt(IInt, []), [TInt(IUInt, [])], false);
"__builtin_clzl",
@@ -41,9 +35,6 @@ let builtins = {
(TInt(IInt, []), [TInt(IULong, [])], false);
"__builtin_ctzll",
(TInt(IInt, []), [TInt(IULongLong, [])], false);
- (* Float arithmetic *)
- "__builtin_fsqrt",
- (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
(* Memory accesses *)
"__builtin_read16_reversed",
(TInt(IUShort, []), [TPtr(TInt(IUShort, [AConst]), [])], false);
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index b194b84a..4dbd6c05 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -135,9 +135,19 @@ let string_of_errmsg msg =
let builtins_generic = {
Builtins.typedefs = [];
Builtins.functions = [
+ (* Integer arithmetic *)
+ "__builtin_bswap",
+ (TInt(IUInt, []), [TInt(IUInt, [])], false);
+ "__builtin_bswap32",
+ (TInt(IUInt, []), [TInt(IUInt, [])], false);
+ "__builtin_bswap16",
+ (TInt(IUShort, []), [TInt(IUShort, [])], false);
(* Floating-point absolute value *)
"__builtin_fabs",
- (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
+ (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
+ (* Float arithmetic *)
+ "__builtin_fsqrt",
+ (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
(* Block copy *)
"__builtin_memcpy_aligned",
(TVoid [],
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index d33d6252..35d6b89f 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -40,12 +40,6 @@ let builtins = {
(TInt(IInt, []), [TInt(IULong, [])], false);
"__builtin_ctzll",
(TInt(IInt, []), [TInt(IULongLong, [])], false);
- "__builtin_bswap",
- (TInt(IUInt, []), [TInt(IUInt, [])], false);
- "__builtin_bswap32",
- (TInt(IUInt, []), [TInt(IUInt, [])], false);
- "__builtin_bswap16",
- (TInt(IUShort, []), [TInt(IUShort, [])], false);
"__builtin_cmpb",
(TInt (IUInt, []), [TInt(IUInt, []);TInt(IUInt, [])], false);
(* Float arithmetic *)
@@ -65,8 +59,6 @@ let builtins = {
(TFloat(FDouble, []),
[TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
false);
- "__builtin_fsqrt",
- (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
"__builtin_frsqrte",
(TFloat(FDouble, []), [TFloat(FDouble, [])], false);
"__builtin_fres",
diff --git a/riscV/CBuiltins.ml b/riscV/CBuiltins.ml
index 385f9d13..0c981d11 100644
--- a/riscV/CBuiltins.ml
+++ b/riscV/CBuiltins.ml
@@ -26,14 +26,8 @@ let builtins = {
"__builtin_fence",
(TVoid [], [], false);
(* Integer arithmetic *)
- "__builtin_bswap",
- (TInt(IUInt, []), [TInt(IUInt, [])], false);
"__builtin_bswap64",
(TInt(IULongLong, []), [TInt(IULongLong, [])], false);
- "__builtin_bswap32",
- (TInt(IUInt, []), [TInt(IUInt, [])], false);
- "__builtin_bswap16",
- (TInt(IUShort, []), [TInt(IUShort, [])], false);
(* Float arithmetic *)
"__builtin_fmadd",
(TFloat(FDouble, []),
@@ -51,8 +45,6 @@ let builtins = {
(TFloat(FDouble, []),
[TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
false);
- "__builtin_fsqrt",
- (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
"__builtin_fmax",
(TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
"__builtin_fmin",
diff --git a/x86/CBuiltins.ml b/x86/CBuiltins.ml
index 09303223..69a2eb64 100644
--- a/x86/CBuiltins.ml
+++ b/x86/CBuiltins.ml
@@ -31,14 +31,8 @@ let builtins = {
];
Builtins.functions = [
(* Integer arithmetic *)
- "__builtin_bswap",
- (TInt(IUInt, []), [TInt(IUInt, [])], false);
"__builtin_bswap64",
(TInt(IULongLong, []), [TInt(IULongLong, [])], false);
- "__builtin_bswap32",
- (TInt(IUInt, []), [TInt(IUInt, [])], false);
- "__builtin_bswap16",
- (TInt(IUShort, []), [TInt(IUShort, [])], false);
"__builtin_clz",
(TInt(IInt, []), [TInt(IUInt, [])], false);
"__builtin_clzl",
@@ -52,8 +46,6 @@ let builtins = {
"__builtin_ctzll",
(TInt(IInt, []), [TInt(IULongLong, [])], false);
(* Float arithmetic *)
- "__builtin_fsqrt",
- (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
"__builtin_fmax",
(TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false);
"__builtin_fmin",