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>

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)