diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index f9bf56d92d4..23aaf0b9030 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -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-") || @@ -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) diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 8fe9a739626..2f6df1409e3 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -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 diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp index 0ffb6814cfe..05eedbf1bb3 100644 --- a/src/pointer-analysis/value_set_fi.cpp +++ b/src/pointer-analysis/value_set_fi.cpp @@ -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; @@ -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); } } diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp index c72a9578ced..c82fd4066d9 100644 --- a/src/pointer-analysis/value_set_fivr.cpp +++ b/src/pointer-analysis/value_set_fivr.cpp @@ -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; @@ -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); } } diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp index 49014e22297..c1c58d1b4a8 100644 --- a/src/pointer-analysis/value_set_fivrns.cpp +++ b/src/pointer-analysis/value_set_fivrns.cpp @@ -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; @@ -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); } } diff --git a/src/util/expr.h b/src/util/expr.h index 94ecf1dee0f..8150cee98f9 100644 --- a/src/util/expr.h +++ b/src/util/expr.h @@ -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. +/// This API will eventually replace exprt. +class expr_protectedt : public exprt +{ +protected: + // 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: diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 1162dd9883f..f8b36335b48 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -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 } diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 9df4c4ff51c..38fbe13c7fc 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -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; @@ -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; diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 251d00b7c27..c549178259f 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -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); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index 9c8bd7363ad..381fd9ca75b 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -20,16 +20,17 @@ Author: Daniel Kroening, kroening@kroening.com #include /// An expression without operands -class nullary_exprt : public exprt +class nullary_exprt : public expr_protectedt { public: // constructors DEPRECATED("use nullary_exprt(id, type) instead") - explicit nullary_exprt(const irep_idt &_id) : exprt(_id) + explicit nullary_exprt(const irep_idt &_id) : expr_protectedt(_id, typet()) { } - nullary_exprt(const irep_idt &_id, const typet &_type) : exprt(_id, _type) + nullary_exprt(const irep_idt &_id, const typet &_type) + : expr_protectedt(_id, _type) { } @@ -56,19 +57,19 @@ class nullary_exprt : public exprt }; /// An expression with three operands -class ternary_exprt : public exprt +class ternary_exprt : public expr_protectedt { public: // constructors DEPRECATED("use ternary_exprt(id, op0, op1, op2, type) instead") - explicit ternary_exprt(const irep_idt &_id) : exprt(_id) + explicit ternary_exprt(const irep_idt &_id) : expr_protectedt(_id, type()) { operands().resize(3); } DEPRECATED("use ternary_exprt(id, op0, op1, op2, type) instead") explicit ternary_exprt(const irep_idt &_id, const typet &_type) - : exprt(_id, _type) + : expr_protectedt(_id, _type) { operands().resize(3); } @@ -79,11 +80,16 @@ class ternary_exprt : public exprt const exprt &_op1, const exprt &_op2, const typet &_type) - : exprt(_id, _type) + : expr_protectedt(_id, _type) { add_to_operands(_op0, _op1, _op2); } + // make op0 to op2 public + using exprt::op0; + using exprt::op1; + using exprt::op2; + const exprt &op3() const = delete; exprt &op3() = delete; }; @@ -286,42 +292,36 @@ inline void validate_expr(const nondet_symbol_exprt &value) /// \brief Generic base class for unary expressions -class unary_exprt:public exprt +class unary_exprt : public expr_protectedt { public: DEPRECATED("use unary_exprt(id, op) instead") - unary_exprt() + unary_exprt() : expr_protectedt(irep_idt(), typet()) { operands().resize(1); } DEPRECATED("use unary_exprt(id, op) instead") - explicit unary_exprt(const irep_idt &_id):exprt(_id) + explicit unary_exprt(const irep_idt &_id) : expr_protectedt(_id, typet()) { operands().resize(1); } - unary_exprt( - const irep_idt &_id, - const exprt &_op): - exprt(_id, _op.type()) + unary_exprt(const irep_idt &_id, const exprt &_op) + : expr_protectedt(_id, _op.type()) { add_to_operands(_op); } DEPRECATED("use unary_exprt(id, op, type) instead") - unary_exprt( - const irep_idt &_id, - const typet &_type):exprt(_id, _type) + unary_exprt(const irep_idt &_id, const typet &_type) + : expr_protectedt(_id, _type) { operands().resize(1); } - unary_exprt( - const irep_idt &_id, - const exprt &_op, - const typet &_type): - exprt(_id, _type) + unary_exprt(const irep_idt &_id, const exprt &_op, const typet &_type) + : expr_protectedt(_id, _type) { add_to_operands(_op); } @@ -588,32 +588,29 @@ inline void validate_expr(const bswap_exprt &value) /// \brief A base class for expressions that are predicates, /// i.e., Boolean-typed. -class predicate_exprt:public exprt +class predicate_exprt : public expr_protectedt { public: DEPRECATED("use predicate_exprt(id) instead") - predicate_exprt():exprt(irep_idt(), bool_typet()) + predicate_exprt() : expr_protectedt(irep_idt(), bool_typet()) { } - explicit predicate_exprt(const irep_idt &_id): - exprt(_id, bool_typet()) + explicit predicate_exprt(const irep_idt &_id) + : expr_protectedt(_id, bool_typet()) { } DEPRECATED("use unary_predicate_exprt(id, op) instead") - predicate_exprt( - const irep_idt &_id, - const exprt &_op):exprt(_id, bool_typet()) + predicate_exprt(const irep_idt &_id, const exprt &_op) + : expr_protectedt(_id, bool_typet()) { add_to_operands(_op); } DEPRECATED("use binary_predicate_exprt(op1, id, op2) instead") - predicate_exprt( - const irep_idt &_id, - const exprt &_op0, - const exprt &_op1):exprt(_id, bool_typet()) + predicate_exprt(const irep_idt &_id, const exprt &_op0, const exprt &_op1) + : expr_protectedt(_id, bool_typet()) { add_to_operands(_op0, _op1); } @@ -693,34 +690,30 @@ inline void validate_expr(const sign_exprt &expr) } /// \brief A base class for binary expressions -class binary_exprt:public exprt +class binary_exprt : public expr_protectedt { public: DEPRECATED("use binary_exprt(lhs, id, rhs) instead") - binary_exprt() + binary_exprt() : expr_protectedt(irep_idt(), typet()) { operands().resize(2); } DEPRECATED("use binary_exprt(lhs, id, rhs) instead") - explicit binary_exprt(const irep_idt &_id):exprt(_id) + explicit binary_exprt(const irep_idt &_id) : expr_protectedt(_id, typet()) { operands().resize(2); } DEPRECATED("use binary_exprt(lhs, id, rhs, type) instead") - binary_exprt( - const irep_idt &_id, - const typet &_type):exprt(_id, _type) + binary_exprt(const irep_idt &_id, const typet &_type) + : expr_protectedt(_id, _type) { operands().resize(2); } - binary_exprt( - const exprt &_lhs, - const irep_idt &_id, - const exprt &_rhs): - exprt(_id, _lhs.type()) + binary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs) + : expr_protectedt(_id, _lhs.type()) { add_to_operands(_lhs, _rhs); } @@ -729,8 +722,8 @@ class binary_exprt:public exprt const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, - const typet &_type): - exprt(_id, _type) + const typet &_type) + : expr_protectedt(_id, _type) { add_to_operands(_lhs, _rhs); } @@ -753,6 +746,10 @@ class binary_exprt:public exprt check(expr, vm); } + // make op0 and op1 public + using exprt::op0; + using exprt::op1; + const exprt &op2() const = delete; exprt &op2() = delete; const exprt &op3() const = delete; @@ -927,23 +924,22 @@ template<> inline bool can_cast_expr(const exprt &base) /// \brief A base class for multi-ary expressions /// Associativity is not specified. -class multi_ary_exprt:public exprt +class multi_ary_exprt : public expr_protectedt { public: DEPRECATED("use multi_ary_exprt(id, op, type) instead") - multi_ary_exprt() + multi_ary_exprt() : expr_protectedt(irep_idt(), typet()) { } DEPRECATED("use multi_ary_exprt(id, op, type) instead") - explicit multi_ary_exprt(const irep_idt &_id):exprt(_id) + explicit multi_ary_exprt(const irep_idt &_id) : expr_protectedt(_id, typet()) { } DEPRECATED("use multi_ary_exprt(id, op, type) instead") - multi_ary_exprt( - const irep_idt &_id, - const typet &_type):exprt(_id, _type) + multi_ary_exprt(const irep_idt &_id, const typet &_type) + : expr_protectedt(_id, _type) { } @@ -951,16 +947,13 @@ class multi_ary_exprt:public exprt const irep_idt &_id, operandst &&_operands, const typet &_type) - : exprt(_id, _type) + : expr_protectedt(_id, _type) { operands() = std::move(_operands); } - multi_ary_exprt( - const exprt &_lhs, - const irep_idt &_id, - const exprt &_rhs): - exprt(_id, _lhs.type()) + multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, const exprt &_rhs) + : expr_protectedt(_id, _lhs.type()) { add_to_operands(_lhs, _rhs); } @@ -969,11 +962,61 @@ class multi_ary_exprt:public exprt const exprt &_lhs, const irep_idt &_id, const exprt &_rhs, - const typet &_type): - exprt(_id, _type) + const typet &_type) + : expr_protectedt(_id, _type) { add_to_operands(_lhs, _rhs); } + + // In contrast to exprt::opX, the methods + // below check the size. + exprt &op0() + { + PRECONDITION(operands().size() >= 1); + return operands().front(); + } + + exprt &op1() + { + PRECONDITION(operands().size() >= 2); + return operands()[1]; + } + + exprt &op2() + { + PRECONDITION(operands().size() >= 3); + return operands()[2]; + } + + exprt &op3() + { + PRECONDITION(operands().size() >= 4); + return operands()[3]; + } + + const exprt &op0() const + { + PRECONDITION(operands().size() >= 1); + return operands().front(); + } + + const exprt &op1() const + { + PRECONDITION(operands().size() >= 2); + return operands()[1]; + } + + const exprt &op2() const + { + PRECONDITION(operands().size() >= 3); + return operands()[2]; + } + + const exprt &op3() const + { + PRECONDITION(operands().size() >= 4); + return operands()[3]; + } }; /// \brief Cast an exprt to a \ref multi_ary_exprt @@ -3064,11 +3107,11 @@ inline void validate_expr(const extractbit_exprt &value) /// \brief Extracts a sub-range of a bit-vector operand -class extractbits_exprt:public exprt +class extractbits_exprt : public expr_protectedt { public: DEPRECATED("use extractbits_exprt(value, upper, lower) instead") - extractbits_exprt():exprt(ID_extractbits) + extractbits_exprt() : expr_protectedt(ID_extractbits, typet()) { operands().resize(3); } @@ -3082,7 +3125,8 @@ class extractbits_exprt:public exprt const exprt &_src, const exprt &_upper, const exprt &_lower, - const typet &_type):exprt(ID_extractbits, _type) + const typet &_type) + : expr_protectedt(ID_extractbits, _type) { add_to_operands(_src, _upper, _lower); } @@ -3421,20 +3465,17 @@ inline void validate_expr(const if_exprt &value) /// \brief Operator to update elements in structs and arrays /// \remark This expression will eventually be replaced by separate /// array and struct update operators. -class with_exprt:public exprt +class with_exprt : public expr_protectedt { public: - with_exprt( - const exprt &_old, - const exprt &_where, - const exprt &_new_value): - exprt(ID_with, _old.type()) + with_exprt(const exprt &_old, const exprt &_where, const exprt &_new_value) + : expr_protectedt(ID_with, _old.type()) { add_to_operands(_old, _where, _new_value); } DEPRECATED("use with_exprt(old, where, new_value) instead") - with_exprt():exprt(ID_with) + with_exprt() : expr_protectedt(ID_with, typet()) { operands().resize(3); } @@ -3507,12 +3548,11 @@ inline void validate_expr(const with_exprt &value) "Array/structure update must have three operands"); } - -class index_designatort:public exprt +class index_designatort : public expr_protectedt { public: - explicit index_designatort(const exprt &_index): - exprt(ID_index_designator) + explicit index_designatort(const exprt &_index) + : expr_protectedt(ID_index_designator, typet()) { add_to_operands(_index); } @@ -3562,12 +3602,11 @@ inline void validate_expr(const index_designatort &value) validate_operands(value, 1, "Index designator must have one operand"); } - -class member_designatort:public exprt +class member_designatort : public expr_protectedt { public: - explicit member_designatort(const irep_idt &_component_name): - exprt(ID_member_designator) + explicit member_designatort(const irep_idt &_component_name) + : expr_protectedt(ID_member_designator, typet()) { set(ID_component_name, _component_name); } @@ -3711,7 +3750,7 @@ inline void validate_expr(const update_exprt &value) #if 0 /// \brief Update of one element of an array -class array_update_exprt:public exprt +class array_update_exprt:public expr_protectedt { public: array_update_exprt( @@ -3723,7 +3762,7 @@ class array_update_exprt:public exprt add_to_operands(_array, _index, _new_value); } - array_update_exprt():exprt(ID_array_update) + array_update_exprt():expr_protectedt(ID_array_update) { operands().resize(3); } @@ -4284,21 +4323,22 @@ class type_exprt : public nullary_exprt }; /// \brief A constant literal expression -class constant_exprt:public exprt +class constant_exprt : public expr_protectedt { public: DEPRECATED("use constant_exprt(value, type) instead") - constant_exprt():exprt(ID_constant) + constant_exprt() : expr_protectedt(ID_constant, typet()) { } DEPRECATED("use constant_exprt(value, type) instead") - explicit constant_exprt(const typet &type):exprt(ID_constant, type) + explicit constant_exprt(const typet &type) + : expr_protectedt(ID_constant, type) { } - constant_exprt(const irep_idt &_value, const typet &_type): - exprt(ID_constant, _type) + constant_exprt(const irep_idt &_value, const typet &_type) + : expr_protectedt(ID_constant, _type) { set_value(_value); }