From cd236fa98ee06d3a34fe9a315256124759e3a6ab Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Feb 2024 10:38:22 +0000 Subject: [PATCH] Enable sqrt* intrinsics Requires fixes in CBMC's sqrt* implementations. --- docs/src/rust-feature-support/intrinsics.md | 4 +-- .../codegen/intrinsic.rs | 4 +-- tests/kani/Intrinsics/Math/Arith/sqrt.rs | 28 +++++++++++++++++++ 3 files changed, 32 insertions(+), 4 deletions(-) create mode 100644 tests/kani/Intrinsics/Math/Arith/sqrt.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 0705d3b00f1b..304ff22e5b56 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -211,8 +211,8 @@ sinf32 | Partial | Results are overapproximated; [this test](https://github.com/ sinf64 | Partial | Results are overapproximated; [this test](https://github.com/model-checking/kani/blob/main/tests/kani/Intrinsics/Math/Trigonometry/sinf64.rs) explains how | size_of | Yes | | size_of_val | Yes | | -sqrtf32 | No | | -sqrtf64 | No | | +sqrtf32 | Partial | Results are overapproximated | +sqrtf64 | Partial | Results are overapproximated | sub_with_overflow | Yes | | transmute | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/nomicon/transmutes.html) | truncf32 | Yes | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 3412cba290d2..3b9abdf2e1e0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -555,8 +555,8 @@ impl<'tcx> GotocCtx<'tcx> { "simd_xor" => codegen_intrinsic_binop!(bitxor), "size_of" => unreachable!(), "size_of_val" => codegen_size_align!(size), - "sqrtf32" => unstable_codegen!(codegen_simple_intrinsic!(Sqrtf)), - "sqrtf64" => unstable_codegen!(codegen_simple_intrinsic!(Sqrt)), + "sqrtf32" => codegen_simple_intrinsic!(Sqrtf), + "sqrtf64" => codegen_simple_intrinsic!(Sqrt), "sub_with_overflow" => self.codegen_op_with_overflow( BinaryOperator::OverflowResultMinus, fargs, diff --git a/tests/kani/Intrinsics/Math/Arith/sqrt.rs b/tests/kani/Intrinsics/Math/Arith/sqrt.rs new file mode 100644 index 000000000000..d9003ae8d066 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/sqrt.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_sqrt32() { + let positive = 4.0_f32; + let negative = -4.0_f32; + let negative_zero = -0.0_f32; + + let abs_difference = (positive.sqrt() - 2.0).abs(); + + assert!(abs_difference <= f32::EPSILON); + assert!(negative.sqrt().is_nan()); + assert!(negative_zero.sqrt() == negative_zero); +} + +#[kani::proof] +fn verify_sqrt64() { + let positive = 4.0_f64; + let negative = -4.0_f64; + let negative_zero = -0.0_f64; + + let abs_difference = (positive.sqrt() - 2.0).abs(); + + assert!(abs_difference <= 1e-10); + assert!(negative.sqrt().is_nan()); + assert!(negative_zero.sqrt() == negative_zero); +}