Fix flatten2bv abort on non-constant FPA float (#9101)#9102
Draft
kroening wants to merge 5 commits into
Draft
Conversation
kroening
requested review from
TGWDB,
martin-cs,
peterschrammel and
tautschnig
as code owners
kroening
changed the title
The SMT2 export path aborts with an invariant violation when flatten2bv encounters a non-constant FPA-encoded float (e.g. a nondet float stored in a union and read back as unsigned). Add a minimal reproducer that exercises this code path via the classic union-based float-to-int type-punning idiom. The test is marked KNOWNBUG because the export currently aborts (SIGABRT) instead of producing a complete SMT2 formula.
When flatten2bv encounters a non-constant floatbv expression under FPA theory (e.g. a nondet float stored in a union), it now emits the same bvfromfloat round-trip that find_symbols already uses for explicit typecast(floatbv→bv): declare a fresh BV variable and assert that ((_ to_fp E S) bv) equals the float expression. Previously this hit an UNEXPECTEDCASE invariant violation, aborting the SMT2 export mid-write and leaving a truncated output file. The regression test is promoted from KNOWNBUG to CORE.
kroening
force-pushed
the
kroening/issue-9101-knownbug-test
branch
from
481d85e to
3693209
Compare
The test explicitly controls the output format (--smt2 --fpa --outfile -) and must not be re-run with a different solver backend appended. Add broken-smt-backend and no-new-smt tags, matching the convention used by other --outfile tests (e.g. array_of_bool_as_bitvec/test-smt2-outfile.desc).
Tests using --outfile - dump raw SMT2 to stdout, which is not valid XML. Add the new test to the exclusion list in validate-trace-xml-schema/check.py, matching the existing exclusions for array_of_bool_as_bitvec and others.
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9102 +/- ##
===========================================
+ Coverage 80.77% 80.79% +0.01%
===========================================
Files 1712 1712
Lines 189814 189830 +16
Branches 73 73
===========================================
+ Hits 153324 153364 +40
+ Misses 36490 36466 -24 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
The bvfromfloat auxiliary (declare-fun + assert) must be emitted at the SMT-LIB top level, not inline during expression conversion. Move the declaration logic into find_symbols, which runs before any expression output. find_symbols now pre-creates a bvfromfloat entry for every non-constant floatbv-typed expression it visits under FPA theory. flatten2bv then simply looks up the existing entry by its defined_expressions key (a synthetic typecast_exprt from floatbv to bv).
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
1 participant
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.
Closes #9101
Problem
--smt2 --fpa --outfileaborts with an invariant violation (flatten2bv of a non-constant FPA-encoded float is unsupported) when the program reinterprets the bits of a non-constant float through a union — the classicunion { float f; unsigned u; }idiom pervasive in bit-exact libm code. The native SAT backend solves the same program without issue.Root cause
The union
with_exprthandling inconvert_expr(andconvert_union) callsflatten2bv(value)directly on a float-typed value. Under FPA theory,flatten2bvonly handled constant floats (emitting their IEEE-754 bit pattern as a literal BV). Non-constant floats need thebvfromfloatround-trip — declare a fresh BV variable and assert((_ to_fp E S) bv) == float— but this was only wired up for explicittypecast_exprt(floatbv→bv)infind_symbols.Fix
Extend the non-constant branch of
flatten2bvto emit the samebvfromfloatround-trip inline, usingdefined_expressionswith a synthetictypecast_exprtas cache key for deduplication (consistent with the existingfind_symbolsmechanism).Testing
regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/exercises the exact reproducer from--smt2 --outfileaborts (flatten2bv: unsupported) on float↔int type-punning that native solving handles #9101 (nondet float through union,--smt2 --fpa --outfile -).union-double-bits-fpaandunion-bits-double-fpatests continue to pass.