Align floating-point predicates across float_utilst and float_bvt

regression/cbmc-library/__builtin_finite/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  __builtin_finite();
+  assert(0);
+  return 0;
+}

regression/cbmc-library/__builtin_finite/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-library/__builtin_finitef/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  __builtin_finitef();
+  assert(0);
+  return 0;
+}

regression/cbmc-library/__builtin_finitef/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-library/__builtin_finitel/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  __builtin_finitel();
+  assert(0);
+  return 0;
+}

regression/cbmc-library/__builtin_finitel/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-library/__builtin_isfinite/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  __builtin_isfinite();
+  assert(0);
+  return 0;
+}

regression/cbmc-library/__builtin_isfinite/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--pointer-check --bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/Float-predicates/main.c

@@ -0,0 +1,28 @@
+// Test floating-point classification predicates: isfinite, isinf (signed).
+
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  float pos_inf = 1.0f / 0.0f;
+  float neg_inf = -1.0f / 0.0f;
+  float nan_val = 0.0f / 0.0f;
+  float normal = 1.5f;
+  float zero = 0.0f;
+
+  // isfinite
+  assert(isfinite(normal));
+  assert(isfinite(zero));
+  assert(!isfinite(pos_inf));
+  assert(!isfinite(neg_inf));
+  assert(!isfinite(nan_val));
+
+  // isinf with sign
+  assert(isinf(pos_inf) && pos_inf > 0);
+  assert(isinf(neg_inf) && neg_inf < 0);
+  assert(!isinf(normal));
+  assert(!isinf(nan_val));
+
+  return 0;
+}

regression/cbmc/Float-predicates/test.desc

@@ -0,0 +1,10 @@
+CORE no-new-smt
+main.c
+--floatbv
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Floating-point classification predicates.

regression/cbmc/Float-predicates/test_smt.desc

@@ -0,0 +1,10 @@
+CORE smt-backend no-new-smt
+main.c
+--smt2 --z3
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Floating-point classification predicates (SMT path).

src/ansi-c/c_typecheck_expr.cpp

@@ -3246,9 +3246,12 @@ exprt c_typecheck_baset::do_special_functions(
 
     return typecast_exprt::conditional_cast(isnan_expr, expr.type());
   }
-  else if(identifier==CPROVER_PREFIX "isfinitef" ||
-          identifier==CPROVER_PREFIX "isfinited" ||
-          identifier==CPROVER_PREFIX "isfiniteld")
+  else if(
+    identifier == CPROVER_PREFIX "isfinitef" ||
+    identifier == CPROVER_PREFIX "isfinited" ||
+    identifier == CPROVER_PREFIX "isfiniteld" ||
+    identifier == "__builtin_isfinite" || identifier == "__builtin_finite" ||
+    identifier == "__builtin_finitef" || identifier == "__builtin_finitel")
   {
     if(expr.arguments().size()!=1)
     {

src/ansi-c/library/math.c

@@ -251,6 +251,34 @@ int __builtin_isnanf(float f)
   return __CPROVER_isnanf(f);
 }
 
+/* FUNCTION: __builtin_isfinite */
+
+int __builtin_isfinite(double d)
+{
+  return __CPROVER_isfinited(d);
+}
+
+/* FUNCTION: __builtin_finite */
+
+int __builtin_finite(double d)
+{
+  return __CPROVER_isfinited(d);
+}
+
+/* FUNCTION: __builtin_finitef */
+
+int __builtin_finitef(float f)
+{
+  return __CPROVER_isfinitef(f);
+}
+
+/* FUNCTION: __builtin_finitel */
+
+int __builtin_finitel(long double ld)
+{
+  return __CPROVER_isfiniteld(ld);
+}
+
 /* FUNCTION: __builtin_huge_valf */
 
 float __builtin_huge_valf(void)

src/solvers/flattening/boolbv.cpp

@@ -457,11 +457,9 @@ literalt boolbvt::convert_rest(const exprt &expr)
     if(op.type().id() == ID_floatbv)
     {
       float_utilst float_utils(prop, to_floatbv_type(op.type()));
-      return prop.land(
-        !float_utils.is_infinity(bv),
-        !float_utils.is_NaN(bv));
+      return float_utils.is_finite(bv);
     }
-    else if(op.id() == ID_fixedbv)
+    else if(op.type().id() == ID_fixedbv)
       return const_literal(true);
   }
   else if(expr.id()==ID_isinf)

src/solvers/floatbv/float_utils.cpp

@@ -813,15 +813,6 @@ literalt float_utilst::is_zero(const bvt &src)
   return bv_utils.is_zero(all_but_sign);
 }
 
-literalt float_utilst::is_plus_inf(const bvt &src)
-{
-  bvt and_bv;
-  and_bv.push_back(!sign_bit(src));
-  and_bv.push_back(exponent_all_ones(src));
-  and_bv.push_back(fraction_all_zeros(src));
-  return prop.land(and_bv);
-}
-
 literalt float_utilst::is_infinity(const bvt &src)
 {
   return prop.land(
@@ -841,21 +832,17 @@ bvt float_utilst::get_fraction(const bvt &src)
   return bv_utils.extract(src, 0, spec.f-1);
 }
 
-literalt float_utilst::is_minus_inf(const bvt &src)
-{
-  bvt and_bv;
-  and_bv.push_back(sign_bit(src));
-  and_bv.push_back(exponent_all_ones(src));
-  and_bv.push_back(fraction_all_zeros(src));
-  return prop.land(and_bv);
-}
-
 literalt float_utilst::is_NaN(const bvt &src)
 {
   return prop.land(exponent_all_ones(src),
                    !fraction_all_zeros(src));
 }
 
+literalt float_utilst::is_finite(const bvt &src)
+{
+  return !exponent_all_ones(src);
+}
+
 literalt float_utilst::exponent_all_ones(const bvt &src)
 {
   bvt exponent=src;

src/solvers/floatbv/float_utils.h

@@ -107,9 +107,9 @@ class float_utilst
   literalt is_normal(const bvt &);
   literalt is_zero(const bvt &); // this returns true on both 0 and -0
   literalt is_infinity(const bvt &);
-  literalt is_plus_inf(const bvt &);
-  literalt is_minus_inf(const bvt &);
   literalt is_NaN(const bvt &);
+  /// Returns true iff \p src is finite (not NaN and not infinity).
+  literalt is_finite(const bvt &);
 
   // add/sub
   virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract);