From a4e2c1beb5c0ef4d77e6c6ed888fc2eff8f0a2cc Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 12 Feb 2021 15:40:35 +0000 Subject: [PATCH 1/5] Tests demonstrating pointer-encoding unsoundness The tests exercise the way the back-end encodes pointers. Upcoming encoding changes will ensure that these can soundly be handled. --- regression/cbmc/Pointer_Arithmetic18/main.c | 11 ++++++++++ .../cbmc/Pointer_Arithmetic18/test.desc | 8 +++++++ regression/cbmc/Pointer_comparison1/main.c | 22 +++++++++++++++++++ regression/cbmc/Pointer_comparison1/test.desc | 8 +++++++ 4 files changed, 49 insertions(+) create mode 100644 regression/cbmc/Pointer_Arithmetic18/main.c create mode 100644 regression/cbmc/Pointer_Arithmetic18/test.desc create mode 100644 regression/cbmc/Pointer_comparison1/main.c create mode 100644 regression/cbmc/Pointer_comparison1/test.desc diff --git a/regression/cbmc/Pointer_Arithmetic18/main.c b/regression/cbmc/Pointer_Arithmetic18/main.c new file mode 100644 index 00000000000..90345662392 --- /dev/null +++ b/regression/cbmc/Pointer_Arithmetic18/main.c @@ -0,0 +1,11 @@ +#define MB 0x00100000 +#define BASE (15 * MB) +#define OFFSET (1 * MB) + +main() +{ + char *base = BASE; + int offset = OFFSET; + int n = 2; + __CPROVER_assert(&((char *)base)[offset] != 0, "no wrap-around expected"); +} diff --git a/regression/cbmc/Pointer_Arithmetic18/test.desc b/regression/cbmc/Pointer_Arithmetic18/test.desc new file mode 100644 index 00000000000..94d7221330d --- /dev/null +++ b/regression/cbmc/Pointer_Arithmetic18/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--32 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/cbmc/Pointer_comparison1/main.c b/regression/cbmc/Pointer_comparison1/main.c new file mode 100644 index 00000000000..08022bf75fd --- /dev/null +++ b/regression/cbmc/Pointer_comparison1/main.c @@ -0,0 +1,22 @@ +#include + +int main() +{ + if(sizeof(void *) != 8) + return 0; + + char *p = malloc(1); + if(p == 0) + return 0; + + if( + (unsigned long)p > + 42) // unsoundly evaluates to true due to pointer encoding + { + return 0; + } + + __CPROVER_assert(0, ""); + + return 0; +} diff --git a/regression/cbmc/Pointer_comparison1/test.desc b/regression/cbmc/Pointer_comparison1/test.desc new file mode 100644 index 00000000000..6b765c70f48 --- /dev/null +++ b/regression/cbmc/Pointer_comparison1/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring From e6d5d493d030364ddd11dcad147fd2cee3197ca9 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 12 Feb 2021 16:44:56 +0000 Subject: [PATCH 2/5] Store pointer encoding configuration in boolbv_widtht Rather than handling the object/offset bit width in multiple places, make boolbv_widtht the only place to provide this information. --- src/solvers/flattening/boolbv_width.cpp | 26 +++++++++++- src/solvers/flattening/boolbv_width.h | 7 +++- src/solvers/flattening/bv_pointers.cpp | 56 ++++++++++++++++++------- src/solvers/flattening/bv_pointers.h | 2 - 4 files changed, 73 insertions(+), 18 deletions(-) diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp index 57c5bc3e3cd..6ef50981798 100644 --- a/src/solvers/flattening/boolbv_width.cpp +++ b/src/solvers/flattening/boolbv_width.cpp @@ -11,8 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include +#include #include boolbv_widtht::boolbv_widtht(const namespacet &_ns):ns(_ns) @@ -23,6 +25,24 @@ boolbv_widtht::~boolbv_widtht() { } +std::size_t boolbv_widtht::get_object_width(const pointer_typet &type) const +{ + return config.bv_encoding.object_bits; +} + +std::size_t boolbv_widtht::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); + PRECONDITION(pointer_width >= object_width); + return pointer_width - object_width; +} + +std::size_t boolbv_widtht::get_address_width(const pointer_typet &type) const +{ + return type.get_width(); +} + const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const { // check cache first @@ -182,7 +202,11 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const CHECK_RETURN(entry.total_width > 0); } else if(type_id==ID_pointer) - entry.total_width = type_checked_cast(type).get_width(); + { + entry.total_width = + get_address_width(type_checked_cast(type)); + DATA_INVARIANT(entry.total_width != 0, "pointer must have width"); + } else if(type_id==ID_struct_tag) entry=get_entry(ns.follow_tag(to_struct_tag_type(type))); else if(type_id==ID_union_tag) diff --git a/src/solvers/flattening/boolbv_width.h b/src/solvers/flattening/boolbv_width.h index d25115b3a83..e29e351b94e 100644 --- a/src/solvers/flattening/boolbv_width.h +++ b/src/solvers/flattening/boolbv_width.h @@ -11,7 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_SOLVERS_FLATTENING_BOOLBV_WIDTH_H #include -#include + +class namespacet; class boolbv_widtht { @@ -33,6 +34,10 @@ class boolbv_widtht const struct_typet &type, const irep_idt &member) const; + std::size_t get_object_width(const pointer_typet &type) const; + std::size_t get_offset_width(const pointer_typet &type) const; + std::size_t get_address_width(const pointer_typet &type) const; + protected: const namespacet &ns; diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index c2becd93654..57dadcf6d04 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -34,6 +33,10 @@ literalt bv_pointerst::convert_rest(const exprt &expr) bvt invalid_bv; encode(pointer_logic.get_invalid_object(), invalid_bv); + const pointer_typet &type = to_pointer_type(operands[0].type()); + const std::size_t object_bits = boolbv_width.get_object_width(type); + const std::size_t offset_bits = boolbv_width.get_offset_width(type); + bvt equal_invalid_bv; equal_invalid_bv.resize(object_bits); @@ -89,10 +92,6 @@ bv_pointerst::bv_pointerst( : boolbvt(_ns, _prop, message_handler, get_array_constraints), pointer_logic(_ns) { - object_bits=config.bv_encoding.object_bits; - std::size_t pointer_width = boolbv_width(pointer_type(empty_typet())); - offset_bits=pointer_width-object_bits; - bits=pointer_width; } bool bv_pointerst::convert_address_of_rec( @@ -121,6 +120,8 @@ bool bv_pointerst::convert_address_of_rec( const exprt &index=index_expr.index(); const typet &array_type = array.type(); + const std::size_t bits = boolbv_width(pointer_type(empty_typet())); + // recursive call if(array_type.id()==ID_pointer) { @@ -155,6 +156,7 @@ bool bv_pointerst::convert_address_of_rec( if(convert_address_of_rec(byte_extract_expr.op(), bv)) return true; + const std::size_t bits = boolbv_width(pointer_type(empty_typet())); CHECK_RETURN(bv.size()==bits); offset_arithmetic(bv, 1, byte_extract_expr.offset()); @@ -223,8 +225,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) { PRECONDITION(expr.type().id() == ID_pointer); - // make sure the config hasn't been changed - PRECONDITION(bits==boolbv_width(expr.type())); + const std::size_t bits = boolbv_width(expr.type()); if(expr.id()==ID_symbol) { @@ -504,7 +505,8 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) expr.id() == ID_pointer_offset && to_unary_expr(expr).op().type().id() == ID_pointer) { - bvt op0 = convert_bv(to_unary_expr(expr).op()); + const exprt &op0 = to_unary_expr(expr).op(); + bvt op0_bv = convert_bv(op0); std::size_t width=boolbv_width(expr.type()); @@ -512,10 +514,10 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) return conversion_failed(expr); // we need to strip off the object part - op0.resize(offset_bits); + op0_bv.resize(boolbv_width.get_offset_width(to_pointer_type(op0.type()))); // we do a sign extension to permit negative offsets - return bv_utils.sign_extension(op0, width); + return bv_utils.sign_extension(op0_bv, width); } else if( expr.id() == ID_object_size && @@ -542,7 +544,8 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) expr.id() == ID_pointer_object && to_unary_expr(expr).op().type().id() == ID_pointer) { - bvt op0 = convert_bv(to_unary_expr(expr).op()); + const exprt &op0 = to_unary_expr(expr).op(); + bvt op0_bv = convert_bv(op0); std::size_t width=boolbv_width(expr.type()); @@ -551,9 +554,12 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) // erase offset bits - op0.erase(op0.begin()+0, op0.begin()+offset_bits); + op0_bv.erase( + op0_bv.begin() + 0, + op0_bv.begin() + + boolbv_width.get_offset_width(to_pointer_type(op0.type()))); - return bv_utils.zero_extension(op0, width); + return bv_utils.zero_extension(op0_bv, width); } else if( expr.id() == ID_typecast && @@ -586,6 +592,9 @@ exprt bv_pointerst::bv_get_rec( std::string value_addr, value_offset, value; + const std::size_t bits = boolbv_width(to_pointer_type(type)); + const std::size_t offset_bits = + boolbv_width.get_offset_width(to_pointer_type(type)); for(std::size_t i=0; i Date: Wed, 9 Aug 2017 18:34:29 +0100 Subject: [PATCH 3/5] Lower byte_{extract,update} when pointers are involved This is in preparation of the flattened bit width of pointers not necessarily matching the width claimed by the front-end. --- src/solvers/flattening/boolbv_byte_extract.cpp | 8 ++++++-- src/solvers/flattening/boolbv_byte_update.cpp | 7 +++++-- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index 9b78b79ecbd..cce55d6572a 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -38,8 +38,12 @@ bvt map_bv(const bv_endianness_mapt &map, const bvt &src) bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) { // array logic does not handle byte operators, thus lower when operating on - // unbounded arrays - if(is_unbounded_array(expr.op().type())) + // unbounded arrays; similarly, byte extracts over pointers are not to be + // handled here + if( + is_unbounded_array(expr.op().type()) || + has_subtype(expr.type(), ID_pointer, ns) || + has_subtype(expr.op().type(), ID_pointer, ns)) { return convert_bv(lower_byte_extract(expr, ns)); } diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp index 2210fc48cb7..3ee84ad4ca8 100644 --- a/src/solvers/flattening/boolbv_byte_update.cpp +++ b/src/solvers/flattening/boolbv_byte_update.cpp @@ -20,10 +20,13 @@ Author: Daniel Kroening, kroening@kroening.com bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) { // if we update (from) an unbounded array, lower the expression as the array - // logic does not handle byte operators + // logic does not handle byte operators; similarly, data types that contain + // pointers must not be handled here if( is_unbounded_array(expr.op().type()) || - is_unbounded_array(expr.value().type())) + is_unbounded_array(expr.value().type()) || + has_subtype(expr.value().type(), ID_pointer, ns) || + has_subtype(expr.op0().type(), ID_pointer, ns)) { return convert_bv(lower_byte_update(expr, ns)); } From 726a92f8abb16dd8e8d178b5517217b4bfc9c364 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 12 Feb 2021 16:45:12 +0000 Subject: [PATCH 4/5] Store null-pointer-is-zero in pointer_logict This keeps configurable aspects out of bv_pointerst. --- src/solvers/flattening/pointer_logic.cpp | 3 +++ src/solvers/flattening/pointer_logic.h | 6 ++++++ 2 files changed, 9 insertions(+) diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp index f96921d3a48..ba37c9b5403 100644 --- a/src/solvers/flattening/pointer_logic.cpp +++ b/src/solvers/flattening/pointer_logic.cpp @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -159,6 +160,8 @@ pointer_logict::pointer_logict(const namespacet &_ns):ns(_ns) // add INVALID invalid_object=objects.number(exprt("INVALID")); + + null_is_zero_address = config.ansi_c.NULL_is_zero; } pointer_logict::~pointer_logict() diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h index 8736c4ae28c..a572f71437e 100644 --- a/src/solvers/flattening/pointer_logic.h +++ b/src/solvers/flattening/pointer_logic.h @@ -70,9 +70,15 @@ class pointer_logict void get_dynamic_objects(std::vector &objects) const; + bool get_null_is_zero() const + { + return null_is_zero_address; + } + protected: const namespacet &ns; std::size_t null_object, invalid_object; + bool null_is_zero_address; }; #endif // CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H From bb9c1985f696349aaab7762727b95c53944b03f4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 12 Feb 2021 18:13:25 +0000 Subject: [PATCH 5/5] Encode integer addresses together with pointer object/offset Instead of encoding pointers with the same bit width a pointer on a given platform has, just widen the bit-blasted encoding to include both the previous object/offset encoding as well as an (integer) address. The encoding is thus also trivially extended to handle larger numbers of objects and offsets of the same width as the address. Furthermore clean up the code to encapsulate encoding properly, and make in-code layout of pointer encoding more natural (it's now object, offset, integer-address). Fixes: #436 Fixes: #311 Fixes: #94 --- .../cbmc/Pointer_Arithmetic12/test.desc | 4 +- .../cbmc/Pointer_Arithmetic13/test.desc | 2 +- .../cbmc/Pointer_Arithmetic18/test.desc | 2 +- regression/cbmc/Pointer_comparison1/test.desc | 2 +- .../cbmc/address_space_size_limit1/test.c | 16 - .../cbmc/address_space_size_limit1/test.desc | 7 - .../cbmc/address_space_size_limit3/test.desc | 2 +- src/solvers/flattening/boolbv_width.cpp | 10 +- src/solvers/flattening/bv_pointers.cpp | 514 ++++++++++++++---- src/solvers/flattening/bv_pointers.h | 32 +- src/solvers/smt2/smt2_conv.cpp | 103 ++-- 11 files changed, 512 insertions(+), 182 deletions(-) delete mode 100644 regression/cbmc/address_space_size_limit1/test.c delete mode 100644 regression/cbmc/address_space_size_limit1/test.desc diff --git a/regression/cbmc/Pointer_Arithmetic12/test.desc b/regression/cbmc/Pointer_Arithmetic12/test.desc index b3a154d150b..369ec919c3d 100644 --- a/regression/cbmc/Pointer_Arithmetic12/test.desc +++ b/regression/cbmc/Pointer_Arithmetic12/test.desc @@ -1,4 +1,4 @@ -CORE +THOROUGH main.i --32 --little-endian ^EXIT=0$ @@ -6,3 +6,5 @@ main.i ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring +-- +Takes around 2 minutes to run. diff --git a/regression/cbmc/Pointer_Arithmetic13/test.desc b/regression/cbmc/Pointer_Arithmetic13/test.desc index 52168c7eba4..9efefbc7362 100644 --- a/regression/cbmc/Pointer_Arithmetic13/test.desc +++ b/regression/cbmc/Pointer_Arithmetic13/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^EXIT=0$ diff --git a/regression/cbmc/Pointer_Arithmetic18/test.desc b/regression/cbmc/Pointer_Arithmetic18/test.desc index 94d7221330d..0098f266ed3 100644 --- a/regression/cbmc/Pointer_Arithmetic18/test.desc +++ b/regression/cbmc/Pointer_Arithmetic18/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --32 ^EXIT=0$ diff --git a/regression/cbmc/Pointer_comparison1/test.desc b/regression/cbmc/Pointer_comparison1/test.desc index 6b765c70f48..6de79559914 100644 --- a/regression/cbmc/Pointer_comparison1/test.desc +++ b/regression/cbmc/Pointer_comparison1/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c ^EXIT=10$ diff --git a/regression/cbmc/address_space_size_limit1/test.c b/regression/cbmc/address_space_size_limit1/test.c deleted file mode 100644 index a4f9e047262..00000000000 --- a/regression/cbmc/address_space_size_limit1/test.c +++ /dev/null @@ -1,16 +0,0 @@ - -#include -#include - -int main(int argc, char** argv) -{ - - int i; - char* c; - for(i=0; i<300; ++i) - { - c=(char*)malloc(1); - assert(c!=(char*)0); - } - -} diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc deleted file mode 100644 index 3bc849b0cbf..00000000000 --- a/regression/cbmc/address_space_size_limit1/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE thorough-paths broken-smt-backend -test.c ---no-simplify --unwind 300 --object-bits 8 -too many addressed objects -^EXIT=6$ -^SIGNAL=0$ --- diff --git a/regression/cbmc/address_space_size_limit3/test.desc b/regression/cbmc/address_space_size_limit3/test.desc index ac8f72553aa..32244336607 100644 --- a/regression/cbmc/address_space_size_limit3/test.desc +++ b/regression/cbmc/address_space_size_limit3/test.desc @@ -1,4 +1,4 @@ -CORE +THOROUGH main.i --32 --little-endian --object-bits 25 --pointer-check ^EXIT=10$ diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp index 6ef50981798..991b45da0ed 100644 --- a/src/solvers/flattening/boolbv_width.cpp +++ b/src/solvers/flattening/boolbv_width.cpp @@ -27,15 +27,12 @@ boolbv_widtht::~boolbv_widtht() std::size_t boolbv_widtht::get_object_width(const pointer_typet &type) const { - return config.bv_encoding.object_bits; + return type.get_width(); } std::size_t boolbv_widtht::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); - PRECONDITION(pointer_width >= object_width); - return pointer_width - object_width; + return type.get_width(); } std::size_t boolbv_widtht::get_address_width(const pointer_typet &type) const @@ -203,8 +200,9 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const } else if(type_id==ID_pointer) { + const pointer_typet &t = type_checked_cast(type); entry.total_width = - get_address_width(type_checked_cast(type)); + get_address_width(t) + get_object_width(t) + get_offset_width(t); DATA_INVARIANT(entry.total_width != 0, "pointer must have width"); } else if(type_id==ID_struct_tag) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 57dadcf6d04..f2ba6558035 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -73,8 +73,11 @@ literalt bv_pointerst::convert_rest(const exprt &expr) operands[0].type().id()==ID_pointer && operands[1].type().id()==ID_pointer) { - const bvt &bv0=convert_bv(operands[0]); - const bvt &bv1=convert_bv(operands[1]); + // comparison over integers + bvt bv0 = convert_bv(operands[0]); + address_bv(bv0, to_pointer_type(operands[0].type())); + bvt bv1 = convert_bv(operands[1]); + address_bv(bv1, to_pointer_type(operands[1].type())); return bv_utils.rel( bv0, expr.id(), bv1, bv_utilst::representationt::UNSIGNED); @@ -90,8 +93,38 @@ bv_pointerst::bv_pointerst( message_handlert &message_handler, bool get_array_constraints) : boolbvt(_ns, _prop, message_handler, get_array_constraints), - pointer_logic(_ns) + pointer_logic(_ns), + need_address_bounds(false) { + const pointer_typet type = pointer_type(empty_typet()); + + // the address of NULL is zero unless the platform uses a different + // configuration, in which case we use a non-deterministic integer + // value + bvt &null_pointer = pointer_bits[pointer_logic.get_null_object()]; + null_pointer.resize( + boolbv_width.get_address_width(type), const_literal(false)); + if(!pointer_logic.get_null_is_zero()) + { + for(auto &literal : null_pointer) + literal = prop.new_variable(); + } + + // use the maximum integer as the address of an invalid object, + // unless NULL is not zero on this platform (and might thus be this + // maximum integer), in which case we use a non-deterministic + // integer value + bvt &invalid_object = pointer_bits[pointer_logic.get_invalid_object()]; + invalid_object.resize( + boolbv_width.get_address_width(type), const_literal(true)); + if(!pointer_logic.get_null_is_zero()) + { + for(auto &literal : invalid_object) + literal = prop.new_variable(); + + // NULL and INVALID are distinct + prop.l_set_to_false(bv_utils.equal(null_pointer, invalid_object)); + } } bool bv_pointerst::convert_address_of_rec( @@ -126,7 +159,7 @@ bool bv_pointerst::convert_address_of_rec( if(array_type.id()==ID_pointer) { // this should be gone - bv=convert_pointer_type(array); + bv = convert_bv(array); CHECK_RETURN(bv.size()==bits); } else if(array_type.id()==ID_array || @@ -258,11 +291,55 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag) { // Cast from a bitvector type to pointer. - // We just do a zero extension. - const bvt &op_bv=convert_bv(op); + // Fixed integer address is NULL object plus given offset. + if(op.id() == ID_constant) + { + bvt bv; + + encode(pointer_logic.get_null_object(), bv); + offset_arithmetic(bv, 1, op); + + return bv; + } + + // For all other cases we postpone until we know the full set of objects. + std::size_t width = + boolbv_width.get_offset_width(to_pointer_type(expr.type())) + + boolbv_width.get_object_width(to_pointer_type(expr.type())); - return bv_utils.zero_extension(op_bv, bits); + bvt bv; + bv.resize(width); + + for(std::size_t i = 0; i < width; i++) + bv[i] = prop.new_variable(); + + bvt op_bv = convert_bv(op); + bv_utilst::representationt rep = op_type.id() == ID_signedbv + ? bv_utilst::representationt::SIGNED + : bv_utilst::representationt::UNSIGNED; + + DATA_INVARIANT( + op_bv.size() <= + boolbv_width.get_address_width(to_pointer_type(expr.type())), + "integer cast to pointer of smaller size"); + op_bv = bv_utils.extension( + op_bv, + boolbv_width.get_address_width(to_pointer_type(expr.type())), + rep); + + bv.insert(bv.end(), op_bv.begin(), op_bv.end()); + + postponed_list.push_back(postponedt()); + postponed_list.back().op = op_bv; + postponed_list.back().bv = bv; + postponed_list.back().expr = expr; + + DATA_INVARIANT( + postponed_list.back().bv.size() == bits, + "pointer encoding does not have matching width"); + + return postponed_list.back().bv; } } else if(expr.id()==ID_if) @@ -305,7 +382,18 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) else { mp_integer i = bvrep2integer(value, bits, false); - bv=bv_utils.build_constant(i, bits); + bvt bv_offset = bv_utils.build_constant( + i, boolbv_width.get_offset_width(to_pointer_type(expr.type()))); + bvt bv_addr = bv_utils.build_constant( + i, boolbv_width.get_address_width(to_pointer_type(expr.type()))); + + encode(pointer_logic.get_invalid_object(), bv); + object_bv(bv, to_pointer_type(expr.type())); + bv.insert(bv.end(), bv_offset.begin(), bv_offset.end()); + bv.insert(bv.end(), bv_addr.begin(), bv_addr.end()); + + DATA_INVARIANT( + bv.size() == bits, "pointer encoding does not have matching width"); } return bv; @@ -350,12 +438,15 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) count == 1, "there should be exactly one pointer-type operand in a pointer-type sum"); - bvt sum=bv_utils.build_constant(0, bits); - - forall_operands(it, plus_expr) + exprt sum = plus_expr; + for(exprt::operandst::iterator it = sum.operands().begin(); + it != sum.operands().end();) // no ++it { if(it->type().id()==ID_pointer) + { + it = sum.operands().erase(it); continue; + } if(it->type().id()!=ID_unsignedbv && it->type().id()!=ID_signedbv) @@ -365,21 +456,14 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) return failed_bv; } - bv_utilst::representationt rep= - it->type().id()==ID_signedbv?bv_utilst::representationt::SIGNED: - bv_utilst::representationt::UNSIGNED; - - bvt op=convert_bv(*it); - CHECK_RETURN(!op.empty()); - - // we cut any extra bits off - - if(op.size()>bits) - op.resize(bits); - else if(op.size()type(); + ++it; + } + CHECK_RETURN(!sum.operands().empty()); + if(sum.operands().size() == 1) + { + exprt tmp = sum.operands().front(); + sum.swap(tmp); } offset_arithmetic(bv, size, sum); @@ -465,6 +549,10 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) bvt lhs = convert_bv(minus_expr.lhs()); bvt rhs = convert_bv(minus_expr.rhs()); + // this is address arithmetic, but does consider the type + address_bv(lhs, to_pointer_type(minus_expr.lhs().type())); + address_bv(rhs, to_pointer_type(minus_expr.rhs().type())); + std::size_t width=boolbv_width(expr.type()); if(width==0) @@ -514,7 +602,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) return conversion_failed(expr); // we need to strip off the object part - op0_bv.resize(boolbv_width.get_offset_width(to_pointer_type(op0.type()))); + offset_bv(op0_bv, to_pointer_type(op0.type())); // we do a sign extension to permit negative offsets return bv_utils.sign_extension(op0_bv, width); @@ -552,12 +640,8 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) if(width==0) return conversion_failed(expr); - // erase offset bits - - op0_bv.erase( - op0_bv.begin() + 0, - op0_bv.begin() + - boolbv_width.get_offset_width(to_pointer_type(op0.type()))); + // erase offset and integer bits + object_bv(op0_bv, to_pointer_type(op0.type())); return bv_utils.zero_extension(op0_bv, width); } @@ -566,15 +650,18 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) to_typecast_expr(expr).op().type().id() == ID_pointer) { // pointer to int - bvt op0 = convert_pointer_type(to_typecast_expr(expr).op()); + bvt op0 = convert_bv(to_typecast_expr(expr).op()); - // squeeze it in! + // erase offset and object bits + address_bv(op0, to_pointer_type(to_typecast_expr(expr).op().type())); std::size_t width=boolbv_width(expr.type()); if(width==0) return conversion_failed(expr); + need_address_bounds = true; + return bv_utils.zero_extension(op0, width); } @@ -590,12 +677,15 @@ exprt bv_pointerst::bv_get_rec( if(type.id()!=ID_pointer) return SUB::bv_get_rec(expr, bv, offset, type); - std::string value_addr, value_offset, value; + std::string value, value_offset, value_obj; - const std::size_t bits = boolbv_width(to_pointer_type(type)); + const std::size_t object_bits = + boolbv_width.get_object_width(to_pointer_type(type)); const std::size_t offset_bits = boolbv_width.get_offset_width(to_pointer_type(type)); - for(std::size_t i=0; i(binary2integer(value_addr, false)); + numeric_cast_v(binary2integer(value_obj, false)); pointer.offset=binary2integer(value_offset, true); // we add the elaborated expression as operand @@ -643,33 +733,66 @@ void bv_pointerst::encode(std::size_t addr, bvt &bv) const pointer_typet type = pointer_type(empty_typet()); const std::size_t offset_bits = boolbv_width.get_offset_width(type); const std::size_t object_bits = boolbv_width.get_object_width(type); + const std::size_t address_bits = boolbv_width.get_object_width(type); + const std::size_t bits = offset_bits + object_bits + address_bits; + PRECONDITION(boolbv_width(type) == bits); - bv.resize(boolbv_width(type)); - - // set offset to zero - for(std::size_t i=0; isecond.reserve(address_bits); + for(unsigned i = 0; i < address_bits; ++i) + entry.first->second.push_back(prop.new_variable()); + } + + bv.insert(bv.end(), entry.first->second.begin(), entry.first->second.end()); + + DATA_INVARIANT( + bv.size() == bits, "pointer encoding does not have matching width"); } void bv_pointerst::offset_arithmetic(bvt &bv, const mp_integer &x) { const pointer_typet type = pointer_type(empty_typet()); const std::size_t offset_bits = boolbv_width.get_offset_width(type); + const std::size_t object_bits = boolbv_width.get_object_width(type); + const std::size_t address_bits = boolbv_width.get_object_width(type); + // add to offset_bits bvt bv1=bv; - bv1.resize(offset_bits); // strip down + offset_bv(bv1, type); bvt bv2=bv_utils.build_constant(x, offset_bits); bvt tmp=bv_utils.add(bv1, bv2); - // copy offset bits + // update offset bits for(std::size_t i=0; isecond.reserve(address_bits); + for(unsigned i = 0; i < address_bits; ++i) + entry.first->second.push_back(prop.new_variable()); + } + encode(a, bv); } -void bv_pointerst::do_postponed( - const postponedt &postponed) +void bv_pointerst::do_postponed_non_typecast(const postponedt &postponed) { if(postponed.expr.id() == ID_is_dynamic_object) { - const std::size_t offset_bits = boolbv_width.get_offset_width( - to_pointer_type(to_unary_expr(postponed.expr).op().type())); - + const auto &type = + to_pointer_type(to_unary_expr(postponed.expr).op().type()); const auto &objects = pointer_logic.objects; std::size_t number=0; @@ -754,11 +891,10 @@ void bv_pointerst::do_postponed( // only compare object part bvt bv; encode(number, bv); - - bv.erase(bv.begin(), bv.begin()+offset_bits); + object_bv(bv, type); bvt saved_bv=postponed.op; - saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits); + object_bv(saved_bv, type); POSTCONDITION(bv.size()==saved_bv.size()); PRECONDITION(postponed.bv.size()==1); @@ -774,9 +910,8 @@ void bv_pointerst::do_postponed( } else if(postponed.expr.id()==ID_object_size) { - const std::size_t offset_bits = boolbv_width.get_offset_width( - to_pointer_type(to_unary_expr(postponed.expr).op().type())); - + const auto &type = + to_pointer_type(to_unary_expr(postponed.expr).op().type()); const auto &objects = pointer_logic.objects; std::size_t number=0; @@ -798,11 +933,10 @@ void bv_pointerst::do_postponed( // only compare object part bvt bv; encode(number, bv); - - bv.erase(bv.begin(), bv.begin()+offset_bits); + object_bv(bv, type); bvt saved_bv=postponed.op; - saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits); + object_bv(saved_bv, type); bvt size_bv = convert_bv(object_size); @@ -811,15 +945,195 @@ void bv_pointerst::do_postponed( PRECONDITION(size_bv.size() == postponed.bv.size()); literalt l1=bv_utils.equal(bv, saved_bv); + literalt l2=bv_utils.equal(postponed.bv, size_bv); prop.l_set_to_true(prop.limplies(l1, l2)); } } + else if(postponed.expr.id() == ID_typecast) + { + // defer until phase 2 as the other postponed expressions may + // yield additional entries in pointer_bits + need_address_bounds = true; + } else UNREACHABLE; } +void bv_pointerst::encode_object_bounds(bounds_mapt &dest) +{ + const auto &objects = pointer_logic.objects; + std::size_t number = 0; + + const bvt null_pointer = pointer_bits.at(pointer_logic.get_null_object()); + const bvt &invalid_object = + pointer_bits.at(pointer_logic.get_invalid_object()); + + bvt conj; + conj.reserve(objects.size()); + + for(const exprt &expr : objects) + { + const auto size_expr = size_of_expr(expr.type(), ns); + + if(!size_expr.has_value()) + { + ++number; + continue; + } + + bvt size_bv = convert_bv(*size_expr); + + // NULL, INVALID have no size + DATA_INVARIANT( + number != pointer_logic.get_null_object(), + "NULL object cannot have a size"); + DATA_INVARIANT( + number != pointer_logic.get_invalid_object(), + "INVALID object cannot have a size"); + + bvt object_bv; + encode(number, object_bv); + + // prepare comparison over integers + bvt bv = object_bv; + address_bv(bv, pointer_type(expr.type())); + DATA_INVARIANT( + bv.size() == null_pointer.size(), + "NULL pointer encoding does not have matching width"); + DATA_INVARIANT( + bv.size() == invalid_object.size(), + "INVALID pointer encoding does not have matching width"); + DATA_INVARIANT( + size_bv.size() == bv.size(), + "pointer encoding does not have matching width"); + + // NULL, INVALID must not be within object bounds + literalt null_lower_bound = bv_utils.rel( + null_pointer, ID_lt, bv, bv_utilst::representationt::UNSIGNED); + + literalt inv_obj_lower_bound = bv_utils.rel( + invalid_object, ID_lt, bv, bv_utilst::representationt::UNSIGNED); + + // compute the upper bound with the side effect of enforcing the + // object addresses not to wrap around/overflow + bvt obj_upper_bound = bv_utils.add_sub_no_overflow( + bv, size_bv, false, bv_utilst::representationt::UNSIGNED); + + literalt null_upper_bound = bv_utils.rel( + null_pointer, + ID_ge, + obj_upper_bound, + bv_utilst::representationt::UNSIGNED); + + literalt inv_obj_upper_bound = bv_utils.rel( + invalid_object, + ID_ge, + obj_upper_bound, + bv_utilst::representationt::UNSIGNED); + + // store bounds for re-use + dest.insert({number, {bv, obj_upper_bound}}); + + conj.push_back(prop.lor(null_lower_bound, null_upper_bound)); + conj.push_back(prop.lor(inv_obj_lower_bound, inv_obj_upper_bound)); + + ++number; + } + + if(!conj.empty()) + prop.l_set_to_true(prop.land(conj)); +} + +void bv_pointerst::do_postponed_typecast( + const postponedt &postponed, + const bounds_mapt &bounds) +{ + if(postponed.expr.id() != ID_typecast) + return; + + const pointer_typet &type = to_pointer_type(postponed.expr.type()); + const std::size_t bits = boolbv_width.get_offset_width(type) + + boolbv_width.get_object_width(type) + + boolbv_width.get_address_width(type); + + // given an integer (possibly representing an address) postponed.op, + // compute the object and offset that it may refer to + bvt saved_bv = postponed.op; + + bvt conj, oob_conj; + conj.reserve(bounds.size() + 3); + oob_conj.reserve(bounds.size()); + + for(const auto &bounds_entry : bounds) + { + std::size_t number = bounds_entry.first; + + // pointer must be within object bounds + const bvt &lb = bounds_entry.second.first; + const bvt &ub = bounds_entry.second.second; + + literalt lower_bound = + bv_utils.rel(saved_bv, ID_ge, lb, bv_utilst::representationt::UNSIGNED); + + literalt upper_bound = + bv_utils.rel(saved_bv, ID_lt, ub, bv_utilst::representationt::UNSIGNED); + + // compute the offset within the object, and the corresponding + // pointer bv + bvt offset = bv_utils.sub(saved_bv, lb); + + bvt bv; + encode(number, bv); + object_bv(bv, type); + DATA_INVARIANT( + offset.size() == boolbv_width.get_offset_width(type), + "pointer encoding does not have matching width"); + bv.insert(bv.end(), offset.begin(), offset.end()); + bv.insert(bv.end(), saved_bv.begin(), saved_bv.end()); + DATA_INVARIANT( + bv.size() == bits, "pointer encoding does not have matching width"); + + // if the integer address is within the object bounds, return an + // adjusted offset + literalt in_bounds = prop.land(lower_bound, upper_bound); + conj.push_back(prop.limplies(in_bounds, bv_utils.equal(bv, postponed.bv))); + oob_conj.push_back(!in_bounds); + } + + // append integer address as both offset and address + bvt invalid_bv, null_bv; + encode(pointer_logic.get_invalid_object(), invalid_bv); + object_bv(invalid_bv, type); + invalid_bv.insert(invalid_bv.end(), saved_bv.begin(), saved_bv.end()); + invalid_bv.insert(invalid_bv.end(), saved_bv.begin(), saved_bv.end()); + encode(pointer_logic.get_null_object(), null_bv); + object_bv(null_bv, type); + null_bv.insert(null_bv.end(), saved_bv.begin(), saved_bv.end()); + null_bv.insert(null_bv.end(), saved_bv.begin(), saved_bv.end()); + + // NULL is always NULL + conj.push_back(prop.limplies( + bv_utils.equal(saved_bv, pointer_bits.at(pointer_logic.get_null_object())), + bv_utils.equal(null_bv, postponed.bv))); + + // INVALID is always INVALID + conj.push_back(prop.limplies( + bv_utils.equal( + saved_bv, pointer_bits.at(pointer_logic.get_invalid_object())), + bv_utils.equal(invalid_bv, postponed.bv))); + + // one of the objects or NULL or INVALID with an offset + conj.push_back(prop.limplies( + prop.land(oob_conj), + prop.lor( + bv_utils.equal(null_bv, postponed.bv), + bv_utils.equal(invalid_bv, postponed.bv)))); + + prop.l_set_to_true(prop.land(conj)); +} + void bv_pointerst::post_process() { // post-processing arrays may yield further objects, do this first @@ -829,7 +1143,19 @@ void bv_pointerst::post_process() it=postponed_list.begin(); it!=postponed_list.end(); it++) - do_postponed(*it); + do_postponed_non_typecast(*it); + + if(need_address_bounds) + { + // make sure NULL and INVALID are unique addresses + bounds_mapt bounds; + encode_object_bounds(bounds); + + for(postponed_listt::const_iterator it = postponed_list.begin(); + it != postponed_list.end(); + it++) + do_postponed_typecast(*it, bounds); + } // Clear the list to avoid re-doing in case of incremental usage. postponed_list.clear(); diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h index d50a6f6b7ef..509770823a7 100644 --- a/src/solvers/flattening/bv_pointers.h +++ b/src/solvers/flattening/bv_pointers.h @@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H #define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H - #include "boolbv.h" #include "pointer_logic.h" @@ -31,6 +30,10 @@ class bv_pointerst:public boolbvt // NOLINTNEXTLINE(readability/identifiers) typedef boolbvt SUB; + typedef std::map pointer_bitst; + pointer_bitst pointer_bits; + bool need_address_bounds; + void encode(std::size_t object, bvt &bv); virtual bvt convert_pointer_type(const exprt &expr); @@ -53,8 +56,6 @@ class bv_pointerst:public boolbvt void offset_arithmetic(bvt &bv, const mp_integer &x); void offset_arithmetic(bvt &bv, const mp_integer &factor, const exprt &index); - void offset_arithmetic( - bvt &bv, const mp_integer &factor, const bvt &index_bv); struct postponedt { @@ -65,7 +66,30 @@ class bv_pointerst:public boolbvt typedef std::list postponed_listt; postponed_listt postponed_list; - void do_postponed(const postponedt &postponed); + void do_postponed_non_typecast(const postponedt &postponed); + typedef std::map> bounds_mapt; + void encode_object_bounds(bounds_mapt &dest); + void + do_postponed_typecast(const postponedt &postponed, const bounds_mapt &bounds); + + void object_bv(bvt &bv, const pointer_typet &type) const + { + bv.resize(boolbv_width.get_object_width(type)); + } + + void offset_bv(bvt &bv, const pointer_typet &type) const + { + bv.erase(bv.begin(), bv.begin() + boolbv_width.get_object_width(type)); + bv.resize(boolbv_width.get_offset_width(type)); + } + + void address_bv(bvt &bv, const pointer_typet &type) const + { + bv.erase( + bv.begin(), + bv.begin() + boolbv_width.get_object_width(type) + + boolbv_width.get_offset_width(type)); + } }; #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index c4c562226f0..196c22f10c0 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -210,10 +210,9 @@ void smt2_convt::define_object_size( PRECONDITION(expr.id() == ID_object_size); const exprt &ptr = to_unary_expr(expr).op(); std::size_t size_width = boolbv_width(expr.type()); - std::size_t pointer_width = boolbv_width(ptr.type()); std::size_t number = 0; - std::size_t h=pointer_width-1; - std::size_t l=pointer_width-config.bv_encoding.object_bits; + std::size_t object_bits = + boolbv_width.get_object_width(to_pointer_type(ptr.type())); for(const auto &o : pointer_logic.objects) { @@ -230,12 +229,12 @@ void smt2_convt::define_object_size( continue; } - out << "(assert (implies (= " << - "((_ extract " << h << " " << l << ") "; + out << "(assert (implies (= " + << "((_ extract " << object_bits - 1 << " 0) "; convert_expr(ptr); - out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))" - << "(= " << id << " (_ bv" << *object_size << " " << size_width - << "))))\n"; + out << ") (_ bv" << number << " " << object_bits << "))" + << "(= " << id << " (_ bv" << object_size->to_ulong() << " " + << size_width << "))))\n"; ++number; } @@ -568,10 +567,14 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type) mp_integer v = numeric_cast_v(bv_expr); // split into object and offset - mp_integer pow=power(2, width-config.bv_encoding.object_bits); + std::size_t object_bits = + boolbv_width.get_object_width(to_pointer_type(type)); + std::size_t offset_bits = + boolbv_width.get_offset_width(to_pointer_type(type)); + mp_integer pow = power(2, object_bits); pointer_logict::pointert ptr; - ptr.object = numeric_cast_v(v / pow); - ptr.offset=v%pow; + ptr.object = numeric_cast_v(v % pow); + ptr.offset = (v % power(2, object_bits + offset_bits)) / pow; return pointer_logic.pointer_expr(ptr, to_pointer_type(type)); } else if(type.id()==ID_struct) @@ -614,12 +617,18 @@ void smt2_convt::convert_address_of_rec( expr.id()==ID_string_constant || expr.id()==ID_label) { - out - << "(concat (_ bv" - << pointer_logic.add_object(expr) << " " - << config.bv_encoding.object_bits << ")" - << " (_ bv0 " - << boolbv_width(result_type)-config.bv_encoding.object_bits << "))"; + std::string addr = + expr.id() == ID_symbol + ? expr.get_string(ID_identifier) + "$address" + : "(_ bv0 " + + std::to_string(boolbv_width.get_address_width(result_type)) + ")"; + + out << "(concat " + << "(concat " + << "(_ bv" << pointer_logic.add_object(expr) << " " + << boolbv_width.get_object_width(result_type) << ") " + << "(_ bv0 " << boolbv_width.get_offset_width(result_type) << ")) " + << addr << ")"; } else if(expr.id()==ID_index) { @@ -1424,23 +1433,21 @@ void smt2_convt::convert_expr(const exprt &expr) op.type().id() == ID_pointer, "operand of pointer offset expression shall be of pointer type"); + std::size_t object_bits = + boolbv_width.get_object_width(to_pointer_type(op.type())); std::size_t offset_bits = - boolbv_width(op.type()) - config.bv_encoding.object_bits; - std::size_t result_width=boolbv_width(expr.type()); + boolbv_width.get_offset_width(to_pointer_type(op.type())); + std::size_t ext = boolbv_width(expr.type()) - offset_bits; - // max extract width - if(offset_bits>result_width) - offset_bits=result_width; - - // too few bits? - if(result_width>offset_bits) - out << "((_ zero_extend " << result_width-offset_bits << ") "; + if(ext > 0) + out << "((_ zero_extend " << ext << ") "; - out << "((_ extract " << offset_bits-1 << " 0) "; + out << "((_ extract " << object_bits + offset_bits - 1 << " " << object_bits + << ") "; convert_expr(op); out << ")"; - if(result_width>offset_bits) + if(ext > 0) out << ")"; // zero_extend } else if(expr.id()==ID_pointer_object) @@ -1451,15 +1458,14 @@ void smt2_convt::convert_expr(const exprt &expr) op.type().id() == ID_pointer, "pointer object expressions should be of pointer type"); - std::size_t ext=boolbv_width(expr.type())-config.bv_encoding.object_bits; - std::size_t pointer_width = boolbv_width(op.type()); + std::size_t object_bits = + boolbv_width.get_object_width(to_pointer_type(op.type())); + std::size_t ext = boolbv_width(expr.type()) - object_bits; if(ext>0) out << "((_ zero_extend " << ext << ") "; - out << "((_ extract " - << pointer_width-1 << " " - << pointer_width-config.bv_encoding.object_bits << ") "; + out << "((_ extract " << object_bits - 1 << " 0) "; convert_expr(op); out << ")"; @@ -1472,14 +1478,13 @@ void smt2_convt::convert_expr(const exprt &expr) } else if(expr.id() == ID_is_invalid_pointer) { - const auto &op = to_unary_expr(expr).op(); - std::size_t pointer_width = boolbv_width(op.type()); - out << "(= ((_ extract " - << pointer_width-1 << " " - << pointer_width-config.bv_encoding.object_bits << ") "; - convert_expr(op); - out << ") (_ bv" << pointer_logic.get_invalid_object() - << " " << config.bv_encoding.object_bits << "))"; + std::size_t object_bits = boolbv_width.get_object_width( + to_pointer_type(to_unary_expr(expr).op().type())); + + out << "(= ((_ extract " << object_bits - 1 << " 0) "; + convert_expr(to_unary_expr(expr).op()); + out << ") (_ bv" << pointer_logic.get_invalid_object() << " " << object_bits + << "))"; } else if(expr.id()==ID_string_constant) { @@ -2956,30 +2961,28 @@ void smt2_convt::convert_is_dynamic_object(const unary_exprt &expr) std::vector dynamic_objects; pointer_logic.get_dynamic_objects(dynamic_objects); + std::size_t object_bits = + boolbv_width.get_object_width(to_pointer_type(expr.op().type())); + if(dynamic_objects.empty()) out << "false"; else { - std::size_t pointer_width = boolbv_width(expr.op().type()); - - out << "(let ((?obj ((_ extract " - << pointer_width-1 << " " - << pointer_width-config.bv_encoding.object_bits << ") "; + out << "(let ((?obj ((_ extract " << object_bits << " 0) "; convert_expr(expr.op()); out << "))) "; if(dynamic_objects.size()==1) { - out << "(= (_ bv" << dynamic_objects.front() - << " " << config.bv_encoding.object_bits << ") ?obj)"; + out << "(= (_ bv" << dynamic_objects.front() << " " << object_bits + << ") ?obj)"; } else { out << "(or"; for(const auto &object : dynamic_objects) - out << " (= (_ bv" << object - << " " << config.bv_encoding.object_bits << ") ?obj)"; + out << " (= (_ bv" << object << " " << object_bits << ") ?obj)"; out << ")"; // or }