Skip to content

avoid direct access to exprt::opX() #3972

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
Jan 28, 2019
Merged

avoid direct access to exprt::opX() #3972

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/ansi-c/c_typecheck_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,8 @@ void c_typecheck_baset::add_rounding_mode(exprt &expr)
else
UNREACHABLE;

expr.op2()=from_integer(0, unsigned_int_type());
to_ieee_float_op_expr(expr).rounding_mode() =
from_integer(0, unsigned_int_type());
}
}
}
Expand Down
23 changes: 8 additions & 15 deletions src/ansi-c/expr2c.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -782,14 +782,11 @@ std::string expr2ct::convert_typecast(
}

std::string expr2ct::convert_trinary(
const exprt &src,
const ternary_exprt &src,
Copy link
Collaborator

Choose a reason for hiding this comment

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

Request for work outside this PR: can we unify "ternery" vs "trinary"?

const std::string &symbol1,
const std::string &symbol2,
unsigned precedence)
{
if(src.operands().size()!=3)
return convert_norep(src, precedence);

const exprt &op0=src.op0();
const exprt &op1=src.op1();
const exprt &op2=src.op2();
Expand Down Expand Up @@ -3346,18 +3343,14 @@ std::string expr2ct::convert_extractbit(
return dest;
}

std::string expr2ct::convert_extractbits(
const exprt &src,
unsigned precedence)
std::string
expr2ct::convert_extractbits(const extractbits_exprt &src, unsigned precedence)
{
if(src.operands().size()!=3)
return convert_norep(src, precedence);

std::string dest=convert_with_precedence(src.op0(), precedence);
std::string dest = convert_with_precedence(src.src(), precedence);
dest+='[';
dest+=convert_with_precedence(src.op1(), precedence);
dest += convert_with_precedence(src.upper(), precedence);
dest+=", ";
dest+=convert_with_precedence(src.op2(), precedence);
dest += convert_with_precedence(src.lower(), precedence);
dest+=']';

return dest;
Expand Down Expand Up @@ -3758,7 +3751,7 @@ std::string expr2ct::convert_with_precedence(
return convert_binary(src, "==>", precedence=3, true);

else if(src.id()==ID_if)
return convert_trinary(src, "?", ":", precedence=3);
return convert_trinary(to_if_expr(src), "?", ":", precedence = 3);

else if(src.id()==ID_forall)
return convert_quantifier(src, "forall", precedence=2);
Expand Down Expand Up @@ -3864,7 +3857,7 @@ std::string expr2ct::convert_with_precedence(
return convert_extractbit(src, precedence);

else if(src.id()==ID_extractbits)
return convert_extractbits(src, precedence);
return convert_extractbits(to_extractbits_expr(src), precedence);

else if(src.id()==ID_initializer_list ||
src.id()==ID_compound_literal)
Expand Down
11 changes: 6 additions & 5 deletions src/ansi-c/expr2c_class.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -118,8 +118,10 @@ class expr2ct
std::string convert_array_of(const exprt &src, unsigned precedence);

std::string convert_trinary(
const exprt &src, const std::string &symbol1,
const std::string &symbol2, unsigned precedence);
const ternary_exprt &src,
const std::string &symbol1,
const std::string &symbol2,
unsigned precedence);

std::string convert_overflow(
const exprt &src, unsigned &precedence);
Expand Down Expand Up @@ -155,9 +157,8 @@ class expr2ct
const exprt &src,
unsigned precedence);

std::string convert_extractbits(
const exprt &src,
unsigned precedence);
std::string
convert_extractbits(const extractbits_exprt &src, unsigned precedence);

std::string convert_unary(
const exprt &src, const std::string &symbol,
Expand Down
80 changes: 43 additions & 37 deletions src/util/simplify_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,26 +65,26 @@ bool simplify_exprt::simplify_abs(exprt &expr)
if(expr.operands().size()!=1)
return true;

if(expr.op0().is_constant())
if(to_unary_expr(expr).op().is_constant())
{
const typet &type = expr.op0().type();
const typet &type = to_unary_expr(expr).op().type();

if(type.id()==ID_floatbv)
{
ieee_floatt value(to_constant_expr(expr.op0()));
ieee_floatt value(to_constant_expr(to_unary_expr(expr).op()));
value.set_sign(false);
expr=value.to_expr();
return false;
}
else if(type.id()==ID_signedbv ||
type.id()==ID_unsignedbv)
{
auto value = numeric_cast<mp_integer>(expr.op0());
auto value = numeric_cast<mp_integer>(to_unary_expr(expr).op());
if(value.has_value())
{
if(*value >= 0)
{
expr=expr.op0();
expr = to_unary_expr(expr).op();
return false;
}
else
Expand Down Expand Up @@ -1221,55 +1221,56 @@ bool simplify_exprt::simplify_with(exprt &expr)
if((expr.operands().size()%2)!=1)
return true;

const typet op0_type=ns.follow(expr.op0().type());
auto &with_expr = to_with_expr(expr);

const typet old_type_followed = ns.follow(with_expr.old().type());

// now look at first operand

if(op0_type.id()==ID_struct)
if(old_type_followed.id() == ID_struct)
{
if(expr.op0().id()==ID_struct ||
expr.op0().id()==ID_constant)
if(with_expr.old().id() == ID_struct || with_expr.old().id() == ID_constant)
{
while(expr.operands().size()>1)
while(with_expr.operands().size() > 1)
{
const irep_idt &component_name=
expr.op1().get(ID_component_name);
const irep_idt &component_name =
with_expr.where().get(ID_component_name);

if(!to_struct_type(op0_type).
has_component(component_name))
if(!to_struct_type(old_type_followed).has_component(component_name))
return result;

std::size_t number=to_struct_type(op0_type).
component_number(component_name);
std::size_t number =
to_struct_type(old_type_followed).component_number(component_name);

expr.op0().operands()[number].swap(expr.op2());
with_expr.old().operands()[number].swap(with_expr.new_value());

expr.operands().erase(++expr.operands().begin());
expr.operands().erase(++expr.operands().begin());
with_expr.operands().erase(++with_expr.operands().begin());
with_expr.operands().erase(++with_expr.operands().begin());

result=false;
}
}
}
else if(expr.op0().type().id()==ID_array)
else if(with_expr.old().type().id() == ID_array)
{
if(expr.op0().id()==ID_array ||
expr.op0().id()==ID_constant)
{
while(expr.operands().size()>1)
{
const auto i = numeric_cast<mp_integer>(expr.op1());
const auto i = numeric_cast<mp_integer>(with_expr.where());

if(!i.has_value())
break;

if(*i < 0 || *i >= expr.op0().operands().size())
if(*i < 0 || *i >= with_expr.old().operands().size())
break;

expr.op0().operands()[numeric_cast_v<std::size_t>(*i)].swap(expr.op2());
with_expr.old().operands()[numeric_cast_v<std::size_t>(*i)].swap(
with_expr.new_value());

expr.operands().erase(++expr.operands().begin());
expr.operands().erase(++expr.operands().begin());
with_expr.operands().erase(++with_expr.operands().begin());
with_expr.operands().erase(++with_expr.operands().begin());

result=false;
}
Expand Down Expand Up @@ -1663,24 +1664,27 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)

// byte_extract(byte_update(root, offset, value), offset) =>
// value
if(((expr.id()==ID_byte_extract_big_endian &&
expr.op().id()==ID_byte_update_big_endian) ||
(expr.id()==ID_byte_extract_little_endian &&
expr.op().id()==ID_byte_update_little_endian)) &&
expr.offset()==expr.op().op1())
if(
((expr.id() == ID_byte_extract_big_endian &&
expr.op().id() == ID_byte_update_big_endian) ||
(expr.id() == ID_byte_extract_little_endian &&
expr.op().id() == ID_byte_update_little_endian)) &&
expr.offset() == to_byte_update_expr(expr.op()).offset())
{
if(base_type_eq(expr.type(), expr.op().op2().type(), ns))
const auto &op_byte_update = to_byte_update_expr(expr.op());

if(base_type_eq(expr.type(), op_byte_update.value().type(), ns))
{
exprt tmp=expr.op().op2();
exprt tmp = op_byte_update.value();
expr.swap(tmp);

return false;
}
else if(
el_size.has_value() &&
*el_size <= pointer_offset_bits(expr.op().op2().type(), ns))
*el_size <= pointer_offset_bits(op_byte_update.value().type(), ns))
{
expr.op()=expr.op().op2();
expr.op() = op_byte_update.value();
expr.offset()=from_integer(0, expr.offset().type());

simplify_byte_extract(expr);
Expand Down Expand Up @@ -1811,9 +1815,11 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
{
// byte_update(byte_update(root, offset, value), offset, value2) =>
// byte_update(root, offset, value2)
if(expr.id()==expr.op().id() &&
expr.offset()==expr.op().op1() &&
base_type_eq(expr.value().type(), expr.op().op2().type(), ns))
if(
expr.id() == expr.op().id() &&
expr.offset() == to_byte_update_expr(expr.op()).offset() &&
base_type_eq(
expr.value().type(), to_byte_update_expr(expr.op()).value().type(), ns))
{
expr.op()=expr.op().op0();
return false;
Expand Down
18 changes: 9 additions & 9 deletions src/util/simplify_expr_array.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,15 +65,15 @@ bool simplify_exprt::simplify_index(exprt &expr)
{
// we have (a WITH [i:=e])[j]

const exprt &with_expr=array;

if(with_expr.operands().size()!=3)
if(array.operands().size() != 3)
return true;

if(with_expr.op1()==expr.op1())
const auto &with_expr = to_with_expr(array);

if(with_expr.where() == expr.op1())
{
// simplify (e with [i:=v])[i] to v
exprt tmp=with_expr.op2();
exprt tmp = with_expr.new_value();
expr.swap(tmp);
return false;
}
Expand All @@ -82,19 +82,19 @@ bool simplify_exprt::simplify_index(exprt &expr)
// Turn (a with i:=x)[j] into (i==j)?x:a[j].
// watch out that the type of i and j might be different.
const exprt rhs_casted =
typecast_exprt::conditional_cast(with_expr.op1(), expr.op1().type());
typecast_exprt::conditional_cast(with_expr.where(), expr.op1().type());

equal_exprt equality_expr(expr.op1(), rhs_casted);

simplify_inequality(equality_expr);

index_exprt new_index_expr(with_expr.op0(), expr.op1(), expr.type());
index_exprt new_index_expr(with_expr.old(), expr.op1(), expr.type());

simplify_index(new_index_expr); // recursive call

if(equality_expr.is_true())
{
expr=with_expr.op2();
expr = with_expr.new_value();
return false;
}
else if(equality_expr.is_false())
Expand All @@ -103,7 +103,7 @@ bool simplify_exprt::simplify_index(exprt &expr)
return false;
}

if_exprt if_expr(equality_expr, with_expr.op2(), new_index_expr);
if_exprt if_expr(equality_expr, with_expr.new_value(), new_index_expr);
simplify_if(if_expr);

expr.swap(if_expr);
Expand Down
6 changes: 3 additions & 3 deletions src/util/simplify_expr_floatbv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -293,9 +293,9 @@ bool simplify_exprt::simplify_floatbv_op(exprt &expr)
"binary operations have two operands, here an addtional parameter "
"is for the rounding mode");

exprt op0=expr.op0();
exprt op1=expr.op1();
exprt op2=expr.op2(); // rounding mode
exprt op0 = to_ieee_float_op_expr(expr).lhs();
exprt op1 = to_ieee_float_op_expr(expr).rhs();
exprt op2 = to_ieee_float_op_expr(expr).rounding_mode(); // rounding mode

INVARIANT(
op0.type() == type,
Expand Down
18 changes: 10 additions & 8 deletions src/util/simplify_expr_pointer.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -142,26 +142,28 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr)
if(expr.operands().size()==3)
{
bool result=true;
if(!simplify_rec(expr.op0()))
auto &if_expr = to_if_expr(expr);

if(!simplify_rec(if_expr.cond()))
result=false;
if(!simplify_address_of_arg(expr.op1()))
if(!simplify_address_of_arg(if_expr.true_case()))
result=false;
if(!simplify_address_of_arg(expr.op2()))
if(!simplify_address_of_arg(if_expr.false_case()))
result=false;

// op0 is a constant?
if(expr.op0().is_true())
// condition is a constant?
if(if_expr.cond().is_true())
{
result=false;
exprt tmp;
tmp.swap(expr.op1());
tmp.swap(if_expr.true_case());
expr.swap(tmp);
}
else if(expr.op0().is_false())
else if(if_expr.cond().is_false())
{
result=false;
exprt tmp;
tmp.swap(expr.op2());
tmp.swap(if_expr.false_case());
expr.swap(tmp);
}

Expand Down