diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index c46a472b438..7517a6d664f 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -68,40 +68,16 @@ void bv_endianness_mapt::build_big_endian(const typet &src) endianness_mapt bv_pointerst::endianness_map(const typet &type, bool little_endian) const { - return bv_endianness_mapt{type, little_endian, ns, bv_pointers_width}; + return bv_endianness_mapt{type, little_endian, ns, bv_width}; } -std::size_t bv_pointerst::bv_pointers_widtht:: -operator()(const typet &type) const -{ - if(type.id() != ID_pointer) - return boolbv_widtht::operator()(type); - - // check or update the cache, just like boolbv_widtht does - std::pair cache_result = - cache.insert(std::pair(type, entryt())); - - if(cache_result.second) - { - std::size_t &total_width = cache_result.first->second.total_width; - - total_width = get_address_width(to_pointer_type(type)); - DATA_INVARIANT(total_width > 0, "pointer width shall be greater than zero"); - } - - return cache_result.first->second.total_width; -} - -std::size_t bv_pointerst::bv_pointers_widtht::get_object_width( - const pointer_typet &type) const +std::size_t bv_pointerst::get_object_width(const pointer_typet &) const { // not actually type-dependent for now - (void)type; return config.bv_encoding.object_bits; } -std::size_t bv_pointerst::bv_pointers_widtht::get_offset_width( - const pointer_typet &type) const +std::size_t bv_pointerst::get_offset_width(const pointer_typet &type) const { const std::size_t pointer_width = type.get_width(); const std::size_t object_width = get_object_width(type); @@ -109,12 +85,41 @@ std::size_t bv_pointerst::bv_pointers_widtht::get_offset_width( return pointer_width - object_width; } -std::size_t bv_pointerst::bv_pointers_widtht::get_address_width( - const pointer_typet &type) const +std::size_t bv_pointerst::get_address_width(const pointer_typet &type) const { return type.get_width(); } +bvt bv_pointerst::object_literals(const bvt &bv, const pointer_typet &type) + const +{ + const std::size_t offset_width = get_offset_width(type); + const std::size_t object_width = get_object_width(type); + PRECONDITION(bv.size() >= offset_width + object_width); + + return bvt( + bv.begin() + offset_width, bv.begin() + offset_width + object_width); +} + +bvt bv_pointerst::offset_literals(const bvt &bv, const pointer_typet &type) + const +{ + const std::size_t offset_width = get_offset_width(type); + PRECONDITION(bv.size() >= offset_width); + + return bvt(bv.begin(), bv.begin() + offset_width); +} + +bvt bv_pointerst::object_offset_encoding(const bvt &object, const bvt &offset) +{ + bvt result; + result.reserve(offset.size() + object.size()); + result.insert(result.end(), offset.begin(), offset.end()); + result.insert(result.end(), object.begin(), object.end()); + + return result; +} + literalt bv_pointerst::convert_rest(const exprt &expr) { PRECONDITION(expr.type().id() == ID_bool); @@ -136,8 +141,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr) bvt invalid_bv = object_literals( encode(pointer_logic.get_invalid_object(), type), type); - const std::size_t object_bits = - bv_pointers_width.get_object_width(type); + const std::size_t object_bits = get_object_width(type); bvt equal_invalid_bv; equal_invalid_bv.reserve(object_bits); @@ -210,8 +214,7 @@ bv_pointerst::bv_pointerst( message_handlert &message_handler, bool get_array_constraints) : boolbvt(_ns, _prop, message_handler, get_array_constraints), - pointer_logic(_ns), - bv_pointers_width(_ns) + pointer_logic(_ns) { } @@ -460,7 +463,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) count == 1, "there should be exactly one pointer-type operand in a pointer-type sum"); - const std::size_t offset_bits = bv_pointers_width.get_offset_width(type); + const std::size_t offset_bits = get_offset_width(type); bvt sum = bv_utils.build_constant(0, offset_bits); forall_operands(it, plus_expr) @@ -815,8 +818,8 @@ exprt bv_pointerst::bv_get_rec( bvt bv_pointerst::encode(std::size_t addr, const pointer_typet &type) const { - const std::size_t offset_bits = bv_pointers_width.get_offset_width(type); - const std::size_t object_bits = bv_pointers_width.get_object_width(type); + const std::size_t offset_bits = get_offset_width(type); + const std::size_t object_bits = get_object_width(type); bvt zero_offset(offset_bits, const_literal(false)); @@ -834,7 +837,7 @@ bvt bv_pointerst::offset_arithmetic( const bvt &bv, const mp_integer &x) { - const std::size_t offset_bits = bv_pointers_width.get_offset_width(type); + const std::size_t offset_bits = get_offset_width(type); return offset_arithmetic( type, bv, 1, bv_utils.build_constant(x, offset_bits)); @@ -852,7 +855,7 @@ bvt bv_pointerst::offset_arithmetic( index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED: bv_utilst::representationt::UNSIGNED; - const std::size_t offset_bits = bv_pointers_width.get_offset_width(type); + const std::size_t offset_bits = get_offset_width(type); bv_index=bv_utils.extension(bv_index, offset_bits, rep); return offset_arithmetic(type, bv, factor, bv_index); @@ -874,7 +877,7 @@ bvt bv_pointerst::offset_arithmetic( bv_index = bv_utils.signed_multiplier(index, bv_factor); } - const std::size_t offset_bits = bv_pointers_width.get_offset_width(type); + const std::size_t offset_bits = get_offset_width(type); bv_index = bv_utils.sign_extension(bv_index, offset_bits); bvt offset_bv = offset_literals(bv, type); @@ -889,7 +892,7 @@ bvt bv_pointerst::add_addr(const exprt &expr) std::size_t a=pointer_logic.add_object(expr); const pointer_typet type = pointer_type(expr.type()); - const std::size_t object_bits = bv_pointers_width.get_object_width(type); + const std::size_t object_bits = get_object_width(type); const std::size_t max_objects=std::size_t(1)< convert_address_of_rec(const exprt &expr); + optionalt convert_address_of_rec(const exprt &); NODISCARD - bvt offset_arithmetic( - const pointer_typet &type, - const bvt &bv, - const mp_integer &x); + bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &); NODISCARD bvt offset_arithmetic( - const pointer_typet &type, - const bvt &bv, + const pointer_typet &, + const bvt &, const mp_integer &factor, const exprt &index); NODISCARD bvt offset_arithmetic( - const pointer_typet &type, - const bvt &bv, + const pointer_typet &, + const bvt &, const mp_integer &factor, const bvt &index_bv); @@ -115,43 +94,21 @@ class bv_pointerst:public boolbvt /// \param bv: Encoded pointer /// \param type: Type of the encoded pointer /// \return Vector of literals identifying the object part of \p bv - bvt object_literals(const bvt &bv, const pointer_typet &type) const - { - const std::size_t offset_width = bv_pointers_width.get_offset_width(type); - const std::size_t object_width = bv_pointers_width.get_object_width(type); - PRECONDITION(bv.size() >= offset_width + object_width); - - return bvt( - bv.begin() + offset_width, bv.begin() + offset_width + object_width); - } + bvt object_literals(const bvt &bv, const pointer_typet &type) const; /// Given a pointer encoded in \p bv, extract the literals representing the /// offset into an object that the pointer points to. /// \param bv: Encoded pointer /// \param type: Type of the encoded pointer /// \return Vector of literals identifying the offset part of \p bv - bvt offset_literals(const bvt &bv, const pointer_typet &type) const - { - const std::size_t offset_width = bv_pointers_width.get_offset_width(type); - PRECONDITION(bv.size() >= offset_width); - - return bvt(bv.begin(), bv.begin() + offset_width); - } + bvt offset_literals(const bvt &bv, const pointer_typet &type) const; /// Construct a pointer encoding from given encodings of \p object and \p /// offset. /// \param object: Encoded object /// \param offset: Encoded offset /// \return Pointer encoding - static bvt object_offset_encoding(const bvt &object, const bvt &offset) - { - bvt result; - result.reserve(offset.size() + object.size()); - result.insert(result.end(), offset.begin(), offset.end()); - result.insert(result.end(), object.begin(), object.end()); - - return result; - } + static bvt object_offset_encoding(const bvt &object, const bvt &offset); }; #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H