Skip to content

simplifier: new interface for simplify_node #4982

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
Aug 6, 2019
Merged

simplifier: new interface for simplify_node #4982

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
be5a2d5
simplifier: new interface for simplify_node
Jul 30, 2019
85e8337
use mult_exprt/plus_exprt instead of binary_exprt
Aug 5, 2019
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
70 changes: 32 additions & 38 deletions src/util/simplify_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -571,8 +571,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
op_type.id() == ID_floatbv ? ID_ieee_float_notequal : ID_notequal,
from_integer(0, op_type));
inequality.add_source_location()=expr.source_location();
simplify_node(inequality);
return std::move(inequality);
return changed(simplify_node(inequality));
}

// eliminate casts from proper bool
Expand Down Expand Up @@ -611,9 +610,8 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
{
// rewrite (_Bool)x to (_Bool)(x!=0)
exprt inequality = is_not_zero(expr.op(), ns);
simplify_node(inequality);
auto new_expr = expr;
new_expr.op() = std::move(inequality);
new_expr.op() = simplify_node(std::move(inequality));
Copy link
Collaborator

Choose a reason for hiding this comment

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

See below: std::move doesn't seem to be very useful here.

Copy link
Member Author

Choose a reason for hiding this comment

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

Fixed -- the method now takes an exprt as argument.

return changed(simplify_typecast(new_expr)); // recursive call
}

Expand Down Expand Up @@ -724,9 +722,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
*it = simplify_typecast(new_operand); // recursive call
}

simplify_node(result); // possibly recursive call

return std::move(result);
return changed(simplify_node(result)); // possibly recursive call
}
}
else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
Expand Down Expand Up @@ -1978,10 +1974,9 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
{
exprt compo_offset = from_integer(*i, offset.type());
plus_exprt new_offset(offset, compo_offset);
simplify_node(new_offset);
exprt new_value(with.new_value());
auto tmp = expr;
tmp.set_offset(std::move(new_offset));
tmp.set_offset(simplify_node(std::move(new_offset)));
Copy link
Collaborator

Choose a reason for hiding this comment

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

simplify_node takes a const exprt & as argument, the std::move doesn't seem to be useful?

Copy link
Member Author

Choose a reason for hiding this comment

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

fixed

tmp.set_value(std::move(new_value));
Copy link
Collaborator

Choose a reason for hiding this comment

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

This code could really do with some cleanup: 1) I'd move the definitions (new_offset, new_value) closer to their use; 2) creating an explicit copy in new_value just so that we can std::move it seems to have little value.

return changed(simplify_byte_update(tmp)); // recursive call
}
Expand All @@ -1993,22 +1988,20 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
if(i.has_value())
{
const exprt &index=with.where();
mult_exprt index_offset(index, from_integer(*i, index.type()));
simplify_node(index_offset);
exprt index_offset =
simplify_node(mult_exprt(index, from_integer(*i, index.type())));

// index_offset may need a typecast
if(offset.type() != index.type())
{
typecast_exprt tmp(index_offset, offset.type());
simplify_node(tmp);
index_offset.swap(tmp);
index_offset =
simplify_node(typecast_exprt(index_offset, offset.type()));
}

plus_exprt new_offset(offset, index_offset);
simplify_node(new_offset);
exprt new_value(with.new_value());
auto tmp = expr;
tmp.set_offset(std::move(new_offset));
tmp.set_offset(simplify_node(std::move(new_offset)));
tmp.set_value(std::move(new_value));
Copy link
Collaborator

Choose a reason for hiding this comment

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

Same comments as above: move definitions closer, avoid useless copy, no std::move

return changed(simplify_byte_update(tmp)); // recursive call
}
Expand Down Expand Up @@ -2226,20 +2219,19 @@ bool simplify_exprt::simplify_node_preorder(exprt &expr)
return result;
}

bool simplify_exprt::simplify_node(exprt &expr)
simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
{
if(!expr.has_operands())
return true; // no change
if(!node.has_operands())
return unchanged(node); // no change

// #define DEBUGX

#ifdef DEBUGX
exprt old(expr);
exprt old(node);
#endif

bool no_change = true;

no_change = sort_and_join(expr) && no_change;
exprt expr = node;
bool no_change_sort_and_join = sort_and_join(expr);

resultt<> r = unchanged(expr);

Expand Down Expand Up @@ -2440,26 +2432,23 @@ bool simplify_exprt::simplify_node(exprt &expr)
r = simplify_complex(to_unary_expr(expr));
}

if(r.has_changed())
{
expr = r.expr;
no_change = false;
}
if(!no_change_sort_and_join)
r = changed(r);

#ifdef DEBUGX
if(
!no_change
r.has_changed()
# ifdef DEBUG_ON_DEMAND
&& debug_on
# endif
)
{
std::cout << "===== " << old.id() << ": " << format(old) << '\n'
<< " ---> " << format(expr) << '\n';
std::cout << "===== " << node.id() << ": " << format(node) << '\n'
<< " ---> " << format(r.expr) << '\n';
}
#endif

return no_change;
return r;
}

simplify_exprt::resultt<> simplify_exprt::simplify_rec(const exprt &expr)
Expand All @@ -2485,30 +2474,35 @@ simplify_exprt::resultt<> simplify_exprt::simplify_rec(const exprt &expr)

// We work on a copy to prevent unnecessary destruction of sharing.
exprt tmp=expr;
bool result = simplify_node_preorder(tmp);
bool no_change = simplify_node_preorder(tmp);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Maybe this isn't the final piece? simplify_node_preorder will also need the interface change.

Copy link
Member Author

Choose a reason for hiding this comment

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

indeed; will make that the next (final) PR.


if(!simplify_node(tmp))
result=false;
auto simplify_node_result = simplify_node(tmp);

if(simplify_node_result.has_changed())
{
no_change = false;
tmp = simplify_node_result.expr;
}

#ifdef USE_LOCAL_REPLACE_MAP
#if 1
replace_mapt::const_iterator it=local_replace_map.find(tmp);
if(it!=local_replace_map.end())
{
tmp=it->second;
result=false;
no_change = false;
}
#else
if(!local_replace_map.empty() &&
!replace_expr(local_replace_map, tmp))
{
simplify_rec(tmp);
result=false;
no_change = false;
}
#endif
#endif

if(result) // no change
if(no_change) // no change
{
return unchanged(expr);
}
Expand Down
4 changes: 2 additions & 2 deletions src/util/simplify_expr_array.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -184,8 +184,8 @@ simplify_exprt::simplify_index(const index_exprt &expr)
// add offset to index
mult_exprt offset(
from_integer(*sub_size, byte_extract_expr.offset().type()), index);
plus_exprt final_offset(byte_extract_expr.offset(), offset);
simplify_node(final_offset);
exprt final_offset =
simplify_node(plus_exprt(byte_extract_expr.offset(), offset));

exprt result_expr(array.id(), expr.type());
result_expr.add_to_operands(byte_extract_expr.op(), final_offset);
Expand Down
10 changes: 4 additions & 6 deletions src/util/simplify_expr_boolean.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
binary_exprt new_expr = implies_expr;
new_expr.id(ID_or);
new_expr.op0() = boolean_negate(new_expr.op0());
simplify_node(new_expr);
return std::move(new_expr);
return changed(simplify_node(new_expr));
}
else if(expr.id()==ID_xor)
{
Expand Down Expand Up @@ -192,8 +191,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)

Forall_operands(it, tmp)
{
*it = boolean_negate(*it);
simplify_node(*it);
*it = simplify_node(boolean_negate(*it));
Copy link
Collaborator

Choose a reason for hiding this comment

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

As remarked elsewhere, boolean_negate should not require further simplifier calls.

Copy link
Member Author

Choose a reason for hiding this comment

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

will make that a separate PR

}

tmp.id(tmp.id() == ID_and ? ID_or : ID_and);
Expand All @@ -211,15 +209,15 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
auto const &op_as_exists = to_exists_expr(op);
forall_exprt rewritten_op(
op_as_exists.symbol(), not_exprt(op_as_exists.where()));
simplify_node(rewritten_op.where());
rewritten_op.where() = simplify_node(rewritten_op.where());
return std::move(rewritten_op);
}
else if(op.id() == ID_forall) // !(forall: a) <-> exists: not a
{
auto const &op_as_forall = to_forall_expr(op);
exists_exprt rewritten_op(
op_as_forall.symbol(), not_exprt(op_as_forall.where()));
simplify_node(rewritten_op.where());
rewritten_op.where() = simplify_node(rewritten_op.where());
Copy link
Collaborator

Choose a reason for hiding this comment

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

Should use boolean_negate in the line above and then skip the simplify_node call. Here and for the case a few lines earlier as well.

return std::move(rewritten_op);
}

Expand Down
2 changes: 1 addition & 1 deletion src/util/simplify_expr_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -210,7 +210,7 @@ class simplify_exprt
NODISCARD resultt<> simplify_inequality_pointer_object(const exprt &);

// main recursion
bool simplify_node(exprt &expr);
NODISCARD resultt<> simplify_node(exprt);
bool simplify_node_preorder(exprt &expr);
NODISCARD resultt<> simplify_rec(const exprt &);

Expand Down
26 changes: 7 additions & 19 deletions src/util/simplify_expr_if.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -350,41 +350,29 @@ simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr)
else if(truevalue.is_false() && falsevalue.is_true())
{
// a?0:1 <-> !a
exprt tmp = boolean_negate(cond);
simplify_node(tmp);
return std::move(tmp);
return changed(simplify_node(boolean_negate(cond)));
}
else if(falsevalue.is_false())
{
// a?b:0 <-> a AND b
and_exprt tmp(cond, truevalue);
simplify_node(tmp);
return std::move(tmp);
return changed(simplify_node(and_exprt(cond, truevalue)));
}
else if(falsevalue.is_true())
{
// a?b:1 <-> !a OR b
exprt tmp_not_cond = boolean_negate(cond);
simplify_node(tmp_not_cond);
or_exprt tmp(tmp_not_cond, truevalue);
simplify_node(tmp);
return std::move(tmp);
return changed(simplify_node(
or_exprt(simplify_node(boolean_negate(cond)), truevalue)));
Copy link
Collaborator

Choose a reason for hiding this comment

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

As agreed in another PR, calling simplify_node on the result of boolean_negate is unnecessary. Unrelated to this PR, but should be fixed now that we're looking at this code. Applies here and below.

}
else if(truevalue.is_true())
{
// a?1:b <-> a||(!a && b) <-> a OR b
or_exprt tmp(cond, falsevalue);
simplify_node(tmp);
return std::move(tmp);
return changed(simplify_node(or_exprt(cond, falsevalue)));
}
else if(truevalue.is_false())
{
// a?0:b <-> !a && b
exprt tmp_not_cond = boolean_negate(cond);
simplify_node(tmp_not_cond);
and_exprt tmp(tmp_not_cond, falsevalue);
simplify_node(tmp);
return std::move(tmp);
return changed(simplify_node(
and_exprt(simplify_node(boolean_negate(cond)), falsevalue)));
}
}
}
Expand Down
38 changes: 13 additions & 25 deletions src/util/simplify_expr_int.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -568,9 +568,7 @@ simplify_exprt::simplify_minus(const minus_exprt &expr)
// rewrite "a-b" to "a+(-b)"
unary_minus_exprt rhs_negated(operands[1]);
plus_exprt plus_expr(operands[0], simplify_unary_minus(rhs_negated));
simplify_node(plus_expr);

return std::move(plus_expr);
return changed(simplify_node(plus_expr));
}
else if(
minus_expr.type().id() == ID_pointer &&
Expand Down Expand Up @@ -649,12 +647,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_bitwise(const exprt &expr)
}

new_expr.type()=bool_typet();
simplify_node(new_expr);
new_expr = simplify_node(new_expr);

new_expr = typecast_exprt(new_expr, expr.type());
simplify_node(new_expr);

return std::move(new_expr);
return changed(simplify_node(new_expr));
}
}

Expand Down Expand Up @@ -1486,8 +1482,7 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
new_expr.id(ID_equal);
new_expr = simplify_inequality_no_constant(new_expr);
new_expr = boolean_negate(new_expr);
simplify_node(new_expr);
return std::move(new_expr);
return changed(simplify_node(new_expr));
Copy link
Collaborator

Choose a reason for hiding this comment

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

return new_expr; should do

}
else if(expr.id()==ID_gt)
{
Expand All @@ -1497,17 +1492,15 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
new_expr.op0().swap(new_expr.op1());
new_expr = simplify_inequality_no_constant(new_expr);
new_expr = boolean_negate(new_expr);
simplify_node(new_expr);
return std::move(new_expr);
return changed(simplify_node(new_expr));
Copy link
Collaborator

Choose a reason for hiding this comment

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

return new_expr;

}
else if(expr.id()==ID_lt)
{
auto new_expr = expr;
new_expr.id(ID_ge);
new_expr = simplify_inequality_no_constant(new_expr);
new_expr = boolean_negate(new_expr);
simplify_node(new_expr);
return std::move(new_expr);
return changed(simplify_node(new_expr));
Copy link
Collaborator

Choose a reason for hiding this comment

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

return new_expr;

}
else if(expr.id()==ID_le)
{
Expand Down Expand Up @@ -1588,10 +1581,9 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
if(!eliminate_common_addends(new_expr.op0(), new_expr.op1()))
{
// remove zeros
simplify_node(new_expr.op0());
simplify_node(new_expr.op1());
new_expr = simplify_inequality(new_expr); // recursive call
return std::move(new_expr);
new_expr.op0() = simplify_node(new_expr.op0());
new_expr.op1() = simplify_node(new_expr.op1());
return changed(simplify_inequality(new_expr)); // recursive call
}
}

Expand Down Expand Up @@ -1625,8 +1617,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
new_expr.id(ID_equal);
new_expr = simplify_inequality_rhs_is_constant(new_expr);
new_expr = boolean_negate(new_expr);
simplify_node(new_expr);
return std::move(new_expr);
return changed(simplify_node(new_expr));
Copy link
Collaborator

Choose a reason for hiding this comment

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

return new_expr;

}

// very special case for pointers
Expand Down Expand Up @@ -1839,8 +1830,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
new_expr.id(ID_equal);
new_expr = simplify_inequality_rhs_is_constant(new_expr);
new_expr = boolean_negate(new_expr);
simplify_node(new_expr);
return std::move(new_expr);
return changed(simplify_node(new_expr));
Copy link
Collaborator

Choose a reason for hiding this comment

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

return new_expr;

}
else if(expr.id()==ID_gt)
{
Expand All @@ -1863,8 +1853,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
new_expr.id(ID_ge);
new_expr = simplify_inequality_rhs_is_constant(new_expr);
new_expr = boolean_negate(new_expr);
simplify_node(new_expr);
return std::move(new_expr);
return changed(simplify_node(new_expr));
Copy link
Collaborator

Choose a reason for hiding this comment

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

return new_expr;

}
else if(expr.id()==ID_le)
{
Expand All @@ -1881,8 +1870,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
new_expr.op1() = from_integer(i, new_expr.op1().type());
new_expr = simplify_inequality_rhs_is_constant(new_expr);
new_expr = boolean_negate(new_expr);
simplify_node(new_expr);
return std::move(new_expr);
return changed(simplify_node(new_expr));
Copy link
Collaborator

Choose a reason for hiding this comment

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

return new_expr;

}
}
#endif
Expand Down
Loading