Fix flatten2bv abort on non-constant FPA float (#9101)

regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/main.c

@@ -0,0 +1,24 @@
+// Reproducer for #9101: flatten2bv aborts on non-constant FPA-encoded float
+// when exporting to SMT2 with --fpa.
+//
+// The classic union-based float-to-int type-punning idiom (used pervasively
+// in bit-exact libm code) triggers an invariant violation in the SMT2 export
+// path because flatten2bv does not handle non-constant floatbv expressions
+// under FPA theory.  The native (SAT) back-end solves this without issue.
+
+extern void reach_error(void);
+extern float __VERIFIER_nondet_float(void);
+
+int main(void)
+{
+  float f = __VERIFIER_nondet_float();
+  union
+  {
+    float f;
+    unsigned u;
+  } pun;
+  pun.f = f;
+  if((pun.u & 0x7fffffffu) > 0x7f800000u)
+    reach_error();
+  return 0;
+}

regression/cbmc/smt2-fpa-nonconst-union-flatten2bv/test.desc

@@ -0,0 +1,17 @@
+CORE broken-smt-backend no-new-smt
+main.c
+--smt2 --fpa --outfile -
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Issue #9101: `--smt2 --fpa --outfile` previously aborted with an invariant
+violation ("flatten2bv of a non-constant FPA-encoded float is unsupported")
+when the program reinterprets the bits of a non-constant float through a
+union.  The fix emits the same bvfromfloat round-trip (declare a fresh BV,
+assert to_fp(bv) == float) that find_symbols uses for explicit typecasts.
+
+Tagged broken-smt-backend/no-new-smt because this test explicitly controls
+the output format (--smt2 --fpa --outfile -) and must not be re-run with a
+different solver backend.

regression/validate-trace-xml-schema/check.py

@@ -16,6 +16,7 @@
     ['array_of_bool_as_bitvec', 'test-smt2-outfile.desc'],
     ['deterministic-smt-output', 'test.desc'],
     ['z3-lambda-unflatten', 'test.desc'],
+    ['smt2-fpa-nonconst-union-flatten2bv', 'test.desc'],
     # these tests expect input from stdin
     ['json-interface1', 'test_wrong_option.desc'],
     ['json-interface1', 'test.desc'],

src/solvers/smt2/smt2_conv.cpp

@@ -5252,23 +5252,27 @@ void smt2_convt::flatten2bv(const exprt &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())
       {
+        // A floatbv constant's IEEE-754 interchange bit pattern is exactly
+        // its bit-vector representation, so emit it as a literal BV.
         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");
+        // Non-constant float under FPA theory: look up the bvfromfloat
+        // auxiliary that find_symbols pre-created for this expression.
+        const auto &floatbv_type = to_floatbv_type(type);
+        const typecast_exprt tc{expr, bv_typet{floatbv_type.width()}};
+
+        auto it = defined_expressions.find(tc);
+        CHECK_RETURN_WITH_DIAGNOSTICS(
+          it != defined_expressions.end(),
+          "flatten2bv: bvfromfloat entry missing for non-constant float");
+        out << it->second;
       }
     }
     else
@@ -6046,6 +6050,37 @@ void smt2_convt::find_symbols(const exprt &expr)
       defined_expressions[expr] = id;
     }
   }
+  else if(
+    use_FPA_theory && !expr.is_constant() &&
+    expr.type().id() == ID_floatbv)
+  {
+    // Pre-create a bvfromfloat auxiliary for non-constant floatbv
+    // expressions that may be passed to flatten2bv (e.g. when stored
+    // into a union or flattened as part of a struct).  The SMT-LIB FP
+    // theory has no fp-to-bitvector operator, so the round-trip
+    // (declare fresh BV, assert to_fp(BV) == float) must be emitted at
+    // the top level, before flatten2bv is called mid-expression.
+    const auto &floatbv_type = to_floatbv_type(expr.type());
+    const typecast_exprt tc{expr, bv_typet{floatbv_type.width()}};
+
+    if(defined_expressions.find(tc) == defined_expressions.end())
+    {
+      const irep_idt id =
+        "bvfromfloat." + std::to_string(defined_expressions.size());
+      out << "(declare-fun " << id << " () ";
+      convert_type(tc.type());
+      out << ')' << '\n';
+
+      out << "(assert (= ";
+      out << "((_ to_fp " << floatbv_type.get_e() << " "
+          << floatbv_type.get_f() + 1 << ") " << id << ')';
+      convert_expr(expr);
+      out << ')'; // =
+      out << ')' << '\n';
+
+      defined_expressions[tc] = id;
+    }
+  }
   else if(expr.id() == ID_initial_state)
   {
     irep_idt function = "initial-state";