gcc floating-point builtins

regression/cbmc/Float_lib1/main.c

@@ -27,9 +27,27 @@ int main() {
   assert(__builtin_fpclassify(0, 1, 2, 3, 4, DBL_MIN/2)==3);
   assert(__builtin_fpclassify(0, 1, 2, 3, 4, -0.0)==4);
 
+  assert(__builtin_isinf(DBL_MAX+DBL_MAX)==1);
+  assert(__builtin_isinf(0.0)==0);
+  assert(__builtin_isinf(-(DBL_MAX+DBL_MAX))==1);
+
+  assert(__builtin_isinf_sign(DBL_MAX+DBL_MAX)==1);
+  assert(__builtin_isinf_sign(0.0)==0);
+  assert(__builtin_isinf_sign(-(DBL_MAX+DBL_MAX))==-1);
+
   // these are compile-time
   _Static_assert(__builtin_fpclassify(0, 1, 2, 3, 4, -0.0)==4,
                  "__builtin_fpclassify is constant");
+
+  _Static_assert(__builtin_isnormal(DBL_MIN),
+                 "__builtin_isnormal is constant");
+
+  _Static_assert(!__builtin_isinf(0),
+                 "__builtin_isinf is constant");
+
+  _Static_assert(__builtin_isinf_sign(0)==0,
+                 "__builtin_isinf_sign is constant");
+
   #endif
 
   assert(signbit(-1.0)!=0);

src/ansi-c/c_typecheck_expr.cpp

@@ -2255,7 +2255,7 @@ exprt c_typecheck_baset::do_special_functions(
     isnan_exprt isnan_expr(expr.arguments().front());
     isnan_expr.add_source_location()=source_location;
 
-    return isnan_expr;
+    return typecast_exprt::conditional_cast(isnan_expr, expr.type());
   }
   else if(identifier==CPROVER_PREFIX "isfinitef" ||
           identifier==CPROVER_PREFIX "isfinited" ||
@@ -2271,7 +2271,7 @@ exprt c_typecheck_baset::do_special_functions(
     isfinite_exprt isfinite_expr(expr.arguments().front());
     isfinite_expr.add_source_location()=source_location;
 
-    return isfinite_expr;
+    return typecast_exprt::conditional_cast(isfinite_expr, expr.type());
   }
   else if(identifier==CPROVER_PREFIX "inf" ||
           identifier=="__builtin_inf")
@@ -2343,30 +2343,64 @@ exprt c_typecheck_baset::do_special_functions(
     if(expr.arguments().size()!=1)
     {
       err_location(f_op);
-      error() << "isinf expects one operand" << eom;
+      error() << identifier << " expects one operand" << eom;
       throw 0;
     }
 
     isinf_exprt isinf_expr(expr.arguments().front());
     isinf_expr.add_source_location()=source_location;
 
-    return isinf_expr;
+    return typecast_exprt::conditional_cast(isinf_expr, expr.type());
+  }
+  else if(identifier == "__builtin_isinf_sign")
+  {
+    if(expr.arguments().size() != 1)
+    {
+      err_location(f_op);
+      error() << identifier << " expects one operand" << eom;
+      throw 0;
+    }
+
+    // returns 1 for +inf and -1 for -inf, and 0 otherwise
+
+    const exprt &fp_value = expr.arguments().front();
+
+    isinf_exprt isinf_expr(fp_value);
+    isinf_expr.add_source_location() = source_location;
+
+    return if_exprt(
+      isinf_exprt(fp_value),
+      if_exprt(
+        sign_exprt(fp_value),
+        from_integer(-1, expr.type()),
+        from_integer(1, expr.type())),
+      from_integer(0, expr.type()));
   }
-  else if(identifier==CPROVER_PREFIX "isnormalf" ||
-          identifier==CPROVER_PREFIX "isnormald" ||
-          identifier==CPROVER_PREFIX "isnormalld")
+  else if(identifier == CPROVER_PREFIX "isnormalf" ||
+          identifier == CPROVER_PREFIX "isnormald" ||
+          identifier == CPROVER_PREFIX "isnormalld" ||
+          identifier == "__builtin_isnormal")
   {
     if(expr.arguments().size()!=1)
     {
       err_location(f_op);
-      error() << "isnormal expects one operand" << eom;
+      error() << identifier << " expects one operand" << eom;
+      throw 0;
+    }
+
+    const exprt &fp_value = expr.arguments()[0];
+
+    if(fp_value.type().id() != ID_floatbv)
+    {
+      err_location(fp_value);
+      error() << "non-floating-point argument for " << identifier << eom;
       throw 0;
     }
 
     isnormal_exprt isnormal_expr(expr.arguments().front());
     isnormal_expr.add_source_location()=source_location;
 
-    return isnormal_expr;
+    return typecast_exprt::conditional_cast(isnormal_expr, expr.type());
   }
   else if(identifier==CPROVER_PREFIX "signf" ||
           identifier==CPROVER_PREFIX "signd" ||
@@ -2378,14 +2412,14 @@ exprt c_typecheck_baset::do_special_functions(
     if(expr.arguments().size()!=1)
     {
       err_location(f_op);
-      error() << "sign expects one operand" << eom;
+      error() << identifier << " expects one operand" << eom;
       throw 0;
     }
 
     sign_exprt sign_expr(expr.arguments().front());
     sign_expr.add_source_location()=source_location;
 
-    return sign_expr;
+    return typecast_exprt::conditional_cast(sign_expr, expr.type());
   }
   else if(identifier=="__builtin_popcount" ||
           identifier=="__builtin_popcountl" ||

src/util/std_expr.h

@@ -2111,6 +2111,15 @@ class typecast_exprt:public unary_exprt
     unary_exprt(ID_typecast, op, _type)
   {
   }
+
+  // returns a typecast if the type doesn't already match
+  static exprt conditional_cast(const exprt &expr, const typet &type)
+  {
+    if(expr.type() == type)
+      return expr;
+    else
+      return typecast_exprt(expr, type);
+  }
 };
 
 /*! \brief Cast a generic exprt to a \ref typecast_exprt