pointer_logic: use mp_integer for numbering objects

Replacing std::size_t by mp_integer makes the code more platform-independent
and easier to use as overflow is no longer a concern.

Author: kroening

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