SMT-LIB2: shifts with wider shift distances

This fixes the case of converting shifts where the shift distance is wider
than the shift operand to SMT-LIB2.

SMT-LIB2 requires that the width of the shift operand and the shift distance
is the same.  To not lose leading bits of the shift distance, use the
wider one of the two as the width of the shift, and truncate the result
when needed.

Author: kroening

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.",