Add overrides for fma, fmaf, llvm.fmuladd.*, and llvm.fma.*

Fixes #1154.

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics.hs

@@ -283,6 +283,10 @@ declare_overrides =
   , basic_llvm_override LLVM.llvmLog2Override_F64
   , basic_llvm_override LLVM.llvmLog10Override_F32
   , basic_llvm_override LLVM.llvmLog10Override_F64
+  , basic_llvm_override LLVM.llvmFmaOverride_F32
+  , basic_llvm_override LLVM.llvmFmaOverride_F64
+  , basic_llvm_override LLVM.llvmFmuladdOverride_F32
+  , basic_llvm_override LLVM.llvmFmuladdOverride_F64
   , basic_llvm_override LLVM.llvmIsFpclassOverride_F32
   , basic_llvm_override LLVM.llvmIsFpclassOverride_F64
 
@@ -319,6 +323,8 @@ declare_overrides =
   , basic_llvm_override Libc.llvmCeilfOverride
   , basic_llvm_override Libc.llvmFloorOverride
   , basic_llvm_override Libc.llvmFloorfOverride
+  , basic_llvm_override Libc.llvmFmaOverride
+  , basic_llvm_override Libc.llvmFmafOverride
   , basic_llvm_override Libc.llvmIsinfOverride
   , basic_llvm_override Libc.llvm__isinfOverride
   , basic_llvm_override Libc.llvm__isinffOverride

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs

@@ -1013,6 +1013,54 @@ llvmIsFpclassOverride_F64 =
   [llvmOvr| i1 @llvm.is.fpclass.f64( double, i32 ) |]
   (\_memOps bak args -> Ctx.uncurryAssignment (callIsFpclass bak) args)
 
+llvmFmaOverride_F32 ::
+     forall sym p
+   . IsSymInterface sym
+  => LLVMOverride p sym
+        (EmptyCtx ::> FloatType SingleFloat
+                  ::> FloatType SingleFloat
+                  ::> FloatType SingleFloat)
+        (FloatType SingleFloat)
+llvmFmaOverride_F32 =
+  [llvmOvr| float @llvm.fma.f32( float, float, float ) |]
+  (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callFMA bak) args)
+
+llvmFmaOverride_F64 ::
+     forall sym p
+   . IsSymInterface sym
+  => LLVMOverride p sym
+        (EmptyCtx ::> FloatType DoubleFloat
+                  ::> FloatType DoubleFloat
+                  ::> FloatType DoubleFloat)
+        (FloatType DoubleFloat)
+llvmFmaOverride_F64 =
+  [llvmOvr| double @llvm.fma.f64( double, double, double ) |]
+  (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callFMA bak) args)
+
+llvmFmuladdOverride_F32 ::
+     forall sym p
+   . IsSymInterface sym
+  => LLVMOverride p sym
+        (EmptyCtx ::> FloatType SingleFloat
+                  ::> FloatType SingleFloat
+                  ::> FloatType SingleFloat)
+        (FloatType SingleFloat)
+llvmFmuladdOverride_F32 =
+  [llvmOvr| float @llvm.fmuladd.f32( float, float, float ) |]
+  (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callFMA bak) args)
+
+llvmFmuladdOverride_F64 ::
+     forall sym p
+   . IsSymInterface sym
+  => LLVMOverride p sym
+        (EmptyCtx ::> FloatType DoubleFloat
+                  ::> FloatType DoubleFloat
+                  ::> FloatType DoubleFloat)
+        (FloatType DoubleFloat)
+llvmFmuladdOverride_F64 =
+  [llvmOvr| double @llvm.fmuladd.f64( double, double, double ) |]
+  (\_memOps bak args -> Ctx.uncurryAssignment (Libc.callFMA bak) args)
+
 
 llvmX86_pclmulqdq
 --declare <2 x i64> @llvm.x86.pclmulqdq(<2 x i64>, <2 x i64>, i8) #1

crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/Libc.hs

@@ -738,6 +738,30 @@ llvmFloorfOverride =
   [llvmOvr| float @floorf( float ) |]
   (\_memOps sym args -> Ctx.uncurryAssignment (callFloor sym) args)
 
+llvmFmafOverride ::
+     forall sym p
+   . IsSymInterface sym
+  => LLVMOverride p sym
+        (EmptyCtx ::> FloatType SingleFloat
+                  ::> FloatType SingleFloat
+                  ::> FloatType SingleFloat)
+        (FloatType SingleFloat)
+llvmFmafOverride =
+  [llvmOvr| float @fmaf( float, float, float ) |]
+  (\_memOps bak args -> Ctx.uncurryAssignment (callFMA bak) args)
+
+llvmFmaOverride ::
+     forall sym p
+   . IsSymInterface sym
+  => LLVMOverride p sym
+        (EmptyCtx ::> FloatType DoubleFloat
+                  ::> FloatType DoubleFloat
+                  ::> FloatType DoubleFloat)
+        (FloatType DoubleFloat)
+llvmFmaOverride =
+  [llvmOvr| double @fma( double, double, double ) |]
+  (\_memOps bak args -> Ctx.uncurryAssignment (callFMA bak) args)
+
 
 -- math.h defines isinf() and isnan() as macros, so you might think it unusual
 -- to provide function overrides for them. However, if you write, say,
@@ -870,6 +894,18 @@ callFloor ::
   OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
 callFloor bak (regValue -> x) = liftIO $ iFloatRound @_ @fi (backendGetSym bak) RTN x
 
+-- | An implementation of @libc@'s @fma@ function.
+callFMA ::
+     forall fi p sym bak ext r args ret
+   . IsSymBackend sym bak
+  => bak
+  -> RegEntry sym (FloatType fi)
+  -> RegEntry sym (FloatType fi)
+  -> RegEntry sym (FloatType fi)
+  -> OverrideSim p sym ext r args ret (RegValue sym (FloatType fi))
+callFMA bak (regValue -> x) (regValue -> y) (regValue -> z) = liftIO $
+  iFloatFMA @_ @fi (backendGetSym bak) RNE x y z
+
 -- | An implementation of @libc@'s @isinf@ macro. This returns @1@ when the
 -- argument is positive infinity, @-1@ when the argument is negative infinity,
 -- and zero otherwise.

crux-llvm/test-data/golden/fmuladd.c

@@ -0,0 +1,27 @@
+// A regression test for https://github.com/GaloisInc/crucible/issues/1154.
+#include <crucible.h>
+#include <math.h>
+
+// LLVM is liable to optimize these functions in a way that uses the
+// llvm.fmuladd.* or llvm.fma.* intrinsics.
+float fmuladdf(float a, float b, float c) {
+  return a * b + c;
+}
+
+double fmuladd(double a, double b, double c) {
+  return a * b + c;
+}
+
+int main(void) {
+  float f1 = fmuladdf(1.0f, 2.0f, 3.0f);
+  check(f1 == f1);
+  float f2 = fmaf(1.0f, 2.0f, 3.0f);
+  check(f2 == f2);
+
+  double d1 = fmuladd(1.0, 2.0, 3.0);
+  check(d1 == d1);
+  double d2 = fma(1.0, 2.0, 3.0);
+  check(d2 == d2);
+
+  return 0;
+}

crux-llvm/test-data/golden/fmuladd.config

@@ -0,0 +1 @@
+opt-level: 0

crux-llvm/test-data/golden/fmuladd.z3.good

@@ -0,0 +1 @@
+[Crux] Overall status: Valid.