From 6ae3f00c88a458abc381057456780af9e7d7e451 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 16:54:19 +0200 Subject: [PATCH 1/4] Enable powif* intrinsics (#2999) 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/intrinsic.rs | 4 ++-- ...2.rs => cast_abstract_args_to_concrete.rs} | 3 --- .../cast_abstract_args_to_concrete_fixme.rs | 24 ------------------- tests/kani/Intrinsics/Math/Arith/powi.rs | 22 +++++++++++++++++ 5 files changed, 26 insertions(+), 31 deletions(-) rename tests/kani/Cast/{cast_abstract_args_to_concrete_fixme2.rs => cast_abstract_args_to_concrete.rs} (92%) delete mode 100644 tests/kani/Cast/cast_abstract_args_to_concrete_fixme.rs 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 501a9952f05e..f97db5d8ab6c 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 12352190e6e2..91f7ea20c9b1 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/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); +} From 754691122aeb0c762180c77bc1fa9fcf1edc75d5 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Fri, 2 Aug 2024 15:41:14 +0000 Subject: [PATCH 2/4] Automatic toolchain upgrade to nightly-2024-08-02 (#3407) Update Rust toolchain from nightly-2024-08-01 to nightly-2024-08-02 without any other source changes. This is an automatically generated pull request. If any of the CI checks fail, manual intervention is required. In such a case, review the changes at https://github.com/rust-lang/rust from https://github.com/rust-lang/rust/commit/28a58f2fa7f0c46b8fab8237c02471a915924fe5 up to https://github.com/rust-lang/rust/commit/8e86c9567154dc5a9ada15ab196d23eae2bd7d89. --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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"] From 24fc8aafb4c6a38dd182a3620e87efbd88fc0318 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 18:32:33 +0200 Subject: [PATCH 3/4] Prepare use of GitHub merge queues (#3408) Merge queues should help us avoid having to merge from main repeatedly even when all approvals are in and all CI jobs have succeeded. See https://docs.github.com/en/repositories/configuring-branches-and-merges-in-your-repository/configuring-pull-request-merges/managing-a-merge-queue By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. Co-authored-by: Felipe R. Monteiro --- .github/workflows/audit.yml | 1 + .github/workflows/format-check.yml | 1 + .github/workflows/kani.yml | 1 + .github/workflows/release.yml | 1 + 4 files changed, 4 insertions(+) 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' From beccc4c42111d14f369103bb0f9a6ccb15927968 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 2 Aug 2024 20:42:31 +0200 Subject: [PATCH 4/4] Enable fma* intrinsics (#3002) Implemented in CBMC 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/fma.rs | 26 +++++++++++++++++++ 3 files changed, 30 insertions(+), 4 deletions(-) create mode 100644 tests/kani/Intrinsics/Math/Arith/fma.rs diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index f97db5d8ab6c..77392cd37fc6 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -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 | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 91f7ea20c9b1..8f93a4c61553 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -447,8 +447,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); diff --git a/tests/kani/Intrinsics/Math/Arith/fma.rs b/tests/kani/Intrinsics/Math/Arith/fma.rs new file mode 100644 index 000000000000..379d5aa81db5 --- /dev/null +++ b/tests/kani/Intrinsics/Math/Arith/fma.rs @@ -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); +}