Skip to content

exprt::opX cleanup #3465

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
Nov 27, 2018
Merged

exprt::opX cleanup #3465

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
3 changes: 2 additions & 1 deletion src/analyses/constant_propagator.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -631,7 +631,8 @@ void constant_propagator_ait::replace(
d.partial_evaluate(rhs, ns);

if(rhs.id()==ID_constant)
rhs.add_source_location()=it->code.op0().source_location();
rhs.add_source_location() =
to_code_assign(it->code).lhs().source_location();
}
else if(it->is_function_call())
{
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/escape_analysis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,7 @@ void escape_domaint::get_rhs_aliases(
}
else if(rhs.id()==ID_address_of)
{
get_rhs_aliases_address_of(to_address_of_expr(rhs).op0(), alias_set);
get_rhs_aliases_address_of(to_address_of_expr(rhs).op(), alias_set);
}
}

Expand Down
19 changes: 5 additions & 14 deletions src/analyses/flow_insensitive_analysis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -317,24 +317,15 @@ bool flow_insensitive_analysis_baset::do_function_call_rec(
}
else if(function.id()==ID_if)
{
if(function.operands().size()!=3)
throw "if takes three arguments";
const auto &if_expr = to_if_expr(function);

new_data =
do_function_call_rec(
l_call,
function.op1(),
arguments,
state,
goto_functions);
new_data = do_function_call_rec(
l_call, if_expr.true_case(), arguments, state, goto_functions);

new_data =
do_function_call_rec(
l_call,
function.op2(),
arguments,
state,
goto_functions) || new_data;
l_call, if_expr.false_case(), arguments, state, goto_functions) ||
new_data;
}
else if(function.id()==ID_dereference)
{
Expand Down
2 changes: 1 addition & 1 deletion src/analyses/global_may_alias.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ void global_may_alias_domaint::get_rhs_aliases(
}
else if(rhs.id()==ID_address_of)
{
get_rhs_aliases_address_of(to_address_of_expr(rhs).op0(), alias_set);
get_rhs_aliases_address_of(to_address_of_expr(rhs).object(), alias_set);
}
}

Expand Down
28 changes: 14 additions & 14 deletions src/analyses/interval_domain.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -339,25 +339,25 @@ void interval_domaint::assume_rec(
cond.id()==ID_gt || cond.id()==ID_ge ||
cond.id()==ID_equal || cond.id()==ID_notequal)
{
assert(cond.operands().size()==2);
const auto &rel = to_binary_relation_expr(cond);

if(negation) // !x<y ---> x>=y
{
if(cond.id()==ID_lt)
assume_rec(cond.op0(), ID_ge, cond.op1());
else if(cond.id()==ID_le)
assume_rec(cond.op0(), ID_gt, cond.op1());
else if(cond.id()==ID_gt)
assume_rec(cond.op0(), ID_le, cond.op1());
else if(cond.id()==ID_ge)
assume_rec(cond.op0(), ID_lt, cond.op1());
else if(cond.id()==ID_equal)
assume_rec(cond.op0(), ID_notequal, cond.op1());
else if(cond.id()==ID_notequal)
assume_rec(cond.op0(), ID_equal, cond.op1());
if(rel.id() == ID_lt)
assume_rec(rel.op0(), ID_ge, rel.op1());
else if(rel.id() == ID_le)
assume_rec(rel.op0(), ID_gt, rel.op1());
else if(rel.id() == ID_gt)
assume_rec(rel.op0(), ID_le, rel.op1());
else if(rel.id() == ID_ge)
assume_rec(rel.op0(), ID_lt, rel.op1());
else if(rel.id() == ID_equal)
assume_rec(rel.op0(), ID_notequal, rel.op1());
else if(rel.id() == ID_notequal)
assume_rec(rel.op0(), ID_equal, rel.op1());
}
else
assume_rec(cond.op0(), cond.id(), cond.op1());
assume_rec(rel.op0(), rel.id(), rel.op1());
}
else if(cond.id()==ID_not)
{
Expand Down
136 changes: 71 additions & 65 deletions src/analyses/invariant_set.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,21 +95,26 @@ std::string inv_object_storet::build_string(const exprt &expr) const
// we ignore some casts
if(expr.id()==ID_typecast)
{
assert(expr.operands().size()==1);
const auto &typecast_expr = to_typecast_expr(expr);

if(expr.type().id()==ID_signedbv ||
expr.type().id()==ID_unsignedbv)
if(
typecast_expr.type().id() == ID_signedbv ||
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggestion that I shouldn't be making because out-of-scope for this PR: we use typecast_expr.type().id() and typecast_expr.op().type().id() several times in here, maybe add some temporaries?

typecast_expr.type().id() == ID_unsignedbv)
{
if(expr.op0().type().id()==ID_signedbv ||
expr.op0().type().id()==ID_unsignedbv)
const typet &op_type = typecast_expr.op().type();

if(op_type.id() == ID_signedbv || op_type.id() == ID_unsignedbv)
{
if(to_bitvector_type(expr.type()).get_width()>=
to_bitvector_type(expr.op0().type()).get_width())
return build_string(expr.op0());
if(
to_bitvector_type(typecast_expr.type()).get_width() >=
to_bitvector_type(op_type).get_width())
{
return build_string(typecast_expr.op());
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: please add braces for readability

Copy link
Member Author

Choose a reason for hiding this comment

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

done

}
}
else if(expr.op0().type().id()==ID_bool)
else if(op_type.id() == ID_bool)
{
return build_string(expr.op0());
return build_string(typecast_expr.op());
}
}
}
Expand Down Expand Up @@ -137,8 +142,8 @@ std::string inv_object_storet::build_string(const exprt &expr) const

if(expr.id()==ID_member)
{
assert(expr.operands().size()==1);
return build_string(expr.op0())+"."+expr.get_string(ID_component_name);
return build_string(to_member_expr(expr).compound()) + "." +
expr.get_string(ID_component_name);
}

if(expr.id()==ID_symbol)
Expand All @@ -158,8 +163,7 @@ bool invariant_sett::get_object(
bool inv_object_storet::is_constant_address(const exprt &expr)
{
if(expr.id()==ID_address_of)
if(expr.operands().size()==1)
return is_constant_address_rec(expr.op0());
return is_constant_address_rec(to_address_of_expr(expr).object());

return false;
}
Expand All @@ -169,15 +173,12 @@ bool inv_object_storet::is_constant_address_rec(const exprt &expr)
if(expr.id()==ID_symbol)
return true;
else if(expr.id()==ID_member)
{
assert(expr.operands().size()==1);
return is_constant_address_rec(expr.op0());
}
return is_constant_address_rec(to_member_expr(expr).compound());
else if(expr.id()==ID_index)
{
assert(expr.operands().size()==2);
if(expr.op1().is_constant())
return is_constant_address_rec(expr.op0());
const auto &index_expr = to_index_expr(expr);
if(index_expr.index().is_constant())
return is_constant_address_rec(index_expr.array());
}

return false;
Expand Down Expand Up @@ -429,14 +430,14 @@ void invariant_sett::strengthen_rec(const exprt &expr)
else if(expr.id()==ID_le ||
expr.id()==ID_lt)
{
assert(expr.operands().size()==2);
const auto &rel = to_binary_relation_expr(expr);

// special rule: x <= (a & b)
// implies: x<=a && x<=b

if(expr.op1().id()==ID_bitand)
if(rel.op1().id() == ID_bitand)
{
const exprt &bitand_op=expr.op1();
const exprt &bitand_op = rel.op1();

forall_operands(it, bitand_op)
{
Expand All @@ -450,12 +451,11 @@ void invariant_sett::strengthen_rec(const exprt &expr)

std::pair<unsigned, unsigned> p;

if(get_object(expr.op0(), p.first) ||
get_object(expr.op1(), p.second))
if(get_object(rel.op0(), p.first) || get_object(rel.op1(), p.second))
return;

const auto i0 = numeric_cast<mp_integer>(expr.op0());
const auto i1 = numeric_cast<mp_integer>(expr.op1());
const auto i0 = numeric_cast<mp_integer>(rel.op0());
const auto i1 = numeric_cast<mp_integer>(rel.op1());

if(expr.id()==ID_le)
{
Expand Down Expand Up @@ -483,9 +483,9 @@ void invariant_sett::strengthen_rec(const exprt &expr)
}
else if(expr.id()==ID_equal)
{
assert(expr.operands().size()==2);
const auto &equal_expr = to_equal_expr(expr);

const typet &op_type=ns->follow(expr.op0().type());
const typet &op_type = ns->follow(equal_expr.op0().type());

if(op_type.id()==ID_struct)
{
Expand All @@ -495,9 +495,9 @@ void invariant_sett::strengthen_rec(const exprt &expr)
for(const auto &comp : struct_type.components())
{
const member_exprt lhs_member_expr(
expr.op0(), comp.get_name(), comp.type());
equal_expr.op0(), comp.get_name(), comp.type());
const member_exprt rhs_member_expr(
expr.op1(), comp.get_name(), comp.type());
equal_expr.op1(), comp.get_name(), comp.type());

const equal_exprt equality(lhs_member_expr, rhs_member_expr);

Expand All @@ -511,48 +511,51 @@ void invariant_sett::strengthen_rec(const exprt &expr)
// special rule: x = (a & b)
// implies: x<=a && x<=b

if(expr.op1().id()==ID_bitand)
if(equal_expr.op1().id() == ID_bitand)
{
const exprt &bitand_op=expr.op1();
const exprt &bitand_op = equal_expr.op1();

forall_operands(it, bitand_op)
{
exprt tmp(expr);
exprt tmp(equal_expr);
tmp.op1()=*it;
tmp.id(ID_le);
strengthen_rec(tmp);
}

return;
}
else if(expr.op0().id()==ID_bitand)
else if(equal_expr.op0().id() == ID_bitand)
{
exprt tmp(expr);
exprt tmp(equal_expr);
std::swap(tmp.op0(), tmp.op1());
strengthen_rec(tmp);
return;
}

// special rule: x = (type) y
if(expr.op1().id()==ID_typecast)
if(equal_expr.op1().id() == ID_typecast)
{
assert(expr.op1().operands().size()==1);
add_type_bounds(expr.op0(), expr.op1().op0().type());
const auto &typecast_expr = to_typecast_expr(equal_expr.op1());
add_type_bounds(equal_expr.op0(), typecast_expr.op().type());
}
else if(expr.op0().id()==ID_typecast)
else if(equal_expr.op0().id() == ID_typecast)
{
assert(expr.op0().operands().size()==1);
add_type_bounds(expr.op1(), expr.op0().op0().type());
const auto &typecast_expr = to_typecast_expr(equal_expr.op0());
add_type_bounds(equal_expr.op1(), typecast_expr.op().type());
}

std::pair<unsigned, unsigned> p, s;

if(get_object(expr.op0(), p.first) ||
get_object(expr.op1(), p.second))
if(
get_object(equal_expr.op0(), p.first) ||
get_object(equal_expr.op1(), p.second))
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: please add braces for readability.

Copy link
Member Author

Choose a reason for hiding this comment

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

done

{
return;
}

const auto i0 = numeric_cast<mp_integer>(expr.op0());
const auto i1 = numeric_cast<mp_integer>(expr.op1());
const auto i0 = numeric_cast<mp_integer>(equal_expr.op0());
const auto i1 = numeric_cast<mp_integer>(equal_expr.op1());
if(i0.has_value())
add_bounds(p.second, boundst(*i0));
else if(i1.has_value())
Expand All @@ -569,13 +572,16 @@ void invariant_sett::strengthen_rec(const exprt &expr)
}
else if(expr.id()==ID_notequal)
{
assert(expr.operands().size()==2);
const auto &notequal_expr = to_notequal_expr(expr);

std::pair<unsigned, unsigned> p;

if(get_object(expr.op0(), p.first) ||
get_object(expr.op1(), p.second))
if(
get_object(notequal_expr.op0(), p.first) ||
get_object(notequal_expr.op1(), p.second))
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit pick: please add braces for readability.

Copy link
Member Author

Choose a reason for hiding this comment

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

done

{
return;
}

// check if this is a contradiction
if(has_eq(p))
Expand Down Expand Up @@ -629,19 +635,19 @@ tvt invariant_sett::implies_rec(const exprt &expr) const
expr.id()==ID_equal ||
expr.id()==ID_notequal)
{
assert(expr.operands().size()==2);
const auto &rel = to_binary_relation_expr(expr);

std::pair<unsigned, unsigned> p;

bool ob0=get_object(expr.op0(), p.first);
bool ob1=get_object(expr.op1(), p.second);
bool ob0 = get_object(rel.op0(), p.first);
bool ob1 = get_object(rel.op1(), p.second);

if(ob0 || ob1)
return tvt::unknown();

tvt r;

if(expr.id()==ID_le)
if(rel.id() == ID_le)
{
r=is_le(p);
if(!r.is_unknown())
Expand All @@ -653,7 +659,7 @@ tvt invariant_sett::implies_rec(const exprt &expr) const

return b0<=b1;
}
else if(expr.id()==ID_lt)
else if(rel.id() == ID_lt)
{
r=is_lt(p);
if(!r.is_unknown())
Expand All @@ -665,9 +671,9 @@ tvt invariant_sett::implies_rec(const exprt &expr) const

return b0<b1;
}
else if(expr.id()==ID_equal)
else if(rel.id() == ID_equal)
return is_eq(p);
else if(expr.id()==ID_notequal)
else if(rel.id() == ID_notequal)
return is_ne(p);
else
UNREACHABLE;
Expand Down Expand Up @@ -717,10 +723,9 @@ void invariant_sett::nnf(exprt &expr, bool negate)
}
else if(expr.id()==ID_not)
{
assert(expr.operands().size()==1);
nnf(expr.op0(), !negate);
nnf(to_not_expr(expr).op(), !negate);
exprt tmp;
tmp.swap(expr.op0());
tmp.swap(to_not_expr(expr).op());
expr.swap(tmp);
}
else if(expr.id()==ID_and)
Expand All @@ -741,14 +746,15 @@ void invariant_sett::nnf(exprt &expr, bool negate)
}
else if(expr.id()==ID_typecast)
{
assert(expr.operands().size()==1);
const auto &typecast_expr = to_typecast_expr(expr);

if(expr.op0().type().id()==ID_unsignedbv ||
expr.op0().type().id()==ID_signedbv)
if(
typecast_expr.op().type().id() == ID_unsignedbv ||
typecast_expr.op().type().id() == ID_signedbv)
{
equal_exprt tmp;
tmp.lhs()=expr.op0();
tmp.rhs()=from_integer(0, expr.op0().type());
tmp.lhs() = typecast_expr.op();
tmp.rhs() = from_integer(0, typecast_expr.op().type());
nnf(tmp, !negate);
expr.swap(tmp);
}
Expand Down
Loading