Adding NodeManager::prepareToBeDestroyed() (Fixes: #128)

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 03a54d49b24a84efe8eb2bf6ec04617ccd197c84..6fd33113b297ceef5a00223b0d40722b29cc4c41 100644 (file)
--- 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 16d1b4534c302bcd30af31ae0f0a681e1d7d4c57..323f2146959d7cc7ce527ed50009a2f0744b8b53 100644 (file)
--- 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 171c751865e185c5106873ecfd2f766aa4ec2088..6c97854132f17be25259fbf9fee1fb3e39176eb2 100644 (file)
--- 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 fcfca5296a32e7361159a7481206f8314694f9b2..35e73842e1ab91a4b959fafd7144c0dd0fe7fb31 100644 (file)
--- 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
+   * <code>d_inDestruction</code> by calling
+   * <code>prepareToBeDestroyed</code>.
    */
   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
+   * <code>prepareToBeDestroyed()</code> 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 a16db24112f65fdecfe73a3af7316f09f27c1d96..6be992479696ece5574268f7b1682a71ee0318f3 100644 (file)
--- 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 dc046429a40a4dc66c5dd3077c4fa1996b54fa33..e0061dcd9452dce688ad91558b2508bd7918d435 100644 (file)
--- 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 \