From ea2b756666fa60b47efe16510d81c3b29beab4df Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Sun, 6 Nov 2016 11:46:40 +0100 Subject: Check for stack overflow in a tested program Check if a state reaches the maximum number of stack frames allowed. To be performant, the number of stack frames are checked. In comparison, native execution checks the size of the stack. Still, this is good enough to find possible stack overflows. The limit can be changed with `-max-stack-frames`. The current default is 8192 frames. --- lib/Core/Executor.cpp | 15 +++++++++++++++ test/Feature/StackOverflow.c | 16 ++++++++++++++++ 2 files changed, 31 insertions(+) create mode 100644 test/Feature/StackOverflow.c diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 099123cd..0dac7abe 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -302,6 +302,12 @@ namespace { MaxMemoryInhibit("max-memory-inhibit", cl::desc("Inhibit forking at memory cap (vs. random terminate) (default=on)"), cl::init(true)); + + cl::opt RuntimeMaxStackFrames( + "max-stack-frames", + cl::desc("Terminates a state after the limit of stack frames is reached " + "(default=8192). Disable check with 0."), + cl::init(8192)); } @@ -1283,11 +1289,20 @@ void Executor::executeCall(ExecutionState &state, if (InvokeInst *ii = dyn_cast(i)) transferToBasicBlock(ii->getNormalDest(), i->getParent(), state); } else { + // Check if maximum stack size was reached. + // We currently only count the number of stack frames + if (RuntimeMaxStackFrames && state.stack.size() > RuntimeMaxStackFrames) { + terminateStateEarly(state, "Maximum stack size reached."); + klee_warning("Maximum stack size reached."); + return; + } + // FIXME: I'm not really happy about this reliance on prevPC but it is ok, I // guess. This just done to avoid having to pass KInstIterator everywhere // instead of the actual instruction, since we can't make a KInstIterator // from just an instruction (unlike LLVM). KFunction *kf = kmodule->functionMap[f]; + state.pushFrame(state.prevPC, kf); state.pc = kf->instructions; diff --git a/test/Feature/StackOverflow.c b/test/Feature/StackOverflow.c new file mode 100644 index 00000000..837d3db8 --- /dev/null +++ b/test/Feature/StackOverflow.c @@ -0,0 +1,16 @@ +// RUN: %llvmgcc -emit-llvm -g -c -o %t.bc %s +// RUN: rm -rf %t.klee-out +// RUN: %klee --output-dir=%t.klee-out %t.bc > %t.output.log 2>&1 +// RUN: FileCheck -input-file=%t.output.log %s + +void recursive(unsigned nr){ + if (nr == 0) + return; + recursive(nr-1); +} + +int main() { + recursive(10000); + return 0; +} +// CHECK: Maximum stack size reached -- cgit 1.4.1