From 5bca619d7c11273e9492fa01fc7492e2cbb4eff5 Mon Sep 17 00:00:00 2001
From: Martin Nowack <m.nowack@imperial.ac.uk>
Date: Sun, 29 Jul 2018 16:16:09 +0100
Subject: 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.
---
 lib/Module/Checks.cpp | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'lib/Module')

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;
-- 
cgit 1.4.1