From ea28adf170ac8dd8d6d53f1563214f78d5032e8e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 7 Feb 2024 10:20:46 +0000 Subject: [PATCH] Enable powif* intrinsics These are supported by CBMC with https://github.com/diffblue/cbmc/pull/8192 merged. Resolves: #2763 --- docs/src/rust-feature-support/intrinsics.md | 4 ++-- .../codegen_cprover_gotoc/codegen/intrinsic.rs | 4 ++-- tests/kani/Intrinsics/Math/Arith/powi.rs | 18 ++++++++++++++++++ 3 files changed, 22 insertions(+), 4 deletions(-) create mode 100644 tests/kani/Intrinsics/Math/Arith/powi.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 0705d3b00f1b..a424e777a30c 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -187,8 +187,8 @@ nontemporal_store | No | | offset | Partial | Doesn't check [all UB conditions](https://doc.rust-lang.org/std/primitive.pointer.html#safety-2) | powf32 | No | | powf64 | No | | -powif32 | No | | -powif64 | No | | +powif32 | Partial | Results are overapproximated | +powif64 | Partial | Results are overapproximated | pref_align_of | Yes | | prefetch_read_data | No | | prefetch_read_instruction | No | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 3412cba290d2..6db8bc15beb0 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -476,8 +476,8 @@ impl<'tcx> GotocCtx<'tcx> { ), "powf32" => unstable_codegen!(codegen_simple_intrinsic!(Powf)), "powf64" => unstable_codegen!(codegen_simple_intrinsic!(Pow)), - "powif32" => unstable_codegen!(codegen_simple_intrinsic!(Powif)), - "powif64" => unstable_codegen!(codegen_simple_intrinsic!(Powi)), + "powif32" => codegen_simple_intrinsic!(Powif), + "powif64" => codegen_simple_intrinsic!(Powi), "pref_align_of" => codegen_intrinsic_const!(), "ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, place), "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc), diff --git a/tests/kani/Intrinsics/Math/Arith/powi.rs b/tests/kani/Intrinsics/Math/Arith/powi.rs new file mode 100644 index 000000000000..70d9d8b0d46b --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/powi.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#[kani::proof] +fn verify_powi32() { + let x: f32 = kani::any(); + kani::assume(x.is_normal()); + let x2 = x.powi(2); + assert!(x2 >= 0.0); +} + +#[kani::proof] +fn verify_powi64() { + let x: f64 = kani::any(); + kani::assume(x.is_normal()); + let x2 = x.powi(2); + assert!(x2 >= 0.0); +}