Skip to content

Refactor boolbvt::convert_overflow #6752

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 5 commits into from
Mar 24, 2022
Merged

Refactor boolbvt::convert_overflow #6752

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
e884c43
Split `convert_overflow` into binary and unary variations
thomasspriggs Mar 23, 2022
c0797f9
Factor out conversion of operands for `binary_overflow_exprt`
thomasspriggs Mar 23, 2022
9b1a388
Factor out working out signedness in `convert_binary_overflow`
thomasspriggs Mar 23, 2022
c5c5e91
Use can_cast_type inplace of type id in `convert_binary_overflow`
thomasspriggs Mar 23, 2022
fad0e20
Remove lambda in `convert_binary_overflow`
thomasspriggs Mar 23, 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
12 changes: 9 additions & 3 deletions src/solvers/flattening/boolbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -417,10 +417,16 @@ literalt boolbvt::convert_rest(const exprt &expr)
else if(expr.id()==ID_onehot || expr.id()==ID_onehot0)
return convert_onehot(to_unary_expr(expr));
else if(
can_cast_expr<binary_overflow_exprt>(expr) ||
can_cast_expr<unary_minus_overflow_exprt>(expr))
const auto binary_overflow =
expr_try_dynamic_cast<binary_overflow_exprt>(expr))
{
return convert_overflow(expr);
return convert_binary_overflow(*binary_overflow);
}
else if(
const auto unary_overflow =
expr_try_dynamic_cast<unary_overflow_exprt>(expr))
{
return convert_unary_overflow(*unary_overflow);
}
else if(expr.id()==ID_isnan)
{
Expand Down
5 changes: 4 additions & 1 deletion src/solvers/flattening/boolbv.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
#include "arrays.h"

class array_comprehension_exprt;
class binary_overflow_exprt;
class bitreverse_exprt;
class bswap_exprt;
class byte_extract_exprt;
Expand All @@ -38,6 +39,7 @@ class floatbv_typecast_exprt;
class ieee_float_op_exprt;
class member_exprt;
class replication_exprt;
class unary_overflow_exprt;
class union_typet;

class boolbvt:public arrayst
Expand Down Expand Up @@ -140,7 +142,8 @@ class boolbvt:public arrayst
virtual literalt convert_reduction(const unary_exprt &expr);
virtual literalt convert_onehot(const unary_exprt &expr);
virtual literalt convert_extractbit(const extractbit_exprt &expr);
virtual literalt convert_overflow(const exprt &expr);
virtual literalt convert_binary_overflow(const binary_overflow_exprt &expr);
virtual literalt convert_unary_overflow(const unary_overflow_exprt &expr);
virtual literalt convert_equality(const equal_exprt &expr);
virtual literalt convert_verilog_case_equality(
const binary_relation_exprt &expr);
Expand Down
82 changes: 37 additions & 45 deletions src/solvers/flattening/boolbv_overflow.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,55 +7,49 @@ Author: Daniel Kroening, [email protected]
\*******************************************************************/

#include <util/bitvector_expr.h>
#include <util/bitvector_types.h>
#include <util/invariant.h>

#include "boolbv.h"

literalt boolbvt::convert_overflow(const exprt &expr)
literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr)
{
const auto plus_or_minus_conversion =
[&](
const binary_overflow_exprt &overflow_expr,
const std::function<literalt(
bv_utilst *, const bvt &, const bvt &, bv_utilst::representationt)>
&bv_util_overflow) {
const bvt &bv0 = convert_bv(overflow_expr.lhs());
const bvt &bv1 = convert_bv(overflow_expr.rhs());

if(bv0.size() != bv1.size())
return SUB::convert_rest(expr);

bv_utilst::representationt rep =
overflow_expr.lhs().type().id() == ID_signedbv
? bv_utilst::representationt::SIGNED
: bv_utilst::representationt::UNSIGNED;

return bv_util_overflow(&bv_utils, bv0, bv1, rep);
};
const bvt &bv0 = convert_bv(expr.lhs());
const bvt &bv1 = convert_bv(
expr.rhs(),
can_cast_expr<mult_overflow_exprt>(expr)
? optionalt<std::size_t>{bv0.size()}
: nullopt);

const bv_utilst::representationt rep =
can_cast_type<signedbv_typet>(expr.lhs().type())
? bv_utilst::representationt::SIGNED
: bv_utilst::representationt::UNSIGNED;

if(
const auto plus_overflow = expr_try_dynamic_cast<plus_overflow_exprt>(expr))
{
return plus_or_minus_conversion(*plus_overflow, &bv_utilst::overflow_add);
if(bv0.size() != bv1.size())
return SUB::convert_rest(expr);

return bv_utils.overflow_add(bv0, bv1, rep);
}
if(const auto minus = expr_try_dynamic_cast<minus_overflow_exprt>(expr))
{
return plus_or_minus_conversion(*minus, &bv_utilst::overflow_sub);
if(bv0.size() != bv1.size())
return SUB::convert_rest(expr);

return bv_utils.overflow_sub(bv0, bv1, rep);
}
else if(
const auto mult_overflow = expr_try_dynamic_cast<mult_overflow_exprt>(expr))
{
if(
mult_overflow->lhs().type().id() != ID_unsignedbv &&
mult_overflow->lhs().type().id() != ID_signedbv)
!can_cast_type<unsignedbv_typet>(expr.lhs().type()) &&
!can_cast_type<signedbv_typet>(expr.lhs().type()))
{
return SUB::convert_rest(expr);

bvt bv0 = convert_bv(mult_overflow->lhs());
bvt bv1 = convert_bv(mult_overflow->rhs(), bv0.size());

bv_utilst::representationt rep =
mult_overflow->lhs().type().id() == ID_signedbv
? bv_utilst::representationt::SIGNED
: bv_utilst::representationt::UNSIGNED;
}

DATA_INVARIANT(
mult_overflow->lhs().type() == mult_overflow->rhs().type(),
Expand All @@ -65,10 +59,10 @@ literalt boolbvt::convert_overflow(const exprt &expr)
std::size_t new_size=old_size*2;

// sign/zero extension
bv0=bv_utils.extension(bv0, new_size, rep);
bv1=bv_utils.extension(bv1, new_size, rep);
const bvt &bv0_extended = bv_utils.extension(bv0, new_size, rep);
const bvt &bv1_extended = bv_utils.extension(bv1, new_size, rep);

bvt result=bv_utils.multiplier(bv0, bv1, rep);
bvt result = bv_utils.multiplier(bv0_extended, bv1_extended, rep);

if(rep==bv_utilst::representationt::UNSIGNED)
{
Expand Down Expand Up @@ -100,23 +94,15 @@ literalt boolbvt::convert_overflow(const exprt &expr)
else if(
const auto shl_overflow = expr_try_dynamic_cast<shl_overflow_exprt>(expr))
{
const bvt &bv0 = convert_bv(shl_overflow->lhs());
const bvt &bv1 = convert_bv(shl_overflow->rhs());

std::size_t old_size = bv0.size();
std::size_t new_size = old_size * 2;

bv_utilst::representationt rep =
shl_overflow->lhs().type().id() == ID_signedbv
? bv_utilst::representationt::SIGNED
: bv_utilst::representationt::UNSIGNED;

bvt bv_ext=bv_utils.extension(bv0, new_size, rep);

bvt result=bv_utils.shift(bv_ext, bv_utilst::shiftt::SHIFT_LEFT, bv1);

// a negative shift is undefined; yet this isn't an overflow
literalt neg_shift = shl_overflow->lhs().type().id() == ID_unsignedbv
literalt neg_shift = rep == bv_utilst::representationt::UNSIGNED
? const_literal(false)
: bv1.back(); // sign bit

Expand Down Expand Up @@ -161,7 +147,13 @@ literalt boolbvt::convert_overflow(const exprt &expr)
return
prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), overflow));
}
else if(

return SUB::convert_rest(expr);
}

literalt boolbvt::convert_unary_overflow(const unary_overflow_exprt &expr)
{
if(
Comment on lines +154 to +156
Copy link
Collaborator

Choose a reason for hiding this comment

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

There really is just this single unary_minus_overflow_exprt that exists for this case, so I would suggest to make this convert_unary_minus_overflow(const unary_minus_overflow_exprt &expr).

Copy link
Contributor Author

Choose a reason for hiding this comment

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

unary_minus_overflow_exprt and unary_overflow_exprt are currently equivalent. This fact could be used to simplify the way they are currently used, or even to remove unary_overflow_exprt and just keep unary_minus_overflow_exprt. However I think it would make it more difficult to add other kinds of unary overflow expressions. Adding more checks isn't something I am planning to work on but does seem worth considering. The following example unary operations might be considered for overflow checks -

  • The existing abs_exprt.
  • Increment operators ++ / --.
  • The trigonometric tan / "tangent" operation.
  • Could a narrowing cast be considered to overflow?

const auto unary_minus_overflow =
expr_try_dynamic_cast<unary_minus_overflow_exprt>(expr))
{
Expand Down