smt2: flatten FPA-encoded floats to their IEEE bit pattern

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

@@ -0,0 +1,33 @@
+#include <stdint.h>
+
+// 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 float-to-bit-vector operation, 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;
+}

regression/cbmc/union-double-bits-fpa/test.desc

@@ -0,0 +1,34 @@
+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 float-to-bit-vector operation, 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`
+("flatten2bv FPA-encoded float ..." test cases), which drive
+`flatten2bv` directly with `use_FPA_theory == true` and abort
+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.

src/solvers/smt2/smt2_conv.cpp

@@ -5004,11 +5004,51 @@ 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)
+    {
+      // The SMT-LIB FloatingPoint theory has no float-to-bit-vector
+      // operation, so an FPA-encoded value cannot be flattened with a
+      // single operator.  Two shapes cover the cases that arise from
+      // type-punning (union / byte access):
+      //   - a constant: the IEEE interchange bit pattern is the value's
+      //     bit-vector representation, emitted as a literal;
+      //   - a bit-pattern reinterpret `(float)bits` (a typecast from a
+      //     same-width bit-vector): flattening recovers exactly those
+      //     bits, i.e. the typecast operand.
+      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 if(expr.id() == ID_typecast)
+      {
+        const auto &tc = to_typecast_expr(expr);
+        if(
+          tc.op().type().id() == ID_bv &&
+          boolbv_width(tc.op().type()) == boolbv_width(type))
+        {
+          convert_expr(tc.op());
+        }
+        else
+        {
+          UNEXPECTEDCASE(
+            "flatten2bv of a non-constant FPA float that is not a "
+            "bit-pattern reinterpret is unsupported: " +
+            id2string(expr.id()));
+        }
+      }
+      else
+      {
+        UNEXPECTEDCASE(
+          "flatten2bv of a non-constant FPA float that is not a "
+          "bit-pattern reinterpret is unsupported: " +
+          id2string(expr.id()));
+      }
+    }
+    else
+      convert_expr(expr);
   }
   else
     convert_expr(expr);

unit/solvers/smt2/smt2_conv.cpp

@@ -6,6 +6,8 @@
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
+#include <util/c_types.h>
+#include <util/ieee_float.h>
 #include <util/mathematical_types.h>
 #include <util/message.h>
 #include <util/namespace.h>
@@ -156,3 +158,94 @@ 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);
+}
+
+TEST_CASE(
+  "smt2_convt::flatten2bv FPA-encoded float bit-pattern reinterpret",
+  "[core][solvers][smt2]")
+{
+  // Drive `flatten2bv` on the second supported shape: a typecast
+  // `(double)<bv64>` from a same-width generic bit-vector to a
+  // floatbv.  This shape is produced by lower_byte_operators when a
+  // float field is reconstructed from raw bytes; flattening it to bv
+  // must recover the typecast operand without requiring any
+  // float-to-bit-vector operation.
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+  std::ostringstream out;
+  smt2_convt conv{
+    ns, "test", "", "QF_AUFBV", smt2_convt::solvert::CPROVER_SMT2, out};
+
+  // 64-bit generic-bv symbol that the float is reinterpreted from.
+  const bv_typet bv64{64};
+  const symbol_exprt bv_sym{"bits", bv64};
+
+  // (double)<bv64>: same-width reinterpret typecast, op type ID_bv.
+  const floatbv_typet double_type =
+    ieee_float_spect::double_precision().to_type();
+  const typecast_exprt reinterpret_to_double{bv_sym, double_type};
+
+  // Wrap in a single-member union so convert_union -> flatten2bv is
+  // driven on the typecast (rather than on a plain symbol/constant).
+  const union_typet u_type{{struct_union_typet::componentt{"d", double_type}}};
+  const union_exprt u_expr{"d", reinterpret_to_double, u_type};
+
+  const unsignedbv_typet u64{64};
+  // Cast the union to bv64 and assert equality with a fresh bv64
+  // symbol; the SMT2 emission for the LHS goes:
+  //   typecast(union -> bv64)
+  //     -> convert_expr(union_exprt)
+  //     -> convert_union
+  //     -> flatten2bv(typecast(<bv>, double))    <- reinterpret branch
+  //     -> convert_expr(typecast operand)        emits |bits|
+  const symbol_exprt rhs{"rhs", u64};
+  conv.set_to(equal_exprt{typecast_exprt{u_expr, u64}, rhs}, true);
+
+  // The reinterpret branch emits the typecast operand directly; the
+  // operand is the bv64 symbol `bits`.  The resulting assertion
+  // therefore reduces to `(= bits rhs)` -- in particular without any
+  // `((_ to_fp ...))` wrapper that would indicate the value-
+  // converting/find_symbols round-trip.
+  REQUIRE(out.str().find("(= bits rhs)") != std::string::npos);
+  REQUIRE(out.str().find("(_ to_fp") == std::string::npos);
+}