Adding a garbage list that get collected during the ~Scope. Removing the CDHashMap garbage.

3 files changed, 116 insertions, 132 deletions

diff --git a/src/context/cdhashmap.h b/src/context/cdhashmap.h
index 86a7cb141..21e30cef6 100644
--- a/src/context/cdhashmap.h
+++ b/src/context/cdhashmap.h
@@ -58,7 +58,7 @@
  **     its CDOhash_map object memory freed.  Here, the CDOhash_map is restored
  **     to a "NULL-map" state (see above), signaling it to remove
  **     itself from the map completely and put itself on a "trash
- **     list" for the map.
+ **     list" for its scope.
  **
  **     Third, you might obliterate() the key.  This calls the CDOhash_map
  **     destructor, which calls destroy(), which does a successive
@@ -70,24 +70,18 @@
  **     Fourth, you might delete the cdhashmap(calling CDHashMap::~CDHashMap()).
  **     This first calls destroy(), as per ContextObj contract, but
  **     cdhashmapdoesn't save/restore itself, so that does nothing at the
- **     CDHashMap-level.  Then it empties the trash.  Then, for each
- **     element in the map, it marks it as being "part of a complete
- **     map destruction", which essentially short-circuits
+ **     CDHashMap-level. Then, for each element in the map, it marks it as being
+ **     "part of a complete map destruction", which essentially short-circuits
  **     CDOhash_map::restore() (see CDOhash_map::restore()), then deallocates
- **     it.  Finally it asserts that the trash is empty (which it
- **     should be, since restore() was short-circuited).
+ **     it.
  **
  **     Fifth, you might clear() the CDHashMap.  This does exactly the
  **     same as CDHashMap::~CDHashMap(), except that it doesn't call destroy()
  **     on itself.
  **
- **     CDHashMap::emptyTrash() simply goes through and calls
- **     ->deleteSelf() on all elements in the trash.
  **     ContextObj::deleteSelf() calls the CDOhash_map destructor, then
  **     frees the memory associated to the CDOhash_map.  CDOhash_map::~CDOhash_map()
- **     calls destroy(), which restores as much as possible.  (Note,
- **     though, that since objects placed on the trash have already
- **     restored to the fullest extent possible, it does nothing.)
+ **     calls destroy(), which restores as much as possible.
  **/
 
 #include "cvc4_private.h"
@@ -157,7 +151,7 @@ class CDOhash_map : public ContextObj {
         } else {
           Debug("gc") << "CDHashMap<> trash push_back " << this << std::endl;
           //this->deleteSelf();
-          d_map->d_trash.push_back(this);
+          enqueueToGarbageCollect();
         }
       } else {
         d_data = p->d_data;
@@ -290,8 +284,6 @@ class CDHashMap : public ContextObj {
   Element* d_first;
   Context* d_context;
 
-  std::vector<Element*> d_trash;
-
   // Nothing to save; the elements take care of themselves
   virtual ContextObj* save(ContextMemoryManager* pCMM) {
     Unreachable();
@@ -302,75 +294,38 @@ class CDHashMap : public ContextObj {
     Unreachable();
   }
 
-  void emptyTrash() {
-    //FIXME multithreading
-    for(typename std::vector<Element*>::iterator i = d_trash.begin();
-        i != d_trash.end();
-        ++i) {
-      Debug("gc") << "emptyTrash(): " << *i << std::endl;
-      (*i)->deleteSelf();
-    }
-    d_trash.clear();
-  }
-
   // no copy or assignment
   CDHashMap(const CDHashMap&) CVC4_UNDEFINED;
   CDHashMap& operator=(const CDHashMap&) CVC4_UNDEFINED;
 
 public:
-
-  CDHashMap(Context* context) :
-    ContextObj(context),
-    d_map(),
-    d_first(NULL),
-    d_context(context),
-    d_trash() {
-  }
+  CDHashMap(Context* context)
+    : ContextObj(context), d_map(), d_first(NULL), d_context(context) {}
 
   ~CDHashMap() {
-    Debug("gc") << "cdhashmap" << this
-                << " disappearing, destroying..." << std::endl;
+    Debug("gc") << "cdhashmap" << this << " disappearing, destroying..."
+                << std::endl;
     destroy();
-    Debug("gc") << "cdhashmap" << this
-                << " disappearing, done destroying" << std::endl;
-
-    Debug("gc") << "cdhashmap" << this << " gone, emptying trash" << std::endl;
-    emptyTrash();
-    Debug("gc") << "done emptying trash for " << this << std::endl;
-
-    for(typename table_type::iterator i = d_map.begin();
-        i != d_map.end();
-        ++i) {
-      // mark it as being a destruction (short-circuit restore())
-      (*i).second->d_map = NULL;
-      if(!(*i).second->d_noTrash) {
-        (*i).second->deleteSelf();
-      }
-    }
-    d_map.clear();
-    d_first = NULL;
-
-    Assert(d_trash.empty());
+    Debug("gc") << "cdhashmap" << this << " disappearing, done destroying"
+                << std::endl;
+    clear();
   }
 
-  void clear() throw(AssertionException) {
-    Debug("gc") << "clearing cdhashmap" << this << ", emptying trash" << std::endl;
-    emptyTrash();
+  void clear() {
+    Debug("gc") << "clearing cdhashmap" << this << ", emptying trash"
+                << std::endl;
     Debug("gc") << "done emptying trash for " << this << std::endl;
 
-    for(typename table_type::iterator i = d_map.begin();
-        i != d_map.end();
-        ++i) {
+    for (auto& key_element_pair : d_map) {
       // mark it as being a destruction (short-circuit restore())
-      (*i).second->d_map = NULL;
-      if(!(*i).second->d_noTrash) {
-        (*i).second->deleteSelf();
+      Element* element = key_element_pair.second;
+      element->d_map = nullptr;
+      if (!element->d_noTrash) {
+        element->deleteSelf();
       }
     }
     d_map.clear();
-    d_first = NULL;
-
-    Assert(d_trash.empty());
+    d_first = nullptr;
   }
 
   // The usual operators of map
@@ -389,8 +344,6 @@ public:
 
   // If a key is not present, a new object is created and inserted
   Element& operator[](const Key& k) {
-    emptyTrash();
-
     typename table_type::iterator i = d_map.find(k);
 
     Element* obj;
@@ -404,8 +357,6 @@ public:
   }
 
   bool insert(const Key& k, const Data& d) {
-    emptyTrash();
-
     typename table_type::iterator i = d_map.find(k);
 
     if(i == d_map.end()) {// create new object
@@ -443,8 +394,6 @@ public:
    * insertAtContextLevelZero() a key that already is in the map.
    */
   void insertAtContextLevelZero(const Key& k, const Data& d) {
-    emptyTrash();
-
     AlwaysAssert(d_map.find(k) == d_map.end());
 
     Element* obj = new(true) Element(d_context, this, k, d,
@@ -566,10 +515,6 @@ public:
     }
   }
 
-  iterator find(const Key& k) {
-    emptyTrash();
-    return const_cast<const CDHashMap*>(this)->find(k);
-  }
 
 };/* class CDHashMap<> */
 
diff --git a/src/context/context.cpp b/src/context/context.cpp
index 2b781b95c..66d6a6542 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -296,6 +296,10 @@ ContextObj::ContextObj(bool allocatedInCMM, Context* pContext) :
   d_pScope->addToChain(this);
 }
 
+void ContextObj::enqueueToGarbageCollect() {
+  Assert(d_pScope != NULL);
+  d_pScope->enqueueToGarbageCollect(this);
+}
 
 ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) {
   if(preNotify) {
@@ -354,6 +358,29 @@ std::ostream& operator<<(std::ostream& out,
   return out << " --> NULL";
 }
 
+Scope::~Scope() {
+  // Call restore() method on each ContextObj object in the list.
+  // Note that it is the responsibility of restore() to return the
+  // next item in the list.
+  while (d_pContextObjList != NULL) {
+    d_pContextObjList = d_pContextObjList->restoreAndContinue();
+  }
+
+  if (d_garbage) {
+    while (!d_garbage->empty()) {
+      ContextObj* obj = d_garbage->back();
+      d_garbage->pop_back();
+      obj->deleteSelf();
+    }
+  }
+}
+
+void Scope::enqueueToGarbageCollect(ContextObj* obj) {
+  if (!d_garbage) {
+    d_garbage.reset(new std::vector<ContextObj*>);
+  }
+  d_garbage->push_back(obj);
+}
 
 } /* CVC4::context namespace */
 } /* CVC4 namespace */
diff --git a/src/context/context.h b/src/context/context.h
index 9b3f57a5d..92eb10441 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -19,12 +19,13 @@
 #ifndef __CVC4__CONTEXT__CONTEXT_H
 #define __CVC4__CONTEXT__CONTEXT_H
 
-#include <iostream>
 #include <cstdlib>
 #include <cstring>
-#include <vector>
+#include <iostream>
+#include <memory>
 #include <new>
 #include <typeinfo>
+#include <vector>
 
 #include "base/cvc4_assert.h"
 #include "base/output.h"
@@ -257,6 +258,14 @@ class Scope {
    */
   ContextObj* d_pContextObjList;
 
+  /**
+   * A list of ContextObj to be garbage collected before the destruction of this
+   * scope. deleteSelf() will be called on each element during ~Scope().
+   *
+   * This is either nullptr or list owned by this scope.
+   */
+  std::unique_ptr<std::vector<ContextObj*>> d_garbage;
+
   friend std::ostream&
   operator<<(std::ostream&, const Scope&) throw(AssertionException);
 
@@ -266,54 +275,60 @@ public:
    * Constructor: Create a new Scope; set the level and the previous Scope
    * if any.
    */
-  Scope(Context* pContext, ContextMemoryManager* pCMM, int level) throw() :
-    d_pContext(pContext),
-    d_pCMM(pCMM),
-    d_level(level),
-    d_pContextObjList(NULL) {
+ Scope(Context* pContext, ContextMemoryManager* pCMM, int level) throw()
+     : d_pContext(pContext),
+       d_pCMM(pCMM),
+       d_level(level),
+       d_pContextObjList(nullptr),
+       d_garbage() {}
+
+ /**
+  * Destructor: Clears out all of the garbage and restore all of the objects
+  * in ContextObjList.
+  */
+ ~Scope();
+
+ /**
+  * Get the Context for this Scope
+  */
+ Context* getContext() const throw() { return d_pContext; }
+
+ /**
+  * Get the ContextMemoryManager for this Scope
+  */
+ ContextMemoryManager* getCMM() const throw() { return d_pCMM; }
+
+ /**
+  * Get the level of the current Scope
+  */
+ int getLevel() const throw() { return d_level; }
+
+ /**
+  * Return true iff this Scope is the current top Scope
+  */
+ bool isCurrent() const throw() { return this == d_pContext->getTopScope(); }
+
+ /**
+  * When a ContextObj object is modified for the first time in this
+  * Scope, it should call this method to add itself to the list of
+  * objects that will need to be restored.  Defined inline below.
+  */
+ void addToChain(ContextObj* pContextObj) throw(AssertionException);
+
+ /**
+  * Overload operator new for use with ContextMemoryManager to allow
+  * creation of new Scope objects in the current memory region.
+  */
+ static void* operator new(size_t size, ContextMemoryManager* pCMM) {
+   Trace("context_mm") << "Scope::new " << size << " in " << pCMM << std::endl;
+   return pCMM->newData(size);
   }
 
   /**
-   * Destructor: Restore all of the objects in ContextObjList.  Defined inline
-   * below.
-   */
-  ~Scope();
-
-  /**
-   * Get the Context for this Scope
-   */
-  Context* getContext() const throw() { return d_pContext; }
-
-  /**
-   * Get the ContextMemoryManager for this Scope
+   * Enqueues a ContextObj to be garbage collected via a call to deleteSelf()
+   * during the destruction of this scope.
    */
-  ContextMemoryManager* getCMM() const throw() { return d_pCMM; }
-
-  /**
-   * Get the level of the current Scope
-   */
-  int getLevel() const throw() { return d_level; }
-
-  /**
-   * Return true iff this Scope is the current top Scope
-   */
-  bool isCurrent() const throw() { return this == d_pContext->getTopScope(); }
-
-  /**
-   * When a ContextObj object is modified for the first time in this
-   * Scope, it should call this method to add itself to the list of
-   * objects that will need to be restored.  Defined inline below.
-   */
-  void addToChain(ContextObj* pContextObj) throw(AssertionException);
-
-  /**
-   * Overload operator new for use with ContextMemoryManager to allow
-   * creation of new Scope objects in the current memory region.
-   */
-  static void* operator new(size_t size, ContextMemoryManager* pCMM) {
-    Trace("context_mm") << "Scope::new " << size << " in " << pCMM << std::endl;
-    return pCMM->newData(size);
-  }
+  void enqueueToGarbageCollect(ContextObj* obj);
 
   /**
    * Overload operator delete for Scope objects allocated using
@@ -647,6 +662,12 @@ public:
     ::operator delete(this);
   }
 
+  /**
+   * Use this to enqueue calling deleteSelf() at the time of the destruction of
+   * the enclosing Scope.
+   */
+  void enqueueToGarbageCollect();
+
 };/* class ContextObj */
 
 /**
@@ -725,15 +746,6 @@ inline void ContextObj::makeSaveRestorePoint() throw(AssertionException) {
   update();
 }
 
-inline Scope::~Scope() {
-  // Call restore() method on each ContextObj object in the list.
-  // Note that it is the responsibility of restore() to return the
-  // next item in the list.
-  while(d_pContextObjList != NULL) {
-    d_pContextObjList = d_pContextObjList->restoreAndContinue();
-  }
-}
-
 inline void
 Scope::addToChain(ContextObj* pContextObj) throw(AssertionException) {
   if(d_pContextObjList != NULL) {