Add saturating arithmetic support to SMT2 incremental solver

Implements conversion of saturating_plus and saturating_minus
expressions to SMT formulas for both signed and unsigned bit-vector
types.

Fixes: #8070

Author: tautschnig

regression/cbmc/saturating_arithmetric/test.desc

@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1310,6 +1310,142 @@ static smt_termt convert_expr_to_smt(
     mult_overflow.pretty());
 }
 
+static smt_termt convert_expr_to_smt(
+  const saturating_plus_exprt &saturating_plus,
+  const sub_expression_mapt &converted)
+{
+  const auto &op_type = saturating_plus.type();
+  const smt_termt &left = converted.at(saturating_plus.lhs());
+  const smt_termt &right = converted.at(saturating_plus.rhs());
+
+  if(const auto signed_type = type_try_dynamic_cast<signedbv_typet>(op_type))
+  {
+    const std::size_t width = signed_type->get_width();
+
+    // Compute sum with one extra bit using sign extension
+    const auto extended_left = smt_bit_vector_theoryt::sign_extend(1)(left);
+    const auto extended_right = smt_bit_vector_theoryt::sign_extend(1)(right);
+    const auto sum = smt_bit_vector_theoryt::add(extended_left, extended_right);
+
+    // Extract the top bit (sign bit of extended result) and the original sign bit
+    const auto top_bit = smt_bit_vector_theoryt::extract(width, width)(sum);
+    const auto sign_bit = smt_bit_vector_theoryt::extract(width - 1, width - 1)(sum);
+
+    // If the top two bits are equal, no overflow occurred
+    const auto no_overflow = smt_core_theoryt::equal(top_bit, sign_bit);
+
+    // Extract the result (lower bits)
+    const auto result = smt_bit_vector_theoryt::extract(width - 1, 0)(sum);
+
+    // If overflow occurred, check if it's positive or negative overflow
+    const auto is_positive_overflow = smt_core_theoryt::equal(
+      top_bit, smt_bit_vector_constant_termt{0, 1});
+
+    // Return MAX if positive overflow, MIN if negative overflow, otherwise result
+    return smt_core_theoryt::if_then_else(
+      no_overflow,
+      result,
+      smt_core_theoryt::if_then_else(
+        is_positive_overflow,
+        smt_bit_vector_constant_termt{power(2, width - 1) - 1, width}, // MAX
+        smt_bit_vector_constant_termt{power(2, width - 1), width})); // MIN (as unsigned representation)
+  }
+  else if(const auto unsigned_type = type_try_dynamic_cast<unsignedbv_typet>(op_type))
+  {
+    const std::size_t width = unsigned_type->get_width();
+
+    // Compute sum with one extra bit using zero extension
+    const auto extended_left = smt_bit_vector_theoryt::zero_extend(1)(left);
+    const auto extended_right = smt_bit_vector_theoryt::zero_extend(1)(right);
+    const auto sum = smt_bit_vector_theoryt::add(extended_left, extended_right);
+
+    // Check if the top bit is set (overflow occurred)
+    const auto overflow_bit = smt_bit_vector_theoryt::extract(width, width)(sum);
+    const auto no_overflow = smt_core_theoryt::equal(
+      overflow_bit, smt_bit_vector_constant_termt{0, 1});
+
+    // Extract the result (lower bits)
+    const auto result = smt_bit_vector_theoryt::extract(width - 1, 0)(sum);
+
+    // Return MAX if overflow, otherwise result
+    return smt_core_theoryt::if_then_else(
+      no_overflow,
+      result,
+      smt_bit_vector_constant_termt{power(2, width) - 1, width}); // MAX
+  }
+  UNIMPLEMENTED_FEATURE(
+    "Generation of SMT formula for saturating plus expression: " +
+    saturating_plus.pretty());
+}
+
+static smt_termt convert_expr_to_smt(
+  const saturating_minus_exprt &saturating_minus,
+  const sub_expression_mapt &converted)
+{
+  const auto &op_type = saturating_minus.type();
+  const smt_termt &left = converted.at(saturating_minus.lhs());
+  const smt_termt &right = converted.at(saturating_minus.rhs());
+
+  if(const auto signed_type = type_try_dynamic_cast<signedbv_typet>(op_type))
+  {
+    const std::size_t width = signed_type->get_width();
+
+    // Compute difference with one extra bit using sign extension
+    const auto extended_left = smt_bit_vector_theoryt::sign_extend(1)(left);
+    const auto extended_right = smt_bit_vector_theoryt::sign_extend(1)(right);
+    const auto diff = smt_bit_vector_theoryt::subtract(extended_left, extended_right);
+
+    // Extract the top bit (sign bit of extended result) and the original sign bit
+    const auto top_bit = smt_bit_vector_theoryt::extract(width, width)(diff);
+    const auto sign_bit = smt_bit_vector_theoryt::extract(width - 1, width - 1)(diff);
+
+    // If the top two bits are equal, no overflow occurred
+    const auto no_overflow = smt_core_theoryt::equal(top_bit, sign_bit);
+
+    // Extract the result (lower bits)
+    const auto result = smt_bit_vector_theoryt::extract(width - 1, 0)(diff);
+
+    // If overflow occurred, check if it's positive or negative overflow
+    const auto is_positive_overflow = smt_core_theoryt::equal(
+      top_bit, smt_bit_vector_constant_termt{0, 1});
+
+    // Return MAX if positive overflow, MIN if negative overflow, otherwise result
+    return smt_core_theoryt::if_then_else(
+      no_overflow,
+      result,
+      smt_core_theoryt::if_then_else(
+        is_positive_overflow,
+        smt_bit_vector_constant_termt{power(2, width - 1) - 1, width}, // MAX
+        smt_bit_vector_constant_termt{power(2, width - 1), width})); // MIN (as unsigned representation)
+  }
+  else if(const auto unsigned_type = type_try_dynamic_cast<unsignedbv_typet>(op_type))
+  {
+    const std::size_t width = unsigned_type->get_width();
+
+    // Compute difference with one extra bit using zero extension
+    const auto extended_left = smt_bit_vector_theoryt::zero_extend(1)(left);
+    const auto extended_right = smt_bit_vector_theoryt::zero_extend(1)(right);
+    const auto diff = smt_bit_vector_theoryt::subtract(extended_left, extended_right);
+
+    // Check if the top bit is set (underflow occurred)
+    const auto underflow_bit = smt_bit_vector_theoryt::extract(width, width)(diff);
+    const auto no_underflow = smt_core_theoryt::equal(
+      underflow_bit, smt_bit_vector_constant_termt{0, 1});
+
+    // Extract the result (lower bits)
+    const auto result = smt_bit_vector_theoryt::extract(width - 1, 0)(diff);
+
+    // Return MIN (0) if underflow, otherwise result
+    return smt_core_theoryt::if_then_else(
+      no_underflow,
+      result,
+      smt_bit_vector_constant_termt{0, width}); // MIN
+  }
+  UNIMPLEMENTED_FEATURE(
+    "Generation of SMT formula for saturating minus expression: " +
+    saturating_minus.pretty());
+}
+
 static smt_termt convert_expr_to_smt(
   const pointer_object_exprt &pointer_object,
   const sub_expression_mapt &converted)
@@ -1774,6 +1910,18 @@ static smt_termt dispatch_expr_to_smt_conversion(
   {
     return convert_expr_to_smt(*shl_overflow, converted);
   }
+  if(
+    const auto saturating_plus =
+      expr_try_dynamic_cast<saturating_plus_exprt>(expr))
+  {
+    return convert_expr_to_smt(*saturating_plus, converted);
+  }
+  if(
+    const auto saturating_minus =
+      expr_try_dynamic_cast<saturating_minus_exprt>(expr))
+  {
+    return convert_expr_to_smt(*saturating_minus, converted);
+  }
   if(const auto array_construction = expr_try_dynamic_cast<array_exprt>(expr))
   {
     return convert_expr_to_smt(*array_construction, converted);