From 3fd9be596e20664e62f8daf5ddabaa10d7b4de3f Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Wed, 29 Jan 2020 19:13:20 +0000 Subject: Enforce fork/branch limits in branch() and fix double termination * extend help messages for -max-memory and -max-memory-inhibit * introduces branchingPermitted() * enforces fork/branch limits in branch() (vector version) * changes main loop * calls updateStates() before checkMemoryUsage() * calls updateStates() again in case we early terminate states This should prevent double termination for now. Other solutions are imho more expensive as we would have to compare possibly large vectors of states (either states(arr) in checkMemoryUsage() or removedStates in terminateState()). --- lib/Core/Executor.cpp | 127 ++++++++++++++++++++++++++------------------- lib/Core/Executor.h | 8 ++- test/Feature/MemoryLimit.c | 4 +- 3 files changed, 83 insertions(+), 56 deletions(-) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 3272201a..b7041148 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -307,14 +307,15 @@ cl::opt MaxDepth( cl::opt MaxMemory("max-memory", cl::desc("Refuse to fork when above this amount of " - "memory (in MB) (default=2000)"), + "memory (in MB) (see -max-memory-inhibit) and terminate " + "states when additional 100MB allocated (default=2000)"), cl::init(2000), cl::cat(TerminationCat)); cl::opt MaxMemoryInhibit( "max-memory-inhibit", cl::desc( - "Inhibit forking at memory cap (vs. random terminate) (default=true)"), + "Inhibit forking when above memory cap (see -max-memory) (default=true)"), cl::init(true), cl::cat(TerminationCat)); @@ -844,6 +845,28 @@ void Executor::initializeGlobalObjects(ExecutionState &state) { } } + +bool Executor::branchingPermitted(const ExecutionState &state) const { + if ((MaxMemoryInhibit && atMemoryLimit) || + state.forkDisabled || + inhibitForking || + (MaxForks!=~0u && stats::forks >= MaxForks)) { + + if (MaxMemoryInhibit && atMemoryLimit) + klee_warning_once(0, "skipping fork (memory cap exceeded)"); + else if (state.forkDisabled) + klee_warning_once(0, "skipping fork (fork disabled on current path)"); + else if (inhibitForking) + klee_warning_once(0, "skipping fork (fork disabled globally)"); + else + klee_warning_once(0, "skipping fork (max-forks reached)"); + + return false; + } + + return true; +} + void Executor::branch(ExecutionState &state, const std::vector< ref > &conditions, std::vector &result) { @@ -851,13 +874,13 @@ void Executor::branch(ExecutionState &state, unsigned N = conditions.size(); assert(N); - if (MaxForks!=~0u && stats::forks >= MaxForks) { + if (!branchingPermitted(state)) { unsigned next = theRNG.getInt32() % N; for (unsigned i=0; i condition, bool isInternal) { } else if (res==Solver::Unknown) { assert(!replayKTest && "in replay mode, only one branch can be true."); - if ((MaxMemoryInhibit && atMemoryLimit) || - current.forkDisabled || - inhibitForking || - (MaxForks!=~0u && stats::forks >= MaxForks)) { - - if (MaxMemoryInhibit && atMemoryLimit) - klee_warning_once(0, "skipping fork (memory cap exceeded)"); - else if (current.forkDisabled) - klee_warning_once(0, "skipping fork (fork disabled on current path)"); - else if (inhibitForking) - klee_warning_once(0, "skipping fork (fork disabled globally)"); - else - klee_warning_once(0, "skipping fork (max-forks reached)"); - + if (!branchingPermitted(current)) { TimerStatIncrementer timer(stats::forkTime); if (theRNG.getBool()) { addConstraint(current, condition); @@ -2895,39 +2905,46 @@ 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) + - (memory->getUsedDeterministicSize() >> 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 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; - } +bool Executor::checkMemoryUsage() { + if (!MaxMemory) return true; + + // 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. + if ((stats::instructions & 0xFFFFU) != 0) // every 65536 instructions + return true; + + // check memory limit + const auto mallocUsage = util::GetTotalMallocUsage() >> 20U; + const auto mmapUsage = memory->getUsedDeterministicSize() >> 20U; + const auto totalUsage = mallocUsage + mmapUsage; + atMemoryLimit = totalUsage > MaxMemory; // inhibit forking + if (!atMemoryLimit) + return true; + + // only terminate states when threshold (+100MB) exceeded + if (totalUsage <= MaxMemory + 100) + return true; + + // just guess at how many to kill + const auto numStates = states.size(); + auto toKill = std::max(1UL, numStates - numStates * MaxMemory / totalUsage); + klee_warning("killing %lu states (over memory cap: %luMB)", toKill, totalUsage); + + // randomly select states for early termination + std::vector arr(states.begin(), states.end()); // FIXME: expensive + for (unsigned i = 0, N = arr.size(); N && i < toKill; ++i, --N) { + unsigned idx = theRNG.getInt32() % N; + // Make two pulls to try and not hit a state that + // covered new code. + if (arr[idx]->coveredNew) + idx = theRNG.getInt32() % N; + + std::swap(arr[idx], arr[N - 1]); + terminateStateEarly(*arr[N - 1], "Memory limit exceeded."); } + + return false; } void Executor::doDumpStates() { @@ -3016,6 +3033,7 @@ void Executor::run(ExecutionState &initialState) { std::vector newStates(states.begin(), states.end()); searcher->update(0, newStates, std::vector()); + // main interpreter loop while (!states.empty() && !haltExecution) { ExecutionState &state = searcher->selectState(); KInstruction *ki = state.pc; @@ -3026,13 +3044,16 @@ void Executor::run(ExecutionState &initialState) { if (::dumpStates) dumpStates(); if (::dumpPTree) dumpPTree(); - checkMemoryUsage(); - updateStates(&state); + + if (!checkMemoryUsage()) { + // update searchers when states were terminated early due to memory pressure + updateStates(nullptr); + } } delete searcher; - searcher = 0; + searcher = nullptr; doDumpStates(); } diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 7acbc60f..d27fa503 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -436,7 +436,13 @@ private: ref e, ref value); - void checkMemoryUsage(); + /// check memory usage and terminate states when over threshold of -max-memory + 100MB + /// \return true if below threshold, false otherwise (states were terminated) + bool checkMemoryUsage(); + + /// check if branching/forking is allowed + bool branchingPermitted(const ExecutionState &state) const; + void printDebugInstructions(ExecutionState &state); void doDumpStates(); diff --git a/test/Feature/MemoryLimit.c b/test/Feature/MemoryLimit.c index 1cdf7260..e9635cab 100644 --- a/test/Feature/MemoryLimit.c +++ b/test/Feature/MemoryLimit.c @@ -9,14 +9,14 @@ // RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.little.bc > %t.little.log // RUN: not grep -q "MALLOC FAILED" %t.little.log // RUN: not grep -q "DONE" %t.little.log -// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.klee-out/warnings.txt +// RUN: grep "WARNING: killing 1 states (over memory cap" %t.klee-out/warnings.txt // RUN: %clang -emit-llvm -g -c %s -o %t.big.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --max-memory=20 %t.big.bc > %t.big.log 2> %t.big.err // RUN: not grep -q "MALLOC FAILED" %t.big.log // RUN: not grep -q "DONE" %t.big.log -// RUN: grep "WARNING: killing 1 states (over memory cap)" %t.klee-out/warnings.txt +// RUN: grep "WARNING: killing 1 states (over memory cap" %t.klee-out/warnings.txt #include #include -- cgit 1.4.1