Merge pull request #1629 from owen-jones-diffblue/owen-jones-diffblue/refactor-vsa-objectt

Replace objectt with optional<mp_integer>

Author: tautschnig

src/pointer-analysis/value_set.cpp

@@ -75,24 +75,23 @@ value_sett::entryt &value_sett::get_entry(
 bool value_sett::insert(
   object_mapt &dest,
   object_numberingt::number_type n,
-  const objectt &object) const
+  const offsett &offset) const
 {
   auto entry=dest.read().find(n);
 
   if(entry==dest.read().end())
   {
     // new
-    dest.write()[n]=object;
+    dest.write()[n] = offset;
     return true;
   }
-  else if(!entry->second.offset_is_set)
+  else if(!entry->second)
     return false; // no change
-  else if(object.offset_is_set &&
-          entry->second.offset==object.offset)
+  else if(offset && *entry->second == *offset)
     return false; // no change
   else
   {
-    dest.write()[n].offset_is_set=false;
+    dest.write()[n].reset();
     return true;
   }
 }
@@ -155,8 +154,8 @@ void value_sett::output(
       {
         result="<"+from_expr(ns, identifier, o)+", ";
 
-        if(o_it->second.offset_is_set)
-          result+=integer2string(o_it->second.offset)+"";
+        if(o_it->second)
+          result += integer2string(*o_it->second) + "";
         else
           result+='*';
 
@@ -199,8 +198,8 @@ exprt value_sett::to_expr(const object_map_dt::value_type &it) const
 
   od.object()=object;
 
-  if(it.second.offset_is_set)
-    od.offset()=from_integer(it.second.offset, index_type());
+  if(it.second)
+    od.offset() = from_integer(*it.second, index_type());
 
   od.type()=od.object().type();
 
@@ -282,7 +281,7 @@ bool value_sett::eval_pointer_offset(
         it=object_map.begin();
         it!=object_map.end();
         it++)
-      if(!it->second.offset_is_set)
+      if(!it->second)
         return false;
       else
       {
@@ -292,7 +291,7 @@ bool value_sett::eval_pointer_offset(
         if(ptr_offset<0)
           return false;
 
-        ptr_offset+=it->second.offset;
+        ptr_offset += *it->second;
 
         if(mod && ptr_offset!=previous_offset)
           return false;
@@ -635,15 +634,15 @@ void value_sett::get_value_set_rec(
         it!=pointer_expr_set.read().end();
         it++)
     {
-      objectt object=it->second;
+      offsett offset = it->second;
 
       // adjust by offset
-      if(object.offset_is_set && i_is_set)
-        object.offset+=i;
+      if(offset && i_is_set)
+        *offset += i;
       else
-        object.offset_is_set=false;
+        offset.reset();
 
-      insert(dest, it->first, object);
+      insert(dest, it->first, offset);
     }
   }
   else if(expr.id()==ID_mult)
@@ -668,12 +667,12 @@ void value_sett::get_value_set_rec(
         it!=pointer_expr_set.read().end();
         it++)
     {
-      objectt object=it->second;
+      offsett offset = it->second;
 
       // kill any offset
-      object.offset_is_set=false;
+      offset.reset();
 
-      insert(dest, it->first, object);
+      insert(dest, it->first, offset);
     }
   }
   else if(expr.id()==ID_side_effect)
@@ -1002,24 +1001,23 @@ void value_sett::get_reference_set_rec(
         if(ns.follow(object.type())!=array_type)
           index_expr.make_typecast(array.type());
 
-        objectt o=a_it->second;
+        offsett o = a_it->second;
         mp_integer i;
 
         if(offset.is_zero())
         {
         }
-        else if(!to_integer(offset, i) &&
-                o.offset_is_set)
+        else if(!to_integer(offset, i) && o)
         {
           mp_integer size=pointer_offset_size(array_type.subtype(), ns);
 
           if(size<=0)
-            o.offset_is_set=false;
+            o.reset();
           else
-            o.offset=i*size;
+            *o = i * size;
         }
         else
-          o.offset_is_set=false;
+          o.reset();
 
         insert(dest, index_expr, o);
       }
@@ -1052,7 +1050,7 @@ void value_sett::get_reference_set_rec(
         insert(dest, exprt(ID_unknown, expr.type()));
       else
       {
-        objectt o=it->second;
+        offsett o = it->second;
 
         member_exprt member_expr(object, component_name, expr.type());
 
@@ -1282,7 +1280,7 @@ void value_sett::do_free(
         else
         {
           // adjust
-          objectt o=o_it->second;
+          offsett o = o_it->second;
           exprt tmp(object);
           to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
           insert(new_object_map, tmp, o);

src/pointer-analysis/value_set.h

@@ -61,54 +61,23 @@ class value_sett
   typedef irep_idt idt;
 
   /// Represents the offset into an object: either a unique integer offset,
-  /// or an unknown value, represented by `!offset_is_set`.
-  class objectt
+  /// or an unknown value, represented by `!offset`.
+  typedef optionalt<mp_integer> offsett;
+  bool offset_is_zero(const offsett &offset) const
   {
-  public:
-    /// Constructs an unknown offset
-    objectt():offset_is_set(false)
-    {
-    }
-
-    /// Constructs a known offset
-    explicit objectt(const mp_integer &_offset):
-      offset(_offset),
-      offset_is_set(true)
-    {
-    }
-
-    /// Offset into the target object. Ignored if `offset_is_set` is false.
-    mp_integer offset;
-
-    /// If true, `offset` gives a unique integer offset; if false, represents
-    /// an unknown offset.
-    bool offset_is_set;
-
-    bool offset_is_zero() const
-    { return offset_is_set && offset.is_zero(); }
-
-    bool operator==(const objectt &other) const
-    {
-      return
-        offset_is_set==other.offset_is_set &&
-        (!offset_is_set || offset==other.offset);
-    }
-    bool operator!=(const objectt &other) const
-    {
-      return !(*this==other);
-    }
-  };
+    return offset && offset->is_zero();
+  }
 
   /// Represents a set of expressions (`exprt` instances) with corresponding
-  /// offsets (`objectt` instances). This is the RHS set of a single row of
+  /// offsets (`offsett` instances). This is the RHS set of a single row of
   /// the enclosing `value_sett`, such as `{ null, dynamic_object1 }`.
-  /// The set is represented as a map from numbered `exprt`s to `objectt`
+  /// The set is represented as a map from numbered `exprt`s to `offsett`
   /// instead of a set of pairs to make lookup by `exprt` easier. All
   /// methods matching the interface of `std::map` forward those methods
   /// to the internal map.
   class object_map_dt
   {
-    typedef std::map<object_numberingt::number_type, objectt> data_typet;
+    typedef std::map<object_numberingt::number_type, offsett> data_typet;
     data_typet data;
 
   public:
@@ -135,9 +104,18 @@ class value_sett
     void erase(key_type i) { data.erase(i); }
     void erase(const_iterator it) { data.erase(it); }
 
-    objectt &operator[](key_type i) { return data[i]; }
-    objectt &at(key_type i) { return data.at(i); }
-    const objectt &at(key_type i) const { return data.at(i); }
+    offsett &operator[](key_type i)
+    {
+      return data[i];
+    }
+    offsett &at(key_type i)
+    {
+      return data.at(i);
+    }
+    const offsett &at(key_type i) const
+    {
+      return data.at(i);
+    }
 
     template <typename It>
     void insert(It b, It e) { data.insert(b, e); }
@@ -210,21 +188,21 @@ class value_sett
   /// \param src: expression to add
   bool insert(object_mapt &dest, const exprt &src) const
   {
-    return insert(dest, object_numbering.number(src), objectt());
+    return insert(dest, object_numbering.number(src), offsett());
   }
 
   /// Adds an expression to an object map, with known offset. If the
   /// destination map has an existing entry for the same expression
   /// with a differing offset its offset is marked unknown.
   /// \param dest: object map to update
   /// \param src: expression to add
-  /// \param offset: offset into `src`
+  /// \param offset_value: offset into `src`
   bool insert(
     object_mapt &dest,
     const exprt &src,
-    const mp_integer &offset) const
+    const mp_integer &offset_value) const
   {
-    return insert(dest, object_numbering.number(src), objectt(offset));
+    return insert(dest, object_numbering.number(src), offsett(offset_value));
   }
 
   /// Adds a numbered expression and offset to an object map. If the
@@ -237,17 +215,17 @@ class value_sett
   bool insert(
     object_mapt &dest,
     object_numberingt::number_type n,
-    const objectt &object) const;
+    const offsett &offset) const;
 
   /// Adds an expression and offset to an object map. If the
   /// destination map has an existing entry for the same expression
   /// with a differing offset its offset is marked unknown.
   /// \param dest: object map to update
   /// \param expr: expression to add
   /// \param object: offset into `expr` (may be unknown).
-  bool insert(object_mapt &dest, const exprt &expr, const objectt &object) const
+  bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
   {
-    return insert(dest, object_numbering.number(expr), object);
+    return insert(dest, object_numbering.number(expr), offset);
   }
 
   /// Represents a row of a `value_sett`. For example, this might represent