From 8398771cf598e842d963ff319cec90544166a8dd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 13 Dec 2024 16:31:22 +0100 Subject: [PATCH 01/24] Update cargo dependencies (#3776) This includes updates beyond patch version level to `cargo_metadata` and `tree-sitter` (and `tree-sitter-rust`), which required code changes. (Updating `which` did not entail code changes.) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- Cargo.lock | 115 ++++++++++++++++++++++---------- cprover_bindings/Cargo.toml | 2 +- deny.toml | 4 +- kani-driver/Cargo.toml | 4 +- kani-driver/src/call_cargo.rs | 32 ++++----- tools/build-kani/Cargo.toml | 4 +- tools/build-kani/src/sysroot.rs | 12 ++-- tools/kani-cov/Cargo.toml | 4 +- tools/kani-cov/src/coverage.rs | 2 +- 9 files changed, 111 insertions(+), 68 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 7931066348b7..0c2954adf118 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -160,9 +160,9 @@ dependencies = [ [[package]] name = "bstr" -version = "1.11.0" +version = "1.11.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1a68f1f47cdf0ec8ee4b941b2eee2a80cb796db73118c0dd09ac63fbe405be22" +checksum = "786a307d683a5bf92e6fd5fd69a7eb613751668d1d8d67d802846dfe367c62c8" dependencies = [ "memchr", "regex-automata 0.4.9", @@ -176,7 +176,7 @@ dependencies = [ "anyhow", "cargo_metadata", "clap", - "which", + "which 7.0.0", ] [[package]] @@ -211,23 +211,23 @@ dependencies = [ [[package]] name = "cargo_metadata" -version = "0.18.1" +version = "0.19.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2d886547e41f740c616ae73108f6eb70afe6d940c7bc697cb30f13daec073037" +checksum = "8769706aad5d996120af43197bf46ef6ad0fda35216b4505f926a365a232d924" dependencies = [ "camino", "cargo-platform", "semver", "serde", "serde_json", - "thiserror", + "thiserror 2.0.6", ] [[package]] name = "cc" -version = "1.2.3" +version = "1.2.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "27f657647bcff5394bf56c7317665bbf790a137a50eaaa5c6bfbb9e27a518f2d" +checksum = "9157bbaa6b165880c27a4293a474c91cdcf265cc68cc829bf10be0964a391caf" dependencies = [ "shlex", ] @@ -273,7 +273,7 @@ dependencies = [ "tracing", "tracing-subscriber", "tracing-tree 0.4.0 (git+https://github.com/Nadrieril/tracing-tree)", - "which", + "which 6.0.3", ] [[package]] @@ -587,6 +587,12 @@ version = "0.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80" +[[package]] +name = "foldhash" +version = "0.1.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f81ec6369c545a7d40e4589b5597581fa1c441fe1cce96dd1de43159910a36a2" + [[package]] name = "getopts" version = "0.2.21" @@ -627,7 +633,7 @@ checksum = "3a6ad932c6dd3cfaf16b66754a42f87bbeefd591530c4b6a8334270a7df3e853" dependencies = [ "ahash", "petgraph", - "thiserror", + "thiserror 1.0.69", ] [[package]] @@ -644,6 +650,9 @@ name = "hashbrown" version = "0.15.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bf151400ff0baff5465007dd2f3e717f3fe502074ca563069ce3a6629d07b289" +dependencies = [ + "foldhash", +] [[package]] name = "hashlink" @@ -819,7 +828,7 @@ dependencies = [ "toml", "tracing", "tracing-subscriber", - "which", + "which 7.0.0", ] [[package]] @@ -867,9 +876,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" [[package]] name = "libc" -version = "0.2.167" +version = "0.2.168" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09d6582e104315a817dff97f75133544b2e094ee22447d2acf4a74e189ba06fc" +checksum = "5aaeb2981e0606ca11d79718f8bb01164f1d6ed75080182d3abf017e6d244b6d" [[package]] name = "linear-map" @@ -1319,9 +1328,9 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.5.7" +version = "0.5.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f" +checksum = "03a862b389f93e68874fbf580b9de08dd02facb9a788ebadaf4a3fd33cf58834" dependencies = [ "bitflags", ] @@ -1449,18 +1458,18 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "semver" -version = "1.0.23" +version = "1.0.24" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61697e0a1c7e512e84a621326239844a24d8207b4669b41bc18b32ea5cbf988b" +checksum = "3cb6eb87a131f756572d7fb904f6e7b68633f09cca868c5df1c4b8d1a694bbba" dependencies = [ "serde", ] [[package]] name = "serde" -version = "1.0.215" +version = "1.0.216" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6513c1ad0b11a9376da888e3e0baa0077f1aed55c17f50e7b2397136129fb88f" +checksum = "0b9781016e935a97e8beecf0c933758c97a5520d32930e460142b4cd80c6338e" dependencies = [ "serde_derive", ] @@ -1476,9 +1485,9 @@ dependencies = [ [[package]] name = "serde_derive" -version = "1.0.215" +version = "1.0.216" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0" +checksum = "46f859dbbf73865c6627ed570e78961cd3ac92407a2d117204c49232485da55e" dependencies = [ "proc-macro2", "quote", @@ -1595,14 +1604,19 @@ dependencies = [ "kani", ] +[[package]] +name = "streaming-iterator" +version = "0.1.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2b2231b7c3057d5e4ad0156fb3dc807d900806020c5ffa3ee6ff2c8c76fb8520" + [[package]] name = "string-interner" -version = "0.17.0" +version = "0.18.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1c6a0d765f5807e98a091107bae0a56ea3799f66a5de47b2c84c94a39c09974e" +checksum = "1a3275464d7a9f2d4cac57c89c2ef96a8524dba2864c8d6f82e3980baf136f9b" dependencies = [ - "cfg-if", - "hashbrown 0.14.5", + "hashbrown 0.15.2", "serde", ] @@ -1684,7 +1698,16 @@ version = "1.0.69" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52" dependencies = [ - "thiserror-impl", + "thiserror-impl 1.0.69", +] + +[[package]] +name = "thiserror" +version = "2.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8fec2a1820ebd077e2b90c4df007bebf344cd394098a13c563957d0afc83ea47" +dependencies = [ + "thiserror-impl 2.0.6", ] [[package]] @@ -1698,6 +1721,17 @@ dependencies = [ "syn 2.0.90", ] +[[package]] +name = "thiserror-impl" +version = "2.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d65750cab40f4ff1929fb1ba509e9914eb756131cef4210da8d5d700d26f6312" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.90", +] + [[package]] name = "thread_local" version = "1.1.8" @@ -1747,7 +1781,7 @@ version = "0.1.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8450ade61b78735ed7811cc14639462723d87a6cd748a41e7bfde554ac5033dd" dependencies = [ - "thiserror", + "thiserror 1.0.69", ] [[package]] @@ -1900,30 +1934,31 @@ dependencies = [ [[package]] name = "tree-sitter" -version = "0.23.2" +version = "0.24.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0203df02a3b6dd63575cc1d6e609edc2181c9a11867a271b25cfd2abff3ec5ca" +checksum = "8ac95b18f0f727aaaa012bd5179a1916706ee3ed071920fdbda738750b0c0bf5" dependencies = [ "cc", "regex", "regex-syntax 0.8.5", + "streaming-iterator", "tree-sitter-language", ] [[package]] name = "tree-sitter-language" -version = "0.1.2" +version = "0.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e8ddffe35a0e5eeeadf13ff7350af564c6e73993a24db62caee1822b185c2600" +checksum = "c199356c799a8945965bb5f2c55b2ad9d9aa7c4b4f6e587fe9dea0bc715e5f9c" [[package]] name = "tree-sitter-rust" -version = "0.21.2" +version = "0.23.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "277690f420bf90741dea984f3da038ace46c4fe6047cba57a66822226cde1c93" +checksum = "a4d64d449ca63e683c562c7743946a646671ca23947b9c925c0cfbe65051a4af" dependencies = [ "cc", - "tree-sitter", + "tree-sitter-language", ] [[package]] @@ -2017,6 +2052,18 @@ dependencies = [ "winsafe", ] +[[package]] +name = "which" +version = "7.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c9cad3279ade7346b96e38731a641d7343dd6a53d55083dd54eadfa5a1b38c6b" +dependencies = [ + "either", + "home", + "rustix", + "winsafe", +] + [[package]] name = "winapi" version = "0.3.9" diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index e26f23d5c081..a190019d4cc2 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -17,7 +17,7 @@ lazy_static = "1.4.0" num = "0.4.0" num-traits = "0.2" serde = {version = "1", features = ["derive"]} -string-interner = "0.17.0" +string-interner = "0.18" tracing = "0.1" linear-map = {version = "1.2", features = ["serde_impl"]} diff --git a/deny.toml b/deny.toml index 0347d4ac177a..f0b9049ffc03 100644 --- a/deny.toml +++ b/deny.toml @@ -16,14 +16,13 @@ yanked = "deny" allow = [ "MIT", "Apache-2.0", - "MPL-2.0", ] confidence-threshold = 0.8 # All these exceptions should probably appear in: tools/build-kani/license-notes.txt exceptions = [ { name = "unicode-ident", allow=["Unicode-3.0"] }, - { name = "rustc_apfloat", allow=["Apache-2.0 WITH LLVM-exception"] }, + { name = "foldhash", allow=["Zlib"] }, ] [licenses.private] @@ -43,4 +42,3 @@ wildcards = "allow" unknown-registry = "deny" unknown-git = "deny" allow-registry = ["https://github.com/rust-lang/crates.io-index"] -allow-git = ["https://github.com/Nadrieril/tracing-tree"] diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 1025b4b201e2..7b4a970a6753 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -13,7 +13,7 @@ publish = false [dependencies] kani_metadata = { path = "../kani_metadata" } -cargo_metadata = "0.18.0" +cargo_metadata = "0.19" anyhow = "1" console = "0.15.1" once_cell = "1.19.0" @@ -35,7 +35,7 @@ tempfile = "3" tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]} tracing-subscriber = {version = "0.3.8", features = ["env-filter", "json", "fmt"]} rand = "0.8" -which = "6" +which = "7" time = {version = "0.3.36", features = ["formatting"]} tokio = { version = "1.40.0", features = ["io-util", "process", "rt", "time"] } diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index cec8226e5f8e..f26a8e0aa4e8 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -9,7 +9,8 @@ use crate::util; use anyhow::{Context, Result, bail}; use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel}; use cargo_metadata::{ - Artifact as RustcArtifact, Message, Metadata, MetadataCommand, Package, PackageId, Target, + Artifact as RustcArtifact, CrateType, Message, Metadata, MetadataCommand, Package, PackageId, + Target, TargetKind, }; use kani_metadata::{ArtifactType, CompilerArtifactStub}; use std::collections::HashMap; @@ -22,16 +23,6 @@ use std::path::{Path, PathBuf}; use std::process::Command; use tracing::{debug, trace}; -//---- Crate types identifier used by cargo. -const CRATE_TYPE_BIN: &str = "bin"; -const CRATE_TYPE_CDYLIB: &str = "cdylib"; -const CRATE_TYPE_DYLIB: &str = "dylib"; -const CRATE_TYPE_LIB: &str = "lib"; -const CRATE_TYPE_PROC_MACRO: &str = "proc-macro"; -const CRATE_TYPE_RLIB: &str = "rlib"; -const CRATE_TYPE_STATICLIB: &str = "staticlib"; -const CRATE_TYPE_TEST: &str = "test"; - /// The outputs of kani-compiler being invoked via cargo on a project. pub struct CargoOutputs { /// The directory where compiler outputs should be directed. @@ -123,8 +114,8 @@ crate-type = ["lib"] .run_build(cmd)? .into_iter() .filter_map(|artifact| { - if artifact.target.crate_types.contains(&CRATE_TYPE_LIB.to_string()) - || artifact.target.crate_types.contains(&CRATE_TYPE_RLIB.to_string()) + if artifact.target.crate_types.contains(&CrateType::Lib) + || artifact.target.crate_types.contains(&CrateType::RLib) { map_kani_artifact(artifact) } else { @@ -576,26 +567,29 @@ fn package_targets(args: &VerificationArgs, package: &Package) -> Vec { + match kind { + TargetKind::Bin => { if args.target.include_bin(&target.name) { // Binary targets. verification_targets.push(VerificationTarget::Bin(target.clone())); } } - CRATE_TYPE_LIB | CRATE_TYPE_RLIB | CRATE_TYPE_CDYLIB | CRATE_TYPE_DYLIB - | CRATE_TYPE_STATICLIB => { + TargetKind::Lib + | TargetKind::RLib + | TargetKind::CDyLib + | TargetKind::DyLib + | TargetKind::StaticLib => { if args.target.include_lib() { supported_lib = true; } } - CRATE_TYPE_PROC_MACRO => { + TargetKind::ProcMacro => { if args.target.include_lib() { unsupported_lib = true; ignored_unsupported.push(target.name.as_str()); } } - CRATE_TYPE_TEST => { + TargetKind::Test => { // Test target. if args.target.include_tests() { if args.tests { diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index 25e022e70d3f..ee8d842db0eb 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -11,6 +11,6 @@ publish = false [dependencies] anyhow = "1" -cargo_metadata = "0.18.0" +cargo_metadata = "0.19" clap = { version = "4.4.11", features=["derive"] } -which = "6" +which = "7" diff --git a/tools/build-kani/src/sysroot.rs b/tools/build-kani/src/sysroot.rs index 29d481e4b9dd..139dce794f13 100644 --- a/tools/build-kani/src/sysroot.rs +++ b/tools/build-kani/src/sysroot.rs @@ -13,7 +13,7 @@ use crate::{AutoRun, cp}; use anyhow::{Result, bail, format_err}; -use cargo_metadata::{Artifact, Message}; +use cargo_metadata::{Artifact, Message, TargetKind}; use std::ffi::OsStr; use std::fs; use std::io::BufReader; @@ -194,9 +194,13 @@ fn copy_artifacts(artifacts: &[Artifact], sysroot_lib: &Path, copy_std: bool) -> /// Check if an artifact is a rust library that can be used by rustc on further crates compilations. /// This inspects the kind of targets that this artifact originates from. fn is_rust_lib(artifact: &Artifact) -> bool { - artifact.target.kind.iter().any(|kind| match kind.as_str() { - "lib" | "rlib" | "proc-macro" => true, - "bin" | "dylib" | "cdylib" | "staticlib" | "custom-build" => false, + artifact.target.kind.iter().any(|kind| match kind { + TargetKind::Lib | TargetKind::RLib | TargetKind::ProcMacro => true, + TargetKind::Bin + | TargetKind::DyLib + | TargetKind::CDyLib + | TargetKind::StaticLib + | TargetKind::CustomBuild => false, _ => unreachable!("Unknown crate type {kind}"), }) } diff --git a/tools/kani-cov/Cargo.toml b/tools/kani-cov/Cargo.toml index 4b9f14cc3ca9..a2764791dcf1 100644 --- a/tools/kani-cov/Cargo.toml +++ b/tools/kani-cov/Cargo.toml @@ -17,5 +17,5 @@ console = "0.15.8" serde = "1.0.197" serde_derive = "1.0.197" serde_json = "1.0.115" -tree-sitter = "0.23.0" -tree-sitter-rust = "0.21.2" +tree-sitter = "0.24" +tree-sitter-rust = "0.23" diff --git a/tools/kani-cov/src/coverage.rs b/tools/kani-cov/src/coverage.rs index 96a3dfdb7353..0898010ea2d0 100644 --- a/tools/kani-cov/src/coverage.rs +++ b/tools/kani-cov/src/coverage.rs @@ -154,7 +154,7 @@ pub struct FunctionInfo { pub fn function_info_from_file(filepath: &PathBuf) -> Vec { let source_code = fs::read_to_string(filepath).expect("could not read source file"); let mut parser = Parser::new(); - parser.set_language(&tree_sitter_rust::language()).expect("Error loading Rust grammar"); + parser.set_language(&tree_sitter_rust::LANGUAGE.into()).expect("Error loading Rust grammar"); let tree = parser.parse(&source_code, None).expect("Failed to parse file"); From c1c5b46ca7fa637603b51e277793ff20b3a57c94 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Sat, 14 Dec 2024 07:49:12 -0500 Subject: [PATCH 02/24] Automatic toolchain upgrade to nightly-2024-12-14 (#3780) Update Rust toolchain from nightly-2024-12-13 to nightly-2024-12-14 without any other source changes. Co-authored-by: celinval <35149715+celinval@users.noreply.github.com> --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index f7fb65c37ec5..c4f751d10526 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-12-13" +channel = "nightly-2024-12-14" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 86f53662d785f1ac3a6488a99323aba57aa6362c Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 16 Dec 2024 11:36:45 +0100 Subject: [PATCH 03/24] Automatic cargo update to 2024-12-16 (#3782) Dependency upgrade resulting from `cargo update`. Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com> --- Cargo.lock | 118 ++++++++++++----------------------------------------- 1 file changed, 26 insertions(+), 92 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 0c2954adf118..290aeae08dba 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -140,7 +140,7 @@ dependencies = [ "miniz_oxide", "object", "rustc-demangle", - "windows-targets 0.52.6", + "windows-targets", ] [[package]] @@ -220,7 +220,7 @@ dependencies = [ "semver", "serde", "serde_json", - "thiserror 2.0.6", + "thiserror 2.0.7", ] [[package]] @@ -324,12 +324,12 @@ checksum = "5b63caa9aa9397e2d9480a9b13673856c78d8ac123288526c37d7839f2a86990" [[package]] name = "colored" -version = "2.1.0" +version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cbf2150cce219b664a8a70df7a1f933836724b503f8a413af9365b4dcc4d90b8" +checksum = "117725a109d387c937a1533ce01b450cbde6b88abceea8473c4d7a85853cda3c" dependencies = [ "lazy_static", - "windows-sys 0.48.0", + "windows-sys 0.59.0", ] [[package]] @@ -415,9 +415,9 @@ dependencies = [ [[package]] name = "crossbeam-deque" -version = "0.8.5" +version = "0.8.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "613f8cc01fe9cf1a3eb3d7f488fd2fa8388403e97039e2f73692932e291a770d" +checksum = "9dd111b7b7f7d55b72c0a6ae361660ee5853c9af73f70c3c2ef6858b950e2e51" dependencies = [ "crossbeam-epoch", "crossbeam-utils", @@ -434,9 +434,9 @@ dependencies = [ [[package]] name = "crossbeam-utils" -version = "0.8.20" +version = "0.8.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "22ec99545bb0ed0ea7bb9b8e1e9122ea386ff8a48c0922e43f36d45ab09e0e80" +checksum = "d0a5c400df2834b80a4c3327b3aad3a4c4cd4de0629063962b03235697506a28" [[package]] name = "crossterm" @@ -938,9 +938,9 @@ checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" [[package]] name = "memuse" -version = "0.2.1" +version = "0.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2145869435ace5ea6ea3d35f59be559317ec9a0d04e1812d5f185a87b6d36f1a" +checksum = "3d97bbf43eb4f088f8ca469930cde17fa036207c9a5e02ccc5107c4e8b17c964" [[package]] name = "minimal-lexical" @@ -1149,7 +1149,7 @@ dependencies = [ "libc", "redox_syscall", "smallvec", - "windows-targets 0.52.6", + "windows-targets", ] [[package]] @@ -1703,11 +1703,11 @@ dependencies = [ [[package]] name = "thiserror" -version = "2.0.6" +version = "2.0.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8fec2a1820ebd077e2b90c4df007bebf344cd394098a13c563957d0afc83ea47" +checksum = "93605438cbd668185516ab499d589afb7ee1859ea3d5fc8f6b0755e1c7443767" dependencies = [ - "thiserror-impl 2.0.6", + "thiserror-impl 2.0.7", ] [[package]] @@ -1723,9 +1723,9 @@ dependencies = [ [[package]] name = "thiserror-impl" -version = "2.0.6" +version = "2.0.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d65750cab40f4ff1929fb1ba509e9914eb756131cef4210da8d5d700d26f6312" +checksum = "e1d8749b4531af2117677a5fcd12b1348a3fe2b81e36e61ffeac5c4aa3273e36" dependencies = [ "proc-macro2", "quote", @@ -2095,22 +2095,13 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" -[[package]] -name = "windows-sys" -version = "0.48.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" -dependencies = [ - "windows-targets 0.48.5", -] - [[package]] name = "windows-sys" version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" dependencies = [ - "windows-targets 0.52.6", + "windows-targets", ] [[package]] @@ -2119,22 +2110,7 @@ version = "0.59.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" dependencies = [ - "windows-targets 0.52.6", -] - -[[package]] -name = "windows-targets" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c" -dependencies = [ - "windows_aarch64_gnullvm 0.48.5", - "windows_aarch64_msvc 0.48.5", - "windows_i686_gnu 0.48.5", - "windows_i686_msvc 0.48.5", - "windows_x86_64_gnu 0.48.5", - "windows_x86_64_gnullvm 0.48.5", - "windows_x86_64_msvc 0.48.5", + "windows-targets", ] [[package]] @@ -2143,46 +2119,28 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" dependencies = [ - "windows_aarch64_gnullvm 0.52.6", - "windows_aarch64_msvc 0.52.6", - "windows_i686_gnu 0.52.6", + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", "windows_i686_gnullvm", - "windows_i686_msvc 0.52.6", - "windows_x86_64_gnu 0.52.6", - "windows_x86_64_gnullvm 0.52.6", - "windows_x86_64_msvc 0.52.6", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", ] -[[package]] -name = "windows_aarch64_gnullvm" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" - [[package]] name = "windows_aarch64_gnullvm" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" -[[package]] -name = "windows_aarch64_msvc" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" - [[package]] name = "windows_aarch64_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" -[[package]] -name = "windows_i686_gnu" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" - [[package]] name = "windows_i686_gnu" version = "0.52.6" @@ -2195,48 +2153,24 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" -[[package]] -name = "windows_i686_msvc" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" - [[package]] name = "windows_i686_msvc" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" -[[package]] -name = "windows_x86_64_gnu" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" - [[package]] name = "windows_x86_64_gnu" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" -[[package]] -name = "windows_x86_64_gnullvm" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" - [[package]] name = "windows_x86_64_gnullvm" version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" -[[package]] -name = "windows_x86_64_msvc" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" - [[package]] name = "windows_x86_64_msvc" version = "0.52.6" From 68f1adb4a745d44127564bd9b8af796418eb06f8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 16 Dec 2024 17:04:34 +0100 Subject: [PATCH 04/24] Bump Kani version to 0.57.0 (#3777) Updated version in all `Cargo.toml` files (via `find . -name Cargo.toml -exec sed -i 's/version = "0.56.0"/version = "0.57.0"/' {} \;`) and ran `cargo build-dev` to have `Cargo.lock` files updated. GitHub generated release notes: ## What's Changed * Remove the overflow checks for wrapping_offset by @zhassan-aws in https://github.com/model-checking/kani/pull/3589 * `kani-cov`: A coverage tool for Kani by @adpaco-aws in https://github.com/model-checking/kani/pull/3121 * Automatic toolchain upgrade to nightly-2024-10-04 by @github-actions in https://github.com/model-checking/kani/pull/3570 * Automatic toolchain upgrade to nightly-2024-10-05 by @github-actions in https://github.com/model-checking/kani/pull/3591 * Automatic toolchain upgrade to nightly-2024-10-06 by @github-actions in https://github.com/model-checking/kani/pull/3592 * Exclude Charon from workspace by @zhassan-aws in https://github.com/model-checking/kani/pull/3580 * Support fully-qualified --package arguments by @celinval in https://github.com/model-checking/kani/pull/3593 * Automatic toolchain upgrade to nightly-2024-10-07 by @github-actions in https://github.com/model-checking/kani/pull/3595 * Automatic toolchain upgrade to nightly-2024-10-08 by @github-actions in https://github.com/model-checking/kani/pull/3597 * Automatic cargo update to 2024-10-14 by @github-actions in https://github.com/model-checking/kani/pull/3598 * Bump tests/perf/s2n-quic from `17171ec` to `7752afb` by @dependabot in https://github.com/model-checking/kani/pull/3601 * Automatic toolchain upgrade to nightly-2024-10-09 by @github-actions in https://github.com/model-checking/kani/pull/3600 * Automatic toolchain upgrade to nightly-2024-10-10 by @github-actions in https://github.com/model-checking/kani/pull/3602 * Automatic toolchain upgrade to nightly-2024-10-11 by @github-actions in https://github.com/model-checking/kani/pull/3603 * Loop Contracts Annotation for While-Loop by @qinheping in https://github.com/model-checking/kani/pull/3151 * Automatic toolchain upgrade to nightly-2024-10-12 by @github-actions in https://github.com/model-checking/kani/pull/3604 * Update toolchain to 2024-10-15 by @zhassan-aws in https://github.com/model-checking/kani/pull/3605 * Automatic toolchain upgrade to nightly-2024-10-16 by @github-actions in https://github.com/model-checking/kani/pull/3607 * Implement proper function pointer handling for validity checks by @celinval in https://github.com/model-checking/kani/pull/3606 * Update toolchain to 2024-10-17 by @zhassan-aws in https://github.com/model-checking/kani/pull/3610 * Add fn that checks pointers point to same allocation by @celinval in https://github.com/model-checking/kani/pull/3583 * Automatic toolchain upgrade to nightly-2024-10-18 by @github-actions in https://github.com/model-checking/kani/pull/3613 * [aeneas] Preserve variable names by @zhassan-aws in https://github.com/model-checking/kani/pull/3560 * [Breaking change] Make `kani::check` private by @celinval in https://github.com/model-checking/kani/pull/3614 * Emit an error when proof_for_contract function is not found by @zhassan-aws in https://github.com/model-checking/kani/pull/3609 * Automatic toolchain upgrade to nightly-2024-10-19 by @github-actions in https://github.com/model-checking/kani/pull/3617 * Automatic toolchain upgrade to nightly-2024-10-20 by @github-actions in https://github.com/model-checking/kani/pull/3619 * Update test small_slice_eq by @qinheping in https://github.com/model-checking/kani/pull/3618 * Automatic toolchain upgrade to nightly-2024-10-21 by @github-actions in https://github.com/model-checking/kani/pull/3621 * Automatic cargo update to 2024-10-21 by @github-actions in https://github.com/model-checking/kani/pull/3622 * Bump tests/perf/s2n-quic from `7752afb` to `cd0314b` by @dependabot in https://github.com/model-checking/kani/pull/3625 * Update coverage flag in docs by @zhassan-aws in https://github.com/model-checking/kani/pull/3626 * Automatic toolchain upgrade to nightly-2024-10-22 by @github-actions in https://github.com/model-checking/kani/pull/3628 * Automatic toolchain upgrade to nightly-2024-10-23 by @github-actions in https://github.com/model-checking/kani/pull/3635 * Remove dead Option layer from run_piped by @zhassan-aws in https://github.com/model-checking/kani/pull/3634 * Add `free(0)` to codegen of loop contracts by @qinheping in https://github.com/model-checking/kani/pull/3637 * [Lean] Rename user-facing options from Aeneas to Lean by @zhassan-aws in https://github.com/model-checking/kani/pull/3630 * Fix ICE due to mishandling of Aggregate rvalue for raw pointers to trait objects by @carolynzech in https://github.com/model-checking/kani/pull/3636 * Automatic toolchain upgrade to nightly-2024-10-24 by @github-actions in https://github.com/model-checking/kani/pull/3639 * Add regular & fixme tests for function contracts by @celinval in https://github.com/model-checking/kani/pull/3371 * Call `goto-instrument` with `DFCC` only once by @qinheping in https://github.com/model-checking/kani/pull/3642 * Build and include `kani-cov` in the bundle by @adpaco-aws in https://github.com/model-checking/kani/pull/3641 * Fix loop contracts transformation when loops in branching by @qinheping in https://github.com/model-checking/kani/pull/3640 * Update toolchain to 10/25 by @carolynzech in https://github.com/model-checking/kani/pull/3648 * Automatic toolchain upgrade to nightly-2024-10-26 by @github-actions in https://github.com/model-checking/kani/pull/3651 * Automatic toolchain upgrade to nightly-2024-10-27 by @github-actions in https://github.com/model-checking/kani/pull/3652 * Bump tests/perf/s2n-quic from `cd0314b` to `ed9db08` by @dependabot in https://github.com/model-checking/kani/pull/3655 * Automatic cargo update to 2024-10-28 by @github-actions in https://github.com/model-checking/kani/pull/3654 * Automatic toolchain upgrade to nightly-2024-10-28 by @github-actions in https://github.com/model-checking/kani/pull/3653 * Reduce the number of object bits for refcell test by @zhassan-aws in https://github.com/model-checking/kani/pull/3656 * Move any_slice_from_array to kani_core by @qinheping in https://github.com/model-checking/kani/pull/3646 * Upgrade toolchain to 2024-10-29 by @zhassan-aws in https://github.com/model-checking/kani/pull/3658 * Add a timeout option by @zhassan-aws in https://github.com/model-checking/kani/pull/3649 * Upgrade toolchain to 2024-10-30 by @tautschnig in https://github.com/model-checking/kani/pull/3661 * Upgrade Rust toolchain to 2024-10-31 by @zhassan-aws in https://github.com/model-checking/kani/pull/3668 * Upgrade toolchain to 2024-11-01 by @tautschnig in https://github.com/model-checking/kani/pull/3671 * Automatic toolchain upgrade to nightly-2024-11-02 by @github-actions in https://github.com/model-checking/kani/pull/3673 * Implement `Arbitrary` for `Range*` by @c410-f3r in https://github.com/model-checking/kani/pull/3666 * Automatic toolchain upgrade to nightly-2024-11-03 by @github-actions in https://github.com/model-checking/kani/pull/3674 * codegen: Ask the layout if it is uninhabited, not its impl detail by @workingjubilee in https://github.com/model-checking/kani/pull/3675 * Automatic cargo update to 2024-11-04 by @github-actions in https://github.com/model-checking/kani/pull/3677 * Bump tests/perf/s2n-quic from `192de7d` to `65d55a4` by @dependabot in https://github.com/model-checking/kani/pull/3678 * Update dependencies following Audit workflow failure. by @remi-delmas-3000 in https://github.com/model-checking/kani/pull/3680 * Harness output individual files by @Alexander-Aghili in https://github.com/model-checking/kani/pull/3360 * Update Charon submodule to 2024-11-04 by @zhassan-aws in https://github.com/model-checking/kani/pull/3686 * Add support for float_to_int_unchecked by @zhassan-aws in https://github.com/model-checking/kani/pull/3660 * Change `same_allocation` to accept wide pointers by @celinval in https://github.com/model-checking/kani/pull/3684 * Automatic upgrade of CBMC from 6.3.1 to 6.4.0 by @github-actions in https://github.com/model-checking/kani/pull/3689 * Derive `Arbitrary` for enums with a single variant by @AlgebraicWolf in https://github.com/model-checking/kani/pull/3692 * Update cbmc-viewer to 3.10 by @remi-delmas-3000 in https://github.com/model-checking/kani/pull/3683 * Apply loop contracts only if there exists some usage by @qinheping in https://github.com/model-checking/kani/pull/3694 * Remove symtab json support by @celinval in https://github.com/model-checking/kani/pull/3695 * Remove CBMC viewer and visualize option by @zhassan-aws in https://github.com/model-checking/kani/pull/3699 * Ignore derivative in Cargo deny by @qinheping in https://github.com/model-checking/kani/pull/3708 * Upgrade Rust toolchain to 2024-11-08 by @zhassan-aws in https://github.com/model-checking/kani/pull/3703 * Automatic cargo update to 2024-11-11 by @github-actions in https://github.com/model-checking/kani/pull/3704 * Update verify-std-check workflow to enable loop contracts by @qinheping in https://github.com/model-checking/kani/pull/3705 * Automatic toolchain upgrade to nightly-2024-11-09 by @github-actions in https://github.com/model-checking/kani/pull/3709 * Bump tests/perf/s2n-quic from `65d55a4` to `cb41b35` by @dependabot in https://github.com/model-checking/kani/pull/3706 * Add support for f16 and f128 in float_to_int_unchecked intrinsic by @zhassan-aws in https://github.com/model-checking/kani/pull/3701 * Upgrade toolchain to nightly-2024-11-11 by @qinheping in https://github.com/model-checking/kani/pull/3710 * Automatic toolchain upgrade to nightly-2024-11-12 by @github-actions in https://github.com/model-checking/kani/pull/3713 * Update charon submodule by @zhassan-aws in https://github.com/model-checking/kani/pull/3716 * Revert "Ignore derivative in Cargo deny" by @qinheping in https://github.com/model-checking/kani/pull/3712 * Upgrade toolchain to nightly-2024-11-13 by @qinheping in https://github.com/model-checking/kani/pull/3715 * Automatic toolchain upgrade to nightly-2024-11-14 by @github-actions in https://github.com/model-checking/kani/pull/3719 * Automatic toolchain upgrade to nightly-2024-11-15 by @github-actions in https://github.com/model-checking/kani/pull/3720 * Fix codegen for rvalue aggregate raw pointer to an adt with slice tail by @carolynzech in https://github.com/model-checking/kani/pull/3644 * Improve Kani handling of function markers by @celinval in https://github.com/model-checking/kani/pull/3718 * Automatic toolchain upgrade to nightly-2024-11-16 by @github-actions in https://github.com/model-checking/kani/pull/3722 * Automatic toolchain upgrade to nightly-2024-11-17 by @github-actions in https://github.com/model-checking/kani/pull/3724 * Automatic cargo update to 2024-11-18 by @github-actions in https://github.com/model-checking/kani/pull/3723 * Bump tests/perf/s2n-quic from `cb41b35` to `4c3ba69` by @dependabot in https://github.com/model-checking/kani/pull/3725 * Automatic toolchain upgrade to nightly-2024-11-18 by @github-actions in https://github.com/model-checking/kani/pull/3727 * Enable contracts for const generic functions by @qinheping in https://github.com/model-checking/kani/pull/3726 * List Subcommand Improvements by @carolynzech in https://github.com/model-checking/kani/pull/3729 * Automatic toolchain upgrade to nightly-2024-11-19 by @github-actions in https://github.com/model-checking/kani/pull/3730 * add support for enum, struct, tuple in llbc backend by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/3721 * Fix issues with how we compute DST size by @celinval in https://github.com/model-checking/kani/pull/3687 * Bump tests/perf/s2n-quic from `4c3ba69` to `c84ba19` by @dependabot in https://github.com/model-checking/kani/pull/3736 * Fix size and alignment computation for intrinsics by @celinval in https://github.com/model-checking/kani/pull/3734 * Automatic cargo update to 2024-11-25 by @github-actions in https://github.com/model-checking/kani/pull/3735 * Cleanup a few internal compiler deps by @celinval in https://github.com/model-checking/kani/pull/3739 * Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in https://github.com/model-checking/kani/pull/3742 * Dropping support for Ubuntu 18.04 / AL2. by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/3744 * Update toolchain to nightly-2024-11-26 by @celinval in https://github.com/model-checking/kani/pull/3740 * Automatic upgrade of CBMC from 6.4.0 to 6.4.1 by @github-actions in https://github.com/model-checking/kani/pull/3748 * Automatic cargo update to 2024-12-02 by @github-actions in https://github.com/model-checking/kani/pull/3749 * Update download-artifact, upload-artifact and checkout to v4 by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/3745 * Bump tests/perf/s2n-quic from `c84ba19` to `96d2e22` by @dependabot in https://github.com/model-checking/kani/pull/3750 * Upgrade toolchain to 2024-11-27 by @tautschnig in https://github.com/model-checking/kani/pull/3751 * Upgrade toolchain to 2024-11-28 by @tautschnig in https://github.com/model-checking/kani/pull/3753 * Setup/CI: cleanup Ubuntu 18.04 and cbmc-viewer left-overs and enable 24.04 by @tautschnig in https://github.com/model-checking/kani/pull/3758 * Automatic cargo update to 2024-12-09 by @github-actions in https://github.com/model-checking/kani/pull/3766 * Bump tests/perf/s2n-quic from `96d2e22` to `e4a2365` by @dependabot in https://github.com/model-checking/kani/pull/3767 * Upgrade toolchain to 2024-12-09 by @carolynzech in https://github.com/model-checking/kani/pull/3768 * Add out of bounds check for `offset` intrinsics by @celinval in https://github.com/model-checking/kani/pull/3755 * Upgrade toolchain to 2024-12-12 by @carolynzech in https://github.com/model-checking/kani/pull/3774 * Automatic toolchain upgrade to nightly-2024-12-13 by @github-actions in https://github.com/model-checking/kani/pull/3775 ## New Contributors * @c410-f3r made their first contribution in https://github.com/model-checking/kani/pull/3666 * @workingjubilee made their first contribution in https://github.com/model-checking/kani/pull/3675 * @Alexander-Aghili made their first contribution in https://github.com/model-checking/kani/pull/3360 * @AlgebraicWolf made their first contribution in https://github.com/model-checking/kani/pull/3692 * @thanhnguyen-aws made their first contribution in https://github.com/model-checking/kani/pull/3721 **Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.56.0...kani-0.57.0 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: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Carolyn Zech --- CHANGELOG.md | 46 ++++++++++++++++++++++++++++++++++ Cargo.lock | 20 +++++++-------- Cargo.toml | 2 +- cprover_bindings/Cargo.toml | 2 +- kani-compiler/Cargo.toml | 2 +- kani-driver/Cargo.toml | 2 +- kani_metadata/Cargo.toml | 2 +- library/kani/Cargo.toml | 2 +- library/kani_core/Cargo.toml | 2 +- library/kani_macros/Cargo.toml | 2 +- library/std/Cargo.toml | 2 +- tools/build-kani/Cargo.toml | 2 +- 12 files changed, 66 insertions(+), 20 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3835d15177dd..883564672c86 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,52 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.) This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards. +## [0.57.0] + +### Major Changes +* `kani-cov`: A coverage tool for Kani by @adpaco-aws in https://github.com/model-checking/kani/pull/3121 +* Add a timeout option by @zhassan-aws in https://github.com/model-checking/kani/pull/3649 +* Loop Contracts Annotation for While-Loop by @qinheping in https://github.com/model-checking/kani/pull/3151 +* Harness output individual files by @Alexander-Aghili in https://github.com/model-checking/kani/pull/3360 +* Enable support for Ubuntu 24.04 by @tautschnig in https://github.com/model-checking/kani/pull/3758 + +### Breaking Changes +* Make `kani::check` private by @celinval in https://github.com/model-checking/kani/pull/3614 +* Remove symtab json support by @celinval in https://github.com/model-checking/kani/pull/3695 +* Remove CBMC viewer and visualize option by @zhassan-aws in https://github.com/model-checking/kani/pull/3699 +* Dropping support for Ubuntu 18.04 / AL2. by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/3744 + +### What's Changed +* Remove the overflow checks for wrapping_offset by @zhassan-aws in https://github.com/model-checking/kani/pull/3589 +* Support fully-qualified --package arguments by @celinval in https://github.com/model-checking/kani/pull/3593 +* Implement proper function pointer handling for validity checks by @celinval in https://github.com/model-checking/kani/pull/3606 +* Add fn that checks pointers point to same allocation by @celinval in https://github.com/model-checking/kani/pull/3583 +* [Lean back-end] Preserve variable names by @zhassan-aws in https://github.com/model-checking/kani/pull/3560 +* Emit an error when proof_for_contract function is not found by @zhassan-aws in https://github.com/model-checking/kani/pull/3609 +* [Lean back-end] Rename user-facing options from Aeneas to Lean by @zhassan-aws in https://github.com/model-checking/kani/pull/3630 +* Fix ICE due to mishandling of Aggregate rvalue for raw pointers to trait objects by @carolynzech in https://github.com/model-checking/kani/pull/3636 +* Fix loop contracts transformation when loops in branching by @qinheping in https://github.com/model-checking/kani/pull/3640 +* Move any_slice_from_array to kani_core by @qinheping in https://github.com/model-checking/kani/pull/3646 +* Implement `Arbitrary` for `Range*` by @c410-f3r in https://github.com/model-checking/kani/pull/3666 +* Add support for float_to_int_unchecked by @zhassan-aws in https://github.com/model-checking/kani/pull/3660 +* Change `same_allocation` to accept wide pointers by @celinval in https://github.com/model-checking/kani/pull/3684 +* Derive `Arbitrary` for enums with a single variant by @AlgebraicWolf in https://github.com/model-checking/kani/pull/3692 +* Apply loop contracts only if there exists some usage by @qinheping in https://github.com/model-checking/kani/pull/3694 +* Add support for f16 and f128 in float_to_int_unchecked intrinsic by @zhassan-aws in https://github.com/model-checking/kani/pull/3701 +* Fix codegen for rvalue aggregate raw pointer to an adt with slice tail by @carolynzech in https://github.com/model-checking/kani/pull/3644 +* Improve Kani handling of function markers by @celinval in https://github.com/model-checking/kani/pull/3718 +* Enable contracts for const generic functions by @qinheping in https://github.com/model-checking/kani/pull/3726 +* List Subcommand Improvements by @carolynzech in https://github.com/model-checking/kani/pull/3729 +* [Lean back-end] add support for enum, struct, tuple in llbc backend by @thanhnguyen-aws in https://github.com/model-checking/kani/pull/3721 +* Fix issues with how we compute DST size by @celinval in https://github.com/model-checking/kani/pull/3687 +* Fix size and alignment computation for intrinsics by @celinval in https://github.com/model-checking/kani/pull/3734 +* Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in https://github.com/model-checking/kani/pull/3742 +* Add out of bounds check for `offset` intrinsics by @celinval in https://github.com/model-checking/kani/pull/3755 +* Automatic upgrade of CBMC from 6.3.1 to 6.4.1 +* Rust toolchain upgraded to nightly-2024-12-13 by @zhassan-aws @carolynzech @qinheping @celinval @tautschnig + +**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.56.0...kani-0.57.0 + ## [0.56.0] ### Major/Breaking Changes diff --git a/Cargo.lock b/Cargo.lock index 290aeae08dba..e6e86976fe84 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -171,7 +171,7 @@ dependencies = [ [[package]] name = "build-kani" -version = "0.56.0" +version = "0.57.0" dependencies = [ "anyhow", "cargo_metadata", @@ -400,7 +400,7 @@ dependencies = [ [[package]] name = "cprover_bindings" -version = "0.56.0" +version = "0.57.0" dependencies = [ "lazy_static", "linear-map", @@ -754,7 +754,7 @@ checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5" [[package]] name = "kani" -version = "0.56.0" +version = "0.57.0" dependencies = [ "kani_core", "kani_macros", @@ -762,7 +762,7 @@ dependencies = [ [[package]] name = "kani-compiler" -version = "0.56.0" +version = "0.57.0" dependencies = [ "charon", "clap", @@ -801,7 +801,7 @@ dependencies = [ [[package]] name = "kani-driver" -version = "0.56.0" +version = "0.57.0" dependencies = [ "anyhow", "cargo_metadata", @@ -833,7 +833,7 @@ dependencies = [ [[package]] name = "kani-verifier" -version = "0.56.0" +version = "0.57.0" dependencies = [ "anyhow", "home", @@ -842,14 +842,14 @@ dependencies = [ [[package]] name = "kani_core" -version = "0.56.0" +version = "0.57.0" dependencies = [ "kani_macros", ] [[package]] name = "kani_macros" -version = "0.56.0" +version = "0.57.0" dependencies = [ "proc-macro-error2", "proc-macro2", @@ -859,7 +859,7 @@ dependencies = [ [[package]] name = "kani_metadata" -version = "0.56.0" +version = "0.57.0" dependencies = [ "clap", "cprover_bindings", @@ -1599,7 +1599,7 @@ dependencies = [ [[package]] name = "std" -version = "0.56.0" +version = "0.57.0" dependencies = [ "kani", ] diff --git a/Cargo.toml b/Cargo.toml index 3c61638025e5..f6236785e038 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-verifier" -version = "0.56.0" +version = "0.57.0" edition = "2021" description = "A bit-precise model checker for Rust." readme = "README.md" diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index a190019d4cc2..b8f0210f9c72 100644 --- a/cprover_bindings/Cargo.toml +++ b/cprover_bindings/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "cprover_bindings" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml index 9f084da7b962..50ae4e0a58d6 100644 --- a/kani-compiler/Cargo.toml +++ b/kani-compiler/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-compiler" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml index 7b4a970a6753..123801e81a0a 100644 --- a/kani-driver/Cargo.toml +++ b/kani-driver/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani-driver" -version = "0.56.0" +version = "0.57.0" edition = "2021" description = "Build a project with Kani and run all proof harnesses" license = "MIT OR Apache-2.0" diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml index 2a0a03401c40..840990adca7a 100644 --- a/kani_metadata/Cargo.toml +++ b/kani_metadata/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_metadata" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml index 3ad1b286ebe6..a8c697e3d19f 100644 --- a/library/kani/Cargo.toml +++ b/library/kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml index df55e6278282..c214c64c0f02 100644 --- a/library/kani_core/Cargo.toml +++ b/library/kani_core/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_core" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml index a7876176adb2..13f20b96b6c7 100644 --- a/library/kani_macros/Cargo.toml +++ b/library/kani_macros/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "kani_macros" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml index e1e353704723..08c033407fb4 100644 --- a/library/std/Cargo.toml +++ b/library/std/Cargo.toml @@ -5,7 +5,7 @@ # Note: this package is intentionally named std to make sure the names of # standard library symbols are preserved name = "std" -version = "0.56.0" +version = "0.57.0" edition = "2021" license = "MIT OR Apache-2.0" publish = false diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml index ee8d842db0eb..ff5b3a406db1 100644 --- a/tools/build-kani/Cargo.toml +++ b/tools/build-kani/Cargo.toml @@ -3,7 +3,7 @@ [package] name = "build-kani" -version = "0.56.0" +version = "0.57.0" edition = "2021" description = "Builds Kani, Sysroot and release bundle." license = "MIT OR Apache-2.0" From d253bda3112cf068956aa1ec573d50a7a5a7585a Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 16 Dec 2024 18:24:48 +0000 Subject: [PATCH 05/24] Bump tests/perf/s2n-quic from `e4a2365` to `0b3f892` (#3785) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `e4a2365` to `0b3f892`.
Commits
  • 0b3f892 ci: specify specific bolero dependency rather than workspace dependency in s2...
  • 1d2aaa7 ci: specify specific bolero dependency rather than workspace dependency (#2424)
  • 5dd0c47 fix(s2n-quic-dc): make debug assertions cheaper for TCP accept manager (#2419)
  • b6ace28 fix(ci): fix the release (#2423)
  • 1b65715 ci: add neqo from required resumption test client (#2420)
  • 0006a28 ci: remove bench test from s2n-quic CI (#2418)
  • d59d63a ci: update h3spec to 0.11 (#2416)
  • 05ac54c build: do fewer optimizations in release (#2417)
  • 85f3048 ci: update wireshark to v4 (#2160)
  • 7e37e77 fix(s2n-quic-dc): use wake_forced for worker::Waker (#2415)
  • Additional commits viewable in compare view

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 e4a236578bcb..0b3f892ec7d4 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit e4a236578bcb36109d238753307c970d6c997666 +Subproject commit 0b3f892ec7d431249e41cae49fdc03869fd85b89 From e6f6d7d5c297637db1c4957c1f83fd0a74857f87 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 16 Dec 2024 15:07:29 -0500 Subject: [PATCH 06/24] Upgrade toolchain to 2024-12-15 (#3784) Culprit PRs: - https://github.com/rust-lang/rust/pull/133938, specifically https://github.com/rust-lang/rust/pull/133938/commits/1d56943f34ee3e1d28ae7677b8410af867f267da - https://github.com/rust-lang/rust/pull/134295 For coroutine closures, I opened #3783 to track feature support--adding support for this appears non-trivial, and I didn't want to block toolchain upgrades on it. Resolves #3781 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../src/codegen_cprover_gotoc/codegen/place.rs | 10 ++++++++++ .../src/codegen_cprover_gotoc/codegen/rvalue.rs | 9 +++++++++ .../src/codegen_cprover_gotoc/codegen/typ.rs | 11 +++++------ .../src/kani_middle/points_to/points_to_analysis.rs | 4 ++-- .../kani_middle/transform/check_uninit/ty_layout.rs | 1 + .../src/kani_middle/transform/check_values.rs | 2 ++ .../src/kani_middle/transform/internal_mir.rs | 6 ++++++ rust-toolchain.toml | 2 +- 8 files changed, 36 insertions(+), 9 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 3dccbea5837f..b6189c070538 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -283,6 +283,16 @@ impl GotocCtx<'_> { .member("direct_fields", &self.symbol_table) .member(field_name, &self.symbol_table)) } + TyKind::RigidTy(RigidTy::CoroutineClosure(def, args)) => { + let typ = Ty::new_coroutine_closure(def, args); + let goto_typ = self.codegen_ty_stable(typ); + Err(UnimplementedData::new( + "Coroutine closures", + "https://github.com/model-checking/kani/issues/3783", + goto_typ, + *parent_expr.location(), + )) + } TyKind::RigidTy(RigidTy::Str) | TyKind::RigidTy(RigidTy::Array(_, _)) | TyKind::RigidTy(RigidTy::Slice(_)) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 68c174ae2119..d13597794d19 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -729,6 +729,15 @@ impl GotocCtx<'_> { } } AggregateKind::Coroutine(_, _, _) => self.codegen_rvalue_coroutine(&operands, res_ty), + AggregateKind::CoroutineClosure(_, _) => { + let ty = self.codegen_ty_stable(res_ty); + self.codegen_unimplemented_expr( + "CoroutineClosure", + ty, + loc, + "https://github.com/model-checking/kani/issues/3783", + ) + } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 903baf8eaced..748eb42e7655 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -590,6 +590,9 @@ impl<'tcx> GotocCtx<'tcx> { } ty::Closure(_, subst) => self.codegen_ty_closure(ty, subst), ty::Coroutine(..) => self.codegen_ty_coroutine(ty), + ty::CoroutineClosure(..) => unimplemented!( + "Kani does not yet support coroutine closures. Please post your example at https://github.com/model-checking/kani/issues/3783" + ), ty::Never => self.ensure_struct(NEVER_TYPE_EMPTY_STRUCT_NAME, "!", |_, _| vec![]), ty::Tuple(ts) => { if ts.is_empty() { @@ -619,11 +622,7 @@ impl<'tcx> GotocCtx<'tcx> { ty::Bound(_, _) | ty::Param(_) => unreachable!("monomorphization bug"), // type checking remnants which shouldn't be reachable - ty::CoroutineWitness(_, _) - | ty::CoroutineClosure(_, _) - | ty::Infer(_) - | ty::Placeholder(_) - | ty::Error(_) => { + ty::CoroutineWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => { unreachable!("remnants of type checking") } } @@ -879,7 +878,7 @@ impl<'tcx> GotocCtx<'tcx> { /// Generates a struct for a variant of the coroutine. /// - /// The field `discriminant_field` should be `Some(idx)` when generating the variant for the direct (top-[evel) fields of the coroutine. + /// The field `discriminant_field` should be `Some(idx)` when generating the variant for the direct (top-level) fields of the coroutine. /// Then the field with the index `idx` will be treated as the discriminant and will be given a special name to work with the rest of the code. /// The field `discriminant_field` should be `None` when generating an actual variant of the coroutine because those don't contain the discriminant as a field. fn codegen_coroutine_variant_struct( diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index 369296db6ed4..345a27309b50 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -136,7 +136,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> { /// Update current dataflow state based on the information we can infer from the given /// statement. - fn apply_statement_effect( + fn apply_primary_statement_effect( &mut self, state: &mut Self::Domain, statement: &Statement<'tcx>, @@ -184,7 +184,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> { } } - fn apply_terminator_effect<'mir>( + fn apply_primary_terminator_effect<'mir>( &mut self, state: &mut Self::Domain, terminator: &'mir Terminator<'tcx>, diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs index 8a9e3ac094d5..0a1fc16dcc07 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ty_layout.rs @@ -393,6 +393,7 @@ fn data_bytes_for_ty( | RigidTy::FnPtr(_) | RigidTy::Closure(_, _) | RigidTy::Coroutine(_, _, _) + | RigidTy::CoroutineClosure(_, _) | RigidTy::CoroutineWitness(_, _) | RigidTy::Foreign(_) | RigidTy::Dynamic(_, _, _) => Err(LayoutComputationError::UnsupportedType(ty)), diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index 5d66d00cf094..2276906aae81 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/kani-compiler/src/kani_middle/transform/check_values.rs @@ -640,6 +640,7 @@ impl MirVisitor for CheckValueVisitor<'_, '_> { AggregateKind::Array(_) | AggregateKind::Closure(_, _) | AggregateKind::Coroutine(_, _, _) + | AggregateKind::CoroutineClosure(_, _) | AggregateKind::RawPtr(_, _) | AggregateKind::Tuple => {} }, @@ -981,6 +982,7 @@ pub fn ty_validity_per_offset( | RigidTy::FnPtr(_) | RigidTy::Closure(_, _) | RigidTy::Coroutine(_, _, _) + | RigidTy::CoroutineClosure(_, _) | RigidTy::CoroutineWitness(_, _) | RigidTy::Foreign(_) | RigidTy::Dynamic(_, _, _) => Err(format!("Unsupported {ty:?}")), diff --git a/kani-compiler/src/kani_middle/transform/internal_mir.rs b/kani-compiler/src/kani_middle/transform/internal_mir.rs index d29a5e688d2c..4f1095cce06e 100644 --- a/kani-compiler/src/kani_middle/transform/internal_mir.rs +++ b/kani-compiler/src/kani_middle/transform/internal_mir.rs @@ -56,6 +56,12 @@ impl RustcInternalMir for AggregateKind { internal(tcx, generic_args), ) } + AggregateKind::CoroutineClosure(coroutine_def, generic_args) => { + rustc_middle::mir::AggregateKind::CoroutineClosure( + internal(tcx, coroutine_def.0), + internal(tcx, generic_args), + ) + } AggregateKind::RawPtr(ty, mutability) => rustc_middle::mir::AggregateKind::RawPtr( internal(tcx, ty), internal(tcx, mutability), diff --git a/rust-toolchain.toml b/rust-toolchain.toml index c4f751d10526..62deebf7a7d2 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-12-14" +channel = "nightly-2024-12-15" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From 9fd39c0023bc31956fe77db6c4ece7a5cc24e5a8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 16 Dec 2024 23:04:29 +0100 Subject: [PATCH 07/24] Fix toolchain version in 0.57.0 CHANGELOG (#3786) By now, we have updated to 2024-12-14. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- CHANGELOG.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 883564672c86..2f2805277846 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -46,7 +46,7 @@ This file was introduced starting Kani 0.23.0, so it only contains changes from * Add a Kani function that checks if the range of a float is valid for conversion to int by @zhassan-aws in https://github.com/model-checking/kani/pull/3742 * Add out of bounds check for `offset` intrinsics by @celinval in https://github.com/model-checking/kani/pull/3755 * Automatic upgrade of CBMC from 6.3.1 to 6.4.1 -* Rust toolchain upgraded to nightly-2024-12-13 by @zhassan-aws @carolynzech @qinheping @celinval @tautschnig +* Rust toolchain upgraded to nightly-2024-12-15 by @zhassan-aws @carolynzech @qinheping @celinval @tautschnig **Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.56.0...kani-0.57.0 From 3f5f8e8c7ff2519d5cf9524a65e23739d209980e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 17 Dec 2024 16:23:41 +0100 Subject: [PATCH 08/24] Package Docker release step: ensure compiler is installed (#3789) The "Package Docker" job failed with "error: linker `cc` not found", see https://github.com/model-checking/kani/actions/runs/12371001460/job/34526835431. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- scripts/ci/Dockerfile.bundle-release-20-04 | 2 +- scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 | 2 +- scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt | 2 +- scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 | 2 +- scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/ci/Dockerfile.bundle-release-20-04 b/scripts/ci/Dockerfile.bundle-release-20-04 index 7a8b7f21b74b..963aa952d6df 100644 --- a/scripts/ci/Dockerfile.bundle-release-20-04 +++ b/scripts/ci/Dockerfile.bundle-release-20-04 @@ -17,7 +17,7 @@ COPY ./target/package/kani-verifier-*[^e] ./kani-verifier # directory. Rustup is purged for space. RUN apt-get update && \ - apt-get install -y curl && \ + apt-get install -y curl build-essential && \ curl -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain none && \ (cd kani-verifier/; cargo) && \ rustup default $(rustup toolchain list | awk '{ print $1 }') && \ diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 index 44084606f98d..f81af91f6f52 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04 @@ -7,7 +7,7 @@ FROM ubuntu:20.04 ENV DEBIAN_FRONTEND=noninteractive \ DEBCONF_NONINTERACTIVE_SEEN=true RUN apt-get update && \ - apt-get install -y curl && \ + apt-get install -y curl build-essential && \ curl -sSf https://sh.rustup.rs | sh -s -- -y ENV PATH="/root/.cargo/bin:${PATH}" diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt index ebba8e3a178b..35bc522b651f 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-20-04-alt @@ -9,7 +9,7 @@ ENV DEBIAN_FRONTEND=noninteractive \ DEBCONF_NONINTERACTIVE_SEEN=true \ KANI_HOME="/tmp" RUN apt-get update && \ - apt-get install -y curl && \ + apt-get install -y curl build-essential && \ curl -sSf https://sh.rustup.rs | sh -s -- -y ENV PATH="/root/.cargo/bin:${PATH}" diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 index f53c11cf7fcb..f7dd23e1233d 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-22-04 @@ -7,7 +7,7 @@ FROM ubuntu:22.04 ENV DEBIAN_FRONTEND=noninteractive \ DEBCONF_NONINTERACTIVE_SEEN=true RUN apt-get update && \ - apt-get install -y curl && \ + apt-get install -y curl build-essential && \ curl -sSf https://sh.rustup.rs | sh -s -- -y ENV PATH="/root/.cargo/bin:${PATH}" diff --git a/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 b/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 index db4e8b88640d..1b85fd2e0b58 100644 --- a/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 +++ b/scripts/ci/Dockerfile.bundle-test-ubuntu-24-04 @@ -7,7 +7,7 @@ FROM ubuntu:24.04 ENV DEBIAN_FRONTEND=noninteractive \ DEBCONF_NONINTERACTIVE_SEEN=true RUN apt-get update && \ - apt-get install -y curl && \ + apt-get install -y curl build-essential && \ curl -sSf https://sh.rustup.rs | sh -s -- -y ENV PATH="/root/.cargo/bin:${PATH}" From b7ae080b4f591990362bc68694b287ef8ced09bc Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 18 Dec 2024 18:17:58 -0500 Subject: [PATCH 09/24] Improve `--jobs` UI (#3790) Improve the documentation for the `--jobs` option, change it to use `hide_short_help` like other unstable options, and print the current thread number so that users can match the harness to its output. Example: ```rust #[kani::modifies(x)] #[kani::ensures(|_| x.iter().map(|v| *v == 0).fold(true,|a,b|a&b))] fn zero(x: &mut [u8]) { x.fill(0) } #[kani::proof_for_contract(zero)] fn harness() { let mut x = [kani::any(), kani::any(), kani::any()]; zero(&mut x); } #[kani::proof] fn harness_2() { assert!(true); } #[kani::proof] fn harness_3() { assert!(false); } ``` ``` cargo kani -j --enable-unstable --output-format=terse -Z function-contracts Kani Rust Verifier 0.57.0 (cargo plugin) warning: Found the following unsupported constructs: - caller_location (1) - foreign function (1) Verification will fail if one or more of these constructs is reachable. See https://model-checking.github.io/kani/rust-feature-support.html for more details. Finished `dev` profile [unoptimized + debuginfo] target(s) in 0.02s Thread 4: Checking harness harness_2... Thread 2: Checking harness harness_3... Thread 4: VERIFICATION RESULT: ** 0 of 1 failed VERIFICATION:- SUCCESSFUL Verification Time: 0.0137195s Thread 2: VERIFICATION RESULT: ** 1 of 1 failed Failed Checks: assertion failed: false File: "src/lib.rs", line 26, in harness_3 VERIFICATION:- FAILED Verification Time: 0.012914542s Thread 0: Checking harness harness... Thread 0: VERIFICATION RESULT: ** 0 of 217 failed VERIFICATION:- SUCCESSFUL Verification Time: 18.47224s Summary: Verification failed for - harness_3 Complete - 2 successfully verified harnesses, 1 failures, 3 total. ``` 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: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- kani-driver/src/args/mod.rs | 7 ++++-- kani-driver/src/harness_runner.rs | 37 +++++++++++++++++++++++++------ 2 files changed, 35 insertions(+), 9 deletions(-) diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 66ff247ddc82..9b2408d484e2 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -257,8 +257,11 @@ pub struct VerificationArgs { // consumes everything pub cbmc_args: Vec, - /// Number of parallel jobs, defaults to 1 - #[arg(short, long, hide = true, requires("enable_unstable"))] + /// Number of threads to spawn to verify harnesses in parallel. + /// Omit the flag entirely to run sequentially (i.e. one thread). + /// Pass -j to run with the thread pool's default number of threads. + /// Pass -j to specify N threads. + #[arg(short, long, hide_short_help = true, requires("enable_unstable"))] pub jobs: Option>, /// Enable extra pointer checks such as invalid pointers in relation operations and pointer diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs index ee14992cba78..b78e1dc9d80b 100644 --- a/kani-driver/src/harness_runner.rs +++ b/kani-driver/src/harness_runner.rs @@ -103,14 +103,23 @@ impl<'pr> HarnessRunner<'_, 'pr> { } impl KaniSession { - fn process_output(&self, result: &VerificationResult, harness: &HarnessMetadata) { + fn process_output( + &self, + result: &VerificationResult, + harness: &HarnessMetadata, + thread_index: usize, + ) { if self.should_print_output() { if self.args.output_into_files { - self.write_output_to_file(result, harness); + self.write_output_to_file(result, harness, thread_index); } let output = result.render(&self.args.output_format, harness.attributes.should_panic); - println!("{}", output); + if rayon::current_num_threads() > 1 { + println!("Thread {thread_index}: {output}"); + } else { + println!("{output}"); + } } } @@ -118,7 +127,12 @@ impl KaniSession { !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old } - fn write_output_to_file(&self, result: &VerificationResult, harness: &HarnessMetadata) { + fn write_output_to_file( + &self, + result: &VerificationResult, + harness: &HarnessMetadata, + thread_index: usize, + ) { let target_dir = self.result_output_dir().unwrap(); let file_name = target_dir.join(harness.pretty_name.clone()); let path = Path::new(&file_name); @@ -126,7 +140,11 @@ impl KaniSession { std::fs::create_dir_all(prefix).unwrap(); let mut file = File::create(&file_name).unwrap(); - let file_output = result.render(&OutputFormat::Regular, harness.attributes.should_panic); + let mut file_output = + result.render(&OutputFormat::Regular, harness.attributes.should_panic); + if rayon::current_num_threads() > 1 { + file_output = format!("Thread {thread_index}:\n{file_output}"); + } if let Err(e) = writeln!(file, "{}", file_output) { eprintln!( @@ -148,13 +166,18 @@ impl KaniSession { binary: &Path, harness: &HarnessMetadata, ) -> Result { + let thread_index = rayon::current_thread_index().unwrap_or_default(); if !self.args.common_args.quiet { - println!("Checking harness {}...", harness.pretty_name); + if rayon::current_num_threads() > 1 { + println!("Thread {thread_index}: Checking harness {}...", harness.pretty_name); + } else { + println!("Checking harness {}...", harness.pretty_name); + } } let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?; - self.process_output(&result, harness); + self.process_output(&result, harness, thread_index); self.gen_and_add_concrete_playback(harness, &mut result)?; Ok(result) } From 7a08474d65cd6b6da8097ed23256a3a37757e20e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9mi=20Delmas?= Date: Fri, 20 Dec 2024 04:24:12 -0500 Subject: [PATCH 10/24] Update kissat to v4.0.1 (#3791) New in 4.0.1 is gate extraction and clausal congruence closure. It could help improve performance in equivalence checking problems, by detecting and merging structurally equivalent literals and clauses within a SAT formula. 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: Remi Delmas --- docs/src/build-from-source.md | 2 +- kani-dependencies | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/src/build-from-source.md b/docs/src/build-from-source.md index e0982bf2899b..bfe5d9057d8d 100644 --- a/docs/src/build-from-source.md +++ b/docs/src/build-from-source.md @@ -12,7 +12,7 @@ In general, the following dependencies are required to build Kani from source. 1. Cargo installed via [rustup](https://rustup.rs/) 2. [CBMC](https://github.com/diffblue/cbmc) (latest release) -3. [Kissat](https://github.com/arminbiere/kissat) (Release 3.1.1) +3. [Kissat](https://github.com/arminbiere/kissat) (Release 4.0.1) Kani has been tested in [Ubuntu](#install-dependencies-on-ubuntu) and [macOS](##install-dependencies-on-macos) platforms. diff --git a/kani-dependencies b/kani-dependencies index 004e9a0a9811..ed8e32faca90 100644 --- a/kani-dependencies +++ b/kani-dependencies @@ -2,4 +2,4 @@ CBMC_MAJOR="6" CBMC_MINOR="4" CBMC_VERSION="6.4.1" -KISSAT_VERSION="3.1.1" +KISSAT_VERSION="4.0.1" From 4251ae843588b934e162692759de56abb4a4542e Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 23 Dec 2024 06:20:27 +0000 Subject: [PATCH 11/24] Automatic cargo update to 2024-12-23 (#3792) Dependency upgrade resulting from `cargo update`. Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com> --- Cargo.lock | 130 ++++++++++++++++++++++++++++------------------------- 1 file changed, 68 insertions(+), 62 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index e6e86976fe84..de3f2603cf30 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -90,9 +90,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.94" +version = "1.0.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c1fd03a028ef38ba2276dce7e33fcd6369c158a1bca17946c4b1b701891c1ff7" +checksum = "34ac096ce696dc2fcabef30516bb13c0a68a11d30131d3df6f04711467681b04" [[package]] name = "arrayvec" @@ -176,7 +176,7 @@ dependencies = [ "anyhow", "cargo_metadata", "clap", - "which 7.0.0", + "which 7.0.1", ] [[package]] @@ -220,14 +220,14 @@ dependencies = [ "semver", "serde", "serde_json", - "thiserror 2.0.7", + "thiserror 2.0.9", ] [[package]] name = "cc" -version = "1.2.4" +version = "1.2.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9157bbaa6b165880c27a4293a474c91cdcf265cc68cc829bf10be0964a391caf" +checksum = "c31a0499c1dc64f458ad13872de75c0eb7e3fdb0e67964610c914b034fc5956e" dependencies = [ "shlex", ] @@ -307,7 +307,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -372,15 +372,15 @@ dependencies = [ [[package]] name = "console" -version = "0.15.8" +version = "0.15.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e1f83fc076bd6dd27517eacdf25fef6c4dfe5f1d7448bafaaf3a26f13b5e4eb" +checksum = "ea3c6ecd8059b57859df5c69830340ed3c41d30e3da0c1cbed90a96ac853041b" dependencies = [ "encode_unicode", - "lazy_static", "libc", - "unicode-width 0.1.14", - "windows-sys 0.52.0", + "once_cell", + "unicode-width 0.2.0", + "windows-sys 0.59.0", ] [[package]] @@ -532,25 +532,31 @@ checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0" [[package]] name = "encode_unicode" -version = "0.3.6" +version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a357d28ed41a50f9c765dbfe56cbc04a64e53e5fc58ba79fbc34c10ef3df831f" +checksum = "34aa73646ffb006b8f5147f3dc182bd4bcb190227ce861fc4a4844bf8e3cb2c0" [[package]] name = "env_filter" -version = "0.1.2" +version = "0.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4f2c92ceda6ceec50f43169f9ee8424fe2db276791afde7b2cd8bc084cb376ab" +checksum = "186e05a59d4c50738528153b83b0b0194d3a29507dfec16eccd4b342903397d0" dependencies = [ "log", "regex", ] +[[package]] +name = "env_home" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c7f84e12ccf0a7ddc17a6c41c93326024c42920d7ee630d04950e6926645c0fe" + [[package]] name = "env_logger" -version = "0.11.5" +version = "0.11.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e13fa619b91fb2381732789fc5de83b45675e882f66623b7d8cb4f643017018d" +checksum = "dcaee3d8e3cfc3fd92428d477bc97fc29ec8716d180c0d74c643bb26166660e0" dependencies = [ "anstream", "anstyle", @@ -589,9 +595,9 @@ checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80" [[package]] name = "foldhash" -version = "0.1.3" +version = "0.1.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f81ec6369c545a7d40e4589b5597581fa1c441fe1cce96dd1de43159910a36a2" +checksum = "a0d2fde1f7b3d48b8395d5f2de76c18a528bd6a9cdde438df747bfcba3e05d6f" [[package]] name = "getopts" @@ -672,11 +678,11 @@ checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" [[package]] name = "home" -version = "0.5.9" +version = "0.5.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e3d1354bf6b7235cb4a0576c2619fd4ed18183f689b12b006a0ee7329eeff9a5" +checksum = "589533453244b0995c858700322199b2becb13b627df2851f64a2775d024abcf" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.59.0", ] [[package]] @@ -779,7 +785,7 @@ dependencies = [ "shell-words", "strum", "strum_macros", - "syn 2.0.90", + "syn 2.0.91", "tracing", "tracing-subscriber", "tracing-tree 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)", @@ -828,7 +834,7 @@ dependencies = [ "toml", "tracing", "tracing-subscriber", - "which 7.0.0", + "which 7.0.1", ] [[package]] @@ -854,7 +860,7 @@ dependencies = [ "proc-macro-error2", "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -876,9 +882,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" [[package]] name = "libc" -version = "0.2.168" +version = "0.2.169" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5aaeb2981e0606ca11d79718f8bb01164f1d6ed75080182d3abf017e6d244b6d" +checksum = "b5aba8db14291edd000dfcc4d620c7ebfb122c613afb886ca8803fa4e128a20a" [[package]] name = "linear-map" @@ -918,7 +924,7 @@ version = "0.1.0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -950,9 +956,9 @@ checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a" [[package]] name = "miniz_oxide" -version = "0.8.0" +version = "0.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1" +checksum = "4ffbe83022cedc1d264172192511ae958937694cd57ce297164951b8b3568394" dependencies = [ "adler2", ] @@ -1100,9 +1106,9 @@ dependencies = [ [[package]] name = "object" -version = "0.36.5" +version = "0.36.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e" +checksum = "62948e14d923ea95ea2c7c86c71013138b66525b86bdc08d2dcc262bdb497b87" dependencies = [ "memchr", ] @@ -1115,9 +1121,9 @@ checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" [[package]] name = "os_info" -version = "3.9.0" +version = "3.9.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e5ca711d8b83edbb00b44d504503cd247c9c0bd8b0fa2694f2a1a3d8165379ce" +checksum = "eb6651f4be5e39563c4fe5cc8326349eb99a25d805a3493f791d5bfd0269e430" dependencies = [ "log", "windows-sys 0.52.0", @@ -1191,9 +1197,9 @@ dependencies = [ [[package]] name = "predicates" -version = "3.1.2" +version = "3.1.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7e9086cc7640c29a356d1a29fd134380bee9d8f79a17410aa76e7ad295f42c97" +checksum = "a5d19ee57562043d37e82899fade9a22ebab7be9cef5026b07fda9cdd4293573" dependencies = [ "anstyle", "difflib", @@ -1202,15 +1208,15 @@ dependencies = [ [[package]] name = "predicates-core" -version = "1.0.8" +version = "1.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ae8177bee8e75d6846599c6b9ff679ed51e882816914eec639944d7c9aa11931" +checksum = "727e462b119fe9c93fd0eb1429a5f7647394014cf3c04ab2c0350eeb09095ffa" [[package]] name = "predicates-tree" -version = "1.0.11" +version = "1.0.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "41b740d195ed3166cd147c8047ec98db0e22ec019eb8eeb76d343b795304fb13" +checksum = "72dd2d6d381dfb73a193c7fca536518d7caee39fc8503f74e7dc0be0531b425c" dependencies = [ "predicates-core", "termtree", @@ -1246,7 +1252,7 @@ dependencies = [ "proc-macro-error-attr2", "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -1491,14 +1497,14 @@ checksum = "46f859dbbf73865c6627ed570e78961cd3ac92407a2d117204c49232485da55e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] name = "serde_json" -version = "1.0.133" +version = "1.0.134" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c7fceb2473b9166b2294ef05efcb65a3db80803f0b03ef86a5fc88a2b85ee377" +checksum = "d00f4175c42ee48b15416f6193a959ba3a0d67fc699a0db9ad12df9f83991c7d" dependencies = [ "indexmap", "itoa", @@ -1642,7 +1648,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -1658,9 +1664,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.90" +version = "2.0.91" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "919d3b74a5dd0ccd15aeb8f93e7006bd9e14c295087c9896a110f490752bcf31" +checksum = "d53cbcb5a243bd33b7858b1d7f4aca2153490815872d86d955d6ea29f743c035" dependencies = [ "proc-macro2", "quote", @@ -1688,9 +1694,9 @@ dependencies = [ [[package]] name = "termtree" -version = "0.4.1" +version = "0.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3369f5ac52d5eb6ab48c6b4ffdc8efbcad6b89c765749064ba298f2c68a16a76" +checksum = "8f50febec83f5ee1df3015341d8bd429f2d1cc62bcba7ea2076759d315084683" [[package]] name = "thiserror" @@ -1703,11 +1709,11 @@ dependencies = [ [[package]] name = "thiserror" -version = "2.0.7" +version = "2.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "93605438cbd668185516ab499d589afb7ee1859ea3d5fc8f6b0755e1c7443767" +checksum = "f072643fd0190df67a8bab670c20ef5d8737177d6ac6b2e9a236cb096206b2cc" dependencies = [ - "thiserror-impl 2.0.7", + "thiserror-impl 2.0.9", ] [[package]] @@ -1718,18 +1724,18 @@ checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] name = "thiserror-impl" -version = "2.0.7" +version = "2.0.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e1d8749b4531af2117677a5fcd12b1348a3fe2b81e36e61ffeac5c4aa3273e36" +checksum = "7b50fa271071aae2e6ee85f842e2e28ba8cd2c5fb67f11fcb1fd70b276f9e7d4" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -1852,7 +1858,7 @@ checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] [[package]] @@ -2054,12 +2060,12 @@ dependencies = [ [[package]] name = "which" -version = "7.0.0" +version = "7.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c9cad3279ade7346b96e38731a641d7343dd6a53d55083dd54eadfa5a1b38c6b" +checksum = "fb4a9e33648339dc1642b0e36e21b3385e6148e289226f657c809dee59df5028" dependencies = [ "either", - "home", + "env_home", "rustix", "winsafe", ] @@ -2210,5 +2216,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.91", ] From f212ce560be1470df5acc4420d8ace45cab25426 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 23 Dec 2024 10:00:05 -0800 Subject: [PATCH 12/24] Bump tests/perf/s2n-quic from `0b3f892` to `a54686e` (#3793) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `0b3f892` to `a54686e`.
Commits
  • a54686e build(deps): bump docker/setup-buildx-action from 3.7.1 to 3.8.0 (#2427)
  • bf217ba build(deps): update rbpf requirement from 0.2 to 0.3 in /tools/xdp (#2320)
  • 3d27756 build(deps): update bindgen requirement from 0.70 to 0.71 in /tools/xdp (#2426)
  • See full diff in compare view

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 0b3f892ec7d4..a54686e4e1da 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit 0b3f892ec7d431249e41cae49fdc03869fd85b89 +Subproject commit a54686e4e1daad2afbbc01fccaf4cc1a512c58bf From 33b74e03a1fed6b045088e428a5a0cc5fcfd70f6 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Thu, 26 Dec 2024 13:44:08 -0500 Subject: [PATCH 13/24] Upgrade toolchain to nightly-2024-12-18 (#3794) Relevant upstream PR: https://github.com/rust-lang/rust/pull/131808. This required replacing `rustc_ast::Attribute` with the new `rustc_hir::Attribute`. Resolves #3788 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../src/codegen_cprover_gotoc/codegen/span.rs | 2 +- kani-compiler/src/kani_middle/attributes.rs | 45 +++++-------------- kani-compiler/src/main.rs | 1 + rust-toolchain.toml | 2 +- tests/expected/uninit/delayed-ub/expected | 22 ++++----- 5 files changed, 26 insertions(+), 46 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 00160a0db1a0..549fbcf3447d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs @@ -6,7 +6,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Location; use lazy_static::lazy_static; -use rustc_ast::Attribute; +use rustc_hir::Attribute; use rustc_smir::rustc_internal; use rustc_span::Span; use stable_mir::ty::Span as SpanStable; diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 017266717de7..83893da0707d 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -6,11 +6,9 @@ use std::collections::{BTreeMap, HashSet}; use kani_metadata::{CbmcSolver, HarnessAttributes, HarnessKind, Stub}; use quote::ToTokens; -use rustc_ast::{ - AttrArgs, AttrArgsEq, AttrKind, Attribute, ExprKind, LitKind, MetaItem, MetaItemKind, attr, -}; +use rustc_ast::{LitKind, MetaItem, MetaItemKind, attr}; use rustc_errors::ErrorGuaranteed; -use rustc_hir::{def::DefKind, def_id::DefId}; +use rustc_hir::{AttrArgs, AttrKind, Attribute, def::DefKind, def_id::DefId}; use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_session::Session; use rustc_smir::rustc_internal; @@ -673,31 +671,12 @@ fn expect_key_string_value( attr: &Attribute, ) -> Result { let span = attr.span; - let AttrArgs::Eq { eq_span: _, value } = &attr.get_normal_item().args else { + let AttrArgs::Eq { expr, .. } = &attr.get_normal_item().args else { return Err(sess .dcx() .span_err(span, "Expected attribute of the form #[attr = \"value\"]")); }; - let maybe_str = match value { - AttrArgsEq::Ast(expr) => { - if let ExprKind::Lit(tok) = expr.kind { - match LitKind::from_token_lit(tok) { - Ok(l) => l.str(), - Err(err) => { - return Err(sess.dcx().span_err( - span, - format!("Invalid string literal on right hand side of `=` {err:?}"), - )); - } - } - } else { - return Err(sess - .dcx() - .span_err(span, "Expected literal string as right hand side of `=`")); - } - } - AttrArgsEq::Hir(lit) => lit.kind.str(), - }; + let maybe_str = expr.kind.str(); if let Some(str) = maybe_str { Ok(str) } else { @@ -841,7 +820,7 @@ fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec Option { /// Extracts a vector with the path arguments of an attribute. /// /// Emits an error if it couldn't convert any of the arguments and return an empty vector. -fn parse_paths(attr: &Attribute) -> Result, syn::Error> { - let syn_attr = syn_attr(attr); +fn parse_paths(tcx: TyCtxt, attr: &Attribute) -> Result, syn::Error> { + let syn_attr = syn_attr(tcx, attr); let parser = Punctuated::::parse_terminated; let paths = syn_attr.parse_args_with(parser)?; Ok(paths.into_iter().collect()) @@ -990,11 +969,11 @@ fn parse_str_value(attr: &Attribute) -> Option { fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { match &attr.kind { AttrKind::Normal(normal) => { - let segments = &normal.item.path.segments; - if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" { + let segments = &normal.path.segments; + if (!segments.is_empty()) && segments[0].as_str() == "kanitool" { let ident_str = segments[1..] .iter() - .map(|segment| segment.ident.as_str()) + .map(|segment| segment.as_str()) .intersperse("::") .collect::(); KaniAttributeKind::try_from(ident_str.as_str()) @@ -1014,8 +993,8 @@ fn attr_kind(tcx: TyCtxt, attr: &Attribute) -> Option { /// Parse an attribute using `syn`. /// /// This provides a user-friendly interface to manipulate than the internal compiler AST. -fn syn_attr(attr: &Attribute) -> syn::Attribute { - let attr_str = rustc_ast_pretty::pprust::attribute_to_string(attr); +fn syn_attr(tcx: TyCtxt, attr: &Attribute) -> syn::Attribute { + let attr_str = rustc_hir_pretty::attribute_to_string(&tcx, attr); let parser = syn::Attribute::parse_outer; parser.parse_str(&attr_str).unwrap().pop().unwrap() } diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 65f1a22852b7..6f108595dbfc 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -25,6 +25,7 @@ extern crate rustc_data_structures; extern crate rustc_driver; extern crate rustc_errors; extern crate rustc_hir; +extern crate rustc_hir_pretty; extern crate rustc_index; extern crate rustc_interface; extern crate rustc_metadata; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 62deebf7a7d2..506443c043ca 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-12-15" +channel = "nightly-2024-12-18" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/uninit/delayed-ub/expected b/tests/expected/uninit/delayed-ub/expected index dc0411bdba9c..b7c139c2d101 100644 --- a/tests/expected/uninit/delayed-ub/expected +++ b/tests/expected/uninit/delayed-ub/expected @@ -1,44 +1,44 @@ -delayed_ub_trigger_copy.assertion.1\ +delayed_ub_trigger_copy.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\ -delayed_ub_slices.assertion.4\ +delayed_ub_slices.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`" -delayed_ub_structs.assertion.2\ +delayed_ub_structs.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `U`" -delayed_ub_double_copy.assertion.1\ +delayed_ub_double_copy.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\ -delayed_ub_copy.assertion.1\ +delayed_ub_copy.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_closure_capture_laundered.assertion.2\ +delayed_ub_closure_capture_laundered.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_closure_laundered.assertion.2\ +delayed_ub_closure_laundered.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_laundered.assertion.2\ +delayed_ub_laundered.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_static.assertion.4\ +delayed_ub_static.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub_transmute.assertion.2\ +delayed_ub_transmute.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" -delayed_ub.assertion.2\ +delayed_ub.assertion.\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" From a3f28bb864898b31710bb2f740926c426be09c9e Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Sat, 28 Dec 2024 14:34:43 -0500 Subject: [PATCH 14/24] replace ClosureType with ContractMode (to be consistent with kani-compiler) --- library/kani_macros/src/sysroot/contracts/check.rs | 4 ++-- .../kani_macros/src/sysroot/contracts/helpers.rs | 12 ++++++------ library/kani_macros/src/sysroot/contracts/mod.rs | 14 +++++++++----- .../kani_macros/src/sysroot/contracts/replace.rs | 4 ++-- 4 files changed, 19 insertions(+), 15 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 6dbee0fd6c37..055ce9ef2ce5 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -9,7 +9,7 @@ use std::mem; use syn::{Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt, parse_quote}; use super::{ - ClosureType, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, + ContractMode, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, helpers::*, shared::build_ensures, }; @@ -40,7 +40,7 @@ impl<'a> ContractConditionsHandler<'a> { let return_expr = body_stmts.pop(); let (assumes, rest_of_body) = - split_for_remembers(&body_stmts[..], ClosureType::Check); + split_for_remembers(&body_stmts[..], ContractMode::SimpleCheck); quote!({ #(#assumes)* diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index 49d101dad32a..bef8552c866a 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -4,7 +4,7 @@ //! Functions that operate third party data structures with no logic that is //! specific to Kani and contracts. -use crate::attr_impl::contracts::ClosureType; +use crate::attr_impl::contracts::ContractMode; use proc_macro2::{Ident, Span}; use std::borrow::Cow; use syn::spanned::Spanned; @@ -174,7 +174,7 @@ pub fn chunks_by<'a, T, C: Default + Extend>( } /// Splits `stmts` into (preconditions, rest). -/// For example, ClosureType::Check assumes preconditions, so given this sequence of statements: +/// For example, ContractMode::SimpleCheck assumes preconditions, so given this sequence of statements: /// ```ignore /// kani::assume(.. precondition_1); /// kani::assume(.. precondition_2); @@ -183,7 +183,7 @@ pub fn chunks_by<'a, T, C: Default + Extend>( /// ``` /// This function would return the two kani::assume statements in the former slice /// and the remaining statements in the latter. -/// The flow for ClosureType::Replace is the same, except preconditions are asserted rather than assumed. +/// The flow for ContractMode::Replace is the same, except preconditions are asserted rather than assumed. /// /// The caller can use the returned tuple to insert remembers statements after `preconditions` and before `rest`. /// Inserting the remembers statements after `preconditions` ensures that they are bound by the preconditions. @@ -197,12 +197,12 @@ pub fn chunks_by<'a, T, C: Default + Extend>( /// /// Inserting the remembers statements before `rest` ensures that they are declared before the original function executes, /// so that they will store historical, pre-computation values as intended. -pub fn split_for_remembers(stmts: &[Stmt], closure_type: ClosureType) -> (&[Stmt], &[Stmt]) { +pub fn split_for_remembers(stmts: &[Stmt], closure_type: ContractMode) -> (&[Stmt], &[Stmt]) { let mut pos = 0; let check_str = match closure_type { - ClosureType::Check => "assume", - ClosureType::Replace => "assert", + ContractMode::SimpleCheck => "assume", + ContractMode::Replace => "assert", }; for stmt in stmts { diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 41be536ffb6d..a629cca5a248 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -514,11 +514,15 @@ enum ContractConditionsData { }, } -/// Which function are we currently generating? -#[derive(Copy, Clone, Eq, PartialEq)] -enum ClosureType { - Check, - Replace, +/// Enumeration that stores the contract mode values. +/// +/// Keep the discriminant values in sync with [kani::internal::mode]. +#[derive(Copy, Clone, Debug, PartialEq, Eq)] +enum ContractMode { + Original = 0, + RecursiveCheck = 1, + SimpleCheck = 2, + Replace = 3, } impl<'a> ContractConditionsHandler<'a> { diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index b41985dea4c2..50c421ba76af 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -9,7 +9,7 @@ use std::mem; use syn::{Block, Stmt}; use super::{ - ClosureType, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, + ContractMode, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, helpers::*, shared::{build_ensures, try_as_result_assign}, }; @@ -96,7 +96,7 @@ impl<'a> ContractConditionsHandler<'a> { let (remembers, ensures_clause) = build_ensures(attr); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); - let (asserts, rest_of_before) = split_for_remembers(before, ClosureType::Replace); + let (asserts, rest_of_before) = split_for_remembers(before, ContractMode::Replace); quote!({ #(#asserts)* From b18d35aaa7bd9bfb11cfa9790129748785b71bfd Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Sat, 28 Dec 2024 18:08:23 -0500 Subject: [PATCH 15/24] move split_for_remembers to shared.rs; remove unused variants --- .../src/sysroot/contracts/check.rs | 2 +- .../src/sysroot/contracts/helpers.rs | 50 +----------------- .../kani_macros/src/sysroot/contracts/mod.rs | 12 ++--- .../src/sysroot/contracts/replace.rs | 2 +- .../src/sysroot/contracts/shared.rs | 51 ++++++++++++++++++- 5 files changed, 57 insertions(+), 60 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 055ce9ef2ce5..934ed357ad7d 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -10,7 +10,7 @@ use syn::{Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt, use super::{ ContractMode, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, - helpers::*, shared::build_ensures, + helpers::*, shared::{build_ensures, split_for_remembers} }; const WRAPPER_ARG: &str = "_wrapper_arg"; diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index bef8552c866a..5a7da2187418 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -4,12 +4,11 @@ //! Functions that operate third party data structures with no logic that is //! specific to Kani and contracts. -use crate::attr_impl::contracts::ContractMode; use proc_macro2::{Ident, Span}; use std::borrow::Cow; use syn::spanned::Spanned; use syn::{ - Attribute, Expr, ExprBlock, ExprCall, ExprPath, Local, LocalInit, PatIdent, Path, Stmt, + Attribute, Expr, ExprBlock, Local, LocalInit, PatIdent, Stmt, parse_quote, }; @@ -173,53 +172,6 @@ pub fn chunks_by<'a, T, C: Default + Extend>( }) } -/// Splits `stmts` into (preconditions, rest). -/// For example, ContractMode::SimpleCheck assumes preconditions, so given this sequence of statements: -/// ```ignore -/// kani::assume(.. precondition_1); -/// kani::assume(.. precondition_2); -/// let _wrapper_arg = (ptr as * const _,); -/// ... -/// ``` -/// This function would return the two kani::assume statements in the former slice -/// and the remaining statements in the latter. -/// The flow for ContractMode::Replace is the same, except preconditions are asserted rather than assumed. -/// -/// The caller can use the returned tuple to insert remembers statements after `preconditions` and before `rest`. -/// Inserting the remembers statements after `preconditions` ensures that they are bound by the preconditions. -/// To understand why this is important, take the following example: -/// ```ignore -/// #[kani::requires(x < u32::MAX)] -/// #[kani::ensures(|result| old(x + 1) == *result)] -/// fn add_one(x: u32) -> u32 {...} -/// ``` -/// If the `old(x + 1)` statement didn't respect the precondition's upper bound on `x`, Kani would encounter an integer overflow. -/// -/// Inserting the remembers statements before `rest` ensures that they are declared before the original function executes, -/// so that they will store historical, pre-computation values as intended. -pub fn split_for_remembers(stmts: &[Stmt], closure_type: ContractMode) -> (&[Stmt], &[Stmt]) { - let mut pos = 0; - - let check_str = match closure_type { - ContractMode::SimpleCheck => "assume", - ContractMode::Replace => "assert", - }; - - for stmt in stmts { - if let Stmt::Expr(Expr::Call(ExprCall { func, .. }), _) = stmt { - if let Expr::Path(ExprPath { path: Path { segments, .. }, .. }) = func.as_ref() { - let first_two_idents = - segments.iter().take(2).map(|sgmt| sgmt.ident.to_string()).collect::>(); - - if first_two_idents == vec!["kani", check_str] { - pos += 1; - } - } - } - } - stmts.split_at(pos) -} - macro_rules! assert_spanned_err { ($condition:expr, $span_source:expr, $msg:expr, $($args:expr),+) => { if !$condition { diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index a629cca5a248..118f49f897c3 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -514,15 +514,13 @@ enum ContractConditionsData { }, } -/// Enumeration that stores the contract mode values. -/// -/// Keep the discriminant values in sync with [kani::internal::mode]. +/// Enumeration that stores (some of) the contract mode values. +/// We elide the Original and RecursiveCheck variants because we don't need them for any work in this module. #[derive(Copy, Clone, Debug, PartialEq, Eq)] enum ContractMode { - Original = 0, - RecursiveCheck = 1, - SimpleCheck = 2, - Replace = 3, + SimpleCheck, + Replace, + Assert, } impl<'a> ContractConditionsHandler<'a> { diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 50c421ba76af..e5e6f88337f9 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -11,7 +11,7 @@ use syn::{Block, Stmt}; use super::{ ContractMode, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, helpers::*, - shared::{build_ensures, try_as_result_assign}, + shared::{build_ensures, split_for_remembers, try_as_result_assign}, }; impl<'a> ContractConditionsHandler<'a> { diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index d7e77ee2a8d4..b42f51624fb0 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -12,9 +12,56 @@ use std::collections::HashMap; use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::quote; use std::hash::{DefaultHasher, Hash, Hasher}; -use syn::{Expr, ExprCall, ExprClosure, ExprPath, Path, spanned::Spanned, visit_mut::VisitMut}; +use syn::{Expr, ExprCall, ExprClosure, ExprPath, Path, Stmt, spanned::Spanned, visit_mut::VisitMut}; + +use super::{ContractMode, INTERNAL_RESULT_IDENT}; + +/// Splits `stmts` into (preconditions, rest). +/// For example, ContractMode::SimpleCheck assumes preconditions, so given this sequence of statements: +/// ```ignore +/// kani::assume(.. precondition_1); +/// kani::assume(.. precondition_2); +/// let _wrapper_arg = (ptr as * const _,); +/// ... +/// ``` +/// This function would return the two kani::assume statements in the former slice +/// and the remaining statements in the latter. +/// The flow for ContractMode::Replace is the same, except preconditions are asserted rather than assumed. +/// +/// The caller can use the returned tuple to insert remembers statements after `preconditions` and before `rest`. +/// Inserting the remembers statements after `preconditions` ensures that they are bound by the preconditions. +/// To understand why this is important, take the following example: +/// ```ignore +/// #[kani::requires(x < u32::MAX)] +/// #[kani::ensures(|result| old(x + 1) == *result)] +/// fn add_one(x: u32) -> u32 {...} +/// ``` +/// If the `old(x + 1)` statement didn't respect the precondition's upper bound on `x`, Kani would encounter an integer overflow. +/// +/// Inserting the remembers statements before `rest` ensures that they are declared before the original function executes, +/// so that they will store historical, pre-computation values as intended. +pub fn split_for_remembers(stmts: &[Stmt], contract_mode: ContractMode) -> (&[Stmt], &[Stmt]) { + let mut pos = 0; + + let check_str = match contract_mode { + ContractMode::SimpleCheck => "assume", + ContractMode::Replace | ContractMode::Assert => "assert", + }; -use super::INTERNAL_RESULT_IDENT; + for stmt in stmts { + if let Stmt::Expr(Expr::Call(ExprCall { func, .. }), _) = stmt { + if let Expr::Path(ExprPath { path: Path { segments, .. }, .. }) = func.as_ref() { + let first_two_idents = + segments.iter().take(2).map(|sgmt| sgmt.ident.to_string()).collect::>(); + + if first_two_idents == vec!["kani", check_str] { + pos += 1; + } + } + } + } + stmts.split_at(pos) +} /// Used as the "single source of truth" for [`try_as_result_assign`] and [`try_as_result_assign_mut`] /// since we can't abstract over mutability. Input is the object to match on and the name of the From 11f3e0417db82721be8e8d6ddd1d8dc92b7accc0 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Sat, 28 Dec 2024 21:22:41 -0500 Subject: [PATCH 16/24] add ContractMode for assertions to library/kani_macros --- library/kani_core/src/lib.rs | 3 + .../src/sysroot/contracts/assert.rs | 90 +++++++++++++++++++ .../src/sysroot/contracts/bootstrap.rs | 11 +++ .../src/sysroot/contracts/check.rs | 5 +- .../src/sysroot/contracts/helpers.rs | 5 +- .../src/sysroot/contracts/initialize.rs | 2 + .../kani_macros/src/sysroot/contracts/mod.rs | 42 +++++++++ .../src/sysroot/contracts/replace.rs | 2 +- .../src/sysroot/contracts/shared.rs | 4 +- 9 files changed, 156 insertions(+), 8 deletions(-) create mode 100644 library/kani_macros/src/sysroot/contracts/assert.rs diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 2d77fae0c48a..3ba2f459470e 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -496,6 +496,9 @@ macro_rules! kani_intrinsics { /// Stub the body with its contract. pub const REPLACE: Mode = 3; + /// Insert the contract into the body of the function as assertion(s). + pub const ASSERT: Mode = 4; + /// Creates a non-fatal property with the specified condition and message. /// /// This check will not impact the program control flow even when it fails. diff --git a/library/kani_macros/src/sysroot/contracts/assert.rs b/library/kani_macros/src/sysroot/contracts/assert.rs new file mode 100644 index 000000000000..4347bbf3cae6 --- /dev/null +++ b/library/kani_macros/src/sysroot/contracts/assert.rs @@ -0,0 +1,90 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Logic used for generating the code that generates contract preconditions and postconditions as assertions. + +use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; +use quote::quote; +use std::mem; +use syn::{Stmt, parse_quote}; + +use super::{ + ContractConditionsData, ContractConditionsHandler, ContractMode, INTERNAL_RESULT_IDENT, + helpers::*, + shared::{build_ensures, split_for_remembers}, +}; + +impl<'a> ContractConditionsHandler<'a> { + /// Generate a token stream that represents the assert closure. + /// + /// See [`Self::make_assert_body`] for the most interesting parts of this + /// function. + pub fn assert_closure(&self) -> TokenStream2 { + let assert_ident = Ident::new(&self.assert_name, Span::call_site()); + let sig = &self.annotated_fn.sig; + let output = &sig.output; + let body_stmts = self.initial_assert_stmts(); + let body = self.make_assert_body(body_stmts); + + quote!( + #[kanitool::is_contract_generated(assert)] + #[allow(dead_code, unused_variables, unused_mut)] + let mut #assert_ident = || #output #body; + ) + } + + /// Expand the assert closure body. + pub fn expand_assert(&self, closure: &mut Stmt) { + let body = closure_body(closure); + *body = syn::parse2(self.make_assert_body(mem::take(&mut body.block.stmts))).unwrap(); + } + + /// Initialize the list of statements for the assert closure body. + fn initial_assert_stmts(&self) -> Vec { + let return_type = return_type_to_type(&self.annotated_fn.sig.output); + let stmts = &self.annotated_fn.block.stmts; + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + parse_quote! { + let #result : #return_type = {#(#stmts)*}; + #result + } + } + + /// Create the body of an assert closure. + /// + /// Wraps the conditions from this attribute around `self.body`. + fn make_assert_body(&self, mut body_stmts: Vec) -> TokenStream2 { + let Self { attr_copy, .. } = self; + match &self.condition_type { + ContractConditionsData::Requires { attr } => { + quote!({ + kani::assert(#attr, stringify!(#attr_copy)); + #(#body_stmts)* + }) + } + ContractConditionsData::Ensures { attr } => { + let (remembers, ensures_clause) = build_ensures(attr); + + let exec_postconditions = quote!( + kani::assert(#ensures_clause, stringify!(#attr_copy)); + ); + + let return_expr = body_stmts.pop(); + + let (asserts, rest_of_body) = + split_for_remembers(&body_stmts[..], ContractMode::Assert); + + quote!({ + #(#asserts)* + #remembers + #(#rest_of_body)* + #exec_postconditions + #return_expr + }) + } + ContractConditionsData::Modifies { .. } => { + quote!({#(#body_stmts)*}) + } + } + } +} diff --git a/library/kani_macros/src/sysroot/contracts/bootstrap.rs b/library/kani_macros/src/sysroot/contracts/bootstrap.rs index 5a9e12a62ae2..2341655ec9ff 100644 --- a/library/kani_macros/src/sysroot/contracts/bootstrap.rs +++ b/library/kani_macros/src/sysroot/contracts/bootstrap.rs @@ -20,15 +20,18 @@ impl<'a> ContractConditionsHandler<'a> { let modifies_name = &self.modify_name; let recursion_name = &self.recursion_name; let check_name = &self.check_name; + let assert_name = &self.assert_name; let replace_closure = self.replace_closure(); let check_closure = self.check_closure(); let recursion_closure = self.new_recursion_closure(&replace_closure, &check_closure); + let assert_closure = self.assert_closure(); let span = Span::call_site(); let replace_ident = Ident::new(&self.replace_name, span); let check_ident = Ident::new(&self.check_name, span); let recursion_ident = Ident::new(&self.recursion_name, span); + let assert_ident = Ident::new(&self.assert_name, span); // The order of `attrs` and `kanitool::{checked_with, // is_contract_generated}` is important here, because macros are @@ -41,6 +44,7 @@ impl<'a> ContractConditionsHandler<'a> { #[kanitool::recursion_check = #recursion_name] #[kanitool::checked_with = #check_name] #[kanitool::replaced_with = #replace_name] + #[kanitool::asserted_with = #assert_name] #[kanitool::modifies_wrapper = #modifies_name] #vis #sig { // Dummy function used to force the compiler to capture the environment. @@ -72,6 +76,10 @@ impl<'a> ContractConditionsHandler<'a> { #check_closure; kani_register_contract(#check_ident) } + kani::internal::ASSERT => { + #assert_closure; + kani_register_contract(#assert_ident) + } _ => #block } } @@ -94,6 +102,9 @@ impl<'a> ContractConditionsHandler<'a> { let check_closure = expect_closure_in_match(&mut block.stmts, "check"); self.expand_check(check_closure); + let assert_closure = expect_closure_in_match(&mut block.stmts, "assert"); + self.expand_assert(assert_closure); + self.output.extend(quote!(#annotated_fn)); } diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 934ed357ad7d..6a473a2060d2 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -9,8 +9,9 @@ use std::mem; use syn::{Block, Expr, FnArg, Local, LocalInit, Pat, PatIdent, ReturnType, Stmt, parse_quote}; use super::{ - ContractMode, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, - helpers::*, shared::{build_ensures, split_for_remembers} + ContractConditionsData, ContractConditionsHandler, ContractMode, INTERNAL_RESULT_IDENT, + helpers::*, + shared::{build_ensures, split_for_remembers}, }; const WRAPPER_ARG: &str = "_wrapper_arg"; diff --git a/library/kani_macros/src/sysroot/contracts/helpers.rs b/library/kani_macros/src/sysroot/contracts/helpers.rs index 5a7da2187418..becb07d43033 100644 --- a/library/kani_macros/src/sysroot/contracts/helpers.rs +++ b/library/kani_macros/src/sysroot/contracts/helpers.rs @@ -7,10 +7,7 @@ use proc_macro2::{Ident, Span}; use std::borrow::Cow; use syn::spanned::Spanned; -use syn::{ - Attribute, Expr, ExprBlock, Local, LocalInit, PatIdent, Stmt, - parse_quote, -}; +use syn::{Attribute, Expr, ExprBlock, Local, LocalInit, PatIdent, Stmt, parse_quote}; /// If an explicit return type was provided it is returned, otherwise `()`. pub fn return_type_to_type(return_type: &syn::ReturnType) -> Cow { diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index bd06139b27f5..2d2e2d28b190 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/library/kani_macros/src/sysroot/contracts/initialize.rs @@ -71,6 +71,7 @@ impl<'a> ContractConditionsHandler<'a> { let fn_name = &annotated_fn.sig.ident; let generate_name = |purpose| format!("__kani_{purpose}_{fn_name}"); + let assert_name = generate_name("assert"); let check_name = generate_name("check"); let replace_name = generate_name("replace"); let recursion_name = generate_name("recursion_check"); @@ -84,6 +85,7 @@ impl<'a> ContractConditionsHandler<'a> { check_name, replace_name, recursion_name, + assert_name, modify_name: modifies_name, }) } diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 118f49f897c3..ad8fef125c61 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -132,6 +132,7 @@ //! #[kanitool::checked_with = "__kani_check_div"] //! #[kanitool::replaced_with = "__kani_replace_div"] //! #[kanitool::modifies_wrapper = "__kani_modifies_div"] +//! #[kanitool::asserted_with = "__kani_assert_div"] //! fn div(dividend: u32, divisor: u32) -> u32 { //! #[inline(never)] //! #[kanitool::fn_marker = "kani_register_contract"] @@ -226,6 +227,22 @@ //! ; //! kani_register_contract(__kani_check_div) //! } +//! kani::internal::ASSERT => { +//! #[kanitool::is_contract_generated(assert)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_assert_div = +//! || -> u32 +//! { +//! kani::assert(divisor != 0, "divisor != 0"); +//! let result_kani_internal: u32 = { dividend / divisor }; +//! kani::assert(kani::internal::apply_closure(|result: &u32| +//! *result <= dividend, &result_kani_internal), +//! "|result : &u32| *result <= dividend"); +//! result_kani_internal +//! }; +//! ; +//! kani_register_contract(__kani_assert_div) +//! } //! _ => { dividend / divisor } //! } //! } @@ -265,6 +282,7 @@ //! #[kanitool::checked_with = "__kani_check_modify"] //! #[kanitool::replaced_with = "__kani_replace_modify"] //! #[kanitool::modifies_wrapper = "__kani_modifies_modify"] +//! #[kanitool::asserted_with = "__kani_assert_modify"] //! fn modify(ptr: &mut u32) { //! #[inline(never)] //! #[kanitool::fn_marker = "kani_register_contract"] @@ -387,6 +405,27 @@ //! ; //! kani_register_contract(__kani_check_modify) //! } +//! kani::internal::ASSERT => { +//! #[kanitool::is_contract_generated(assert)] +//! #[allow(dead_code, unused_variables, unused_mut)] +//! let mut __kani_assert_modify = +//! || +//! { +//! kani::assert(*ptr < 100, "*ptr < 100"); +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let remember_kani_internal_92cc419d8aca576c = *ptr + 1; +//! let result_kani_internal: () = { *ptr += 1; }; +//! kani::assert(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); +//! kani::assert(kani::internal::apply_closure(|result| +//! (remember_kani_internal_92cc419d8aca576c) == *ptr, +//! &result_kani_internal), "|result| old(*ptr + 1) == *ptr"); +//! result_kani_internal +//! }; +//! ; +//! kani_register_contract(__kani_assert_modify) +//! } //! _ => { *ptr += 1; } //! } //! } @@ -397,6 +436,7 @@ use proc_macro2::{Ident, TokenStream as TokenStream2}; use quote::quote; use syn::{Expr, ExprClosure, ItemFn, parse_macro_input, parse_quote}; +mod assert; mod bootstrap; mod check; #[macro_use] @@ -483,6 +523,8 @@ struct ContractConditionsHandler<'a> { replace_name: String, /// The name of the recursion closure. recursion_name: String, + /// The name of the assertion closure. + assert_name: String, /// The name of the modifies closure. modify_name: String, } diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index e5e6f88337f9..bb2ba01406c0 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -9,7 +9,7 @@ use std::mem; use syn::{Block, Stmt}; use super::{ - ContractMode, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT, + ContractConditionsData, ContractConditionsHandler, ContractMode, INTERNAL_RESULT_IDENT, helpers::*, shared::{build_ensures, split_for_remembers, try_as_result_assign}, }; diff --git a/library/kani_macros/src/sysroot/contracts/shared.rs b/library/kani_macros/src/sysroot/contracts/shared.rs index b42f51624fb0..833303307af8 100644 --- a/library/kani_macros/src/sysroot/contracts/shared.rs +++ b/library/kani_macros/src/sysroot/contracts/shared.rs @@ -12,7 +12,9 @@ use std::collections::HashMap; use proc_macro2::{Ident, Span, TokenStream as TokenStream2}; use quote::quote; use std::hash::{DefaultHasher, Hash, Hasher}; -use syn::{Expr, ExprCall, ExprClosure, ExprPath, Path, Stmt, spanned::Spanned, visit_mut::VisitMut}; +use syn::{ + Expr, ExprCall, ExprClosure, ExprPath, Path, Stmt, spanned::Spanned, visit_mut::VisitMut, +}; use super::{ContractMode, INTERNAL_RESULT_IDENT}; From 1f135c9147eb836433184827bd5c918091fa5af8 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Sat, 28 Dec 2024 21:23:29 -0500 Subject: [PATCH 17/24] add option to use Assert ContractMode --- kani-compiler/src/kani_middle/attributes.rs | 15 ++++++++-- .../src/kani_middle/transform/contracts.rs | 29 +++++++++++++++++++ kani_metadata/src/unstable.rs | 2 ++ 3 files changed, 44 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 017266717de7..32f83f241e8c 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -44,6 +44,9 @@ enum KaniAttributeKind { /// contract, e.g. the contract check is substituted for the target function /// before the the verification runs. ProofForContract, + /// Internal attribute of the contracts implementation that identifies the + /// code implementing the function with the contract clauses as assertions. + AssertedWith, /// Attribute on a function with a contract that identifies the code /// implementing the check for this contract. CheckedWith, @@ -96,6 +99,7 @@ impl KaniAttributeKind { | KaniAttributeKind::RecursionCheck | KaniAttributeKind::CheckedWith | KaniAttributeKind::ModifiesWrapper + | KaniAttributeKind::AssertedWith | KaniAttributeKind::IsContractGenerated | KaniAttributeKind::DisableChecks => false, } @@ -138,6 +142,8 @@ pub struct ContractAttributes { pub replaced_with: Symbol, /// The name of the inner check used to modify clauses. pub modifies_wrapper: Symbol, + /// The name of the contract assert closure + pub asserted_with: Symbol, } impl std::fmt::Debug for KaniAttributes<'_> { @@ -266,17 +272,19 @@ impl<'tcx> KaniAttributes<'tcx> { let checked_with = self.attribute_value(KaniAttributeKind::CheckedWith); let replace_with = self.attribute_value(KaniAttributeKind::ReplacedWith); let modifies_wrapper = self.attribute_value(KaniAttributeKind::ModifiesWrapper); + let asserted_with = self.attribute_value(KaniAttributeKind::AssertedWith); let total = recursion_check .iter() .chain(&checked_with) .chain(&replace_with) .chain(&modifies_wrapper) + .chain(&asserted_with) .count(); - if total != 0 && total != 4 { + if total != 0 && total != 5 { self.tcx.sess.dcx().err(format!( "Failed to parse contract instrumentation tags in function `{}`.\ - Expected `4` attributes, but was only able to process `{total}`", + Expected `5` attributes, but was only able to process `{total}`", self.tcx.def_path_str(self.item) )); } @@ -286,6 +294,7 @@ impl<'tcx> KaniAttributes<'tcx> { checked_with: checked_with?, replaced_with: replace_with?, modifies_wrapper: modifies_wrapper?, + asserted_with: asserted_with?, }) } @@ -379,6 +388,7 @@ impl<'tcx> KaniAttributes<'tcx> { | KaniAttributeKind::CheckedWith | KaniAttributeKind::ModifiesWrapper | KaniAttributeKind::RecursionCheck + | KaniAttributeKind::AssertedWith | KaniAttributeKind::ReplacedWith => { self.attribute_value(kind); } @@ -531,6 +541,7 @@ impl<'tcx> KaniAttributes<'tcx> { | KaniAttributeKind::ModifiesWrapper | KaniAttributeKind::RecursionCheck | KaniAttributeKind::RecursionTracker + | KaniAttributeKind::AssertedWith | KaniAttributeKind::ReplacedWith => { self.tcx.dcx().span_err(self.tcx.def_span(self.item), format!("Contracts are not supported on harnesses. (Found the kani-internal contract attribute `{}`)", kind.as_ref())); } diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 0281742d008f..5df3c999edad 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -224,6 +224,7 @@ impl AnyModifiesPass { /// #[kanitool::recursion_check = "__kani_recursion_check_modify"] /// #[kanitool::checked_with = "__kani_check_modify"] /// #[kanitool::replaced_with = "__kani_replace_modify"] +/// #[kanitool::asserted_with = "__kani_assert_modify"] /// #[kanitool::modifies_wrapper = "__kani_modifies_modify"] /// fn name_fn(ptr: &mut u32) { /// #[kanitool::fn_marker = "kani_register_contract"] @@ -247,6 +248,11 @@ impl AnyModifiesPass { /// let mut __kani_check_name_fn = || { /* check body */ }; /// kani_register_contract(__kani_check_name_fn) /// } +/// kani::internal::ASSERT => { +/// #[kanitool::is_contract_generated(assert)] +/// let mut __kani_check_name_fn = || { /* assert body */ }; +/// kani_register_contract(__kani_assert_name_fn) +/// } /// _ => { /* original body */ } /// } /// } @@ -267,6 +273,8 @@ pub struct FunctionWithContractPass { check_fn: Option, /// Functions that should be stubbed by their contract. replace_fns: HashSet, + /// Should we interpret contracts as assertions? (true iff the contracts-as-assertions option is passed) + are_contracts_asserted: bool, /// Functions annotated with contract attributes will contain contract closures even if they /// are not to be used in this harness. /// In order to avoid bringing unnecessary logic, we clear their body. @@ -346,6 +354,10 @@ impl FunctionWithContractPass { FunctionWithContractPass { check_fn, replace_fns, + are_contracts_asserted: queries + .args() + .unstable_features + .contains(&"contracts-as-assertions".to_string()), unused_closures: Default::default(), run_contract_fn, } @@ -371,6 +383,9 @@ impl FunctionWithContractPass { /// kani::internal::SIMPLE_CHECK => { /// // same as above /// } + /// kani::internal::ASSERT => { + /// // same as above + /// } /// _ => { /* original code */} /// } /// } @@ -431,6 +446,7 @@ impl FunctionWithContractPass { } /// Return which contract mode to use for this function if any. + /// TODO document precedence fn contract_mode(&self, tcx: TyCtxt, fn_def: FnDef) -> Option { let kani_attributes = KaniAttributes::for_def_id(tcx, fn_def.def_id()); kani_attributes.has_contract().then(|| { @@ -443,6 +459,8 @@ impl FunctionWithContractPass { } } else if self.replace_fns.contains(&fn_def_id) { ContractMode::Replace + } else if self.are_contracts_asserted { + ContractMode::Assert } else { ContractMode::Original } @@ -456,24 +474,34 @@ impl FunctionWithContractPass { let recursion_closure = find_closure(tcx, fn_def, &body, contract.recursion_check.as_str()); let check_closure = find_closure(tcx, fn_def, &body, contract.checked_with.as_str()); let replace_closure = find_closure(tcx, fn_def, &body, contract.replaced_with.as_str()); + let assert_closure = find_closure(tcx, fn_def, &body, contract.asserted_with.as_str()); match mode { ContractMode::Original => { // No contract instrumentation needed. Add all closures to the list of unused. self.unused_closures.insert(recursion_closure); self.unused_closures.insert(check_closure); self.unused_closures.insert(replace_closure); + self.unused_closures.insert(assert_closure); } ContractMode::RecursiveCheck => { self.unused_closures.insert(replace_closure); self.unused_closures.insert(check_closure); + self.unused_closures.insert(assert_closure); } ContractMode::SimpleCheck => { self.unused_closures.insert(replace_closure); self.unused_closures.insert(recursion_closure); + self.unused_closures.insert(assert_closure); } ContractMode::Replace => { self.unused_closures.insert(recursion_closure); self.unused_closures.insert(check_closure); + self.unused_closures.insert(assert_closure); + } + ContractMode::Assert => { + self.unused_closures.insert(recursion_closure); + self.unused_closures.insert(check_closure); + self.unused_closures.insert(replace_closure); } } } @@ -488,6 +516,7 @@ enum ContractMode { RecursiveCheck = 1, SimpleCheck = 2, Replace = 3, + Assert = 4, } fn find_closure(tcx: TyCtxt, fn_def: FnDef, body: &Body, name: &str) -> ClosureDef { diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index e4f5bcaadd57..3d260085e8c2 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -85,6 +85,8 @@ pub enum UnstableFeature { FunctionContracts, /// Enable loop contracts [RFC 12](https://model-checking.github.io/kani/rfc/rfcs/0012-loop-contracts.html) LoopContracts, + /// Enable function contracts to be interpreted as assertions. (Requires function-contracts option). + ContractsAsAssertions, /// Memory predicate APIs. MemPredicates, /// Automatically check that no invalid value is produced which is considered UB in Rust. From 7913e3c05d25237cf73652c2ae0051d5918a5307 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 30 Dec 2024 07:51:45 +0000 Subject: [PATCH 18/24] Automatic cargo update to 2024-12-30 (#3800) Dependency upgrade resulting from `cargo update`. Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com> --- Cargo.lock | 54 +++++++++++++++++++++++++++--------------------------- 1 file changed, 27 insertions(+), 27 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index de3f2603cf30..2d7e93794faf 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -225,9 +225,9 @@ dependencies = [ [[package]] name = "cc" -version = "1.2.5" +version = "1.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c31a0499c1dc64f458ad13872de75c0eb7e3fdb0e67964610c914b034fc5956e" +checksum = "8d6dbb628b8f8555f86d0323c2eb39e3ec81901f4b83e091db8a6a76d316a333" dependencies = [ "shlex", ] @@ -307,7 +307,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.91", + "syn 2.0.93", ] [[package]] @@ -627,9 +627,9 @@ checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f" [[package]] name = "glob" -version = "0.3.1" +version = "0.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" +checksum = "a8d1add55171497b4705a648c6b583acafb01d58050a51727785f0b2c8e0a2b2" [[package]] name = "graph-cycles" @@ -785,7 +785,7 @@ dependencies = [ "shell-words", "strum", "strum_macros", - "syn 2.0.91", + "syn 2.0.93", "tracing", "tracing-subscriber", "tracing-tree 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)", @@ -860,7 +860,7 @@ dependencies = [ "proc-macro-error2", "proc-macro2", "quote", - "syn 2.0.91", + "syn 2.0.93", ] [[package]] @@ -924,7 +924,7 @@ version = "0.1.0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.91", + "syn 2.0.93", ] [[package]] @@ -1252,7 +1252,7 @@ dependencies = [ "proc-macro-error-attr2", "proc-macro2", "quote", - "syn 2.0.91", + "syn 2.0.93", ] [[package]] @@ -1275,9 +1275,9 @@ dependencies = [ [[package]] name = "quote" -version = "1.0.37" +version = "1.0.38" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" +checksum = "0e4dccaaaf89514f546c693ddc140f729f958c247918a13380cccc6078391acc" dependencies = [ "proc-macro2", ] @@ -1425,9 +1425,9 @@ dependencies = [ [[package]] name = "rustversion" -version = "1.0.18" +version = "1.0.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e819f2bc632f285be6d7cd36e25940d45b2391dd6d9b939e79de557f7014248" +checksum = "f7c45b9784283f1b2e7fb61b42047c2fd678ef0960d4f6f1eba131594cc369d4" [[package]] name = "ryu" @@ -1473,9 +1473,9 @@ dependencies = [ [[package]] name = "serde" -version = "1.0.216" +version = "1.0.217" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b9781016e935a97e8beecf0c933758c97a5520d32930e460142b4cd80c6338e" +checksum = "02fc4265df13d6fa1d00ecff087228cc0a2b5f3c0e87e258d8b94a156e984c70" dependencies = [ "serde_derive", ] @@ -1491,13 +1491,13 @@ dependencies = [ [[package]] name = "serde_derive" -version = "1.0.216" +version = "1.0.217" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "46f859dbbf73865c6627ed570e78961cd3ac92407a2d117204c49232485da55e" +checksum = "5a9bf7cf98d04a2b28aead066b7496853d4779c9cc183c440dbac457641e19a0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.91", + "syn 2.0.93", ] [[package]] @@ -1648,7 +1648,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.91", + "syn 2.0.93", ] [[package]] @@ -1664,9 +1664,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.91" +version = "2.0.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d53cbcb5a243bd33b7858b1d7f4aca2153490815872d86d955d6ea29f743c035" +checksum = "9c786062daee0d6db1132800e623df74274a0a87322d8e183338e01b3d98d058" dependencies = [ "proc-macro2", "quote", @@ -1724,7 +1724,7 @@ checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" dependencies = [ "proc-macro2", "quote", - "syn 2.0.91", + "syn 2.0.93", ] [[package]] @@ -1735,7 +1735,7 @@ checksum = "7b50fa271071aae2e6ee85f842e2e28ba8cd2c5fb67f11fcb1fd70b276f9e7d4" dependencies = [ "proc-macro2", "quote", - "syn 2.0.91", + "syn 2.0.93", ] [[package]] @@ -1858,7 +1858,7 @@ checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d" dependencies = [ "proc-macro2", "quote", - "syn 2.0.91", + "syn 2.0.93", ] [[package]] @@ -1940,9 +1940,9 @@ dependencies = [ [[package]] name = "tree-sitter" -version = "0.24.5" +version = "0.24.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8ac95b18f0f727aaaa012bd5179a1916706ee3ed071920fdbda738750b0c0bf5" +checksum = "5f2434c86ba59ed15af56039cc5bf1acf8ba76ce301e32ef08827388ef285ec5" dependencies = [ "cc", "regex", @@ -2216,5 +2216,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.91", + "syn 2.0.93", ] From d4a8fc092f8443da6623df9e84878d3ffdc67437 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 30 Dec 2024 15:44:36 -0500 Subject: [PATCH 19/24] tests --- .../assert-postconditions.expected | 9 +++ .../as-assertions/assert-postconditions.rs | 32 ++++++++++ .../assert-preconditions.expected | 21 ++++++ .../as-assertions/assert-preconditions.rs | 64 +++++++++++++++++++ .../as-assertions/precedence.expected | 13 ++++ .../as-assertions/precedence.rs | 48 ++++++++++++++ 6 files changed, 187 insertions(+) create mode 100644 tests/expected/function-contract/as-assertions/assert-postconditions.expected create mode 100644 tests/expected/function-contract/as-assertions/assert-postconditions.rs create mode 100644 tests/expected/function-contract/as-assertions/assert-preconditions.expected create mode 100644 tests/expected/function-contract/as-assertions/assert-preconditions.rs create mode 100644 tests/expected/function-contract/as-assertions/precedence.expected create mode 100644 tests/expected/function-contract/as-assertions/precedence.rs diff --git a/tests/expected/function-contract/as-assertions/assert-postconditions.expected b/tests/expected/function-contract/as-assertions/assert-postconditions.expected new file mode 100644 index 000000000000..08b8171aa4e1 --- /dev/null +++ b/tests/expected/function-contract/as-assertions/assert-postconditions.expected @@ -0,0 +1,9 @@ +assertion\ + - Status: FAILURE\ + - Description: "|result| old(*add_two_ptr + 1) == *add_two_ptr" + +assertion\ + - Status: SUCCESS\ + - Description: "|result| old(*add_one_ptr + 1) == *add_one_ptr" + +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/as-assertions/assert-postconditions.rs b/tests/expected/function-contract/as-assertions/assert-postconditions.rs new file mode 100644 index 000000000000..fb6a0dbcc849 --- /dev/null +++ b/tests/expected/function-contract/as-assertions/assert-postconditions.rs @@ -0,0 +1,32 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts -Zcontracts-as-assertions + +// Test -Zcontracts-as-assertions for postconditions. + +#[kani::requires(*add_three_ptr < 100)] +#[kani::modifies(add_three_ptr)] +fn add_three(add_three_ptr: &mut u32) { + *add_three_ptr += 1; + add_two(add_three_ptr); +} + +#[kani::ensures(|result| old(*add_two_ptr + 1) == *add_two_ptr)] // incorrect -- should be old(*add_two_ptr + 1) +fn add_two(add_two_ptr: &mut u32) { + *add_two_ptr += 1; + add_one(add_two_ptr) +} + +#[kani::requires(*add_one_ptr < 102)] +#[kani::modifies(add_one_ptr)] +#[kani::ensures(|result| old(*add_one_ptr + 1) == *add_one_ptr)] // correct -- assertion should always succeed +fn add_one(add_one_ptr: &mut u32) { + *add_one_ptr += 1; +} + +// -Zcontracts-as-assertions introduces this failure; without it, add_two's and add_one's contracts are ignored. +#[kani::proof_for_contract(add_three)] +fn prove_add_three() { + let mut i = kani::any(); + add_three(&mut i); +} diff --git a/tests/expected/function-contract/as-assertions/assert-preconditions.expected b/tests/expected/function-contract/as-assertions/assert-preconditions.expected new file mode 100644 index 000000000000..3d496f83c925 --- /dev/null +++ b/tests/expected/function-contract/as-assertions/assert-preconditions.expected @@ -0,0 +1,21 @@ +assertion\ + - Status: SUCCESS\ + - Description: "*ptr < 100"\ + +assertion\ + - Status: FAILURE\ + - Description: "*ptr == 1" + +assertion\ + - Status: FAILURE\ + - Description: "*ptr < 100" + +assertion\ + - Status: FAILURE\ + - Description: "*ptr == 1" + +Summary: +Verification failed for - should_fail::prove_add_three_contract +Verification failed for - should_fail::prove_add_one +Verification failed for - should_fail::prove_add_three +Complete - 1 successfully verified harnesses, 3 failures, 4 total. diff --git a/tests/expected/function-contract/as-assertions/assert-preconditions.rs b/tests/expected/function-contract/as-assertions/assert-preconditions.rs new file mode 100644 index 000000000000..6bd0f47c6be8 --- /dev/null +++ b/tests/expected/function-contract/as-assertions/assert-preconditions.rs @@ -0,0 +1,64 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts -Zcontracts-as-assertions + +// Test -Zcontracts-as-assertions for preconditions. + +#[kani::requires(*ptr < 100)] +#[kani::ensures(|result| old(*ptr + 3) == *ptr)] +#[kani::modifies(ptr)] +fn add_three(ptr: &mut u32) { + *ptr += 1; + add_two(ptr); +} + +#[kani::requires(*ptr < 101)] +#[kani::ensures(|result| old(*ptr + 2) == *ptr)] +fn add_two(ptr: &mut u32) { + *ptr += 1; + add_one(ptr); +} + +#[kani::requires(*ptr == 1)] +#[kani::modifies(ptr)] +fn add_one(ptr: &mut u32) { + *ptr += 1; +} + +mod should_fail { + use crate::*; + + // add_three and add_one's preconditions are asserted, causing failure. + #[kani::proof] + fn prove_add_three() { + let mut i = kani::any(); + add_three(&mut i); + } + + // add_three's precondition is asserted, causing failure. + #[kani::proof_for_contract(add_one)] + fn prove_add_one() { + let mut i = kani::any(); + add_three(&mut i); + } + + // Since add_three is the target of the proof_for_contract, its precondition gets assumed. + // However, add_one's precondition is still asserted, causing failure. + #[kani::proof_for_contract(add_three)] + fn prove_add_three_contract() { + let mut i = kani::any(); + add_three(&mut i); + } +} + +mod should_pass { + use crate::*; + // Same as should_fail::prove_add_one, with the added assumption of add_three's precondition. + // Note that add_one's precondition gets assumed since it's the target of the proof_for_contract. + #[kani::proof_for_contract(add_one)] + fn prove_add_one() { + let mut i = kani::any(); + kani::assume(i < 100); + add_three(&mut i); + } +} diff --git a/tests/expected/function-contract/as-assertions/precedence.expected b/tests/expected/function-contract/as-assertions/precedence.expected new file mode 100644 index 000000000000..16fcc8fa1c75 --- /dev/null +++ b/tests/expected/function-contract/as-assertions/precedence.expected @@ -0,0 +1,13 @@ +assertion\ + - Status: UNREACHABLE\ + - Description: "*add_one_ptr == 1" + +assertion\ + - Status: UNREACHABLE\ + - Description: "|result| old(*add_one_ptr + 1) == *add_one_ptr" + +assertion\ + - Status: UNREACHABLE\ + - Description: "|result| old(*add_one_ptr + 1) == *add_one_ptr" + +Complete - 2 successfully verified harnesses, 0 failures, 2 total. diff --git a/tests/expected/function-contract/as-assertions/precedence.rs b/tests/expected/function-contract/as-assertions/precedence.rs new file mode 100644 index 000000000000..06af70eaa372 --- /dev/null +++ b/tests/expected/function-contract/as-assertions/precedence.rs @@ -0,0 +1,48 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts -Zcontracts-as-assertions + +// If a function is the target of a proof_for_contract or stub_verified, we should defer to the contract handling for those modes. +// i.e., test that -Zcontracts-as-assertions does not override the contract handling for proof_for_contract and stub_verified. + +#[kani::modifies(add_three_ptr)] +#[kani::requires(*add_three_ptr < 100)] +fn add_three(add_three_ptr: &mut u32) { + *add_three_ptr += 1; + add_two(add_three_ptr); +} + +#[kani::requires(*add_two_ptr < 101)] +#[kani::ensures(|result| old(*add_two_ptr + 2) == *add_two_ptr)] +fn add_two(add_two_ptr: &mut u32) { + *add_two_ptr += 1; + add_one(add_two_ptr); +} + +#[kani::modifies(add_one_ptr)] +#[kani::requires(*add_one_ptr == 1)] +#[kani::ensures(|result| old(*add_one_ptr + 1) == *add_one_ptr)] +fn add_one(add_one_ptr: &mut u32) { + *add_one_ptr += 1; +} + +// Test that proof_for_contract takes precedence over the assert mode, i.e. +// that the target of the proof for contract still has its preconditions assumed. +#[kani::proof_for_contract(add_one)] +fn proof_for_contract_takes_precedence() { + let mut i = kani::any(); + // if add_one's precondition was asserted, verification would fail, + // but since it's assumed, we get a vacuously successful proof instead. + kani::assume(i == 2); + add_one(&mut i); +} + +// Test that stub_verified takes precedence over the assert mode. +// Verification should succeed because we stub add_two by its contract, +// meaning we never reach add_one's contract. +#[kani::proof_for_contract(add_three)] +#[kani::stub_verified(add_two)] +fn stub_verified_takes_precedence() { + let mut i = kani::any(); + add_three(&mut i); +} From 979ecb0e963af6e2d90b7d8004c3997a20d6deed Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 30 Dec 2024 16:27:18 -0500 Subject: [PATCH 20/24] documentation --- .../src/kani_middle/transform/contracts.rs | 4 +++- kani_metadata/src/unstable.rs | 2 +- .../kani_macros/src/sysroot/contracts/mod.rs | 23 ++++++++++++++++++- 3 files changed, 26 insertions(+), 3 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs index 5df3c999edad..d9b5016267ad 100644 --- a/kani-compiler/src/kani_middle/transform/contracts.rs +++ b/kani-compiler/src/kani_middle/transform/contracts.rs @@ -446,7 +446,9 @@ impl FunctionWithContractPass { } /// Return which contract mode to use for this function if any. - /// TODO document precedence + /// Note that the Check and Replace modes take precedence over the Assert mode. + /// This precedence ensures that a given `target` of a proof_for_contract(target) or stub_verified(target) + /// use their Check or Replace closures, respectively, rather than the Assert closure. fn contract_mode(&self, tcx: TyCtxt, fn_def: FnDef) -> Option { let kani_attributes = KaniAttributes::for_def_id(tcx, fn_def.def_id()); kani_attributes.has_contract().then(|| { diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs index 3d260085e8c2..a791ca5dca60 100644 --- a/kani_metadata/src/unstable.rs +++ b/kani_metadata/src/unstable.rs @@ -85,7 +85,7 @@ pub enum UnstableFeature { FunctionContracts, /// Enable loop contracts [RFC 12](https://model-checking.github.io/kani/rfc/rfcs/0012-loop-contracts.html) LoopContracts, - /// Enable function contracts to be interpreted as assertions. (Requires function-contracts option). + /// Interpret function contracts as assertions. (Requires function-contracts option). ContractsAsAssertions, /// Memory predicate APIs. MemPredicates, diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index ad8fef125c61..7bb2ec9100ec 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -116,6 +116,27 @@ //! //! We register this closure as `#[kanitool::recursion_check = "__kani_recursion_..."]`. //! +//! ## Assert closure +//! Kani has an option to interpret contracts as assertions. +//! To support that option, we generate a closure that asserts preconditions and postconditions. +//! This option is especially useful for verifying that a function does not violate the contracts of its dependencies. +//! For example: +//! ```ignore +//! #[kani::requires(x >= 0)] +//! fn foo(x: i32) { +//! bar(x); +//! } +//! +//! #[kani::requires(x > 0)] +//! fn bar(x: i32) {...} +//! ``` +//! If we call foo(0), we would satisfy the check closure, since we satisfy foo's precondition. +//! However, we would violate bar()'s precondition that x > 0. +//! By using bar's assert closure instead of its original body, we can assert that callers of bar() respect its contract +//! and catch this issue. +//! +//! We register this closure as `#[kanitool::asserted_with = "__kani_assert_..."]` +//! //! # Complete example //! //! ``` @@ -557,7 +578,7 @@ enum ContractConditionsData { } /// Enumeration that stores (some of) the contract mode values. -/// We elide the Original and RecursiveCheck variants because we don't need them for any work in this module. +/// We elide the Original and RecursiveCheck variants because we don't need them for any work in this crate. #[derive(Copy, Clone, Debug, PartialEq, Eq)] enum ContractMode { SimpleCheck, From ba4a108f6db80e7415af000e7da3f2b1deabdb6b Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 30 Dec 2024 16:30:44 -0500 Subject: [PATCH 21/24] tweak comment --- kani-compiler/src/kani_middle/attributes.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 32f83f241e8c..64763a08241b 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -44,8 +44,8 @@ enum KaniAttributeKind { /// contract, e.g. the contract check is substituted for the target function /// before the the verification runs. ProofForContract, - /// Internal attribute of the contracts implementation that identifies the - /// code implementing the function with the contract clauses as assertions. + /// Internal attribute of the contracts implementation. Identifies the + /// code implementing the function with its contract clauses asserted. AssertedWith, /// Attribute on a function with a contract that identifies the code /// implementing the check for this contract. From e8c9311986b6aeb8a5e09779e2b4578151924199 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 30 Dec 2024 16:39:45 -0500 Subject: [PATCH 22/24] doc nits --- library/kani_macros/src/sysroot/contracts/mod.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index 7bb2ec9100ec..4dd7d504f39a 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -128,11 +128,11 @@ //! } //! //! #[kani::requires(x > 0)] -//! fn bar(x: i32) {...} +//! fn bar(x: i32) { } //! ``` //! If we call foo(0), we would satisfy the check closure, since we satisfy foo's precondition. -//! However, we would violate bar()'s precondition that x > 0. -//! By using bar's assert closure instead of its original body, we can assert that callers of bar() respect its contract +//! However, we would violate bar's precondition that x > 0. +//! By using bar's assert closure instead of its original body, we can assert that callers of bar respect its contract //! and catch this issue. //! //! We register this closure as `#[kanitool::asserted_with = "__kani_assert_..."]` From c4e2090f4db6d068403674c6ab956c41be089ec0 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 31 Dec 2024 11:04:28 -0500 Subject: [PATCH 23/24] try splitting & simplifying tests to reduce runner load --- .../as-assertions/assert-postconditions.rs | 2 - ...ted => assert-preconditions-fail.expected} | 8 +--- ...itions.rs => assert-preconditions-fail.rs} | 20 ---------- .../assert-preconditions-pass.expected | 0 .../assert-preconditions-pass.rs | 39 +++++++++++++++++++ 5 files changed, 40 insertions(+), 29 deletions(-) rename tests/expected/function-contract/as-assertions/{assert-preconditions.expected => assert-preconditions-fail.expected} (55%) rename tests/expected/function-contract/as-assertions/{assert-preconditions.rs => assert-preconditions-fail.rs} (58%) create mode 100644 tests/expected/function-contract/as-assertions/assert-preconditions-pass.expected create mode 100644 tests/expected/function-contract/as-assertions/assert-preconditions-pass.rs diff --git a/tests/expected/function-contract/as-assertions/assert-postconditions.rs b/tests/expected/function-contract/as-assertions/assert-postconditions.rs index fb6a0dbcc849..bb6fdda41dd3 100644 --- a/tests/expected/function-contract/as-assertions/assert-postconditions.rs +++ b/tests/expected/function-contract/as-assertions/assert-postconditions.rs @@ -17,8 +17,6 @@ fn add_two(add_two_ptr: &mut u32) { add_one(add_two_ptr) } -#[kani::requires(*add_one_ptr < 102)] -#[kani::modifies(add_one_ptr)] #[kani::ensures(|result| old(*add_one_ptr + 1) == *add_one_ptr)] // correct -- assertion should always succeed fn add_one(add_one_ptr: &mut u32) { *add_one_ptr += 1; diff --git a/tests/expected/function-contract/as-assertions/assert-preconditions.expected b/tests/expected/function-contract/as-assertions/assert-preconditions-fail.expected similarity index 55% rename from tests/expected/function-contract/as-assertions/assert-preconditions.expected rename to tests/expected/function-contract/as-assertions/assert-preconditions-fail.expected index 3d496f83c925..744c8d8090d8 100644 --- a/tests/expected/function-contract/as-assertions/assert-preconditions.expected +++ b/tests/expected/function-contract/as-assertions/assert-preconditions-fail.expected @@ -1,10 +1,6 @@ -assertion\ - - Status: SUCCESS\ - - Description: "*ptr < 100"\ - assertion\ - Status: FAILURE\ - - Description: "*ptr == 1" + - Description: "*ptr < 100" assertion\ - Status: FAILURE\ @@ -15,7 +11,5 @@ assertion\ - Description: "*ptr == 1" Summary: -Verification failed for - should_fail::prove_add_three_contract Verification failed for - should_fail::prove_add_one Verification failed for - should_fail::prove_add_three -Complete - 1 successfully verified harnesses, 3 failures, 4 total. diff --git a/tests/expected/function-contract/as-assertions/assert-preconditions.rs b/tests/expected/function-contract/as-assertions/assert-preconditions-fail.rs similarity index 58% rename from tests/expected/function-contract/as-assertions/assert-preconditions.rs rename to tests/expected/function-contract/as-assertions/assert-preconditions-fail.rs index 6bd0f47c6be8..715a09d66e56 100644 --- a/tests/expected/function-contract/as-assertions/assert-preconditions.rs +++ b/tests/expected/function-contract/as-assertions/assert-preconditions-fail.rs @@ -41,24 +41,4 @@ mod should_fail { let mut i = kani::any(); add_three(&mut i); } - - // Since add_three is the target of the proof_for_contract, its precondition gets assumed. - // However, add_one's precondition is still asserted, causing failure. - #[kani::proof_for_contract(add_three)] - fn prove_add_three_contract() { - let mut i = kani::any(); - add_three(&mut i); - } -} - -mod should_pass { - use crate::*; - // Same as should_fail::prove_add_one, with the added assumption of add_three's precondition. - // Note that add_one's precondition gets assumed since it's the target of the proof_for_contract. - #[kani::proof_for_contract(add_one)] - fn prove_add_one() { - let mut i = kani::any(); - kani::assume(i < 100); - add_three(&mut i); - } } diff --git a/tests/expected/function-contract/as-assertions/assert-preconditions-pass.expected b/tests/expected/function-contract/as-assertions/assert-preconditions-pass.expected new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/tests/expected/function-contract/as-assertions/assert-preconditions-pass.rs b/tests/expected/function-contract/as-assertions/assert-preconditions-pass.rs new file mode 100644 index 000000000000..df0757a5a897 --- /dev/null +++ b/tests/expected/function-contract/as-assertions/assert-preconditions-pass.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts -Zcontracts-as-assertions + +// Test -Zcontracts-as-assertions for preconditions. + +#[kani::requires(*ptr < 100)] +#[kani::ensures(|result| old(*ptr + 3) == *ptr)] +#[kani::modifies(ptr)] +fn add_three(ptr: &mut u32) { + *ptr += 1; + add_two(ptr); +} + +#[kani::requires(*ptr < 101)] +#[kani::ensures(|result| old(*ptr + 2) == *ptr)] +fn add_two(ptr: &mut u32) { + *ptr += 1; + add_one(ptr); +} + +#[kani::requires(*ptr == 1)] +#[kani::modifies(ptr)] +fn add_one(ptr: &mut u32) { + *ptr += 1; +} + + +mod should_pass { + use crate::*; + // Same as should_fail::prove_add_one, with the added assumption of add_three's precondition. + // Note that add_one's precondition gets assumed since it's the target of the proof_for_contract. + #[kani::proof_for_contract(add_one)] + fn prove_add_one() { + let mut i = kani::any(); + kani::assume(i < 100); + add_three(&mut i); + } +} From 15ee0a6ca6fb405f8d3e67bf554412ec5423a2e8 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 31 Dec 2024 11:06:29 -0500 Subject: [PATCH 24/24] format --- .../function-contract/as-assertions/assert-preconditions-pass.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/expected/function-contract/as-assertions/assert-preconditions-pass.rs b/tests/expected/function-contract/as-assertions/assert-preconditions-pass.rs index df0757a5a897..2c1cd2b3df75 100644 --- a/tests/expected/function-contract/as-assertions/assert-preconditions-pass.rs +++ b/tests/expected/function-contract/as-assertions/assert-preconditions-pass.rs @@ -25,7 +25,6 @@ fn add_one(ptr: &mut u32) { *ptr += 1; } - mod should_pass { use crate::*; // Same as should_fail::prove_add_one, with the added assumption of add_three's precondition.