llvm12: Implement llvm.{s,u}{max,min} intrinsics

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>

3 files changed, 71 insertions, 0 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index aaa56a55..a8ca86c2 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1720,6 +1720,35 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
       break;
     }
 
+#if LLVM_VERSION_CODE >= LLVM_VERSION(12, 0)
+    case Intrinsic::smax:
+    case Intrinsic::smin:
+    case Intrinsic::umax:
+    case Intrinsic::umin: {
+      if (isa<VectorType>(i->getOperand(0)->getType()) ||
+          isa<VectorType>(i->getOperand(1)->getType()))
+        return terminateStateOnExecError(
+            state, "llvm.{s,u}{max,min} with vectors is not supported");
+
+      ref<Expr> op1 = eval(ki, 1, state).value;
+      ref<Expr> op2 = eval(ki, 2, state).value;
+
+      ref<Expr> cond = nullptr;
+      if (f->getIntrinsicID() == Intrinsic::smax)
+        cond = SgtExpr::create(op1, op2);
+      else if (f->getIntrinsicID() == Intrinsic::smin)
+        cond = SltExpr::create(op1, op2);
+      else if (f->getIntrinsicID() == Intrinsic::umax)
+        cond = UgtExpr::create(op1, op2);
+      else // (f->getIntrinsicID() == Intrinsic::umin)
+        cond = UltExpr::create(op1, op2);
+
+      ref<Expr> result = SelectExpr::create(cond, op1, op2);
+      bindLocal(ki, state, result);
+      break;
+    }
+#endif
+
 #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0)
     case Intrinsic::fshr:
     case Intrinsic::fshl: {
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index eaec7722..a10dc9e3 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -70,6 +70,12 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
       case Intrinsic::fshr:
       case Intrinsic::fshl:
 #endif
+#if LLVM_VERSION_CODE >= LLVM_VERSION(12, 0)
+      case Intrinsic::smax:
+      case Intrinsic::smin:
+      case Intrinsic::umax:
+      case Intrinsic::umin:
+#endif
         break;
 
         // Lower vacopy so that object resolution etc is handled by
diff --git a/test/Intrinsics/MinMax.ll b/test/Intrinsics/MinMax.ll
new file mode 100644
index 00000000..c2dc66f5
--- /dev/null
+++ b/test/Intrinsics/MinMax.ll
@@ -0,0 +1,36 @@
+; REQUIRES: geq-llvm-12.0
+; RUN: rm -rf %t.klee-out
+; RUN: %klee -exit-on-error --output-dir=%t.klee-out --optimize=false %s
+define dso_local i32 @main() local_unnamed_addr {
+  smax:
+  %0 = call i32 @llvm.smax.i32(i32 -10, i32 10)
+  %cmp = icmp ne i32 %0, 10
+  br i1 %cmp, label %abort.block, label %smin
+
+  smin:
+  %1 = call i32 @llvm.smin.i32(i32 -10, i32 10)
+  %cmp1 = icmp ne i32 %1, -10
+  br i1 %cmp1, label %abort.block, label %umax
+
+  umax:
+  %2 = call i32 @llvm.umax.i32(i32 10, i32 20)
+  %cmp2 = icmp ne i32 %2, 20
+  br i1 %cmp2, label %abort.block, label %umin
+
+  umin:
+  %3 = call i32 @llvm.umin.i32(i32 10, i32 5)
+  %cmp3 = icmp ne i32 %3, 5
+  br i1 %cmp3, label %abort.block, label %exit.block
+
+  exit.block:
+    ret i32 0
+
+  abort.block:
+    call void @abort()
+    unreachable
+}
+declare void @abort() noreturn nounwind
+declare i32 @llvm.smax.i32(i32, i32)
+declare i32 @llvm.smin.i32(i32, i32)
+declare i32 @llvm.umax.i32(i32, i32)
+declare i32 @llvm.umin.i32(i32, i32)