I think this finishes off the CDMap<>/Attribute leaks

2 files changed, 109 insertions, 69 deletions

diff --git a/src/context/cdmap.h b/src/context/cdmap.h
index 1dc44d087..4adf90e4f 100644
--- a/src/context/cdmap.h
+++ b/src/context/cdmap.h
@@ -25,73 +25,76 @@
 #include "context/context.h"
 #include "util/Assert.h"
 
+#include <vector>
 #include <iterator>
 #include <ext/hash_map>
 
 namespace CVC4 {
 namespace context {
 
-// Auxiliary class: almost the same as CDO (see cdo.h), but on
-// setNull() call it erases itself from the map.
+// Auxiliary class: almost the same as CDO (see cdo.h)
 
 template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap;
 
+template <class T, class U>
+inline std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) {
+  return out << "[" << p.first << "," << p.second << "]";
+}
+
 template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
 class CDOmap : public ContextObj {
   Key d_key;
   Data d_data;
-  bool d_inMap; // whether the data must be in the map
-  CDMap<Key, Data, HashFcn>* d_cdmap;
+  CDMap<Key, Data, HashFcn>* d_map;
 
   // Doubly-linked list for keeping track of elements in order of insertion
-  CDOmap<Key, Data, HashFcn>* d_prev;
-  CDOmap<Key, Data, HashFcn>* d_next;
+  CDOmap* d_prev;
+  CDOmap* d_next;
 
   virtual ContextObj* save(ContextMemoryManager* pCMM) {
-    return new(pCMM) CDOmap<Key, Data, HashFcn>(*this);
+    return new(pCMM) CDOmap(*this);
   }
 
   virtual void restore(ContextObj* data) {
-    CDOmap<Key, Data, HashFcn>* p((CDOmap<Key, Data, HashFcn>*) data);
-    if(p->d_inMap) {
-      d_data = p->d_data;
-      d_inMap = true;
-    } else {
-      // Erase itself from the map and put itself into trash.  We cannot
-      // "delete this" here, because it will break context operations in
-      // a non-trivial way.
-      if(d_cdmap->d_map.count(d_key) > 0) {
-        d_cdmap->d_map.erase(d_key);
-        d_cdmap->d_trash.push_back(this);
+    CDOmap* p = static_cast<CDOmap*>(data);
+    if(p->d_map == NULL) {
+      Assert(d_map->d_map.find(d_key) != d_map->d_map.end() &&
+             (*d_map->d_map.find(d_key)).second == this);
+      // no longer in map (popped beyond first level in which it was)
+      d_map->d_map.erase(d_key);
+      // If we call deleteSelf() here, it re-enters restore().  So,
+      // put it on a "trash heap" instead, for later deletion.
+      //
+      // FIXME multithreading
+      if(d_map->d_first == this) {
+        d_map->d_first = d_next;
       }
-
-      d_prev->d_next = d_next;
       d_next->d_prev = d_prev;
-
-      if(d_cdmap->d_first == this) {
-        d_cdmap->d_first = d_next;
-
-        if(d_next == this) {
-          d_cdmap->d_first = NULL;
-        }
-      }
+      d_prev->d_next = d_next;
+      d_map->d_trash.push_back(this);
+    } else {
+      d_data = p->d_data;
     }
   }
 
 public:
 
   CDOmap(Context* context,
-         CDMap<Key, Data, HashFcn>* cdmap,
+         CDMap<Key, Data, HashFcn>* map,
 	 const Key& key,
          const Data& data) :
     ContextObj(context),
     d_key(key),
-    d_inMap(false),
-    d_cdmap(cdmap) {
+    d_map(NULL) {
 
+    // makeCurrent(), then set the data and then the map.  Order is
+    // important; we can't initialize d_map in the constructor init
+    // list above, because we want the restore of d_map to NULL to
+    // signal us to remove the element from the map.
     set(data);
+    d_map = map;
 
-    CDOmap<Key, Data, HashFcn>*& first = d_cdmap->d_first;
+    CDOmap*& first = d_map->d_first;
     if(first == NULL) {
       first = d_next = d_prev = this;
     } else {
@@ -101,12 +104,13 @@ public:
     }
   }
 
-  ~CDOmap() throw(AssertionException) { destroy(); }
+  ~CDOmap() throw(AssertionException) {
+    destroy();
+  }
 
   void set(const Data& data) {
     makeCurrent();
     d_data = data;
-    d_inMap = true;
   }
 
   const Key& getKey() const {
@@ -121,19 +125,19 @@ public:
     return get();
   }
 
-  CDOmap<Key, Data, HashFcn>& operator=(const Data& data) {
+  CDOmap& operator=(const Data& data) {
     set(data);
     return *this;
   }
 
-  CDOmap<Key, Data, HashFcn>* next() const {
-    if(d_next == d_cdmap->d_first) {
+  CDOmap* next() const {
+    if(d_next == d_map->d_first) {
       return NULL;
     } else {
       return d_next;
     }
   }
-};/* class CDOmap */
+};/* class CDOmap<> */
 
 // Dummy subclass of ContextObj to serve as our data class
 class CDMapData : public ContextObj {
@@ -151,6 +155,7 @@ public:
 
   CDMapData(Context* context) : ContextObj(context) {}
   CDMapData(const ContextObj& co) : ContextObj(co) {}
+  ~CDMapData() { destroy(); }
 };
 
 /**
@@ -161,16 +166,18 @@ public:
 template <class Key, class Data, class HashFcn>
 class CDMap : public ContextObj {
 
+  typedef CDOmap<Key, Data, HashFcn> Element;
+  typedef __gnu_cxx::hash_map<Key, Element*, HashFcn> table_type;
+
   friend class CDOmap<Key, Data, HashFcn>;
 
-  typedef __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn> table_type;
   table_type d_map;
 
-  // The vector of CDOmap objects to be destroyed
-  std::vector<CDOmap<Key, Data, HashFcn>*> d_trash;
-  CDOmap<Key, Data, HashFcn>* d_first;
+  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) {
     return new(pCMM) CDMapData(*this);
@@ -179,14 +186,12 @@ class CDMap : public ContextObj {
   // Similarly, nothing to restore
   virtual void restore(ContextObj* data) {}
 
-  // Destroy stale CDOmap objects from trash
   void emptyTrash() {
-    for(typename std::vector<CDOmap<Key, Data, HashFcn>*>::iterator
-          i = d_trash.begin(), iend = d_trash.end(); i != iend; ++i) {
-      /*
-        delete *i;
-        free(*i);
-      */
+    //FIXME multithreading
+    for(typename std::vector<Element*>::iterator i = d_trash.begin();
+        i != d_trash.end();
+        ++i) {
+      (*i)->deleteSelf();
     }
     d_trash.clear();
   }
@@ -196,19 +201,19 @@ public:
   CDMap(Context* context) :
     ContextObj(context),
     d_first(NULL),
-    d_context(context) {
+    d_context(context),
+    d_trash() {
   }
 
   ~CDMap() throw(AssertionException) {
-    // Delete all the elements and clear the map
-    /*for(typename table_type::iterator
-          i = d_map.begin(), iend = d_map.end(); i != iend; ++i) {
-
-        delete (*i).second;
-        free((*i).second);
-
-    }*/
-    d_map.clear();
+    destroy();
+    for(typename table_type::iterator i = d_map.begin();
+        i != d_map.end();
+        ++i) {
+      (*i).second->deleteSelf();
+    }
+    //d_map.clear();
+    Debug("gc") << "cdmap gone, emptying trash" << std::endl;
     emptyTrash();
   }
 
@@ -222,17 +227,15 @@ public:
     return d_map.count(k);
   }
 
-  typedef CDOmap<Key, Data, HashFcn>& ElementReference;
-
   // If a key is not present, a new object is created and inserted
-  CDOmap<Key, Data, HashFcn>& operator[](const Key& k) {
+  Element& operator[](const Key& k) {
     emptyTrash();
 
     typename table_type::iterator i = d_map.find(k);
 
-    CDOmap<Key, Data, HashFcn>* obj;
+    Element* obj;
     if(i == d_map.end()) {// create new object
-      obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, Data());
+      obj = new(true) Element(d_context, this, k, Data());
       d_map[k] = obj;
     } else {
       obj = (*i).second;
@@ -246,8 +249,7 @@ public:
     typename table_type::iterator i = d_map.find(k);
 
     if(i == d_map.end()) {// create new object
-      CDOmap<Key, Data, HashFcn>*
-	obj = new(true) CDOmap<Key, Data, HashFcn>(d_context, this, k, d);
+      Element* obj = new(true) Element(d_context, this, k, d);
       d_map[k] = obj;
     } else {
       (*i).second->set(d);
@@ -256,12 +258,40 @@ public:
 
   // FIXME: no erase(), too much hassle to implement efficiently...
 
+  /**
+   * "Obliterating" is kind of like erasing, except it's not
+   * backtrackable; the key is permanently removed from the map.
+   * (Naturally, it can be re-added as a new element.)
+   */
+  void obliterate(const Key& k) {
+    typename table_type::iterator i = d_map.find(k);
+    if(i != d_map.end()) {
+      Debug("gc") << "key " << k << " obliterated" << std::endl;
+      // We can't call ->deleteSelf() here, because it calls the
+      // ContextObj destructor, which calls CDOmap::destroy(), which
+      // restore()'s, which puts the CDOmap on the trash, which causes
+      // a double-delete.
+      (*i).second->~CDOmap();
+
+      typename table_type::iterator j = d_map.find(k);
+      // This if() succeeds for objects inserted when in the
+      // zero-scope: they were never save()'d there, so restore()
+      // never gets a NULL map and so they leak.
+      if(j != d_map.end()) {
+        Element* elt = (*j).second;
+        d_map.erase(j);//FIXME multithreading
+        // was already destructed, so don't call ->deleteSelf()
+        ::operator delete(elt);
+      }
+    }
+  }
+
   class iterator {
-    const CDOmap<Key, Data, HashFcn>* d_it;
+    const Element* d_it;
 
   public:
 
-    iterator(const CDOmap<Key, Data, HashFcn>* p) : d_it(p) {}
+    iterator(const Element* p) : d_it(p) {}
     iterator(const iterator& i) : d_it(i.d_it) {}
 
     // Default constructor
@@ -302,7 +332,7 @@ public:
 
     // Actual postfix increment: returns Proxy with the old value.
     // Now, an expression like *i++ will return the current *i, and
-    // then advance the orderedIterator.  However, don't try to use
+    // then advance the iterator.  However, don't try to use
     // Proxy for anything else.
     const Proxy operator++(int) {
       Proxy e(*(*this));
@@ -323,6 +353,7 @@ public:
 
   iterator find(const Key& k) const {
     typename table_type::const_iterator i = d_map.find(k);
+
     if(i == d_map.end()) {
       return end();
     } else {
@@ -330,6 +361,11 @@ public:
     }
   }
 
+  iterator find(const Key& k) {
+    emptyTrash();
+    return const_cast<const CDMap*>(this)->find(k);
+  }
+
 };/* class CDMap<> */
 
 }/* CVC4::context namespace */
diff --git a/src/context/context.cpp b/src/context/context.cpp
index d2e2bfa1b..05024430c 100644
--- a/src/context/context.cpp
+++ b/src/context/context.cpp
@@ -177,6 +177,10 @@ ContextObj* ContextObj::restoreAndContinue() {
 
 void ContextObj::destroy() throw(AssertionException) {
   for(;;) {
+    // If valgrind reports invalid writes on the next few lines,
+    // here's a hint: make sure all classes derived from ContextObj in
+    // the system properly call destroy() in their destructors.
+    // That's needed to maintain this linked list properly.
     if(next() != NULL) {
       next()->prev() = prev();
     }