Merge pull request #5822 from tautschnig/pointer-encoding-width

Store pointer encoding configuration in boolbv_widtht

Author: tautschnig

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.

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 \

src/solvers/flattening/boolbv.h

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 //
 
 #include <util/byte_operators.h>
+#include <util/endianness_map.h>
 #include <util/expr.h>
 #include <util/mp_arith.h>
 #include <util/optional.h>
@@ -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

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -17,9 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/lowering/expr_lowering.h>
 
-#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);
 

src/solvers/flattening/boolbv_byte_update.cpp

@@ -15,8 +15,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/lowering/expr_lowering.h>
 
-#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<std::size_t>(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<update_width; bit++)
       if(offset+bit<bv.size())

src/solvers/flattening/boolbv_union.cpp

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

src/solvers/flattening/boolbv_width.cpp

@@ -13,16 +13,13 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/exception_utils.h>
 #include <util/invariant.h>
+#include <util/namespace.h>
 #include <util/std_types.h>
 
 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<pointer_typet>(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();

src/solvers/flattening/boolbv_width.h

@@ -11,15 +11,16 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_SOLVERS_FLATTENING_BOOLBV_WIDTH_H
 
 #include <util/std_types.h>
-#include <util/namespace.h>
+
+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;
   }

src/solvers/flattening/boolbv_with.cpp

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