diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2018-09-12 14:58:11 +0000 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-02-19 12:05:22 +0000 |
commit | 9cfa329a77d3dfec4746ca307c6da1b3e904cbfa (patch) | |
tree | c9379a0ab0b5afdf740fae0a01c67bf76d061d86 /lib/Expr/Updates.cpp | |
parent | 86ab439d589d0afb1b710ef58296d07a263092e3 (diff) | |
download | klee-9cfa329a77d3dfec4746ca307c6da1b3e904cbfa.tar.gz |
Use `ref<>` for UpdateNode
Remove additional reference counting as part of UpdateNodeList and UpdateNode. Simplifies code.
Diffstat (limited to 'lib/Expr/Updates.cpp')
-rw-r--r-- | lib/Expr/Updates.cpp | 120 |
1 files changed, 12 insertions, 108 deletions
diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp index 7264ca89..4734f592 100644 --- a/lib/Expr/Updates.cpp +++ b/lib/Expr/Updates.cpp @@ -13,13 +13,11 @@ using namespace klee; -UpdateNode::UpdateNode(const UpdateNode *_next, - const ref<Expr> &_index, - const ref<Expr> &_value) - : refCount(0), - next(_next), - index(_index), - value(_value) { +/// + +UpdateNode::UpdateNode(const ref<UpdateNode> &_next, const ref<Expr> &_index, + const ref<Expr> &_value) + : next(_next), index(_index), value(_value) { // FIXME: What we need to check here instead is that _value is of the same width // as the range of the array that the update node is part of. /* @@ -27,23 +25,11 @@ UpdateNode::UpdateNode(const UpdateNode *_next, "Update value should be 8-bit wide."); */ computeHash(); - if (next) { - ++next->refCount; - size = 1 + next->size; - } - else size = 1; + size = next.isNull() ? 1 : 1 + next->size; } extern "C" void vc_DeleteExpr(void*); -// This is deliberately empty to avoid recursively deleting UpdateNodes -// (i.e. ``if (--next->refCount==0) delete next;``). -// UpdateList manages the correct destruction of a chain UpdateNodes -// non-recursively. -UpdateNode::~UpdateNode() { - assert(refCount == 0 && "Deleted UpdateNode when a reference is still held"); -} - int UpdateNode::compare(const UpdateNode &b) const { if (int i = index.compare(b.index)) return i; @@ -52,95 +38,15 @@ int UpdateNode::compare(const UpdateNode &b) const { unsigned UpdateNode::computeHash() { hashValue = index->hash() ^ value->hash(); - if (next) + if (!next.isNull()) hashValue ^= next->hash(); return hashValue; } /// -UpdateList::UpdateList(const Array *_root, const UpdateNode *_head) - : root(_root), - head(_head) { - if (head) ++head->refCount; -} - -UpdateList::UpdateList(const UpdateList &b) - : root(b.root), - head(b.head) { - if (head) ++head->refCount; -} - -UpdateList::~UpdateList() { - tryFreeNodes(); -} - -void UpdateList::tryFreeNodes() { - // We need to be careful and avoid having the UpdateNodes recursively deleting - // themselves. This is done in cooperation with the private dtor of UpdateNode - // which does nothing. - // - // This method will free UpdateNodes that only this instance has references - // to, i.e. it will delete a continguous chain of UpdateNodes that all have - // a ``refCount`` of 1 starting at the head. - // - // In the following examples the Head0 is the head of this UpdateList instance - // and Head1 is the head of some other instance of UpdateList. - // - // [x] represents an UpdateNode where the reference count for that node is x. - // - // Example: Simple chain. - // - // [1] -> [1] -> [1] -> nullptr - // ^Head0 - // - // Result: The entire chain is freed - // - // nullptr - // ^Head0 - // - // Example: A chain where two UpdateLists share some nodes - // - // [1] -> [1] -> [2] -> [1] -> nullptr - // ^Head0 ^Head1 - // - // Result: Part of the chain is freed and the UpdateList with head Head1 - // is now the exclusive owner of the UpdateNodes. - // - // nullptr [1] -> [1] -> nullptr - // ^Head0 ^Head1 - // - // Example: A chain where two UpdateLists point at the same head - // - // [2] -> [1] -> [1] -> [1] -> nullptr - // ^Head0 - // Head1 - // - // Result: No UpdateNodes are freed but now the UpdateList with head Head1 - // is now the exclusive owner of the UpdateNodes. - // - // [1] -> [1] -> [1] -> [1] -> nullptr - // ^Head1 - // - // nullptr - // ^Head0 - // - while (head && --head->refCount==0) { - const UpdateNode *n = head->next; - delete head; - head = n; - } -} - -UpdateList &UpdateList::operator=(const UpdateList &b) { - if (b.head) ++b.head->refCount; - // Drop reference to the current head and free a chain of nodes - // if we are the only UpdateList referencing them - tryFreeNodes(); - root = b.root; - head = b.head; - return *this; -} +UpdateList::UpdateList(const Array *_root, const ref<UpdateNode> &_head) + : root(_root), head(_head) {} void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) { @@ -149,9 +55,7 @@ void UpdateList::extend(const ref<Expr> &index, const ref<Expr> &value) { assert(root->getRange() == value->getWidth()); } - if (head) --head->refCount; head = new UpdateNode(head, index, value); - ++head->refCount; } int UpdateList::compare(const UpdateList &b) const { @@ -167,8 +71,8 @@ int UpdateList::compare(const UpdateList &b) const { else if (getSize() > b.getSize()) return 1; // XXX build comparison into update, make fast - const UpdateNode *an=head, *bn=b.head; - for (; an && bn; an=an->next,bn=bn->next) { + const auto *an = head.get(), *bn = b.head.get(); + for (; an && bn; an = an->next.get(), bn = bn->next.get()) { if (an==bn) { // exploit shared list structure return 0; } else { @@ -184,7 +88,7 @@ unsigned UpdateList::hash() const { unsigned res = 0; for (unsigned i = 0, e = root->name.size(); i != e; ++i) res = (res * Expr::MAGIC_HASH_CONSTANT) + root->name[i]; - if (head) + if (head.get()) res ^= head->hash(); return res; } |