Skip to content

Commit 5538759

Browse files
committed
Add implementation of multiplication operator bvmul.
Also add tests for its conversion from `mult_exprt` and of the factory integrity.
1 parent 7488488 commit 5538759

File tree

5 files changed

+84
-2
lines changed

5 files changed

+84
-2
lines changed

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -391,8 +391,22 @@ convert_expr_to_smt(const euclidean_mod_exprt &euclidean_modulo)
391391

392392
static smt_termt convert_expr_to_smt(const mult_exprt &multiply)
393393
{
394-
UNIMPLEMENTED_FEATURE(
395-
"Generation of SMT formula for multiply expression: " + multiply.pretty());
394+
if(std::all_of(
395+
multiply.operands().cbegin(),
396+
multiply.operands().cend(),
397+
[](exprt operand) {
398+
return can_cast_type<integer_bitvector_typet>(operand.type());
399+
}))
400+
{
401+
return convert_multiary_operator_to_terms(
402+
multiply, smt_bit_vector_theoryt::multiply);
403+
}
404+
else
405+
{
406+
UNIMPLEMENTED_FEATURE(
407+
"Generation of SMT formula for multiply expression: " +
408+
multiply.pretty());
409+
}
396410
}
397411

398412
static smt_termt convert_expr_to_smt(const address_of_exprt &address_of)

src/solvers/smt2_incremental/smt_bit_vector_theory.cpp

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -250,3 +250,26 @@ void smt_bit_vector_theoryt::subtractt::validate(
250250
const smt_function_application_termt::factoryt<
251251
smt_bit_vector_theoryt::subtractt>
252252
smt_bit_vector_theoryt::subtract{};
253+
254+
const char *smt_bit_vector_theoryt::multiplyt::identifier()
255+
{
256+
return "bvmul";
257+
}
258+
259+
smt_sortt smt_bit_vector_theoryt::multiplyt::return_sort(
260+
const smt_termt &lhs,
261+
const smt_termt &rhs)
262+
{
263+
return lhs.get_sort();
264+
}
265+
266+
void smt_bit_vector_theoryt::multiplyt::validate(
267+
const smt_termt &lhs,
268+
const smt_termt &rhs)
269+
{
270+
validate_bit_vector_predicate_arguments(lhs, rhs);
271+
}
272+
273+
const smt_function_application_termt::factoryt<
274+
smt_bit_vector_theoryt::multiplyt>
275+
smt_bit_vector_theoryt::multiply{};

src/solvers/smt2_incremental/smt_bit_vector_theory.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,14 @@ class smt_bit_vector_theoryt
100100
static void validate(const smt_termt &lhs, const smt_termt &rhs);
101101
};
102102
static const smt_function_application_termt::factoryt<subtractt> subtract;
103+
104+
struct multiplyt final
105+
{
106+
static const char *identifier();
107+
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs);
108+
static void validate(const smt_termt &lhs, const smt_termt &rhs);
109+
};
110+
static const smt_function_application_termt::factoryt<multiplyt> multiply;
103111
};
104112

105113
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -328,4 +328,21 @@ TEST_CASE(
328328
REQUIRE_THROWS(
329329
convert_expr_to_smt(minus_exprt{true_exprt{}, false_exprt{}}));
330330
}
331+
332+
SECTION("Multiplication of two constant size bit-vectors")
333+
{
334+
const auto constructed_term =
335+
convert_expr_to_smt(mult_exprt{one_bvint, two_bvint});
336+
const auto expected_term =
337+
smt_bit_vector_theoryt::multiply(smt_term_one, smt_term_two);
338+
CHECK(constructed_term == expected_term);
339+
}
340+
341+
SECTION(
342+
"Ensure that multiplication node conversion fails if the operands are not "
343+
"bit-vector based")
344+
{
345+
const cbmc_invariants_should_throwt invariants_throw;
346+
REQUIRE_THROWS(convert_expr_to_smt(mult_exprt{one_bvint, false_exprt{}}));
347+
}
331348
}

unit/solvers/smt2_incremental/smt_bit_vector_theory.cpp

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -213,4 +213,24 @@ TEST_CASE(
213213
// invariant violation.
214214
REQUIRE_THROWS(smt_bit_vector_theoryt::subtract(true_val, three));
215215
}
216+
217+
SECTION("Multiplication")
218+
{
219+
const auto function_application =
220+
smt_bit_vector_theoryt::multiply(two, three);
221+
REQUIRE(
222+
function_application.function_identifier() ==
223+
smt_identifier_termt("bvmul", smt_bit_vector_sortt{8}));
224+
REQUIRE(function_application.get_sort() == smt_bit_vector_sortt{8});
225+
REQUIRE(function_application.arguments().size() == 2);
226+
REQUIRE(function_application.arguments()[0].get() == two);
227+
REQUIRE(function_application.arguments()[1].get() == three);
228+
229+
cbmc_invariants_should_throwt invariants_throw;
230+
// Bit-vectors of mismatched sorts are going to hit an invariant violation.
231+
REQUIRE_THROWS(smt_bit_vector_theoryt::multiply(three, four));
232+
// A multiplication of a bool and a bitvector should hit an
233+
// invariant violation.
234+
REQUIRE_THROWS(smt_bit_vector_theoryt::multiply(true_val, three));
235+
}
216236
}

0 commit comments

Comments
 (0)