From 0fa58a0be00b17e1c83bdbf7d8be491ce55c236d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 28 Oct 2026 07:41:58 +0000 Subject: [PATCH] Incremental SMT2: fix shift extension for mismatched widths When the shift operand and distance have different bit widths, the incremental SMT2 backend extended them according to their type signedness (extension_for_type). This is wrong for shifts: the shift kind determines how the operand should be extended, and the distance is always treated as unsigned. Specifically: - lshr of a signed operand was sign-extended (wrong: should zero-extend to avoid shifting sign bits into the result); - ashr of an unsigned operand was zero-extended (wrong: should sign-extend to shift copies of the MSB into the result); - A signed distance was sign-extended (wrong: shift distances are unsigned in the CBMC IR, per the SAT backend semantics). Fix: always zero-extend the distance; extend the operand according to the shift kind (sign-extend for ashr, zero-extend for lshr and shl). The C front end only produces lshr for unsigned and ashr for signed operands, so the default configuration is not affected. The bug affects producers of GOTO programs that create shift expressions with the "opposite" combination (e.g. lshr of a signed value). Related to #9177/PR #9178 which fixes the same class of bug in the non-incremental SMT2 backend. Reported by Jeroen Robben (https://reports.robben.io/methodology/). Fixes #9362 Co-authored-by: Kiro --- .../smt2_incremental/convert_expr_to_smt.cpp | 17 ++++++++++++----- .../smt2_incremental/convert_expr_to_smt.cpp | 19 +++++++++++++------ 2 files changed, 25 insertions(+), 11 deletions(-) diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 8188e629d5d8..af2093423edc 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -24,6 +24,7 @@ #include #include #include +#include /// Post order visitation is used in order to construct the the smt terms bottom /// upwards without using recursion to traverse the input `exprt`. Therefore @@ -969,17 +970,23 @@ static smt_termt convert_to_smt_shift( const std::size_t second_width = second_bit_vector_sort->bit_width(); if(first_width > second_width) { + // Shift distances are unsigned: always zero-extend the distance. return factory( first_operand, - extension_for_type(shift.op1().type())(first_width - second_width)( + smt_bit_vector_theoryt::zero_extend(first_width - second_width)( second_operand)); } else if(first_width < second_width) { - const auto result = factory( - extension_for_type(shift.op0().type())(second_width - first_width)( - first_operand), - second_operand); + // The operand must be extended according to the shift kind, not + // its type signedness: ashr sign-extends (to shift copies of the + // MSB into the result), all others zero-extend. + const std::size_t ext = second_width - first_width; + const smt_termt extended_operand = + std::is_same::value + ? smt_termt{smt_bit_vector_theoryt::sign_extend(ext)(first_operand)} + : smt_termt{smt_bit_vector_theoryt::zero_extend(ext)(first_operand)}; + const auto result = factory(extended_operand, second_operand); return smt_bit_vector_theoryt::extract(first_width - 1, 0)(result); } else diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index aea2daf27629..786f3bbf13e9 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1198,23 +1198,30 @@ TEST_CASE( symbol_exprt{"foo", make_type(32)}, symbol_exprt{"bar", make_type(8)}); INFO("Input expr: " + input.pretty(2, 0)); + // Shift distances are always zero-extended, regardless of type. const smt_termt expected_result = make_shift_term( smt_identifier_termt{"foo", smt_bit_vector_sortt{32}}, - make_extension(24)( + smt_bit_vector_theoryt::zero_extend(24)( smt_identifier_termt{"bar", smt_bit_vector_sortt{8}})); CHECK(test.convert(input) == expected_result); } SECTION("Wider right hand side") { + // The operand is extended by the shift kind: ashr sign-extends, + // lshr and shl zero-extend. + const smt_termt foo{ + smt_identifier_termt{"foo", smt_bit_vector_sortt{8}}}; + const smt_termt extended_foo = + shift_description == "Arithmetic right shift." + ? smt_termt{smt_bit_vector_theoryt::sign_extend(24)(foo)} + : smt_termt{smt_bit_vector_theoryt::zero_extend(24)(foo)}; const exprt input = make_shift_expr( symbol_exprt{"foo", make_type(8)}, symbol_exprt{"bar", make_type(32)}); INFO("Input expr: " + input.pretty(2, 0)); - const smt_termt expected_result = - smt_bit_vector_theoryt::extract(7, 0)(make_shift_term( - make_extension(24)( - smt_identifier_termt{"foo", smt_bit_vector_sortt{8}}), - smt_identifier_termt{"bar", smt_bit_vector_sortt{32}})); + const smt_termt expected_result = smt_bit_vector_theoryt::extract( + 7, 0)(make_shift_term( + extended_foo, smt_identifier_termt{"bar", smt_bit_vector_sortt{32}})); CHECK(test.convert(input) == expected_result); } }