From c9172458bbfdca8b89293000624761cf0fcd0736 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 15 Feb 2021 13:55:51 +0000 Subject: [PATCH 1/3] bv_endianness_mapt is specific to bv_pointerst The special-casing of the endianness encoding handled by bv_endianness_mapt is really specific to bv_pointerst, not boolbvt in general. Thus, move this data structure to bv_pointers.cpp and enable overriding the endianness map from boolbvt. This commit is refactoring only, no changes in behaviour intended. --- scripts/expected_doxygen_warnings.txt | 4 +- src/solvers/Makefile | 1 - src/solvers/flattening/boolbv.h | 7 +++ .../flattening/boolbv_byte_extract.cpp | 8 ++- src/solvers/flattening/boolbv_byte_update.cpp | 10 ++-- src/solvers/flattening/boolbv_union.cpp | 6 +-- src/solvers/flattening/boolbv_with.cpp | 6 +-- src/solvers/flattening/bv_endianness_map.cpp | 36 ------------- src/solvers/flattening/bv_endianness_map.h | 40 -------------- src/solvers/flattening/bv_pointers.cpp | 52 +++++++++++++++++++ src/solvers/flattening/bv_pointers.h | 3 ++ 11 files changed, 75 insertions(+), 98 deletions(-) delete mode 100644 src/solvers/flattening/bv_endianness_map.cpp delete mode 100644 src/solvers/flattening/bv_endianness_map.h diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt index a733c2bfa57..314cc2cf55f 100644 --- a/scripts/expected_doxygen_warnings.txt +++ b/scripts/expected_doxygen_warnings.txt @@ -83,8 +83,8 @@ warning: Include graph for 'cbmc_parse_options.cpp' not generated, too many node warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'goto_model.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. -warning: Included by graph for 'c_types.h' not generated, too many nodes (111), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. +warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. warning: Included by graph for 'expr.h' not generated, too many nodes (87), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES. diff --git a/src/solvers/Makefile b/src/solvers/Makefile index ec9ddfceb18..1b70e5960b7 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -130,7 +130,6 @@ SRC = $(BOOLEFORCE_SRC) \ flattening/boolbv_width.cpp \ flattening/boolbv_with.cpp \ flattening/bv_dimacs.cpp \ - flattening/bv_endianness_map.cpp \ flattening/bv_minimize.cpp \ flattening/bv_pointers.cpp \ flattening/bv_utils.cpp \ diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 6fcafa31792..9d9e7303198 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com // #include +#include #include #include #include @@ -92,6 +93,12 @@ class boolbvt:public arrayst return map; } + virtual endianness_mapt + endianness_map(const typet &type, bool little_endian) const + { + return endianness_mapt{type, little_endian, ns}; + } + boolbv_widtht boolbv_width; protected: diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index 9b78b79ecbd..868f393ba3b 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -17,9 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "bv_endianness_map.h" - -bvt map_bv(const bv_endianness_mapt &map, const bvt &src) +bvt map_bv(const endianness_mapt &map, const bvt &src) { PRECONDITION(map.number_of_bits() == src.size()); bvt result; @@ -101,11 +99,11 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) const bool little_endian = expr.id() == ID_byte_extract_little_endian; // first do op0 - const bv_endianness_mapt op_map(op.type(), little_endian, ns, boolbv_width); + const endianness_mapt op_map = endianness_map(op.type(), little_endian); const bvt op_bv=map_bv(op_map, convert_bv(op)); // do result - bv_endianness_mapt result_map(expr.type(), little_endian, ns, boolbv_width); + endianness_mapt result_map = endianness_map(expr.type(), little_endian); bvt bv; bv.resize(width); diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp index 2210fc48cb7..5d97db8dcec 100644 --- a/src/solvers/flattening/boolbv_byte_update.cpp +++ b/src/solvers/flattening/boolbv_byte_update.cpp @@ -15,8 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "bv_endianness_map.h" - bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) { // if we update (from) an unbounded array, lower the expression as the array @@ -67,8 +65,8 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) } else { - bv_endianness_mapt map_op(op.type(), false, ns, boolbv_width); - bv_endianness_mapt map_value(value.type(), false, ns, boolbv_width); + endianness_mapt map_op = endianness_map(op.type(), false); + endianness_mapt map_value = endianness_map(value.type(), false); const std::size_t offset_i = numeric_cast_v(offset); @@ -99,8 +97,8 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) offset_expr, from_integer(offset / byte_width, offset_expr.type())); literalt equal=convert(equality); - bv_endianness_mapt map_op(op.type(), little_endian, ns, boolbv_width); - bv_endianness_mapt map_value(value.type(), little_endian, ns, boolbv_width); + endianness_mapt map_op = endianness_map(op.type(), little_endian); + endianness_mapt map_value = endianness_map(value.type(), little_endian); for(std::size_t bit=0; bit #include -#include "bv_endianness_map.h" - bvt boolbvt::convert_union(const union_exprt &expr) { std::size_t width=boolbv_width(expr.type()); @@ -45,8 +43,8 @@ bvt boolbvt::convert_union(const union_exprt &expr) config.ansi_c.endianness == configt::ansi_ct::endiannesst::IS_BIG_ENDIAN, "endianness should be set to either little endian or big endian"); - bv_endianness_mapt map_u(expr.type(), false, ns, boolbv_width); - bv_endianness_mapt map_op(expr.op().type(), false, ns, boolbv_width); + endianness_mapt map_u = endianness_map(expr.type(), false); + endianness_mapt map_op = endianness_map(expr.op().type(), false); for(std::size_t i=0; i #include -#include "bv_endianness_map.h" - bvt boolbvt::convert_with(const with_exprt &expr) { bvt bv = convert_bv(expr.old()); @@ -248,8 +246,8 @@ void boolbvt::convert_with_union( assert( config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_BIG_ENDIAN); - bv_endianness_mapt map_u(type, false, ns, boolbv_width); - bv_endianness_mapt map_op2(op2.type(), false, ns, boolbv_width); + endianness_mapt map_u = endianness_map(type, false); + endianness_mapt map_op2 = endianness_map(op2.type(), false); for(std::size_t i=0; i -#include - -#include "boolbv_width.h" - -void bv_endianness_mapt::build_little_endian(const typet &src) -{ - const std::size_t width = boolbv_width(src); - - if(width == 0) - return; - - const std::size_t new_size = map.size() + width; - map.reserve(new_size); - - for(std::size_t i = map.size(); i < new_size; ++i) - map.push_back(i); -} - -void bv_endianness_mapt::build_big_endian(const typet &src) -{ - if(src.id() == ID_pointer) - build_little_endian(src); - else - endianness_mapt::build_big_endian(src); -} diff --git a/src/solvers/flattening/bv_endianness_map.h b/src/solvers/flattening/bv_endianness_map.h deleted file mode 100644 index d15f3d463b2..00000000000 --- a/src/solvers/flattening/bv_endianness_map.h +++ /dev/null @@ -1,40 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Michael Tautschnig - -\*******************************************************************/ - -#ifndef CPROVER_SOLVERS_FLATTENING_BV_ENDIANNESS_MAP_H -#define CPROVER_SOLVERS_FLATTENING_BV_ENDIANNESS_MAP_H - -#include - -class boolbv_widtht; - -/// Map bytes according to the configured endianness. The key difference to -/// endianness_mapt is that bv_endianness_mapt is aware of the bit-level -/// encoding of types, which need not co-incide with the bit layout at -/// source-code level. -class bv_endianness_mapt : public endianness_mapt -{ -public: - bv_endianness_mapt( - const typet &type, - bool little_endian, - const namespacet &_ns, - boolbv_widtht &_boolbv_width) - : endianness_mapt(_ns), boolbv_width(_boolbv_width) - { - build(type, little_endian); - } - -protected: - boolbv_widtht &boolbv_width; - - virtual void build_little_endian(const typet &type) override; - virtual void build_big_endian(const typet &type) override; -}; - -#endif // CPROVER_SOLVERS_FLATTENING_BV_ENDIANNESS_MAP_H diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index c2becd93654..77a1592eee1 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -16,6 +16,58 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +/// Map bytes according to the configured endianness. The key difference to +/// endianness_mapt is that bv_endianness_mapt is aware of the bit-level +/// encoding of types, which need not co-incide with the bit layout at +/// source-code level. +class bv_endianness_mapt : public endianness_mapt +{ +public: + bv_endianness_mapt( + const typet &type, + bool little_endian, + const namespacet &_ns, + const boolbv_widtht &_boolbv_width) + : endianness_mapt(_ns), boolbv_width(_boolbv_width) + { + build(type, little_endian); + } + +protected: + const boolbv_widtht &boolbv_width; + + void build_little_endian(const typet &type) override; + void build_big_endian(const typet &type) override; +}; + +void bv_endianness_mapt::build_little_endian(const typet &src) +{ + const std::size_t width = boolbv_width(src); + + if(width == 0) + return; + + const std::size_t new_size = map.size() + width; + map.reserve(new_size); + + for(std::size_t i = map.size(); i < new_size; ++i) + map.push_back(i); +} + +void bv_endianness_mapt::build_big_endian(const typet &src) +{ + if(src.id() == ID_pointer) + build_little_endian(src); + else + endianness_mapt::build_big_endian(src); +} + +endianness_mapt +bv_pointerst::endianness_map(const typet &type, bool little_endian) const +{ + return bv_endianness_mapt{type, little_endian, ns, boolbv_width}; +} + literalt bv_pointerst::convert_rest(const exprt &expr) { PRECONDITION(expr.type().id() == ID_bool); diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h index 0c6c01cfb2f..114237b4d92 100644 --- a/src/solvers/flattening/bv_pointers.h +++ b/src/solvers/flattening/bv_pointers.h @@ -25,6 +25,9 @@ class bv_pointerst:public boolbvt void post_process() override; + endianness_mapt + endianness_map(const typet &type, bool little_endian) const override; + protected: pointer_logict pointer_logic; From d2815459a1daa6b338c9820cfb3345317b6686e8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 15 Feb 2021 15:51:36 +0000 Subject: [PATCH 2/3] Enable overriding of boolbvt::boolbv_width With upcoming changes to pointer encoding it will be necessary to enable children of boolbvt to define their own bit encoding width of data types. This commit is refactoring only, no changes in behaviour intended. --- src/solvers/flattening/boolbv.h | 10 +++++++--- src/solvers/flattening/boolbv_width.cpp | 11 ++++------- src/solvers/flattening/boolbv_width.h | 7 ++++--- src/solvers/flattening/bv_pointers.cpp | 2 +- src/solvers/flattening/bv_pointers.h | 5 +++++ 5 files changed, 21 insertions(+), 14 deletions(-) diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 9d9e7303198..c74c4798ef7 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -47,7 +47,7 @@ class boolbvt:public arrayst bool get_array_constraints = false) : arrayst(_ns, _prop, message_handler, get_array_constraints), unbounded_array(unbounded_arrayt::U_NONE), - boolbv_width(_ns), + bv_width(_ns), bv_utils(_prop), functions(*this), map(_prop) @@ -93,15 +93,19 @@ class boolbvt:public arrayst return map; } + virtual std::size_t boolbv_width(const typet &type) const + { + return bv_width(type); + } + virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const { return endianness_mapt{type, little_endian, ns}; } - boolbv_widtht boolbv_width; - protected: + boolbv_widtht bv_width; bv_utilst bv_utils; // uninterpreted functions diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp index 57c5bc3e3cd..be1848d65ee 100644 --- a/src/solvers/flattening/boolbv_width.cpp +++ b/src/solvers/flattening/boolbv_width.cpp @@ -13,16 +13,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include boolbv_widtht::boolbv_widtht(const namespacet &_ns):ns(_ns) { } -boolbv_widtht::~boolbv_widtht() -{ -} - const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const { // check cache first @@ -184,11 +181,11 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const else if(type_id==ID_pointer) entry.total_width = type_checked_cast(type).get_width(); else if(type_id==ID_struct_tag) - entry=get_entry(ns.follow_tag(to_struct_tag_type(type))); + entry.total_width = operator()(ns.follow_tag(to_struct_tag_type(type))); else if(type_id==ID_union_tag) - entry=get_entry(ns.follow_tag(to_union_tag_type(type))); + entry.total_width = operator()(ns.follow_tag(to_union_tag_type(type))); else if(type_id==ID_c_enum_tag) - entry=get_entry(ns.follow_tag(to_c_enum_tag_type(type))); + entry.total_width = operator()(ns.follow_tag(to_c_enum_tag_type(type))); else if(type_id==ID_c_bit_field) { entry.total_width=to_c_bit_field_type(type).get_width(); diff --git a/src/solvers/flattening/boolbv_width.h b/src/solvers/flattening/boolbv_width.h index d25115b3a83..36b30e105a1 100644 --- a/src/solvers/flattening/boolbv_width.h +++ b/src/solvers/flattening/boolbv_width.h @@ -11,15 +11,16 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_SOLVERS_FLATTENING_BOOLBV_WIDTH_H #include -#include + +class namespacet; class boolbv_widtht { public: explicit boolbv_widtht(const namespacet &_ns); - ~boolbv_widtht(); + virtual ~boolbv_widtht() = default; - std::size_t operator()(const typet &type) const + virtual std::size_t operator()(const typet &type) const { return get_entry(type).total_width; } diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 77a1592eee1..73ea13b2763 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -65,7 +65,7 @@ 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, boolbv_width}; + return bv_endianness_mapt{type, little_endian, ns, bv_width}; } literalt bv_pointerst::convert_rest(const exprt &expr) diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h index 114237b4d92..fd1bbda6903 100644 --- a/src/solvers/flattening/bv_pointers.h +++ b/src/solvers/flattening/bv_pointers.h @@ -25,6 +25,11 @@ class bv_pointerst:public boolbvt void post_process() override; + std::size_t boolbv_width(const typet &type) const override + { + return bv_width(type); + } + endianness_mapt endianness_map(const typet &type, bool little_endian) const override; From 5cf2b07c12f3753ca5f17c7d10c755fe2f87f59c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 15 Feb 2021 21:56:08 +0000 Subject: [PATCH 3/3] Make pointer flattened width configurable by bv_pointerst In preparation of tweaking the propositional encoding, place all knowledge of the bit width of encoded pointers in bv_pointerst. Also, do not hard-code the width just once, but really look at each type. --- src/solvers/flattening/bv_pointers.cpp | 147 +++++++++++++++++++------ src/solvers/flattening/bv_pointers.h | 35 ++++-- 2 files changed, 144 insertions(+), 38 deletions(-) diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index 73ea13b2763..8791d77d24c 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -65,7 +65,51 @@ 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_width}; + return bv_endianness_mapt{type, little_endian, ns, bv_pointers_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 +{ + // 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 +{ + 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 bv_pointerst::bv_pointers_widtht::get_address_width( + const pointer_typet &type) const +{ + return type.get_width(); } literalt bv_pointerst::convert_rest(const exprt &expr) @@ -83,8 +127,15 @@ literalt bv_pointerst::convert_rest(const exprt &expr) if(!bv.empty()) { + const pointer_typet &type = to_pointer_type(operands[0].type()); + bvt invalid_bv; - encode(pointer_logic.get_invalid_object(), invalid_bv); + encode(pointer_logic.get_invalid_object(), type, invalid_bv); + + const std::size_t object_bits = + bv_pointers_width.get_object_width(type); + const std::size_t offset_bits = + bv_pointers_width.get_offset_width(type); bvt equal_invalid_bv; equal_invalid_bv.resize(object_bits); @@ -139,12 +190,9 @@ 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), + bv_pointers_width(_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( @@ -163,7 +211,8 @@ bool bv_pointerst::convert_address_of_rec( } else if(expr.id() == ID_null_object) { - encode(pointer_logic.get_null_object(), bv); + pointer_typet pt = pointer_type(expr.type()); + encode(pointer_logic.get_null_object(), pt, bv); return false; } else if(expr.id()==ID_index) @@ -173,6 +222,9 @@ bool bv_pointerst::convert_address_of_rec( const exprt &index=index_expr.index(); const typet &array_type = array.type(); + pointer_typet type = pointer_type(expr.type()); + const std::size_t bits = boolbv_width(type); + // recursive call if(array_type.id()==ID_pointer) { @@ -194,7 +246,7 @@ bool bv_pointerst::convert_address_of_rec( auto size = pointer_offset_size(array_type.subtype(), ns); CHECK_RETURN(size.has_value() && *size >= 0); - offset_arithmetic(bv, *size, index); + offset_arithmetic(type, bv, *size, index); CHECK_RETURN(bv.size()==bits); return false; } @@ -207,9 +259,11 @@ bool bv_pointerst::convert_address_of_rec( if(convert_address_of_rec(byte_extract_expr.op(), bv)) return true; + pointer_typet type = pointer_type(expr.type()); + const std::size_t bits = boolbv_width(type); CHECK_RETURN(bv.size()==bits); - offset_arithmetic(bv, 1, byte_extract_expr.offset()); + offset_arithmetic(type, bv, 1, byte_extract_expr.offset()); CHECK_RETURN(bv.size()==bits); return false; } @@ -230,7 +284,8 @@ bool bv_pointerst::convert_address_of_rec( CHECK_RETURN(offset.has_value()); // add offset - offset_arithmetic(bv, *offset); + pointer_typet type = pointer_type(expr.type()); + offset_arithmetic(type, bv, *offset); } else { @@ -273,15 +328,13 @@ bool bv_pointerst::convert_address_of_rec( bvt bv_pointerst::convert_pointer_type(const exprt &expr) { - PRECONDITION(expr.type().id() == ID_pointer); + const pointer_typet &type = to_pointer_type(expr.type()); - // 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) { const irep_idt &identifier=to_symbol_expr(expr).get_identifier(); - const typet &type=expr.type(); return map.get_literals(identifier, type, bits); } @@ -352,7 +405,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) bv.resize(bits); if(value==ID_NULL) - encode(pointer_logic.get_null_object(), bv); + encode(pointer_logic.get_null_object(), type, bv); else { mp_integer i = bvrep2integer(value, bits, false); @@ -433,7 +486,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) sum=bv_utils.add(sum, op); } - offset_arithmetic(bv, size, sum); + offset_arithmetic(type, bv, size, sum); return bv; } @@ -476,7 +529,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) element_size = *element_size_opt; } - offset_arithmetic(bv, element_size, neg_op1); + offset_arithmetic(type, bv, element_size, neg_op1); return bv; } @@ -556,7 +609,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()); @@ -564,10 +618,11 @@ 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( + bv_pointers_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 && @@ -594,7 +649,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()); @@ -603,9 +659,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() + + bv_pointers_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 && @@ -638,6 +697,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 = + bv_pointers_width.get_offset_width(to_pointer_type(type)); for(std::size_t i=0; i