Merge pull request #8922 from tautschnig/fix-8054-smt2-incr-floating-point

Add floating point support to incremental SMT2 solver via bit-blasting

Author: tautschnig

regression/cbmc-incr-smt2/floating-point/basic.c

@@ -0,0 +1,9 @@
+int main()
+{
+  float x = 1.0f;
+  float y = 2.0f;
+  __CPROVER_assert(x + y == 3.0f, "float add");
+  __CPROVER_assert(x < y, "float lt");
+  __CPROVER_assert(x != y, "float ne");
+  __CPROVER_assert(!(x != x), "x == x");
+}

regression/cbmc-incr-smt2/floating-point/basic.desc

@@ -0,0 +1,9 @@
+CORE
+basic.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Basic floating-point operations via bit-blasting in incremental SMT2.

regression/cbmc-incr-smt2/floating-point/float16_ops.c

@@ -0,0 +1,38 @@
+// _Float16 requires GCC >= 12 or Clang >= 15.
+// On other compilers, fall back to a trivial float test.
+#if defined(__GNUC__) && !defined(__clang__) && __GNUC__ >= 12
+#  define HAS_FLOAT16
+#elif defined(__clang__) && __clang_major__ >= 15
+#  define HAS_FLOAT16
+#endif
+
+#ifdef HAS_FLOAT16
+
+int main()
+{
+  _Float16 a = 3.0f16;
+  _Float16 b = 2.0f16;
+
+  __CPROVER_assert(a + b == 5.0f16, "add");
+  __CPROVER_assert(a - b == 1.0f16, "sub");
+  __CPROVER_assert(a * b == 6.0f16, "mul");
+  __CPROVER_assert(a / b == 1.5f16, "div");
+  __CPROVER_assert(a > b, "gt");
+  __CPROVER_assert(b < a, "lt");
+  __CPROVER_assert(-a == -3.0f16, "neg");
+
+  int i = (int)a;
+  __CPROVER_assert(i == 3, "to_int");
+  _Float16 c = (_Float16)5;
+  __CPROVER_assert(c == 5.0f16, "from_int");
+  float d = (float)a;
+  __CPROVER_assert(d == 3.0f, "f16_to_f32");
+}
+
+#else
+
+int main()
+{
+}
+
+#endif

regression/cbmc-incr-smt2/floating-point/float16_ops.desc

@@ -0,0 +1,11 @@
+CORE
+float16_ops.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+Tests float arithmetic, comparisons, negation, and casts via
+incremental SMT2 with float_bvt bit-blasting. Uses _Float16
+where available (GCC >= 12, Clang >= 15) for small formulae.

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -96,6 +96,12 @@ static smt_sortt convert_type_to_smt_sort(const array_typet &type)
     convert_type_to_smt_sort(type.element_type())};
 }
 
+static smt_sortt convert_type_to_smt_sort(const floatbv_typet &type)
+{
+  // Convert floating-point to bitvector for bit-blasting
+  return smt_bit_vector_sortt{type.get_width()};
+}
+
 smt_sortt convert_type_to_smt_sort(const typet &type)
 {
   if(const auto bool_type = type_try_dynamic_cast<bool_typet>(type))
@@ -104,6 +110,10 @@ smt_sortt convert_type_to_smt_sort(const typet &type)
   }
   if(const auto bitvector_type = type_try_dynamic_cast<bitvector_typet>(type))
   {
+    if(const auto floatbv_type = type_try_dynamic_cast<floatbv_typet>(type))
+    {
+      return convert_type_to_smt_sort(*floatbv_type);
+    }
     return convert_type_to_smt_sort(*bitvector_type);
   }
   if(const auto array_type = type_try_dynamic_cast<array_typet>(type))
@@ -182,13 +192,8 @@ static smt_termt make_bitvector_resize_cast(
       "type: " +
       to_type.pretty());
   }
-  if(type_try_dynamic_cast<floatbv_typet>(to_type))
-  {
-    UNIMPLEMENTED_FEATURE(
-      "Generation of SMT formula for type cast to floating-point bitvector "
-      "type: " +
-      to_type.pretty());
-  }
+  // After float lowering, floatbv types are treated as bitvectors.
+  // Same-width casts (e.g., from float_bvt::pack) are handled below.
   const std::size_t from_width = from_type.get_width();
   const std::size_t to_width = to_type.get_width();
   if(to_width == from_width)
@@ -272,8 +277,11 @@ static smt_termt convert_expr_to_smt(
   const floatbv_typecast_exprt &float_cast,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for floating point type cast expression: " +
+  // Floating-point operations should be lowered to bitvector operations
+  // before reaching this point. If we get here, it means the lowering failed.
+  UNREACHABLE_BECAUSE(
+    "Floating point type cast expression should have been lowered to "
+    "bitvector operations: " +
     float_cast.pretty());
 }
 
@@ -535,17 +543,19 @@ static smt_termt convert_expr_to_smt(
   const ieee_float_equal_exprt &float_equal,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for floating point equality expression: " +
+  UNREACHABLE_BECAUSE(
+    "Floating point equality expression should have been lowered to "
+    "bitvector operations: " +
     float_equal.pretty());
 }
 
 static smt_termt convert_expr_to_smt(
   const ieee_float_notequal_exprt &float_not_equal,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for floating point not equal expression: " +
+  UNREACHABLE_BECAUSE(
+    "Floating point not equal expression should have been lowered to "
+    "bitvector operations: " +
     float_not_equal.pretty());
 }
 
@@ -785,8 +795,9 @@ static smt_termt convert_expr_to_smt(
 {
   // This case includes the floating point plus, minus, division and
   // multiplication operations.
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for floating point operation expression: " +
+  UNREACHABLE_BECAUSE(
+    "Floating point operation expression should have been lowered to "
+    "bitvector operations: " +
     float_operation.pretty());
 }
 
@@ -1158,35 +1169,39 @@ static smt_termt convert_expr_to_smt(
   const isnan_exprt &is_nan_expr,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for is not a number expression: " +
+  UNREACHABLE_BECAUSE(
+    "Is not a number expression should have been lowered to "
+    "bitvector operations: " +
     is_nan_expr.pretty());
 }
 
 static smt_termt convert_expr_to_smt(
   const isfinite_exprt &is_finite_expr,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for is finite expression: " +
+  UNREACHABLE_BECAUSE(
+    "Is finite expression should have been lowered to "
+    "bitvector operations: " +
     is_finite_expr.pretty());
 }
 
 static smt_termt convert_expr_to_smt(
   const isinf_exprt &is_infinite_expr,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for is infinite expression: " +
+  UNREACHABLE_BECAUSE(
+    "Is infinite expression should have been lowered to "
+    "bitvector operations: " +
     is_infinite_expr.pretty());
 }
 
 static smt_termt convert_expr_to_smt(
   const isnormal_exprt &is_normal_expr,
   const sub_expression_mapt &converted)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for is infinite expression: " +
+  UNREACHABLE_BECAUSE(
+    "Is normal expression should have been lowered to "
+    "bitvector operations: " +
     is_normal_expr.pretty());
 }
 

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -11,6 +11,7 @@
 #include <util/std_expr.h>
 #include <util/string_constant.h>
 
+#include <solvers/floatbv/float_bv.h>
 #include <solvers/smt2_incremental/ast/smt_commands.h>
 #include <solvers/smt2_incremental/ast/smt_responses.h>
 #include <solvers/smt2_incremental/ast/smt_terms.h>
@@ -308,6 +309,42 @@ static exprt lower_zero_extend(exprt expr, const namespacet &ns)
   return expr;
 }
 
+/// \brief Check whether an expression or any of its immediate operands
+///   has floating-point bitvector type.
+static bool has_floatbv_type(const exprt &expr)
+{
+  if(expr.type().id() == ID_floatbv)
+    return true;
+  for(const auto &op : expr.operands())
+  {
+    if(op.type().id() == ID_floatbv)
+      return true;
+  }
+  return false;
+}
+
+/// \brief Lower floating-point operations to bitvector expressions.
+/// Traverses \p expr bottom-up and replaces float-specific sub-expressions
+/// (e.g., ieee_float_equal, floatbv_plus) with their bitvector equivalents
+/// using \ref float_bvt::convert.
+static exprt lower_floatbv(exprt expr)
+{
+  // Recurse into operands first (bottom-up)
+  for(auto &op : expr.operands())
+    op = lower_floatbv(op);
+
+  // Only attempt float_bv conversion on expressions involving floats
+  if(has_floatbv_type(expr))
+  {
+    const float_bvt float_bv;
+    const exprt converted = float_bv.convert(expr);
+    if(!converted.is_nil())
+      return converted;
+  }
+
+  return expr;
+}
+
 void smt2_incremental_decision_proceduret::ensure_handle_for_expr_defined(
   const exprt &in_expr)
 {
@@ -688,7 +725,8 @@ exprt smt2_incremental_decision_proceduret::lower(exprt expression) const
 {
   const exprt lowered = struct_encoding.encode(lower_zero_extend(
     lower_enum(
-      lower_byte_operators(lower_rw_ok_pointer_in_range(expression, ns), ns),
+      lower_byte_operators(
+        lower_floatbv(lower_rw_ok_pointer_in_range(expression, ns)), ns),
       ns),
     ns));
   log.conditional_output(log.debug(), [&](messaget::mstreamt &debug) {