Il 14/10/2014 03:25, Mark R. Tuttle ha scritto:
Thanks, Luca. Can you estimate how complete your branch is for the
overflow instrinsics? Is this something I could complete with a bit of
advice from you? -Mark
On Mon, Oct 13, 2014 at 6:00 PM, Luca Dariz <[email protected]
<mailto:[email protected]>> wrote:
Il 13/10/2014 23:47, Mark R. Tuttle ha scritto:
*Can KLEE check for integer overflow?*
Since KLEE is based on STP and STP is based on a theory of bit
vectors,
I had hoped it might be easy for KLEE to check for an overflow
bit.Since
CLANG has -fsanitize=unsigned-integer-__overflow and
-fsanitize=integer I
had hoped it would be easy to compile with these flags and run
KLEE, but
KLEE does not appear to support the LLVM arithmetic with overflow
intrinsics like llvm.uadd.with.overflow.* that CLANG inserts.
Hi Mark,
the implementation of these intrinsics is just incomplete, I started
to expand it to detect unsigned integer overflow in this branch
https://github.com/luckyluke/__klee/tree/detect-overflow
<https://github.com/luckyluke/klee/tree/detect-overflow>.
Best Regards,
Luca Dariz
Hi Mark,
for now only the checks related to -fsanitize=unsigned-integer-overflow
are tested, I started working on -fsanitize=signed-integer-overflow but
it is not complete yet. I attach the temporary patch based on my
detect-overflow branch, if you want to try it or enhance. Please note
that signed multiplication overflow still does not work, and divrem is
missing.
As an advice, in order to consider all the possible corner cases, I
found useful to have a look at the LLVM compiler-rt library, which
contains the code that expand the llvm.*.with.overflow intrinsics, just
in case you want to add some additional checks.
I re-add klee-dev since somehow I left it out of this thread.
Hope this helps,
Luca Dariz
diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp
index e36d180..97a8cdf 100644
--- a/lib/Core/SpecialFunctionHandler.cpp
+++ b/lib/Core/SpecialFunctionHandler.cpp
@@ -112,6 +112,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = {
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
@@ -765,3 +766,11 @@ void SpecialFunctionHandler::handleMulOverflow(ExecutionState &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 601b149..d52b8fc 100644
--- a/lib/Core/SpecialFunctionHandler.h
+++ b/lib/Core/SpecialFunctionHandler.h
@@ -135,6 +135,7 @@ namespace klee {
HANDLER(handleAddOverflow);
HANDLER(handleMulOverflow);
HANDLER(handleSubOverflow);
+ HANDLER(handleDivRemOverflow);
#undef HANDLER
};
} // End klee namespace
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index 9d4f0fe..b8a3339 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -6,7 +6,7 @@
// License. See LICENSE.TXT for details.
//
//===----------------------------------------------------------------------===//
-
+#include <iostream>
#include "Passes.h"
#include "klee/Config/Version.h"
@@ -118,10 +118,14 @@ 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);
+
Function *F = builder.GetInsertBlock()->getParent();
Value *op1 = ii->getArgOperand(0);
@@ -169,7 +173,143 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
result = builder.CreateMul(op1, op2);
overflow = phi_of;
block_split = true;
- }
+
+ } else if (ii->getIntrinsicID() == Intrinsic::sadd_with_overflow){
+ result = builder.CreateAdd(op1, op2);
+ // overflow if ((op2 >= 0) && (result < op1))
+ Value *op2ge0 =
+ builder.CreateICmpSGE(op2,
+ ConstantInt::getSigned(op2->getType(), 0));
+ Value *cond_ge0 =
+ builder.CreateAnd(op2ge0, builder.CreateICmpSLT(result, op1));
+ // overflow if ((op2 < 0) && (result >= op1))
+ Value *op2lt0 =
+ builder.CreateICmpSLT(op2,
+ ConstantInt::getSigned(op2->getType(), 0));
+ Value *cond_lt0 =
+ builder.CreateAnd(op2lt0, builder.CreateICmpSGE(result, op1));
+ overflow = builder.CreateOr(cond_ge0, cond_lt0);
+ } else if (ii->getIntrinsicID() == Intrinsic::ssub_with_overflow){
+ result = builder.CreateSub(op1, op2);
+ // overflow if ((op2 >= 0) && (result > op1))
+ Value *op2ge0 =
+ builder.CreateICmpSGE(op2,
+ ConstantInt::getSigned(op2->getType(), 0));
+ Value *cond_ge0 =
+ builder.CreateAnd(op2ge0, builder.CreateICmpSGT(result, op1));
+ // overflow if ((op2 < 0) && (result <= op1))
+ Value *op2lt0 =
+ builder.CreateICmpSLT(op2,
+ ConstantInt::getSigned(op2->getType(), 0));
+ Value *cond_lt0 =
+ builder.CreateAnd(op2lt0, builder.CreateICmpSLE(result, op1));
+ overflow = builder.CreateOr(cond_ge0, cond_lt0);
+ } else if (ii->getIntrinsicID() == Intrinsic::smul_with_overflow){
+ uint64_t bit_width = op1->getType()->getPrimitiveSizeInBits();
+ Value *int_min = ConstantInt::get(op1->getType(),
+ APInt::getSignedMinValue(bit_width));
+ Value *int_max = ConstantInt::get(op1->getType(),
+ APInt::getSignedMaxValue(bit_width));
+
+ // std::cerr << int_min << " " << int_max << "\n";
+
+ // overflow if (op1 == int_min) && ((op2 != 0) || (op2 != 1))
+ Value *op1_min = builder.CreateICmpEQ(op1, int_min);
+ Value *op2_eq0 =
+ builder.CreateICmpNE(op2, ConstantInt::getSigned(op2->getType(), 0));
+ Value *op2_eq1 =
+ builder.CreateICmpNE(op2, ConstantInt::getSigned(op2->getType(), 1));
+ Value *overflow_1 =
+ builder.CreateAnd(op1_min, builder.CreateAnd(op2_eq0, op2_eq1));
+
+ // overflow if (op2 == int_min) && ((op1 != 0) || (op1 != 1))
+ Value *op2_min = builder.CreateICmpEQ(op2, int_min);
+ Value *op1_eq0 =
+ builder.CreateICmpNE(op1, ConstantInt::getSigned(op1->getType(), 0));
+ Value *op1_eq1 =
+ builder.CreateICmpNE(op1, ConstantInt::getSigned(op1->getType(), 1));
+ Value *overflow_2 =
+ builder.CreateAnd(op2_min, builder.CreateAnd(op1_eq0, op1_eq1));
+
+ // branch if overflow is detected
+ BasicBlock *entry = builder.GetInsertBlock();
+ entry->setName(Twine(entry->getName(), "_smul_start"));
+ BasicBlock *end_of = entry->splitBasicBlock(builder.GetInsertPoint(),
+ "smul_end");
+ BasicBlock *check_abs = BasicBlock::Create(builder.getContext(),
+ "smul_check_abs",
+ F, end_of);
+ BasicBlock *check_sign = BasicBlock::Create(builder.getContext(),
+ "smul_check_sign",
+ F, end_of);
+ BasicBlock *check_sequal = BasicBlock::Create(builder.getContext(),
+ "smul_check_same_sign",
+ F, end_of);
+ BasicBlock *check_sdiff = BasicBlock::Create(builder.getContext(),
+ "smul_check_diff_sign",
+ F, end_of);
+
+ entry->getTerminator()->eraseFromParent();
+ builder.SetInsertPoint(entry);
+ Value *overflow_on_min = builder.CreateOr(overflow_1, overflow_2);
+ builder.CreateCondBr(overflow_on_min, end_of, check_abs);
+
+ // no overflow if (|op1| < 2) && (|op2| < 2),
+ // otherwise perform a check depending on the sign of the operands
+
+ // compute absolute values
+ builder.SetInsertPoint(check_abs);
+ Value *op1_neg = builder.CreateNeg(op1);
+ Value *op1_isneg =
+ builder.CreateICmpSLT(op1, Constant::getNullValue(op1->getType()));
+ Value *op1_abs = builder.CreateSelect(op1_isneg, op1_neg, op1);
+ Value *op2_neg = builder.CreateNeg(op2);
+ Value *op2_isneg =
+ builder.CreateICmpSLT(op2, Constant::getNullValue(op2->getType()));
+ Value *op2_abs = builder.CreateSelect(op2_isneg, op2_neg, op2);
+
+ // check if (|op1| < 2) && (|op2| < 2)
+ Value *op1_g1 =
+ builder.CreateICmpSGT(op1_abs,
+ ConstantInt::getSigned(op1->getType(), 2));
+ Value *op2_g1 =
+ builder.CreateICmpSGT(op2_abs,
+ ConstantInt::getSigned(op2->getType(), 2));
+ Value *overflow_no_abs = builder.CreateAnd(op1_g1, op2_g1);
+ builder.CreateCondBr(overflow_no_abs, end_of, check_sign);
+
+ // check sign
+ builder.SetInsertPoint(check_sign);
+ Value *different_sign = builder.CreateXor(op1_isneg, op2_isneg);
+ builder.CreateCondBr(different_sign, check_sequal, check_sdiff);
+
+ // operands have same sign
+ builder.SetInsertPoint(check_sequal);
+ Value *div_sequal = builder.CreateSDiv(int_max, op2_abs);
+ Value *overflow_sequal = builder.CreateICmpSGT(op1_abs, div_sequal);
+ builder.CreateBr(end_of);
+
+ // operands have different sign
+ builder.SetInsertPoint(check_sdiff);
+ Value *div_sdiff = builder.CreateSDiv(int_min,
+ builder.CreateNeg(op2_abs));
+ Value *overflow_sdiff = builder.CreateICmpSGT(op1_abs, div_sdiff);
+ builder.CreateBr(end_of);
+
+ // merge overflow values
+ builder.SetInsertPoint(end_of, end_of->begin());
+ PHINode *phi_of = builder.CreatePHI(overflow_on_min->getType(), 4);
+ phi_of->addIncoming(overflow_on_min, entry);
+ phi_of->addIncoming(overflow_no_abs, check_abs);
+ phi_of->addIncoming(overflow_sequal, check_sequal);
+ phi_of->addIncoming(overflow_sdiff, check_sdiff);
+
+ result = builder.CreateMul(op1, op2);
+ overflow = phi_of;
+ block_split = true;
+
+ F->viewCFG();
+ }
Value *resultStruct =
builder.CreateInsertValue(UndefValue::get(ii->getType()), result, 0);
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index fe80994..23eff17 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -786,6 +786,7 @@ static const char *modelledExternals[] = {
"__ubsan_handle_add_overflow",
"__ubsan_handle_sub_overflow",
"__ubsan_handle_mul_overflow",
+ "__ubsan_handle_divrem_overflow",
};
// Symbols we aren't going to warn about
static const char *dontCareExternals[] = {
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
