Skip to content

Commit cd7d05d

Browse files
author
Daniel Kroening
committed
introduce protected_exprt
This will serve as the interface that we aspire exprt to offer; in particular, access to opX is protected.
1 parent 8474807 commit cd7d05d

14 files changed

+152
-124
lines changed

src/analyses/goto_check.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1293,7 +1293,7 @@ void goto_checkt::bounds_check(
12931293
const exprt &pointer=
12941294
to_dereference_expr(ode.root_object()).pointer();
12951295

1296-
if_exprt size(
1296+
exprt size = if_exprt(
12971297
dynamic_object(pointer),
12981298
typecast_exprt(dynamic_size(ns), object_size(pointer).type()),
12991299
object_size(pointer));

src/ansi-c/expr2c.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1941,9 +1941,11 @@ std::string expr2ct::convert_constant(
19411941
if(src.operands().size()!=1)
19421942
return convert_norep(src, precedence);
19431943

1944-
if(src.op0().id()==ID_constant)
1944+
const auto &annotation = to_unary_expr(src).op();
1945+
1946+
if(annotation.id() == ID_constant)
19451947
{
1946-
const irep_idt &op_value=src.op0().get(ID_value);
1948+
const irep_idt &op_value = to_constant_expr(annotation).get_value();
19471949

19481950
if(op_value=="INVALID" ||
19491951
has_prefix(id2string(op_value), "INVALID-") ||
@@ -1953,7 +1955,7 @@ std::string expr2ct::convert_constant(
19531955
return convert_norep(src, precedence);
19541956
}
19551957
else
1956-
return convert_with_precedence(src.op0(), precedence);
1958+
return convert_with_precedence(annotation, precedence);
19571959
}
19581960
}
19591961
else if(type.id()==ID_string)

src/goto-programs/remove_function_pointers.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -392,13 +392,13 @@ void remove_function_pointerst::remove_function_pointer(
392392
t3->make_goto(t_final, true_exprt());
393393

394394
// goto to call
395-
address_of_exprt address_of(fun, pointer_type(fun.type()));
395+
const address_of_exprt address_of(fun, pointer_type(fun.type()));
396396

397-
if(address_of.type()!=pointer.type())
398-
address_of.make_typecast(pointer.type());
397+
const auto casted_address =
398+
typecast_exprt::conditional_cast(address_of, pointer.type());
399399

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

404404
// fall-through

src/pointer-analysis/value_set_fi.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -870,8 +870,8 @@ void value_set_fit::get_reference_set_sharing_rec(
870870
insert(dest, exprt(ID_unknown, expr.type()));
871871
else
872872
{
873-
index_exprt index_expr(
874-
object, from_integer(0, index_type()), expr.type());
873+
exprt index_expr =
874+
index_exprt(object, from_integer(0, index_type()), expr.type());
875875

876876
// adjust type?
877877
if(object.type().id() != "#REF#" && object.type() != array_type)

src/pointer-analysis/value_set_fivr.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -981,8 +981,8 @@ void value_set_fivrt::get_reference_set_sharing_rec(
981981
insert_from(dest, exprt(ID_unknown, expr.type()));
982982
else
983983
{
984-
index_exprt index_expr(
985-
object, from_integer(0, index_type()), expr.type());
984+
exprt index_expr =
985+
index_exprt(object, from_integer(0, index_type()), expr.type());
986986

987987
// adjust type?
988988
if(object.type().id() != "#REF#" && object.type() != array_type)

src/pointer-analysis/value_set_fivrns.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -674,8 +674,8 @@ void value_set_fivrnst::get_reference_set_rec(
674674
insert_from(dest, exprt(ID_unknown, expr.type()));
675675
else
676676
{
677-
index_exprt index_expr(
678-
object, from_integer(0, index_type()), expr.type());
677+
exprt index_expr =
678+
index_exprt(object, from_integer(0, index_type()), expr.type());
679679

680680
// adjust type?
681681
if(object.type() != array_type)

src/solvers/flattening/arrays.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -546,7 +546,7 @@ void arrayst::add_array_constraints_with(
546546
{
547547
const typet &subtype = expr.type().subtype();
548548
index_exprt index_expr1(expr, other_index, subtype);
549-
index_exprt index_expr2(expr.op0(), other_index, subtype);
549+
index_exprt index_expr2(expr.old(), other_index, subtype);
550550

551551
equal_exprt equality_expr(index_expr1, index_expr2);
552552

@@ -646,12 +646,12 @@ void arrayst::add_array_constraints_array_of(
646646
index_exprt index_expr(expr, index, subtype);
647647

648648
DATA_INVARIANT(
649-
base_type_eq(index_expr.type(), expr.op0().type(), ns),
649+
base_type_eq(index_expr.type(), expr.what().type(), ns),
650650
"array_of operand type should match array element type");
651651

652652
// add constraint
653653
lazy_constraintt lazy(
654-
lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.op0()));
654+
lazy_typet::ARRAY_OF, equal_exprt(index_expr, expr.what()));
655655
add_array_constraint(lazy, false); // added immediately
656656
}
657657
}

src/solvers/flattening/boolbv_array_of.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,7 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
4242
if(to_integer(array_size, size))
4343
return conversion_failed(expr);
4444

45-
const bvt &tmp=convert_bv(expr.op0());
45+
const bvt &tmp = convert_bv(expr.what());
4646

4747
INVARIANT(
4848
size * tmp.size() == width,

src/solvers/smt2/smt2_conv.cpp

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -3361,11 +3361,11 @@ void smt2_convt::convert_floatbv_div(const ieee_float_op_exprt &expr)
33613361
if(use_FPA_theory)
33623362
{
33633363
out << "(fp.div ";
3364-
convert_rounding_mode_FPA(expr.op2());
3364+
convert_rounding_mode_FPA(expr.rounding_mode());
33653365
out << " ";
3366-
convert_expr(expr.op0());
3366+
convert_expr(expr.lhs());
33673367
out << " ";
3368-
convert_expr(expr.op1());
3368+
convert_expr(expr.rhs());
33693369
out << ")";
33703370
}
33713371
else
@@ -3555,8 +3555,8 @@ void smt2_convt::convert_with(const with_exprt &expr)
35553555
{
35563556
const struct_typet &struct_type = to_struct_type(ns.follow(expr_type));
35573557

3558-
const exprt &index=expr.op1();
3559-
const exprt &value=expr.op2();
3558+
const exprt &index = expr.where();
3559+
const exprt &value = expr.new_value();
35603560

35613561
const irep_idt &component_name=index.get(ID_component_name);
35623562

@@ -3569,7 +3569,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
35693569
const std::string &smt_typename = datatype_map.at(expr_type);
35703570

35713571
out << "(update-" << smt_typename << "." << component_name << " ";
3572-
convert_expr(expr.op0());
3572+
convert_expr(expr.old());
35733573
out << " ";
35743574
convert_expr(value);
35753575
out << ")";
@@ -3583,7 +3583,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
35833583
boolbv_width.get_member(struct_type, component_name);
35843584

35853585
out << "(let ((?withop ";
3586-
convert_expr(expr.op0());
3586+
convert_expr(expr.old());
35873587
out << ")) ";
35883588

35893589
if(m.width==struct_width)
@@ -3626,7 +3626,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
36263626
{
36273627
const union_typet &union_type = to_union_type(ns.follow(expr_type));
36283628

3629-
const exprt &value=expr.op2();
3629+
const exprt &value = expr.new_value();
36303630

36313631
std::size_t total_width=boolbv_width(union_type);
36323632
CHECK_RETURN_WITH_DIAGNOSTICS(
@@ -3651,7 +3651,7 @@ void smt2_convt::convert_with(const with_exprt &expr)
36513651
out << "((_ extract "
36523652
<< (total_width-1)
36533653
<< " " << member_width << ") ";
3654-
convert_expr(expr.op0());
3654+
convert_expr(expr.old());
36553655
out << ") ";
36563656
flatten2bv(value);
36573657
out << ")";

src/util/expr.h

Lines changed: 34 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -318,6 +318,40 @@ class exprt:public irept
318318
const_unique_depth_iteratort unique_depth_cend() const;
319319
};
320320

321+
/// Protected class for all expressions.
322+
/// This API will eventually replace exprt.
323+
class protected_exprt : public exprt
324+
{
325+
protected:
326+
// constructors
327+
DEPRECATED("use protected_exprt(id, type) instead")
328+
protected_exprt() : exprt()
329+
{
330+
}
331+
332+
DEPRECATED("use protected_exprt(id, type) instead")
333+
explicit protected_exprt(const irep_idt &_id) : exprt(_id)
334+
{
335+
}
336+
337+
protected_exprt(const irep_idt &_id, const typet &_type) : exprt(_id, _type)
338+
{
339+
}
340+
341+
// protect these low-level methods
342+
using exprt::make_bool;
343+
using exprt::make_typecast;
344+
using exprt::op0;
345+
using exprt::op1;
346+
using exprt::op2;
347+
using exprt::op3;
348+
// using exprt::find;
349+
// using exprt::get;
350+
// using exprt::set;
351+
using exprt::add;
352+
using exprt::remove;
353+
};
354+
321355
class expr_visitort
322356
{
323357
public:

src/util/pointer_offset_size.cpp

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -595,8 +595,11 @@ exprt build_sizeof_expr(
595595
const constant_exprt &expr,
596596
const namespacet &ns)
597597
{
598-
const typet &type=
599-
static_cast<const typet &>(expr.find(ID_C_c_sizeof_type));
598+
// need to cast down to access 'find'
599+
const auto &expr_as_irep = static_cast<const irept &>(expr);
600+
601+
const typet &type =
602+
static_cast<const typet &>(expr_as_irep.find(ID_C_c_sizeof_type));
600603

601604
if(type.is_nil())
602605
return nil_exprt();

src/util/simplify_expr.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1889,7 +1889,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
18891889
exprt compo_offset = from_integer(*i, offset.type());
18901890
plus_exprt new_offset(offset, compo_offset);
18911891
simplify_node(new_offset);
1892-
exprt new_value(with.op2());
1892+
exprt new_value(with.new_value());
18931893
expr.op1().swap(new_offset);
18941894
expr.op2().swap(new_value);
18951895
simplify_byte_update(expr); // do this recursively
@@ -1916,7 +1916,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
19161916

19171917
plus_exprt new_offset(offset, index_offset);
19181918
simplify_node(new_offset);
1919-
exprt new_value(with.op2());
1919+
exprt new_value(with.new_value());
19201920
expr.op1().swap(new_offset);
19211921
expr.op2().swap(new_value);
19221922
simplify_byte_update(expr); // do this recursively

src/util/std_expr.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -149,8 +149,8 @@ extractbits_exprt::extractbits_exprt(
149149
const exprt &_src,
150150
const std::size_t _upper,
151151
const std::size_t _lower,
152-
const typet &_type):
153-
exprt(ID_extractbits, _type)
152+
const typet &_type)
153+
: protected_exprt(ID_extractbits, _type)
154154
{
155155
PRECONDITION(_upper >= _lower);
156156
operands().resize(3);

0 commit comments

Comments
 (0)