From 8398771cf598e842d963ff319cec90544166a8dd Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 13 Dec 2024 16:31:22 +0100 Subject: [PATCH 01/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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/20] 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 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 14/20] 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 b34ed134e27a5f55a19a7c05ef872c44a0b08b7d Mon Sep 17 00:00:00 2001 From: "Shoyu Vanilla (Flint)" Date: Fri, 3 Jan 2025 03:27:20 +0900 Subject: [PATCH 15/20] fix: clippy (#3806) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../src/irep/goto_binary_serde.rs | 22 +++++++++---------- cprover_bindings/src/utils.rs | 1 + kani_metadata/src/artifact.rs | 4 ++-- library/kani/src/models/mod.rs | 5 ++--- 4 files changed, 16 insertions(+), 16 deletions(-) diff --git a/cprover_bindings/src/irep/goto_binary_serde.rs b/cprover_bindings/src/irep/goto_binary_serde.rs index c1b901ddd5c8..15cc0afa8902 100644 --- a/cprover_bindings/src/irep/goto_binary_serde.rs +++ b/cprover_bindings/src/irep/goto_binary_serde.rs @@ -936,9 +936,9 @@ where } } -//////////////////////////////////////// -//// Dynamic memory usage computation -//////////////////////////////////////// +// ================================== +// Dynamic memory usage computation +// ================================== #[cfg(test)] mod sharing_stats { @@ -1032,7 +1032,7 @@ mod sharing_stats { } } - impl<'a, W> DynamicUsage for GotoBinarySerializer<'a, W> + impl DynamicUsage for GotoBinarySerializer<'_, W> where W: Write, { @@ -1127,9 +1127,9 @@ mod sharing_stats { max_count = *count; max_id = Some(id); }; - nof_unique = nof_unique + 1; + nof_unique += 1; let incr = (*count as f64 - avg_count) / (nof_unique as f64); - avg_count = avg_count + incr; + avg_count += incr; } SharingStats { _nof_unique: nof_unique, @@ -1156,7 +1156,7 @@ mod sharing_stats { } impl GotoBinarySharingStats { - fn from_serializer<'a, W: Write>(s: &GotoBinarySerializer<'a, W>) -> Self { + fn from_serializer(s: &GotoBinarySerializer<'_, W>) -> Self { GotoBinarySharingStats { _allocated_bytes: s.dynamic_usage(), _string_stats: SharingStats::new(&s.string_count), @@ -1173,7 +1173,7 @@ mod sharing_stats { } } - impl<'a, W> GotoBinarySerializer<'a, W> + impl GotoBinarySerializer<'_, W> where W: Write, { @@ -1277,13 +1277,13 @@ mod tests { let mut writer = BufWriter::new(&mut vec); let mut serializer = GotoBinarySerializer::new(&mut writer); - for u in std::u8::MIN..std::u8::MAX { + for u in u8::MIN..u8::MAX { serializer.write_u8(u); } } // read back from byte stream - for u in std::u8::MIN..std::u8::MAX { + for u in u8::MIN..u8::MAX { assert_eq!(vec[u as usize], u); } } @@ -1352,7 +1352,7 @@ mod tests { let foo = String::from("foo").intern(); let bar = String::from("bar").intern(); let baz = String::from("baz").intern(); - let strings = vec![foo, bar, foo, bar, foo, baz, baz, bar, foo]; + let strings = [foo, bar, foo, bar, foo, baz, baz, bar, foo]; let mut vec: Vec = Vec::new(); diff --git a/cprover_bindings/src/utils.rs b/cprover_bindings/src/utils.rs index 4a323277ec9e..e161fb886a22 100644 --- a/cprover_bindings/src/utils.rs +++ b/cprover_bindings/src/utils.rs @@ -106,6 +106,7 @@ mod tests { use num::BigInt; #[test] + #[allow(clippy::bool_assert_comparison)] fn test_fits_in_bits() { assert_eq!(BigInt::from(10).fits_in_bits(3, false), false); assert_eq!(BigInt::from(10).fits_in_bits(4, false), true); diff --git a/kani_metadata/src/artifact.rs b/kani_metadata/src/artifact.rs index 12f8f9a49566..dbb41a213bc8 100644 --- a/kani_metadata/src/artifact.rs +++ b/kani_metadata/src/artifact.rs @@ -99,7 +99,7 @@ mod test { #[test] fn test_convert_ok() { - let path = PathBuf::from("/tmp/my_file.rs").with_extension(&SymTabGoto); + let path = PathBuf::from("/tmp/my_file.rs").with_extension(SymTabGoto); let goto = convert_type(&path, SymTabGoto, Goto); assert_eq!(goto.as_os_str(), "/tmp/my_file.out"); @@ -109,7 +109,7 @@ mod test { #[test] fn test_set_extension_ok() { - let path = PathBuf::from("/tmp/my_file.rs").with_extension(&SymTabGoto); + let path = PathBuf::from("/tmp/my_file.rs").with_extension(SymTabGoto); assert_eq!(path.as_os_str(), "/tmp/my_file.symtab.out"); } } diff --git a/library/kani/src/models/mod.rs b/library/kani/src/models/mod.rs index 2081ddf639df..af5ac336e09e 100644 --- a/library/kani/src/models/mod.rs +++ b/library/kani/src/models/mod.rs @@ -191,7 +191,7 @@ mod test { u64: From, { assert_eq!( - unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, M, E, LANES>(mask.clone())) }, + unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, M, E, LANES>(mask)) }, mask.to_bitmask() ); } @@ -220,8 +220,7 @@ mod test { let bitmask = mask.to_bitmask(); assert_eq!(bitmask, 0b1010); - let kani_mask = - unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask.clone())) }; + let kani_mask = unsafe { u64::from(kani_intrinsic::simd_bitmask::<_, u8, u32, 4>(mask)) }; assert_eq!(kani_mask, bitmask); } } From 555d52c20732f1c2585c0f28996387f812062cda Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9mi=20Delmas?= Date: Thu, 2 Jan 2025 14:56:43 -0500 Subject: [PATCH 16/20] Update dependencies (02.01.2025). (#3809) 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 --- Cargo.lock | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 2d7e93794faf..5724746ca638 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -160,9 +160,9 @@ dependencies = [ [[package]] name = "bstr" -version = "1.11.1" +version = "1.11.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "786a307d683a5bf92e6fd5fd69a7eb613751668d1d8d67d802846dfe367c62c8" +checksum = "c94feba04f99cbce6558bbe1c18e38692a056981cb66c96f0878c2452aa28023" dependencies = [ "memchr", "regex-automata 0.4.9", @@ -307,7 +307,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.93", + "syn 2.0.94", ] [[package]] @@ -785,7 +785,7 @@ dependencies = [ "shell-words", "strum", "strum_macros", - "syn 2.0.93", + "syn 2.0.94", "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.93", + "syn 2.0.94", ] [[package]] @@ -924,7 +924,7 @@ version = "0.1.0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.93", + "syn 2.0.94", ] [[package]] @@ -1252,7 +1252,7 @@ dependencies = [ "proc-macro-error-attr2", "proc-macro2", "quote", - "syn 2.0.93", + "syn 2.0.94", ] [[package]] @@ -1497,7 +1497,7 @@ checksum = "5a9bf7cf98d04a2b28aead066b7496853d4779c9cc183c440dbac457641e19a0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.93", + "syn 2.0.94", ] [[package]] @@ -1648,7 +1648,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.93", + "syn 2.0.94", ] [[package]] @@ -1664,9 +1664,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.93" +version = "2.0.94" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c786062daee0d6db1132800e623df74274a0a87322d8e183338e01b3d98d058" +checksum = "987bc0be1cdea8b10216bd06e2ca407d40b9543468fafd3ddfb02f36e77f71f3" dependencies = [ "proc-macro2", "quote", @@ -1724,7 +1724,7 @@ checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" dependencies = [ "proc-macro2", "quote", - "syn 2.0.93", + "syn 2.0.94", ] [[package]] @@ -1735,7 +1735,7 @@ checksum = "7b50fa271071aae2e6ee85f842e2e28ba8cd2c5fb67f11fcb1fd70b276f9e7d4" dependencies = [ "proc-macro2", "quote", - "syn 2.0.93", + "syn 2.0.94", ] [[package]] @@ -1858,7 +1858,7 @@ checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d" dependencies = [ "proc-macro2", "quote", - "syn 2.0.93", + "syn 2.0.94", ] [[package]] @@ -2185,9 +2185,9 @@ checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" [[package]] name = "winnow" -version = "0.6.20" +version = "0.6.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "36c1fec1a2bb5866f07c25f68c26e565c4c200aebb96d7e55710c19d3e8ac49b" +checksum = "e6f5bb5257f2407a5425c6e749bfd9692192a73e70a6060516ac04f889087d68" dependencies = [ "memchr", ] @@ -2216,5 +2216,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.93", + "syn 2.0.94", ] From 91a41ea6bd6875212a19bfeaf1fc9bb3e7ecbc8e Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Thu, 2 Jan 2025 20:55:47 -0500 Subject: [PATCH 17/20] Update charon submodule (#3801) Update Charon submodule to https://github.com/AeneasVerif/charon/commit/adc0a855aa1428d68e4270edef0d52131cef06ab Relevant Charon PRs: https://github.com/AeneasVerif/charon/pull/457: This required updating the code that creates places to also pass in the type. https://github.com/AeneasVerif/charon/pull/464: This replaced the file-to-id hash table by a vector, thus requiring that we add one in Kani's translation context. https://github.com/AeneasVerif/charon/pull/474: The translation context is no longer parameterized by a lifetime https://github.com/AeneasVerif/charon/pull/491: This required changing the type of indices 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: thanhnguyen-aws --- Cargo.lock | 194 ++++++++---------- charon | 2 +- .../codegen_aeneas_llbc/compiler_interface.rs | 13 +- .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs | 95 +++++---- 4 files changed, 146 insertions(+), 158 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 5724746ca638..e8cdaf3e2a3f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -39,6 +39,16 @@ dependencies = [ "memchr", ] +[[package]] +name = "annotate-snippets" +version = "0.11.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "710e8eae58854cdc1790fcb56cca04d712a17be849eeb81da2a724bf4bae2bc4" +dependencies = [ + "anstyle", + "unicode-width 0.2.0", +] + [[package]] name = "anstream" version = "0.6.18" @@ -94,12 +104,6 @@ version = "1.0.95" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "34ac096ce696dc2fcabef30516bb13c0a68a11d30131d3df6f04711467681b04" -[[package]] -name = "arrayvec" -version = "0.5.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "23b62fc65de8e4e7f52534fb52b0f3ed04746ae267519eef2a83941e8085068b" - [[package]] name = "arrayvec" version = "0.7.6" @@ -155,7 +159,7 @@ version = "3.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c5839ee4f953e811bfdcf223f509cb2c6a3e1447959b0bff459405575bc17f22" dependencies = [ - "arrayvec 0.7.6", + "arrayvec", ] [[package]] @@ -176,7 +180,7 @@ dependencies = [ "anyhow", "cargo_metadata", "clap", - "which 7.0.1", + "which", ] [[package]] @@ -240,28 +244,27 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "charon" -version = "0.1.45" +version = "0.1.58" dependencies = [ + "annotate-snippets", + "anstream", "anyhow", "assert_cmd", "clap", "colored", - "convert_case 0.6.0", - "derive-visitor", + "convert_case", + "derive_generic_visitor", "env_logger", "hashlink", "index_vec", "indoc", - "itertools 0.13.0", + "itertools", "lazy_static", "log", "macros", "nom", "nom-supreme", "petgraph", - "pretty", - "regex", - "rustc_apfloat", "rustc_version", "serde", "serde-map-to-array", @@ -273,7 +276,7 @@ dependencies = [ "tracing", "tracing-subscriber", "tracing-tree 0.4.0 (git+https://github.com/Nadrieril/tracing-tree)", - "which 6.0.3", + "which", ] [[package]] @@ -307,7 +310,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.94", + "syn", ] [[package]] @@ -383,12 +386,6 @@ dependencies = [ "windows-sys 0.59.0", ] -[[package]] -name = "convert_case" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6245d59a3e82a7fc217c5828a6692dbc6dfb63a0c8c90495621f7b9d79704a0e" - [[package]] name = "convert_case" version = "0.6.0" @@ -481,6 +478,41 @@ dependencies = [ "memchr", ] +[[package]] +name = "darling" +version = "0.20.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f63b86c8a8826a49b8c21f08a2d07338eec8d900540f8630dc76284be802989" +dependencies = [ + "darling_core", + "darling_macro", +] + +[[package]] +name = "darling_core" +version = "0.20.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "95133861a8032aaea082871032f5815eb9e98cef03fa916ab4500513994df9e5" +dependencies = [ + "fnv", + "ident_case", + "proc-macro2", + "quote", + "strsim", + "syn", +] + +[[package]] +name = "darling_macro" +version = "0.20.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d336a2a514f6ccccaa3e09b02d41d35330c07ddf03a62165fcec10bb561c7806" +dependencies = [ + "darling_core", + "quote", + "syn", +] + [[package]] name = "deranged" version = "0.3.11" @@ -491,25 +523,26 @@ dependencies = [ ] [[package]] -name = "derive-visitor" -version = "0.4.0" +name = "derive_generic_visitor" +version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d47165df83b9707cbada3216607a5d66125b6a66906de0bc1216c0669767ca9e" +checksum = "b3e1c241e4f464b614bd7650f1a7c4c0e20e5ef21564d6b916b4c51fd76f7688" dependencies = [ - "derive-visitor-macros", + "derive_generic_visitor_macros", ] [[package]] -name = "derive-visitor-macros" -version = "0.4.0" +name = "derive_generic_visitor_macros" +version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "427b39a85fecafea16b1a5f3f50437151022e35eb4fe038107f08adbf7f8def6" +checksum = "885f5274163b5b1720591c0c24b34350a0b05e4774351f9fb3d13c192d8c995b" dependencies = [ - "convert_case 0.4.0", - "itertools 0.10.5", + "convert_case", + "darling", + "itertools", "proc-macro2", "quote", - "syn 1.0.109", + "syn", ] [[package]] @@ -593,6 +626,12 @@ version = "0.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0ce7134b9999ecaf8bcd65542e436736ef32ddca1b3e06094cb6ec5755203b80" +[[package]] +name = "fnv" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" + [[package]] name = "foldhash" version = "0.1.4" @@ -691,6 +730,12 @@ version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" +[[package]] +name = "ident_case" +version = "1.0.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b9e0384b61958566e926dc50660321d12159025e767c18e043daf26b70104c39" + [[package]] name = "indent_write" version = "2.2.0" @@ -728,15 +773,6 @@ version = "1.70.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" -[[package]] -name = "itertools" -version = "0.10.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b0fd2260e829bddf4cb6ea802289de2f86d6a7a690192fbe91b3f46e0f2c8473" -dependencies = [ - "either", -] - [[package]] name = "itertools" version = "0.13.0" @@ -774,7 +810,7 @@ dependencies = [ "clap", "cprover_bindings", "home", - "itertools 0.13.0", + "itertools", "kani_metadata", "lazy_static", "num", @@ -785,7 +821,7 @@ dependencies = [ "shell-words", "strum", "strum_macros", - "syn 2.0.94", + "syn", "tracing", "tracing-subscriber", "tracing-tree 0.4.0 (registry+https://github.com/rust-lang/crates.io-index)", @@ -834,7 +870,7 @@ dependencies = [ "toml", "tracing", "tracing-subscriber", - "which 7.0.1", + "which", ] [[package]] @@ -860,7 +896,7 @@ dependencies = [ "proc-macro-error2", "proc-macro2", "quote", - "syn 2.0.94", + "syn", ] [[package]] @@ -924,7 +960,7 @@ version = "0.1.0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.94", + "syn", ] [[package]] @@ -1222,17 +1258,6 @@ dependencies = [ "termtree", ] -[[package]] -name = "pretty" -version = "0.12.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b55c4d17d994b637e2f4daf6e5dc5d660d209d5642377d675d7a1c3ab69fa579" -dependencies = [ - "arrayvec 0.5.2", - "typed-arena", - "unicode-width 0.1.14", -] - [[package]] name = "proc-macro-error-attr2" version = "2.0.0" @@ -1252,7 +1277,7 @@ dependencies = [ "proc-macro-error-attr2", "proc-macro2", "quote", - "syn 2.0.94", + "syn", ] [[package]] @@ -1391,16 +1416,6 @@ version = "0.1.24" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "719b953e2095829ee67db738b3bfa9fa368c94900df327b3f07fe6e794d2fe1f" -[[package]] -name = "rustc_apfloat" -version = "0.2.2+llvm-462a31f5a5ab" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "121e2195ff969977a4e2b5c9965ea867fce7e4cb5aee5b09dee698a7932d574f" -dependencies = [ - "bitflags", - "smallvec", -] - [[package]] name = "rustc_version" version = "0.4.1" @@ -1497,7 +1512,7 @@ checksum = "5a9bf7cf98d04a2b28aead066b7496853d4779c9cc183c440dbac457641e19a0" dependencies = [ "proc-macro2", "quote", - "syn 2.0.94", + "syn", ] [[package]] @@ -1648,18 +1663,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.94", -] - -[[package]] -name = "syn" -version = "1.0.109" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", + "syn", ] [[package]] @@ -1724,7 +1728,7 @@ checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" dependencies = [ "proc-macro2", "quote", - "syn 2.0.94", + "syn", ] [[package]] @@ -1735,7 +1739,7 @@ checksum = "7b50fa271071aae2e6ee85f842e2e28ba8cd2c5fb67f11fcb1fd70b276f9e7d4" dependencies = [ "proc-macro2", "quote", - "syn 2.0.94", + "syn", ] [[package]] @@ -1858,7 +1862,7 @@ checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d" dependencies = [ "proc-macro2", "quote", - "syn 2.0.94", + "syn", ] [[package]] @@ -1967,12 +1971,6 @@ dependencies = [ "tree-sitter-language", ] -[[package]] -name = "typed-arena" -version = "2.0.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6af6ae20167a9ece4bcb41af5b80f8a1f1df981f6391189ce00fd257af04126a" - [[package]] name = "unicode-ident" version = "1.0.14" @@ -2046,18 +2044,6 @@ version = "0.11.0+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" -[[package]] -name = "which" -version = "6.0.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4ee928febd44d98f2f459a4a79bd4d928591333a494a10a868418ac1b39cf1f" -dependencies = [ - "either", - "home", - "rustix", - "winsafe", -] - [[package]] name = "which" version = "7.0.1" @@ -2216,5 +2202,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.94", + "syn", ] diff --git a/charon b/charon index 454078ebdb4a..adc0a855aa14 160000 --- a/charon +++ b/charon @@ -1 +1 @@ -Subproject commit 454078ebdb4a607e2b21dc115e1ca99b516e436f +Subproject commit adc0a855aa1428d68e4270edef0d52131cef06ab diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 5a5f02969b01..ddc6f6264d1e 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -38,7 +38,6 @@ use rustc_smir::rustc_internal; use stable_mir::mir::mono::{Instance, MonoItem}; use stable_mir::{CrateDef, DefId}; use std::any::Any; -use std::collections::{HashMap, HashSet}; use std::fs::File; use std::path::Path; use std::sync::{Arc, Mutex}; @@ -394,16 +393,6 @@ fn create_charon_transformation_context(tcx: TyCtxt) -> TransformCtx { }; let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into(); let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() }; - let errors = ErrorCtx { - continue_on_failure: true, - error_on_warnings: false, - dcx: &(), - external_decls_with_errors: HashSet::new(), - ignored_failed_decls: HashSet::new(), - external_dep_sources: HashMap::new(), - def_id: None, - def_id_is_local: true, - error_count: 0, - }; + let errors = ErrorCtx::new(true, false); TransformCtx { options, translated, errors } } diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs index 24cb007be0b8..1664867b087d 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs @@ -6,12 +6,11 @@ //! This module contains a context for translating stable MIR into Charon's //! unstructured low-level borrow calculus (ULLBC) +use charon_lib::ast::krate::TypeDeclId as CharonTypeDeclId; use charon_lib::ast::meta::{ AttrInfo as CharonAttrInfo, Loc as CharonLoc, RawSpan as CharonRawSpan, }; -use charon_lib::ast::types::{ - Ty as CharonTy, TyKind as CharonTyKind, TypeDeclId as CharonTypeDeclId, -}; +use charon_lib::ast::types::{Ty as CharonTy, TyKind as CharonTyKind}; use charon_lib::ast::{ AbortKind as CharonAbortKind, AggregateKind as CharonAggregateKind, AnyTransId as CharonAnyTransId, Assert as CharonAssert, BinOp as CharonBinOp, @@ -19,21 +18,23 @@ use charon_lib::ast::{ BuiltinTy as CharonBuiltinTy, Call as CharonCall, CastKind as CharonCastKind, ConstGeneric as CharonConstGeneric, ConstGenericVar as CharonConstGenericVar, ConstGenericVarId as CharonConstGenericVarId, ConstantExpr as CharonConstantExpr, - Disambiguator as CharonDisambiguator, Field as CharonField, FieldId as CharonFieldId, - FieldProjKind as CharonFieldProjKind, FileName as CharonFileName, FnOperand as CharonFnOperand, + DeBruijnVar as CharonDeBruijnVar, Disambiguator as CharonDisambiguator, Field as CharonField, + FieldId as CharonFieldId, FieldProjKind as CharonFieldProjKind, File as CharonFile, + FileId as CharonFileId, FileName as CharonFileName, FnOperand as CharonFnOperand, FnPtr as CharonFnPtr, FunDecl as CharonFunDecl, FunDeclId as CharonFunDeclId, FunId as CharonFunId, FunIdOrTraitMethodRef as CharonFunIdOrTraitMethodRef, FunSig as CharonFunSig, GenericArgs as CharonGenericArgs, GenericParams as CharonGenericParams, IntegerTy as CharonIntegerTy, ItemKind as CharonItemKind, ItemMeta as CharonItemMeta, ItemOpacity as CharonItemOpacity, Literal as CharonLiteral, LiteralTy as CharonLiteralTy, - Name as CharonName, Opaque as CharonOpaque, Operand as CharonOperand, + Locals, Name as CharonName, Opaque as CharonOpaque, Operand as CharonOperand, PathElem as CharonPathElem, Place as CharonPlace, ProjectionElem as CharonProjectionElem, RawConstantExpr as CharonRawConstantExpr, RefKind as CharonRefKind, Region as CharonRegion, - RegionId as CharonRegionId, RegionVar as CharonRegionVar, Rvalue as CharonRvalue, - ScalarValue as CharonScalarValue, Span as CharonSpan, TranslatedCrate as CharonTranslatedCrate, - TypeDecl as CharonTypeDecl, TypeDeclKind as CharonTypeDeclKind, TypeId as CharonTypeId, - TypeVar as CharonTypeVar, TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, Var as CharonVar, - VarId as CharonVarId, Variant as CharonVariant, VariantId as CharonVariantId, + RegionBinder as CharonRegionBinder, RegionId as CharonRegionId, RegionVar as CharonRegionVar, + Rvalue as CharonRvalue, ScalarValue as CharonScalarValue, Span as CharonSpan, + TranslatedCrate as CharonTranslatedCrate, TypeDecl as CharonTypeDecl, + TypeDeclKind as CharonTypeDeclKind, TypeId as CharonTypeId, TypeVar as CharonTypeVar, + TypeVarId as CharonTypeVarId, UnOp as CharonUnOp, Var as CharonVar, VarId as CharonVarId, + Variant as CharonVariant, VariantId as CharonVariantId, }; use charon_lib::errors::{Error as CharonError, ErrorCtx as CharonErrorCtx}; use charon_lib::ids::Vector as CharonVector; @@ -60,6 +61,7 @@ use stable_mir::ty::{ MirConst, Region, RegionKind, RigidTy, Span, Ty, TyConst, TyConstKind, TyKind, UintTy, }; use stable_mir::{CrateDef, DefId}; +use std::collections::HashMap; use std::path::PathBuf; use tracing::{debug, trace}; @@ -70,8 +72,9 @@ pub struct Context<'a, 'tcx> { instance: Instance, translated: &'a mut CharonTranslatedCrate, id_map: &'a mut FxHashMap, - errors: &'a mut CharonErrorCtx<'tcx>, + errors: &'a mut CharonErrorCtx, local_names: FxHashMap, + file_to_id: HashMap, } impl<'a, 'tcx> Context<'a, 'tcx> { @@ -82,7 +85,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { instance: Instance, translated: &'a mut CharonTranslatedCrate, id_map: &'a mut FxHashMap, - errors: &'a mut CharonErrorCtx<'tcx>, + errors: &'a mut CharonErrorCtx, ) -> Self { let mut local_names = FxHashMap::default(); // populate names of locals @@ -93,8 +96,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } } } - - Self { tcx, instance, translated, id_map, errors, local_names } + let file_to_id: HashMap = HashMap::new(); + Self { tcx, instance, translated, id_map, errors, local_names, file_to_id } } fn tcx(&self) -> TyCtxt<'tcx> { @@ -102,7 +105,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } fn span_err(&mut self, span: CharonSpan, msg: &str) { - self.errors.span_err(span, msg); + self.errors.span_err(self.translated, span, msg); } fn continue_on_failure(&self) -> bool { @@ -136,6 +139,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { item_meta, signature, kind: CharonItemKind::Regular, + is_global_initializer: None, body: Ok(body), }; @@ -645,11 +649,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { /// Compute the span information for MIR span fn translate_span(&mut self, span: Span) -> CharonSpan { let filename = CharonFileName::Local(PathBuf::from(span.get_filename())); - let file_id = match self.translated.file_to_id.get(&filename) { + let file_id = match self.file_to_id.get(&filename) { Some(file_id) => *file_id, None => { - let file_id = self.translated.id_to_file.push(filename.clone()); - self.translated.file_to_id.insert(filename, file_id); + let file = CharonFile { name: filename.clone(), contents: None }; + let file_id = self.translated.files.push(file); + self.file_to_id.insert(filename, file_id); file_id } }; @@ -699,7 +704,6 @@ impl<'a, 'tcx> Context<'a, 'tcx> { is_closure: false, closure_info: None, generics: CharonGenericParams::default(), - parent_params_info: None, inputs: args, output: ret_type, } @@ -717,11 +721,12 @@ impl<'a, 'tcx> Context<'a, 'tcx> { fn translate_body(&mut self, mir_body: Body) -> CharonBody { let span = self.translate_span(mir_body.span); let arg_count = self.instance.fn_abi().unwrap().args.len(); - let locals = self.translate_body_locals(&mir_body); + let vars = self.translate_body_locals(&mir_body); + let locals = Locals { vars, arg_count }; let body: CharonBodyContents = mir_body.blocks.iter().map(|bb| self.translate_block(bb)).collect(); - let body_expr = CharonExprBody { span, arg_count, locals, body, comments: Vec::new() }; + let body_expr = CharonExprBody { span, locals, body, comments: Vec::new() }; CharonBody::Unstructured(body_expr) } @@ -764,9 +769,11 @@ impl<'a, 'tcx> Context<'a, 'tcx> { fn translate_ty(&mut self, ty: Ty) -> CharonTy { match ty.kind() { TyKind::RigidTy(rigid_ty) => self.translate_rigid_ty(rigid_ty), - TyKind::Param(paramty) => CharonTy::new(CharonTyKind::TypeVar( - CharonTypeVarId::from_usize(paramty.index as usize), - )), + TyKind::Param(paramty) => { + let debr = + CharonDeBruijnVar::free(CharonTypeVarId::from_usize(paramty.index as usize)); + CharonTy::new(CharonTyKind::TypeVar(debr)) + } x => todo!("Not yet implemented translation for TyKind: {:?}", x), } } @@ -778,7 +785,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { translate_constant_expr_to_const_generic(c_raw_constexpr).unwrap() } TyConstKind::Param(paramc) => { - CharonConstGeneric::Var(CharonConstGenericVarId::from_usize(paramc.index as usize)) + let debr = CharonDeBruijnVar::free(CharonConstGenericVarId::from_usize( + paramc.index as usize, + )); + CharonConstGeneric::Var(debr) } _ => todo!(), } @@ -843,15 +853,16 @@ impl<'a, 'tcx> Context<'a, 'tcx> { }; CharonTy::new(CharonTyKind::Adt(CharonTypeId::Tuple, generic_args)) } - RigidTy::FnDef(def_id, args) => { - if !args.0.is_empty() { - unimplemented!("generic args are not yet handled"); - } + RigidTy::FnDef(def_id, _args) => { let sig = def_id.fn_sig().value; let inputs = sig.inputs().iter().map(|ty| self.translate_ty(*ty)).collect(); let output = self.translate_ty(sig.output()); // TODO: populate regions? - CharonTy::new(CharonTyKind::Arrow(CharonVector::new(), inputs, output)) + let rb = CharonRegionBinder { + regions: CharonVector::new(), + skip_binder: (inputs, output), + }; + CharonTy::new(CharonTyKind::Arrow(rb)) } RigidTy::Adt(adt_def, genarg) => { let def_id = adt_def.def_id(); @@ -1004,10 +1015,10 @@ impl<'a, 'tcx> Context<'a, 'tcx> { } fn translate_place(&mut self, place: &Place) -> CharonPlace { - let projection = self.translate_projection(place, &place.projection); + let (_projection, ty) = self.translate_projection(place, &place.projection); let local = place.local; let var_id = CharonVarId::from_usize(local); - CharonPlace { var_id, projection } + CharonPlace::new(var_id, ty) } fn place_ty(&self, place: &Place) -> Ty { @@ -1251,7 +1262,7 @@ impl<'a, 'tcx> Context<'a, 'tcx> { &mut self, place: &Place, projection: &[ProjectionElem], - ) -> Vec { + ) -> (Vec, CharonTy) { let c_place_ty = self.translate_ty(self.place_ty(place)); let mut c_provec = Vec::new(); let mut current_ty = c_place_ty.clone(); @@ -1291,27 +1302,29 @@ impl<'a, 'tcx> Context<'a, 'tcx> { current_var = varid.to_index(); } ProjectionElem::Index(local) => { - let c_operand = - CharonOperand::Copy(CharonPlace::new(CharonVarId::from_usize(*local))); + let c_operand = CharonOperand::Copy(CharonPlace::new( + CharonVarId::from_usize(*local), + current_ty.clone(), + )); c_provec.push(CharonProjectionElem::Index { - offset: c_operand, + offset: Box::new(c_operand), from_end: false, - ty: current_ty.clone(), }); } _ => continue, } } - c_provec + (c_provec, current_ty) } fn translate_region(&self, region: Region) -> CharonRegion { match region.kind { RegionKind::ReStatic => CharonRegion::Static, RegionKind::ReErased => CharonRegion::Erased, - RegionKind::ReEarlyParam(_) => CharonRegion::Unknown, - RegionKind::ReBound(_, _) | RegionKind::RePlaceholder(_) => { + RegionKind::ReEarlyParam(_) + | RegionKind::ReBound(_, _) + | RegionKind::RePlaceholder(_) => { todo!("Not yet implemented RegionKind: {:?}", region.kind) } } From 954fa15a0b18d4dc7c9ec9f9c896f21cc01c24bd Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Fri, 3 Jan 2025 02:07:30 -0800 Subject: [PATCH 18/20] Upgrade toolchain to 2024-12-19 (#3810) Upgrade Rust toolchain to 2024-12-19. Resolves #3795 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 506443c043ca..75152d6384f4 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-18" +channel = "nightly-2024-12-19" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] From d4b85a352f46ba0ed3ac8760945ad831db081650 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Mon, 6 Jan 2025 09:05:06 -0500 Subject: [PATCH 19/20] Automatic cargo update to 2025-01-06 (#3812) Dependency upgrade resulting from `cargo update`. Co-authored-by: tautschnig <1144736+tautschnig@users.noreply.github.com> --- Cargo.lock | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index e8cdaf3e2a3f..45a46da09280 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -164,9 +164,9 @@ dependencies = [ [[package]] name = "bstr" -version = "1.11.2" +version = "1.11.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c94feba04f99cbce6558bbe1c18e38692a056981cb66c96f0878c2452aa28023" +checksum = "531a9155a481e2ee699d4f98f43c0ca4ff8ee1bfd55c31e9e98fb29d2b176fe0" dependencies = [ "memchr", "regex-automata 0.4.9", @@ -229,9 +229,9 @@ dependencies = [ [[package]] name = "cc" -version = "1.2.6" +version = "1.2.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8d6dbb628b8f8555f86d0323c2eb39e3ec81901f4b83e091db8a6a76d316a333" +checksum = "a012a0df96dd6d06ba9a1b29d6402d1a5d77c6befd2566afdc26e10603dc93d7" dependencies = [ "shlex", ] @@ -1157,9 +1157,9 @@ checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" [[package]] name = "os_info" -version = "3.9.1" +version = "3.9.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eb6651f4be5e39563c4fe5cc8326349eb99a25d805a3493f791d5bfd0269e430" +checksum = "6e6520c8cc998c5741ee68ec1dc369fc47e5f0ea5320018ecf2a1ccd6328f48b" dependencies = [ "log", "windows-sys 0.52.0", @@ -1668,9 +1668,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.94" +version = "2.0.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "987bc0be1cdea8b10216bd06e2ca407d40b9543468fafd3ddfb02f36e77f71f3" +checksum = "46f71c0377baf4ef1cc3e3402ded576dccc315800fbc62dfc7fe04b009773b4a" dependencies = [ "proc-macro2", "quote", @@ -1685,12 +1685,13 @@ checksum = "f764005d11ee5f36500a149ace24e00e3da98b0158b3e2d53a7495660d3f4d60" [[package]] name = "tempfile" -version = "3.14.0" +version = "3.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "28cce251fcbc87fac86a866eeb0d6c2d536fc16d06f184bb61aeae11aa4cee0c" +checksum = "9a8a559c81686f576e8cd0290cd2a24a2a9ad80c98b3478856500fcbd7acd704" dependencies = [ "cfg-if", "fastrand", + "getrandom", "once_cell", "rustix", "windows-sys 0.59.0", @@ -2171,9 +2172,9 @@ checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" [[package]] name = "winnow" -version = "0.6.21" +version = "0.6.22" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e6f5bb5257f2407a5425c6e749bfd9692192a73e70a6060516ac04f889087d68" +checksum = "39281189af81c07ec09db316b302a3e67bf9bd7cbf6c820b50e35fee9c2fa980" dependencies = [ "memchr", ] From 23a36bb62e2dfb1559578f98e2d85bbbd6a9bc3b Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Mon, 6 Jan 2025 18:20:15 +0000 Subject: [PATCH 20/20] Bump tests/perf/s2n-quic from `a54686e` to `ac52a48` (#3813) Bumps [tests/perf/s2n-quic](https://github.com/aws/s2n-quic) from `a54686e` to `ac52a48`.
Commits
  • ac52a48 fix(s2n-quic-dc): handle spurious TCP acceptor worker wakeups (#2434)
  • 8d9b09e fix(s2n-quic-dc): Pause the cleaner thread for the tail of the execution time...
  • d7db13c feat(s2n-quic-dc): Globally cache the control socket (#2431)
  • 239a8d9 fix(s2n-quic-dc): Import fixes + new metrics (#2430)
  • 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 a54686e4e1da..ac52a4805a62 160000 --- a/tests/perf/s2n-quic +++ b/tests/perf/s2n-quic @@ -1 +1 @@ -Subproject commit a54686e4e1daad2afbbc01fccaf4cc1a512c58bf +Subproject commit ac52a4805a62ca4c7c9d1c17e86ba41c2afd308f