Merge pull request #8884 from tautschnig/fma

Add fused multiply-add (FMA) support with single rounding

Author: kroening

regression/cbmc-library/fma/precision.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  // Basic FMA
+  assert(fmaf(2.0f, 3.0f, 4.0f) == 10.0f);
+  assert(fmaf(-3.0f, 2.0f, 10.0f) == 4.0f);
+
+  // FMA vs mul+add: FMA preserves precision lost by separate mul+add.
+  // 0x1.fffffep+23 * 0x1.000002p+0 + 1.0:
+  // mul rounds product to 0x1p+24, then +1 = 0x1p+24 (unchanged)
+  // FMA keeps exact product, +1 = 0x1.000002p+24
+  assert(0x1.fffffep+23f * 0x1.000002p+0f + 1.0f == 0x1p+24f);
+  assert(fmaf(0x1.fffffep+23f, 0x1.000002p+0f, 1.0f) == 0x1.000002p+24f);
+
+  // FMA for remainder: fma(-n, y, x) computes x - n*y with single rounding
+  float x = 0x1.d55556p+0f;
+  float y = 0x1.555556p-2f;
+  assert(x - 5.0f * y == 0x1.55555p-3f);       // mul+sub: two roundings
+  assert(fmaf(-5.0f, y, x) == 0x1.555554p-3f); // FMA: one rounding
+}

regression/cbmc-library/fma/special_cases.c

@@ -0,0 +1,32 @@
+// IEEE 754 FMA special cases
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  // fma(NaN, y, z) = NaN
+  assert(isnan(fmaf(NAN, 1.0f, 0.0f)));
+
+  // fma(x, NaN, z) = NaN
+  assert(isnan(fmaf(1.0f, NAN, 0.0f)));
+
+  // fma(x, y, NaN) = NaN
+  assert(isnan(fmaf(1.0f, 1.0f, NAN)));
+
+  // fma(0, inf, z) = NaN (0 * inf is undefined)
+  assert(isnan(fmaf(0.0f, INFINITY, 1.0f)));
+
+  // fma(inf, 0, z) = NaN
+  assert(isnan(fmaf(INFINITY, 0.0f, 1.0f)));
+
+  // fma(inf, x, -inf) = NaN when inf*x = +inf (inf + (-inf) is undefined)
+  assert(isnan(fmaf(INFINITY, 1.0f, -INFINITY)));
+
+  // fma(inf, x, z) = +inf for finite z
+  assert(isinf(fmaf(INFINITY, 2.0f, 3.0f)));
+
+  // fma(x, y, inf) = +inf for finite x*y
+  assert(isinf(fmaf(2.0f, 3.0f, INFINITY)));
+
+  return 0;
+}

regression/cbmc-library/fma/test_bv_encoding.desc

@@ -0,0 +1,11 @@
+CORE smt-backend
+precision.c
+--smt2 --outfile -
+float_bv\.floatbv_fma
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Verify that float_bvt generates valid SMT2 for FMA expressions
+(non-FPA bitvector encoding).

regression/cbmc-library/fma/test_fpa_emission.desc

@@ -0,0 +1,10 @@
+CORE smt-backend
+precision.c
+--smt2 --fpa --outfile -
+fp\.fma
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Verify that the SMT2 FPA backend emits fp.fma (not a bitvector encoding).

regression/cbmc-library/fma/test_fpa_special_cases.desc

@@ -0,0 +1,11 @@
+CORE smt-backend
+special_cases.c
+--smt2 --fpa --no-built-in-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Run FMA special cases through an external SMT solver with FPA theory.
+Verifies NaN, infinity, and 0*inf handling end-to-end.

regression/cbmc-library/fma/test_fpa_special_emission.desc

@@ -0,0 +1,10 @@
+CORE smt-backend
+special_cases.c
+--smt2 --fpa --outfile -
+fp\.fma
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Verify that FMA special cases (NaN, inf) emit fp.fma via FPA backend.

regression/cbmc-library/fma/test_precision.desc

@@ -0,0 +1,8 @@
+CORE
+precision.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-library/fma/test_special_cases.desc

@@ -0,0 +1,10 @@
+CORE
+special_cases.c
+--floatbv --no-built-in-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+IEEE 754 FMA special cases: NaN propagation, 0*inf, inf+(-inf), inf results.

regression/cbmc/Float-fma-precision1/main.c

@@ -0,0 +1,17 @@
+// fmaf should compute x*y+z with a single rounding.
+// The C library model used to do x*y then +z (two roundings).
+// Example: fmaf(1+eps, 1+eps, -(1+2*eps)) where eps = 2^-23
+// Exact result: eps^2 = 2^-46 > 0
+// Double rounding: (1+eps)*(1+eps) rounds to 1+2*eps, then +c = 0
+// True FMA: should give eps^2 which is > 0
+#include <assert.h>
+#include <math.h>
+
+int main()
+{
+  float a = 1.0f + 1.1920929e-7f;    // 1 + 2^-23
+  float c = -(1.0f + 2.3841858e-7f); // -(1 + 2^-22)
+  float r = fmaf(a, a, c);
+  assert(r > 0.0f);
+  return 0;
+}

regression/cbmc/Float-fma-precision1/test.desc

@@ -0,0 +1,8 @@
+CORE no-new-smt
+main.c
+--floatbv --no-built-in-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+fmaf with single rounding via __CPROVER_fmaf built-in.