Skip to content

New SMT2 backend: arithmetic operators implementation for fixed size bit vectors #6614

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 9 commits into from
Feb 3, 2022
Merged

New SMT2 backend: arithmetic operators implementation for fixed size bit vectors #6614

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
426aebb
Add implementation of arithmetic operator `bvadd`.
NlightNFotis Jan 27, 2022
7488488
Add implementation of arithmetic operator `bvsub`.
NlightNFotis Feb 1, 2022
5538759
Add implementation of multiplication operator `bvmul`.
NlightNFotis Jan 27, 2022
149f7e4
Add implementation of (unsigned) division operator `bvudiv`.
NlightNFotis Jan 28, 2022
0c4a39b
Add implementation of (signed) division operator (`bvsdiv`).
NlightNFotis Feb 2, 2022
f259dc0
Add (unsigned) remainder (modulus) arithmetic operator `bvurem`.
NlightNFotis Jan 28, 2022
a1c923c
Add implementation of signed remainder operator (`bvsrem`).
NlightNFotis Feb 2, 2022
10a2a53
Add implementation of negation (unary minus - `bvneg`) operator.
NlightNFotis Jan 28, 2022
b11a3b2
Rename `validate_bit_vector_predicate_arguments` to `validate_bit_vec…
NlightNFotis Feb 2, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
125 changes: 111 additions & 14 deletions src/solvers/smt2_incremental/convert_expr_to_smt.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -154,9 +154,19 @@ static smt_termt convert_expr_to_smt(const bitnot_exprt &bitwise_not)

static smt_termt convert_expr_to_smt(const unary_minus_exprt &unary_minus)
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for unary minus expression: " +
unary_minus.pretty());
const bool operand_is_bitvector =
can_cast_type<integer_bitvector_typet>(unary_minus.op().type());
if(operand_is_bitvector)
{
return smt_bit_vector_theoryt::negate(
convert_expr_to_smt(unary_minus.op()));
}
else
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for unary minus expression: " +
unary_minus.pretty());
}
}

static smt_termt convert_expr_to_smt(const unary_plus_exprt &unary_plus)
Expand Down Expand Up @@ -326,20 +336,67 @@ static optionalt<smt_termt> try_relational_conversion(const exprt &expr)

static smt_termt convert_expr_to_smt(const plus_exprt &plus)
{
UNIMPLEMENTED_FEATURE(
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ I would prefer it if commits could be titled such that the title encompasses the entirety of what they change. The fact that you effectively have "Also add conversion of plus_exprt to smt_bit_vector_theoryt::addition" in the message body is kind of a red flag which suggests that you have combined unrelated changes together (even if one change depends of the other).

"Generation of SMT formula for plus expression: " + plus.pretty());
if(std::all_of(
plus.operands().cbegin(), plus.operands().cend(), [](exprt operand) {
return can_cast_type<integer_bitvector_typet>(operand.type());
}))
{
return convert_multiary_operator_to_terms(
plus, smt_bit_vector_theoryt::add);
}
else
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for plus expression: " + plus.pretty());
}
}

static smt_termt convert_expr_to_smt(const minus_exprt &minus)
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for minus expression: " + minus.pretty());
const bool both_operands_bitvector =
can_cast_type<integer_bitvector_typet>(minus.lhs().type()) &&
can_cast_type<integer_bitvector_typet>(minus.rhs().type());

if(both_operands_bitvector)
{
return smt_bit_vector_theoryt::subtract(
convert_expr_to_smt(minus.lhs()), convert_expr_to_smt(minus.rhs()));
}
else
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for minus expression: " + minus.pretty());
}
}

static smt_termt convert_expr_to_smt(const div_exprt &divide)
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for divide expression: " + divide.pretty());
const bool both_operands_bitvector =
can_cast_type<integer_bitvector_typet>(divide.lhs().type()) &&
can_cast_type<integer_bitvector_typet>(divide.rhs().type());

const bool both_operands_unsigned =
can_cast_type<unsignedbv_typet>(divide.lhs().type()) &&
can_cast_type<unsignedbv_typet>(divide.rhs().type());

if(both_operands_bitvector)
{
if(both_operands_unsigned)
{
return smt_bit_vector_theoryt::unsigned_divide(
convert_expr_to_smt(divide.lhs()), convert_expr_to_smt(divide.rhs()));
}
else
{
return smt_bit_vector_theoryt::signed_divide(
convert_expr_to_smt(divide.lhs()), convert_expr_to_smt(divide.rhs()));
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 I suggest introducing lhs_term and rhs_term variables above this if statement, so that the calls to convert_expr_to_smt are not duplicated in the two branches.

}
}
else
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for divide expression: " + divide.pretty());
}
}

static smt_termt convert_expr_to_smt(const ieee_float_op_exprt &float_operation)
Expand All @@ -353,9 +410,35 @@ static smt_termt convert_expr_to_smt(const ieee_float_op_exprt &float_operation)

static smt_termt convert_expr_to_smt(const mod_exprt &truncation_modulo)
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for truncation modulo expression: " +
truncation_modulo.pretty());
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ We expect this operator to be applied only to (signed/unsigned) integer bit vectors. It might be good to document this expectation using a UNEXPECTEDCASE macro, similar to how smt2_convt::convert_mod does this.

const bool both_operands_bitvector =
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)
{
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()));
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Factor out the common convert_expr_to_smt sub-expressions, like I suggested with your implementation for the divide operations.

}
}
else
{
UNIMPLEMENTED_FEATURE(
"Generation of SMT formula for remainder (modulus) expression: " +
truncation_modulo.pretty());
}
}

static smt_termt
Expand All @@ -368,8 +451,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)
Expand Down
Loading