Nice patch by Gang Hu, Heming Cui and Junfeng Yang fixing a memory

leak in KLEE.

From Gang Hu: "The memory leak is caused by two reasons.  First, the
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.



git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@148402 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 41 insertions, 0 deletions

diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index c6a2cad4..db685639 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -86,9 +86,46 @@ ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions)
 }
 
 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 @@ void ExecutionState::popFrame() {
   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) {