aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2018-09-12 14:58:11 +0000
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-02-19 12:05:22 +0000
commit9cfa329a77d3dfec4746ca307c6da1b3e904cbfa (patch)
treec9379a0ab0b5afdf740fae0a01c67bf76d061d86 /lib/Core
parent86ab439d589d0afb1b710ef58296d07a263092e3 (diff)
downloadklee-9cfa329a77d3dfec4746ca307c6da1b3e904cbfa.tar.gz
Use `ref<>` for UpdateNode
Remove additional reference counting as part of UpdateNodeList and UpdateNode. Simplifies code.
Diffstat (limited to 'lib/Core')
-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
6 files changed, 51 insertions, 100 deletions
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 */