Enable fma* intrinsics

Requires support in CBMC.

docs/src/rust-feature-support/intrinsics.md

@@ -159,8 +159,8 @@ fdiv_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809)
 float_to_int_unchecked | No | |
 floorf32 | Yes | |
 floorf64 | Yes | |
-fmaf32 | No | |
-fmaf64 | No | |
+fmaf32 | Partial | Results are overapproximated |
+fmaf64 | Partial | Results are overapproximated |
 fmul_fast | Partial | [#809](https://github.com/model-checking/kani/issues/809) |
 forget | Yes | |
 frem_fast | No | |

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -438,8 +438,8 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             "floorf32" => codegen_simple_intrinsic!(Floorf),
             "floorf64" => codegen_simple_intrinsic!(Floor),
-            "fmaf32" => unstable_codegen!(codegen_simple_intrinsic!(Fmaf)),
-            "fmaf64" => unstable_codegen!(codegen_simple_intrinsic!(Fma)),
+            "fmaf32" => codegen_simple_intrinsic!(Fmaf),
+            "fmaf64" => codegen_simple_intrinsic!(Fma),
             "fmul_fast" => {
                 let fargs_clone = fargs.clone();
                 let binop_stmt = codegen_intrinsic_binop!(mul);

tests/kani/Intrinsics/Math/Arith/fma.rs

@@ -0,0 +1,26 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+fn verify_fma_32() {
+    let m = 10.0_f32;
+    let x = 4.0_f32;
+    let b = 60.0_f32;
+
+    // 100.0
+    let abs_difference = (m.mul_add(x, b) - ((m * x) + b)).abs();
+
+    assert!(abs_difference <= f32::EPSILON);
+}
+
+#[kani::proof]
+fn verify_fma_64() {
+    let m = 10.0_f64;
+    let x = 4.0_f64;
+    let b = 60.0_f64;
+
+    // 100.0
+    let abs_difference = (m.mul_add(x, b) - ((m * x) + b)).abs();
+
+    assert!(abs_difference < 1e-10);
+}