3 files changed, 148 insertions, 0 deletions
diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp
index 5cf57069..c6fc9d3a 100644
--- a/lib/Module/Checks.cpp
+++ b/lib/Module/Checks.cpp
@@ -94,3 +94,62 @@ bool DivCheckPass::runOnModule(Module &M) {
   }
   return moduleChanged;
 }
+
+char OvershiftCheckPass::ID;
+
+bool OvershiftCheckPass::runOnModule(Module &M) {
+  Function *overshiftCheckFunction = 0;
+
+  bool moduleChanged = false;
+
+  for (Module::iterator f = M.begin(), fe = M.end(); f != fe; ++f) {
+    for (Function::iterator b = f->begin(), be = f->end(); b != be; ++b) {
+      for (BasicBlock::iterator i = b->begin(), ie = b->end(); i != ie; ++i) {
+          if (BinaryOperator* binOp = dyn_cast<BinaryOperator>(i)) {
+          // find all shift instructions
+          Instruction::BinaryOps opcode = binOp->getOpcode();
+
+          if (opcode == Instruction::Shl ||
+              opcode == Instruction::LShr ||
+              opcode == Instruction::AShr ) {
+            std::vector<llvm::Value*> args;
+
+            // Determine bit width of first operand
+            uint64_t bitWidth=i->getOperand(0)->getType()->getScalarSizeInBits();
+
+            ConstantInt *bitWidthC = ConstantInt::get(Type::getInt64Ty(getGlobalContext()),bitWidth,false);
+            args.push_back(bitWidthC);
+
+            CastInst *shift =
+              CastInst::CreateIntegerCast(i->getOperand(1),
+                                          Type::getInt64Ty(getGlobalContext()),
+                                          false,  /* sign doesn't matter */
+                                          "int_cast_to_i64",
+                                          i);
+            args.push_back(shift);
+
+
+            // Lazily bind the function to avoid always importing it.
+            if (!overshiftCheckFunction) {
+              Constant *fc = M.getOrInsertFunction("klee_overshift_check",
+                                                   Type::getVoidTy(getGlobalContext()),
+                                                   Type::getInt64Ty(getGlobalContext()),
+                                                   Type::getInt64Ty(getGlobalContext()),
+                                                   NULL);
+              overshiftCheckFunction = cast<Function>(fc);
+            }
+
+            // Inject CallInstr to check if overshifting possible
+#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0)
+            CallInst::Create(overshiftCheckFunction, args, "", &*i);
+#else
+            CallInst::Create(overshiftCheckFunction, args.begin(), args.end(), "", &*i);
+#endif
+            moduleChanged = true;
+          }
+        }
+      }
+    }
+  }
+  return moduleChanged;
+}
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index 0d0244dd..ff13efda 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -57,6 +57,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;
@@ -224,6 +228,52 @@ static void forceImport(Module *m, const char *name, LLVM_TYPE_Q Type *retType,
 }
 #endif
 
+/// 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()) {
@@ -284,6 +334,7 @@ void KModule::prepare(const Interpreter::ModuleOptions &opts,
   PassManager pm;
   pm.add(new RaiseAsmPass());
   if (opts.CheckDivZero) pm.add(new DivCheckPass());
+  if (opts.CheckOvershift) pm.add(new OvershiftCheckPass());
   // FIXME: This false here is to work around a bug in
   // IntrinsicLowering which caches values which may eventually be
   // deleted (via RAUW). This can be removed once LLVM fixes this
@@ -328,6 +379,19 @@ 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).
+   */
+  if (opts.CheckDivZero)
+    inlineChecks(module, "klee_div_zero_check");
+  if (opts.CheckOvershift)
+    inlineChecks(module, "klee_overshift_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/lib/Module/Passes.h b/lib/Module/Passes.h
index d83e57ec..0c294daa 100644
--- a/lib/Module/Passes.h
+++ b/lib/Module/Passes.h
@@ -143,6 +143,31 @@ public:
   virtual bool runOnModule(llvm::Module &M);
 };
 
+/// This pass injects checks to check for overshifting.
+///
+/// Overshifting is where a Shl, LShr or AShr is performed
+/// where the shift amount is greater than width of the bitvector
+/// being shifted.
+/// In LLVM (and in C/C++) this undefined behaviour!
+///
+/// Example:
+/// \code
+///     unsigned char x=15;
+///     x << 4 ; // Defined behaviour
+///     x << 8 ; // Undefined behaviour
+///     x << 255 ; // Undefined behaviour
+/// \endcode
+class OvershiftCheckPass : public llvm::ModulePass {
+  static char ID;
+public:
+#if LLVM_VERSION_CODE < LLVM_VERSION(2, 8)
+  OvershiftCheckPass(): ModulePass((intptr_t) &ID) {}
+#else
+  OvershiftCheckPass(): ModulePass(ID) {}
+#endif
+  virtual bool runOnModule(llvm::Module &M);
+};
+
 /// LowerSwitchPass - Replace all SwitchInst instructions with chained branch
 /// instructions.  Note that this cannot be a BasicBlock pass because it
 /// modifies the CFG!