diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-30 08:22:06 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-30 08:22:06 +0000 |
commit | 09d8860f19b928114460386fa17847a8ffb02244 (patch) | |
tree | 72064c34a09c32b7d52a10c28c2684b28149c100 /src/context | |
parent | 473e87a54cdcff5384ebf09dc433a4c2a0b30c8b (diff) |
I think this finishes off the CDMap<>/Attribute leaks
Diffstat (limited to 'src/context')
-rw-r--r-- | src/context/cdmap.h | 174 | ||||
-rw-r--r-- | src/context/context.cpp | 4 |
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(); } |