diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 38 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.h | 4 | ||||
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 43 | ||||
| -rw-r--r-- | lib/Module/IntrinsicCleaner.cpp | 78 |
4 files changed, 120 insertions, 43 deletions
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index 59e269cb..f06ae4f5 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -108,6 +108,12 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { // operator new(unsigned long) add("_Znwm", handleNew, true), + // clang -fsanitize=unsigned-integer-overflow + add("__ubsan_handle_add_overflow", handleAddOverflow, false), + add("__ubsan_handle_sub_overflow", handleSubOverflow, false), + add("__ubsan_handle_mul_overflow", handleMulOverflow, false), + add("__ubsan_handle_divrem_overflow", handleDivRemOverflow, false), + #undef addDNR #undef add }; @@ -707,3 +713,35 @@ void SpecialFunctionHandler::handleMarkGlobal(ExecutionState &state, mo->isGlobal = true; } } + +void SpecialFunctionHandler::handleAddOverflow(ExecutionState &state, + KInstruction *target, + std::vector<ref<Expr> > &arguments) { + executor.terminateStateOnError(state, + "overflow on unsigned addition", + "overflow.err"); +} + +void SpecialFunctionHandler::handleSubOverflow(ExecutionState &state, + KInstruction *target, + std::vector<ref<Expr> > &arguments) { + executor.terminateStateOnError(state, + "overflow on unsigned subtraction", + "overflow.err"); +} + +void SpecialFunctionHandler::handleMulOverflow(ExecutionState &state, + KInstruction *target, + std::vector<ref<Expr> > &arguments) { + executor.terminateStateOnError(state, + "overflow on unsigned multiplication", + "overflow.err"); +} + +void SpecialFunctionHandler::handleDivRemOverflow(ExecutionState &state, + KInstruction *target, + std::vector<ref<Expr> > &arguments) { + executor.terminateStateOnError(state, + "overflow on division or remainder", + "overflow.err"); +} diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index f68c6edb..d52b8fc5 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -132,6 +132,10 @@ namespace klee { HANDLER(handleUnderConstrained); HANDLER(handleWarning); HANDLER(handleWarningOnce); + HANDLER(handleAddOverflow); + HANDLER(handleMulOverflow); + HANDLER(handleSubOverflow); + HANDLER(handleDivRemOverflow); #undef HANDLER }; } // End klee namespace diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index c4a6876e..c780ae90 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -230,22 +230,19 @@ void ExprSMTLIBPrinter::printFullExpression( printCastExpr(cast<CastExpr>(e)); return; - case Expr::Ne: - printNotEqualExpr(cast<NeExpr>(e)); - return; - case Expr::Select: // the if-then-else expression. printSelectExpr(cast<SelectExpr>(e), expectedSort); return; case Expr::Eq: - /* The "=" operator is special in that it can take any sort but we must - * enforce that both arguments are the same sort. We do this in a lazy way - * by enforcing the second argument is of the same type as the first. + case Expr::Ne: + /* The "=" and distinct operators are special in that it can take any sort + * but we must enforce that both arguments are the same sort. We do this in + * a lazy way by enforcing the second argument is of the same type as the + * first. */ printSortArgsExpr(e, getSort(e->getKid(0))); - return; case Expr::And: @@ -337,32 +334,6 @@ void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr> &e) { *p << ")"; } -void ExprSMTLIBPrinter::printNotEqualExpr(const ref<NeExpr> &e) { - *p << "(not ("; - p->pushIndent(); - *p << "=" - << " "; - p->pushIndent(); - printSeperator(); - - /* The "=" operators allows both sorts. We assume - * that the second argument sort should be forced to be the same sort as the - * first argument - */ - SMTLIB_SORT s = getSort(e->getKid(0)); - - printExpression(e->getKid(0), s); - printSeperator(); - printExpression(e->getKid(1), s); - p->popIndent(); - printSeperator(); - - *p << ")"; - p->popIndent(); - printSeperator(); - *p << ")"; -} - const char *ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr> &e) { switch (e->getKind()) { @@ -407,8 +378,8 @@ const char *ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr> &e) { case Expr::Eq: return "="; - - // Not Equal does not exist directly in SMTLIBv2 + case Expr::Ne: + return "distinct"; case Expr::Ult: return "bvult"; diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index 0f095269..da97621a 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; @@ -116,7 +118,11 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { break; } + case Intrinsic::sadd_with_overflow: + case Intrinsic::ssub_with_overflow: + case Intrinsic::smul_with_overflow: case Intrinsic::uadd_with_overflow: + case Intrinsic::usub_with_overflow: case Intrinsic::umul_with_overflow: { IRBuilder<> builder(ii->getParent(), ii); @@ -124,13 +130,71 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { Value *op2 = ii->getArgOperand(1); Value *result = 0; - if (ii->getIntrinsicID() == Intrinsic::uadd_with_overflow) - result = builder.CreateAdd(op1, op2); - else - result = builder.CreateMul(op1, op2); + Value *result_ext = 0; + Value *overflow = 0; + + unsigned int bw = op1->getType()->getPrimitiveSizeInBits(); + unsigned int bw2 = op1->getType()->getPrimitiveSizeInBits()*2; + + if ((ii->getIntrinsicID() == Intrinsic::uadd_with_overflow) || + (ii->getIntrinsicID() == Intrinsic::usub_with_overflow) || + (ii->getIntrinsicID() == Intrinsic::umul_with_overflow)) { + + Value *op1ext = + builder.CreateZExt(op1, IntegerType::get(M.getContext(), bw2)); + Value *op2ext = + builder.CreateZExt(op2, IntegerType::get(M.getContext(), bw2)); + Value *int_max_s = + ConstantInt::get(op1->getType(), APInt::getMaxValue(bw)); + Value *int_max = + builder.CreateZExt(int_max_s, IntegerType::get(M.getContext(), bw2)); + + if (ii->getIntrinsicID() == Intrinsic::uadd_with_overflow){ + result_ext = builder.CreateAdd(op1ext, op2ext); + } else if (ii->getIntrinsicID() == Intrinsic::usub_with_overflow){ + result_ext = builder.CreateSub(op1ext, op2ext); + } else if (ii->getIntrinsicID() == Intrinsic::umul_with_overflow){ + result_ext = builder.CreateMul(op1ext, op2ext); + } + overflow = builder.CreateICmpUGT(result_ext, int_max); + + } else if ((ii->getIntrinsicID() == Intrinsic::sadd_with_overflow) || + (ii->getIntrinsicID() == Intrinsic::ssub_with_overflow) || + (ii->getIntrinsicID() == Intrinsic::smul_with_overflow)) { + + Value *op1ext = + builder.CreateSExt(op1, IntegerType::get(M.getContext(), bw2)); + Value *op2ext = + builder.CreateSExt(op2, IntegerType::get(M.getContext(), bw2)); + Value *int_max_s = + ConstantInt::get(op1->getType(), APInt::getSignedMaxValue(bw)); + Value *int_min_s = + ConstantInt::get(op1->getType(), APInt::getSignedMinValue(bw)); + Value *int_max = + builder.CreateSExt(int_max_s, IntegerType::get(M.getContext(), bw2)); + Value *int_min = + builder.CreateSExt(int_min_s, IntegerType::get(M.getContext(), bw2)); + + if (ii->getIntrinsicID() == Intrinsic::sadd_with_overflow){ + result_ext = builder.CreateAdd(op1ext, op2ext); + } else if (ii->getIntrinsicID() == Intrinsic::ssub_with_overflow){ + result_ext = builder.CreateSub(op1ext, op2ext); + } else if (ii->getIntrinsicID() == Intrinsic::smul_with_overflow){ + result_ext = builder.CreateMul(op1ext, op2ext); + } + overflow = builder.CreateOr(builder.CreateICmpSGT(result_ext, int_max), + builder.CreateICmpSLT(result_ext, int_min)); + } - Value *overflow = builder.CreateICmpULT(result, op1); - + // This trunc cound be replaced by a more general trunc replacement + // that allows to detect also undefined behavior in assignments or + // overflow in operation with integers whose dimension is smaller than + // int's dimension, e.g. + // uint8_t = uint8_t + uint8_t; + // if one desires the wrapping should write + // uint8_t = (uint8_t + uint8_t) & 0xFF; + // before this, must check if it has side effects on other operations + result = builder.CreateTrunc(result_ext, op1->getType()); Value *resultStruct = builder.CreateInsertValue(UndefValue::get(ii->getType()), result, 0); resultStruct = builder.CreateInsertValue(resultStruct, overflow, 1); |