diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2018-07-29 16:51:32 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2018-10-24 14:15:25 +0300 |
commit | ecc7fae9cbac9aa970aac072276e5bca1c583c02 (patch) | |
tree | cb6130e01e06aa2b749d5c5a5a9a462bc1842ee8 /lib/Module | |
parent | aba37b07e909b30636e06f33b456af3abaa8ed0e (diff) | |
download | klee-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.cpp | 5 |
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; |