From cd4d55c5d609dde909f2ed20e5b19ce8ff85d070 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 29 Nov 2025 17:23:38 +0100 Subject: [PATCH] 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 --- .../cbmc/saturating_arithmetric/test.desc | 2 +- .../smt2_incremental/convert_expr_to_smt.cpp | 160 ++++++++++++++++++ 2 files changed, 161 insertions(+), 1 deletion(-) diff --git a/regression/cbmc/saturating_arithmetric/test.desc b/regression/cbmc/saturating_arithmetric/test.desc index 1c039664a91..9efefbc7362 100644 --- a/regression/cbmc/saturating_arithmetric/test.desc +++ b/regression/cbmc/saturating_arithmetric/test.desc @@ -1,4 +1,4 @@ -CORE no-new-smt +CORE main.c ^EXIT=0$ diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index d5910628470..30a94e302a6 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1310,6 +1310,154 @@ 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(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(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(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(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 +1922,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(expr)) + { + return convert_expr_to_smt(*saturating_plus, converted); + } + if( + const auto saturating_minus = + expr_try_dynamic_cast(expr)) + { + return convert_expr_to_smt(*saturating_minus, converted); + } if(const auto array_construction = expr_try_dynamic_cast(expr)) { return convert_expr_to_smt(*array_construction, converted);