diff options
| -rw-r--r-- | lib/Core/Executor.cpp | 38 | ||||
| -rw-r--r-- | lib/Module/IntrinsicCleaner.cpp | 1 | ||||
| -rw-r--r-- | test/Intrinsics/abs-no-overflow.ll | 57 | ||||
| -rw-r--r-- | test/Intrinsics/abs-overflow.ll | 12 |
4 files changed, 108 insertions, 0 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index a8ca86c2..74ca7fb7 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1721,6 +1721,44 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f, } #if LLVM_VERSION_CODE >= LLVM_VERSION(12, 0) + case Intrinsic::abs: { + if (isa<VectorType>(i->getOperand(0)->getType())) + return terminateStateOnExecError( + state, "llvm.abs with vectors is not supported"); + + ref<Expr> op = eval(ki, 1, state).value; + ref<Expr> poison = eval(ki, 2, state).value; + + assert(poison->getWidth() == 1 && "Second argument is not an i1"); + unsigned bw = op->getWidth(); + + uint64_t moneVal = APInt(bw, -1, true).getZExtValue(); + uint64_t sminVal = APInt::getSignedMinValue(bw).getZExtValue(); + + ref<ConstantExpr> zero = ConstantExpr::create(0, bw); + ref<ConstantExpr> mone = ConstantExpr::create(moneVal, bw); + ref<ConstantExpr> smin = ConstantExpr::create(sminVal, bw); + + if (poison->isTrue()) { + ref<Expr> issmin = EqExpr::create(op, smin); + if (issmin->isTrue()) + return terminateStateOnExecError( + state, "llvm.abs called with poison and INT_MIN"); + } + + // conditions to flip the sign: INT_MIN < op < 0 + ref<Expr> negative = SltExpr::create(op, zero); + ref<Expr> notsmin = NeExpr::create(op, smin); + ref<Expr> cond = AndExpr::create(negative, notsmin); + + // flip and select the result + ref<Expr> flip = MulExpr::create(op, mone); + ref<Expr> result = SelectExpr::create(cond, flip, op); + + bindLocal(ki, state, result); + break; + } + case Intrinsic::smax: case Intrinsic::smin: case Intrinsic::umax: diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp index 08b87d0e..b3b356d2 100644 --- a/lib/Module/IntrinsicCleaner.cpp +++ b/lib/Module/IntrinsicCleaner.cpp @@ -71,6 +71,7 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) { case Intrinsic::fshl: #endif #if LLVM_VERSION_CODE >= LLVM_VERSION(12, 0) + case Intrinsic::abs: case Intrinsic::smax: case Intrinsic::smin: case Intrinsic::umax: diff --git a/test/Intrinsics/abs-no-overflow.ll b/test/Intrinsics/abs-no-overflow.ll new file mode 100644 index 00000000..7f476e2a --- /dev/null +++ b/test/Intrinsics/abs-no-overflow.ll @@ -0,0 +1,57 @@ +; LLVM has an intrinsic for abs. +; This file is based on the following code with poisoning of llvm.abs disabled. +; ``` +; #include "klee/klee.h" +; +; #include <assert.h> +; #include <limits.h> +; +; volatile int abs_a; +; +; int main(void) +; { +; int a; +; klee_make_symbolic(&a, sizeof(a), "a"); +; +; abs_a = a < 0 ? -a : a; +; if (abs_a == INT_MIN) +; assert(abs_a == a); +; else +; assert(abs_a >= 0); +; return abs_a; +; } +; ``` +; REQUIRES: geq-llvm-12.0 +; RUN: rm -rf %t.klee-out +; RUN: %klee -exit-on-error --output-dir=%t.klee-out --optimize=false %s + +@0 = private unnamed_addr constant [2 x i8] c"a\00", align 1 +define dso_local i32 @main() local_unnamed_addr { + %1 = alloca i32, align 4 + %2 = bitcast i32* %1 to i8* + call void @klee_make_symbolic(i8* nonnull %2, i64 4, i8* getelementptr inbounds ([2 x i8], [2 x i8]* @0, i64 0, i64 0)) + %3 = load i32, i32* %1, align 4 + ; Call with is_int_min_poison == 0 (false), expects INT_MIN to be returned + %abs_a = call i32 @llvm.abs.i32(i32 %3, i1 false) + %4 = icmp eq i32 %abs_a, -2147483648 + br i1 %4, label %int_min, label %not_int_min + +int_min: + %5 = icmp eq i32 %abs_a, %3 + br i1 %5, label %exit.block, label %abort.block + +not_int_min: + %6 = icmp sgt i32 %abs_a, -1 + br i1 %6, label %exit.block, label %abort.block + +exit.block: + ret i32 0 + +abort.block: + call void @abort() + unreachable +} + +declare dso_local void @klee_make_symbolic(i8*, i64, i8*) +declare i32 @llvm.abs.i32(i32, i1 immarg) +declare void @abort() noreturn nounwind diff --git a/test/Intrinsics/abs-overflow.ll b/test/Intrinsics/abs-overflow.ll new file mode 100644 index 00000000..33b47ecf --- /dev/null +++ b/test/Intrinsics/abs-overflow.ll @@ -0,0 +1,12 @@ +; REQUIRES: geq-llvm-12.0 +; RUN: rm -rf %t.klee-out +; RUN: %klee --output-dir=%t.klee-out --optimize=false %s 2> %t.stderr.log +; RUN: FileCheck %s < %t.stderr.log + +define i32 @main() { + %1 = call i32 @llvm.abs.i32(i32 -2147483648, i1 true) + ; CHECK: llvm.abs called with poison and INT_MIN + ret i32 0 +} + +declare i32 @llvm.abs.i32(i32, i1 immarg) |