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