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.

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;