From 34114b8f392e74647ba5c3956182e864ab101a96 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 9 Aug 2017 18:31:07 +0100 Subject: [PATCH] Use a specialised endianness map for flattening The bit width of flattened expressions need not coincide with the size of data types at source code level. Thus the mapping needs to be adjusted. --- src/solvers/Makefile | 1 + .../flattening/boolbv_byte_extract.cpp | 8 ++-- src/solvers/flattening/boolbv_byte_update.cpp | 11 ++--- src/solvers/flattening/boolbv_union.cpp | 7 ++-- src/solvers/flattening/boolbv_with.cpp | 7 ++-- src/solvers/flattening/bv_endianness_map.cpp | 36 +++++++++++++++++ src/solvers/flattening/bv_endianness_map.h | 40 +++++++++++++++++++ src/util/endianness_map.h | 8 +++- 8 files changed, 101 insertions(+), 17 deletions(-) create mode 100644 src/solvers/flattening/bv_endianness_map.cpp create mode 100644 src/solvers/flattening/bv_endianness_map.h diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 3d1a572eb36..73785f7e3af 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -127,6 +127,7 @@ SRC = $(BOOLEFORCE_SRC) \ flattening/boolbv_vector.cpp \ flattening/boolbv_width.cpp \ flattening/boolbv_with.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_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp index f3841a6f0f3..2515da21123 100644 --- a/src/solvers/flattening/boolbv_byte_extract.cpp +++ b/src/solvers/flattening/boolbv_byte_extract.cpp @@ -12,15 +12,15 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include "bv_conversion_exceptions.h" +#include "bv_endianness_map.h" #include "flatten_byte_extract_exceptions.h" #include "flatten_byte_operators.h" -bvt map_bv(const endianness_mapt &map, const bvt &src) +bvt map_bv(const bv_endianness_mapt &map, const bvt &src) { assert(map.number_of_bits()==src.size()); @@ -95,11 +95,11 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr) // first do op0 - endianness_mapt op_map(op.type(), little_endian, ns); + bv_endianness_mapt op_map(op.type(), little_endian, ns, boolbv_width); const bvt op_bv=map_bv(op_map, convert_bv(op)); // do result - endianness_mapt result_map(expr.type(), little_endian, ns); + bv_endianness_mapt result_map(expr.type(), little_endian, ns, boolbv_width); bvt bv; bv.resize(width); diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp index 1ffcd8d91b7..66b3cf68180 100644 --- a/src/solvers/flattening/boolbv_byte_update.cpp +++ b/src/solvers/flattening/boolbv_byte_update.cpp @@ -13,7 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include + +#include "bv_endianness_map.h" bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) { @@ -63,8 +64,8 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) } else { - endianness_mapt map_op(op.type(), false, ns); - endianness_mapt map_value(value.type(), false, ns); + bv_endianness_mapt map_op(op.type(), false, ns, boolbv_width); + bv_endianness_mapt map_value(value.type(), false, ns, boolbv_width); std::size_t offset_i=integer2unsigned(offset); @@ -93,8 +94,8 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr) equality.rhs()=from_integer(offset/byte_width, offset_expr.type()); literalt equal=convert(equality); - endianness_mapt map_op(op.type(), little_endian, ns); - endianness_mapt map_value(value.type(), little_endian, ns); + bv_endianness_mapt map_op(op.type(), little_endian, ns, boolbv_width); + bv_endianness_mapt map_value(value.type(), little_endian, ns, boolbv_width); for(std::size_t bit=0; bit #include -#include + +#include "bv_endianness_map.h" bvt boolbvt::convert_union(const union_exprt &expr) { @@ -41,8 +42,8 @@ bvt boolbvt::convert_union(const union_exprt &expr) assert( config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_BIG_ENDIAN); - endianness_mapt map_u(expr.type(), false, ns); - endianness_mapt map_op(expr.op0().type(), false, ns); + bv_endianness_mapt map_u(expr.type(), false, ns, boolbv_width); + bv_endianness_mapt map_op(expr.op0().type(), false, ns, boolbv_width); for(std::size_t i=0; i #include #include -#include #include +#include "bv_endianness_map.h" + bvt boolbvt::convert_with(const exprt &expr) { if(expr.operands().size()<3) @@ -286,8 +287,8 @@ void boolbvt::convert_with_union( assert( config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_BIG_ENDIAN); - endianness_mapt map_u(type, false, ns); - endianness_mapt map_op2(op2.type(), false, ns); + bv_endianness_mapt map_u(type, false, ns, boolbv_width); + bv_endianness_mapt map_op2(op2.type(), false, ns, boolbv_width); 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 new file mode 100644 index 00000000000..d15f3d463b2 --- /dev/null +++ b/src/solvers/flattening/bv_endianness_map.h @@ -0,0 +1,40 @@ +/*******************************************************************\ + +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/util/endianness_map.h b/src/util/endianness_map.h index 835f7e52938..6d6900d7ad4 100644 --- a/src/util/endianness_map.h +++ b/src/util/endianness_map.h @@ -37,6 +37,10 @@ class endianness_mapt build(type, little_endian); } + explicit endianness_mapt(const namespacet &_ns) : ns(_ns) + { + } + size_t map_bit(size_t bit) const { assert(bit map; // bit-nr to bit-nr - void build_little_endian(const typet &type); - void build_big_endian(const typet &type); + virtual void build_little_endian(const typet &type); + virtual void build_big_endian(const typet &type); }; inline std::ostream &operator<<(