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.

Author: tautschnig

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 \

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -13,11 +13,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
 #include <util/byte_operators.h>
-#include <util/endianness_map.h>
 
+#include "bv_endianness_map.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());
 
@@ -84,11 +84,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);
 

src/solvers/flattening/boolbv_byte_update.cpp

@@ -13,7 +13,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
-#include <util/endianness_map.h>
+
+#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<update_width; bit++)
       if(offset+bit<bv.size())

src/solvers/flattening/boolbv_union.cpp

@@ -10,7 +10,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/config.h>
-#include <util/endianness_map.h>
+
+#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<op_bv.size(); i++)
       bv[map_u.map_bit(i)]=op_bv[map_op.map_bit(i)];

src/solvers/flattening/boolbv_with.cpp

@@ -12,9 +12,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/arith_tools.h>
 #include <util/base_type.h>
-#include <util/endianness_map.h>
 #include <util/config.h>
 
+#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<op2_bv.size(); i++)
       next_bv[map_u.map_bit(i)]=op2_bv[map_op2.map_bit(i)];

src/solvers/flattening/bv_endianness_map.cpp

@@ -0,0 +1,36 @@
+/*******************************************************************\
+
+Module:
+
+Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include "bv_endianness_map.h"
+
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+
+#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(type);
+  else
+    endianness_mapt::build_big_endian(src);
+}

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 <util/endianness_map.h>
+
+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

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.size());
@@ -58,8 +62,8 @@ class endianness_mapt
   const namespacet &ns;
   std::vector<size_t> 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<<(