From 9cfa329a77d3dfec4746ca307c6da1b3e904cbfa Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Wed, 12 Sep 2018 14:58:11 +0000 Subject: Use `ref<>` for UpdateNode Remove additional reference counting as part of UpdateNodeList and UpdateNode. Simplifies code. --- lib/Solver/FastCexSolver.cpp | 4 ++-- lib/Solver/IndependentSolver.cpp | 3 +-- lib/Solver/STPBuilder.cpp | 17 ++++++++--------- lib/Solver/Z3Builder.cpp | 4 ++-- 4 files changed, 13 insertions(+), 15 deletions(-) (limited to 'lib/Solver') diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 3e1162fd..722f624f 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -804,8 +804,8 @@ public: const Array *array = re->updates.root; CexObjectData &cod = getObjectData(array); CexValueData index = evalRangeForExpr(re->index); - - for (const UpdateNode *un = re->updates.head; un; un = un->next) { + + for (const auto *un = re->updates.head.get(); un; un = un->next.get()) { CexValueData ui = evalRangeForExpr(un->index); // If these indices can't alias, continue propogation diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 7beb1a7c..cd59c741 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -120,8 +120,7 @@ public: const Array *array = re->updates.root; // Reads of a constant array don't alias. - if (re->updates.root->isConstantArray() && - !re->updates.head) + if (re->updates.root->isConstantArray() && re->updates.head.isNull()) continue; if (!wholeObjects.count(array)) { diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index ef6697ef..5857e6f0 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -480,12 +480,11 @@ ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) { bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr); if (!hashed) { - un_expr = vc_writeExpr(vc, - getArrayForUpdate(root, un->next), - construct(un->index, 0), - construct(un->value, 0)); - - _arr_hash.hashUpdateNodeExpr(un, un_expr); + un_expr = + vc_writeExpr(vc, getArrayForUpdate(root, un->next.get()), + construct(un->index, 0), construct(un->value, 0)); + + _arr_hash.hashUpdateNodeExpr(un, un_expr); } return un_expr; @@ -560,9 +559,9 @@ ExprHandle STPBuilder::constructActual(ref e, int *width_out) { ReadExpr *re = cast(e); assert(re && re->updates.root); *width_out = re->updates.root->getRange(); - return vc_readExpr(vc, - getArrayForUpdate(re->updates.root, re->updates.head), - construct(re->index, 0)); + return vc_readExpr( + vc, getArrayForUpdate(re->updates.root, re->updates.head.get()), + construct(re->index, 0)); } case Expr::Select: { diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index 43440fa7..29f55b31 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -439,7 +439,7 @@ Z3ASTHandle Z3Builder::getArrayForUpdate(const Array *root, bool hashed = _arr_hash.lookupUpdateNodeExpr(un, un_expr); if (!hashed) { - un_expr = writeExpr(getArrayForUpdate(root, un->next), + un_expr = writeExpr(getArrayForUpdate(root, un->next.get()), construct(un->index, 0), construct(un->value, 0)); _arr_hash.hashUpdateNodeExpr(un, un_expr); @@ -522,7 +522,7 @@ Z3ASTHandle Z3Builder::constructActual(ref e, int *width_out) { ReadExpr *re = cast(e); assert(re && re->updates.root); *width_out = re->updates.root->getRange(); - return readExpr(getArrayForUpdate(re->updates.root, re->updates.head), + return readExpr(getArrayForUpdate(re->updates.root, re->updates.head.get()), construct(re->index, 0)); } -- cgit 1.4.1