From: Morgan Deters Date: Tue, 21 Sep 2010 22:40:50 +0000 (+0000) Subject: remove assertion in TNode destructor and ensure all TNode methods check rc > 0 (resol... X-Git-Tag: cvc5-1.0.0~8855 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=818d7fc74583965e87c35360c2fed890844efbba;p=cvc5.git remove assertion in TNode destructor and ensure all TNode methods check rc > 0 (resolves bug #200); on NodeManager/ExprManager side, no more prepareToBeDestroyed() / inDestruction --- 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 operator==(const NodeTemplate& node) const { + assertTNodeNotExpired(); + node.assertTNodeNotExpired(); return d_nv == node.d_nv; } @@ -231,6 +240,8 @@ public: */ template bool operator!=(const NodeTemplate& node) const { + assertTNodeNotExpired(); + node.assertTNodeNotExpired(); return d_nv != node.d_nv; } @@ -242,6 +253,8 @@ public: */ template inline bool operator<(const NodeTemplate& node) const { + assertTNodeNotExpired(); + node.assertTNodeNotExpired(); return d_nv->d_id < node.d_nv->d_id; } @@ -253,6 +266,8 @@ public: */ template inline bool operator>(const NodeTemplate& node) const { + assertTNodeNotExpired(); + node.assertTNodeNotExpired(); return d_nv->d_id > node.d_nv->d_id; } @@ -264,6 +279,8 @@ public: */ template inline bool operator<=(const NodeTemplate& node) const { + assertTNodeNotExpired(); + node.assertTNodeNotExpired(); return d_nv->d_id <= node.d_nv->d_id; } @@ -275,6 +292,8 @@ public: */ template inline bool operator>=(const NodeTemplate& 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 >(); } @@ -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 >(); } @@ -479,10 +486,7 @@ public: */ template inline iterator begin() { - if(!ref_count) { - Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" ); - } - + assertTNodeNotExpired(); return d_nv->begin< NodeTemplate, kind >(); } @@ -499,10 +503,7 @@ public: */ template inline iterator end() { - if(!ref_count) { - Assert( d_nv->d_rc > 0, "TNode pointing to an expired NodeValue" ); - } - + assertTNodeNotExpired(); return d_nv->end< NodeTemplate, 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 >(); } @@ -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 >(); } @@ -538,10 +533,7 @@ public: */ template 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, kind >(); } @@ -552,10 +544,7 @@ public: */ template 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, 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 inline size_t NodeTemplate::getNumChildren() const { + assertTNodeNotExpired(); return d_nv->getNumChildren(); } template template inline const T& NodeTemplate::getConst() const { + assertTNodeNotExpired(); return d_nv->getConst(); } @@ -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::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::NodeTemplate(const NodeTemplate& 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::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 NodeTemplate::~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& 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& e) { template NodeTemplate NodeTemplate::eqNode(const NodeTemplate& 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 NodeTemplate NodeTemplate::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 NodeTemplate NodeTemplate::andNode(const NodeTemplate& 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 NodeTemplate NodeTemplate::orNode(const NodeTemplate& 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 NodeTemplate NodeTemplate::iteNode(const NodeTemplate& thenpart, const NodeTemplate& 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 NodeTemplate NodeTemplate::iffNode(const NodeTemplate& 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 NodeTemplate NodeTemplate::impNode(const NodeTemplate& 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 NodeTemplate NodeTemplate::xorNode(const NodeTemplate& 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 inline void NodeTemplate::printAst(std::ostream& out, int indent) const { + assertTNodeNotExpired(); d_nv->printAst(out, indent); } @@ -943,9 +905,7 @@ NodeTemplate NodeTemplate::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 NodeTemplate::getOperator() const { */ template inline bool NodeTemplate::hasOperator() const { + assertTNodeNotExpired(); return NodeManager::hasOperator(getKind()); } @@ -987,9 +948,7 @@ TypeNode NodeTemplate::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 @@ -97,19 +97,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 - * d_inDestruction by calling - * prepareToBeDestroyed. - */ - 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 @@ -248,23 +235,6 @@ public: NodeManager(context::Context* ctxt); ~NodeManager(); - /** - * 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 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;