Skip to content

introduce protected_exprt #3855

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 5 commits into from
Jan 29, 2019
Merged

introduce protected_exprt #3855

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
1280010
avoid direct access to exprt::op0()
Jan 24, 2019
6c14669
use conditional_cast instead of make_typecast
Jan 24, 2019
39d38f1
replace exprt::make_typecast() by typecast_exprt()
Jan 26, 2019
adb0533
multi_ary_exprt::opX with precondtion
Jan 25, 2019
a48f855
introduce expr_protectedt
Jan 24, 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
8 changes: 5 additions & 3 deletions src/ansi-c/expr2c.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1939,9 +1939,11 @@ std::string expr2ct::convert_constant(
if(src.operands().size()!=1)
return convert_norep(src, precedence);

if(src.op0().id()==ID_constant)
const auto &annotation = to_unary_expr(src).op();

if(annotation.id() == ID_constant)
{
const irep_idt &op_value=src.op0().get(ID_value);
const irep_idt &op_value = to_constant_expr(annotation).get_value();

if(op_value=="INVALID" ||
has_prefix(id2string(op_value), "INVALID-") ||
Expand All @@ -1951,7 +1953,7 @@ std::string expr2ct::convert_constant(
return convert_norep(src, precedence);
}
else
return convert_with_precedence(src.op0(), precedence);
return convert_with_precedence(annotation, precedence);
}
}
else if(type.id()==ID_string)
Expand Down
8 changes: 4 additions & 4 deletions src/goto-programs/remove_function_pointers.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -391,13 +391,13 @@ void remove_function_pointerst::remove_function_pointer(
t3->make_goto(t_final, true_exprt());

// goto to call
address_of_exprt address_of(fun, pointer_type(fun.type()));
const address_of_exprt address_of(fun, pointer_type(fun.type()));

if(address_of.type()!=pointer.type())
address_of.make_typecast(pointer.type());
const auto casted_address =
typecast_exprt::conditional_cast(address_of, pointer.type());

goto_programt::targett t4=new_code_gotos.add_instruction();
t4->make_goto(t1, equal_exprt(pointer, address_of));
t4->make_goto(t1, equal_exprt(pointer, casted_address));
}

// fall-through
Expand Down
8 changes: 6 additions & 2 deletions src/pointer-analysis/value_set_fi.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -853,9 +853,13 @@ void value_set_fit::get_reference_set_sharing_rec(
index_exprt index_expr(
object, from_integer(0, index_type()), expr.type());

exprt casted_index;

// adjust type?
if(object.type().id() != "#REF#" && object.type() != array_type)
index_expr.make_typecast(array.type());
casted_index = typecast_exprt(index_expr, array.type());
else
casted_index = index_expr;

offsett o = a_it->second;
mp_integer i;
Expand All @@ -868,7 +872,7 @@ void value_set_fit::get_reference_set_sharing_rec(
else
o.reset();

insert(dest, index_expr, o);
insert(dest, casted_index, o);
}
}

Expand Down
8 changes: 6 additions & 2 deletions src/pointer-analysis/value_set_fivr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -964,9 +964,13 @@ void value_set_fivrt::get_reference_set_sharing_rec(
index_exprt index_expr(
object, from_integer(0, index_type()), expr.type());

exprt casted_index;

// adjust type?
if(object.type().id() != "#REF#" && object.type() != array_type)
index_expr.make_typecast(array.type());
casted_index = typecast_exprt(index_expr, array.type());
else
casted_index = index_expr;

offsett o = a_it->second;
mp_integer i;
Expand All @@ -979,7 +983,7 @@ void value_set_fivrt::get_reference_set_sharing_rec(
else
o.reset();

insert_from(dest, index_expr, o);
insert_from(dest, casted_index, o);
}
}

Expand Down
10 changes: 7 additions & 3 deletions src/pointer-analysis/value_set_fivrns.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -657,9 +657,13 @@ void value_set_fivrnst::get_reference_set_rec(
index_exprt index_expr(
object, from_integer(0, index_type()), expr.type());

exprt casted_index;

// adjust type?
if(object.type() != array_type)
index_expr.make_typecast(array.type());
if(object.type().id() != "#REF#" && object.type() != array_type)
casted_index = typecast_exprt(index_expr, array.type());
else
casted_index = index_expr;

offsett o = a_it->second;
mp_integer i;
Expand All @@ -672,7 +676,7 @@ void value_set_fivrnst::get_reference_set_rec(
else
o.reset();

insert_from(dest, index_expr, o);
insert_from(dest, casted_index, o);
}
}

Expand Down
22 changes: 22 additions & 0 deletions src/util/expr.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -319,6 +319,28 @@ class exprt:public irept
const_unique_depth_iteratort unique_depth_cend() const;
};

/// Base class for all expressions. This protects low-level methods in
/// exprt that are not type safe. Depcrecated constructors are removed.
Copy link
Member

Choose a reason for hiding this comment

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

Typo in deprecated

/// This API will eventually replace exprt.
class expr_protectedt : public exprt
{
protected:
Copy link
Contributor

Choose a reason for hiding this comment

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

❓ Would it make more sense to use protected inheritance? I assume the answer is no as there remains calls to other methods, that have not been removed, but perhaps given this direction of travel it would making more sense to using them into the public section? (I think you can do this, but I have not actually tried).

Copy link
Contributor

Choose a reason for hiding this comment

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

This would circumvent the need for this class entirely and just update the classes that inherit from exprt to protected extend it and in fact allow for explicitly identifying the classes that use the wrong interface.

Copy link
Member Author

Choose a reason for hiding this comment

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

There are a lot of classes inheriting from exprt; furthermore, the interface of exprt should change as well, once we are there.

// constructors
expr_protectedt(const irep_idt &_id, const typet &_type) : exprt(_id, _type)
{
}

// protect these low-level methods
using exprt::add;
using exprt::make_bool;
using exprt::make_typecast;
using exprt::op0;
using exprt::op1;
using exprt::op2;
using exprt::op3;
using exprt::remove;
};

class expr_visitort
{
public:
Expand Down
4 changes: 1 addition & 3 deletions src/util/format_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,9 +104,7 @@ static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)

std::string operator_str = id2string(src.id()); // default

if(
src.id() == ID_equal && !src.operands().empty() &&
src.op0().type().id() == ID_bool)
if(src.id() == ID_equal && to_equal_expr(src).op0().type().id() == ID_bool)
{
operator_str = u8"\u21d4"; // <=>, U+21D4
}
Expand Down
10 changes: 6 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 @@ -1123,8 +1123,9 @@ bool simplify_exprt::simplify_if(if_exprt &expr)
else if(falsevalue.is_true())
{
// a?b:1 <-> !a OR b
or_exprt tmp(boolean_negate(cond), truevalue);
simplify_node(tmp.op0());
exprt tmp_not_cond = boolean_negate(cond);
simplify_node(tmp_not_cond);
or_exprt tmp(tmp_not_cond, truevalue);
simplify_node(tmp);
expr.swap(tmp);
return false;
Expand All @@ -1140,8 +1141,9 @@ bool simplify_exprt::simplify_if(if_exprt &expr)
else if(truevalue.is_false())
{
// a?0:b <-> !a && b
and_exprt tmp(boolean_negate(cond), falsevalue);
simplify_node(tmp.op0());
exprt tmp_not_cond = boolean_negate(cond);
simplify_node(tmp_not_cond);
and_exprt tmp(tmp_not_cond, falsevalue);
simplify_node(tmp);
expr.swap(tmp);
return false;
Expand Down
4 changes: 2 additions & 2 deletions src/util/std_expr.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,8 +167,8 @@ extractbits_exprt::extractbits_exprt(
const exprt &_src,
const std::size_t _upper,
const std::size_t _lower,
const typet &_type):
exprt(ID_extractbits, _type)
const typet &_type)
: expr_protectedt(ID_extractbits, _type)
{
PRECONDITION(_upper >= _lower);
operands().resize(3);
Expand Down
Loading