Fix --nan-check false positive for finite/+INFINITY division

regression/cbmc/float-finite-div-infinity/main.c

@@ -0,0 +1,49 @@
+// Test case for bug fix: finite / +INFINITY should NOT trigger --nan-check
+// According to IEEE 754-2019 Section 6.1: "division(x, ∞) for finite x"
+// should produce 0.0, not NaN. Hence, none of the operations below should
+// trigger nan-check assertions.
+
+#include <assert.h>
+#include <math.h>
+#include <stdint.h>
+
+union float_bits
+{
+  uint32_t u;
+  float f;
+};
+
+int main(void)
+{
+  // Test case 1: Using union to create +INFINITY as mentioned in the bug report
+  union float_bits a, b;
+  a.u = 1065353216; // 1.0
+  b.u = 2139095040; // +INF
+
+  // This should produce 0.0, not NaN - should NOT trigger nan-check failure
+  float result1 = a.f / b.f;
+  assert(fpclassify(result1) == FP_ZERO && !signbit(result1));
+
+  // Test case 2: Direct assignment as mentioned in the bug report
+  float x = 1.0f;
+  float y = INFINITY;
+  float result2 = x / y;
+  assert(fpclassify(result2) == FP_ZERO && !signbit(result2));
+
+  // Test case 3: Negative finite / infinity should also be 0.0 (negative zero)
+  float neg_x = -1.0f;
+  float result3 = neg_x / INFINITY;
+  assert(fpclassify(result3) == FP_ZERO && signbit(result3));
+
+  // Test case 4: Various finite values divided by infinity
+  float nd_positive = __VERIFIER_nondet_float();
+  __CPROVER_assume(isfinite(nd_positive) && nd_positive > 0);
+  float result4 = nd_positive / INFINITY;
+  assert(fpclassify(result4) == FP_ZERO && !signbit(result4));
+  float nd_negative = __VERIFIER_nondet_float();
+  __CPROVER_assume(isfinite(nd_negative) && nd_negative < 0);
+  float result5 = nd_negative / INFINITY;
+  assert(fpclassify(result5) == FP_ZERO && signbit(result5));
+
+  return 0;
+}

regression/cbmc/float-finite-div-infinity/test.desc

@@ -0,0 +1,12 @@
+CORE no-new-smt broken-cprover-smt-backend
+main.c
+--nan-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This test verifies that dividing a finite float by +INFINITY does NOT
+incorrectly trigger a NaN check failure (bug fix). According to IEEE 754-2019
+Section 6.1, division(x, ∞) for finite x = 0.0. Only inf/inf should produce NaN
+(which is covered in test float-inf-div-inf)

regression/cbmc/float-inf-div-inf/main.c

@@ -0,0 +1,28 @@
+// Test case for bug fix: inf / inf SHOULD trigger --nan-check failure
+// According to IEEE 754-2019, inf/inf produces NaN
+
+#include <assert.h>
+#include <math.h>
+
+int main(void)
+{
+  // Ensure infinity / infinity produces NaN and triggers nan-check
+  float inf1 = INFINITY;
+  float inf2 = INFINITY;
+  float result1 = inf1 / inf2; // Should trigger NaN check
+  assert(isnan(result1));
+
+  // Also test -inf / inf
+  float result2 = (-INFINITY) / INFINITY; // Should trigger NaN check
+  assert(isnan(result2));
+
+  // And inf / -inf
+  float result3 = INFINITY / (-INFINITY); // Should trigger NaN check
+  assert(isnan(result3));
+
+  // And -inf / -inf
+  float result4 = (-INFINITY) / (-INFINITY); // Should trigger NaN check
+  assert(isnan(result4));
+
+  return 0;
+}

regression/cbmc/float-inf-div-inf/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--nan-check
+\[main.NaN.1\] line \d+ NaN on / in inf1 / inf2: FAILURE
+\[main.NaN.2\] line \d+ NaN on / in -(\+INFINITY|return_value___builtin_(huge_val|inf)f\$\d+|\(\(float\)1\.000000e\+300\)) / (\+INFINITY|return_value___builtin_(huge_val|inf)f\$\d+|\(float\)1\.000000e\+300): FAILURE
+\[main.NaN.3\] line \d+ NaN on / in (\+INFINITY|return_value___builtin_(huge_val|inf)f\$\d+|\(float\)1\.000000e\+300) / -(\+INFINITY|return_value___builtin_(huge_val|inf)f\$\d+|\(\(float\)1\.000000e\+300\)): FAILURE
+\[main.NaN.4\] line \d+ NaN on / in -(\+INFINITY|return_value___builtin_(huge_val|inf)f\$\d+|\(\(float\)1\.000000e\+300\)) / -(\+INFINITY|return_value___builtin_(huge_val|inf)f\$\d+|\(\(float\)1\.000000e\+300\)): FAILURE
+^\*\* 4 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test verifies that inf/inf correctly triggers NaN check failures.
+According to IEEE 754-2019, inf/inf = NaN.

regression/cbmc/float-nan-check/main.c

@@ -39,8 +39,8 @@ int main(void)
   // these operations should generate assertions
   // 0.0 / 0.0 = NaN
   f = myzero / myzero;
-  // n / Inf = NaN
-  f = n / (myinf);
+  // Inf / Inf = NaN (per IEEE 754-2019 Section 6.1)
+  f = myinf / myinf;
   // Inf * 0 = NaN
   f = (myinf)*myzero;
   // -Inf + Inf = NaN

regression/cbmc/float-nan-check/test.desc

@@ -3,7 +3,7 @@ main.c
 --nan-check
 \[main.NaN.1\] line \d+ NaN on \+ in byte_extract_(big|little)_endian\(c, (0|0l|0ll), float\) \+ myzero: SUCCESS
 \[main.NaN.2\] line \d+ NaN on / in myzero / myzero: FAILURE
-\[main.NaN.3\] line \d+ NaN on / in \(float\)n / myinf: FAILURE
+\[main.NaN.3\] line \d+ NaN on / in myinf / myinf: FAILURE
 \[main.NaN.4\] line \d+ NaN on \* in myinf \* myzero: FAILURE
 \[main.NaN.5\] line \d+ NaN on \+ in -myinf \+ myinf: FAILURE
 \[main.NaN.6\] line \d+ NaN on \+ in myinf \+ -myinf: FAILURE

regression/smt2_solver/fp/fp-isNegative1.desc

@@ -0,0 +1,7 @@
+CORE
+fp-isNegative1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

regression/smt2_solver/fp/fp-isNegative1.smt2

@@ -0,0 +1,11 @@
+(set-logic FP)
+
+; positive number
+(define-fun pos () Float32 (fp #b0 #b10000000 #b00000000000000000000000))
+
+; negative number
+(define-fun neg () Float32 (fp #b1 #b10000000 #b00000000000000000000000))
+
+; fp.isNegative should be true for neg, false for pos
+(assert (not (fp.isNegative neg)))
+(check-sat)

regression/smt2_solver/fp/fp-isPositive1.desc

@@ -0,0 +1,7 @@
+CORE
+fp-isPositive1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

regression/smt2_solver/fp/fp-isPositive1.smt2

@@ -0,0 +1,11 @@
+(set-logic FP)
+
+; positive number
+(define-fun pos () Float32 (fp #b0 #b10000000 #b00000000000000000000000))
+
+; negative number
+(define-fun neg () Float32 (fp #b1 #b10000000 #b00000000000000000000000))
+
+; fp.isPositive should be true for pos, false for neg
+(assert (not (fp.isPositive pos)))
+(check-sat)

src/ansi-c/c_typecheck_expr.cpp

@@ -3247,9 +3247,11 @@ 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")
   {
     if(expr.arguments().size()!=1)
     {

src/ansi-c/goto-conversion/goto_check_c.cpp

@@ -1254,18 +1254,20 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
   {
     const auto &div_expr = to_div_expr(expr);
 
-    // there a two ways to get a new NaN on division:
-    // 0/0 = NaN and x/inf = NaN
+    // there are two ways to get a new NaN on division:
+    // 0/0 = NaN and inf/inf = NaN
     // (note that x/0 = +-inf for x!=0 and x!=inf)
-    const and_exprt zero_div_zero(
+    // (note that finite/inf = +-0.0, NOT NaN per IEEE 754-2019 Section 6.1)
+    and_exprt zero_div_zero(
       ieee_float_equal_exprt(
         div_expr.op0(), from_integer(0, div_expr.dividend().type())),
       ieee_float_equal_exprt(
         div_expr.op1(), from_integer(0, div_expr.divisor().type())));
 
-    const isinf_exprt div_inf(div_expr.op1());
+    and_exprt inf_div_inf{
+      isinf_exprt{div_expr.op0()}, isinf_exprt{div_expr.op1()}};
 
-    isnan = or_exprt(zero_div_zero, div_inf);
+    isnan = or_exprt{std::move(zero_div_zero), std::move(inf_div_inf)};
   }
   else if(expr.id() == ID_mult)
   {

src/ansi-c/library/math.c

@@ -112,6 +112,27 @@ int __finitef(float f) { return __CPROVER_isfinitef(f); }
 
 int __finitel(long double ld) { return __CPROVER_isfiniteld(ld); }
 
+/* FUNCTION: __isfinite */
+
+int __isfinite(double d)
+{
+  return __CPROVER_isfinited(d);
+}
+
+/* FUNCTION: __isfinitef */
+
+int __isfinitef(float f)
+{
+  return __CPROVER_isfinitef(f);
+}
+
+/* FUNCTION: __isfinitel */
+
+int __isfinitel(long double ld)
+{
+  return __CPROVER_isfiniteld(ld);
+}
+
 /* FUNCTION: isinf */
 
 #undef isinf

src/ansi-c/library_check.sh

@@ -65,6 +65,7 @@ perl -p -i -e 's/^__CPROVER_(tolower|toupper)\n//' __functions # tolower, touppe
 perl -p -i -e 's/^(creat|fcntl|open|openat)64\n//' __functions # same as creat, fcntl, open, openat
 perl -p -i -e 's/^__CPROVER_deallocate\n//' __functions # free-01
 perl -p -i -e 's/^__builtin_alloca\n//' __functions # alloca-01
+perl -p -i -e 's/^__isfinite[fl]?\n//' __functions # isfinite
 perl -p -i -e 's/^fclose_cleanup\n//' __functions # fopen
 perl -p -i -e 's/^fopen64\n//' __functions # fopen
 perl -p -i -e 's/^freopen64\n//' __functions # freopen

src/solvers/smt2/smt2_parser.cpp

@@ -1369,6 +1369,32 @@ void smt2_parsert::setup_expressions()
     return not_exprt(typecast_exprt(op[0], bool_typet()));
   };
 
+  expressions["fp.isNegative"] = [this]
+  {
+    auto op = operands();
+
+    if(op.size() != 1)
+      throw error("fp.isNegative takes one operand");
+
+    if(op[0].type().id() != ID_floatbv)
+      throw error("fp.isNegative takes FloatingPoint operand");
+
+    return sign_exprt{op[0]};
+  };
+
+  expressions["fp.isPositive"] = [this]
+  {
+    auto op = operands();
+
+    if(op.size() != 1)
+      throw error("fp.isPositive takes one operand");
+
+    if(op[0].type().id() != ID_floatbv)
+      throw error("fp.isPositive takes FloatingPoint operand");
+
+    return not_exprt{sign_exprt{op[0]}};
+  };
+
   expressions["fp"] = [this] { return function_application_fp(operands()); };
 
   expressions["fp.add"] = [this] {

src/util/ieee_float.cpp

@@ -1051,7 +1051,7 @@ ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)
     return *this;
   }
 
-  // x/inf = NaN
+  // inf/inf = NaN, x/inf = 0 for finite x
   if(other.infinity_flag)
   {
     if(infinity_flag)