Add support for converting mismatched shift operands to smt

In order to bring this conversion closer to parity with the old SMT
backend.

Shift operations of this kind have been seen during testing of the
overflow operations, which is work which will be submitted in a
following PR.

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -121,6 +121,16 @@ static smt_termt convert_c_bool_cast(
     smt_bit_vector_constant_termt{0, c_bool_width});
 }
 
+static std::function<std::function<smt_termt(smt_termt)>(std::size_t)>
+extension_for_type(const typet &type)
+{
+  if(can_cast_type<signedbv_typet>(type))
+    return smt_bit_vector_theoryt::sign_extend;
+  if(can_cast_type<unsignedbv_typet>(type))
+    return smt_bit_vector_theoryt::zero_extend;
+  UNREACHABLE;
+}
+
 static smt_termt make_bitvector_resize_cast(
   const smt_termt &from_term,
   const bitvector_typet &from_type,
@@ -147,10 +157,7 @@ static smt_termt make_bitvector_resize_cast(
   if(to_width < from_width)
     return smt_bit_vector_theoryt::extract(to_width - 1, 0)(from_term);
   const std::size_t extension_size = to_width - from_width;
-  if(can_cast_type<signedbv_typet>(from_type))
-    return smt_bit_vector_theoryt::sign_extend(extension_size)(from_term);
-  else
-    return smt_bit_vector_theoryt::zero_extend(extension_size)(from_term);
+  return extension_for_type(from_type)(extension_size)(from_term);
 }
 
 struct sort_based_cast_to_bit_vector_convertert final
@@ -658,7 +665,33 @@ convert_to_smt_shift(const factoryt &factory, const shiftt &shift)
 {
   const smt_termt first_operand = convert_expr_to_smt(shift.op0());
   const smt_termt second_operand = convert_expr_to_smt(shift.op1());
-  return factory(first_operand, second_operand);
+  const auto first_bit_vector_sort =
+    first_operand.get_sort().cast<smt_bit_vector_sortt>();
+  const auto second_bit_vector_sort =
+    second_operand.get_sort().cast<smt_bit_vector_sortt>();
+  INVARIANT(
+    first_bit_vector_sort && second_bit_vector_sort,
+    "Shift expressions are expected to have bit vector operands.");
+  const std::size_t first_width = first_bit_vector_sort->bit_width();
+  const std::size_t second_width = second_bit_vector_sort->bit_width();
+  if(first_width > second_width)
+  {
+    return factory(
+      first_operand,
+      extension_for_type(shift.op1().type())(first_width - second_width)(
+        second_operand));
+  }
+  else if(first_width < second_width)
+  {
+    return factory(
+      extension_for_type(shift.op0().type())(second_width - first_width)(
+        first_operand),
+      second_operand);
+  }
+  else
+  {
+    return factory(first_operand, second_operand);
+  }
 }
 
 static smt_termt convert_expr_to_smt(const shift_exprt &shift)

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -819,6 +819,84 @@ SCENARIO(
   }
 }
 
+TEST_CASE(
+  "expr to smt conversion for shifts of mismatched operands.",
+  "[core][smt2_incremental]")
+{
+  using make_typet = std::function<typet(std::size_t)>;
+  const make_typet make_unsigned = constructor_oft<unsignedbv_typet>{};
+  const make_typet make_signed = constructor_oft<signedbv_typet>{};
+  using make_extensiont =
+    std::function<std::function<smt_termt(smt_termt)>(std::size_t)>;
+  const make_extensiont zero_extend = smt_bit_vector_theoryt::zero_extend;
+  const make_extensiont sign_extend = smt_bit_vector_theoryt::sign_extend;
+  std::string type_description;
+  make_typet make_type;
+  make_extensiont make_extension;
+  using type_rowt = std::tuple<std::string, make_typet, make_extensiont>;
+  std::tie(type_description, make_type, make_extension) = GENERATE_REF(
+    type_rowt{"Unsigned operands.", make_unsigned, zero_extend},
+    type_rowt{"Signed operands.", make_signed, sign_extend});
+  SECTION(type_description)
+  {
+    using make_shift_exprt = std::function<exprt(exprt, exprt)>;
+    const make_shift_exprt left_shift_expr = constructor_of<shl_exprt>();
+    const make_shift_exprt arithmetic_right_shift_expr =
+      constructor_of<ashr_exprt>();
+    const make_shift_exprt logical_right_shift_expr =
+      constructor_of<lshr_exprt>();
+    using make_shift_termt = std::function<smt_termt(smt_termt, smt_termt)>;
+    const make_shift_termt left_shift_term = smt_bit_vector_theoryt::shift_left;
+    const make_shift_termt arithmetic_right_shift_term =
+      smt_bit_vector_theoryt::arithmetic_shift_right;
+    const make_shift_termt logical_right_shift_term =
+      smt_bit_vector_theoryt::logical_shift_right;
+    std::string shift_description;
+    make_shift_exprt make_shift_expr;
+    make_shift_termt make_shift_term;
+    using shift_rowt =
+      std::tuple<std::string, make_shift_exprt, make_shift_termt>;
+    std::tie(shift_description, make_shift_expr, make_shift_term) =
+      GENERATE_REF(
+        shift_rowt{"Left shift.", left_shift_expr, left_shift_term},
+        shift_rowt{
+          "Arithmetic right shift.",
+          arithmetic_right_shift_expr,
+          arithmetic_right_shift_term},
+        shift_rowt{
+          "Logical right shift.",
+          logical_right_shift_expr,
+          logical_right_shift_term});
+    SECTION(shift_description)
+    {
+      SECTION("Wider left hand side")
+      {
+        const exprt input = make_shift_expr(
+          symbol_exprt{"foo", make_type(32)},
+          symbol_exprt{"bar", make_type(8)});
+        INFO("Input expr: " + input.pretty(2, 0));
+        const smt_termt expected_result = make_shift_term(
+          smt_identifier_termt{"foo", smt_bit_vector_sortt{32}},
+          make_extension(24)(
+            smt_identifier_termt{"bar", smt_bit_vector_sortt{8}}));
+        CHECK(convert_expr_to_smt(input) == expected_result);
+      }
+      SECTION("Wider right hand side")
+      {
+        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 = make_shift_term(
+          make_extension(24)(
+            smt_identifier_termt{"foo", smt_bit_vector_sortt{8}}),
+          smt_identifier_termt{"bar", smt_bit_vector_sortt{32}});
+        CHECK(convert_expr_to_smt(input) == expected_result);
+      }
+    }
+  }
+}
+
 TEST_CASE(
   "expr to smt conversion for extract bits expressions",
   "[core][smt2_incremental]")