diff options
author | Lukas Zaoral <lzaoral@redhat.com> | 2021-07-07 10:33:46 +0200 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2021-09-10 15:14:56 +0100 |
commit | 8775b9cf6c716f51fe90d668e734a1288c8b5404 (patch) | |
tree | 5f586ff87b1fddfdebbcc670b658ea0e054c7d41 /lib | |
parent | 3d7c05a7e86a72a4fc8df115591bd1e7a50f9d84 (diff) | |
download | klee-8775b9cf6c716f51fe90d668e734a1288c8b5404.tar.gz |
llvm12: Implement llvm.abs intrinsic
The vector variants are not implemented at the moment. See: https://reviews.llvm.org/D84125 Co-authored-by: Lukas Zaoral <lzaoral@redhat.com> Co-authored-by: Martin Nowack <m.nowack@imperial.ac.uk>
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 38 | ||||
-rw-r--r-- | lib/Module/IntrinsicCleaner.cpp | 1 |
2 files changed, 39 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: |