diff options
author | Luca Dariz <l.dariz@imamoter.cnr.t> | 2014-09-23 14:52:00 +0200 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2015-02-13 18:49:49 +0000 |
commit | dbe13e13a215aa7212b5737dd8903699301a4940 (patch) | |
tree | 95981808ecab4298b54544bc5c28a1b9a1373b1b /lib | |
parent | 64a404f89da5aa6a99e688c007c56f1f422541bc (diff) | |
download | klee-dbe13e13a215aa7212b5737dd8903699301a4940.tar.gz |
Fix overflow detection in unsigned multiplication
Previously the check was done as unsigned int a, b, c; c = a * b; if (c < a) // error but it is wrong, since it catches only a subset of all the possible overflows. This patch improves the check as unsigned int a, b, c; if ((a > 1) && (b > 1){ if ((UINT_MAX/a) < b) // error } An additional case has been added to the tests, with two 32-bit values that cause overflow and are not detected by the old check. It is also necessary to break the lowering procedure in case the current BasicBlock is splitted; in this case it was necessary in order not to trigger the division by 0 error.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Module/IntrinsicCleaner.cpp | 38 |
1 files changed, 36 insertions, 2 deletions
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index ebdbd3a6..9d4f0fec 100644 --- a/lib/Module/IntrinsicCleaner.cpp +++ b/lib/Module/IntrinsicCleaner.cpp @@ -66,13 +66,15 @@ bool IntrinsicCleanerPass::runOnModule(Module &M) { bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { bool dirty = false; + bool block_split=false; #if LLVM_VERSION_CODE <= LLVM_VERSION(3, 1) unsigned WordSize = TargetData.getPointerSizeInBits() / 8; #else unsigned WordSize = DataLayout.getPointerSizeInBits() / 8; #endif - for (BasicBlock::iterator i = b.begin(), ie = b.end(); i != ie;) { + for (BasicBlock::iterator i = b.begin(), ie = b.end(); + (i != ie) && (block_split == false);) { IntrinsicInst *ii = dyn_cast<IntrinsicInst>(&*i); // increment now since LowerIntrinsic deletion makes iterator invalid. ++i; @@ -120,6 +122,7 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { case Intrinsic::usub_with_overflow: case Intrinsic::umul_with_overflow: { IRBuilder<> builder(ii->getParent(), ii); + Function *F = builder.GetInsertBlock()->getParent(); Value *op1 = ii->getArgOperand(0); Value *op2 = ii->getArgOperand(1); @@ -133,8 +136,39 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { result = builder.CreateSub(op1, op2); overflow = builder.CreateICmpUGT(result, op1); } else if (ii->getIntrinsicID() == Intrinsic::umul_with_overflow){ + BasicBlock *entry = builder.GetInsertBlock(); + entry->setName(Twine(entry->getName(), "_umul_start")); + BasicBlock *cont_of = entry->splitBasicBlock(builder.GetInsertPoint(), + "umul_end"); + BasicBlock *on_of = BasicBlock::Create(builder.getContext(), + "umul_overflow", F, cont_of); + + // remove the branch inserted by splitBasicBlock, we'll add our own + entry->getTerminator()->eraseFromParent(); + builder.SetInsertPoint(entry); + Value *no_overflow = builder.getFalse(); + Value *one = ConstantInt::getSigned(op1->getType(), 1); + Value *op1_g1 = builder.CreateICmpUGT(op1, one); + Value *op2_g1 = builder.CreateICmpUGT(op2, one); + Value *may_of = builder.CreateAnd(op1_g1, op2_g1); + builder.CreateCondBr(may_of, on_of, cont_of); + + builder.SetInsertPoint(on_of); + uint64_t bit_size = op1->getType()->getPrimitiveSizeInBits(); + Value *uint_max = ConstantInt::get(op1->getType(), + APInt::getMaxValue(bit_size)); + Value *div1 = builder.CreateUDiv(uint_max, op1); + Value *overflow1 = builder.CreateICmpUGT(op2, div1); + builder.CreateBr(cont_of); + + builder.SetInsertPoint(cont_of, cont_of->begin()); + PHINode *phi_of = builder.CreatePHI(no_overflow->getType(), 2); + phi_of->addIncoming(overflow1, on_of); + phi_of->addIncoming(no_overflow, entry); + result = builder.CreateMul(op1, op2); - overflow = builder.CreateICmpULT(result, op1); + overflow = phi_of; + block_split = true; } Value *resultStruct = |