From cf4d347cbbbb4c1a1e1db99337cfd2b22b84b756 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Mon, 8 Mar 2010 23:49:47 +0000 Subject: This fixes regressions at levels >= 1 which were failing * implement zombification and garbage collection of NodeValues (but GC not turned on yet) * implement removal of key nodes from all attribute tables * audit NodeBuilder and fix memory leaks and improper reference-count management. This is in many places a re-write. Clearly documented invariants on NodeBuilder state. (Closes Bug 38) * created a "BackedNodeBuilder" that can be used to construct NodeBuilders with a stack-based backing store for a size that's not a compile-time constant. * NodeValues no longer depend on Node for toStream()'ing * make unit test-building "silent" with --enable-silent-rules * (Makefile.am, Makefile.builds.in) fix top-level build system so that "make regressN" works with unbuilt/out-of-date source trees in the expected way. * (various) code cleanup, documentation, formatting --- src/expr/node_manager.h | 130 ++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 110 insertions(+), 20 deletions(-) (limited to 'src/expr/node_manager.h') diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index c4f54727a..32c1cd210 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -28,6 +28,7 @@ #include "expr/kind.h" #include "expr/expr.h" +#include "expr/node_value.h" #include "context/context.h" namespace CVC4 { @@ -50,31 +51,65 @@ typedef Attribute TypeAttr; class NodeManager { static __thread NodeManager* s_current; - template friend class CVC4::NodeBuilder; + template friend class CVC4::NodeBuilderBase; typedef __gnu_cxx::hash_set NodeValueSet; + typedef __gnu_cxx::hash_set ZombieSet; + NodeValueSet d_nodeValueSet; expr::attr::AttributeManager d_attrManager; expr::NodeValue* poolLookup(expr::NodeValue* nv) const; void poolInsert(expr::NodeValue* nv); + void poolRemove(expr::NodeValue* nv); friend class NodeManagerScope; friend class expr::NodeValue; - std::vector d_zombieList; + bool d_reclaiming; + ZombieSet d_zombies; + /** + * Register a NodeValue as a zombie. + */ inline void gc(expr::NodeValue* nv) { Assert(nv->d_rc == 0); - d_zombieList.push_back(nv); + if(d_reclaiming) {// FIXME multithreading + // currently reclaiming zombies; just push onto the list + Debug("gc") << "zombifying node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() + << " [CURRENTLY-RECLAIMING]\n"; + d_zombies.insert(nv);// FIXME multithreading + } else { + Debug("gc") << "zombifying node value " << nv + << " [" << nv->d_id << "]: " << nv->toString() << "\n"; + d_zombies.insert(nv);// FIXME multithreading + + // for now, collect eagerly. can add heuristic here later.. + reclaimZombies(); + } } + /** + * Reclaim all zombies. + */ + void reclaimZombies(); + + /** + * Reclaim a particular zombie. + */ + void reclaimZombie(expr::NodeValue* nv); + public: - NodeManager(context::Context* ctxt) : d_attrManager(ctxt) { + NodeManager(context::Context* ctxt) : + d_attrManager(ctxt), + d_reclaiming(false) { poolInsert( &expr::NodeValue::s_null ); } @@ -95,6 +130,29 @@ public: Node mkVar(const Type* type); Node mkVar(); + template + inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv, + const AttrKind&) const; + + // Note that there are two, distinct hasAttribute() declarations for + // a reason (rather than using a pointer-valued argument with a + // default value): they permit more optimized code in the underlying + // hasAttribute() implementations. + + template + inline bool hasAttribute(expr::NodeValue* nv, + const AttrKind&) const; + + template + inline bool hasAttribute(expr::NodeValue* nv, + const AttrKind&, + typename AttrKind::value_type&) const; + + template + inline void setAttribute(expr::NodeValue* nv, + const AttrKind&, + const typename AttrKind::value_type& value); + template inline typename AttrKind::value_type getAttribute(TNode n, const AttrKind&) const; @@ -118,7 +176,6 @@ public: const AttrKind&, const typename AttrKind::value_type& value); - /** Get the type for booleans. */ inline const BooleanType* booleanType() const { return BooleanType::getInstance(); @@ -131,16 +188,16 @@ public: /** Make a function type from domain to range. */ inline const FunctionType* - mkFunctionType(const Type* domain, const Type* range); + mkFunctionType(const Type* domain, const Type* range) const; /** Make a function type with input types from argTypes. */ inline const FunctionType* - mkFunctionType(const std::vector& argTypes, const Type* range); + mkFunctionType(const std::vector& argTypes, const Type* range) const; /** Make a new sort with the given name. */ - inline const Type* mkSort(const std::string& name); + inline const Type* mkSort(const std::string& name) const; - inline const Type* getType(TNode n); + inline const Type* getType(TNode n) const; }; /** @@ -202,37 +259,63 @@ public: } }; +template +inline typename AttrKind::value_type NodeManager::getAttribute(expr::NodeValue* nv, + const AttrKind&) const { + return d_attrManager.getAttribute(nv, AttrKind()); +} + +template +inline bool NodeManager::hasAttribute(expr::NodeValue* nv, + const AttrKind&) const { + return d_attrManager.hasAttribute(nv, AttrKind()); +} + +template +inline bool NodeManager::hasAttribute(expr::NodeValue* nv, + const AttrKind&, + typename AttrKind::value_type& ret) const { + return d_attrManager.hasAttribute(nv, AttrKind(), ret); +} + +template +inline void NodeManager::setAttribute(expr::NodeValue* nv, + const AttrKind&, + const typename AttrKind::value_type& value) { + d_attrManager.setAttribute(nv, AttrKind(), value); +} + template inline typename AttrKind::value_type NodeManager::getAttribute(TNode n, const AttrKind&) const { - return d_attrManager.getAttribute(n, AttrKind()); + return d_attrManager.getAttribute(n.d_nv, AttrKind()); } template inline bool NodeManager::hasAttribute(TNode n, const AttrKind&) const { - return d_attrManager.hasAttribute(n, AttrKind()); + return d_attrManager.hasAttribute(n.d_nv, AttrKind()); } template inline bool NodeManager::hasAttribute(TNode n, const AttrKind&, typename AttrKind::value_type& ret) const { - return d_attrManager.hasAttribute(n, AttrKind(), ret); + return d_attrManager.hasAttribute(n.d_nv, AttrKind(), ret); } template inline void NodeManager::setAttribute(TNode n, const AttrKind&, const typename AttrKind::value_type& value) { - d_attrManager.setAttribute(n, AttrKind(), value); + d_attrManager.setAttribute(n.d_nv, AttrKind(), value); } /** Make a function type from domain to range. - * TODO: Function types should be unique for this manager. */ + * TODO: Function types should be unique for this manager. */ const FunctionType* NodeManager::mkFunctionType(const Type* domain, - const Type* range) { + const Type* range) const { std::vector argTypes; argTypes.push_back(domain); return new FunctionType(argTypes, range); @@ -242,23 +325,29 @@ NodeManager::mkFunctionType(const Type* domain, * TODO: Function types should be unique for this manager. */ const FunctionType* NodeManager::mkFunctionType(const std::vector& argTypes, - const Type* range) { + const Type* range) const { Assert( argTypes.size() > 0 ); return new FunctionType(argTypes, range); } const Type* -NodeManager::mkSort(const std::string& name) { +NodeManager::mkSort(const std::string& name) const { return new SortType(name); } -inline const Type* NodeManager::getType(TNode n) { +inline const Type* NodeManager::getType(TNode n) const { return getAttribute(n, CVC4::expr::TypeAttr()); } inline void NodeManager::poolInsert(expr::NodeValue* nv) { Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), "NodeValue already in the pool!"); - d_nodeValueSet.insert(nv); + d_nodeValueSet.insert(nv);// FIXME multithreading +} + +inline void NodeManager::poolRemove(expr::NodeValue* nv) { + Assert(d_nodeValueSet.find(nv) != d_nodeValueSet.end(), + "NodeValue is not in the pool!"); + d_nodeValueSet.erase(nv);// FIXME multithreading } }/* CVC4 namespace */ @@ -305,12 +394,13 @@ inline Node NodeManager::mkVar(const Type* type, const std::string& name) { } inline Node NodeManager::mkVar(const Type* type) { - Node n = NodeBuilder<>(this, kind::VARIABLE); + Node n = mkVar(); n.setAttribute(expr::TypeAttr(), type); return n; } inline Node NodeManager::mkVar() { + // TODO: rewrite to not use NodeBuilder return NodeBuilder<>(this, kind::VARIABLE); } -- cgit v1.2.3