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..c74c4798ef7 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 @@ -46,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) @@ -92,9 +93,19 @@ class boolbvt:public arrayst return map; } - boolbv_widtht boolbv_width; + 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}; + } protected: + boolbv_widtht bv_width; bv_utilst bv_utils; // uninterpreted functions 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 +#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/boolbv_with.cpp b/src/solvers/flattening/boolbv_with.cpp index 3b855b05a92..d770a75712d 100644 --- a/src/solvers/flattening/boolbv_with.cpp +++ b/src/solvers/flattening/boolbv_with.cpp @@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #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..8791d77d24c 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -16,6 +16,102 @@ 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, 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) { PRECONDITION(expr.type().id() == ID_bool); @@ -31,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); @@ -87,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( @@ -111,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) @@ -121,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) { @@ -142,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; } @@ -155,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; } @@ -178,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 { @@ -221,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); } @@ -300,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); @@ -381,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; } @@ -424,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; } @@ -504,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()); @@ -512,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 && @@ -542,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()); @@ -551,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 && @@ -586,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