Merge pull request #68 from MartinNowack/feature_kleeInternalFunctions

Feature klee internal functions

3 files changed, 63 insertions, 80 deletions

diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp
index 79fd4afc..80b6b245 100644
--- a/lib/Module/Checks.cpp
+++ b/lib/Module/Checks.cpp
@@ -83,7 +83,12 @@ bool DivCheckPass::runOnModule(Module &M) {
               divZeroCheckFunction = cast<Function>(fc);
             }
 
-	    CallInst::Create(divZeroCheckFunction, denominator, "", &*i);
+            CallInst * ci = CallInst::Create(divZeroCheckFunction, denominator, "", &*i);
+
+            // Set debug location of checking call to that of the div/rem
+            // operation so error locations are reported in the correct
+            // location.
+            ci->setDebugLoc(binOp->getDebugLoc());
             moduleChanged = true;
           }
         }
@@ -138,11 +143,14 @@ bool OvershiftCheckPass::runOnModule(Module &M) {
             }
 
             // Inject CallInstr to check if overshifting possible
+            CallInst* ci =
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 0)
             CallInst::Create(overshiftCheckFunction, args, "", &*i);
 #else
             CallInst::Create(overshiftCheckFunction, args.begin(), args.end(), "", &*i);
 #endif
+            // set debug information from binary operand to preserve it
+            ci->setDebugLoc(binOp->getDebugLoc());
             moduleChanged = true;
           }
         }
diff --git a/lib/Module/InstructionInfoTable.cpp b/lib/Module/InstructionInfoTable.cpp
index 301db1ff..19d7e511 100644
--- a/lib/Module/InstructionInfoTable.cpp
+++ b/lib/Module/InstructionInfoTable.cpp
@@ -33,6 +33,7 @@
 #include "llvm/Analysis/DebugInfo.h"
 #endif
 #include "llvm/Analysis/ValueTracking.h"
+#include "llvm/Support/Debug.h"
 
 #include <map>
 #include <string>
@@ -108,64 +109,35 @@ InstructionInfoTable::InstructionInfoTable(Module *m)
 
   for (Module::iterator fnIt = m->begin(), fn_ie = m->end(); 
        fnIt != fn_ie; ++fnIt) {
-    const std::string *initialFile = &dummyString;
-    unsigned initialLine = 0;
-
-    // It may be better to look for the closest stoppoint to the entry
-    // following the CFG, but it is not clear that it ever matters in
-    // practice.
-    for (inst_iterator it = inst_begin(fnIt), ie = inst_end(fnIt);
-         it != ie; ++it)
-      if (getInstructionDebugInfo(&*it, initialFile, initialLine))
-        break;
-    
-    typedef std::map<BasicBlock*, std::pair<const std::string*,unsigned> > 
-      sourceinfo_ty;
-    sourceinfo_ty sourceInfo;
-    for (llvm::Function::iterator bbIt = fnIt->begin(), bbie = fnIt->end(); 
-         bbIt != bbie; ++bbIt) {
-      std::pair<sourceinfo_ty::iterator, bool>
-        res = sourceInfo.insert(std::make_pair(bbIt,
-                                               std::make_pair(initialFile,
-                                                              initialLine)));
-      if (!res.second)
-        continue;
-
-      std::vector<BasicBlock*> worklist;
-      worklist.push_back(bbIt);
-
-      do {
-        BasicBlock *bb = worklist.back();
-        worklist.pop_back();
-
-        sourceinfo_ty::iterator si = sourceInfo.find(bb);
-        assert(si != sourceInfo.end());
-        const std::string *file = si->second.first;
-        unsigned line = si->second.second;
-        
-        for (BasicBlock::iterator it = bb->begin(), ie = bb->end();
-             it != ie; ++it) {
-          Instruction *instr = it;
-          unsigned assemblyLine = 0;
-          std::map<const Instruction*, unsigned>::const_iterator ltit = 
-            lineTable.find(instr);
-          if (ltit!=lineTable.end())
-            assemblyLine = ltit->second;
-          getInstructionDebugInfo(instr, file, line);
-          infos.insert(std::make_pair(instr,
-                                      InstructionInfo(id++,
-                                                      *file,
-                                                      line,
-                                                      assemblyLine)));        
-        }
-        
-        for (succ_iterator it = succ_begin(bb), ie = succ_end(bb); 
-             it != ie; ++it) {
-          if (sourceInfo.insert(std::make_pair(*it,
-                                               std::make_pair(file, line))).second)
-            worklist.push_back(*it);
-        }
-      } while (!worklist.empty());
+
+    for (inst_iterator it = inst_begin(fnIt), ie = inst_end(fnIt); it != ie;
+        ++it) {
+      const std::string *initialFile = &dummyString;
+      unsigned initialLine = 0;
+      Instruction *instr = &*it;
+      unsigned assemblyLine = 0;
+
+      std::map<const Instruction*, unsigned>::const_iterator ltit =
+        lineTable.find(instr);
+      if (ltit!=lineTable.end())
+        assemblyLine = ltit->second;
+      if (getInstructionDebugInfo(instr, initialFile, initialLine))
+      {
+        infos.insert(std::make_pair(instr,
+                                    InstructionInfo(id++,
+                                                    *initialFile,
+                                                    initialLine,
+                                                    assemblyLine)));
+        DEBUG_WITH_TYPE("klee_obtained_debug", dbgs() <<
+          "Instruction: \"" << *instr << "\" (assembly line " << assemblyLine <<
+          ") has debug location " << *initialFile << ":" << initialLine << "\n");
+      }
+      else
+      {
+        DEBUG_WITH_TYPE("klee_missing_debug", dbgs() <<
+          "Instruction: \"" << *instr << "\" (assembly line " << assemblyLine <<
+          ") is missing debug info.\n");
+      }
     }
   }
 }
diff --git a/lib/Module/KModule.cpp b/lib/Module/KModule.cpp
index d889b51f..34e5f60c 100644
--- a/lib/Module/KModule.cpp
+++ b/lib/Module/KModule.cpp
@@ -229,7 +229,7 @@ static void forceImport(Module *m, const char *name, LLVM_TYPE_Q Type *retType,
 /// 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;
+  std::vector<CallSite> checkCalls;
     Function* runtimeCheckCall = module->getFunction(functionName);
     if (runtimeCheckCall == 0)
     {
@@ -237,22 +237,19 @@ static void inlineChecks(Module *module, const char * 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);
-        }
+    for (Value::use_iterator i = runtimeCheckCall->use_begin(),
+        e = runtimeCheckCall->use_end(); i != e; ++i)
+      if (isa<InvokeInst>(*i) || isa<CallInst>(*i)) {
+        CallSite cs(*i);
+        if (!cs.getCalledFunction())
+          continue;
+        checkCalls.push_back(cs);
       }
-    }
 
     unsigned int successCount=0;
     unsigned int failCount=0;
     InlineFunctionInfo IFI(0,0);
-    for ( std::vector<CallInst*>::iterator ci = checkCalls.begin(),
+    for ( std::vector<CallSite>::iterator ci = checkCalls.begin(),
           cie = checkCalls.end();
           ci != cie; ++ci)
     {
@@ -269,6 +266,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 +382,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)