Add bit vector theory shift operations

Author: thomasspriggs

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -508,3 +508,72 @@ void smt_bit_vector_theoryt::negatet::validate(const smt_termt &operand)
 
 const smt_function_application_termt::factoryt<smt_bit_vector_theoryt::negatet>
   smt_bit_vector_theoryt::negate{};
+
+const char *smt_bit_vector_theoryt::shift_leftt::identifier()
+{
+  return "bvshl";
+}
+
+smt_sortt smt_bit_vector_theoryt::shift_leftt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::shift_leftt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_operator_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::shift_leftt>
+  smt_bit_vector_theoryt::shift_left{};
+
+const char *smt_bit_vector_theoryt::logical_shift_rightt::identifier()
+{
+  return "bvlshr";
+}
+
+smt_sortt smt_bit_vector_theoryt::logical_shift_rightt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::logical_shift_rightt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_operator_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::logical_shift_rightt>
+  smt_bit_vector_theoryt::logical_shift_right{};
+
+const char *smt_bit_vector_theoryt::arithmetic_shift_rightt::identifier()
+{
+  return "bvashr";
+}
+
+smt_sortt smt_bit_vector_theoryt::arithmetic_shift_rightt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::arithmetic_shift_rightt::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_operator_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::arithmetic_shift_rightt>
+  smt_bit_vector_theoryt::arithmetic_shift_right{};

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -197,6 +197,33 @@ class smt_bit_vector_theoryt
     static void validate(const smt_termt &operand);
   };
   static const smt_function_application_termt::factoryt<negatet> negate;
+
+  // Shift operations
+  struct shift_leftt final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<shift_leftt> shift_left;
+
+  struct logical_shift_rightt final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<logical_shift_rightt>
+    logical_shift_right;
+
+  struct arithmetic_shift_rightt final
+  {
+    static const char *identifier();
+    static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
+    static void validate(const smt_termt &lhs, const smt_termt &rhs);
+  };
+  static const smt_function_application_termt::factoryt<arithmetic_shift_rightt>
+    arithmetic_shift_right;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -431,3 +431,62 @@ TEST_CASE(
     REQUIRE_THROWS(smt_bit_vector_theoryt::negate(true_val));
   }
 }
+
+TEST_CASE("SMT bit vector shifts", "[core][smt2_incremental]")
+{
+  const smt_bit_vector_constant_termt two{2, 8};
+  const smt_bit_vector_constant_termt three{3, 8};
+  const smt_bit_vector_constant_termt wider{4, 16};
+  const smt_bool_literal_termt true_val{true};
+  SECTION("shift left")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::shift_left(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvshl", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::shift_left(three, wider));
+    REQUIRE_THROWS(smt_bit_vector_theoryt::shift_left(true_val, three));
+  }
+  SECTION("logical shift right")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::logical_shift_right(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvlshr", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(smt_bit_vector_theoryt::logical_shift_right(three, wider));
+    REQUIRE_THROWS(
+      smt_bit_vector_theoryt::logical_shift_right(true_val, three));
+  }
+  SECTION("arithmetic shift right")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::arithmetic_shift_right(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvashr", smt_bit_vector_sortt{8}));
+    REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
+    REQUIRE(function_application.arguments().size() == 2);
+    REQUIRE(function_application.arguments()[0].get() == two);
+    REQUIRE(function_application.arguments()[1].get() == three);
+
+    cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(
+      smt_bit_vector_theoryt::arithmetic_shift_right(three, wider));
+    REQUIRE_THROWS(
+      smt_bit_vector_theoryt::arithmetic_shift_right(true_val, three));
+  }
+}