diff --git a/.github/workflows/audit.yml b/.github/workflows/audit.yml index 3ae9d192f376..5b75d6162c85 100644 --- a/.github/workflows/audit.yml +++ b/.github/workflows/audit.yml @@ -7,6 +7,7 @@ name: Cargo Audit on: pull_request: + merge_group: push: # Run on changes to branches but not tags. branches: diff --git a/.github/workflows/format-check.yml b/.github/workflows/format-check.yml index 5ab7dcb1b9c3..cc13306a4eaf 100644 --- a/.github/workflows/format-check.yml +++ b/.github/workflows/format-check.yml @@ -3,6 +3,7 @@ name: Kani Format Check on: pull_request: + merge_group: push: # Not just any push, as that includes tags. # We don't want to re-trigger this workflow when tagging an existing commit. diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index dd077eff25e1..a565c9cd4cbe 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -3,6 +3,7 @@ name: Kani CI on: pull_request: + merge_group: push: # Not just any push, as that includes tags. # We don't want to re-trigger this workflow when tagging an existing commit. diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 72ef4e2de889..ad2e339f19e1 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -8,6 +8,7 @@ name: Release Bundle on: pull_request: + merge_group: push: branches: - 'main' diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 7816876d460e..77392cd37fc6 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 | Partial | Results are overapproximated | powf64 | Partial | Results are overapproximated | -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 57f52dc50b18..8f93a4c61553 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -490,8 +490,8 @@ impl<'tcx> GotocCtx<'tcx> { ), "powf32" => codegen_simple_intrinsic!(Powf), "powf64" => 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, loc), "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc), diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 8753157827b5..0c0e9e9f196c 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-08-01" +channel = "nightly-2024-08-02" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs b/tests/kani/Cast/cast_abstract_args_to_concrete.rs similarity index 92% rename from tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs rename to tests/kani/Cast/cast_abstract_args_to_concrete.rs index 51067e0e0a73..6694f799493a 100644 --- a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme2.rs +++ b/tests/kani/Cast/cast_abstract_args_to_concrete.rs @@ -1,9 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// https://github.com/model-checking/kani/issues/555 -// kani-flags: --no-undefined-function-checks - // This regression test is in response to issue #135. // The type of the second parameter to powi is a `CInteger`, but // the type of `2` here is a `u32`. This test ensures that diff --git a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs b/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs deleted file mode 100644 index faeb74c5d66a..000000000000 --- a/tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs +++ /dev/null @@ -1,24 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT - -//! This test is a modified version of cast_abstract_args_to_concrete_fixme.rs. -//! The original test requires --no-undefined-function-checks to pass. This is an issue that -//! require investigation. See https://github.com/model-checking/kani/issues/555. -//! -//! Once this issue is fixed. Please remove this test and remove the kani flag from the original -//! test: --no-undefined-function-check - -fn main() { - let _x32 = 1.0f32.powi(2); - let _x64 = 1.0f64.powi(2); - - unsafe { - let size: libc::size_t = mem::size_of::(); - let my_num: *mut libc::c_void = libc::malloc(size); - if my_num.is_null() { - panic!("failed to allocate memory"); - } - let my_num2 = libc::memset(my_num, 1, size); - libc::free(my_num); - } -} diff --git a/tests/kani/Intrinsics/Math/Arith/powi.rs b/tests/kani/Intrinsics/Math/Arith/powi.rs new file mode 100644 index 000000000000..c7986d18a9ef --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/powi.rs @@ -0,0 +1,22 @@ +// 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()); + kani::assume(x >= 1e-19 || x <= -1e-19); + kani::assume(x <= 1.84e19 && x >= -1.84e19); + let x2 = x.powi(2); + assert!(x2 >= 0.0); +} + +#[kani::proof] +fn verify_powi64() { + let x: f64 = kani::any(); + kani::assume(x.is_normal()); + kani::assume(x >= 1e-153 || x <= -1e-153); + kani::assume(x <= 1.34e154 && x >= -1.34e154); + let x2 = x.powi(2); + assert!(x2 >= 0.0); +}