Align floating-point predicates across float_utilst and float_bvt#8988
Open
tautschnig wants to merge 3 commits into
Open
Align floating-point predicates across float_utilst and float_bvt#8988tautschnig wants to merge 3 commits into
tautschnig wants to merge 3 commits into
Conversation
tautschnig
requested review from
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
This PR aligns floating-point classification predicates between float_utilst and other float encodings by introducing a shared is_finite helper, simplifying predicate conversion, and adding regressions to cover the updated behavior (bitvector and SMT paths).
Changes:
- Add
float_utilst::is_finiteand remove unusedis_plus_inf/is_minus_inf. - Simplify
ID_isfiniteconversion inboolbvtto use the new helper. - Add new regressions for
isfiniteandisinf(floatbv and SMT/Z3 paths).
Reviewed changes
Copilot reviewed 6 out of 6 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
src/solvers/floatbv/float_utils.h |
Removes unused infinity-sign helpers; declares new is_finite predicate. |
src/solvers/floatbv/float_utils.cpp |
Implements float_utilst::is_finite and deletes unused helpers. |
src/solvers/flattening/boolbv.cpp |
Refactors ID_isfinite conversion to call float_utilst::is_finite. |
regression/cbmc/Float-predicates/test.desc |
Adds floatbv regression for classification predicates. |
regression/cbmc/Float-predicates/test_smt.desc |
Adds SMT/Z3 regression for classification predicates. |
regression/cbmc/Float-predicates/main.c |
Test program exercising isfinite and isinf (with sign checks). |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| @@ -0,0 +1,10 @@ | |||
| CORE no-new-smt | |||
There was a problem hiding this comment.
This test runs CBMC with --smt2 --z3 but isn't labeled smt-backend. In regression/cbmc/CMakeLists.txt, the default regression profile excludes tests with the smt-backend label, so without it this test may run unexpectedly in default CI (and require Z3). Add smt-backend to the label line (e.g., CORE smt-backend no-new-smt).
Suggested change
| CORE no-new-smt | |
| CORE smt-backend no-new-smt |
| !float_utils.is_NaN(bv)); | ||
| return float_utils.is_finite(bv); | ||
| } | ||
| else if(op.id() == ID_fixedbv) |
There was a problem hiding this comment.
The fixedbv fast-path is checking op.id() == ID_fixedbv, but ID_fixedbv is a type id (and the surrounding isnan/isinf/isnormal branches use op.type().id()). As written, this branch will never match and ID_isfinite on fixedbv will fall through to SUB::convert_rest, likely producing an unexpected result or conversion failure. Use op.type().id() == ID_fixedbv here for consistency with the other predicates.
Suggested change
| else if(op.id() == ID_fixedbv) | |
| else if(op.type().id() == ID_fixedbv) |
GCC's <math.h> macros expand isfinite(x) to __builtin_isfinite(x),
yet c_typecheck_expr.cpp only recognised the __CPROVER_-prefixed
helpers (__CPROVER_isfinite{f,d,ld}). As a result, on glibc systems
where isfinite() goes through __builtin_isfinite, CBMC failed to
lower the call to an isfinite_exprt and instead treated the call as
a body-less function. Symptoms include a 'no body for callee
__builtin_isfinite' warning and havocked nondet results that make
assert(isfinite(...)) fail.
Aligns with the existing handling of __builtin_isnan,
__builtin_isinf, __builtin_isinf_sign, and __builtin_isnormal.
Add the missing identifiers to the isfinite_exprt branch of
c_typecheck_expr.cpp:
__builtin_isfinite (modern variant)
__builtin_finite (older glibc internal alias)
__builtin_finitef (float variant)
__builtin_finitel (long double variant)
Also add fallback library bodies in library/math.c so that indirect
calls (function pointers etc.) resolve correctly, mirroring the
existing __builtin_isnan{,f} entries.
Stub regression/cbmc-library/ test directories accompany each new
library entry, as required by library_check.sh.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The ID_isfinite branch in boolbvt::convert_rest tested 'op.id() == ID_fixedbv', but ID_fixedbv is a *type* id and op is the operand expression, not a type. The dead branch never matched and fixedbv operands fell through to SUB::convert_rest, which is not prepared to lower an isfinite expression and would yield an unexpected result or conversion failure. The neighbouring ID_isnan, ID_isinf, and ID_isnormal branches all correctly use 'op.type().id() == ID_fixedbv'. Bring ID_isfinite into line. Pre-existing typo, unrelated to the surrounding refactoring; fixed here because it sits in the immediate neighbourhood of changes to the floatbv branch and to keep the fixedbv handling consistent. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
- Add float_utilst::is_finite and use it (float_bvt already has is_finite). - Remove unused float_utilst::is_plus_inf, float_utilst::is_minus_inf (float_bvt does not have these either). - Switch the ID_isfinite floatbv branch in boolbvt::convert_rest to the new helper. Add a regression/cbmc/Float-predicates test exercising isfinite and isinf via <math.h> against both the default SAT and the SMT (Z3) backends. Tagging the SMT test with smt-backend keeps it out of the default and paths-lifo profiles, matching the convention used by other tests that hard-code --smt2 --z3. Tests targeting predicates continue to pass. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
float-predicates
branch
from
dc3f9dc to
f1cae3d
Compare
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## develop #8988 +/- ##
========================================
Coverage 80.60% 80.60%
========================================
Files 1711 1711
Lines 189454 189445 -9
Branches 73 73
========================================
- Hits 152712 152705 -7
+ Misses 36742 36740 -2 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Depends-on: #9020
Tests targeting predicates continue to pass.