about summary refs log tree commit diff homepage
path: root/lib/Module
diff options
context:
space:
mode:
authorMartin Nowack <m.nowack@imperial.ac.uk>2018-07-29 16:16:09 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-10-24 14:15:25 +0300
commit5bca619d7c11273e9492fa01fc7492e2cbb4eff5 (patch)
tree5640badf0e891e2175b5ebb5324a34e1cee6fe18 /lib/Module
parente70783b86bf3427bccd3d0b8cec858b888b8c887 (diff)
downloadklee-5bca619d7c11273e9492fa01fc7492e2cbb4eff5.tar.gz
DivCheck do not instrument multiple times
DivChecker can be executed multiple times due to the new linking
process.
Avoid instrumenting div instructions multiple times by annotating
checked instructions with marker. Only unmarked div instructions will be
instrumented.
Diffstat (limited to 'lib/Module')
-rw-r--r--lib/Module/Checks.cpp9
1 files changed, 9 insertions, 0 deletions
diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp
index b6aadce4..2489b55c 100644
--- a/lib/Module/Checks.cpp
+++ b/lib/Module/Checks.cpp
@@ -11,6 +11,8 @@
 
 #include "klee/Config/Version.h"
 
+#include "KLEEIRMetaData.h"
+
 #include "llvm/IR/Constants.h"
 #include "llvm/IR/DataLayout.h"
 #include "llvm/IR/DerivedTypes.h"
@@ -54,6 +56,11 @@ bool DivCheckPass::runOnModule(Module &M) {
           if (!coOp->isZeroValue())
             continue;
         }
+
+        // Check if the operand is already checked by "klee_div_zero_check"
+        if (KleeIRMetaData::hasAnnotation(I, "klee.check.div", "True"))
+          continue;
+        divInstruction.push_back(binOp);
       }
     }
   }
@@ -63,6 +70,7 @@ bool DivCheckPass::runOnModule(Module &M) {
     return false;
 
   LLVMContext &ctx = M.getContext();
+  KleeIRMetaData md(ctx);
   auto divZeroCheckFunction = cast<Function>(
       M.getOrInsertFunction("klee_div_zero_check", Type::getVoidTy(ctx),
                             Type::getInt64Ty(ctx), NULL));
@@ -74,6 +82,7 @@ bool DivCheckPass::runOnModule(Module &M) {
                               false, /* sign doesn't matter */
                               "int_cast_to_i64");
     Builder.CreateCall(divZeroCheckFunction, denominator);
+    md.addAnnotation(*divInst, "klee.check.div", "True");
   }
 
   return true;