diff --git a/regression/cbmc/union-double-bits-fpa/main.c b/regression/cbmc/union-double-bits-fpa/main.c new file mode 100644 index 00000000000..2f8ed8668dc --- /dev/null +++ b/regression/cbmc/union-double-bits-fpa/main.c @@ -0,0 +1,35 @@ +#include + +// Exercises smt2_convt::flatten2bv on an FPA-encoded `double`: reading the +// bytes of a double through a union forces the SMT2 back-end to turn the +// floating-point value into its IEEE-754 interchange bit pattern. The +// SMT-LIB FloatingPoint theory has no operator for that bit pattern +// (fp.to_ubv / fp.to_sbv are value conversions, not a bit-pattern +// reinterpret), so before this was supported the cprover-smt2 / FPA path +// hit an invariant here. `--no-simplify` keeps the constant from being +// folded away before it reaches the back-end, so the flattening code is +// actually exercised. +// +// The check is meaningful primarily under the cprover-smt2 profile (FPA +// theory); under the SAT back-end the value is bit-vector-encoded anyway, +// in which case the assertions simply hold. + +int main(void) +{ + union + { + double d; + uint64_t bits; + } u; + + u.d = 1.0; + __CPROVER_assert(u.bits == 0x3FF0000000000000ull, "IEEE-754 bits of 1.0"); + + u.d = -2.0; + __CPROVER_assert(u.bits == 0xC000000000000000ull, "IEEE-754 bits of -2.0"); + + u.d = 0.0; + __CPROVER_assert(u.bits == 0x0000000000000000ull, "IEEE-754 bits of 0.0"); + + return 0; +} diff --git a/regression/cbmc/union-double-bits-fpa/test.desc b/regression/cbmc/union-double-bits-fpa/test.desc new file mode 100644 index 00000000000..7ed696b63bc --- /dev/null +++ b/regression/cbmc/union-double-bits-fpa/test.desc @@ -0,0 +1,35 @@ +CORE broken-cprover-smt-backend +main.c +--floatbv --no-simplify +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +End-to-end documentation of the user-visible scenario that motivated +the new `flatten2bv` handling: reading the IEEE-754 bit pattern of +an FPA-encoded `double` through a union. The SMT-LIB FloatingPoint +theory has no operator for that bit pattern (fp.to_ubv / fp.to_sbv are +value conversions, not a bit-pattern reinterpret), so under FPA the +cprover-smt2 / `--smt2 --fpa` path previously hit an invariant here. + +`--no-simplify` keeps the constant union read from being folded +away before it reaches the SMT2 back-end. `double` is IEEE +binary64 on every supported target, so no architecture pinning is +needed. + +The test is tagged `broken-cprover-smt-backend` because CPROVER's +in-tree SMT2 solver does not fully support the SMT-LIB +FloatingPoint theory beyond constant folding: even with the new +flatten2bv path it returns "ERROR" on assertions involving +FPA-encoded values, which is a solver-side limitation. Under the +SAT and incremental-SMT2 (z3) CI profiles `use_FPA_theory` is +false, so the new code path is not exercised by this regression +test in CI; that coverage lives in `unit/solvers/smt2/smt2_conv.cpp` +(the "flatten2bv FPA-encoded float constant" test case), which drives +`flatten2bv` directly with `use_FPA_theory == true` and aborts +without the fix. This regression test still passes under the SAT +and incremental-SMT2 (z3) profiles via the bv-encoded path, and +has been confirmed manually under `--z3 --fpa` to be +solver-compatible. diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e7b9893a882..8d265ad8a72 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -5012,11 +5012,29 @@ void smt2_convt::flatten2bv(const exprt &expr) } else if(type.id()==ID_floatbv) { - INVARIANT( - !use_FPA_theory, - "floatbv expressions should be flattened when using FPA theory"); - - convert_expr(expr); + if(use_FPA_theory) + { + // A floatbv constant's IEEE-754 interchange bit pattern is exactly its + // bit-vector representation, so it is emitted as a literal bit-vector. + // This is the only shape that reaches flatten2bv under FPA: a + // non-constant float whose bits are read is lowered by + // lower_byte_operators into a float typecast, which is handled by the + // bvfromfloat round-trip in find_symbols and never reaches here. + if(expr.is_constant()) + { + const ieee_float_spect spec(to_floatbv_type(type)); + const mp_integer value = bvrep2integer( + to_constant_expr(expr).get_value(), spec.width(), false); + out << "(_ bv" << value << " " << spec.width() << ")"; + } + else + { + UNEXPECTEDCASE( + "flatten2bv of a non-constant FPA-encoded float is unsupported"); + } + } + else + convert_expr(expr); } else convert_expr(expr); diff --git a/unit/solvers/smt2/smt2_conv.cpp b/unit/solvers/smt2/smt2_conv.cpp index 3e7581d62d5..80ebbcffcad 100644 --- a/unit/solvers/smt2/smt2_conv.cpp +++ b/unit/solvers/smt2/smt2_conv.cpp @@ -6,6 +6,8 @@ #include #include #include +#include +#include #include #include #include @@ -156,3 +158,44 @@ TEST_CASE("smt2_convt range encoding", "[core][solvers][smt2]") } } } + +TEST_CASE( + "smt2_convt::flatten2bv FPA-encoded float constant", + "[core][solvers][smt2]") +{ + // Drive `flatten2bv` on a `floatbv` constant under a solver that + // enables the SMT-LIB FloatingPoint theory (use_FPA_theory == true). + // This pins the constant branch of the new flatten2bv handler: + // the constant's IEEE-754 interchange bit pattern is emitted as a + // bit-vector literal. Without the fix, the back-end aborts here + // with `INVARIANT(!use_FPA_theory, ...)`. + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + std::ostringstream out; + // CPROVER_SMT2 sets use_FPA_theory = true at construction time. + smt2_convt conv{ + ns, "test", "", "QF_AUFBV", smt2_convt::solvert::CPROVER_SMT2, out}; + + // double 1.0 -> 0x3FF0000000000000 = 4607182418800017408. + ieee_float_valuet f{ieee_float_spect::double_precision()}; + f.from_double(1.0); + const constant_exprt fp_const = f.to_expr(); + + // Place the constant in a single-member union so that the back-end + // takes a flat-of-float path: + // convert_typecast(union -> bv64) + // -> convert_expr(union_exprt) + // -> convert_union + // -> flatten2bv(float) <- exercises the new code + const union_typet u_type{ + {struct_union_typet::componentt{"d", fp_const.type()}}}; + const union_exprt u_expr{"d", fp_const, u_type}; + + const unsignedbv_typet u64{64}; + const constant_exprt expected = + from_integer(mp_integer{"4607182418800017408"}, u64); + + conv.set_to(equal_exprt{typecast_exprt{u_expr, u64}, expected}, true); + + REQUIRE(out.str().find("(_ bv4607182418800017408 64)") != std::string::npos); +}