Merge pull request #6833 from diffblue/pointer_logic_object

pointer_logic: use mp_integer for numbering objects

Author: kroening

src/solvers/flattening/bv_pointers.cpp

@@ -816,18 +816,14 @@ exprt bv_pointerst::bv_get_rec(
     bvrep, pointer_logic.pointer_expr(pointer, pt)};
 }
 
-bvt bv_pointerst::encode(std::size_t addr, const pointer_typet &type) const
+bvt bv_pointerst::encode(const mp_integer &addr, const pointer_typet &type)
+  const
 {
   const std::size_t offset_bits = get_offset_width(type);
   const std::size_t object_bits = get_object_width(type);
 
   bvt zero_offset(offset_bits, const_literal(false));
-
-  // set variable part
-  bvt object;
-  object.reserve(object_bits);
-  for(std::size_t i=0; i<object_bits; i++)
-    object.push_back(const_literal((addr & (std::size_t(1) << i)) != 0));
+  bvt object = bv_utils.build_constant(addr, object_bits);
 
   return object_offset_encoding(object, zero_offset);
 }
@@ -889,7 +885,7 @@ bvt bv_pointerst::offset_arithmetic(
 
 bvt bv_pointerst::add_addr(const exprt &expr)
 {
-  std::size_t a=pointer_logic.add_object(expr);
+  const auto a = pointer_logic.add_object(expr);
 
   const pointer_typet type = pointer_type(expr.type());
   const std::size_t object_bits = get_object_width(type);

src/solvers/flattening/bv_pointers.h

@@ -40,7 +40,7 @@ class bv_pointerst:public boolbvt
   typedef boolbvt SUB;
 
   NODISCARD
-  bvt encode(std::size_t object, const pointer_typet &) const;
+  bvt encode(const mp_integer &object, const pointer_typet &) const;
 
   virtual bvt convert_pointer_type(const exprt &);
 

src/solvers/flattening/pointer_logic.cpp

@@ -31,17 +31,17 @@ bool pointer_logict::is_dynamic_object(const exprt &expr) const
             SYMEX_DYNAMIC_PREFIX));
 }
 
-void pointer_logict::get_dynamic_objects(std::vector<std::size_t> &o) const
+void pointer_logict::get_dynamic_objects(std::vector<mp_integer> &o) const
 {
   o.clear();
-  std::size_t nr=0;
+  mp_integer nr = 0;
 
   for(auto it = objects.cbegin(); it != objects.cend(); ++it, ++nr)
     if(is_dynamic_object(*it))
       o.push_back(nr);
 }
 
-std::size_t pointer_logict::add_object(const exprt &expr)
+mp_integer pointer_logict::add_object(const exprt &expr)
 {
   // remove any index/member
 
@@ -58,11 +58,10 @@ std::size_t pointer_logict::add_object(const exprt &expr)
 }
 
 exprt pointer_logict::pointer_expr(
-  std::size_t object,
+  const mp_integer &object,
   const pointer_typet &type) const
 {
-  pointert pointer(object, 0);
-  return pointer_expr(pointer, type);
+  return pointer_expr({object, 0}, type);
 }
 
 exprt pointer_logict::pointer_expr(
@@ -89,10 +88,11 @@ exprt pointer_logict::pointer_expr(
 
   if(pointer.object>=objects.size())
   {
-    return constant_exprt("INVALID-" + std::to_string(pointer.object), type);
+    return constant_exprt("INVALID-" + integer2string(pointer.object), type);
   }
 
-  const exprt &object_expr=objects[pointer.object];
+  const exprt &object_expr =
+    objects[numeric_cast_v<std::size_t>(pointer.object)];
 
   typet subtype = type.base_type();
   // This is a gcc extension.

src/solvers/flattening/pointer_logic.h

@@ -27,14 +27,14 @@ class pointer_logict
 
   struct pointert
   {
-    std::size_t object;
-    mp_integer offset;
+    mp_integer object, offset;
 
     pointert()
     {
     }
 
-    pointert(std::size_t _obj, mp_integer _off):object(_obj), offset(_off)
+    pointert(mp_integer _obj, mp_integer _off)
+      : object(std::move(_obj)), offset(std::move(_off))
     {
     }
   };
@@ -45,34 +45,32 @@ class pointer_logict
     const pointer_typet &type) const;
 
   /// Convert an (object,0) pair to an expression
-  exprt pointer_expr(
-    std::size_t object,
-    const pointer_typet &type) const;
+  exprt pointer_expr(const mp_integer &object, const pointer_typet &type) const;
 
   ~pointer_logict();
   explicit pointer_logict(const namespacet &_ns);
 
-  std::size_t add_object(const exprt &expr);
+  mp_integer add_object(const exprt &expr);
 
   /// \return number of NULL object
-  std::size_t get_null_object() const
+  const mp_integer &get_null_object() const
   {
     return null_object;
   }
 
   /// \return number of INVALID object
-  std::size_t get_invalid_object() const
+  const mp_integer &get_invalid_object() const
   {
     return invalid_object;
   }
 
   bool is_dynamic_object(const exprt &expr) const;
 
-  void get_dynamic_objects(std::vector<std::size_t> &objects) const;
+  void get_dynamic_objects(std::vector<mp_integer> &objects) const;
 
 protected:
   const namespacet &ns;
-  std::size_t null_object, invalid_object;
+  mp_integer null_object, invalid_object;
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H

src/solvers/smt2/smt2_conv.cpp

@@ -3153,7 +3153,7 @@ void smt2_convt::convert_mod(const mod_exprt &expr)
 
 void smt2_convt::convert_is_dynamic_object(const unary_exprt &expr)
 {
-  std::vector<std::size_t> dynamic_objects;
+  std::vector<mp_integer> dynamic_objects;
   pointer_logic.get_dynamic_objects(dynamic_objects);
 
   if(dynamic_objects.empty())