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/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,70 @@ 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);
+        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());
 
-        if(width_op0==width_op1)
+        // 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 +1897,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(

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