From beccc4c42111d14f369103bb0f9a6ccb15927968 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 20:42:31 +0200 Subject: [PATCH] Enable fma* intrinsics (#3002) Implemented in CBMC in https://github.com/diffblue/cbmc/pull/8195. --- docs/src/rust-feature-support/intrinsics.md | 4 +-- .../codegen/intrinsic.rs | 4 +-- tests/kani/Intrinsics/Math/Arith/fma.rs | 26 +++++++++++++++++++ 3 files changed, 30 insertions(+), 4 deletions(-) create mode 100644 tests/kani/Intrinsics/Math/Arith/fma.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index f97db5d8ab6c..77392cd37fc6 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/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 | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 91f7ea20c9b1..8f93a4c61553 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -447,8 +447,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); diff --git a/tests/kani/Intrinsics/Math/Arith/fma.rs b/tests/kani/Intrinsics/Math/Arith/fma.rs new file mode 100644 index 000000000000..379d5aa81db5 --- /dev/null +++ b/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); +}