about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2013-08-30 16:43:30 +0100
committerDan Liew <daniel.liew@imperial.ac.uk>2013-09-02 16:45:06 +0100
commitf8301282120cc3cc58d641ddc99f92b14d894692 (patch)
tree0c0f0a308496ee1abb050ceac3a1b95727a1390f
parent8cc2105aeb16e081a2ddd1128b6455cbdcb2ed3d (diff)
downloadklee-f8301282120cc3cc58d641ddc99f92b14d894692.tar.gz
Fixed bug where divide by zero bugs would only be detected once in a program
even if there were many divide by zero bugs.

The fix basically inlines all function calls to klee_div_zero_check()
so that each call to klee_report_error() is a unique instruction
for each instrumentation of a divide operation.

It also seems that inlining the call "magically" fixed the debug information
(file and line number) of the instruction so that the debug information on the
inlined instructions matches that of the instrumented division instruction.

Note that the command line option -emit-all-errors could be used to
workaround the bug fixed in this commit.
-rw-r--r--lib/Module/KModule.cpp61
-rw-r--r--test/Feature/consecutive_divide_by_zero.c30
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;
+}