diff options
| -rw-r--r-- | lib/Module/KModule.cpp | 61 | ||||
| -rw-r--r-- | test/Feature/consecutive_divide_by_zero.c | 30 |
2 files changed, 91 insertions, 0 deletions
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp index 1629bb79..a6047536 100644 --- a/lib/Module/KModule.cpp +++ b/lib/Module/KModule.cpp @@ -47,6 +47,10 @@ #endif #include "llvm/Transforms/Scalar.h" +#include <llvm/Transforms/Utils/Cloning.h> +#include <llvm/Support/InstIterator.h> +#include <llvm/Support/Debug.h> + #include <sstream> using namespace llvm; @@ -212,6 +216,52 @@ static void forceImport(Module *m, const char *name, LLVM_TYPE_Q Type *retType, } } +/// This function will take try to inline all calls to \p functionName +/// in the module \p module . +/// +/// It is intended that this function be used for inling calls to +/// check functions like <tt>klee_div_zero_check()</tt> +static void inlineChecks(Module *module, const char * functionName) { + std::vector<CallInst*> checkCalls; + Function* runtimeCheckCall = module->getFunction(functionName); + if (runtimeCheckCall == 0) + { + DEBUG( klee_warning("Failed to inline %s because no calls were made to it in module", functionName) ); + return; + } + + // Iterate through instructions in module and collect all + // call instructions to "functionName" that we care about. + for (Module::iterator f = module->begin(), fe = module->end(); f != fe; ++f) { + for (inst_iterator i=inst_begin(f), ie = inst_end(f); i != ie; ++i) { + if ( CallInst* ci = dyn_cast<CallInst>(&*i) ) + { + if ( ci->getCalledFunction() == runtimeCheckCall) + checkCalls.push_back(ci); + } + } + } + + unsigned int successCount=0; + unsigned int failCount=0; + InlineFunctionInfo IFI(0,0); + for ( std::vector<CallInst*>::iterator ci = checkCalls.begin(), + cie = checkCalls.end(); + ci != cie; ++ci) + { + // Try to inline the function + if (InlineFunction(*ci,IFI)) + ++successCount; + else + { + ++failCount; + klee_warning("Failed to inline function %s", functionName); + } + } + + DEBUG( klee_message("Tried to inline calls to %s. %u successes, %u failures",functionName, successCount, failCount) ); +} + void KModule::prepare(const Interpreter::ModuleOptions &opts, InterpreterHandler *ih) { if (!MergeAtExit.empty()) { @@ -312,6 +362,17 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts, path.appendComponent("libkleeRuntimeIntrinsic.bca"); 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). + */ + if (opts.CheckDivZero) + inlineChecks(module, "klee_div_zero_check"); + + // Needs to happen after linking (since ctors/dtors can be modified) // and optimization (since global optimization can rewrite lists). injectStaticConstructorsAndDestructors(module); diff --git a/test/Feature/consecutive_divide_by_zero.c b/test/Feature/consecutive_divide_by_zero.c new file mode 100644 index 00000000..c1185870 --- /dev/null +++ b/test/Feature/consecutive_divide_by_zero.c @@ -0,0 +1,30 @@ +// RUN: %llvmgcc -emit-llvm -c -g -O0 %s -o %t.bc +// RUN: %klee -check-div-zero -emit-all-errors=0 %t.bc 2> %t.log +// RUN: grep "completed paths = 3" %t.log +// RUN: grep "generated tests = 3" %t.log +// RUN: grep "consecutive_divide_by_zero.c:24: divide by zero" %t.log +// RUN: grep "consecutive_divide_by_zero.c:27: divide by zero" %t.log + +/* This test case captures a bug where two distinct division +* by zero errors are treated as the same error and so +* only one test case is generated EVEN IF THERE ARE MULTIPLE +* DISTINCT ERRORS! +*/ +int main() +{ + unsigned int a=15; + unsigned int b=15; + volatile unsigned int d1; + volatile unsigned int d2; + + klee_make_symbolic(&d1, sizeof(d1),"divisor1"); + klee_make_symbolic(&d2, sizeof(d2),"divisor2"); + + // deliberate division by zero possible + unsigned int result1 = a / d1; + + // another deliberate division by zero possible + unsigned int result2 = b / d2; + + return 0; +} |