Implement fixedbv/floatbv conversions in SAT and SMT2 back-ends#8790
Open
tautschnig wants to merge 1 commit intodiffblue:developfrom
Open
Implement fixedbv/floatbv conversions in SAT and SMT2 back-ends#8790tautschnig wants to merge 1 commit intodiffblue:developfrom
tautschnig wants to merge 1 commit intodiffblue:developfrom
Conversation
Implements bidirectional conversions between fixed-point numbers (fixedbv) and floating-point numbers (floatbv) for the SAT and SMT2 solver back-ends. SAT back-end (boolbv_typecast.cpp): - fixedbv to floatbv: treat the fixedbv as a signed integer, convert to float via from_signed_integer, then divide by 2^fraction_bits. - floatbv to fixedbv: multiply the float by 2^fraction_bits, then convert to signed integer via to_signed_integer with round-to-zero rounding mode (matching C truncation semantics). SMT2 back-end (smt2_conv.cpp): - fixedbv to floatbv: use ((_ to_fp e s) RNE bv) to convert the signed integer representation to float, then fp.div by 2^fraction_bits. - floatbv to fixedbv: use fp.mul to scale by 2^fraction_bits, then fp.to_sbv to convert to signed integer. Fixes: diffblue#2158 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
fix-2158-fixedbv-floatbv
branch
from
bbba069 to
2198f01
Compare
tautschnig
requested review from
TGWDB,
kroening,
martin-cs and
peterschrammel
as code owners
There was a problem hiding this comment.
Pull request overview
Adds support for converting between fixed-point bitvectors (fixedbv) and floating-point bitvectors (floatbv) across the SAT (bit-blasting) and SMT2 back-ends, along with regression coverage for common conversion patterns.
Changes:
- Implement
fixedbv <-> floatbvconversions in the SMT2 typecast converter (FPA-theory path). - Implement
fixedbv <-> floatbvconversions in the SAT/bit-blasting type conversion logic. - Add multiple CBMC regression tests covering cast and round-trip scenarios (including SMT2 runs).
Reviewed changes
Copilot reviewed 24 out of 24 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
| src/solvers/smt2/smt2_conv.cpp | Adds SMT2 emission for floatbv->fixedbv and fixedbv->floatbv casts (with FPA-theory support; non-FPA path currently TODO). |
| src/solvers/flattening/boolbv_typecast.cpp | Adds bit-blasting conversions for fixedbv->floatbv and floatbv->fixedbv using float_utilst. |
| regression/cbmc/Float-to-fixedbv1/test.desc | New regression test runner for float→fixedbv conversions. |
| regression/cbmc/Float-to-fixedbv1/main.c | New float→fixedbv conversion assertions (plus NaN/Inf smoke coverage). |
| regression/cbmc/Float-to-fixedbv-smt2/test.desc | New regression test runner for float→fixedbv with SMT2 backend. |
| regression/cbmc/Float-to-fixedbv-smt2/main.c | New float→fixedbv assertions for SMT2 backend. |
| regression/cbmc/Float-to-fixedbv-overflow/test.desc | New regression test runner for overflow-ish float→fixedbv scenarios. |
| regression/cbmc/Float-to-fixedbv-overflow/main.c | New float→fixedbv overflow/edge scenario checks (mostly smoke for Inf/NaN). |
| regression/cbmc/Fixedbv-to-float1/test.desc | New regression test runner for fixedbv→float conversions. |
| regression/cbmc/Fixedbv-to-float1/main.c | New fixedbv→float conversion assertions. |
| regression/cbmc/Fixedbv-to-float-smt2/test.desc | New regression test runner for fixedbv→float using --cprover-smt2. |
| regression/cbmc/Fixedbv-to-float-smt2/main.c | New fixedbv→float assertions for SMT2 backend. |
| regression/cbmc/Fixedbv-to-double1/test.desc | New regression test runner for fixedbv→double conversions. |
| regression/cbmc/Fixedbv-to-double1/main.c | New fixedbv→double conversion assertions. |
| regression/cbmc/Fixedbv-float-roundtrip/test.desc | New regression test runner for fixedbv/float round-trips. |
| regression/cbmc/Fixedbv-float-roundtrip/main.c | New round-trip assertions across fixedbv↔float casts. |
| regression/cbmc/Fixedbv-float-precisions/test.desc | New regression test runner for varying fixedbv precisions. |
| regression/cbmc/Fixedbv-float-precisions/main.c | New precision-variation conversion assertions. |
| regression/cbmc/Fixedbv-float-edge-cases/test.desc | New regression test runner for edge-case casts. |
| regression/cbmc/Fixedbv-float-edge-cases/main.c | New edge-case fixedbv/float conversion assertions. |
| regression/cbmc/Fixedbv-float-double1/test.desc | New regression test runner for mixed float/double conversions. |
| regression/cbmc/Fixedbv-float-double1/main.c | New mixed float/double cast + round-trip assertions. |
| regression/cbmc/Double-to-fixedbv1/test.desc | New regression test runner for double→fixedbv conversions. |
| regression/cbmc/Double-to-fixedbv1/main.c | New double→fixedbv conversion assertions (plus NaN/Inf smoke coverage). |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+3165
to
+3173
| // Multiply by scaling factor | ||
| out << "(let ((scaled_val (fp.mul RNE "; | ||
| convert_expr(src); | ||
| out << " "; | ||
| convert_constant(scale_float.to_expr()); | ||
| out << "))) "; | ||
|
|
||
| // Convert to signed bitvector | ||
| out << "(fp.to_sbv " << dest_width << " RNE scaled_val))"; |
Comment on lines
+3162
to
+3173
| ieee_floatt scale_float(src_floatbv_type, ieee_floatt::ROUND_TO_EVEN); | ||
| scale_float.from_integer(scale_factor); | ||
|
|
||
| // Multiply by scaling factor | ||
| out << "(let ((scaled_val (fp.mul RNE "; | ||
| convert_expr(src); | ||
| out << " "; | ||
| convert_constant(scale_float.to_expr()); | ||
| out << "))) "; | ||
|
|
||
| // Convert to signed bitvector | ||
| out << "(fp.to_sbv " << dest_width << " RNE scaled_val))"; |
Comment on lines
+3177
to
+3197
| // Without FPA theory, we work with the bit-level representation | ||
| // This is more complex and requires manual handling | ||
| // For now, we'll use a simplified approach treating it as bit manipulation | ||
|
|
||
| // Get the float as bitvector | ||
| out << "(let ((float_bv "; | ||
| convert_expr(src); | ||
| out << ")) "; | ||
|
|
||
| // Create scale factor as bitvector representation of float | ||
| mp_integer scale_factor = | ||
| power(mp_integer(2), mp_integer(dest_fraction_bits)); | ||
| ieee_floatt scale_float( | ||
| to_floatbv_type(src_type), ieee_floatt::ROUND_TO_EVEN); | ||
| scale_float.from_integer(scale_factor); | ||
|
|
||
| // This is a placeholder - proper implementation would need float arithmetic | ||
| // For bit-level representation without FPA, we'd need to implement | ||
| // float multiplication and conversion manually | ||
| SMT2_TODO("floatbv to fixedbv conversion without FPA theory"); | ||
| out << "(_ bv0 " << dest_width << "))"; // Close let |
Comment on lines
+3346
to
+3355
| else | ||
| { | ||
| // Without FPA theory, use bit-level representation | ||
| // This is complex - would need manual float construction | ||
| // For now, provide a placeholder | ||
| SMT2_TODO("fixedbv to floatbv conversion without FPA theory"); | ||
|
|
||
| // At minimum, output something valid | ||
| out << "(_ bv0 " << dest_floatbv_type.get_width() << ")"; | ||
| } |
Comment on lines
+46
to
+50
| // Test float to fixedbv with truncation | ||
| float f_trunc = 3.9999f; | ||
| fixedbv_t fixed_trunc = (fixedbv_t)f_trunc; | ||
| assert(fixed_trunc > (fixedbv_t)3.99 && fixed_trunc < (fixedbv_t)4.01); | ||
|
|
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.
Implements bidirectional conversions between fixed-point numbers (
fixedbv) and floating-point numbers (floatbv) for the SAT and SMT2 solver back-ends.Fixes: #2158