diff --git a/regression/cbmc/float-finite-div-infinity/main.c b/regression/cbmc/float-finite-div-infinity/main.c new file mode 100644 index 00000000000..eca8189a4d0 --- /dev/null +++ b/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 +#include +#include + +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; +} diff --git a/regression/cbmc/float-finite-div-infinity/test.desc b/regression/cbmc/float-finite-div-infinity/test.desc new file mode 100644 index 00000000000..5b46e27c588 --- /dev/null +++ b/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) diff --git a/regression/cbmc/float-inf-div-inf/main.c b/regression/cbmc/float-inf-div-inf/main.c new file mode 100644 index 00000000000..c3738656e2b --- /dev/null +++ b/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 +#include + +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; +} diff --git a/regression/cbmc/float-inf-div-inf/test.desc b/regression/cbmc/float-inf-div-inf/test.desc new file mode 100644 index 00000000000..e7fffb4ca33 --- /dev/null +++ b/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. diff --git a/regression/cbmc/float-nan-check/main.c b/regression/cbmc/float-nan-check/main.c index 66d39556905..405b6971ee6 100644 --- a/regression/cbmc/float-nan-check/main.c +++ b/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 diff --git a/regression/cbmc/float-nan-check/test.desc b/regression/cbmc/float-nan-check/test.desc index 92033bd0a16..6a9a7437bd2 100644 --- a/regression/cbmc/float-nan-check/test.desc +++ b/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 diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index d2219a7a29a..5b083d75b14 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/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) { diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp index 68c04604a94..0fac945fcc6 100644 --- a/src/ansi-c/goto-conversion/goto_check_c.cpp +++ b/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) { diff --git a/src/ansi-c/library/math.c b/src/ansi-c/library/math.c index c8cf190fc8e..c4b08671267 100644 --- a/src/ansi-c/library/math.c +++ b/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 diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh index 9d973341585..51ab1d462a0 100755 --- a/src/ansi-c/library_check.sh +++ b/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 diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index f7952e56fb5..1363f1d5fe6 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/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] { diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp index 497a9558471..f966d9333dc 100644 --- a/src/util/ieee_float.cpp +++ b/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)