Skip to content

Invariant cleanup in flattening/boolbv_index #3044

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 2 commits into from
Sep 27, 2018
Merged

Invariant cleanup in flattening/boolbv_index #3044

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
af1d428
Replace to_integer with numeric_cast in boolbv_index
hannes-steffenhagen-diffblue Sep 24, 2018
7baf62d
Replace throws and asserts with invariants in boolbv_index
hannes-steffenhagen-diffblue Sep 24, 2018
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
50 changes: 24 additions & 26 deletions src/solvers/flattening/boolbv_index.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -61,16 +61,17 @@ bvt boolbvt::convert_index(const index_exprt &expr)
}

// Must have a finite size
mp_integer array_size;
if(to_integer(array_type.size(), array_size))
throw "failed to convert array size";

// see if the index address is constant
// many of these are compacted by simplify_expr
// but variable location writes will block this
mp_integer index_value;
if(!to_integer(index, index_value))
return convert_index(array, index_value);
mp_integer array_size = numeric_cast_v<mp_integer>(array_type.size());
{
// see if the index address is constant
// many of these are compacted by simplify_expr
// but variable location writes will block this
auto maybe_index_value = numeric_cast<mp_integer>(index);
if(maybe_index_value.has_value())
{
return convert_index(array, maybe_index_value.value());
}
}

// Special case : arrays of one thing (useful for constants)
// TODO : merge with ACTUAL_ARRAY_HACK so that ranges of the same
Expand Down Expand Up @@ -115,12 +116,10 @@ bvt boolbvt::convert_index(const index_exprt &expr)

binary_relation_exprt lower_bound(
from_integer(0, index.type()), ID_le, index);
CHECK_RETURN(lower_bound.lhs().is_not_nil());
binary_relation_exprt upper_bound(
index, ID_lt, from_integer(array_size, index.type()));

if(lower_bound.lhs().is_nil() ||
upper_bound.rhs().is_nil())
throw "number conversion failed (2)";
CHECK_RETURN(upper_bound.rhs().is_not_nil());

and_exprt range_condition(lower_bound, upper_bound);
implies_exprt implication(range_condition, value_equality);
Expand Down Expand Up @@ -172,11 +171,12 @@ bvt boolbvt::convert_index(const index_exprt &expr)
for(mp_integer i=0; i<array_size; i=i+1)
{
index_equality.rhs()=from_integer(i, index_equality.lhs().type());
CHECK_RETURN(index_equality.rhs().is_not_nil());

if(index_equality.rhs().is_nil())
throw "number conversion failed (1)";

assert(it != array.operands().end());
INVARIANT(
it != array.operands().end(),
"this loop iterates over the array, so `it` shouldn't be increased "
"past the array's end");

value_equality.rhs()=*it++;

Expand All @@ -198,10 +198,8 @@ bvt boolbvt::convert_index(const index_exprt &expr)

// get literals for the whole array

const bvt &array_bv=convert_bv(array);

if(array_size*width!=array_bv.size())
throw "unexpected array size";
const bvt &array_bv =
convert_bv(array, numeric_cast_v<std::size_t>(array_size * width));

// TODO: maybe a shifter-like construction would be better
// Would be a lot more compact but propagate worse
Expand Down Expand Up @@ -229,9 +227,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
for(mp_integer i=0; i<array_size; i=i+1)
{
index_equality.rhs()=from_integer(i, index_equality.lhs().type());

if(index_equality.rhs().is_nil())
throw "number conversion failed (1)";
CHECK_RETURN(index_equality.rhs().is_not_nil());

mp_integer offset=i*width;

Expand All @@ -256,7 +252,9 @@ bvt boolbvt::convert_index(const index_exprt &expr)

typet constant_type=index.type(); // type of index operand

assert(array_size>0);
Copy link
Contributor

Choose a reason for hiding this comment

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

My only request is perhaps a better error message here? This shows what's going on, but not why. But I'm not too fussed about it to be honest.

DATA_INVARIANT(
array_size > 0,
"non-positive array sizes are forbidden in goto programs");

for(mp_integer i=0; i<array_size; i=i+1)
{
Expand Down