diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 10 | ||||
-rw-r--r-- | src/expr/node.h | 177 | ||||
-rw-r--r-- | src/expr/node_manager.cpp | 4 | ||||
-rw-r--r-- | src/expr/node_manager.h | 30 | ||||
-rw-r--r-- | src/main/main.cpp | 3 |
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; |