diff --git a/regression/cbmc/union-bits-double-fpa/main.c b/regression/cbmc/union-bits-double-fpa/main.c new file mode 100644 index 00000000000..ff90ff8ceb1 --- /dev/null +++ b/regression/cbmc/union-bits-double-fpa/main.c @@ -0,0 +1,39 @@ +#include + +// Inverse of regression/cbmc/union-double-bits-fpa: write the IEEE-754 +// bit pattern of a double into a union and then read the double field. +// Under `--cprover-smt2` this forces the SMT2 back-end to emit the +// single-operand bit-pattern overload of `to_fp` for the FP read of +// the union: +// +// ((_ to_fp 11 53) ) +// +// CPROVER's smt2 parser previously rejected this overload with +// "unexpected token in an expression"; the parser now recognises it +// and routes it through a bit-level reinterpret typecast. Without +// `--no-simplify` the constant union read would be folded away +// before reaching the back-end, so the parser entry is actually +// exercised. +// +// `double` is IEEE binary64 on every supported target, so no +// architecture pinning is needed. + +int main(void) +{ + union + { + double d; + uint64_t bits; + } u; + + u.bits = 0x3FF0000000000000ULL; + __CPROVER_assert(u.d == 1.0, "bit pattern 0x3FF0... reinterprets as 1.0"); + + u.bits = 0xC000000000000000ULL; + __CPROVER_assert(u.d == -2.0, "bit pattern 0xC000... reinterprets as -2.0"); + + u.bits = 0x0000000000000000ULL; + __CPROVER_assert(u.d == 0.0, "all-zero bits reinterpret as +0.0"); + + return 0; +} diff --git a/regression/cbmc/union-bits-double-fpa/test.desc b/regression/cbmc/union-bits-double-fpa/test.desc new file mode 100644 index 00000000000..244dcaa6071 --- /dev/null +++ b/regression/cbmc/union-bits-double-fpa/test.desc @@ -0,0 +1,33 @@ +CORE broken-cprover-smt-backend +main.c +--floatbv --no-simplify +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Reads a `double` via a union after writing its IEEE-754 bit pattern. +Under `--cprover-smt2` this forces the SMT2 back-end to emit the +single-operand bit-pattern overload of `to_fp`, which CPROVER's smt2 +parser previously rejected with "unexpected token in an expression"; +the parser fix in this commit accepts the overload and routes it +through a bit-level reinterpret typecast. + +`--no-simplify` keeps the constant union read from being folded +away before it reaches the SMT2 back-end, so the parser entry is +actually exercised on the `--cprover-smt2` path. + +The smt2_solver-level tests under regression/smt2_solver/fp/ +(bit-to-fp2, bit-to-fp3, bit-to-fp-bad-width) directly cover the +parser entry under every CI profile. This test additionally pins +down the user-visible end-to-end scenario the PR exists to fix. + +The test is tagged `broken-cprover-smt-backend` (mirroring +union-double-bits-fpa, the inverse direction): CPROVER's in-tree +SMT2 solver does not fully support the SMT-LIB FloatingPoint +theory beyond constant folding. The test still passes under the +SAT, paths-lifo, and incremental-smt2 (z3) CI profiles -- those +don't reach `smt2_convt::flatten2bv` / `smt2_parsert` for this +program but do validate that the C-level scenario produces the +expected results. diff --git a/regression/smt2_solver/fp/bit-to-fp-bad-width.desc b/regression/smt2_solver/fp/bit-to-fp-bad-width.desc new file mode 100644 index 00000000000..75f36f97d16 --- /dev/null +++ b/regression/smt2_solver/fp/bit-to-fp-bad-width.desc @@ -0,0 +1,7 @@ +CORE +bit-to-fp-bad-width.smt2 + +^EXIT=20$ +^SIGNAL=0$ +^\(error "line 7: to_fp bit-pattern reinterpretation expects a bit-vector operand of width 64"\)$ +-- diff --git a/regression/smt2_solver/fp/bit-to-fp-bad-width.smt2 b/regression/smt2_solver/fp/bit-to-fp-bad-width.smt2 new file mode 100644 index 00000000000..45a06aaaf4a --- /dev/null +++ b/regression/smt2_solver/fp/bit-to-fp-bad-width.smt2 @@ -0,0 +1,14 @@ +; +; Wrong-width operand for the bit-pattern reinterpretation overload of +; `to_fp`: the operand must be 1+eb+(sb-1) = 64 bits for a double, so +; the 8-bit bit-vector below should be rejected at parse time. +; +(define-fun B0 () Bool (= + ((_ to_fp 11 53) (_ bv1 8)) + (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000))) + +(assert (not B0)) + +(check-sat) + +(exit) diff --git a/regression/smt2_solver/fp/bit-to-fp2.desc b/regression/smt2_solver/fp/bit-to-fp2.desc new file mode 100644 index 00000000000..8ff69739e02 --- /dev/null +++ b/regression/smt2_solver/fp/bit-to-fp2.desc @@ -0,0 +1,7 @@ +CORE +bit-to-fp2.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- diff --git a/regression/smt2_solver/fp/bit-to-fp2.smt2 b/regression/smt2_solver/fp/bit-to-fp2.smt2 new file mode 100644 index 00000000000..c0ead6c2827 --- /dev/null +++ b/regression/smt2_solver/fp/bit-to-fp2.smt2 @@ -0,0 +1,15 @@ +; +; Reinterpret the 64-bit IEEE-754 interchange pattern of 1.0 +; (0x3FF0000000000000 = 4607182418800017408) as a double via the +; single-argument bit-pattern overload of to_fp, and check it equals 1.0. +; +(define-fun B0 () Bool (= + ((_ to_fp 11 53) (_ bv4607182418800017408 64)) + (fp #b0 #b01111111111 #b0000000000000000000000000000000000000000000000000000))) + +(assert (not B0)) + +; expected to be UNSAT, i.e., they are equal +(check-sat) + +(exit) diff --git a/regression/smt2_solver/fp/bit-to-fp3.desc b/regression/smt2_solver/fp/bit-to-fp3.desc new file mode 100644 index 00000000000..8af25dfaa84 --- /dev/null +++ b/regression/smt2_solver/fp/bit-to-fp3.desc @@ -0,0 +1,7 @@ +CORE +bit-to-fp3.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- diff --git a/regression/smt2_solver/fp/bit-to-fp3.smt2 b/regression/smt2_solver/fp/bit-to-fp3.smt2 new file mode 100644 index 00000000000..21ef9e7bc60 --- /dev/null +++ b/regression/smt2_solver/fp/bit-to-fp3.smt2 @@ -0,0 +1,16 @@ +; +; Reinterpret the 32-bit IEEE-754 interchange pattern of 1.0f +; (0x3F800000 = 1065353216) as a single via the single-argument +; bit-pattern overload of to_fp. Confirms the width plumbing isn't +; hard-wired to double. +; +(define-fun B0 () Bool (= + ((_ to_fp 8 24) (_ bv1065353216 32)) + (fp #b0 #b01111111 #b00000000000000000000000))) + +(assert (not B0)) + +; expected to be UNSAT, i.e., they are equal +(check-sat) + +(exit) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 94ceb8b3306..7b641da89d7 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -737,7 +737,43 @@ exprt smt2_parsert::function_application() // width_f *includes* the hidden bit const ieee_float_spect spec(width_f - 1, width_e); - auto rounding_mode = expression(); + auto first_operand = expression(); + + // The SMT-LIB FloatingPoint theory gives `to_fp` several + // overloads. All but one take a rounding mode followed by a + // source operand; the exception is the bit-pattern + // reinterpretation + // ((_ to_fp eb sb) (_ BitVec eb+sb)) + // which takes a single bit-vector operand and no rounding mode, + // interpreting those bits directly as the IEEE-754 interchange + // encoding. If the form closes after the first operand, this + // is what we just parsed; otherwise the first operand was the + // rounding mode (bound below) and a source operand follows. + if(smt2_tokenizer.peek() == smt2_tokenizert::CLOSE) + { + next_token(); // eat the ')' + + if( + first_operand.type().id() != ID_unsignedbv || + to_unsignedbv_type(first_operand.type()).get_width() != + spec.width()) + { + throw error() << "to_fp bit-pattern reinterpretation expects a " + "bit-vector operand of width " + << spec.width(); + } + + // Reinterpret the bits as a float. Routing through a generic + // bit-vector type makes the conversion a bit-level reinterpret + // (see boolbv_typecastt) rather than a numeric integer-to-float + // conversion. + return typecast_exprt{ + typecast_exprt{std::move(first_operand), bv_typet{spec.width()}}, + spec.to_type()}; + } + + // The genuine rounding-mode + source-operand path. + const exprt &rounding_mode = first_operand; auto source_op = expression();