From: Christopher L. Conway Date: Thu, 27 May 2010 18:39:32 +0000 (+0000) Subject: Adding NodeManager::prepareToBeDestroyed() (Fixes: #128) X-Git-Tag: cvc5-1.0.0~9037 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eb707aa027bb2f439f250fa98fdf0ce550adb49c;p=cvc5.git Adding NodeManager::prepareToBeDestroyed() (Fixes: #128) --- diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 03a54d49b..6fd33113b 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -258,6 +258,10 @@ unsigned ExprManager::maxArity(Kind kind) { return metakind::getUpperBoundForKind(kind); } +void ExprManager::prepareToBeDestroyed() { + d_nodeManager->prepareToBeDestroyed(); +} + NodeManager* ExprManager::getNodeManager() const { return d_nodeManager; } diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 16d1b4534..323f21469 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -220,6 +220,15 @@ public: /** Returns the maximum arity of the given kind. */ static unsigned maxArity(Kind kind); + + /** Signals that this expression manager will soon be destroyed. + * Turns off debugging assertions that may not hold as the system + * is being torn down. + * + * NOTE: It is *not* required to call this function before destroying + * the ExprManager. + */ + void prepareToBeDestroyed(); }; ${mkConst_instantiations} diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 171c75186..6c9785413 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -34,21 +34,22 @@ namespace CVC4 { __thread NodeManager* NodeManager::s_current = 0; /** - * This class ensures that NodeManager::d_reclaiming gets set to false - * even on exceptional exit from NodeManager::reclaimZombies(). + * This class sets it reference argument to true and ensures that it gets set + * to false on destruction. This can be used to make sure a flag gets toggled + * in a function even on exceptional exit (e.g., see reclaimZombies()). */ struct ScopedBool { bool& d_value; - ScopedBool(bool& reclaim) : - d_value(reclaim) { + ScopedBool(bool& value) : + d_value(value) { - Debug("gc") << ">> setting RECLAIM field\n"; + Debug("gc") << ">> setting ScopedBool\n"; d_value = true; } ~ScopedBool() { - Debug("gc") << "<< clearing RECLAIM field\n"; + Debug("gc") << "<< clearing ScopedBool\n"; d_value = false; } }; @@ -76,7 +77,7 @@ struct NVReclaim { NodeManager::NodeManager(context::Context* ctxt) : d_attrManager(ctxt), d_nodeUnderDeletion(NULL), - d_dontGC(false), + d_inReclaimZombies(false), d_inDestruction(false) { poolInsert( &expr::NodeValue::s_null ); @@ -94,10 +95,10 @@ NodeManager::~NodeManager() { // destruction of operators, because they get GCed. NodeManagerScope nms(this); - ScopedBool inDestruction(d_inDestruction); + d_inDestruction = true; { - ScopedBool dontGC(d_dontGC); + ScopedBool dontGC(d_inReclaimZombies); d_attrManager.deleteAllAttributes(); } @@ -118,11 +119,11 @@ void NodeManager::reclaimZombies() { Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n"; // during reclamation, reclaimZombies() is never supposed to be called - Assert(! d_dontGC, "NodeManager::reclaimZombies() not re-entrant!"); + Assert(! d_inReclaimZombies, "NodeManager::reclaimZombies() not re-entrant!"); // whether exit is normal or exceptional, the Reclaim dtor is called - // and ensures that d_reclaiming is set back to false. - ScopedBool r(d_dontGC); + // and ensures that d_inReclaimZombies is set back to false. + ScopedBool r(d_inReclaimZombies); // We copy the set away and clear the NodeManager's set of zombies. // This is because reclaimZombie() decrements the RC of the diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index fcfca5296..35e73842e 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -86,10 +86,18 @@ class NodeManager { * NodeValues, but these shouldn't trigger a (recursive) call to * reclaimZombies(). */ - bool d_dontGC; + bool d_inReclaimZombies; /** - * Marks that we are in the Destructor currently. + * Indicates that the NodeManager is in the process of being destroyed. + * The main purpose of this is to disable certain debugging assertions + * that might be sensitive to the order in which objects get cleaned up + * (e.g., TNode-valued attributes that outlive their associated Node). + * This may be true before or after the actual NodeManager destructor + * is executing, while other associated cleanup procedures run. E.g., + * an object that contains a NodeManager can set + * d_inDestruction by calling + * prepareToBeDestroyed. */ bool d_inDestruction; @@ -169,11 +177,11 @@ class NodeManager { // reclaimZombies(), because it's already running. Debug("gc") << "zombifying node value " << nv << " [" << nv->d_id << "]: " << *nv - << (d_dontGC ? " [CURRENTLY-RECLAIMING]" : "") + << (d_inReclaimZombies ? " [CURRENTLY-RECLAIMING]" : "") << std::endl; d_zombies.insert(nv);// FIXME multithreading - if(!d_dontGC) {// FIXME multithreading + if(!d_inReclaimZombies) {// FIXME multithreading // for now, collect eagerly. can add heuristic here later.. reclaimZombies(); } @@ -243,10 +251,22 @@ public: ~NodeManager(); /** - * Return true if we are in destruction. + * Return true if the destructor has been invoked, or + * prepareToBeDestroyed() has previously been called. */ bool inDestruction() const { return d_inDestruction; } + /** Signals that this expression manager will soon be destroyed. + * Turns off debugging assertions that may not hold as the system + * is being torn down. + * + * NOTE: It is *not* required to call this function before destroying + * the NodeManager. + */ + void prepareToBeDestroyed() { + d_inDestruction = true; + } + /** The node manager in the current context. */ static NodeManager* currentNM() { return s_current; } diff --git a/src/main/main.cpp b/src/main/main.cpp index a16db2411..6be992479 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -168,6 +168,9 @@ int runCvc4(int argc, char* argv[]) { delete cmd; } + // Get ready for tear-down + exprMgr.prepareToBeDestroyed(); + // Remove the parser delete parser; @@ -183,6 +186,7 @@ int runCvc4(int argc, char* argv[]) { return 0; } + } void doCommand(SmtEngine& smt, Command* cmd) { diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index dc046429a..e0061dcd9 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -10,6 +10,7 @@ TESTS = \ distinct.smt \ flet.smt \ flet2.smt \ + ite_real_int_type.smt \ let.smt \ let2.smt \ simple2.smt \