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:51:32 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2018-10-24 14:15:25 +0300
commitecc7fae9cbac9aa970aac072276e5bca1c583c02 (patch)
treecb6130e01e06aa2b749d5c5a5a9a462bc1842ee8 /lib/Module
parentaba37b07e909b30636e06f33b456af3abaa8ed0e (diff)
downloadklee-ecc7fae9cbac9aa970aac072276e5bca1c583c02.tar.gz
ShiftChecker: Instrument shift instructions only once
As the shift checker could be executed multiple times, we need to avoid
that shift instructions are instrumented multiple times as well.

Mark the instrumented instruction using metadata and avoid it in
successive runs.
Diffstat (limited to 'lib/Module')
-rw-r--r--lib/Module/Checks.cpp5
1 files changed, 5 insertions, 0 deletions
diff --git a/lib/Module/Checks.cpp b/lib/Module/Checks.cpp
index 53ba4266..9286c491 100644
--- a/lib/Module/Checks.cpp
+++ b/lib/Module/Checks.cpp
@@ -116,6 +116,9 @@ bool OvershiftCheckPass::runOnModule(Module &M) {
             continue;
         }
 
+        if (KleeIRMetaData::hasAnnotation(I, "klee.check.shift", "True"))
+          continue;
+
         shiftInstructions.push_back(binOp);
       }
     }
@@ -126,6 +129,7 @@ bool OvershiftCheckPass::runOnModule(Module &M) {
 
   // Retrieve the checker function
   auto &ctx = M.getContext();
+  KleeIRMetaData md(ctx);
   auto overshiftCheckFunction = cast<Function>(M.getOrInsertFunction(
       "klee_overshift_check", Type::getVoidTy(ctx), Type::getInt64Ty(ctx),
       Type::getInt64Ty(ctx), NULL));
@@ -147,6 +151,7 @@ bool OvershiftCheckPass::runOnModule(Module &M) {
     args.push_back(shiftValue);
 
     Builder.CreateCall(overshiftCheckFunction, args);
+    md.addAnnotation(*shiftInst, "klee.check.shift", "True");
   }
 
   return true;