From e11bce2790fa9e517e08ae5d3c477da651db3630 Mon Sep 17 00:00:00 2001 From: Tim King Date: Tue, 23 Mar 2010 19:41:49 +0000 Subject: [PATCH] Fixed some memory cleanup and destruction issues with ContextObj, ECData, CDList, and CDMap. Added the d_underTheShotgun field to NodeManager to keep track of which NodeValue is currently being deleted. If a Node or TNode has this node value, it can always be deleted. This avoids the need for introducing SoftNodes. Currently passes Debug and Production make check --- src/context/cdlist.h | 10 ++++++++-- src/context/cdmap.h | 10 +++++----- src/context/context.h | 3 ++- src/expr/node.h | 4 +++- src/expr/node_manager.cpp | 15 +++++++++++++++ src/expr/node_manager.h | 11 ++++++++++- src/expr/node_value.h | 12 ++++++++++++ src/theory/uf/ecdata.h | 2 ++ 8 files changed, 57 insertions(+), 10 deletions(-) diff --git a/src/context/cdlist.h b/src/context/cdlist.h index e3c7e155c..492dc7939 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -138,9 +138,15 @@ public: * Destructor: delete the list */ ~CDList() throw(AssertionException) { - T* list = d_list; destroy(); - free(list); + + if(d_callDestructor) { + for(unsigned i = 0; i < d_size; ++i) { + d_list[i].~T(); + } + } + + free(d_list); } /** diff --git a/src/context/cdmap.h b/src/context/cdmap.h index 460f917ff..1dc44d087 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -201,13 +201,13 @@ public: ~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) { - /* + /*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(); emptyTrash(); } diff --git a/src/context/context.h b/src/context/context.h index 6b9f9fd6d..87e4e5fa1 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -399,7 +399,7 @@ public: /** * Destructor does nothing: subclass must explicitly call destroy() instead. */ - virtual ~ContextObj() {} + virtual ~ContextObj() { Debug("contextgc") << "context obj dest" << std::endl; } /** * If you want to allocate a ContextObj object on the heap, use this @@ -426,6 +426,7 @@ public: * ContextMemoryManager as an argument. */ void deleteSelf() { + this->~ContextObj(); ::operator delete(this); } diff --git a/src/expr/node.h b/src/expr/node.h index 25990cedf..f7cef5a4c 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -522,7 +522,9 @@ NodeTemplate::~NodeTemplate() throw(AssertionException) { if(ref_count) { d_nv->dec(); } - Assert(ref_count || d_nv->d_rc > 0, + Assert(ref_count || + d_nv->d_rc > 0 || + d_nv->isBeingDeleted(), "Temporary node pointing to an expired node"); } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 7b171a48b..ee370f682 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -61,6 +61,19 @@ struct Reclaim { } }; +struct NVReclaim { + NodeValue*& d_reclaimField; + NVReclaim(NodeValue*& reclaim) : + d_reclaimField(reclaim) { + + Debug("gc") << ">> setting NVRECLAIM field\n"; + } + ~NVReclaim() { + Debug("gc") << "<< clearing NVRECLAIM field\n"; + d_reclaimField = NULL; + } +}; + void NodeManager::reclaimZombies() { // FIXME multithreading @@ -104,6 +117,8 @@ void NodeManager::reclaimZombies() { if(nv->getKind() != kind::VARIABLE) { poolRemove(nv); } + NVReclaim rc(d_underTheShotgun); + d_underTheShotgun = nv; // remove attributes d_attrManager.deleteAllAttributes(nv); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index a3be61e48..044deac7f 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -72,6 +72,12 @@ class NodeManager { friend class NodeManagerScope; friend class expr::NodeValue; + bool isCurrentlyDeleting(const expr::NodeValue *nv) const{ + return d_underTheShotgun == nv; + } + + expr::NodeValue* d_underTheShotgun; + bool d_reclaiming; ZombieSet d_zombies; @@ -105,7 +111,10 @@ public: NodeManager(context::Context* ctxt) : d_attrManager(ctxt), - d_reclaiming(false) { + d_underTheShotgun(NULL), + d_reclaiming(false) + + { poolInsert( &expr::NodeValue::s_null ); } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index cbe4e718a..9f1063715 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -141,6 +141,8 @@ private: /** Decrement ref counts of children */ inline void decrRefCounts(); + bool isBeingDeleted() const; + public: template @@ -266,6 +268,9 @@ inline void NodeValue::decrRefCounts() { } inline void NodeValue::inc() { + Assert(!isBeingDeleted(), + "NodeValue is currently being deleted " + "and increment is being called on it. Don't Do That!"); // FIXME multithreading if(EXPECT_TRUE( d_rc < MAX_RC )) { ++d_rc; @@ -301,6 +306,13 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const { return d_children + d_nchildren; } + +inline bool NodeValue::isBeingDeleted() const +{ + return NodeManager::currentNM() != NULL && + NodeManager::currentNM()->isCurrentlyDeleting(this); +} + }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h index 199b09164..248e1e545 100644 --- a/src/theory/uf/ecdata.h +++ b/src/theory/uf/ecdata.h @@ -175,6 +175,8 @@ public: */ ECData(context::Context* context, TNode n); + ~ECData() { Debug("ufgc") << "Calling ECData destructor" << std::endl;} + /** * An ECData takes over the watch list of another ECData. * This is the second step in the union operator for ECData. -- 2.30.2