diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml new file mode 100644 index 000000000000..1bad09cd3c6d --- /dev/null +++ b/.github/workflows/verify-std-check.yml @@ -0,0 +1,89 @@ +# 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 + fetch-depth: 0 + + - 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.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 + 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 + 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", ] 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..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-21" +channel = "nightly-2024-07-30" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] 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) +} 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