Add implementation and tests for arithmetic right shift conversion to SMT terms.

Author: NlightNFotis

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -550,7 +550,6 @@ 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
   if(const auto left_shift = expr_try_dynamic_cast<shl_exprt>(shift))
   {
     return smt_bit_vector_theoryt::shift_left(
@@ -564,10 +563,18 @@ static smt_termt convert_expr_to_smt(const shift_exprt &shift)
       convert_expr_to_smt(right_logical_shift->op0()),
       convert_expr_to_smt(right_logical_shift->op1()));
   }
-
-  // TODO: split into functions for separate types of shift including rotate.
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for shift expression: " + shift.pretty());
+  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(right_arith_shift->op0()),
+      convert_expr_to_smt(right_arith_shift->op1()));
+  }
+  else
+  {
+    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
 {

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -755,3 +755,67 @@ SCENARIO(
     }
   }
 }
+
+SCENARIO(
+  "Arithmetic Right-shift expressions are converted to SMT terms",
+  "[core][smt2_incremental]")
+{
+  GIVEN("An integer bitvector")
+  {
+    const auto one_bvint = from_integer({1}, signedbv_typet{8});
+
+    WHEN("We construct a ashr_exprt and convert it to an SMT term")
+    {
+      const auto shift_expr = ashr_exprt{one_bvint, one_bvint};
+      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_one = smt_bit_vector_constant_termt{1, 8};
+        const auto expected_term =
+          smt_bit_vector_theoryt::arithmetic_shift_right(
+            /* Value to be shifted */
+            smt_term_one,
+            /* Places */
+            smt_term_one);
+        REQUIRE(constructed_term == expected_term);
+      }
+    }
+
+    WHEN("We construct an ashr_exprt and with a shift of 0 places")
+    {
+      const auto zero_bvint = from_integer({0}, signedbv_typet{8});
+      const auto shift_expr = ashr_exprt{one_bvint, zero_bvint};
+      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_zero = smt_bit_vector_constant_termt{0, 8};
+        const smt_termt smt_term_one = smt_bit_vector_constant_termt{1, 8};
+        const auto expected_term =
+          smt_bit_vector_theoryt::arithmetic_shift_right(
+            /* Value to be shifted */
+            smt_term_one,
+            /* Places */
+            smt_term_zero);
+        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{one_bvint, false_exprt{}}));
+      }
+    }
+  }
+}