Skip to content

Simplifier and symex rewriting fixes/extensions #731

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 6 commits into from
Nov 7, 2017
Merged

Simplifier and symex rewriting fixes/extensions #731

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
7064483
simplify_typecast: simplify more pointer arithmetic
tautschnig Mar 3, 2016
ddd3d03
Extended simplify for byte_update, typing
tautschnig Feb 5, 2016
77236cc
Avoid nesting of ID_with/byte_update by rewriting byte_extract to use…
tautschnig Mar 3, 2016
81943f2
Split ID_and/ID_or vs ID_xor simplification
tautschnig Jan 3, 2017
71e9642
Extensions to simplify_byte_extract
tautschnig Jan 6, 2017
14c00dc
Simplify all expressions generated by flatten_byte_operators
tautschnig Jun 6, 2017
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
31 changes: 31 additions & 0 deletions src/goto-symex/symex_clean_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,11 +67,13 @@ void goto_symext::process_array_expr_rec(
expr.swap(tmp);
}
else
{
Forall_operands(it, expr)
{
typet t=it->type();
process_array_expr_rec(*it, t);
}
}

if(!base_type_eq(expr.type(), type, ns))
{
Expand Down Expand Up @@ -166,12 +168,41 @@ void goto_symext::replace_array_equal(exprt &expr)
replace_array_equal(*it);
}

/// Rewrite index/member expressions in byte_extract to offset
static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
{
Copy link
Member

Choose a reason for hiding this comment

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

Wouldn't the natural place for this to happen be the simplifier?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

While that is true, it would cause/require repeated simplification of the same expression (note that this simplification needs to happen before doing symex_assign_*). It may, however, also be useful to add this to the simplifier as a fallback?

Copy link
Member

Choose a reason for hiding this comment

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

Not sure the object descriptors fit into simplifier; leave as is for now.

Forall_operands(it, expr)
adjust_byte_extract_rec(*it, ns);

if(expr.id()==ID_byte_extract_big_endian ||
expr.id()==ID_byte_extract_little_endian)
{
byte_extract_exprt &be=to_byte_extract_expr(expr);
if(be.op().id()==ID_symbol &&
to_ssa_expr(be.op()).get_original_expr().get_bool(ID_C_invalid_object))
return;

object_descriptor_exprt ode;
ode.build(expr, ns);

be.op()=ode.root_object();
be.offset()=ode.offset();
}
}

void goto_symext::clean_expr(
exprt &expr,
statet &state,
const bool write)
{
replace_nondet(expr);
dereference(expr, state, write);

// make sure all remaining byte extract operations use the root
// object to avoid nesting of with/update and byte_update when on
// lhs
if(write)
adjust_byte_extract_rec(expr, ns);

replace_array_equal(expr);
}
16 changes: 8 additions & 8 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 @@ -242,12 +242,12 @@ exprt flatten_byte_extract(

byte_extract_exprt tmp(unpacked);
tmp.type()=subtype;
tmp.offset()=simplify_expr(new_offset, ns);
tmp.offset()=new_offset;
Copy link
Member

Choose a reason for hiding this comment

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

Also wondering about the right place for this -- perhaps where flatten_byte_* is used?

Copy link
Member

Choose a reason for hiding this comment

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

I am also kind of tempted to do the flattening in the simplifier.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I do agree that this should be moved to the simplifier (also note that it only has dependencies within util/), but may I suggest that this happens as a separate PR? Otherwise this PR will become huge.

Copy link
Member

Choose a reason for hiding this comment

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

yes, separate PR

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Thanks, I've put a note on my TODO list. I'll take care of it later on.


array.copy_to_operands(flatten_byte_extract(tmp, ns));
}

return array;
return simplify_expr(array, ns);
}
}
else if(type.id()==ID_struct)
Expand Down Expand Up @@ -277,13 +277,13 @@ exprt flatten_byte_extract(

byte_extract_exprt tmp(unpacked);
tmp.type()=comp.type();
tmp.offset()=simplify_expr(new_offset, ns);
tmp.offset()=new_offset;

s.move_to_operands(tmp);
}

if(!failed)
return s;
return simplify_expr(s, ns);
}

const exprt &root=unpacked.op();
Expand Down Expand Up @@ -333,7 +333,7 @@ exprt flatten_byte_extract(
{
concatenation_exprt concatenation(src.type());
concatenation.operands().swap(op);
return concatenation;
return simplify_expr(concatenation, ns);
}
}

Expand Down Expand Up @@ -413,7 +413,7 @@ exprt flatten_byte_update(
result.swap(with_expr);
}

return result;
return simplify_expr(result, ns);
}
else // sub_size!=1
{
Expand Down Expand Up @@ -512,7 +512,7 @@ exprt flatten_byte_update(
result=with_expr;
}

return result;
return simplify_expr(result, ns);
}
}
else
Expand Down Expand Up @@ -583,7 +583,7 @@ exprt flatten_byte_update(
// original_bits |= newvalue
bitor_exprt bitor_expr(bitand_expr, value_shifted);

return bitor_expr;
return simplify_expr(bitor_expr, ns);
}
else
{
Expand Down
33 changes: 29 additions & 4 deletions src/util/simplify_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -318,12 +318,14 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
// (int)((T*)0 + int) -> (int)(sizeof(T)*(size_t)int) if NULL is zero
if(config.ansi_c.NULL_is_zero &&
(expr_type.id()==ID_signedbv || expr_type.id()==ID_unsignedbv) &&
op_type.id()==ID_pointer &&
expr.op0().id()==ID_plus &&
expr.op0().operands().size()==2 &&
expr.op0().op0().id()==ID_typecast &&
((expr.op0().op0().id()==ID_typecast &&
expr.op0().op0().operands().size()==1 &&
expr.op0().op0().op0().is_zero() &&
op_type.id()==ID_pointer)
expr.op0().op0().op0().is_zero()) ||
(expr.op0().op0().is_constant() &&
to_constant_expr(expr.op0().op0()).get_value()==ID_NULL)))
{
mp_integer sub_size=pointer_offset_size(op_type.subtype(), ns);
if(sub_size!=-1)
Expand Down Expand Up @@ -727,6 +729,20 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
return false;
}
}
else if(operand.id()==ID_address_of)
{
const exprt &o=to_address_of_expr(operand).object();

// turn &array into &array[0] when casting to pointer-to-element-type
if(o.type().id()==ID_array &&
base_type_eq(expr_type, pointer_type(o.type().subtype()), ns))
{
expr=address_of_exprt(index_exprt(o, from_integer(0, size_type())));

simplify_rec(expr);
return false;
}
}

return true;
}
Expand Down Expand Up @@ -1826,6 +1842,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
index_exprt(
result,
from_integer(offset, expr.offset().type()));
result.make_typecast(expr.type());

if(!base_type_eq(expr.type(), op_type_ptr->subtype(), ns))
result.make_typecast(expr.type());
Expand Down Expand Up @@ -1886,7 +1903,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
simplify_member(expr.op());
expr.offset()=
from_integer(offset-m_offset_bits/8, expr.offset().type());
simplify_rec(expr.offset());
simplify_rec(expr);

return false;
}
Expand Down Expand Up @@ -2116,6 +2133,14 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)

return false;
}

if(result_expr.is_not_nil())
{
simplify_rec(result_expr);
expr.swap(result_expr);

return false;
}
}

// replace elements of array or struct expressions, possibly using
Expand Down
121 changes: 60 additions & 61 deletions src/util/simplify_expr_boolean.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,21 +72,60 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
return false;
}
}
else if(expr.id()==ID_or ||
expr.id()==ID_and ||
expr.id()==ID_xor)
else if(expr.id()==ID_xor)
{
if(operands.empty())
return true;

bool result=true;

exprt::operandst::const_iterator last;
bool last_set=false;

bool negate=false;

for(exprt::operandst::iterator it=operands.begin();
for(exprt::operandst::const_iterator it=operands.begin();
it!=operands.end();)
{
if(it->type().id()!=ID_bool)
return true;

bool erase;

if(it->is_true())
{
erase=true;
negate=!negate;
}
else
erase=it->is_false();

if(erase)
{
it=operands.erase(it);
result=false;
}
else
it++;
}

if(operands.empty())
{
expr.make_bool(negate);
return false;
}
else if(operands.size()==1)
{
exprt tmp(operands.front());
if(negate)
tmp.make_not();
expr.swap(tmp);
return false;
}

return result;
}
else if(expr.id()==ID_and || expr.id()==ID_or)
{
std::unordered_set<exprt, irep_hash> expr_set;

bool result=true;

for(exprt::operandst::const_iterator it=operands.begin();
it!=operands.end();)
{
if(it->type().id()!=ID_bool)
Expand All @@ -106,77 +145,37 @@ bool simplify_exprt::simplify_boolean(exprt &expr)
return false;
}

bool erase;

if(expr.id()==ID_and)
erase=is_true;
else if(is_true && expr.id()==ID_xor)
{
erase=true;
negate=!negate;
}
else
erase=is_false;

if(last_set && *it==*last &&
(expr.id()==ID_or || expr.id()==ID_and))
erase=true; // erase duplicate operands
bool erase=
(expr.id()==ID_and ? is_true : is_false) ||
!expr_set.insert(*it).second;

if(erase)
{
it=operands.erase(it);
result=false;
}
else
{
last=it;
last_set=true;
it++;
}
}

// search for a and !a
if(expr.id()==ID_and || expr.id()==ID_or)
{
// first gather all the a's with !a

std::unordered_set<exprt, irep_hash> expr_set;

forall_operands(it, expr)
if(it->id()==ID_not &&
it->operands().size()==1 &&
it->type().id()==ID_bool)
expr_set.insert(it->op0());

// now search for a

if(!expr_set.empty())
for(const exprt &op : operands)
if(op.id()==ID_not &&
op.operands().size()==1 &&
op.type().id()==ID_bool &&
expr_set.find(op.op0())!=expr_set.end())
{
forall_operands(it, expr)
{
if(it->id()!=ID_not &&
expr_set.find(*it)!=expr_set.end())
{
expr.make_bool(expr.id()==ID_or);
return false;
}
}
expr.make_bool(expr.id()==ID_or);
return false;
}
}

if(operands.empty())
{
if(expr.id()==ID_and || negate)
expr=true_exprt();
else
expr=false_exprt();

expr.make_bool(expr.id()==ID_and);
return false;
}
else if(operands.size()==1)
{
if(negate)
expr.op0().make_not();
exprt tmp(operands.front());
expr.swap(tmp);
return false;
Expand Down