smt2: support bit-pattern reinterpretation overload of to_fp

regression/cbmc/union-bits-double-fpa/main.c

@@ -0,0 +1,39 @@
+#include <stdint.h>
+
+// 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) <bv64>)
+//
+// 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;
+}

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.

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"\)$
+--

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)

regression/smt2_solver/fp/bit-to-fp2.desc

@@ -0,0 +1,7 @@
+CORE
+bit-to-fp2.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

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)

regression/smt2_solver/fp/bit-to-fp3.desc

@@ -0,0 +1,7 @@
+CORE
+bit-to-fp3.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^unsat$
+--

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)

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();