Add implementation of signed remainder operator (bvsrem).

Along with this, change the tests and implementation of the conversion
function to account for signed/unsigned inputs.

Author: NlightNFotis

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -405,11 +405,24 @@ static smt_termt convert_expr_to_smt(const mod_exprt &truncation_modulo)
     can_cast_type<integer_bitvector_typet>(truncation_modulo.lhs().type()) &&
     can_cast_type<integer_bitvector_typet>(truncation_modulo.rhs().type());
 
+  const bool both_operands_unsigned =
+    can_cast_type<unsignedbv_typet>(truncation_modulo.lhs().type()) &&
+    can_cast_type<unsignedbv_typet>(truncation_modulo.rhs().type());
+
   if(both_operands_bitvector)
   {
-    return smt_bit_vector_theoryt::unsigned_remainder(
-      convert_expr_to_smt(truncation_modulo.lhs()),
-      convert_expr_to_smt(truncation_modulo.rhs()));
+    if(both_operands_unsigned)
+    {
+      return smt_bit_vector_theoryt::unsigned_remainder(
+        convert_expr_to_smt(truncation_modulo.lhs()),
+        convert_expr_to_smt(truncation_modulo.rhs()));
+    }
+    else
+    {
+      return smt_bit_vector_theoryt::signed_remainder(
+        convert_expr_to_smt(truncation_modulo.lhs()),
+        convert_expr_to_smt(truncation_modulo.rhs()));
+    }
   }
   else
   {

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -342,3 +342,26 @@ void smt_bit_vector_theoryt::unsigned_remaindert::validate(
 const smt_function_application_termt::factoryt<
   smt_bit_vector_theoryt::unsigned_remaindert>
   smt_bit_vector_theoryt::unsigned_remainder{};
+
+const char *smt_bit_vector_theoryt::signed_remaindert::identifier()
+{
+  return "bvsrem";
+}
+
+smt_sortt smt_bit_vector_theoryt::signed_remaindert::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::signed_remaindert::validate(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  validate_bit_vector_predicate_arguments(lhs, rhs);
+}
+
+const smt_function_application_termt::factoryt<
+  smt_bit_vector_theoryt::signed_remaindert>
+  smt_bit_vector_theoryt::signed_remainder{};

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -135,6 +135,15 @@ class smt_bit_vector_theoryt
   };
   static const smt_function_application_termt::factoryt<unsigned_remaindert>
     unsigned_remainder;
+
+  struct signed_remaindert 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<signed_remaindert>
+    signed_remainder;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -374,14 +374,22 @@ TEST_CASE(
   }
 
   SECTION(
-    "Unsigned remainder (modulus) from truncating division of two constant "
+    "Remainder (modulus) from truncating division of two constant "
     "size bit-vectors")
   {
+    // Remainder expression with unsigned operands.
     const auto constructed_term =
       convert_expr_to_smt(mod_exprt{one_bvint_unsigned, two_bvint_unsigned});
     const auto expected_term =
       smt_bit_vector_theoryt::unsigned_remainder(smt_term_one, smt_term_two);
     CHECK(constructed_term == expected_term);
+
+    // Remainder expression with signed operands
+    const auto constructed_term_signed =
+      convert_expr_to_smt(mod_exprt{one_bvint, two_bvint});
+    const auto expected_term_signed =
+      smt_bit_vector_theoryt::signed_remainder(smt_term_one, smt_term_two);
+    CHECK(constructed_term_signed == expected_term_signed);
   }
 
   SECTION(

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -288,4 +288,23 @@ TEST_CASE(
     // A remainder of a bool and a bitvector should hit an invariant violation.
     REQUIRE_THROWS(smt_bit_vector_theoryt::unsigned_remainder(true_val, three));
   }
+
+  SECTION("Signed Remainder")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::signed_remainder(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvsrem", 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;
+    // Bit-vectors of mismatched sorts are going to hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::signed_remainder(three, four));
+    // A remainder of a bool and a bitvector should hit an invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::signed_remainder(true_val, three));
+  }
 }