Intrinsics: Add support for @llvm.f{ma,muladd}.f*

3 files changed, 92 insertions, 0 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 1a16d389..a2928864 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -1680,6 +1680,41 @@ void Executor::executeCall(ExecutionState &state, KInstruction *ki, Function *f,
       break;
     }
 
+    case Intrinsic::fma:
+    case Intrinsic::fmuladd: {
+      // Both fma and fmuladd support float, double and fp80.  Note, that fp80
+      // is not mentioned in the documentation of fmuladd, nevertheless, it is
+      // still supported.  For details see
+      // https://github.com/klee/klee/pull/1507/files#r894993332
+
+      if (isa<VectorType>(i->getOperand(0)->getType()))
+        return terminateStateOnExecError(
+            state, f->getName() + " with vectors is not supported");
+
+      ref<ConstantExpr> op1 =
+          toConstant(state, eval(ki, 1, state).value, "floating point");
+      ref<ConstantExpr> op2 =
+          toConstant(state, eval(ki, 2, state).value, "floating point");
+      ref<ConstantExpr> op3 =
+          toConstant(state, eval(ki, 3, state).value, "floating point");
+
+      if (!fpWidthToSemantics(op1->getWidth()) ||
+          !fpWidthToSemantics(op2->getWidth()) ||
+          !fpWidthToSemantics(op3->getWidth()))
+        return terminateStateOnExecError(
+            state, "Unsupported " + f->getName() + " call");
+
+      // (op1 * op2) + op3
+      APFloat Res(*fpWidthToSemantics(op1->getWidth()), op1->getAPValue());
+      Res.fusedMultiplyAdd(
+          APFloat(*fpWidthToSemantics(op2->getWidth()), op2->getAPValue()),
+          APFloat(*fpWidthToSemantics(op3->getWidth()), op3->getAPValue()),
+          APFloat::rmNearestTiesToEven);
+
+      bindLocal(ki, state, ConstantExpr::alloc(Res.bitcastToAPInt()));
+      break;
+    }
+
 #if LLVM_VERSION_CODE >= LLVM_VERSION(12, 0)
     case Intrinsic::abs: {
       if (isa<VectorType>(i->getOperand(0)->getType()))
diff --git a/lib/Module/IntrinsicCleaner.cpp b/lib/Module/IntrinsicCleaner.cpp
index 7836c202..adef513e 100644
--- a/lib/Module/IntrinsicCleaner.cpp
+++ b/lib/Module/IntrinsicCleaner.cpp
@@ -66,6 +66,8 @@ bool IntrinsicCleanerPass::runOnBasicBlock(BasicBlock &b, Module &M) {
       case Intrinsic::vastart:
       case Intrinsic::vaend:
       case Intrinsic::fabs:
+      case Intrinsic::fma:
+      case Intrinsic::fmuladd:
 #if LLVM_VERSION_CODE >= LLVM_VERSION(7, 0)
       case Intrinsic::fshr:
       case Intrinsic::fshl:
diff --git a/test/Intrinsics/FMulAdd.ll b/test/Intrinsics/FMulAdd.ll
new file mode 100644
index 00000000..989b88a8
--- /dev/null
+++ b/test/Intrinsics/FMulAdd.ll
@@ -0,0 +1,55 @@
+; 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 {
+fma.float:
+  %0 = call float @llvm.fma.f32(float 2.0, float 2.0, float 1.0)
+  %cmp0 = fcmp one float %0, 5.0
+  br i1 %cmp0, label %abort.block, label %fma.double
+
+fma.double:
+  %1 = call double @llvm.fma.f64(double 2.0, double 2.0, double 1.0)
+  %cmp1 = fcmp one double %1, 5.0
+  br i1 %cmp1, label %abort.block, label %fma.fp80
+
+fma.fp80:
+  %2 = call x86_fp80 @llvm.fma.f80(x86_fp80 0xK40008000000000000000,
+                                   x86_fp80 0xK40008000000000000000,
+                                   x86_fp80 0xK3FFF8000000000000000)
+  %cmp2 = fcmp one x86_fp80 %2, 0xK4001A000000000000000
+  br i1 %cmp2, label %abort.block, label %fmuladd.float
+
+fmuladd.float:
+  %3 = call float @llvm.fmuladd.f32(float 2.0, float 2.0, float 1.0)
+  %cmp3 = fcmp one float %3, 5.0
+  br i1 %cmp3, label %abort.block, label %fmuladd.double
+
+fmuladd.double:
+  %4 = call double @llvm.fmuladd.f64(double 2.0, double 2.0, double 1.0)
+  %cmp4 = fcmp one double %4, 5.0
+  br i1 %cmp4, label %abort.block, label %fmuladd.fp80
+
+fmuladd.fp80:
+  %5 = call x86_fp80 @llvm.fmuladd.f80(x86_fp80 0xK40008000000000000000,
+                                       x86_fp80 0xK40008000000000000000,
+                                       x86_fp80 0xK3FFF8000000000000000)
+  %cmp5 = fcmp one x86_fp80 %5, 0xK4001A000000000000000
+  br i1 %cmp4, label %abort.block, label %exit.block
+
+exit.block:
+  ret i32 0
+
+abort.block:
+  call void @abort()
+  unreachable
+}
+
+declare void      @abort() noreturn nounwind
+
+declare float     @llvm.fma.f32(float    %a, float    %b, float    %c)
+declare double    @llvm.fma.f64(double   %a, double   %b, double   %c)
+declare x86_fp80  @llvm.fma.f80(x86_fp80 %a, x86_fp80 %b, x86_fp80 %c)
+
+declare float     @llvm.fmuladd.f32(float    %a, float    %b, float    %c)
+declare double    @llvm.fmuladd.f64(double   %a, double   %b, double   %c)
+declare x86_fp80  @llvm.fmuladd.f80(x86_fp80 %a, x86_fp80 %b, x86_fp80 %c)