Value-set: add support for a base value-set

This is a simple copy-on-write base, intended to allow cheap local analysis on top of a potentially
large, possibly mutable global state.

Author: smowton

src/pointer-analysis/value_set.cpp

@@ -55,7 +55,10 @@ const value_sett::entryt *value_sett::find_entry(const value_sett::idt &id)
   const
 {
   auto found = values.find(id);
-  return found == values.end() ? nullptr : &found->second;
+  if(found != values.end())
+    return &found->second;
+  else
+    return base_value_set ? base_value_set->find_entry(id) : nullptr;
 }
 
 value_sett::entryt &value_sett::get_entry(
@@ -73,6 +76,14 @@ value_sett::entryt &value_sett::get_entry(
   std::pair<valuest::iterator, bool> r=
     values.insert(std::pair<idt, entryt>(index, e));
 
+  if(base_value_set && r.second)
+  {
+    // New entry; copy the existing base entry if found.
+    const entryt *base_entry = base_value_set->find_entry(index);
+    if(base_entry)
+      r.first->second = *base_entry;
+  }
+
   return r.first->second;
 }
 
@@ -188,6 +199,12 @@ void value_sett::output(
 
     out << " } \n";
   }
+
+  if(base_value_set)
+  {
+    out << "NB. the base value-set (" << base_value_set << ") has a further "
+        << base_value_set->size() << " entries\n";
+  }
 }
 
 exprt value_sett::to_expr(const object_map_dt::value_type &it) const
@@ -212,6 +229,10 @@ exprt value_sett::to_expr(const object_map_dt::value_type &it) const
 
 bool value_sett::make_union(const value_sett::valuest &new_values)
 {
+  // Note this method makes no reference to base_value_set -- we assume that
+  // we share the same base, if any, with new_values. This is enforced in the
+  // make_union(const value_sett &) overload.
+
   bool result=false;
 
   valuest::iterator v_it=values.begin();
@@ -1666,3 +1687,13 @@ exprt value_sett::make_member(
 
   return member_expr;
 }
+
+void value_sett::set_base_value_set(const value_sett *base)
+{
+  // Simplifying assumptions -- this way we don't need to check for clashing
+  // keys, for example:
+  INVARIANT(size() == 0, "base_value_set cannot be set for a non-empty set");
+  INVARIANT(!base_value_set, "base_value_set cannot be reset");
+
+  base_value_set = base;
+}

src/pointer-analysis/value_set.h

@@ -38,10 +38,21 @@ class namespacet;
 /// pairs of an `exprt` and an optional offset if known (0 for both dynamic
 /// objects in the example given above). RHS expressions are represented using
 /// numbering to avoid storing redundant duplicate expressions.
+///
+/// A value_sett may have a base (stored in field base_value_set), in which case
+/// any lookup that fails in this value-set will check the base, and any write
+/// to this value-set will copy any entry in the base into this value-set before
+/// performing the write (i.e. we act as a copy-on-write layer on top of the
+/// base). This makes copying or union'ing value-sets with a common base
+/// cheaper -- the intended use case is for faster local analysis on top of a
+/// large, expensive-to-copy global context. value_sett::make_union requires
+/// that the value-sets being merged have the same base (or both have no base);
+/// it is up to the user to make sure this is true.
+
 class value_sett
 {
 public:
-  value_sett():location_number(0)
+  value_sett():location_number(0), base_value_set(nullptr)
   {
   }
 
@@ -340,6 +351,12 @@ class value_sett
     const entryt &e, const typet &type,
     const namespacet &ns);
 
+  /// Gets the number of entries in this value-set.
+  valuest::size_type size() const
+  {
+    return values.size();
+  }
+
   /// Pretty-print this value-set
   /// \param ns: global namespace
   /// \param [out] out: stream to write to
@@ -366,6 +383,9 @@ class value_sett
   /// \return true if anything changed.
   bool make_union(const value_sett &new_values)
   {
+    INVARIANT(
+      new_values.base_value_set == base_value_set,
+      "Unioned value-sets must have the same base");
     return make_union(new_values.values);
   }
 
@@ -459,6 +479,11 @@ class value_sett
     exprt &expr,
     const namespacet &ns) const;
 
+  /// Set the base value-set, to which failing queries fall through. Note for
+  /// simplicity's sake, at the moment this value-set must be empty when this
+  /// is called, and the base value-set cannot be reset later.
+  void set_base_value_set(const value_sett *base);
+
 protected:
   /// Reads the set of objects pointed to by `expr`, including making
   /// recursive lookups for dereference operations etc.
@@ -550,6 +575,8 @@ class value_sett
     const namespacet &)
   {
   }
+
+  const value_sett *base_value_set;
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H