Skip to content

Commit

Permalink
Enable fma* intrinsics
Browse files Browse the repository at this point in the history
Requires support in CBMC.
  • Loading branch information
tautschnig committed Feb 7, 2024
1 parent a82bad4 commit 641e110
Show file tree
Hide file tree
Showing 3 changed files with 30 additions and 4 deletions.
4 changes: 2 additions & 2 deletions docs/src/rust-feature-support/intrinsics.md
Original file line number Diff line number Diff line change
Expand Up @@ -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 | |
Expand Down
4 changes: 2 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
26 changes: 26 additions & 0 deletions tests/kani/Intrinsics/Math/Arith/fma.rs
Original file line number Diff line number Diff line change
@@ -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);
}

0 comments on commit 641e110

Please sign in to comment.