Skip to content

Error handling cleanup in solvers/flattening 7 #2944

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 1 commit into from
Sep 28, 2018
Merged

Error handling cleanup in solvers/flattening 7 #2944

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
10 changes: 4 additions & 6 deletions src/solvers/flattening/equality.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,10 +24,9 @@ literalt equalityt::equality(const exprt &e1, const exprt &e2)

literalt equalityt::equality2(const exprt &e1, const exprt &e2)
{
const typet &type=e1.type();
PRECONDITION(e1.type() == e2.type());

if(e2.type()!=e1.type())
throw "equality got different types";
const typet &type = e1.type();

// check for syntactical equality

Expand All @@ -36,9 +35,8 @@ literalt equalityt::equality2(const exprt &e1, const exprt &e2)

// check for boolean equality

if(type.id()==ID_bool)
throw "equalityt got boolean equality";
// return lequal(convert(e1), convert(e2));
INVARIANT(
type.id() != ID_bool, "method shall not be used to compare Boolean types");

// look it up

Expand Down
136 changes: 72 additions & 64 deletions src/solvers/flattening/flatten_byte_operators.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,12 +51,15 @@ static exprt unpack_rec(
mp_integer element_width=pointer_offset_bits(subtype, ns);
// this probably doesn't really matter
#if 0
if(element_width<=0)
throw "cannot unpack array with non-constant element width:\n"+
type.pretty();
else if(element_width%8!=0)
throw "cannot unpack array of non-byte aligned elements:\n"+
type.pretty();
INVARIANT(
element_width > 0,
"element width of array should be constant",
irep_pretty_diagnosticst(type));

INVARIANT(
element_width % 8 == 0,
"elements in array should be byte-aligned",
irep_pretty_diagnosticst(type));
#endif

if(!unpack_byte_array && element_width==8)
Expand Down Expand Up @@ -199,8 +202,6 @@ exprt flatten_byte_extract(
// big-endian: (short)concatenation(01,02)=0x0102
// little-endian: (short)concatenation(03,04)=0x0304

assert(src.operands().size()==2);

PRECONDITION(
src.id() == ID_byte_extract_little_endian ||
src.id() == ID_byte_extract_big_endian);
Expand Down Expand Up @@ -345,14 +346,14 @@ exprt flatten_byte_update(
const namespacet &ns,
bool negative_offset)
{
assert(src.operands().size()==3);
mp_integer element_size = pointer_offset_size(src.value().type(), ns);

mp_integer element_size=
pointer_offset_size(src.op2().type(), ns);
if(element_size<0)
throw "byte_update of unknown width:\n"+src.pretty();
INVARIANT_WITH_DIAGNOSTICS(
element_size >= 0,
"size of type in bytes must be known",
irep_pretty_diagnosticst(src));

const typet &t=ns.follow(src.op0().type());
const typet &t = ns.follow(src.op().type());

if(t.id()==ID_array)
{
Expand All @@ -368,44 +369,48 @@ exprt flatten_byte_update(
{
mp_integer sub_size=pointer_offset_size(subtype, ns);

if(sub_size==-1)
throw "can't flatten byte_update for sub-type without size";
INVARIANT(
sub_size >= 0,
"bit width (rounded to full bytes) of subtype must be known");

// byte array?
if(sub_size==1)
{
// apply 'array-update-with' element_size times
exprt result=src.op0();
exprt result = src.op();

for(mp_integer i=0; i<element_size; ++i)
{
exprt i_expr=from_integer(i, ns.follow(src.op1().type()));
exprt i_expr = from_integer(i, ns.follow(src.offset().type()));

exprt new_value;

if(i==0 && element_size==1) // bytes?
{
new_value=src.op2();
new_value = src.value();
if(new_value.type()!=subtype)
new_value.make_typecast(subtype);
}
else
{
INVARIANT(
src.id() == ID_byte_update_little_endian ||
src.id() == ID_byte_update_big_endian,
"byte update expression should either be little or big endian");

byte_extract_exprt byte_extract_expr(
src.id()==ID_byte_update_little_endian?
ID_byte_extract_little_endian:
src.id()==ID_byte_update_big_endian?
ID_byte_extract_big_endian:
throw "unexpected src.id() in flatten_byte_update",
src.id() == ID_byte_update_little_endian
? ID_byte_extract_little_endian
: ID_byte_extract_big_endian,
subtype);

byte_extract_expr.op()=src.op2();
byte_extract_expr.op() = src.value();
byte_extract_expr.offset()=i_expr;

new_value=flatten_byte_extract(byte_extract_expr, ns);
}

const plus_exprt where(src.op1(), i_expr);
const plus_exprt where(src.offset(), i_expr);

with_exprt with_expr(result, where, new_value);
with_expr.type()=src.type();
Expand All @@ -417,34 +422,34 @@ exprt flatten_byte_update(
}
else // sub_size!=1
{
exprt result=src.op0();
exprt result = src.op();

// Number of potentially affected array cells:
mp_integer num_elements=
element_size/sub_size+((element_size%sub_size==0)?1:2);

const auto &offset_type=ns.follow(src.op1().type());
const auto &offset_type = ns.follow(src.offset().type());
exprt zero_offset=from_integer(0, offset_type);

exprt sub_size_expr=from_integer(sub_size, offset_type);
exprt element_size_expr=from_integer(element_size, offset_type);

// First potentially affected cell:
div_exprt first_cell(src.op1(), sub_size_expr);
div_exprt first_cell(src.offset(), sub_size_expr);

for(mp_integer i=0; i<num_elements; ++i)
{
plus_exprt cell_index(first_cell, from_integer(i, offset_type));
mult_exprt cell_offset(cell_index, sub_size_expr);
index_exprt old_cell_value(src.op0(), cell_index, subtype);
index_exprt old_cell_value(src.op(), cell_index, subtype);
bool is_first_cell=i==0;
bool is_last_cell=i==num_elements-1;

exprt new_value;
exprt stored_value_offset;
if(element_size<=sub_size)
{
new_value=src.op2();
new_value = src.value();
stored_value_offset=zero_offset;
}
else
Expand All @@ -458,19 +463,20 @@ exprt flatten_byte_update(
stored_value_offset=
from_integer(element_size-sub_size, offset_type);
else
stored_value_offset=minus_exprt(cell_offset, src.op1());

auto extract_opcode=
src.id()==ID_byte_update_little_endian ?
ID_byte_extract_little_endian :
src.id()==ID_byte_update_big_endian ?
ID_byte_extract_big_endian :
throw "unexpected src.id() in flatten_byte_update";
stored_value_offset = minus_exprt(cell_offset, src.offset());

INVARIANT(
src.id() == ID_byte_update_little_endian ||
src.id() == ID_byte_update_big_endian,
"byte update expression should either be little or big endian");

byte_extract_exprt byte_extract_expr(
extract_opcode,
element_size<sub_size ? src.op2().type() : subtype);
src.id() == ID_byte_update_little_endian
? ID_byte_extract_little_endian
: ID_byte_extract_big_endian,
element_size < sub_size ? src.value().type() : subtype);

byte_extract_expr.op()=src.op2();
byte_extract_expr.op() = src.value();
byte_extract_expr.offset()=stored_value_offset;

new_value=flatten_byte_extract(byte_extract_expr, ns);
Expand All @@ -482,15 +488,13 @@ exprt flatten_byte_update(
// target array cell.
exprt overwrite_offset;
if(is_first_cell)
overwrite_offset=mod_exprt(src.op1(), sub_size_expr);
overwrite_offset = mod_exprt(src.offset(), sub_size_expr);
else if(is_last_cell)
{
// This is intentionally negated; passing is_last_cell
// to flatten below leads to it being negated again later.
overwrite_offset=
minus_exprt(
minus_exprt(cell_offset, src.op1()),
stored_value_offset);
overwrite_offset = minus_exprt(
minus_exprt(cell_offset, src.offset()), stored_value_offset);
}
else
overwrite_offset=zero_offset;
Expand All @@ -517,9 +521,10 @@ exprt flatten_byte_update(
}
else
{
throw
"flatten_byte_update can only do arrays of scalars right now, "
"but got "+subtype.id_string();
PRECONDITION_WITH_DIAGNOSTICS(
false,
"flatten_byte_update can only do arrays of scalars right now",
subtype.id_string());
}
}
else if(t.id()==ID_signedbv ||
Expand All @@ -530,11 +535,12 @@ exprt flatten_byte_update(
{
// do a shift, mask and OR
mp_integer type_width=pointer_offset_bits(t, ns);
assert(type_width>0);
CHECK_RETURN(type_width > 0);
std::size_t width=integer2size_t(type_width);

if(element_size*8>width)
throw "flatten_byte_update to update element that is too large";
INVARIANT(
element_size * 8 <= width,
"element bit width must not be larger than width indicated by type");

// build mask
exprt mask=
Expand All @@ -544,16 +550,16 @@ exprt flatten_byte_update(
exprt value_extended;

if(width>integer2unsigned(element_size)*8)
value_extended=
concatenation_exprt(
from_integer(
0, unsignedbv_typet(width-integer2unsigned(element_size)*8)),
src.op2(), t);
value_extended = concatenation_exprt(
from_integer(
0, unsignedbv_typet(width - integer2unsigned(element_size) * 8)),
src.value(),
t);
else
value_extended=src.op2();
value_extended = src.value();

const typet &offset_type=ns.follow(src.op1().type());
mult_exprt offset_times_eight(src.op1(), from_integer(8, offset_type));
const typet &offset_type = ns.follow(src.offset().type());
mult_exprt offset_times_eight(src.offset(), from_integer(8, offset_type));

binary_predicate_exprt offset_ge_zero(
offset_times_eight,
Expand All @@ -578,7 +584,7 @@ exprt flatten_byte_update(
}

// original_bits &= ~mask
bitand_exprt bitand_expr(src.op0(), bitnot_exprt(mask_shifted));
bitand_exprt bitand_expr(src.op(), bitnot_exprt(mask_shifted));

// original_bits |= newvalue
bitor_exprt bitor_expr(bitand_expr, value_shifted);
Expand All @@ -587,8 +593,10 @@ exprt flatten_byte_update(
}
else
{
throw "flatten_byte_update can only do array and scalars "
"right now, but got "+t.id_string();
PRECONDITION_WITH_DIAGNOSTICS(
false,
"flatten_byte_update can only do arrays and scalars right now",
t.id_string());
}
}

Expand Down
4 changes: 1 addition & 3 deletions src/solvers/flattening/functions.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,6 @@ Author: Daniel Kroening, [email protected]

#include "functions.h"

#include <cassert>

#include <util/std_types.h>
#include <util/std_expr.h>

Expand All @@ -32,7 +30,7 @@ void functionst::add_function_constraints()
exprt functionst::arguments_equal(const exprt::operandst &o1,
const exprt::operandst &o2)
{
assert(o1.size()==o2.size());
PRECONDITION(o1.size() == o2.size());

if(o1.empty())
return true_exprt();
Expand Down
19 changes: 8 additions & 11 deletions src/solvers/flattening/pointer_logic.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,8 +11,6 @@ Author: Daniel Kroening, [email protected]

#include "pointer_logic.h"

#include <cassert>

#include <util/arith_tools.h>
#include <util/c_types.h>
#include <util/invariant.h>
Expand Down Expand Up @@ -52,13 +50,11 @@ std::size_t pointer_logict::add_object(const exprt &expr)

if(expr.id()==ID_index)
{
assert(expr.operands().size()==2);
return add_object(expr.op0());
return add_object(to_index_expr(expr).array());
}
else if(expr.id()==ID_member)
{
assert(expr.operands().size()==1);
return add_object(expr.op0());
return add_object(to_member_expr(expr).compound());
}

return objects.number(expr);
Expand Down Expand Up @@ -149,12 +145,15 @@ exprt pointer_logict::object_rec(

for(const auto &c : components)
{
assert(offset>=current_offset);
INVARIANT(
offset >= current_offset,
"when the object has not been found yet its offset must not be smaller"
"than the offset of the current struct component");

const typet &subtype=c.type();

mp_integer sub_size=pointer_offset_size(subtype, ns);
assert(sub_size>0);
CHECK_RETURN(sub_size > 0);
mp_integer new_offset=current_offset+sub_size;

if(new_offset>offset)
Expand All @@ -166,9 +165,7 @@ exprt pointer_logict::object_rec(
offset-current_offset, pointer_type, tmp);
}

assert(new_offset<=offset);
current_offset=new_offset;
assert(current_offset<=offset);
}

return src;
Expand All @@ -183,7 +180,7 @@ pointer_logict::pointer_logict(const namespacet &_ns):ns(_ns)
{
// add NULL
null_object=objects.number(exprt(ID_NULL));
assert(null_object==0);
CHECK_RETURN(null_object == 0);

// add INVALID
invalid_object=objects.number(exprt("INVALID"));
Expand Down