remove assertion in TNode destructor and ensure all TNode methods check rc > 0 (resolves bug #200); on NodeManager/ExprManager side, no more prepareToBeDestroyed() / inDestruction

6 files changed, 69 insertions, 159 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 1eabc9f8a..04ebfa94f 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -398,10 +398,6 @@ 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 ab7aeace1..aaaaf0026 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -240,16 +240,6 @@ 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.h b/src/expr/node.h
index 91c5bb21b..4f306bcff 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -156,6 +156,12 @@ class NodeTemplate {
    */
   void assignNodeValue(expr::NodeValue* ev);
 
+  inline void assertTNodeNotExpired() const throw(AssertionException) {
+    if(!ref_count) {
+      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
+    }
+  }
+
 public:
 
   /** Default constructor, makes a null expression. */
@@ -211,6 +217,7 @@ public:
    * @return true if null
    */
   bool isNull() const {
+    assertTNodeNotExpired();
     return d_nv == &expr::NodeValue::s_null;
   }
 
@@ -221,6 +228,8 @@ public:
    */
   template <bool ref_count_1>
   bool operator==(const NodeTemplate<ref_count_1>& node) const {
+    assertTNodeNotExpired();
+    node.assertTNodeNotExpired();
     return d_nv == node.d_nv;
   }
 
@@ -231,6 +240,8 @@ public:
    */
   template <bool ref_count_1>
   bool operator!=(const NodeTemplate<ref_count_1>& node) const {
+    assertTNodeNotExpired();
+    node.assertTNodeNotExpired();
     return d_nv != node.d_nv;
   }
 
@@ -242,6 +253,8 @@ public:
    */
   template <bool ref_count_1>
   inline bool operator<(const NodeTemplate<ref_count_1>& node) const {
+    assertTNodeNotExpired();
+    node.assertTNodeNotExpired();
     return d_nv->d_id < node.d_nv->d_id;
   }
 
@@ -253,6 +266,8 @@ public:
    */
   template <bool ref_count_1>
   inline bool operator>(const NodeTemplate<ref_count_1>& node) const {
+    assertTNodeNotExpired();
+    node.assertTNodeNotExpired();
     return d_nv->d_id > node.d_nv->d_id;
   }
 
@@ -264,6 +279,8 @@ public:
    */
   template <bool ref_count_1>
   inline bool operator<=(const NodeTemplate<ref_count_1>& node) const {
+    assertTNodeNotExpired();
+    node.assertTNodeNotExpired();
     return d_nv->d_id <= node.d_nv->d_id;
   }
 
@@ -275,6 +292,8 @@ public:
    */
   template <bool ref_count_1>
   inline bool operator>=(const NodeTemplate<ref_count_1>& node) const {
+    assertTNodeNotExpired();
+    node.assertTNodeNotExpired();
     return d_nv->d_id >= node.d_nv->d_id;
   }
 
@@ -284,9 +303,7 @@ public:
    * @return the node representing the i-th child
    */
   NodeTemplate operator[](int i) const {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
+    assertTNodeNotExpired();
     return NodeTemplate(d_nv->getChild(i));
   }
 
@@ -309,6 +326,7 @@ public:
    * @return true if const
    */
   inline bool isConst() const {
+    assertTNodeNotExpired();
     return getMetaKind() == kind::metakind::CONSTANT;
   }
 
@@ -317,10 +335,7 @@ public:
    * @return the ud
    */
   unsigned getId() const {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
-
+    assertTNodeNotExpired();
     return d_nv->getId();
   }
 
@@ -366,10 +381,7 @@ public:
    * @return the kind
    */
   inline Kind getKind() const {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
-
+    assertTNodeNotExpired();
     return Kind(d_nv->d_kind);
   }
 
@@ -378,6 +390,7 @@ public:
    * @return the metakind
    */
   inline kind::MetaKind getMetaKind() const {
+    assertTNodeNotExpired();
     return kind::metaKindOf(getKind());
   }
 
@@ -447,10 +460,7 @@ public:
    * @return the iterator
    */
   inline iterator begin() {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
-
+    assertTNodeNotExpired();
     return d_nv->begin< NodeTemplate<ref_count> >();
   }
 
@@ -460,10 +470,7 @@ public:
    * @return the end of the children iterator.
    */
   inline iterator end() {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
-
+    assertTNodeNotExpired();
     return d_nv->end< NodeTemplate<ref_count> >();
   }
 
@@ -479,10 +486,7 @@ public:
    */
   template <Kind kind>
   inline iterator begin() {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
-
+    assertTNodeNotExpired();
     return d_nv->begin< NodeTemplate<ref_count>, kind >();
   }
 
@@ -499,10 +503,7 @@ public:
    */
   template <Kind kind>
   inline iterator end() {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
-
+    assertTNodeNotExpired();
     return d_nv->end< NodeTemplate<ref_count>, kind >();
   }
 
@@ -512,10 +513,7 @@ public:
    * @return the const_iterator
    */
   inline const_iterator begin() const {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
-
+    assertTNodeNotExpired();
     return d_nv->begin< NodeTemplate<ref_count> >();
   }
 
@@ -525,10 +523,7 @@ public:
    * @return the end of the children const_iterator.
    */
   inline const_iterator end() const {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
-
+    assertTNodeNotExpired();
     return d_nv->end< NodeTemplate<ref_count> >();
   }
 
@@ -538,10 +533,7 @@ public:
    */
   template <Kind kind>
   inline const_iterator begin() const {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
-
+    assertTNodeNotExpired();
     return d_nv->begin< NodeTemplate<ref_count>, kind >();
   }
 
@@ -552,10 +544,7 @@ public:
    */
   template <Kind kind>
   inline const_iterator end() const {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
-
+    assertTNodeNotExpired();
     return d_nv->end< NodeTemplate<ref_count>, kind >();
   }
 
@@ -564,10 +553,7 @@ public:
    * @return the string representation of this node.
    */
   inline std::string toString() const {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
-
+    assertTNodeNotExpired();
     return d_nv->toString();
   }
 
@@ -578,10 +564,7 @@ public:
    */
   inline void toStream(std::ostream& out, int toDepth = -1,
                        bool types = false) const {
-    if(!ref_count) {
-      Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-    }
-
+    assertTNodeNotExpired();
     d_nv->toStream(out, toDepth, types);
   }
 
@@ -670,12 +653,14 @@ struct TNodeHashFunction {
 
 template <bool ref_count>
 inline size_t NodeTemplate<ref_count>::getNumChildren() const {
+  assertTNodeNotExpired();
   return d_nv->getNumChildren();
 }
 
 template <bool ref_count>
 template <class T>
 inline const T& NodeTemplate<ref_count>::getConst() const {
+  assertTNodeNotExpired();
   return d_nv->getConst<T>();
 }
 
@@ -687,9 +672,7 @@ getAttribute(const AttrKind&) const {
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
+  assertTNodeNotExpired();
 
   return NodeManager::currentNM()->getAttribute(*this, AttrKind());
 }
@@ -702,9 +685,7 @@ hasAttribute(const AttrKind&) const {
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
+  assertTNodeNotExpired();
 
   return NodeManager::currentNM()->hasAttribute(*this, AttrKind());
 }
@@ -717,9 +698,7 @@ inline bool NodeTemplate<ref_count>::getAttribute(const AttrKind&,
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
+  assertTNodeNotExpired();
 
   return NodeManager::currentNM()->getAttribute(*this, AttrKind(), ret);
 }
@@ -732,9 +711,7 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
+  assertTNodeNotExpired();
 
   NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
 }
@@ -766,11 +743,11 @@ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e) {
   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
   d_nv = e.d_nv;
   if(ref_count) {
+    Assert(d_nv->d_rc > 0, "Node constructed from TNode with rc == 0");
     d_nv->inc();
   } else {
-    // shouldn't ever happen
-    Assert(d_nv->d_rc > 0,
-           "TNode constructed from Node with rc == 0");
+    // shouldn't ever fail
+    Assert(d_nv->d_rc > 0, "TNode constructed from Node with rc == 0");
   }
 }
 
@@ -779,6 +756,8 @@ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
   d_nv = e.d_nv;
   if(ref_count) {
+    // shouldn't ever fail
+    Assert(d_nv->d_rc > 0, "Node constructed from Node with rc == 0");
     d_nv->inc();
   } else {
     Assert(d_nv->d_rc > 0, "TNode constructed from TNode with rc == 0");
@@ -789,10 +768,9 @@ template <bool ref_count>
 NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) {
   Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
   if(ref_count) {
+    // shouldn't ever fail
+    Assert(d_nv->d_rc > 0, "Node reference count would be negative");
     d_nv->dec();
-  } else {
-    Assert(d_nv->d_rc > 0 || d_nv->isBeingDeleted() || NodeManager::currentNM()->inDestruction(),
-           "TNode pointing to an expired NodeValue at destruction time");
   }
 }
 
@@ -813,10 +791,15 @@ operator=(const NodeTemplate& e) {
   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
   if(EXPECT_TRUE( d_nv != e.d_nv )) {
     if(ref_count) {
+      // shouldn't ever fail
+      Assert(d_nv->d_rc > 0,
+             "Node reference count would be negative");
       d_nv->dec();
     }
     d_nv = e.d_nv;
     if(ref_count) {
+      // shouldn't ever fail
+      Assert(d_nv->d_rc > 0, "Node assigned from Node with rc == 0");
       d_nv->inc();
     } else {
       Assert(d_nv->d_rc > 0, "TNode assigned from TNode with rc == 0");
@@ -832,15 +815,17 @@ operator=(const NodeTemplate<!ref_count>& e) {
   Assert(e.d_nv != NULL, "Expecting a non-NULL expression value on RHS!");
   if(EXPECT_TRUE( d_nv != e.d_nv )) {
     if(ref_count) {
+      // shouldn't ever fail
+      Assert(d_nv->d_rc > 0, "Node reference count would be negative");
       d_nv->dec();
     }
     d_nv = e.d_nv;
     if(ref_count) {
+      Assert(d_nv->d_rc > 0, "Node assigned from TNode with rc == 0");
       d_nv->inc();
     } else {
       // shouldn't ever happen
-      Assert(d_nv->d_rc > 0,
-             "TNode assigned from Node with rc == 0");
+      Assert(d_nv->d_rc > 0, "TNode assigned from Node with rc == 0");
     }
   }
   return *this;
@@ -849,39 +834,27 @@ operator=(const NodeTemplate<!ref_count>& e) {
 template <bool ref_count>
 NodeTemplate<true>
 NodeTemplate<ref_count>::eqNode(const NodeTemplate<ref_count>& right) const {
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
-
+  assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
 }
 
 template <bool ref_count>
 NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
-
+  assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::NOT, *this);
 }
 
 template <bool ref_count>
 NodeTemplate<true>
 NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count>& right) const {
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
-
+  assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
 }
 
 template <bool ref_count>
 NodeTemplate<true>
 NodeTemplate<ref_count>::orNode(const NodeTemplate<ref_count>& right) const {
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
-
+  assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
 }
 
@@ -889,46 +862,35 @@ template <bool ref_count>
 NodeTemplate<true>
 NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count>& thenpart,
                                  const NodeTemplate<ref_count>& elsepart) const {
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
-
+  assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
 }
 
 template <bool ref_count>
 NodeTemplate<true>
 NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count>& right) const {
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
-
+  assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
 }
 
 template <bool ref_count>
 NodeTemplate<true>
 NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count>& right) const {
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
-
+  assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
 }
 
 template <bool ref_count>
 NodeTemplate<true>
 NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count>& right) const {
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
-
+  assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
 }
 
 template <bool ref_count>
 inline void
 NodeTemplate<ref_count>::printAst(std::ostream& out, int indent) const {
+  assertTNodeNotExpired();
   d_nv->printAst(out, indent);
 }
 
@@ -943,9 +905,7 @@ NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
+  assertTNodeNotExpired();
 
   switch(kind::MetaKind mk = getMetaKind()) {
   case kind::metakind::INVALID:
@@ -977,6 +937,7 @@ NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
  */
 template <bool ref_count>
 inline bool NodeTemplate<ref_count>::hasOperator() const {
+  assertTNodeNotExpired();
   return NodeManager::hasOperator(getKind());
 }
 
@@ -987,9 +948,7 @@ TypeNode NodeTemplate<ref_count>::getType(bool check) const
           "There is no current CVC4::NodeManager associated to this thread.\n"
           "Perhaps a public-facing function is missing a NodeManagerScope ?" );
 
-  if(!ref_count) {
-    Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" );
-  }
+  assertTNodeNotExpired();
 
   return NodeManager::currentNM()->getType(*this, check);
 }
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index b7bbe2ff8..1f15f7e29 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -84,8 +84,7 @@ struct NVReclaim {
 NodeManager::NodeManager(context::Context* ctxt) :
   d_attrManager(ctxt),
   d_nodeUnderDeletion(NULL),
-  d_inReclaimZombies(false),
-  d_inDestruction(false) {
+  d_inReclaimZombies(false) {
   poolInsert( &expr::NodeValue::s_null );
 
   for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
@@ -102,7 +101,6 @@ NodeManager::~NodeManager() {
   // destruction of operators, because they get GCed.
 
   NodeManagerScope nms(this);
-  d_inDestruction = true;
 
   {
     ScopedBool dontGC(d_inReclaimZombies);
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index ab727a627..bf1bed5f0 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -98,19 +98,6 @@ class NodeManager {
   bool d_inReclaimZombies;
 
   /**
-   * 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;
-
-  /**
    * The set of zombie nodes.  We may want to revisit this design, as
    * we might like to delete nodes in least-recently-used order.  But
    * we also need to avoid processing a zombie twice.
@@ -248,23 +235,6 @@ public:
   NodeManager(context::Context* ctxt);
   ~NodeManager();
 
-  /**
-   * 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 a6fe10888..950e991c6 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -209,9 +209,6 @@ int runCvc4(int argc, char* argv[]) {
   exit(returnValue);
 #endif
 
-  // Get ready for tear-down
-  exprMgr.prepareToBeDestroyed();
-
   // Remove the parser
   delete parser;