From b5ddbb8272ff1dc7068d43f0c75686445bfa051b Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Mon, 18 Mar 2024 06:22:20 -0700 Subject: [PATCH 1/4] Disable removal of storage markers (#3083) Instead of turning on the address sanitizer to ensure storage markers (`StorageLive` and `StorageDead`) are kept in MIR, directly disable the MIR pass that removes them from MIR (https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/.E2.9C.94.20Keeping.20MIR's.20storage.20markers). This is to ensure we don't get additional instrumentation that is not relevant for Kani, and may unnecessarily increase the code size and compilation time. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- kani-driver/src/call_single_file.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs index fc41bac69d9c..4e8086e7e37b 100644 --- a/kani-driver/src/call_single_file.rs +++ b/kani-driver/src/call_single_file.rs @@ -123,7 +123,7 @@ impl KaniSession { "-Z", "panic_abort_tests=yes", "-Z", - "sanitizer=address", + "mir-enable-passes=-RemoveStorageMarkers", ] .map(OsString::from), ); From cffa07ce8a463e7934c42dc5a45270ebe2687cd1 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 18 Mar 2024 15:33:07 +0000 Subject: [PATCH 2/4] Automatic cargo update to 2024-03-18 (#3086) Dependency upgrade resulting from `cargo update`. --- Cargo.lock | 70 +++++++++++++++++++++++++++++------------------------- 1 file changed, 38 insertions(+), 32 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 89c60b06eec7..d0b86eaf9206 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -83,9 +83,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.80" +version = "1.0.81" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5ad32ce52e4161730f7098c077cd2ed6229b5804ccf99e5366be1ab72a98b4e1" +checksum = "0952808a6c2afd1aa8947271f3a60f1a6763c7b912d210184c5149b5cf147247" [[package]] name = "autocfg" @@ -169,9 +169,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.5.2" +version = "4.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b230ab84b0ffdf890d5a10abdbc8b83ae1c4918275daea1ab8801f71536b2651" +checksum = "949626d00e063efc93b6dca932419ceb5432f99769911c0b995f7e884c778813" dependencies = [ "clap_builder", "clap_derive", @@ -191,14 +191,14 @@ dependencies = [ [[package]] name = "clap_derive" -version = "4.5.0" +version = "4.5.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "307bc0538d5f0f83b8248db3087aa92fe504e4691294d0c96c0eabc33f47ba47" +checksum = "90239a040c80f5e14809ca132ddc4176ab33d5e17e49691793296e3fcb34d72f" dependencies = [ - "heck", + "heck 0.5.0", "proc-macro2", "quote", - "syn 2.0.52", + "syn 2.0.53", ] [[package]] @@ -392,6 +392,12 @@ version = "0.4.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "95505c38b4572b2d910cecb0281560f54b440a19336cbbcb27bf6ce6adc6f5a8" +[[package]] +name = "heck" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" + [[package]] name = "home" version = "0.5.9" @@ -498,7 +504,7 @@ dependencies = [ "proc-macro-error", "proc-macro2", "quote", - "syn 2.0.52", + "syn 2.0.53", ] [[package]] @@ -670,12 +676,12 @@ checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92" [[package]] name = "os_info" -version = "3.7.0" +version = "3.8.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "006e42d5b888366f1880eda20371fedde764ed2213dc8496f49622fa0c99cd5e" +checksum = "6cbb46d5d01695d7a1fb8be5f0d1968bd2b2b8ba1d1b3e7062ce2a0593e57af1" dependencies = [ "log", - "winapi", + "windows-sys", ] [[package]] @@ -751,9 +757,9 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.78" +version = "1.0.79" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2422ad645d89c99f8f3e6b88a9fdeca7fabeac836b1002371c4367c8f984aae" +checksum = "e835ff2298f5721608eb1a980ecaee1aef2c132bf95ecc026a11b7bf3c01c02e" dependencies = [ "unicode-ident", ] @@ -966,7 +972,7 @@ checksum = "7eb0b34b42edc17f6b7cac84a52a1c5f0e1bb2227e997ca9011ea3dd34e8610b" dependencies = [ "proc-macro2", "quote", - "syn 2.0.52", + "syn 2.0.53", ] [[package]] @@ -1000,9 +1006,9 @@ dependencies = [ [[package]] name = "serde_yaml" -version = "0.9.32" +version = "0.9.33" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8fd075d994154d4a774f95b51fb96bdc2832b0ea48425c92546073816cda1f2f" +checksum = "a0623d197252096520c6f2a5e1171ee436e5af99a5d7caa2891e55e61950e6d9" dependencies = [ "indexmap", "itoa", @@ -1074,11 +1080,11 @@ version = "0.25.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "23dc1fa9ac9c169a78ba62f0b841814b7abae11bdd047b9c58f893439e309ea0" dependencies = [ - "heck", + "heck 0.4.1", "proc-macro2", "quote", "rustversion", - "syn 2.0.52", + "syn 2.0.53", ] [[package]] @@ -1087,11 +1093,11 @@ version = "0.26.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c6cf59daf282c0a494ba14fd21610a0325f9f90ec9d1231dea26bcb1d696c946" dependencies = [ - "heck", + "heck 0.4.1", "proc-macro2", "quote", "rustversion", - "syn 2.0.52", + "syn 2.0.53", ] [[package]] @@ -1106,9 +1112,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.52" +version = "2.0.53" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b699d15b36d1f02c3e7c69f8ffef53de37aefae075d8488d4ba1a7788d574a07" +checksum = "7383cd0e49fff4b6b90ca5670bfd3e9d6a733b3f90c686605aa7eec8c4996032" dependencies = [ "proc-macro2", "quote", @@ -1129,22 +1135,22 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.57" +version = "1.0.58" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1e45bcbe8ed29775f228095caf2cd67af7a4ccf756ebff23a306bf3e8b47b24b" +checksum = "03468839009160513471e86a034bb2c5c0e4baae3b43f79ffc55c4a5427b3297" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.57" +version = "1.0.58" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a953cb265bef375dae3de6663da4d3804eee9682ea80d8e2542529b73c531c81" +checksum = "c61f3ba182994efc43764a46c018c347bc492c79f024e705f46567b418f6d4f7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.52", + "syn 2.0.53", ] [[package]] @@ -1210,7 +1216,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.52", + "syn 2.0.53", ] [[package]] @@ -1289,9 +1295,9 @@ checksum = "e51733f11c9c4f72aa0c160008246859e340b00807569a0da0e7a1079b27ba85" [[package]] name = "unsafe-libyaml" -version = "0.2.10" +version = "0.2.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ab4c90930b95a82d00dc9e9ac071b4991924390d46cbd0dfe566148667605e4b" +checksum = "673aac59facbab8a9007c7f6108d11f63b603f7cabff99fabf650fea5c32b861" [[package]] name = "utf8parse" @@ -1529,5 +1535,5 @@ checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6" dependencies = [ "proc-macro2", "quote", - "syn 2.0.52", + "syn 2.0.53", ] From f54b9564ea07b71a69c4f5091ba2f077ecc0ce93 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 18 Mar 2024 11:39:55 -0700 Subject: [PATCH 3/4] Bump tests/perf/s2n-quic from `1a7faa8` to `9e39ca0` (#3087) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `1a7faa8` to `9e39ca0`.
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 1a7faa87ebcf..9e39ca0f4aa0 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 1a7faa87ebcf2b84a068f21af3306a6f42eb8c74 +Subproject commit 9e39ca0f4aa00ffacc9d65879ccc807460c8b04b From 54786ad85bcae8b80948575900e085e6ed035ab8 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 18 Mar 2024 14:05:36 -0700 Subject: [PATCH 4/4] Upgrade toolchain to nightly-2024-03-15 (#3084) Note that with this upgrade Kani can no longer automatically detect loop bounds when using range. For more details, see: https://github.com/model-checking/kani/issues/3088 --- docs/src/getting-started/verification-results/src/main.rs | 1 + rust-toolchain.toml | 2 +- tests/coverage/unreachable/abort/main.rs | 2 +- tests/expected/abort/main.rs | 1 + tests/expected/iterator/main.rs | 1 + tests/kani/Coroutines/main.rs | 1 + 6 files changed, 6 insertions(+), 2 deletions(-) diff --git a/docs/src/getting-started/verification-results/src/main.rs b/docs/src/getting-started/verification-results/src/main.rs index 7a03b34f0f9e..72653cf4dc8f 100644 --- a/docs/src/getting-started/verification-results/src/main.rs +++ b/docs/src/getting-started/verification-results/src/main.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT #[kani::proof] +#[kani::unwind(4)] // ANCHOR: success_example fn success_example() { let mut sum = 0; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 5b83049feef5..7035d1aba20f 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-03-14" +channel = "nightly-2024-03-15" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/coverage/unreachable/abort/main.rs b/tests/coverage/unreachable/abort/main.rs index 2941ec126f3c..39c0b0efb54f 100644 --- a/tests/coverage/unreachable/abort/main.rs +++ b/tests/coverage/unreachable/abort/main.rs @@ -5,7 +5,7 @@ use std::process; -#[kani::proof] +#[cfg_attr(kani, kani::proof, kani::unwind(5))] fn main() { for i in 0..4 { if i == 1 { diff --git a/tests/expected/abort/main.rs b/tests/expected/abort/main.rs index 2941ec126f3c..9e2f5b7a808c 100644 --- a/tests/expected/abort/main.rs +++ b/tests/expected/abort/main.rs @@ -6,6 +6,7 @@ use std::process; #[kani::proof] +#[kani::unwind(5)] fn main() { for i in 0..4 { if i == 1 { diff --git a/tests/expected/iterator/main.rs b/tests/expected/iterator/main.rs index b1cb4a89cfbf..5cf9402bcb23 100644 --- a/tests/expected/iterator/main.rs +++ b/tests/expected/iterator/main.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT #[kani::proof] +#[kani::unwind(4)] fn main() { let mut z = 1; for i in 1..4 { diff --git a/tests/kani/Coroutines/main.rs b/tests/kani/Coroutines/main.rs index 10d92571aaa6..14cbeb426321 100644 --- a/tests/kani/Coroutines/main.rs +++ b/tests/kani/Coroutines/main.rs @@ -9,6 +9,7 @@ use std::ops::{Coroutine, CoroutineState}; use std::pin::Pin; #[kani::proof] +#[kani::unwind(3)] fn main() { let mut add_one = |mut resume: u8| { loop {