Conversion of logical and arithmetic right shift expressions to SMT.

Author: NlightNFotis

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -548,16 +548,31 @@ static smt_termt convert_expr_to_smt(const index_exprt &index)
 static smt_termt convert_expr_to_smt(const shift_exprt &shift)
 {
   // TODO: Dispatch into different types of shifting
+  const auto &first_operand = shift.op0();
+  const auto &second_operand = shift.op1();
+
   if(const auto left_shift = expr_try_dynamic_cast<shl_exprt>(shift))
   {
     return smt_bit_vector_theoryt::shift_left(
-      convert_expr_to_smt(left_shift->op0()),
-      convert_expr_to_smt(left_shift->op1()));
+      convert_expr_to_smt(first_operand), convert_expr_to_smt(second_operand));
+  }
+  else if(
+    const auto right_logical_shift = expr_try_dynamic_cast<lshr_exprt>(shift))
+  {
+    return smt_bit_vector_theoryt::logical_shift_right(
+      convert_expr_to_smt(first_operand), convert_expr_to_smt(second_operand));
+  }
+  else if(
+    const auto right_arith_shift = expr_try_dynamic_cast<ashr_exprt>(shift))
+  {
+    return smt_bit_vector_theoryt::arithmetic_shift_right(
+      convert_expr_to_smt(first_operand), convert_expr_to_smt(second_operand));
+  }
+  else
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for shift expression: " + shift.pretty());
   }
-
-  // TODO: split into functions for separate types of shift including rotate.
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for shift expression: " + shift.pretty());
 }
 
 static smt_termt convert_expr_to_smt(const with_exprt &with)

src/util/bitvector_expr.h

@@ -349,6 +349,12 @@ class ashr_exprt : public shift_exprt
   }
 };
 
+template <>
+inline bool can_cast_expr<ashr_exprt>(const exprt &base)
+{
+  return base.id() == ID_ashr;
+}
+
 /// \brief Logical right shift
 class lshr_exprt : public shift_exprt
 {
@@ -364,6 +370,12 @@ class lshr_exprt : public shift_exprt
   }
 };
 
+template <>
+inline bool can_cast_expr<lshr_exprt>(const exprt &base)
+{
+  return base.id() == ID_lshr;
+}
+
 /// \brief Extracts a single bit of a bit-vector operand
 class extractbit_exprt : public binary_predicate_exprt
 {

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -714,3 +714,103 @@ SCENARIO(
     }
   }
 }
+
+SCENARIO(
+  "Logical Right-shift expressions are converted to SMT terms",
+  "[core][smt2_incremental]")
+{
+  GIVEN("Two integer bitvectors, one for the value and one for the places")
+  {
+    const auto to_be_shifted = from_integer(1, signedbv_typet{8});
+    const auto places = from_integer(2, signedbv_typet{8});
+
+    WHEN("We construct a lshr_exprt and convert it to an SMT term")
+    {
+      const auto shift_expr = lshr_exprt{to_be_shifted, places};
+      const auto constructed_term = convert_expr_to_smt(shift_expr);
+
+      THEN("We should get an logical shift right SMT term")
+      {
+        const smt_termt smt_term_value = smt_bit_vector_constant_termt{1, 8};
+        const smt_termt smt_term_places = smt_bit_vector_constant_termt{2, 8};
+        const auto expected_term = smt_bit_vector_theoryt::logical_shift_right(
+          smt_term_value, smt_term_places);
+        REQUIRE(constructed_term == expected_term);
+      }
+    }
+
+    WHEN(
+      "We construct a malformed lshr_exprt and attempt to convert it to an SMT"
+      " term")
+    {
+      const cbmc_invariants_should_throwt invariants_throw;
+      THEN(
+        "convert_expr_to_smt should throw an exception because of validation "
+        "failure")
+      {
+        REQUIRE_THROWS(
+          convert_expr_to_smt(lshr_exprt{to_be_shifted, false_exprt{}}));
+      }
+    }
+  }
+}
+
+SCENARIO(
+  "Arithmetic Right-shift expressions are converted to SMT terms",
+  "[core][smt2_incremental]")
+{
+  GIVEN("Two integer bitvectors, one for the value and one for the places")
+  {
+    const auto to_be_shifted = from_integer(1, signedbv_typet{8});
+    const auto places = from_integer(2, signedbv_typet{8});
+
+    WHEN("We construct a ashr_exprt and convert it to an SMT term")
+    {
+      const auto shift_expr = ashr_exprt{to_be_shifted, places};
+      const auto constructed_term = convert_expr_to_smt(shift_expr);
+
+      THEN("We should get an arithmetic shift-right SMT term")
+      {
+        const smt_termt smt_term_value = smt_bit_vector_constant_termt{1, 8};
+        const smt_termt smt_term_places = smt_bit_vector_constant_termt{2, 8};
+        const auto expected_term =
+          smt_bit_vector_theoryt::arithmetic_shift_right(
+            smt_term_value, smt_term_places);
+        REQUIRE(constructed_term == expected_term);
+      }
+    }
+
+    WHEN("We construct an ashr_exprt and with a shift of 0 places")
+    {
+      const auto zero_places = from_integer(0, signedbv_typet{8});
+      const auto shift_expr = ashr_exprt{to_be_shifted, zero_places};
+      const auto constructed_term = convert_expr_to_smt(shift_expr);
+
+      THEN(
+        "When we convert it, we should be getting an arithmetic shift-right "
+        "term")
+      {
+        const smt_termt smt_term_value = smt_bit_vector_constant_termt{1, 8};
+        const smt_termt smt_term_places = smt_bit_vector_constant_termt{0, 8};
+        const auto expected_term =
+          smt_bit_vector_theoryt::arithmetic_shift_right(
+            smt_term_value, smt_term_places);
+        REQUIRE(constructed_term == expected_term);
+      }
+    }
+
+    WHEN(
+      "We construct a malformed ashr_exprt and attempt to convert it to an SMT "
+      "term")
+    {
+      const cbmc_invariants_should_throwt invariants_throw;
+      THEN(
+        "convert_expr_to_smt should throw an exception because of validation "
+        "failure")
+      {
+        REQUIRE_THROWS(
+          convert_expr_to_smt(ashr_exprt{to_be_shifted, false_exprt{}}));
+      }
+    }
+  }
+}