No subject
Sat Dec 18 14:45:13 PST 2010
MemoryObject objects are not freed, until the MemoryManager is
destroyed. Second, when KLEE allocates a non-fixed MemoryObject
object, KLEE also allocates a block of memory which is the same as the
object's size. This block of memory is never freed. So, this patch
generally does reference counting on the MemoryObject objects, and
frees them as soon as the reference count drops to zero."
Many thanks to Paul Marinescu as well, who tested this patch
thoroughly on the Coreutils benchmarks. On 1h runs, the memory
consumption typically goes down by 1-5%, but some applications which
see more significant gains.
Modified:
klee/trunk/include/klee/ExecutionState.h
klee/trunk/lib/Core/ExecutionState.cpp
klee/trunk/lib/Core/Memory.cpp
klee/trunk/lib/Core/Memory.h
klee/trunk/lib/Core/MemoryManager.cpp
klee/trunk/lib/Core/MemoryManager.h
Modified: klee/trunk/include/klee/ExecutionState.h
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/include/klee/ExecutionState.h?rev=148402&r1=148401&r2=148402&view=diff
==============================================================================
--- klee/trunk/include/klee/ExecutionState.h (original)
+++ klee/trunk/include/klee/ExecutionState.h Wed Jan 18 12:58:10 2012
@@ -122,6 +122,8 @@
// use on structure
ExecutionState(const std::vector<ref<Expr> > &assumptions);
+ ExecutionState(const ExecutionState& state);
+
~ExecutionState();
ExecutionState *branch();
@@ -129,9 +131,7 @@
void pushFrame(KInstIterator caller, KFunction *kf);
void popFrame();
- void addSymbolic(const MemoryObject *mo, const Array *array) {
- symbolics.push_back(std::make_pair(mo, array));
- }
+ void addSymbolic(const MemoryObject *mo, const Array *array);
void addConstraint(ref<Expr> e) {
constraints.addConstraint(e);
}
Modified: klee/trunk/lib/Core/ExecutionState.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/ExecutionState.cpp?rev=148402&r1=148401&r2=148402&view=diff
==============================================================================
--- klee/trunk/lib/Core/ExecutionState.cpp (original)
+++ klee/trunk/lib/Core/ExecutionState.cpp Wed Jan 18 12:58:10 2012
@@ -86,9 +86,46 @@
}
ExecutionState::~ExecutionState() {
+ for (unsigned int i=0; i<symbolics.size(); i++)
+ {
+ const MemoryObject *mo = symbolics[i].first;
+ assert(mo->refCount > 0);
+ mo->refCount--;
+ if (mo->refCount == 0)
+ delete mo;
+ }
+
while (!stack.empty()) popFrame();
}
+ExecutionState::ExecutionState(const ExecutionState& state)
+ : fnAliases(state.fnAliases),
+ fakeState(state.fakeState),
+ underConstrained(state.underConstrained),
+ depth(state.depth),
+ pc(state.pc),
+ prevPC(state.prevPC),
+ stack(state.stack),
+ constraints(state.constraints),
+ queryCost(state.queryCost),
+ weight(state.weight),
+ addressSpace(state.addressSpace),
+ pathOS(state.pathOS),
+ symPathOS(state.symPathOS),
+ instsSinceCovNew(state.instsSinceCovNew),
+ coveredNew(state.coveredNew),
+ forkDisabled(state.forkDisabled),
+ coveredLines(state.coveredLines),
+ ptreeNode(state.ptreeNode),
+ symbolics(state.symbolics),
+ arrayNames(state.arrayNames),
+ shadowObjects(state.shadowObjects),
+ incomingBBIndex(state.incomingBBIndex)
+{
+ for (unsigned int i=0; i<symbolics.size(); i++)
+ symbolics[i].first->refCount++;
+}
+
ExecutionState *ExecutionState::branch() {
depth++;
@@ -114,6 +151,10 @@
stack.pop_back();
}
+void ExecutionState::addSymbolic(const MemoryObject *mo, const Array *array) {
+ mo->refCount++;
+ symbolics.push_back(std::make_pair(mo, array));
+}
///
std::string ExecutionState::getFnAlias(std::string fn) {
Modified: klee/trunk/lib/Core/Memory.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/Memory.cpp?rev=148402&r1=148401&r2=148402&view=diff
==============================================================================
--- klee/trunk/lib/Core/Memory.cpp (original)
+++ klee/trunk/lib/Core/Memory.cpp Wed Jan 18 12:58:10 2012
@@ -17,6 +17,7 @@
#include "klee/util/BitArray.h"
#include "ObjectHolder.h"
+#include "MemoryManager.h"
#include <llvm/Function.h>
#include <llvm/Instruction.h>
@@ -63,6 +64,8 @@
int MemoryObject::counter = 0;
MemoryObject::~MemoryObject() {
+ if (parent)
+ parent->markFreed(this);
}
void MemoryObject::getAllocInfo(std::string &result) const {
@@ -100,6 +103,7 @@
updates(0, 0),
size(mo->size),
readOnly(false) {
+ mo->refCount++;
if (!UseConstantArrays) {
// FIXME: Leaked.
static unsigned id = 0;
@@ -120,6 +124,7 @@
updates(array, 0),
size(mo->size),
readOnly(false) {
+ mo->refCount++;
makeSymbolic();
}
@@ -135,6 +140,8 @@
size(os.size),
readOnly(false) {
assert(!os.readOnly && "no need to copy read only object?");
+ if (object)
+ object->refCount++;
if (os.knownSymbolics) {
knownSymbolics = new ref<Expr>[size];
@@ -150,6 +157,16 @@
if (flushMask) delete flushMask;
if (knownSymbolics) delete[] knownSymbolics;
delete[] concreteStore;
+
+ if (object)
+ {
+ assert(object->refCount > 0);
+ object->refCount--;
+ if (object->refCount == 0)
+ {
+ delete object;
+ }
+ }
}
/***/
Modified: klee/trunk/lib/Core/Memory.h
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/Memory.h?rev=148402&r1=148401&r2=148402&view=diff
==============================================================================
--- klee/trunk/lib/Core/Memory.h (original)
+++ klee/trunk/lib/Core/Memory.h Wed Jan 18 12:58:10 2012
@@ -30,9 +30,12 @@
class MemoryObject {
friend class STPBuilder;
+ friend class ObjectState;
+ friend class ExecutionState;
private:
static int counter;
+ mutable unsigned refCount;
public:
unsigned id;
@@ -50,6 +53,8 @@
bool fake_object;
bool isUserSpecified;
+ MemoryManager *parent;
+
/// "Location" for which this memory object was allocated. This
/// should be either the allocating instruction or the global object
/// it was allocated for (or whatever else makes sense).
@@ -69,17 +74,21 @@
// XXX this is just a temp hack, should be removed
explicit
MemoryObject(uint64_t _address)
- : id(counter++),
+ : refCount(0),
+ id(counter++),
address(_address),
size(0),
isFixed(true),
+ parent(NULL),
allocSite(0) {
}
MemoryObject(uint64_t _address, unsigned _size,
bool _isLocal, bool _isGlobal, bool _isFixed,
- const llvm::Value *_allocSite)
- : id(counter++),
+ const llvm::Value *_allocSite,
+ MemoryManager *_parent)
+ : refCount(0),
+ id(counter++),
address(_address),
size(_size),
name("unnamed"),
@@ -88,6 +97,7 @@
isFixed(_isFixed),
fake_object(false),
isUserSpecified(false),
+ parent(_parent),
allocSite(_allocSite) {
}
Modified: klee/trunk/lib/Core/MemoryManager.cpp
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/MemoryManager.cpp?rev=148402&r1=148401&r2=148402&view=diff
==============================================================================
--- klee/trunk/lib/Core/MemoryManager.cpp (original)
+++ klee/trunk/lib/Core/MemoryManager.cpp Wed Jan 18 12:58:10 2012
@@ -25,8 +25,10 @@
MemoryManager::~MemoryManager() {
while (!objects.empty()) {
- MemoryObject *mo = objects.back();
- objects.pop_back();
+ MemoryObject *mo = *objects.begin();
+ if (!mo->isFixed)
+ free((void *)mo->address);
+ objects.erase(mo);
delete mo;
}
}
@@ -44,8 +46,8 @@
++stats::allocations;
MemoryObject *res = new MemoryObject(address, size, isLocal, isGlobal, false,
- allocSite);
- objects.push_back(res);
+ allocSite, this);
+ objects.insert(res);
return res;
}
@@ -62,11 +64,20 @@
++stats::allocations;
MemoryObject *res = new MemoryObject(address, size, false, true, true,
- allocSite);
- objects.push_back(res);
+ allocSite, this);
+ objects.insert(res);
return res;
}
void MemoryManager::deallocate(const MemoryObject *mo) {
assert(0);
}
+
+void MemoryManager::markFreed(MemoryObject *mo) {
+ if (objects.find(mo) != objects.end())
+ {
+ if (!mo->isFixed)
+ free((void *)mo->address);
+ objects.erase(mo);
+ }
+}
Modified: klee/trunk/lib/Core/MemoryManager.h
URL: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/MemoryManager.h?rev=148402&r1=148401&r2=148402&view=diff
==============================================================================
--- klee/trunk/lib/Core/MemoryManager.h (original)
+++ klee/trunk/lib/Core/MemoryManager.h Wed Jan 18 12:58:10 2012
@@ -10,7 +10,7 @@
#ifndef KLEE_MEMORYMANAGER_H
#define KLEE_MEMORYMANAGER_H
-#include <vector>
+#include <set>
#include <stdint.h>
namespace llvm {
@@ -22,7 +22,7 @@
class MemoryManager {
private:
- typedef std::vector<MemoryObject*> objects_ty;
+ typedef std::set<MemoryObject*> objects_ty;
objects_ty objects;
public:
@@ -34,6 +34,7 @@
MemoryObject *allocateFixed(uint64_t address, uint64_t size,
const llvm::Value *allocSite);
void deallocate(const MemoryObject *mo);
+ void markFreed(MemoryObject *mo);
};
} // End klee namespace
More information about the klee-commits
mailing list