** 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
** 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"
} 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;
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();
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
// 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;
}
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
* 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,
}
}
- iterator find(const Key& k) {
- emptyTrash();
- return const_cast<const CDHashMap*>(this)->find(k);
- }
};/* class CDHashMap<> */
#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"
*/
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);
* 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
::operator delete(this);
}
+ /**
+ * Use this to enqueue calling deleteSelf() at the time of the destruction of
+ * the enclosing Scope.
+ */
+ void enqueueToGarbageCollect();
+
};/* class ContextObj */
/**
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) {
projects / cvc5.git / commitdiff