From 70bd0215da3183db04796c93f070d805cc93343b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 26 Jul 2024 11:04:59 -0700 Subject: [PATCH 1/7] Add two new CI workflows to check Kani against `verify-rust-std` (#3386) This PR adds the following workflows: 1. `verify-std-check`: This workflow will run either in a PR or via workflow call. It pulls the `main` branch of `verify-rust-std` repository, and see if it can verify the repo with the new Kani version from HEAD. - If verification succeeds, the workflow will succeed. - If the verification fails and this is a PR, the workflow will compare the verification result against the base of the PR. The workflow will succeed if the results match*. 2. `verify-std-update`: This workflow will run the `verify-std-check` workflow. If it succeeds, it will update the `verify-rust-std` branch from HEAD. This workflow will fail if `features/verify-rust-std` branch diverges, and a merge is required. The motivation for this PR is to help us identify any changes to Kani that may break the Rust verification repository, and to keep the `verify-rust-std` up to date as much as possible. * The fallback logic is needed since toolchain upgrades can potentially break the std verification. This will happen in cases where the new toolchain version is incompatible with the library version from the `verify-rust-std`. Those cases should not interfere with Kani development, and they should be fixed when we update the `verify-rust-std` repo. --- .github/workflows/verify-std-check.yml | 86 +++++++++++++++++++++++++ .github/workflows/verify-std-update.yml | 35 ++++++++++ 2 files changed, 121 insertions(+) create mode 100644 .github/workflows/verify-std-check.yml create mode 100644 .github/workflows/verify-std-update.yml diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml new file mode 100644 index 000000000000..667be6b340c5 --- /dev/null +++ b/.github/workflows/verify-std-check.yml @@ -0,0 +1,86 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# This workflow will try to build and run the `verify-rust-std` repository. +# +# This check should be optional, but it has been added to help provide +# visibility to when a PR may break the `verify-rust-std` repository. +# +# We expect toolchain updates to potentially break this workflow in cases where +# the version tracked in the `verify-rust-std` is not compatible with newer +# versions of the Rust toolchain. +# +# Changes unrelated to the toolchain should match the current status of main. + +name: Check Std Verification +on: + pull_request: + workflow_call: + +env: + RUST_BACKTRACE: 1 + +jobs: + verify-std: + runs-on: ${{ matrix.os }} + strategy: + matrix: + # Kani does not support windows. + os: [ ubuntu-22.04, macos-14 ] + steps: + - name: Checkout Library + uses: actions/checkout@v4 + with: + repository: model-checking/verify-rust-std + path: verify-rust-std + submodules: true + + - name: Checkout `Kani` + uses: actions/checkout@v4 + with: + path: kani + + - name: Setup Kani Dependencies + uses: ./kani/.github/actions/setup + with: + os: ${{ matrix.os }} + kani_dir: kani + + - name: Build Kani + working-directory: kani + run: | + cargo build-dev + echo "$(pwd)/scripts" >> $GITHUB_PATH + + - name: Run verification with HEAD + id: check-head + working-directory: verify-rust-std + continue-on-error: true + run: | + kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \ + -Z mem-predicates -Z ptr-to-ref-cast-checks + + # If the head failed, check if it's a new failure. + - name: Checkout base + working-directory: kani + if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request' + run: | + BASE_REF=${{ github.event.pull_request.base.sha }} + git checkout ${BASE_REF} + cargo build-dev + + - name: Run verification with BASE + id: check-base + if: steps.check-head.outcome != 'success' && github.event_name == 'pull_request' + working-directory: verify-rust-std + continue-on-error: true + run: | + kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \ + -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 + run: | + echo "New failure introduced by this change" + exit 1 + diff --git a/.github/workflows/verify-std-update.yml b/.github/workflows/verify-std-update.yml new file mode 100644 index 000000000000..518f80ecd1b8 --- /dev/null +++ b/.github/workflows/verify-std-update.yml @@ -0,0 +1,35 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +# +# This workflow will try to update the verify std branch. + +name: Update "features/verify-rust-std" +on: + schedule: + - cron: "30 3 * * *" # Run this every day at 03:30 UTC + workflow_dispatch: # Allow manual dispatching. + +env: + RUST_BACKTRACE: 1 + +jobs: + # First ensure the HEAD is compatible with the `verify-rust-std` repository. + verify-std: + name: Verify Std + permissions: { } + uses: ./.github/workflows/verify-std-check.yml + + # Push changes to the features branch. + update-branch: + needs: verify-std + permissions: + contents: write + runs-on: ubuntu-latest + steps: + - name: Checkout Kani + uses: actions/checkout@v4 + + - name: Update feature branch + run: | + git push origin HEAD:features/verify-rust-std + From e4f009978575babe69e341567877e5d23aeddc18 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 29 Jul 2024 11:56:52 +0200 Subject: [PATCH 2/7] Automatic cargo update to 2024-07-29 (#3390) Dependency upgrade resulting from `cargo update`. --- Cargo.lock | 73 +++++++++++++++++++++++++++--------------------------- 1 file changed, 37 insertions(+), 36 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 0fd31f73278b..01dbccdd546a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -25,9 +25,9 @@ dependencies = [ [[package]] name = "anstream" -version = "0.6.14" +version = "0.6.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "418c75fa768af9c03be99d17643f93f79bbba589895012a80e3452a19ddda15b" +checksum = "64e15c1ab1f89faffbf04a634d5e1962e9074f2741eef6d97f3c4e322426d526" dependencies = [ "anstyle", "anstyle-parse", @@ -40,33 +40,33 @@ dependencies = [ [[package]] name = "anstyle" -version = "1.0.7" +version = "1.0.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "038dfcf04a5feb68e9c60b21c9625a54c2c0616e79b72b0fd87075a056ae1d1b" +checksum = "1bec1de6f59aedf83baf9ff929c98f2ad654b97c9510f4e70cf6f661d49fd5b1" [[package]] name = "anstyle-parse" -version = "0.2.4" +version = "0.2.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c03a11a9034d92058ceb6ee011ce58af4a9bf61491aa7e1e59ecd24bd40d22d4" +checksum = "eb47de1e80c2b463c735db5b217a0ddc39d612e7ac9e2e96a5aed1f57616c1cb" dependencies = [ "utf8parse", ] [[package]] name = "anstyle-query" -version = "1.1.0" +version = "1.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad186efb764318d35165f1758e7dcef3b10628e26d41a44bc5550652e6804391" +checksum = "6d36fc52c7f6c869915e99412912f22093507da8d9e942ceaf66fe4b7c14422a" dependencies = [ "windows-sys", ] [[package]] name = "anstyle-wincon" -version = "3.0.3" +version = "3.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61a38449feb7068f52bb06c12759005cf459ee52bb4adc1d5a7c4322d716fb19" +checksum = "5bf74e1b6e971609db8ca7a9ce79fd5768ab6ae46441c572e46cf596f59e57f8" dependencies = [ "anstyle", "windows-sys", @@ -140,9 +140,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.5.9" +version = "4.5.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "64acc1846d54c1fe936a78dc189c34e28d3f5afc348403f28ecf53660b9b8462" +checksum = "35723e6a11662c2afb578bcf0b88bf6ea8e21282a953428f240574fcc3a2b5b3" dependencies = [ "clap_builder", "clap_derive", @@ -150,9 +150,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.5.9" +version = "4.5.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6fb8393d67ba2e7bfaf28a23458e4e2b543cc73a99595511eb207fdb8aede942" +checksum = "49eb96cbfa7cfa35017b7cd548c75b14c3118c98b423041d70562665e07fb0fa" dependencies = [ "anstream", "anstyle", @@ -162,9 +162,9 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.5.8" +version = "4.5.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2bac35c6dafb060fd4d275d9a4ffae97917c13a6327903a8be2153cd964f7085" +checksum = "5d029b67f89d30bbb547c89fd5161293c0aec155fc691d7924b64550662db93e" dependencies = [ "heck", "proc-macro2", @@ -174,15 +174,15 @@ dependencies = [ [[package]] name = "clap_lex" -version = "0.7.1" +version = "0.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4b82cf0babdbd58558212896d1a4272303a57bdb245c2bf1147185fb45640e70" +checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97" [[package]] name = "colorchoice" -version = "1.0.1" +version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b6a852b24ab71dffc585bcb46eaf7959d175cb865a7152e35b348d1b2960422" +checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0" [[package]] name = "comfy-table" @@ -384,9 +384,9 @@ dependencies = [ [[package]] name = "is_terminal_polyfill" -version = "1.70.0" +version = "1.70.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f8478577c03552c21db0e2724ffb8986a5ce7af88107e6be5d2ee6e158c12800" +checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" [[package]] name = "itertools" @@ -929,20 +929,21 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.120" +version = "1.0.121" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4e0d21c9a8cae1235ad58a00c11cb40d4b1e5c784f1ef2c537876ed6ffd8b7c5" +checksum = "4ab380d7d9f22ef3f21ad3e6c1ebe8e4fc7a2000ccba2e4d71fc96f15b2cb609" dependencies = [ "itoa", + "memchr", "ryu", "serde", ] [[package]] name = "serde_spanned" -version = "0.6.6" +version = "0.6.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "79e674e01f999af37c49f70a6ede167a8a60b2503e56c5599532a65baa5969a0" +checksum = "eb5b1b31579f3811bf615c144393417496f152e12ac8b7663bf664f4a815306d" dependencies = [ "serde", ] @@ -1098,9 +1099,9 @@ dependencies = [ [[package]] name = "toml" -version = "0.8.15" +version = "0.8.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ac2caab0bf757388c6c0ae23b3293fdb463fee59434529014f85e3263b995c28" +checksum = "81967dd0dd2c1ab0bc3468bd7caecc32b8a4aa47d0c8c695d8c2b2108168d62c" dependencies = [ "serde", "serde_spanned", @@ -1110,18 +1111,18 @@ dependencies = [ [[package]] name = "toml_datetime" -version = "0.6.6" +version = "0.6.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4badfd56924ae69bcc9039335b2e017639ce3f9b001c393c1b2d1ef846ce2cbf" +checksum = "f8fb9f64314842840f1d940ac544da178732128f1c78c21772e876579e0da1db" dependencies = [ "serde", ] [[package]] name = "toml_edit" -version = "0.22.16" +version = "0.22.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "278f3d518e152219c994ce877758516bca5e118eaed6996192a774fb9fbf0788" +checksum = "8d9f8729f5aea9562aac1cc0441f5d6de3cff1ee0c5d67293eeca5eb36ee7c16" dependencies = [ "indexmap", "serde", @@ -1237,9 +1238,9 @@ checksum = "830b7e5d4d90034032940e4ace0d9a9a057e7a45cd94e6c007832e39edb82f6d" [[package]] name = "version_check" -version = "0.9.4" +version = "0.9.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" +checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" [[package]] name = "wait-timeout" @@ -1384,9 +1385,9 @@ checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" [[package]] name = "winnow" -version = "0.6.14" +version = "0.6.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "374ec40a2d767a3c1b4972d9475ecd557356637be906f2cb3f7fe17a6eb5e22f" +checksum = "b480ae9340fc261e6be3e95a1ba86d54ae3f9171132a73ce8d4bbaf68339507c" dependencies = [ "memchr", ] From 91d182953b46b164daf657641f9be78979bfb566 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 29 Jul 2024 10:06:55 -0700 Subject: [PATCH 3/7] Bump tests/perf/s2n-quic from `75afd77` to `cc4e6d0` (#3393) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `75afd77` to `cc4e6d0`.
Commits

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `@dependabot rebase`. [//]: # (dependabot-automerge-start) [//]: # (dependabot-automerge-end) ---
Dependabot commands and options
You can trigger Dependabot actions by commenting on this PR: - `@dependabot rebase` will rebase this PR - `@dependabot recreate` will recreate this PR, overwriting any edits that have been made to it - `@dependabot merge` will merge this PR after your CI passes on it - `@dependabot squash and merge` will squash and merge this PR after your CI passes on it - `@dependabot cancel merge` will cancel a previously requested merge and block automerging - `@dependabot reopen` will reopen this PR if it is closed - `@dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually - `@dependabot show ignore conditions` will show all of the ignore conditions of the specified dependency - `@dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself) - `@dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
Signed-off-by: dependabot[bot] Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com> --- tests/perf/s2n-quic | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/perf/s2n-quic b/tests/perf/s2n-quic index 75afd77dfa88..cc4e6d023f8e 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 75afd77dfa88d696900f12ee747409ddb208a745 +Subproject commit cc4e6d023f8edf92fea294dcaea2fd5a1132cb47 From 93b3081222a9f54a288979ec393fb4cb0c5ed757 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 29 Jul 2024 21:07:55 +0200 Subject: [PATCH 4/7] 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 5/7] 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 6/7] 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 7/7] 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"]