diff options
author | Tim King <taking@google.com> | 2016-11-10 15:22:49 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2016-11-10 15:22:49 -0800 |
commit | 16e809f698060645812667925b3e0c4d403ee71a (patch) | |
tree | 6952e767825c1d99166e1308c39aece2cc9c33c9 /src/expr/node_value.h | |
parent | 13be3be39454a3cf7b05c4399a53bd2dd27996f6 (diff) |
Adding garbage collection of nodes with maxed out reference counts.
Diffstat (limited to 'src/expr/node_value.h')
-rw-r--r-- | src/expr/node_value.h | 27 |
1 files changed, 22 insertions, 5 deletions
diff --git a/src/expr/node_value.h b/src/expr/node_value.h index b403d0c86..8f1df0fff 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -122,6 +122,9 @@ class NodeValue { void inc(); void dec(); + // Returns true if the reference count is maximized. + inline bool HasMaximizedReferenceCount() { return d_rc == MAX_RC; } + /** * Uninitializing constructor for NodeBuilder's use. */ @@ -294,14 +297,20 @@ public: private: + /** + * RAII guard that increases the reference count if the reference count to be > 0. + * Otherwise, this does nothing. This does not just increment the reference + * count to avoid maxing out the d_rc field. This is only for low level functions. + */ class RefCountGuard { NodeValue* d_nv; + bool d_increased; public: RefCountGuard(const NodeValue* nv) : d_nv(const_cast<NodeValue*>(nv)) { - // inc() - if(__builtin_expect( ( d_nv->d_rc < MAX_RC ), true )) { - ++d_nv->d_rc; + d_increased = (d_nv->d_rc == 0); + if(d_increased) { + d_nv->d_rc = 1; } } ~RefCountGuard() { @@ -310,7 +319,7 @@ private: // E.g., this can happen when debugging code calls the print // routines below. As RefCountGuards are scoped on the stack, // this should be fine---but not in multithreaded contexts! - if(__builtin_expect( ( d_nv->d_rc < MAX_RC ), true )) { + if(d_increased) { --d_nv->d_rc; } } @@ -415,6 +424,13 @@ inline void NodeValue::inc() { // FIXME multithreading if(__builtin_expect( ( d_rc < MAX_RC ), true )) { ++d_rc; + if(__builtin_expect( ( d_rc == MAX_RC ), false )) { + Assert(NodeManager::currentNM() != NULL, + "No current NodeManager on incrementing of NodeValue: " + "maybe a public CVC4 interface function is missing a " + "NodeManagerScope ?"); + NodeManager::currentNM()->markRefCountMaxedOut(this); + } } } @@ -425,7 +441,8 @@ inline void NodeValue::dec() { if(__builtin_expect( ( d_rc == 0 ), false )) { Assert(NodeManager::currentNM() != NULL, "No current NodeManager on destruction of NodeValue: " - "maybe a public CVC4 interface function is missing a NodeManagerScope ?"); + "maybe a public CVC4 interface function is missing a " + "NodeManagerScope ?"); NodeManager::currentNM()->markForDeletion(this); } } |