Merge pull request diffblue#2066 from tautschnig/bv-endianness

Use a specialised endianness map for flattening

Author: Daniel Kroening

src/solvers/Makefile

@@ -135,6 +135,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

@@ -12,15 +12,15 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
-#include <util/endianness_map.h>
 #include <util/std_expr.h>
 #include <util/throw_with_nested.h>
 
 #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);
 

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(src);
+  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<<(