From 52595bd833925556982d662c848205cdbb8d8661 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 May 2018 10:06:20 +0100 Subject: [PATCH 1/2] add support for __builtin_fpclassify --- src/ansi-c/c_typecheck_expr.cpp | 45 ++++++++++++++++++++++++++++ src/ansi-c/cprover_builtin_headers.h | 1 + src/ansi-c/library/cprover.h | 1 + src/ansi-c/library/math.c | 35 +++++++--------------- 4 files changed, 57 insertions(+), 25 deletions(-) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 7c3e914ddfa..be086c56f4f 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2195,6 +2195,51 @@ exprt c_typecheck_baset::do_special_functions( return bswap_expr; } + else if( + identifier == "__builtin_fpclassify" || + identifier == CPROVER_PREFIX "fpclassify") + { + if(expr.arguments().size() != 6) + { + err_location(f_op); + error() << identifier << " expects six arguments" << eom; + throw 0; + } + + // This gets 5 integers followed by a float or double. + // The five integers are the return values for the cases + // FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL and FP_ZERO. + // gcc expects this to be able to produce compile-time constants. + + const exprt &fp_value = expr.arguments()[5]; + + if(fp_value.type().id() != ID_floatbv) + { + err_location(fp_value); + error() << "non-floating-point argument for " << identifier << eom; + throw 0; + } + + const auto &floatbv_type = to_floatbv_type(fp_value.type()); + + const exprt zero = ieee_floatt::zero(floatbv_type).to_expr(); + + const auto &arguments = expr.arguments(); + + return if_exprt( + isnan_exprt(fp_value), + arguments[0], + if_exprt( + isinf_exprt(fp_value), + arguments[1], + if_exprt( + isnormal_exprt(fp_value), + arguments[2], + if_exprt( + ieee_float_equal_exprt(fp_value, zero), + arguments[4], + arguments[3])))); // subnormal + } else if(identifier==CPROVER_PREFIX "isnanf" || identifier==CPROVER_PREFIX "isnand" || identifier==CPROVER_PREFIX "isnanld" || diff --git a/src/ansi-c/cprover_builtin_headers.h b/src/ansi-c/cprover_builtin_headers.h index 196e6a8f21e..48b0d056b14 100644 --- a/src/ansi-c/cprover_builtin_headers.h +++ b/src/ansi-c/cprover_builtin_headers.h @@ -39,6 +39,7 @@ __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p); void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent); // float stuff +int __CPROVER_fpclassify(int, int, int, int, int, ...); __CPROVER_bool __CPROVER_isnanf(float f); __CPROVER_bool __CPROVER_isnand(double f); __CPROVER_bool __CPROVER_isnanld(long double f); diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h index 7fce070860a..ab68bbcbe68 100644 --- a/src/ansi-c/library/cprover.h +++ b/src/ansi-c/library/cprover.h @@ -70,6 +70,7 @@ extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_ #endif // float stuff +int __CPROVER_fpclassify(int, int, int, int, int, ...); __CPROVER_bool __CPROVER_isfinite(double f); __CPROVER_bool __CPROVER_isinf(double f); __CPROVER_bool __CPROVER_isnormal(double f); diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index c9f52dc8f76..332c8baaffb 100644 --- a/src/ansi-c/library/math.c +++ b/src/ansi-c/library/math.c @@ -287,11 +287,8 @@ inline short _fdclass(float f) { inline int __fpclassifyd(double d) { __CPROVER_HIDE: - return __CPROVER_isnand(d)?FP_NAN: - __CPROVER_isinfd(d)?FP_INFINITE: - d==0?FP_ZERO: - __CPROVER_isnormald(d)?FP_NORMAL: - FP_SUBNORMAL; + return __CPROVER_fpclassify( + FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d); } /* FUNCTION: __fpclassifyf */ @@ -303,11 +300,8 @@ inline int __fpclassifyd(double d) { inline int __fpclassifyf(float f) { __CPROVER_HIDE: - return __CPROVER_isnanf(f)?FP_NAN: - __CPROVER_isinff(f)?FP_INFINITE: - f==0?FP_ZERO: - __CPROVER_isnormalf(f)?FP_NORMAL: - FP_SUBNORMAL; + return __CPROVER_fpclassify( + FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f); } /* FUNCTION: __fpclassifyl */ @@ -319,11 +313,8 @@ inline int __fpclassifyf(float f) { inline int __fpclassifyl(long double f) { __CPROVER_HIDE: - return __CPROVER_isnanld(f)?FP_NAN: - __CPROVER_isinfld(f)?FP_INFINITE: - f==0?FP_ZERO: - __CPROVER_isnormalld(f)?FP_NORMAL: - FP_SUBNORMAL; + return __CPROVER_fpclassify( + FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, f); } /* FUNCTION: __fpclassify */ @@ -339,20 +330,14 @@ inline int __fpclassifyl(long double f) { #ifdef __APPLE__ inline int __fpclassify(long double d) { __CPROVER_HIDE: - return __CPROVER_isnanld(d)?FP_NAN: - __CPROVER_isinfld(d)?FP_INFINITE: - d==0?FP_ZERO: - __CPROVER_isnormalld(d)?FP_NORMAL: - FP_SUBNORMAL; + return __CPROVER_fpclassify( + FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d); } #else inline int __fpclassify(double d) { __CPROVER_HIDE: - return __CPROVER_isnand(d)?FP_NAN: - __CPROVER_isinfd(d)?FP_INFINITE: - d==0?FP_ZERO: - __CPROVER_isnormald(d)?FP_NORMAL: - FP_SUBNORMAL; + return __CPROVER_fpclassify( + FP_NAN, FP_INFINITE, FP_NORMAL, FP_SUBNORMAL, FP_ZERO, d); } #endif From c3603e332ccba64d7cdcd736dd7e623ea8cf666d Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 22 May 2018 13:08:03 +0100 Subject: [PATCH 2/2] added a test for raw __builtin_fpclassify --- regression/cbmc/Float_lib1/main.c | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/regression/cbmc/Float_lib1/main.c b/regression/cbmc/Float_lib1/main.c index c344517d28d..0db0db8363c 100644 --- a/regression/cbmc/Float_lib1/main.c +++ b/regression/cbmc/Float_lib1/main.c @@ -19,6 +19,19 @@ int main() { assert(fpclassify(-0.0)==FP_ZERO); #endif + #if !defined(__clang__) && defined(__GNUC__) + assert(__builtin_fpclassify(0, 1, 2, 3, 4, DBL_MAX+DBL_MAX)==1); + assert(__builtin_fpclassify(0, 1, 2, 3, 4, 0*(DBL_MAX+DBL_MAX))==0); + assert(__builtin_fpclassify(0, 1, 2, 3, 4, 1.0)==2); + assert(__builtin_fpclassify(0, 1, 2, 3, 4, DBL_MIN)==2); + assert(__builtin_fpclassify(0, 1, 2, 3, 4, DBL_MIN/2)==3); + assert(__builtin_fpclassify(0, 1, 2, 3, 4, -0.0)==4); + + // these are compile-time + _Static_assert(__builtin_fpclassify(0, 1, 2, 3, 4, -0.0)==4, + "__builtin_fpclassify is constant"); + #endif + assert(signbit(-1.0)!=0); assert(signbit(1.0)==0); }