Merge pull request diffblue#2218 from diffblue/builtin_fpclassify

add support for __builtin_fpclassify

Author: Daniel Kroening

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);
 }

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" ||

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);

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);

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