diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index b241150d7ba..fb675b77b20 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -67,11 +67,17 @@ irep_idt custom_bitvector_domaint::object2id(const exprt &src) } else if(op.id()==ID_typecast) { - return object2id(dereference_exprt(to_typecast_expr(op).op())); + irep_idt op_id=object2id(to_typecast_expr(op).op()); + + if(op_id.empty()) + return irep_idt(); + else + return '*'+id2string(op_id); } else { irep_idt op_id=object2id(op); + if(op_id.empty()) return irep_idt(); else @@ -188,9 +194,8 @@ std::set custom_bitvector_analysist::aliases( std::set result; for(const auto &pointer : pointer_set) - { - result.insert(dereference_exprt(pointer)); - } + if(pointer.type().id()==ID_pointer) + result.insert(dereference_exprt(pointer)); result.insert(src); @@ -300,36 +305,39 @@ void custom_bitvector_domaint::transform( exprt lhs=code_function_call.arguments()[0]; - if(lhs.is_constant() && - to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all + if(lhs.type().id()==ID_pointer) { - if(mode==modet::CLEAR_MAY) + if(lhs.is_constant() && + to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all { - for(auto &bit : may_bits) - clear_bit(bit.second, bit_nr); - - // erase blank ones - erase_blank_vectors(may_bits); + if(mode==modet::CLEAR_MAY) + { + for(auto &bit : may_bits) + clear_bit(bit.second, bit_nr); + + // erase blank ones + erase_blank_vectors(may_bits); + } + else if(mode==modet::CLEAR_MUST) + { + for(auto &bit : must_bits) + clear_bit(bit.second, bit_nr); + + // erase blank ones + erase_blank_vectors(must_bits); + } } - else if(mode==modet::CLEAR_MUST) + else { - for(auto &bit : must_bits) - clear_bit(bit.second, bit_nr); - - // erase blank ones - erase_blank_vectors(must_bits); - } - } - else - { - dereference_exprt deref(lhs); + dereference_exprt deref(lhs); - // may alias other stuff - std::set lhs_set=cba.aliases(deref, from); + // may alias other stuff + std::set lhs_set=cba.aliases(deref, from); - for(const auto &lhs : lhs_set) - { - set_bit(lhs, bit_nr, mode); + for(const auto &lhs : lhs_set) + { + set_bit(lhs, bit_nr, mode); + } } } } @@ -415,40 +423,43 @@ void custom_bitvector_domaint::transform( exprt lhs=instruction.code.op0(); - if(lhs.is_constant() && - to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all + if(lhs.type().id()==ID_pointer) { - if(mode==modet::CLEAR_MAY) + if(lhs.is_constant() && + to_constant_expr(lhs).get_value()==ID_NULL) // NULL means all { - for(bitst::iterator b_it=may_bits.begin(); - b_it!=may_bits.end(); - b_it++) - clear_bit(b_it->second, bit_nr); + if(mode==modet::CLEAR_MAY) + { + for(bitst::iterator b_it=may_bits.begin(); + b_it!=may_bits.end(); + b_it++) + clear_bit(b_it->second, bit_nr); - // erase blank ones - erase_blank_vectors(may_bits); - } - else if(mode==modet::CLEAR_MUST) - { - for(bitst::iterator b_it=must_bits.begin(); - b_it!=must_bits.end(); - b_it++) - clear_bit(b_it->second, bit_nr); + // erase blank ones + erase_blank_vectors(may_bits); + } + else if(mode==modet::CLEAR_MUST) + { + for(bitst::iterator b_it=must_bits.begin(); + b_it!=must_bits.end(); + b_it++) + clear_bit(b_it->second, bit_nr); - // erase blank ones - erase_blank_vectors(must_bits); + // erase blank ones + erase_blank_vectors(must_bits); + } } - } - else - { - dereference_exprt deref(lhs); + else + { + dereference_exprt deref(lhs); - // may alias other stuff - std::set lhs_set=cba.aliases(deref, from); + // may alias other stuff + std::set lhs_set=cba.aliases(deref, from); - for(const auto &lhs : lhs_set) - { - set_bit(lhs, bit_nr, mode); + for(const auto &lhs : lhs_set) + { + set_bit(lhs, bit_nr, mode); + } } } } @@ -628,6 +639,9 @@ exprt custom_bitvector_domaint::eval( exprt pointer=src.op0(); + if(pointer.type().id()!=ID_pointer) + return src; + if(pointer.is_constant() && to_constant_expr(pointer).get_value()==ID_NULL) // NULL means all { diff --git a/src/cpp/cpp_typecheck_resolve.cpp b/src/cpp/cpp_typecheck_resolve.cpp index 97fd84135ee..ea116ba3952 100644 --- a/src/cpp/cpp_typecheck_resolve.cpp +++ b/src/cpp/cpp_typecheck_resolve.cpp @@ -2127,9 +2127,11 @@ void cpp_typecheck_resolvet::apply_template_args( DATA_INVARIANT(struct_type.has_component(new_symbol.name), "method should exist in struct"); - member_exprt member(code_type); - member.set_component_name(new_symbol.name); - member.struct_op()=*fargs.operands.begin(); + + member_exprt member( + *fargs.operands.begin(), + new_symbol.name, + code_type); member.add_source_location()=source_location; expr.swap(member); return; diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index b2542cbeee7..280635aed60 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -417,7 +417,7 @@ void interpretert::execute_decl() /// retrieves the member at offset /// \par parameters: an object and a memory offset -irep_idt interpretert::get_component_id( +struct_typet::componentt interpretert::get_component( const irep_idt &object, unsigned offset) { @@ -428,15 +428,16 @@ irep_idt interpretert::get_component_id( const struct_typet &struct_type=to_struct_type(real_type); const struct_typet::componentst &components=struct_type.components(); - for(struct_typet::componentst::const_iterator it=components.begin(); - it!=components.end(); it++) + + for(const auto &c : components) { if(offset<=0) - return it->id(); - size_t size=get_size(it->type()); - offset-=size; + return c; + + offset-=get_size(c.type()); } - return object; + + throw "access out of struct bounds"; } /// returns the type object corresponding to id @@ -600,6 +601,7 @@ exprt interpretert::get_value( result.set_value(ID_NULL); return result; } + if(rhs[offset] #include +#include #include +#include #include "goto_functions.h" #include "goto_trace.h" #include "json_goto_trace.h" -#include "util/message.h" class interpretert:public messaget { @@ -195,7 +196,10 @@ class interpretert:public messaget bool unbounded_size(const typet &); size_t get_size(const typet &type); - irep_idt get_component_id(const irep_idt &object, unsigned offset); + struct_typet::componentt get_component( + const irep_idt &object, + unsigned offset); + typet get_type(const irep_idt &id) const; exprt get_value( const typet &type, diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp index 05f9371e492..005d6ab3a8f 100644 --- a/src/goto-programs/string_abstraction.cpp +++ b/src/goto-programs/string_abstraction.cpp @@ -1333,19 +1333,24 @@ exprt string_abstractiont::member(const exprt &a, whatt what) { if(a.is_nil()) return a; + assert(type_eq(a.type(), string_struct, ns) || is_ptr_string_struct(a.type())); - member_exprt result(build_type(what)); - result.struct_op()=a.type().id()==ID_pointer? + exprt struct_op= + a.type().id()==ID_pointer? dereference_exprt(a, string_struct):a; + irep_idt component_name; + switch(what) { - case whatt::IS_ZERO: result.set_component_name("is_zero"); break; - case whatt::SIZE: result.set_component_name("size"); break; - case whatt::LENGTH: result.set_component_name("length"); break; + case whatt::IS_ZERO: component_name="is_zero"; break; + case whatt::SIZE: component_name="size"; break; + case whatt::LENGTH: component_name="length"; break; } + member_exprt result(struct_op, component_name, build_type(what)); + return result; } diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp index 0f89277ff94..7b2289256bf 100644 --- a/src/linking/linking.cpp +++ b/src/linking/linking.cpp @@ -200,7 +200,7 @@ void linkingt::detailed_conflict_report_rec( conflict_path=conflict_path_before; conflict_path.type()=t1; conflict_path= - member_exprt(conflict_path, components1[i].get_name()); + member_exprt(conflict_path, components1[i]); if(depth>0 && parent_types.find(t1)==parent_types.end()) diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp index 406cac0f99c..1f2d7476914 100644 --- a/src/pointer-analysis/value_set.cpp +++ b/src/pointer-analysis/value_set.cpp @@ -833,7 +833,7 @@ void value_sett::get_value_set_rec( found=true; - member_exprt member(expr.op0(), name, c_it->type()); + member_exprt member(expr.op0(), *c_it); get_value_set_rec(member, dest, suffix, original_type, ns); } } @@ -1050,9 +1050,7 @@ void value_sett::get_reference_set_rec( { objectt o=it->second; - member_exprt member_expr(expr.type()); - member_expr.op0()=object; - member_expr.set_component_name(component_name); + member_exprt member_expr(object, component_name, expr.type()); // We cannot introduce a cast from scalar to non-scalar, // thus, we can only adjust the types of structs and unions. @@ -1121,9 +1119,7 @@ void value_sett::assign( if(subtype.id()==ID_code || c_it->get_is_padding()) continue; - member_exprt lhs_member(subtype); - lhs_member.set_component_name(name); - lhs_member.op0()=lhs; + member_exprt lhs_member(lhs, name, subtype); exprt rhs_member; @@ -1698,9 +1694,7 @@ exprt value_sett::make_member( // give up typet subtype=struct_union_type.component_type(component_name); - member_exprt member_expr(subtype); - member_expr.op0()=src; - member_expr.set_component_name(component_name); + member_exprt member_expr(src, component_name, subtype); return member_expr; } diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp index 63a2c809b5d..5bbbad458f2 100644 --- a/src/solvers/flattening/pointer_logic.cpp +++ b/src/solvers/flattening/pointer_logic.cpp @@ -146,14 +146,11 @@ exprt pointer_logict::object_rec( mp_integer current_offset=0; - for(struct_typet::componentst::const_iterator - it=components.begin(); - it!=components.end(); - it++) + for(const auto &c : components) { assert(offset>=current_offset); - const typet &subtype=it->type(); + const typet &subtype=c.type(); mp_integer sub_size=pointer_offset_size(subtype, ns); assert(sub_size>0); @@ -162,9 +159,7 @@ exprt pointer_logict::object_rec( if(new_offset>offset) { // found it - member_exprt tmp(subtype); - tmp.set_component_name(it->get_name()); - tmp.op0()=src; + member_exprt tmp(src, c); return object_rec( offset-current_offset, pointer_type, tmp); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index e1d6e06c912..702602ac7ef 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -1329,32 +1329,28 @@ inline void validate_expr(const notequal_exprt &value) /*! \brief array index operator */ -class index_exprt:public exprt +class index_exprt:public binary_exprt { public: - index_exprt():exprt(ID_index) + index_exprt():binary_exprt(ID_index) { - operands().resize(2); } - explicit index_exprt(const typet &_type):exprt(ID_index, _type) + explicit index_exprt(const typet &_type):binary_exprt(ID_index, _type) { - operands().resize(2); } index_exprt(const exprt &_array, const exprt &_index): - exprt(ID_index, _array.type().subtype()) + binary_exprt(_array, ID_index, _index, _array.type().subtype()) { - copy_to_operands(_array, _index); } index_exprt( const exprt &_array, const exprt &_index, const typet &_type): - exprt(ID_index, _type) + binary_exprt(_array, ID_index, _index, _type) { - copy_to_operands(_array, _index); } exprt &array() @@ -1795,12 +1791,11 @@ class namespacet; /*! \brief split an expression into a base object and a (byte) offset */ -class object_descriptor_exprt:public exprt +class object_descriptor_exprt:public binary_exprt { public: - object_descriptor_exprt():exprt(ID_object_descriptor) + object_descriptor_exprt():binary_exprt(ID_object_descriptor) { - operands().resize(2); op0().id(ID_unknown); op1().id(ID_unknown); } @@ -1886,20 +1881,18 @@ inline void validate_expr(const object_descriptor_exprt &value) /*! \brief TO_BE_DOCUMENTED */ -class dynamic_object_exprt:public exprt +class dynamic_object_exprt:public binary_exprt { public: - dynamic_object_exprt():exprt(ID_dynamic_object) + dynamic_object_exprt():binary_exprt(ID_dynamic_object) { - operands().resize(2); op0().id(ID_unknown); op1().id(ID_unknown); } explicit dynamic_object_exprt(const typet &type): - exprt(ID_dynamic_object, type) + binary_exprt(ID_dynamic_object, type) { - operands().resize(2); op0().id(ID_unknown); op1().id(ID_unknown); } @@ -1955,6 +1948,7 @@ template<> inline bool can_cast_expr(const exprt &base) { return base.id()==ID_dynamic_object; } + inline void validate_expr(const dynamic_object_exprt &value) { validate_operands(value, 2, "Dynamic object must have two operands"); @@ -1963,18 +1957,16 @@ inline void validate_expr(const dynamic_object_exprt &value) /*! \brief semantic type conversion */ -class typecast_exprt:public exprt +class typecast_exprt:public unary_exprt { public: - explicit typecast_exprt(const typet &_type):exprt(ID_typecast, _type) + explicit typecast_exprt(const typet &_type):unary_exprt(ID_typecast, _type) { - operands().resize(1); } typecast_exprt(const exprt &op, const typet &_type): - exprt(ID_typecast, _type) + unary_exprt(ID_typecast, op, _type) { - copy_to_operands(op); } exprt &op() @@ -3031,17 +3023,17 @@ inline void validate_expr(const address_of_exprt &value) /*! \brief Boolean negation */ -class not_exprt:public exprt +class not_exprt:public unary_exprt { public: - explicit not_exprt(const exprt &op):exprt(ID_not, bool_typet()) + explicit not_exprt(const exprt &op): + unary_exprt(ID_not, op) // type from op.type() { - copy_to_operands(op); + PRECONDITION(op.type().id()==ID_bool); } - not_exprt():exprt(ID_not, bool_typet()) + not_exprt():unary_exprt(ID_not, bool_typet()) { - operands().resize(1); } exprt &op() @@ -3086,6 +3078,7 @@ template<> inline bool can_cast_expr(const exprt &base) { return base.id()==ID_not; } + inline void validate_expr(const not_exprt &value) { validate_operands(value, 1, "Not must have one operand"); @@ -3094,30 +3087,27 @@ inline void validate_expr(const not_exprt &value) /*! \brief Operator to dereference a pointer */ -class dereference_exprt:public exprt +class dereference_exprt:public unary_exprt { public: - explicit dereference_exprt(const typet &type): - exprt(ID_dereference, type) + dereference_exprt():unary_exprt(ID_dereference) { - operands().resize(1); } - explicit dereference_exprt(const exprt &op): - exprt(ID_dereference) + explicit dereference_exprt(const typet &type): + unary_exprt(ID_dereference, type) { - copy_to_operands(op); } - dereference_exprt(const exprt &op, const typet &type): - exprt(ID_dereference, type) + explicit dereference_exprt(const exprt &op): + unary_exprt(ID_dereference, op, op.type().subtype()) { - copy_to_operands(op); + PRECONDITION(op.type().id()==ID_pointer); } - dereference_exprt():exprt(ID_dereference) + dereference_exprt(const exprt &op, const typet &type): + unary_exprt(ID_dereference, op, type) { - operands().resize(1); } exprt &pointer() @@ -3684,39 +3674,33 @@ inline void validate_expr(const array_update_exprt &value) /*! \brief Extract member of struct or union */ -class member_exprt:public exprt +class member_exprt:public unary_exprt { public: - explicit member_exprt(const exprt &op):exprt(ID_member) + // deprecated, and will go away -- use either of the two below + explicit member_exprt(const typet &_type):unary_exprt(ID_member, _type) { - copy_to_operands(op); } - explicit member_exprt(const typet &_type):exprt(ID_member, _type) - { - operands().resize(1); - } - - member_exprt(const exprt &op, const irep_idt &component_name): - exprt(ID_member) + member_exprt( + const exprt &op, + const irep_idt &component_name, + const typet &_type): + unary_exprt(ID_member, op, _type) { - copy_to_operands(op); set_component_name(component_name); } member_exprt( const exprt &op, - const irep_idt &component_name, - const typet &_type): - exprt(ID_member, _type) + const struct_typet::componentt &c): + unary_exprt(ID_member, op, c.type()) { - copy_to_operands(op); - set_component_name(component_name); + set_component_name(c.get_name()); } - member_exprt():exprt(ID_member) + member_exprt():unary_exprt(ID_member) { - operands().resize(1); } irep_idt get_component_name() const @@ -3734,11 +3718,6 @@ class member_exprt:public exprt return get_size_t(ID_component_number); } - void set_component_number(std::size_t component_number) - { - set(ID_component_number, component_number); - } - // will go away, use compound() const exprt &struct_op() const { @@ -3769,6 +3748,7 @@ class member_exprt:public exprt { return static_cast(op).symbol(); } + return to_symbol_expr(op); } }; @@ -4359,18 +4339,18 @@ class null_pointer_exprt:public constant_exprt /*! \brief application of (mathematical) function */ -class function_application_exprt:public exprt +class function_application_exprt:public binary_exprt { public: - function_application_exprt():exprt(ID_function_application) + function_application_exprt():binary_exprt(ID_function_application) { - operands().resize(2); + op0()=symbol_exprt(); } explicit function_application_exprt(const typet &_type): - exprt(ID_function_application, _type) + binary_exprt(ID_function_application, _type) { - operands().resize(2); + op0()=symbol_exprt(); } function_application_exprt( @@ -4380,14 +4360,14 @@ class function_application_exprt:public exprt function()=_function; } - exprt &function() + symbol_exprt &function() { - return op0(); + return static_cast(op0()); } - const exprt &function() const + const symbol_exprt &function() const { - return op0(); + return static_cast(op0()); } typedef exprt::operandst argumentst; @@ -4612,12 +4592,11 @@ inline void validate_expr(const let_exprt &value) /*! \brief A forall expression */ -class forall_exprt:public exprt +class forall_exprt:public binary_exprt { public: - forall_exprt():exprt(ID_forall) + forall_exprt():binary_exprt(ID_forall) { - operands().resize(2); op0()=symbol_exprt(); } @@ -4644,12 +4623,11 @@ class forall_exprt:public exprt /*! \brief An exists expression */ -class exists_exprt:public exprt +class exists_exprt:public binary_exprt { public: - exists_exprt():exprt(ID_exists) + exists_exprt():binary_exprt(ID_exists) { - operands().resize(2); op0()=symbol_exprt(); }