SMT-LIB2: shifts with wider shift distances

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<signed>::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);
   }

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<width_op1
+        else // width_op<width_distance -- distance is wider
         {
-          out << "((_ extract " << width_op0-1 << " 0) ";
+          // enlarge the shift to match the distance operand,
+          // then extract again
+          out << "((_ extract " << width_op - 1 << " 0) ";
+          emit_operator(shift_expr);
+
+          // use sign extension when needed
+          if(shift_expr.op().type().id() == ID_signedbv)
+          {
+            out << "((_ sign_extend " << width_distance - width_op << ") ";
+            convert_expr(shift_expr.op());
+            out << ')'; // sign_extend
+          }
+          else
+          {
+            out << "((_ zero_extend " << width_distance - width_op << ") ";
+            convert_expr(shift_expr.op());
+            out << ')'; // zero_extend
+          }
+
+          out << ' ';
           convert_expr(shift_expr.distance());
-          out << ")"; // extract
+          out << ')'; // bv*sh
+          out << ')'; // extract
         }
       }
       else
@@ -1856,8 +1900,6 @@ void smt2_convt::convert_expr(const exprt &expr)
           "unsupported distance type for " + shift_expr.id_string() + ": " +
           distance_type.id_string());
       }
-
-      out << ")"; // bv*sh
     }
     else
       UNEXPECTEDCASE(

src/util/bitvector_expr.h

@@ -482,6 +482,8 @@ inline shift_exprt &to_shift_expr(exprt &expr)
 }
 
 /// \brief Left shift
+/// Shift distances may exceed the width of the shifted operand.
+/// Shifts with negative shift distance do not have meaning.
 class shl_exprt : public shift_exprt
 {
 public:
@@ -526,6 +528,8 @@ inline shl_exprt &to_shl_expr(exprt &expr)
 }
 
 /// \brief Arithmetic right shift
+/// Shift distances may exceed the width of the shifted operand.
+/// Shifts with negative shift distance do not have meaning.
 class ashr_exprt : public shift_exprt
 {
 public:
@@ -547,6 +551,8 @@ inline bool can_cast_expr<ashr_exprt>(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:

unit/solvers/smt2/smt2_conv.cpp

@@ -1,8 +1,76 @@
 // Author: Diffblue Ltd.
 
-#include <testing-utils/use_catch.h>
+#include <util/bitvector_expr.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
 
 #include <solvers/smt2/smt2_conv.h>
+#include <testing-utils/use_catch.h>
+
+#include <sstream>
+
+/// 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.",