aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
authorMartin Nowack <martin@se.inf.tu-dresden.de>2016-02-23 15:30:39 +0100
committerMartin Nowack <martin@se.inf.tu-dresden.de>2016-02-27 10:22:32 +0100
commitb9b40354336dfac0847041119f64c8d11db8b5e3 (patch)
treef93583c2065af369a23fa386d80b06e83f9060e2 /lib/Core
parentc813f1464ce8ad98d45a6a132499247251e15d96 (diff)
downloadklee-b9b40354336dfac0847041119f64c8d11db8b5e3.tar.gz
Refactoring: Extract checking memory limit into own function
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/Executor.cpp67
-rw-r--r--lib/Core/Executor.h3
2 files changed, 36 insertions, 34 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 854754b0..33cee9f9 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2437,6 +2437,39 @@ void Executor::bindModuleConstants() {
}
}
+void Executor::checkMemoryUsage() {
+ if (!MaxMemory)
+ return;
+ if ((stats::instructions & 0xFFFF) == 0) {
+ // We need to avoid calling GetTotalMallocUsage() often because it
+ // is O(elts on freelist). This is really bad since we start
+ // to pummel the freelist once we hit the memory cap.
+ unsigned mbs = util::GetTotalMallocUsage() >> 20;
+ if (mbs > MaxMemory) {
+ if (mbs > MaxMemory + 100) {
+ // just guess at how many to kill
+ unsigned numStates = states.size();
+ unsigned toKill = std::max(1U, numStates - numStates * MaxMemory / mbs);
+ klee_warning("killing %d states (over memory cap)", toKill);
+ std::vector<ExecutionState *> arr(states.begin(), states.end());
+ for (unsigned i = 0, N = arr.size(); N && i < toKill; ++i, --N) {
+ unsigned idx = rand() % N;
+ // Make two pulls to try and not hit a state that
+ // covered new code.
+ if (arr[idx]->coveredNew)
+ idx = rand() % N;
+
+ std::swap(arr[idx], arr[N - 1]);
+ terminateStateEarly(*arr[N - 1], "Memory limit exceeded.");
+ }
+ }
+ atMemoryLimit = true;
+ } else {
+ atMemoryLimit = false;
+ }
+ }
+}
+
void Executor::run(ExecutionState &initialState) {
bindModuleConstants();
@@ -2522,39 +2555,7 @@ void Executor::run(ExecutionState &initialState) {
executeInstruction(state, ki);
processTimers(&state, MaxInstructionTime);
- if (MaxMemory) {
- if ((stats::instructions & 0xFFFF) == 0) {
- // We need to avoid calling GetMallocUsage() often because it
- // is O(elts on freelist). This is really bad since we start
- // to pummel the freelist once we hit the memory cap.
- unsigned mbs = util::GetTotalMallocUsage() >> 20;
- if (mbs > MaxMemory) {
- if (mbs > MaxMemory + 100) {
- // just guess at how many to kill
- unsigned numStates = states.size();
- unsigned toKill = std::max(1U, numStates - numStates*MaxMemory/mbs);
-
- klee_warning("killing %d states (over memory cap)", toKill);
-
- std::vector<ExecutionState*> arr(states.begin(), states.end());
- for (unsigned i=0,N=arr.size(); N && i<toKill; ++i,--N) {
- unsigned idx = rand() % N;
-
- // Make two pulls to try and not hit a state that
- // covered new code.
- if (arr[idx]->coveredNew)
- idx = rand() % N;
-
- std::swap(arr[idx], arr[N-1]);
- terminateStateEarly(*arr[N-1], "Memory limit exceeded.");
- }
- }
- atMemoryLimit = true;
- } else {
- atMemoryLimit = false;
- }
- }
- }
+ checkMemoryUsage();
updateStates(&state);
}
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 919d2124..8bfa278a 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -399,7 +399,8 @@ private:
void initTimers();
void processTimers(ExecutionState *current,
double maxInstTime);
-
+ void checkMemoryUsage();
+
public:
Executor(const InterpreterOptions &opts, InterpreterHandler *ie);
virtual ~Executor();