From 4a9255706dfcb336db59d30fbe327f9ed2680396 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 21:30:02 +0200 Subject: [PATCH] Enable sqrt* intrinsics (#3000) CBMC's sqrt* implementations were fixed 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/sqrt.rs | 24 +++++++++++++++++++ 3 files changed, 28 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 77392cd37fc6..ce3c9fc1b7a2 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 8f93a4c61553..c4d5396f1fe8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -570,8 +570,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..31afaba8a740 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/sqrt.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_sqrt32() { + let positive = 4.0_f32; + let negative_zero = -0.0_f32; + + let abs_difference = (positive.sqrt() - 2.0).abs(); + + assert!(abs_difference <= f32::EPSILON); + assert!(negative_zero.sqrt() == negative_zero); +} + +#[kani::proof] +fn verify_sqrt64() { + let positive = 4.0_f64; + let negative_zero = -0.0_f64; + + let abs_difference = (positive.sqrt() - 2.0).abs(); + + assert!(abs_difference <= 1e-10); + assert!(negative_zero.sqrt() == negative_zero); +}