diff --git a/src/solvers/flattening/boolbv_shift.cpp b/src/solvers/flattening/boolbv_shift.cpp index e50273f6d5a..39b04567ffa 100644 --- a/src/solvers/flattening/boolbv_shift.cpp +++ b/src/solvers/flattening/boolbv_shift.cpp @@ -53,6 +53,7 @@ bvt boolbvt::convert_shift(const binary_exprt &expr) std::size_t distance; + // no attempt is made to handle negative shift distances if(i<0 || i>std::numeric_limits::max()) distance=0; else @@ -66,6 +67,7 @@ bvt boolbvt::convert_shift(const binary_exprt &expr) } else { + // no attempt is made to handle negative shift distances const bvt &distance=convert_bv(expr.op1()); return bv_utils.shift(op, shift, distance); } diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index e00becc56e9..52fc42df1ea 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1801,21 +1801,21 @@ void smt2_convt::convert_expr(const exprt &expr) type.id()==ID_signedbv || type.id()==ID_bv) { - if(shift_expr.id() == ID_ashr) - out << "(bvashr "; - else if(shift_expr.id() == ID_lshr) - out << "(bvlshr "; - else if(shift_expr.id() == ID_shl) - out << "(bvshl "; - else - UNREACHABLE; - - convert_expr(shift_expr.op()); - out << " "; - // SMT2 requires the shift distance to have the same width as // the value that is shifted -- odd! + auto emit_operator = [this](const exprt &shift_expr) + { + if(shift_expr.id() == ID_ashr) + out << "(bvashr "; + else if(shift_expr.id() == ID_lshr) + out << "(bvlshr "; + else if(shift_expr.id() == ID_shl) + out << "(bvshl "; + else + UNREACHABLE; + }; + const auto &distance_type = shift_expr.distance().type(); if(distance_type.id() == ID_integer || distance_type.id() == ID_natural) { @@ -1825,29 +1825,73 @@ void smt2_convt::convert_expr(const exprt &expr) // shift distance must be bit vector std::size_t width_op0 = boolbv_width(shift_expr.op().type()); exprt tmp=from_integer(i, unsignedbv_typet(width_op0)); + + emit_operator(shift_expr); + convert_expr(shift_expr.op()); + out << ' '; convert_expr(tmp); + out << ')'; // bv*sh } else if( distance_type.id() == ID_signedbv || distance_type.id() == ID_unsignedbv || distance_type.id() == ID_c_enum || distance_type.id() == ID_c_bool) { - std::size_t width_op0 = boolbv_width(shift_expr.op().type()); - std::size_t width_op1 = boolbv_width(distance_type); - - if(width_op0==width_op1) + // No attempt is made to handle negative shift distances. + // The shift distance is always interpreted as binary value, + // irrespectively of its type. + std::size_t width_op = boolbv_width(shift_expr.op().type()); + std::size_t width_distance = boolbv_width(distance_type); + std::size_t width_result = boolbv_width(shift_expr.type()); + + if(width_result != width_op) + UNEXPECTEDCASE( + "unsupported result width for " + shift_expr.id_string()); + + // we use the larger of the two widths + if(width_op == width_distance) + { + emit_operator(shift_expr); + convert_expr(shift_expr.op()); + out << ' '; convert_expr(shift_expr.distance()); - else if(width_op0>width_op1) + out << ')'; // bv*sh + } + else if(width_op > width_distance) { - out << "((_ zero_extend " << width_op0-width_op1 << ") "; + emit_operator(shift_expr); + convert_expr(shift_expr.op()); + out << ' '; + out << "((_ zero_extend " << width_op - width_distance << ") "; convert_expr(shift_expr.distance()); - out << ")"; // zero_extend + out << ')'; // zero_extend + out << ')'; // bv*sh } - else // width_op0(const exprt &base) } /// \brief Logical right shift +/// Shift distances may exceed the width of the shifted operand. +/// Shifts with negative shift distance do not have meaning. class lshr_exprt : public shift_exprt { public: diff --git a/unit/solvers/smt2/smt2_conv.cpp b/unit/solvers/smt2/smt2_conv.cpp index df75870957a..537a63ad582 100644 --- a/unit/solvers/smt2/smt2_conv.cpp +++ b/unit/solvers/smt2/smt2_conv.cpp @@ -1,8 +1,76 @@ // Author: Diffblue Ltd. -#include +#include +#include +#include #include +#include + +#include + +/// helper class for testing smt2_convt +class smt2_conv_testt : public smt2_convt +{ +public: + smt2_conv_testt(const namespacet &_ns, std::ostream &_out) + : smt2_convt{_ns, "", "", "", smt2_convt::solvert::GENERIC, _out} + { + } + + void convert_expr_public(const exprt &expr) + { + convert_expr(expr); + } +}; + +static std::string smt2(const exprt &expr) +{ + symbol_tablet symbol_table; + namespacet ns{symbol_table}; + std::ostringstream out; + smt2_conv_testt smt2_conv{ns, out}; + std::size_t length = out.str().size(); + smt2_conv.convert_expr_public(expr); + return std::string{out.str(), length, std::string::npos}; +} + +TEST_CASE("smt2_convt conversion for shifts", "[core][solvers][smt2]") +{ + GIVEN("A shift expression with equal-with operands") + { + auto op = symbol_exprt{"op", unsignedbv_typet{8}}; + auto distance = symbol_exprt{"dist", unsignedbv_typet{8}}; + auto shift = shl_exprt{op, distance}; + REQUIRE(smt2(shift) == "(bvshl op dist)"); + } + + GIVEN("A shift expression with an unsigned shift operand and wider distance") + { + auto op = symbol_exprt{"op", unsignedbv_typet{8}}; + auto distance = symbol_exprt{"dist", unsignedbv_typet{10}}; + auto shift = shl_exprt{op, distance}; + REQUIRE( + smt2(shift) == "((_ extract 7 0) (bvshl ((_ zero_extend 2) op) dist))"); + } + + GIVEN("A shift expression with a signed shift operand and wider distance") + { + auto op = symbol_exprt{"op", signedbv_typet{8}}; + auto distance = symbol_exprt{"dist", unsignedbv_typet{10}}; + auto shift = ashr_exprt{op, distance}; + REQUIRE( + smt2(shift) == "((_ extract 7 0) (bvashr ((_ sign_extend 2) op) dist))"); + } + + GIVEN("A shift expression with a wider shift operand") + { + auto op = symbol_exprt{"op", unsignedbv_typet{10}}; + auto distance = symbol_exprt{"dist", unsignedbv_typet{8}}; + auto shift = shl_exprt{op, distance}; + REQUIRE(smt2(shift) == "(bvshl op ((_ zero_extend 2) dist))"); + } +} TEST_CASE( "smt2_convt::convert_identifier character escaping.",