aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Expr/Assignment.h2
-rw-r--r--include/klee/Expr/Expr.h40
-rw-r--r--include/klee/Expr/ExprRangeEvaluator.h4
-rw-r--r--lib/Core/AddressSpace.cpp64
-rw-r--r--lib/Core/AddressSpace.h8
-rw-r--r--lib/Core/ExecutionState.cpp6
-rw-r--r--lib/Core/Memory.cpp35
-rw-r--r--lib/Core/Memory.h6
-rw-r--r--lib/Core/ObjectHolder.h32
-rw-r--r--lib/Expr/ArrayExprOptimizer.cpp5
-rw-r--r--lib/Expr/ArrayExprVisitor.cpp12
-rw-r--r--lib/Expr/Expr.cpp5
-rw-r--r--lib/Expr/ExprBuilder.cpp4
-rw-r--r--lib/Expr/ExprEvaluator.cpp2
-rw-r--r--lib/Expr/ExprPPrinter.cpp23
-rw-r--r--lib/Expr/ExprSMTLIBPrinter.cpp8
-rw-r--r--lib/Expr/ExprUtil.cpp9
-rw-r--r--lib/Expr/Updates.cpp120
-rw-r--r--lib/Solver/FastCexSolver.cpp4
-rw-r--r--lib/Solver/IndependentSolver.cpp3
-rw-r--r--lib/Solver/STPBuilder.cpp17
-rw-r--r--lib/Solver/Z3Builder.cpp4
22 files changed, 134 insertions, 279 deletions
diff --git a/include/klee/Expr/Assignment.h b/include/klee/Expr/Assignment.h
index ead459a9..395a3387 100644
--- a/include/klee/Expr/Assignment.h
+++ b/include/klee/Expr/Assignment.h
@@ -73,7 +73,7 @@ namespace klee {
return ConstantExpr::alloc(it->second[index], array->getRange());
} else {
if (allowFreeValues) {
- return ReadExpr::create(UpdateList(array, 0),
+ return ReadExpr::create(UpdateList(array, ref<UpdateNode>(nullptr)),
ConstantExpr::alloc(index, array->getDomain()));
} else {
return ConstantExpr::alloc(0, array->getRange());
diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h
index b979596a..374fc541 100644
--- a/include/klee/Expr/Expr.h
+++ b/include/klee/Expr/Expr.h
@@ -450,23 +450,24 @@ public:
/// Class representing a byte update of an array.
class UpdateNode {
- friend class UpdateList;
+ friend class UpdateList;
- mutable unsigned refCount;
// cache instead of recalc
unsigned hashValue;
public:
- const UpdateNode *next;
+ const ref<UpdateNode> next;
ref<Expr> index, value;
-
+
+ /// @brief Required by klee::ref-managed objects
+ mutable class ReferenceCounter _refCount;
+
private:
/// size of this update sequence, including this update
unsigned size;
public:
- UpdateNode(const UpdateNode *_next,
- const ref<Expr> &_index,
+ UpdateNode(const ref<UpdateNode> &_next, const ref<Expr> &_index,
const ref<Expr> &_value);
unsigned getSize() const { return size; }
@@ -474,9 +475,8 @@ public:
int compare(const UpdateNode &b) const;
unsigned hash() const { return hashValue; }
-private:
- UpdateNode() : refCount(0) {}
- ~UpdateNode();
+ UpdateNode() = delete;
+ ~UpdateNode() = default;
unsigned computeHash();
};
@@ -544,24 +544,24 @@ public:
const Array *root;
/// pointer to the most recent update node
- const UpdateNode *head;
-
+ ref<UpdateNode> head;
+
public:
- UpdateList(const Array *_root, const UpdateNode *_head);
- UpdateList(const UpdateList &b);
- ~UpdateList();
-
- UpdateList &operator=(const UpdateList &b);
+ UpdateList(const Array *_root, const ref<UpdateNode> &_head);
+ UpdateList(const UpdateList &b) = default;
+ ~UpdateList() = default;
+
+ UpdateList &operator=(const UpdateList &b) = default;
/// size of this update list
- unsigned getSize() const { return (head ? head->getSize() : 0); }
-
+ unsigned getSize() const {
+ return (head.get() != nullptr ? head->getSize() : 0);
+ }
+
void extend(const ref<Expr> &index, const ref<Expr> &value);
int compare(const UpdateList &b) const;
unsigned hash() const;
-private:
- void tryFreeNodes();
};
/// Class representing a one byte read from an array.
diff --git a/include/klee/Expr/ExprRangeEvaluator.h b/include/klee/Expr/ExprRangeEvaluator.h
index 4d212764..540ccafd 100644
--- a/include/klee/Expr/ExprRangeEvaluator.h
+++ b/include/klee/Expr/ExprRangeEvaluator.h
@@ -73,7 +73,7 @@ T ExprRangeEvaluator<T>::evalRead(const UpdateList &ul,
T index) {
T res;
- for (const UpdateNode *un=ul.head; un; un=un->next) {
+ for (const UpdateNode *un = ul.head.get(); un; un = un->next.get()) {
T ui = evaluate(un->index);
if (ui.mustEqual(index)) {
@@ -85,7 +85,7 @@ T ExprRangeEvaluator<T>::evalRead(const UpdateList &ul,
}
}
}
-
+
return res.set_union(getInitialReadRange(*ul.root, index));
}
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 12e74c77..e006d4d0 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -30,23 +30,23 @@ void AddressSpace::unbindObject(const MemoryObject *mo) {
}
const ObjectState *AddressSpace::findObject(const MemoryObject *mo) const {
- const MemoryMap::value_type *res = objects.lookup(mo);
-
- return res ? res->second : 0;
+ const auto res = objects.lookup(mo);
+ return res ? res->second.get() : nullptr;
}
ObjectState *AddressSpace::getWriteable(const MemoryObject *mo,
const ObjectState *os) {
assert(!os->readOnly);
- if (cowKey==os->copyOnWriteOwner) {
+ // If this address space owns they object, return it
+ if (cowKey == os->copyOnWriteOwner)
return const_cast<ObjectState*>(os);
- } else {
- ObjectState *n = new ObjectState(*os);
- n->copyOnWriteOwner = cowKey;
- objects = objects.replace(std::make_pair(mo, n));
- return n;
- }
+
+ // Add a copy of this object state that can be updated
+ ref<ObjectState> newObjectState(new ObjectState(*os));
+ newObjectState->copyOnWriteOwner = cowKey;
+ objects = objects.replace(std::make_pair(mo, newObjectState));
+ return newObjectState.get();
}
///
@@ -56,13 +56,14 @@ bool AddressSpace::resolveOne(const ref<ConstantExpr> &addr,
uint64_t address = addr->getZExtValue();
MemoryObject hack(address);
- if (const MemoryMap::value_type *res = objects.lookup_previous(&hack)) {
- const MemoryObject *mo = res->first;
+ if (const auto res = objects.lookup_previous(&hack)) {
+ const auto &mo = res->first;
// Check if the provided address is between start and end of the object
// [mo->address, mo->address + mo->size) or the object is a 0-sized object.
if ((mo->size==0 && address==mo->address) ||
(address - mo->address < mo->size)) {
- result = *res;
+ result.first = res->first;
+ result.second = res->second.get();
return true;
}
}
@@ -88,12 +89,13 @@ bool AddressSpace::resolveOne(ExecutionState &state,
return false;
uint64_t example = cex->getZExtValue();
MemoryObject hack(example);
- const MemoryMap::value_type *res = objects.lookup_previous(&hack);
-
+ const auto res = objects.lookup_previous(&hack);
+
if (res) {
const MemoryObject *mo = res->first;
if (example - mo->address < mo->size) {
- result = *res;
+ result.first = res->first;
+ result.second = res->second.get();
success = true;
return true;
}
@@ -108,14 +110,15 @@ bool AddressSpace::resolveOne(ExecutionState &state,
MemoryMap::iterator start = oi;
while (oi!=begin) {
--oi;
- const MemoryObject *mo = oi->first;
-
+ const auto &mo = oi->first;
+
bool mayBeTrue;
if (!solver->mayBeTrue(state,
mo->getBoundsCheckPointer(address), mayBeTrue))
return false;
if (mayBeTrue) {
- result = *oi;
+ result.first = oi->first;
+ result.second = oi->second.get();
success = true;
return true;
} else {
@@ -131,7 +134,7 @@ bool AddressSpace::resolveOne(ExecutionState &state,
// search forwards
for (oi=start; oi!=end; ++oi) {
- const MemoryObject *mo = oi->first;
+ const auto &mo = oi->first;
bool mustBeTrue;
if (!solver->mustBeTrue(state,
@@ -148,7 +151,8 @@ bool AddressSpace::resolveOne(ExecutionState &state,
mayBeTrue))
return false;
if (mayBeTrue) {
- result = *oi;
+ result.first = oi->first;
+ result.second = oi->second.get();
success = true;
return true;
}
@@ -240,8 +244,10 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
if (timeout && timeout < timer.delta())
return true;
+ auto op = std::make_pair<>(mo, oi->second.get());
+
int incomplete =
- checkPointerInObject(state, solver, p, *oi, rl, maxResolutions);
+ checkPointerInObject(state, solver, p, op, rl, maxResolutions);
if (incomplete != 2)
return incomplete ? true : false;
@@ -265,9 +271,10 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
return true;
if (mustBeTrue)
break;
+ auto op = std::make_pair<>(mo, oi->second.get());
int incomplete =
- checkPointerInObject(state, solver, p, *oi, rl, maxResolutions);
+ checkPointerInObject(state, solver, p, op, rl, maxResolutions);
if (incomplete != 2)
return incomplete ? true : false;
}
@@ -288,7 +295,7 @@ void AddressSpace::copyOutConcretes() {
const MemoryObject *mo = it->first;
if (!mo->isUserSpecified) {
- ObjectState *os = it->second;
+ const auto &os = it->second;
auto address = reinterpret_cast<std::uint8_t*>(mo->address);
if (!os->readOnly)
@@ -298,14 +305,13 @@ void AddressSpace::copyOutConcretes() {
}
bool AddressSpace::copyInConcretes() {
- for (MemoryMap::iterator it = objects.begin(), ie = objects.end();
- it != ie; ++it) {
- const MemoryObject *mo = it->first;
+ for (auto &obj : objects) {
+ const MemoryObject *mo = obj.first;
if (!mo->isUserSpecified) {
- const ObjectState *os = it->second;
+ const auto &os = obj.second;
- if (!copyInConcrete(mo, os, mo->address))
+ if (!copyInConcrete(mo, os.get(), mo->address))
return false;
}
}
diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index 9e7e414a..10310a1e 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -10,8 +10,7 @@
#ifndef KLEE_ADDRESSSPACE_H
#define KLEE_ADDRESSSPACE_H
-#include "ObjectHolder.h"
-
+#include "Memory.h"
#include "klee/Expr/Expr.h"
#include "klee/Internal/ADT/ImmutableMap.h"
#include "klee/Internal/System/Time.h"
@@ -31,8 +30,9 @@ namespace klee {
struct MemoryObjectLT {
bool operator()(const MemoryObject *a, const MemoryObject *b) const;
};
-
- typedef ImmutableMap<const MemoryObject*, ObjectHolder, MemoryObjectLT> MemoryMap;
+
+ typedef ImmutableMap<const MemoryObject *, ref<ObjectState>, MemoryObjectLT>
+ MemoryMap;
class AddressSpace {
private:
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 60715b33..78aa8f67 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -166,9 +166,9 @@ llvm::raw_ostream &klee::operator<<(llvm::raw_ostream &os, const MemoryMap &mm)
MemoryMap::iterator it = mm.begin();
MemoryMap::iterator ie = mm.end();
if (it!=ie) {
- os << "MO" << it->first->id << ":" << it->second;
+ os << "MO" << it->first->id << ":" << it->second.get();
for (++it; it!=ie; ++it)
- os << ", MO" << it->first->id << ":" << it->second;
+ os << ", MO" << it->first->id << ":" << it->second.get();
}
os << "}";
return os;
@@ -265,7 +265,7 @@ bool ExecutionState::merge(const ExecutionState &b) {
}
return false;
}
- if (ai->second != bi->second) {
+ if (ai->second.get() != bi->second.get()) {
if (DebugLogStateMerge)
llvm::errs() << "\t\tmutated: " << ai->first->id << "\n";
mutated.insert(ai->first);
diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp
index c7e7a928..37e6646b 100644
--- a/lib/Core/Memory.cpp
+++ b/lib/Core/Memory.cpp
@@ -11,7 +11,6 @@
#include "Context.h"
#include "MemoryManager.h"
-#include "ObjectHolder.h"
#include "klee/Expr/ArrayCache.h"
#include "klee/Expr/Expr.h"
@@ -42,27 +41,6 @@ namespace {
/***/
-ObjectHolder::ObjectHolder(const ObjectHolder &b) : os(b.os) {
- if (os) ++os->refCount;
-}
-
-ObjectHolder::ObjectHolder(ObjectState *_os) : os(_os) {
- if (os) ++os->refCount;
-}
-
-ObjectHolder::~ObjectHolder() {
- if (os && --os->refCount==0) delete os;
-}
-
-ObjectHolder &ObjectHolder::operator=(const ObjectHolder &b) {
- if (b.os) ++b.os->refCount;
- if (os && --os->refCount==0) delete os;
- os = b.os;
- return *this;
-}
-
-/***/
-
int MemoryObject::counter = 0;
MemoryObject::~MemoryObject() {
@@ -96,7 +74,6 @@ void MemoryObject::getAllocInfo(std::string &result) const {
ObjectState::ObjectState(const MemoryObject *mo)
: copyOnWriteOwner(0),
- refCount(0),
object(mo),
concreteStore(new uint8_t[mo->size]),
concreteMask(0),
@@ -118,7 +95,6 @@ ObjectState::ObjectState(const MemoryObject *mo)
ObjectState::ObjectState(const MemoryObject *mo, const Array *array)
: copyOnWriteOwner(0),
- refCount(0),
object(mo),
concreteStore(new uint8_t[mo->size]),
concreteMask(0),
@@ -134,7 +110,6 @@ ObjectState::ObjectState(const MemoryObject *mo, const Array *array)
ObjectState::ObjectState(const ObjectState &os)
: copyOnWriteOwner(0),
- refCount(0),
object(os.object),
concreteStore(new uint8_t[os.size]),
concreteMask(os.concreteMask ? new BitArray(*os.concreteMask, os.size) : 0),
@@ -188,10 +163,10 @@ const UpdateList &ObjectState::getUpdates() const {
// FIXME: We should be able to do this more efficiently, we just need to be
// careful to get the interaction with the cache right. In particular we
// should avoid creating UpdateNode instances we never use.
- unsigned NumWrites = updates.head ? updates.head->getSize() : 0;
+ unsigned NumWrites = updates.head.isNull() ? 0 : updates.head->getSize();
std::vector< std::pair< ref<Expr>, ref<Expr> > > Writes(NumWrites);
- const UpdateNode *un = updates.head;
- for (unsigned i = NumWrites; i != 0; un = un->next) {
+ const auto *un = updates.head.get();
+ for (unsigned i = NumWrites; i != 0; un = un->next.get()) {
--i;
Writes[i] = std::make_pair(un->index, un->value);
}
@@ -257,7 +232,7 @@ void ObjectState::makeConcrete() {
}
void ObjectState::makeSymbolic() {
- assert(!updates.head &&
+ assert(updates.head.isNull() &&
"XXX makeSymbolic of objects with symbolic values is unsupported");
// XXX simplify this, can just delete various arrays I guess
@@ -612,7 +587,7 @@ void ObjectState::print() const {
}
llvm::errs() << "\tUpdates:\n";
- for (const UpdateNode *un=updates.head; un; un=un->next) {
+ for (const auto *un = updates.head.get(); un; un = un->next.get()) {
llvm::errs() << "\t\t[" << un->index << "] = " << un->value << "\n";
}
}
diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h
index dfda433c..e4260c55 100644
--- a/lib/Core/Memory.h
+++ b/lib/Core/Memory.h
@@ -148,10 +148,12 @@ public:
class ObjectState {
private:
friend class AddressSpace;
+ friend class ref<ObjectState>;
+
unsigned copyOnWriteOwner; // exclusively for AddressSpace
- friend class ObjectHolder;
- unsigned refCount;
+ /// @brief Required by klee::ref-managed objects
+ class ReferenceCounter _refCount;
const MemoryObject *object;
diff --git a/lib/Core/ObjectHolder.h b/lib/Core/ObjectHolder.h
deleted file mode 100644
index cd6c6281..00000000
--- a/lib/Core/ObjectHolder.h
+++ /dev/null
@@ -1,32 +0,0 @@
-//===-- ObjectHolder.h ------------------------------------------*- C++ -*-===//
-//
-// The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef KLEE_OBJECTHOLDER_H
-#define KLEE_OBJECTHOLDER_H
-
-namespace klee {
- class ObjectState;
-
- class ObjectHolder {
- ObjectState *os;
-
- public:
- ObjectHolder() : os(0) {}
- ObjectHolder(ObjectState *_os);
- ObjectHolder(const ObjectHolder &b);
- ~ObjectHolder();
-
- ObjectHolder &operator=(const ObjectHolder &b);
-
- operator class ObjectState *() { return os; }
- operator class ObjectState *() const { return (ObjectState*) os; }
- };
-}
-
-#endif /* KLEE_OBJECTHOLDER_H */
diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp
index 60f2ca6e..d80cc3bc 100644
--- a/lib/Expr/ArrayExprOptimizer.cpp
+++ b/lib/Expr/ArrayExprOptimizer.cpp
@@ -284,7 +284,8 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
// reverse the list
std::vector<const UpdateNode *> us;
us.reserve(read->updates.getSize());
- for (const UpdateNode *un = read->updates.head; un; un = un->next)
+ for (const UpdateNode *un = read->updates.head.get(); un;
+ un = un->next.get())
us.push_back(un);
auto arrayConstValues = read->updates.root->constantValues;
@@ -366,7 +367,7 @@ ref<Expr> ExprOptimizer::getSelectOptExpr(
// reverse the list
std::vector<const UpdateNode *> us;
us.reserve(read->updates.getSize());
- for (const UpdateNode *un = read->updates.head; un; un = un->next)
+ for (const UpdateNode *un = read->updates.head.get(); un; un = un->next.get())
us.push_back(un);
for (auto it = us.rbegin(); it != us.rend(); it++) {
diff --git a/lib/Expr/ArrayExprVisitor.cpp b/lib/Expr/ArrayExprVisitor.cpp
index cada7867..986360f7 100644
--- a/lib/Expr/ArrayExprVisitor.cpp
+++ b/lib/Expr/ArrayExprVisitor.cpp
@@ -63,7 +63,7 @@ ConstantArrayExprVisitor::visitConcat(const ConcatExpr &ce) {
// that is read at a symbolic index
if (base->updates.root->isConstantArray() &&
!isa<ConstantExpr>(base->index)) {
- for (const UpdateNode *un = base->updates.head; un; un = un->next) {
+ for (const auto *un = base->updates.head.get(); un; un = un->next.get()) {
if (!isa<ConstantExpr>(un->index) || !isa<ConstantExpr>(un->value)) {
incompatible = true;
return Action::skipChildren();
@@ -97,7 +97,7 @@ ExprVisitor::Action ConstantArrayExprVisitor::visitRead(const ReadExpr &re) {
// It is an interesting ReadExpr if it contains a concrete array
// that is read at a symbolic index
if (re.updates.root->isConstantArray() && !isa<ConstantExpr>(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()) {
if (!isa<ConstantExpr>(un->index) || !isa<ConstantExpr>(un->value)) {
incompatible = true;
return Action::skipChildren();
@@ -132,7 +132,7 @@ ExprVisitor::Action ConstantArrayExprVisitor::visitRead(const ReadExpr &re) {
ExprVisitor::Action
IndexCompatibilityExprVisitor::visitRead(const ReadExpr &re) {
- if (re.updates.head) {
+ if (!re.updates.head.isNull()) {
compatible = false;
return Action::skipChildren();
} else if (re.updates.root->isConstantArray() &&
@@ -198,13 +198,13 @@ ExprVisitor::Action ArrayReadExprVisitor::inspectRead(ref<Expr> hash,
// pre(*): index is symbolic
if (!isa<ConstantExpr>(re.index)) {
if (readInfo.find(&re) == readInfo.end()) {
- if (re.updates.root->isSymbolicArray() && !re.updates.head) {
+ if (re.updates.root->isSymbolicArray() && re.updates.head.isNull()) {
return Action::doChildren();
}
- if (re.updates.head) {
+ if (!re.updates.head.isNull()) {
// Check preconditions on UpdateList nodes
bool hasConcreteValues = false;
- for (const UpdateNode *un = re.updates.head; un; un = un->next) {
+ for (const auto *un = re.updates.head.get(); un; un = un->next.get()) {
// Symbolic case - \inv(update): index is concrete
if (!isa<ConstantExpr>(un->index)) {
incompatible = true;
diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp
index 6b8dc95f..b798bc37 100644
--- a/lib/Expr/Expr.cpp
+++ b/lib/Expr/Expr.cpp
@@ -537,10 +537,9 @@ ref<Expr> ReadExpr::create(const UpdateList &ul, ref<Expr> index) {
// least recent to find a potential written value for a concrete index;
// stop if an update with symbolic has been found as we don't know which
// array element has been updated
- const UpdateNode *un = ul.head;
+ auto un = ul.head.get();
bool updateListHasSymbolicWrites = false;
- for (; un; un=un->next) {
- // Check if we have an equivalent concrete index
+ for (; un; un = un->next.get()) {
ref<Expr> cond = EqExpr::create(index, un->index);
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(cond)) {
if (CE->isTrue())
diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp
index e1cfa2d2..f8f57d35 100644
--- a/lib/Expr/ExprBuilder.cpp
+++ b/lib/Expr/ExprBuilder.cpp
@@ -326,8 +326,8 @@ namespace {
virtual ref<Expr> Read(const UpdateList &Updates,
const ref<Expr> &Index) {
// Roll back through writes when possible.
- const UpdateNode *UN = Updates.head;
- while (UN && Eq(Index, UN->index)->isFalse())
+ auto UN = Updates.head;
+ while (!UN.isNull() && Eq(Index, UN->index)->isFalse())
UN = UN->next;
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(Index))
diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp
index f03d7669..afd5d641 100644
--- a/lib/Expr/ExprEvaluator.cpp
+++ b/lib/Expr/ExprEvaluator.cpp
@@ -13,7 +13,7 @@ using namespace klee;
ExprVisitor::Action ExprEvaluator::evalRead(const UpdateList &ul,
unsigned index) {
- for (const UpdateNode *un=ul.head; un; un=un->next) {
+ for (auto un = ul.head; !un.isNull(); un = un->next) {
ref<Expr> ui = visit(un->index);
if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ui)) {
diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp
index 2ccd7262..9d34e356 100644
--- a/lib/Expr/ExprPPrinter.cpp
+++ b/lib/Expr/ExprPPrinter.cpp
@@ -92,7 +92,8 @@ private:
if (isVerySimple(e)) {
return true;
} else if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
- return isVerySimple(re->index) && isVerySimpleUpdate(re->updates.head);
+ return isVerySimple(re->index) &&
+ isVerySimpleUpdate(re->updates.head.get());
} else {
Expr *ep = e.get();
for (unsigned i=0; i<ep->getNumKids(); i++)
@@ -113,7 +114,7 @@ private:
// FIXME: This needs to be non-recursive.
if (un) {
if (couldPrintUpdates.insert(un).second) {
- scanUpdate(un->next);
+ scanUpdate(un->next.get());
scan1(un->index);
scan1(un->value);
} else {
@@ -130,7 +131,7 @@ private:
scan1(ep->getKid(i));
if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
usedArrays.insert(re->updates.root);
- scanUpdate(re->updates.head);
+ scanUpdate(re->updates.head.get());
}
} else {
shouldPrint.insert(e);
@@ -139,10 +140,10 @@ private:
}
void printUpdateList(const UpdateList &updates, PrintContext &PC) {
- const UpdateNode *head = updates.head;
+ auto head = updates.head;
// Special case empty list.
- if (!head) {
+ if (head.isNull()) {
// FIXME: We need to do something (assert, mangle, etc.) so that printing
// distinct arrays with the same name doesn't fail.
PC << updates.root->name;
@@ -153,22 +154,22 @@ private:
bool openedList = false, nextShouldBreak = false;
unsigned outerIndent = PC.pos;
unsigned middleIndent = 0;
- for (const UpdateNode *un = head; un; un = un->next) {
+ for (auto un = head; !un.isNull(); un = un->next) {
// We are done if we hit the cache.
- std::map<const UpdateNode*, unsigned>::iterator it =
- updateBindings.find(un);
+ std::map<const UpdateNode *, unsigned>::iterator it =
+ updateBindings.find(un.get());
if (it!=updateBindings.end()) {
if (openedList)
PC << "] @ ";
PC << "U" << it->second;
return;
- } else if (!hasScan || shouldPrintUpdates.count(un)) {
+ } else if (!hasScan || shouldPrintUpdates.count(un.get())) {
if (openedList)
PC << "] @";
if (un != head)
PC.breakLine(outerIndent);
- PC << "U" << updateCounter << ":";
- updateBindings.insert(std::make_pair(un, updateCounter++));
+ PC << "U" << updateCounter << ":";
+ updateBindings.insert(std::make_pair(un.get(), updateCounter++));
openedList = nextShouldBreak = false;
}
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp
index b83a6af4..069eb32f 100644
--- a/lib/Expr/ExprSMTLIBPrinter.cpp
+++ b/lib/Expr/ExprSMTLIBPrinter.cpp
@@ -279,7 +279,7 @@ void ExprSMTLIBPrinter::printReadExpr(const ref<ReadExpr> &e) {
printSeperator();
// print array with updates recursively
- printUpdatesAndArray(e->updates.head, e->updates.root);
+ printUpdatesAndArray(e->updates.head.get(), e->updates.root);
// print index
printSeperator();
@@ -483,7 +483,7 @@ void ExprSMTLIBPrinter::printUpdatesAndArray(const UpdateNode *un,
printSeperator();
// recurse to get the array or update that this store operations applies to
- printUpdatesAndArray(un->next, root);
+ printUpdatesAndArray(un->next.get(), root);
printSeperator();
@@ -713,7 +713,7 @@ void ExprSMTLIBPrinter::scan(const ref<Expr> &e) {
haveConstantArray = true;
// scan the update list
- scanUpdates(re->updates.head);
+ scanUpdates(re->updates.head.get());
}
}
@@ -824,7 +824,7 @@ void ExprSMTLIBPrinter::scanUpdates(const UpdateNode *un) {
while (un != NULL) {
scan(un->index);
scan(un->value);
- un = un->next;
+ un = un->next.get();
}
}
diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp
index 911366f3..3819e3a2 100644
--- a/lib/Expr/ExprUtil.cpp
+++ b/lib/Expr/ExprUtil.cpp
@@ -49,8 +49,9 @@ void klee::findReads(ref<Expr> e,
// especially since we memoize all the expr results anyway. So
// we take a simple approach of memoizing the results for the
// head, which often will be shared among multiple nodes.
- if (updates.insert(re->updates.head).second) {
- for (const UpdateNode *un=re->updates.head; un; un=un->next) {
+ if (updates.insert(re->updates.head.get()).second) {
+ for (const auto *un = re->updates.head.get(); un;
+ un = un->next.get()) {
if (!isa<ConstantExpr>(un->index) &&
visited.insert(un->index).second)
stack.push_back(un->index);
@@ -82,7 +83,7 @@ protected:
const UpdateList &ul = re.updates;
// XXX should we memo better than what ExprVisitor is doing for us?
- for (const UpdateNode *un=ul.head; un; un=un->next) {
+ for (const auto *un = ul.head.get(); un; un = un->next.get()) {
visit(un->index);
visit(un->value);
}
@@ -106,7 +107,7 @@ ExprVisitor::Action ConstantArrayFinder::visitRead(const ReadExpr &re) {
const UpdateList &ul = re.updates;
// FIXME should we memo better than what ExprVisitor is doing for us?
- for (const UpdateNode *un = ul.head; un; un = un->next) {
+ for (const auto *un = ul.head.get(); un; un = un->next.get()) {
visit(un->index);
visit(un->value);
}
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;
}
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<Expr> e, int *width_out) {
ReadExpr *re = cast<ReadExpr>(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<Expr> e, int *width_out) {
ReadExpr *re = cast<ReadExpr>(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));
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-16 06:36:01 +0000