diff options
author | Martin Nowack <martin@se.inf.tu-dresden.de> | 2013-11-13 23:53:46 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2013-12-19 15:45:03 +0000 |
commit | 17ec611bb5ada13350a72f2e1de439499128c62f (patch) | |
tree | 34cbb2376165f53992c45c2a0281b5953c897e23 | |
parent | a329a133d66a86249a3b1ce8025a88f4c0b197c4 (diff) | |
download | klee-17ec611bb5ada13350a72f2e1de439499128c62f.tar.gz |
Allow to specify KLEE-internal functions
KLEE provides runtime library functions to do detection of bugs (e.g. overflow). This runtime functions are not the location of the bugs but it is the next non-runtime library function from the stack. Use the caller inside that function to indicate where the bug is.
-rw-r--r-- | include/klee/Internal/Module/KModule.h | 7 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 42 | ||||
-rw-r--r-- | lib/Core/Executor.h | 5 | ||||
-rw-r--r-- | lib/Module/KModule.cpp | 24 |
4 files changed, 67 insertions, 11 deletions
diff --git a/include/klee/Internal/Module/KModule.h b/include/klee/Internal/Module/KModule.h index 86be131b..80672b5e 100644 --- a/include/klee/Internal/Module/KModule.h +++ b/include/klee/Internal/Module/KModule.h @@ -110,6 +110,13 @@ namespace klee { Cell *constantTable; + // Functions which are part of KLEE runtime + std::set<const llvm::Function*> internalFunctions; + + private: + // Mark function with functionName as part of the KLEE runtime + void addInternalFunction(const char* functionName); + public: KModule(llvm::Module *_module); ~KModule(); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index ef55f21f..f01fa4ee 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2729,16 +2729,54 @@ void Executor::terminateStateOnExit(ExecutionState &state) { terminateState(state); } +const InstructionInfo & Executor::getLastNonKleeInternalInstruction(const ExecutionState &state, + Instruction ** lastInstruction) { + // unroll the stack of the applications state and find + // the last instruction which is not inside a KLEE internal function + ExecutionState::stack_ty::const_reverse_iterator it = state.stack.rbegin(), + itE = state.stack.rend(); + + // don't check beyond the outermost function (i.e. main()) + itE--; + + const InstructionInfo * ii = 0; + if (kmodule->internalFunctions.count(it->kf->function) == 0){ + ii = state.prevPC->info; + *lastInstruction = state.prevPC->inst; + } + + // wind up the stack and check if we are in a KLEE internal function + for (;it != itE; ++it) { + // check calling instruction and if it is contained in a KLEE internal function + const Function * f = (*it->caller).inst->getParent()->getParent(); + if (kmodule->internalFunctions.count(f)){ + ii = 0; + continue; + } + if (!ii){ + ii = (*it->caller).info; + *lastInstruction = (*it->caller).inst; + } + } + + if (!ii) { + // something went wrong, play safe and return the current instruction info + *lastInstruction = state.prevPC->inst; + return *state.prevPC->info; + } + return *ii; +} void Executor::terminateStateOnError(ExecutionState &state, const llvm::Twine &messaget, const char *suffix, const llvm::Twine &info) { std::string message = messaget.str(); static std::set< std::pair<Instruction*, std::string> > emittedErrors; - const InstructionInfo &ii = *state.prevPC->info; + Instruction * lastInst; + const InstructionInfo &ii = getLastNonKleeInternalInstruction(state, &lastInst); if (EmitAllErrors || - emittedErrors.insert(std::make_pair(state.prevPC->inst, message)).second) { + emittedErrors.insert(std::make_pair(lastInst, message)).second) { if (ii.file != "") { klee_message("ERROR: %s:%d: %s", ii.file.c_str(), ii.line, message.c_str()); } else { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index b7318a2c..7d82332c 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -340,6 +340,11 @@ private: /// Get textual information regarding a memory address. std::string getAddressInfo(ExecutionState &state, ref<Expr> address) const; + // Determines the \param lastInstruction of the \param state which is not KLEE + // internal and returns its InstructionInfo + const InstructionInfo & getLastNonKleeInternalInstruction(const ExecutionState &state, + llvm::Instruction** lastInstruction); + // remove state from queue and delete void terminateState(ExecutionState &state); // call exit handler and terminate state diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index d889b51f..4bc10604 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -269,6 +269,17 @@ static void inlineChecks(Module *module, const char * functionName) { DEBUG( klee_message("Tried to inline calls to %s. %u successes, %u failures",functionName, successCount, failCount) ); } +void KModule::addInternalFunction(const char* functionName){ + Function* internalFunction = module->getFunction(functionName); + if (!internalFunction) { + DEBUG_WITH_TYPE("KModule", klee_warning( + "Failed to add internal function %s. Not found.", functionName)); + return ; + } + DEBUG( klee_message("Added function %s.",functionName)); + internalFunctions.insert(internalFunction); +} + void KModule::prepare(const Interpreter::ModuleOptions &opts, InterpreterHandler *ih) { if (!MergeAtExit.empty()) { @@ -374,17 +385,12 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, #endif module = linkWithLibrary(module, path.c_str()); - /* In order for KLEE to report ALL errors at instrumented - * locations the instrumentation call (e.g. "klee_div_zero_check") - * must be inlined. Otherwise one of the instructions in the - * instrumentation function will be used as the the location of - * the error which means that the error cannot be recorded again - * ( unless -emit-all-errors is used). - */ + // Add internal functions which are not used to check if instructions + // have been already visited if (opts.CheckDivZero) - inlineChecks(module, "klee_div_zero_check"); + addInternalFunction("klee_div_zero_check"); if (opts.CheckOvershift) - inlineChecks(module, "klee_overshift_check"); + addInternalFunction("klee_overshift_check"); // Needs to happen after linking (since ctors/dtors can be modified) |