Skip to content

Error handling cleanup in solvers/flattening 6 #2940

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

Error handling cleanup in solvers/flattening 6 #2940

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
60a9d89
Add analysis_exceptiont
danpoe Sep 12, 2018
aa5de1c
Error handling cleanup in solvers/flattening
danpoe Sep 12, 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
2 changes: 0 additions & 2 deletions src/solvers/flattening/bv_minimize.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,6 @@ Author: Georg Weissenbacher, [email protected]

#include "bv_minimize.h"

#include <cassert>

#include <solvers/prop/minimize.h>

void bv_minimizet::add_objective(
Expand Down
92 changes: 45 additions & 47 deletions src/solvers/flattening/bv_pointers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,12 +11,12 @@ Author: Daniel Kroening, [email protected]
#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/config.h>
#include <util/exception_utils.h>
#include <util/pointer_offset_size.h>

literalt bv_pointerst::convert_rest(const exprt &expr)
{
if(expr.type().id()!=ID_bool)
throw "bv_pointerst::convert_rest got non-boolean operand";
PRECONDITION(expr.type().id() == ID_bool);

const exprt::operandst &operands=expr.operands();

Expand Down Expand Up @@ -112,9 +112,6 @@ bool bv_pointerst::convert_address_of_rec(
}
else if(expr.id()==ID_index)
{
if(expr.operands().size()!=2)
throw "index takes two operands";

const index_exprt &index_expr=to_index_expr(expr);
const exprt &array=index_expr.array();
const exprt &index=index_expr.index();
Expand Down Expand Up @@ -182,12 +179,13 @@ bool bv_pointerst::convert_address_of_rec(
// add offset
offset_arithmetic(bv, offset);
}
else if(struct_op_type.id()==ID_union)
else
{
INVARIANT(
struct_op_type.id() == ID_union,
"member expression should operate on struct or union");
// nothing to do, all members have offset 0
}
else
throw "member takes struct or union operand";

return false;
}
Expand Down Expand Up @@ -222,8 +220,7 @@ bool bv_pointerst::convert_address_of_rec(

bvt bv_pointerst::convert_pointer_type(const exprt &expr)
{
if(expr.type().id()!=ID_pointer)
throw "convert_pointer_type got non-pointer type";
PRECONDITION(expr.type().id() == ID_pointer);

// make sure the config hasn't been changed
PRECONDITION(bits==boolbv_width(expr.type()));
Expand Down Expand Up @@ -252,10 +249,9 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
}
else if(expr.id()==ID_typecast)
{
if(expr.operands().size()!=1)
throw "typecast takes one operand";
const typecast_exprt &typecast_expr = to_typecast_expr(expr);

const exprt &op=expr.op0();
const exprt &op = typecast_expr.op();
const typet &op_type=ns.follow(op.type());

if(op_type.id()==ID_pointer)
Expand Down Expand Up @@ -288,15 +284,14 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
}
else if(expr.id()==ID_address_of)
{
if(expr.operands().size()!=1)
throw expr.id_string()+" takes one operand";
const address_of_exprt &address_of_expr = to_address_of_expr(expr);

bvt bv;
bv.resize(bits);

if(convert_address_of_rec(expr.op0(), bv))
if(convert_address_of_rec(address_of_expr.op(), bv))
{
conversion_failed(expr, bv);
conversion_failed(address_of_expr, bv);
return bv;
}

Expand Down Expand Up @@ -324,15 +319,14 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
{
// this has to be pointer plus integer

if(expr.operands().size()<2)
throw "operator + takes at least two operands";
const plus_exprt &plus_expr = to_plus_expr(expr);

bvt bv;

mp_integer size=0;
std::size_t count=0;

forall_operands(it, expr)
forall_operands(it, plus_expr)
{
if(it->type().id()==ID_pointer)
{
Expand All @@ -356,14 +350,13 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
}
}

if(count==0)
throw "found no pointer in pointer-type sum";
else if(count!=1)
throw "found more than one pointer in sum";
INVARIANT(
count == 1,
"there should be exactly one pointer-type operand in a pointer-type sum");

bvt sum=bv_utils.build_constant(0, bits);

forall_operands(it, expr)
forall_operands(it, plus_expr)
{
if(it->type().id()==ID_pointer)
continue;
Expand All @@ -372,7 +365,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
it->type().id()!=ID_signedbv)
{
bvt bv;
conversion_failed(expr, bv);
conversion_failed(plus_expr, bv);
return bv;
}

Expand All @@ -381,9 +374,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
bv_utilst::representationt::UNSIGNED;

bvt op=convert_bv(*it);

if(op.empty())
throw "unexpected pointer arithmetic operand width";
CHECK_RETURN(!op.empty());

// we cut any extra bits off

Expand All @@ -403,27 +394,28 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
{
// this is pointer-integer

if(expr.operands().size()!=2)
throw "operator "+expr.id_string()+" takes two operands";
const minus_exprt &minus_expr = to_minus_expr(expr);

if(expr.op0().type().id()!=ID_pointer)
throw "found no pointer in pointer type in difference";
INVARIANT(
minus_expr.op0().type().id() == ID_pointer,
"first operand should be of pointer type");

bvt bv;

if(expr.op1().type().id()!=ID_unsignedbv &&
expr.op1().type().id()!=ID_signedbv)
if(
minus_expr.op1().type().id() != ID_unsignedbv &&
minus_expr.op1().type().id() != ID_signedbv)
{
bvt bv;
conversion_failed(expr, bv);
conversion_failed(minus_expr, bv);
return bv;
}

const unary_minus_exprt neg_op1(expr.op1());
const unary_minus_exprt neg_op1(minus_expr.op1());

bv=convert_bv(expr.op0());
bv = convert_bv(minus_expr.op0());

typet pointer_sub_type=expr.op0().type().subtype();
typet pointer_sub_type = minus_expr.op0().type().subtype();
mp_integer element_size;

if(pointer_sub_type.id()==ID_empty)
Expand Down Expand Up @@ -462,11 +454,15 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
{
return SUB::convert_byte_extract(to_byte_extract_expr(expr));
}
else if(
expr.id() == ID_byte_update_little_endian ||
expr.id() == ID_byte_update_big_endian)
else
{
throw "byte-wise updates of pointers are unsupported";
INVARIANT(
expr.id() != ID_byte_update_little_endian,
"byte-wise pointer updates are unsupported");

INVARIANT(
expr.id() != ID_byte_update_big_endian,
"byte-wise pointer updates are unsupported");
}

return conversion_failed(expr);
Expand Down Expand Up @@ -723,11 +719,13 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
std::size_t a=pointer_logic.add_object(expr);

const std::size_t max_objects=std::size_t(1)<<object_bits;

if(a==max_objects)
throw
"too many addressed objects: maximum number of objects is set to 2^n="+
std::to_string(max_objects)+" (with n="+std::to_string(object_bits)+"); "+
"use the `--object-bits n` option to increase the maximum number";
throw analysis_exceptiont(
"too many addressed objects: maximum number of objects is set to 2^n=" +
std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
"); " +
"use the `--object-bits n` option to increase the maximum number");

encode(a, bv);
}
Expand Down
Loading