Add implementation and tests for conversion of logical right shift expressions to SMT.

Author: NlightNFotis

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -557,6 +557,13 @@ static smt_termt convert_expr_to_smt(const shift_exprt &shift)
       convert_expr_to_smt(left_shift->op0()),
       convert_expr_to_smt(left_shift->op1()));
   }
+  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(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(

src/util/bitvector_expr.h

@@ -364,6 +364,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,44 @@ SCENARIO(
     }
   }
 }
+
+SCENARIO(
+  "Logical 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 lshr_exprt and convert it to an SMT term")
+    {
+      const auto shift_expr = lshr_exprt{one_bvint, one_bvint};
+      const auto constructed_term = convert_expr_to_smt(shift_expr);
+
+      THEN("We should get an logical shift left SMT term")
+      {
+        const smt_termt smt_term_one = smt_bit_vector_constant_termt{1, 8};
+        const auto expected_term = smt_bit_vector_theoryt::logical_shift_right(
+          /* Value to be shifted */
+          smt_term_one,
+          /* Places */
+          smt_term_one);
+        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{one_bvint, false_exprt{}}));
+      }
+    }
+  }
+}