From 93b3081222a9f54a288979ec393fb4cb0c5ed757 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 29 Jul 2024 21:07:55 +0200 Subject: [PATCH 1/4] Update the rust toolchain to nightly-2024-07-29 (#3392) Changes required due to: - rust-lang/rust@9db265048e Bump to 1.82 Resolves: #3369 Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Celina G. Val --- .github/workflows/verify-std-check.yml | 1 + kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs | 2 +- kani-compiler/src/session.rs | 4 ++-- rust-toolchain.toml | 2 +- 4 files changed, 5 insertions(+), 4 deletions(-) diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml index 667be6b340c5..2ab65be36053 100644 --- a/.github/workflows/verify-std-check.yml +++ b/.github/workflows/verify-std-check.yml @@ -39,6 +39,7 @@ jobs: uses: actions/checkout@v4 with: path: kani + fetch-depth: 0 - name: Setup Kani Dependencies uses: ./kani/.github/actions/setup diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs index aeaf8e0e2d10..0c69cb30b37f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs @@ -25,7 +25,7 @@ pub fn init() { /// Custom panic hook to add more information when panic occurs during goto-c codegen. #[allow(clippy::type_complexity)] -static DEFAULT_HOOK: LazyLock) + Sync + Send + 'static>> = +static DEFAULT_HOOK: LazyLock) + Sync + Send + 'static>> = LazyLock::new(|| { let hook = panic::take_hook(); panic::set_hook(Box::new(|info| { diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index bc0930eb9e4b..7ec2b79a0469 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -29,7 +29,7 @@ const BUG_REPORT_URL: &str = // Custom panic hook when running under user friendly message format. #[allow(clippy::type_complexity)] -static PANIC_HOOK: LazyLock) + Sync + Send + 'static>> = +static PANIC_HOOK: LazyLock) + Sync + Send + 'static>> = LazyLock::new(|| { let hook = panic::take_hook(); panic::set_hook(Box::new(|info| { @@ -46,7 +46,7 @@ static PANIC_HOOK: LazyLock) + Sync + Send + 's // Custom panic hook when executing under json error format `--error-format=json`. #[allow(clippy::type_complexity)] -static JSON_PANIC_HOOK: LazyLock) + Sync + Send + 'static>> = +static JSON_PANIC_HOOK: LazyLock) + Sync + Send + 'static>> = LazyLock::new(|| { let hook = panic::take_hook(); panic::set_hook(Box::new(|info| { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 27c29bb820e2..18eb2aa4836f 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-07-21" +channel = "nightly-2024-07-29" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 7cd31aa3fea07f0326f43e62d8b30764f8354dda Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 29 Jul 2024 14:32:25 -0700 Subject: [PATCH 2/4] Fix verify-std-check outcome check (#3394) It looks like I used `output` instead of `outcome` variable. I noticed that [this PR](https://github.com/model-checking/kani/pull/3392) should've failed the workflow but it didn't because of this mistake. Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com> --- .github/workflows/verify-std-check.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml index 2ab65be36053..1bad09cd3c6d 100644 --- a/.github/workflows/verify-std-check.yml +++ b/.github/workflows/verify-std-check.yml @@ -80,8 +80,10 @@ jobs: -Z mem-predicates -Z ptr-to-ref-cast-checks - name: Compare PR results - if: steps.check-head.outcome != 'success' && steps.check-head.output != github.check-base.output + if: steps.check-head.outcome != 'success' && steps.check-head.outcome != steps.check-base.outcome run: | echo "New failure introduced by this change" + echo "HEAD: ${{ steps.check-head.outcome }}" + echo "BASE: ${{ steps.check-base.outcome }}" exit 1 From 1e0b71dfa44176c32d1ac80bfee375c6ff64d5b8 Mon Sep 17 00:00:00 2001 From: Matias Scharager Date: Tue, 30 Jul 2024 00:11:40 -0400 Subject: [PATCH 3/4] Function Contracts: Interior Mutability Tests (#3351) Test cases for interior mutability using Cell, OnceCell, UnsafeCell, and RefCell. 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: Matias Scharager Co-authored-by: Felipe R. Monteiro --- .../interior-mutability/api/cell.expected | 6 +++ .../interior-mutability/api/cell.rs | 25 ++++++++++++ .../api/cell_stub.expected | 9 +++++ .../interior-mutability/api/cell_stub.rs | 40 +++++++++++++++++++ .../api/unsafecell.expected | 6 +++ .../interior-mutability/api/unsafecell.rs | 24 +++++++++++ .../whole-struct/cell.expected | 6 +++ .../interior-mutability/whole-struct/cell.rs | 25 ++++++++++++ .../whole-struct/oncecell.expected | 6 +++ .../whole-struct/oncecell.rs | 24 +++++++++++ .../whole-struct/refcell.expected | 6 +++ .../whole-struct/refcell.rs | 25 ++++++++++++ .../whole-struct/unsafecell.expected | 6 +++ .../whole-struct/unsafecell.rs | 25 ++++++++++++ 14 files changed, 233 insertions(+) create mode 100644 tests/expected/function-contract/interior-mutability/api/cell.expected create mode 100644 tests/expected/function-contract/interior-mutability/api/cell.rs create mode 100644 tests/expected/function-contract/interior-mutability/api/cell_stub.expected create mode 100644 tests/expected/function-contract/interior-mutability/api/cell_stub.rs create mode 100644 tests/expected/function-contract/interior-mutability/api/unsafecell.expected create mode 100644 tests/expected/function-contract/interior-mutability/api/unsafecell.rs create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/cell.expected create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/cell.rs create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected create mode 100644 tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs diff --git a/tests/expected/function-contract/interior-mutability/api/cell.expected b/tests/expected/function-contract/interior-mutability/api/cell.expected new file mode 100644 index 000000000000..d9b0f5d51e5c --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/api/cell.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| im.x.get() < 101"\ +in function modify + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/api/cell.rs b/tests/expected/function-contract/interior-mutability/api/cell.rs new file mode 100644 index 000000000000..671b6b206ef3 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/api/cell.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +/// Mutating Cell via `as_ptr` in contracts +use std::cell::Cell; + +/// This struct contains Cell which can be mutated +struct InteriorMutability { + x: Cell, +} + +#[kani::requires(im.x.get() < 100)] +#[kani::modifies(im.x.as_ptr())] +#[kani::ensures(|_| im.x.get() < 101)] +///im is an immutable reference with interior mutability +fn modify(im: &InteriorMutability) { + im.x.set(im.x.get() + 1) +} + +#[kani::proof_for_contract(modify)] +fn harness_for_modify() { + let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) }; + modify(&im) +} diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.expected b/tests/expected/function-contract/interior-mutability/api/cell_stub.expected new file mode 100644 index 000000000000..b8da35411e53 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.expected @@ -0,0 +1,9 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| old(im.x.get() + im.x.get()) == im.x.get()"\ + +assertion\ +- Status: SUCCESS\ +- Description: "|_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get()"\ + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/api/cell_stub.rs b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs new file mode 100644 index 000000000000..d01ca379655f --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/api/cell_stub.rs @@ -0,0 +1,40 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +/// The objective of this test is to show that the contracts for double can be replaced as a stub within the contracts for quadruple. +/// This shows that we can generate `kani::any()` for Cell. +use std::cell::Cell; + +/// This struct contains Cell which can be mutated +struct InteriorMutability { + x: Cell, +} + +#[kani::ensures(|_| old(im.x.get() + im.x.get()) == im.x.get())] +#[kani::requires(im.x.get() < 100)] +#[kani::modifies(im.x.as_ptr())] +fn double(im: &InteriorMutability) { + im.x.set(im.x.get() + im.x.get()) +} + +#[kani::proof_for_contract(double)] +fn double_harness() { + let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) }; + double(&im); +} + +#[kani::ensures(|_| old(im.x.get() + im.x.get() + im.x.get() + im.x.get()) == im.x.get())] +#[kani::requires(im.x.get() < 50)] +#[kani::modifies(im.x.as_ptr())] +fn quadruple(im: &InteriorMutability) { + double(im); + double(im) +} + +#[kani::proof_for_contract(quadruple)] +#[kani::stub_verified(double)] +fn quadruple_harness() { + let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) }; + quadruple(&im); +} diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.expected b/tests/expected/function-contract/interior-mutability/api/unsafecell.expected new file mode 100644 index 000000000000..1646a8a78e7f --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| unsafe{ *im.x.get() } < 101"\ +in function modify + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/api/unsafecell.rs b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs new file mode 100644 index 000000000000..8125e3e3c077 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/api/unsafecell.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +use std::cell::UnsafeCell; + +/// This struct contains UnsafeCell which can be mutated +struct InteriorMutability { + x: UnsafeCell, +} + +#[kani::requires(unsafe{*im.x.get()} < 100)] +#[kani::modifies(im.x.get())] +#[kani::ensures(|_| unsafe{*im.x.get()} < 101)] +/// `im` is an immutable reference with interior mutability +fn modify(im: &InteriorMutability) { + unsafe { *im.x.get() += 1 } +} + +#[kani::proof_for_contract(modify)] +fn harness_for_modify() { + let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) }; + modify(&im) +} diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected new file mode 100644 index 000000000000..d9b0f5d51e5c --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| im.x.get() < 101"\ +in function modify + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs new file mode 100644 index 000000000000..9f42f6fa1f6c --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/cell.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +/// The objective of this test is to check the modification of a Cell used as interior mutability in an immutable struct +use std::cell::Cell; + +/// This struct contains Cell which can be mutated +struct InteriorMutability { + x: Cell, +} + +#[kani::requires(im.x.get() < 100)] +#[kani::modifies(&im.x)] +#[kani::ensures(|_| im.x.get() < 101)] +/// `im` is an immutable reference with interior mutability +fn modify(im: &InteriorMutability) { + im.x.set(im.x.get() + 1) +} + +#[kani::proof_for_contract(modify)] +fn harness_for_modify() { + let im: InteriorMutability = InteriorMutability { x: Cell::new(kani::any()) }; + modify(&im) +} diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected new file mode 100644 index 000000000000..a367bcd9fb95 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| im.x.get().is_some()"\ +in function modify + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs new file mode 100644 index 000000000000..6ca32251b60c --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/oncecell.rs @@ -0,0 +1,24 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +/// The objective of this test is to check the modification of an OnceCell used as interior mutability in an immutable struct +use std::cell::OnceCell; + +/// This struct contains OnceCell which can be mutated +struct InteriorMutability { + x: OnceCell, +} + +#[kani::requires(im.x.get().is_none())] +#[kani::modifies(&im.x)] +#[kani::ensures(|_| im.x.get().is_some())] +fn modify(im: &InteriorMutability) { + im.x.set(5).expect("") +} + +#[kani::proof_for_contract(modify)] +fn harness_for_modify() { + let im: InteriorMutability = InteriorMutability { x: OnceCell::new() }; + modify(&im) +} diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected new file mode 100644 index 000000000000..225c290a171e --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| unsafe{ *im.x.as_ptr() } < 101"\ +in function modify + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs new file mode 100644 index 000000000000..1cce5e2364c3 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/refcell.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +/// The objective of this test is to check the modification of a RefCell used as interior mutability in an immutable struct +use std::cell::RefCell; + +/// This struct contains Cell which can be mutated +struct InteriorMutability { + x: RefCell, +} + +#[kani::requires(unsafe{*im.x.as_ptr()} < 100)] +#[kani::modifies(&im.x)] +#[kani::ensures(|_| unsafe{*im.x.as_ptr()} < 101)] +/// `im` is an immutable reference with interior mutability +fn modify(im: &InteriorMutability) { + im.x.replace_with(|&mut old| old + 1); +} + +#[kani::proof_for_contract(modify)] +fn harness_for_modify() { + let im: InteriorMutability = InteriorMutability { x: RefCell::new(kani::any()) }; + modify(&im) +} diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected new file mode 100644 index 000000000000..1646a8a78e7f --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.expected @@ -0,0 +1,6 @@ +assertion\ +- Status: SUCCESS\ +- Description: "|_| unsafe{ *im.x.get() } < 101"\ +in function modify + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs new file mode 100644 index 000000000000..6adb7b12c8b1 --- /dev/null +++ b/tests/expected/function-contract/interior-mutability/whole-struct/unsafecell.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +/// The objective of this test is to check the modification of an UnsafeCell used as interior mutability in an immutable struct +use std::cell::UnsafeCell; + +/// This struct contains UnsafeCell which can be mutated +struct InteriorMutability { + x: UnsafeCell, +} + +#[kani::requires(unsafe{*im.x.get()} < 100)] +#[kani::modifies(im.x.get())] +#[kani::ensures(|_| unsafe{*im.x.get()} < 101)] +/// `im` is an immutable reference with interior mutability +fn modify(im: &InteriorMutability) { + unsafe { *im.x.get() += 1 } +} + +#[kani::proof_for_contract(modify)] +fn harness_for_modify() { + let im: InteriorMutability = InteriorMutability { x: UnsafeCell::new(kani::any()) }; + modify(&im) +} From 1553ae21369ada3a0bb58ef42d61bbdb8676da5a Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 30 Jul 2024 10:54:17 +0000 Subject: [PATCH 4/4] Automatic toolchain upgrade to nightly-2024-07-30 (#3395) Update Rust toolchain from nightly-2024-07-29 to nightly-2024-07-30 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/2cbbe8b8bb2be672b14cf741a2f0ec24a49f3f0b up to https://github.com/rust-lang/rust/commit/612a33f20b9b2c27380edbc4b26a01433ed114bc. --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 18eb2aa4836f..10c7645cf1d7 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-07-29" +channel = "nightly-2024-07-30" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]