Add implementation of multiplication operator bvmul.

Also add tests for its conversion from `mult_exprt` and of the factory
integrity.

Author: NlightNFotis

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -391,8 +391,22 @@ convert_expr_to_smt(const euclidean_mod_exprt &euclidean_modulo)
 
 static smt_termt convert_expr_to_smt(const mult_exprt &multiply)
 {
-  UNIMPLEMENTED_FEATURE(
-    "Generation of SMT formula for multiply expression: " + multiply.pretty());
+  if(std::all_of(
+       multiply.operands().cbegin(),
+       multiply.operands().cend(),
+       [](exprt operand) {
+         return can_cast_type<integer_bitvector_typet>(operand.type());
+       }))
+  {
+    return convert_multiary_operator_to_terms(
+      multiply, smt_bit_vector_theoryt::multiply);
+  }
+  else
+  {
+    UNIMPLEMENTED_FEATURE(
+      "Generation of SMT formula for multiply expression: " +
+      multiply.pretty());
+  }
 }
 
 static smt_termt convert_expr_to_smt(const address_of_exprt &address_of)

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -250,3 +250,26 @@ void smt_bit_vector_theoryt::subtractt::validate(
 const smt_function_application_termt::factoryt<
   smt_bit_vector_theoryt::subtractt>
   smt_bit_vector_theoryt::subtract{};
+
+const char *smt_bit_vector_theoryt::multiplyt::identifier()
+{
+  return "bvmul";
+}
+
+smt_sortt smt_bit_vector_theoryt::multiplyt::return_sort(
+  const smt_termt &lhs,
+  const smt_termt &rhs)
+{
+  return lhs.get_sort();
+}
+
+void smt_bit_vector_theoryt::multiplyt::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::multiplyt>
+  smt_bit_vector_theoryt::multiply{};

src/solvers/smt2_incremental/smt_bit_vector_theory.h

@@ -100,6 +100,14 @@ class smt_bit_vector_theoryt
     static void validate(const smt_termt &lhs, const smt_termt &rhs);
   };
   static const smt_function_application_termt::factoryt<subtractt> subtract;
+
+  struct multiplyt 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<multiplyt> multiply;
 };
 
 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -328,4 +328,21 @@ TEST_CASE(
     REQUIRE_THROWS(
       convert_expr_to_smt(minus_exprt{true_exprt{}, false_exprt{}}));
   }
+
+  SECTION("Multiplication of two constant size bit-vectors")
+  {
+    const auto constructed_term =
+      convert_expr_to_smt(mult_exprt{one_bvint, two_bvint});
+    const auto expected_term =
+      smt_bit_vector_theoryt::multiply(smt_term_one, smt_term_two);
+    CHECK(constructed_term == expected_term);
+  }
+
+  SECTION(
+    "Ensure that multiplication node conversion fails if the operands are not "
+    "bit-vector based")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    REQUIRE_THROWS(convert_expr_to_smt(mult_exprt{one_bvint, false_exprt{}}));
+  }
 }

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

@@ -213,4 +213,24 @@ TEST_CASE(
     // invariant violation.
     REQUIRE_THROWS(smt_bit_vector_theoryt::subtract(true_val, three));
   }
+
+  SECTION("Multiplication")
+  {
+    const auto function_application =
+      smt_bit_vector_theoryt::multiply(two, three);
+    REQUIRE(
+      function_application.function_identifier() ==
+      smt_identifier_termt("bvmul", 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::multiply(three, four));
+    // A multiplication of a bool and a bitvector should hit an
+    // invariant violation.
+    REQUIRE_THROWS(smt_bit_vector_theoryt::multiply(true_val, three));
+  }
 }