diff options
author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-02-23 15:30:39 +0100 |
---|---|---|
committer | Martin Nowack <martin@se.inf.tu-dresden.de> | 2016-02-27 10:22:32 +0100 |
commit | b9b40354336dfac0847041119f64c8d11db8b5e3 (patch) | |
tree | f93583c2065af369a23fa386d80b06e83f9060e2 /lib/Core | |
parent | c813f1464ce8ad98d45a6a132499247251e15d96 (diff) | |
download | klee-b9b40354336dfac0847041119f64c8d11db8b5e3.tar.gz |
Refactoring: Extract checking memory limit into own function
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Executor.cpp | 67 | ||||
-rw-r--r-- | lib/Core/Executor.h | 3 |
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(); |