Skip to content

Error handling cleanup in solvers/flattening 2 #2932

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 28, 2018
Merged

Error handling cleanup in solvers/flattening 2 #2932

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
18fbc60
Error handling cleanup in solvers/flattening
danpoe Sep 10, 2018
ce19636
Remove ID_float_debug1 and ID_float_debug2 expressions
danpoe Sep 21, 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
20 changes: 0 additions & 20 deletions src/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2724,26 +2724,6 @@ exprt c_typecheck_baset::do_special_functions(

return tmp;
}
else if(identifier==CPROVER_PREFIX "float_debug1" ||
identifier==CPROVER_PREFIX "float_debug2")
{
if(expr.arguments().size()!=2)
{
err_location(f_op);
error() << "float_debug expects two operands" << eom;
throw 0;
}

const irep_idt &id=
identifier==CPROVER_PREFIX "float_debug1"?
"float_debug1":"float_debug2";

exprt float_debug_expr(id, expr.type());
float_debug_expr.operands()=expr.arguments();
float_debug_expr.add_source_location()=source_location;

return float_debug_expr;
}
else if(identifier=="__sync_fetch_and_add" ||
identifier=="__sync_fetch_and_sub" ||
identifier=="__sync_fetch_and_or" ||
Expand Down
74 changes: 31 additions & 43 deletions src/solvers/flattening/boolbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ Author: Daniel Kroening, [email protected]

#include "boolbv.h"

#include <cassert>
#include <algorithm>
#include <map>
#include <set>

Expand Down Expand Up @@ -36,7 +36,10 @@ bool boolbvt::literal(
{
if(expr.type().id()==ID_bool)
{
assert(bit==0);
INVARIANT(
bit == 0,
"boolean expressions shall be represented by a single bit and hence the "
"only valid bit index is 0");
return prop_conv_solvert::literal(to_symbol_expr(expr), dest);
}
else
Expand All @@ -54,7 +57,8 @@ bool boolbvt::literal(

const boolbv_mapt::map_entryt &map_entry=it_m->second;

assert(bit<map_entry.literal_map.size());
INVARIANT(
bit < map_entry.literal_map.size(), "bit index shall be within bounds");
if(!map_entry.literal_map[bit].is_set)
return true;

Expand All @@ -66,15 +70,11 @@ bool boolbvt::literal(
const index_exprt &index_expr=to_index_expr(expr);

std::size_t element_width=boolbv_width(index_expr.type());
CHECK_RETURN(element_width != 0);

if(element_width==0)
throw "literal expects a bit-vector type";
mp_integer index = numeric_cast_v<mp_integer>(index_expr.index());

mp_integer index;
if(to_integer(index_expr.index(), index))
throw "literal expects constant index";

std::size_t offset=integer2unsigned(index*element_width);
std::size_t offset = numeric_cast_v<std::size_t>(index * element_width);

return literal(index_expr.array(), bit+offset, dest);
}
Expand All @@ -96,18 +96,16 @@ bool boolbvt::literal(
return literal(expr.op0(), bit+offset, dest);

std::size_t element_width=boolbv_width(subtype);

if(element_width==0)
throw "literal expects a bit-vector type";
CHECK_RETURN(element_width != 0);

offset+=element_width;
}

throw "failed to find component";
INVARIANT(false, "struct type should have accessed component");
}
}

throw "found no literal for expression";
INVARIANT(false, "expression should have a corresponding literal");
}

const bvt &
Expand Down Expand Up @@ -305,18 +303,6 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
return convert_not(to_not_expr(expr));
else if(expr.id()==ID_power)
return convert_power(to_binary_expr(expr));
else if(expr.id()==ID_float_debug1 ||
expr.id()==ID_float_debug2)
{
assert(expr.operands().size()==2);
bvt bv0=convert_bitvector(expr.op0());
bvt bv1=convert_bitvector(expr.op1());
float_utilst float_utils(prop, to_floatbv_type(expr.type()));
bvt bv=expr.id()==ID_float_debug1?
float_utils.debug1(bv0, bv1):
float_utils.debug2(bv0, bv1);
return bv;
}
else if(expr.id() == ID_popcount)
return convert_bv(lower_popcount(to_popcount_expr(expr), ns));

Expand All @@ -330,8 +316,8 @@ bvt boolbvt::convert_lambda(const exprt &expr)
if(width==0)
return conversion_failed(expr);

if(expr.operands().size()!=2)
throw "lambda takes two operands";
DATA_INVARIANT(
expr.operands().size() == 2, "lambda expression should have two operands");
Copy link
Contributor Author

Choose a reason for hiding this comment

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

There currently exists a lambda expression type in a non-public repo. @peterschrammel: Should this be pulled out from there and added to std_expr.h?

Copy link
Member

Choose a reason for hiding this comment

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

That's used in cegis. @pkesseli will remove this as soon as the cegis code has been cleaned up.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I've raised an issue for that as well now: #3039


if(expr.type().id()!=ID_array)
return conversion_failed(expr);
Expand All @@ -358,10 +344,12 @@ bvt boolbvt::convert_lambda(const exprt &expr)

const bvt &tmp=convert_bv(expr_op1);

std::size_t offset=integer2unsigned(i*tmp.size());
INVARIANT(
size * tmp.size() == width,
"total bitvector width shall equal the number of operands times the size "
"per operand");

if(size*tmp.size()!=width)
throw "convert_lambda: unexpected operand width";
std::size_t offset = numeric_cast_v<std::size_t>(i * tmp.size());

for(std::size_t j=0; j<tmp.size(); j++)
bv[offset+j]=tmp[j];
Expand Down Expand Up @@ -399,10 +387,8 @@ bvt boolbvt::convert_symbol(const exprt &expr)
bvt bv;
bv.resize(width);

const irep_idt &identifier=expr.get(ID_identifier);

if(identifier.empty())
throw "convert_symbol got empty identifier";
const irep_idt &identifier = expr.get(ID_identifier);
CHECK_RETURN(!identifier.empty());

if(width==0)
{
Expand All @@ -413,13 +399,15 @@ bvt boolbvt::convert_symbol(const exprt &expr)
{
map.get_literals(identifier, type, width, bv);

forall_literals(it, bv)
if(it->var_no()>=prop.no_variables() &&
!it->is_constant())
{
error() << identifier << eom;
assert(false);
}
INVARIANT_WITH_DIAGNOSTICS(
std::all_of(
bv.begin(),
bv.end(),
[this](const literalt &l) {
return l.var_no() < prop.no_variables() || l.is_constant();
}),
"variable number of non-constant literals should be within bounds",
id2string(identifier));
}

return bv;
Expand Down
2 changes: 0 additions & 2 deletions src/util/irep_ids.def
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -514,8 +514,6 @@ IREP_ID_ONE(ptr_object)
IREP_ID_TWO(C_c_sizeof_type, #c_sizeof_type)
IREP_ID_ONE(array_update)
IREP_ID_ONE(update)
IREP_ID_ONE(float_debug1)
IREP_ID_ONE(float_debug2)
IREP_ID_ONE(static_assert)
IREP_ID_ONE(gcc_attribute_mode)
IREP_ID_TWO(built_in, <built-in>)
Expand Down