add support for __builtin_fpclassify

Author: kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -2195,6 +2195,44 @@ 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.
+
+    if(expr.arguments()[5].type().id()!=ID_floatbv)
+    {
+      err_location(expr.arguments()[5]);
+      error() << "non-floating-point argument for " << identifier << eom;
+      throw 0;
+    }
+
+    const auto &floatbv_type=to_floatbv_type(expr.arguments()[5].type());
+
+    const exprt zero=
+      ieee_floatt::zero(floatbv_type).to_expr();
+
+    return
+      if_exprt(unary_predicate_exprt(ID_isnan, expr.arguments()[5]),
+               expr.arguments()[0],
+      if_exprt(unary_predicate_exprt(ID_isinf, expr.arguments()[5]),
+               expr.arguments()[1],
+      if_exprt(unary_predicate_exprt(ID_isnormal, expr.arguments()[5]),
+               expr.arguments()[2],
+      if_exprt(ieee_float_equal_exprt(expr.arguments()[5], zero),
+               expr.arguments()[4],
+      expr.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