From b349137a68c6d22bc752c14fdea4e397b2c462f4 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 18 Jan 2024 07:46:03 -0800 Subject: [PATCH 1/3] Upgrade toolchain to nightly-2024-01-17 (#2976) Fixes were done to address the following upstream changes: - https://github.com/rust-lang/rust/pull/119606 - https://github.com/rust-lang/rust/pull/119751 - https://github.com/rust-lang/rust/pull/120025 - https://github.com/rust-lang/rust/pull/116520 Resolves #2971 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/typ.rs | 6 +++++- .../src/codegen_cprover_gotoc/utils/debug.rs | 2 +- kani-compiler/src/kani_middle/attributes.rs | 14 +++++++------- kani-compiler/src/kani_middle/intrinsics.rs | 5 +++-- rust-toolchain.toml | 2 +- 5 files changed, 17 insertions(+), 12 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index bdddd8ce9f26..7694feb0dbbf 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -302,7 +302,11 @@ impl<'tcx> GotocCtx<'tcx> { kind: ty::BoundRegionKind::BrEnv, }; let env_region = ty::Region::new_bound(self.tcx, ty::INNERMOST, br); - let env_ty = self.tcx.closure_env_ty(def_id, args, env_region).unwrap(); + let env_ty = self.tcx.closure_env_ty( + Ty::new_closure(self.tcx, def_id, args), + args.as_closure().kind(), + env_region, + ); let sig = sig.skip_binder(); diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs index c30d1539bda2..aeaf8e0e2d10 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs @@ -16,7 +16,7 @@ use tracing::debug; // Use a thread-local global variable to track the current codegen item for debugging. // If Kani panics during codegen, we can grab this item to include the problematic // codegen item in the panic trace. -thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<(Option, Option)> = RefCell::new((None, None))); +thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<(Option, Option)> = const { RefCell::new((None, None)) }); pub fn init() { // Install panic hook diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 3bfef9a409f4..bfc36360270e 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -348,12 +348,12 @@ impl<'tcx> KaniAttributes<'tcx> { "Use of unstable feature `{}`: {}", unstable_attr.feature, unstable_attr.reason )) - .span_note( + .with_span_note( self.tcx.def_span(self.item), format!("the function `{fn_name}` is unstable:"), ) - .note(format!("see issue {} for more information", unstable_attr.issue)) - .help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature)) + .with_note(format!("see issue {} for more information", unstable_attr.issue)) + .with_help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature)) .emit() } @@ -422,7 +422,7 @@ impl<'tcx> KaniAttributes<'tcx> { self.item_name(), ), ) - .span_note(self.tcx.def_span(id), "Try adding a contract to this function.") + .with_span_note(self.tcx.def_span(id), "Try adding a contract to this function.") .emit(); return; }; @@ -448,7 +448,7 @@ impl<'tcx> KaniAttributes<'tcx> { self.item_name(), ), ) - .span_note( + .with_span_note( self.tcx.def_span(def_id), format!( "Try adding a contract to this function or use the unsound `{}` attribute instead.", @@ -624,7 +624,7 @@ impl<'a> UnstableAttrParseError<'a> { self.attr.span, format!("failed to parse `#[kani::unstable]`: {}", self.reason), ) - .note(format!( + .with_note(format!( "expected format: #[kani::unstable({}, {}, {})]", r#"feature="""#, r#"issue="""#, r#"reason="""# )) @@ -665,7 +665,7 @@ fn expect_no_args(tcx: TyCtxt, kind: KaniAttributeKind, attr: &Attribute) { if !attr.is_word() { tcx.dcx() .struct_span_err(attr.span, format!("unexpected argument for `{}`", kind.as_ref())) - .help("remove the extra argument") + .with_help("remove the extra argument") .emit(); } } diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs index c4785ac98b81..8a7fc16d8e9f 100644 --- a/kani-compiler/src/kani_middle/intrinsics.rs +++ b/kani-compiler/src/kani_middle/intrinsics.rs @@ -7,6 +7,7 @@ use rustc_middle::mir::{Body, Const as mirConst, ConstValue, Operand, Terminator use rustc_middle::mir::{Local, LocalDecl}; use rustc_middle::ty::{self, Ty, TyCtxt}; use rustc_middle::ty::{Const, GenericArgsRef}; +use rustc_span::source_map::Spanned; use rustc_span::symbol::{sym, Symbol}; use tracing::{debug, trace}; @@ -48,12 +49,12 @@ impl<'tcx> ModelIntrinsics<'tcx> { fn replace_simd_bitmask( &self, func: &mut Operand<'tcx>, - args: &[Operand<'tcx>], + args: &[Spanned>], gen_args: GenericArgsRef<'tcx>, ) { assert_eq!(args.len(), 1); let tcx = self.tcx; - let arg_ty = args[0].ty(&self.local_decls, tcx); + let arg_ty = args[0].node.ty(&self.local_decls, tcx); if arg_ty.is_simd() { // Get the stub definition. let stub_id = tcx.get_diagnostic_item(Symbol::intern("KaniModelSimdBitmask")).unwrap(); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 620fdc1efa29..2914c0609c1a 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-01-08" +channel = "nightly-2024-01-17" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From 965810e818991e3d46d20010f5e2a37803a259d0 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 18 Jan 2024 18:53:38 +0100 Subject: [PATCH 2/3] Benchcomp visualize: fix missing import (#2977) logging is required when handling errors. --- tools/benchcomp/benchcomp/visualizers/__init__.py | 1 + 1 file changed, 1 insertion(+) diff --git a/tools/benchcomp/benchcomp/visualizers/__init__.py b/tools/benchcomp/benchcomp/visualizers/__init__.py index af973379f19d..4f547eaaaf68 100644 --- a/tools/benchcomp/benchcomp/visualizers/__init__.py +++ b/tools/benchcomp/benchcomp/visualizers/__init__.py @@ -4,6 +4,7 @@ import dataclasses import json +import logging import subprocess import textwrap From 16641d280886cc3608803d5098f28fc57c59a522 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9mi=20Delmas?= Date: Fri, 19 Jan 2024 11:33:16 -0500 Subject: [PATCH 3/3] Cargo update 2024-01-18 (#2978) Starting from clap v4.4.15 https://github.com/clap-rs/clap/pull/5298 in some cases `UnknownArgument` errors are reported as `ArgumentConflict` errors. Co-authored-by: Remi Delmas --- Cargo.lock | 138 +++++++++--------------------------- kani-driver/src/args/mod.rs | 2 +- 2 files changed, 34 insertions(+), 106 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index fc42c86850b1..ff64b733a145 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -34,9 +34,9 @@ dependencies = [ [[package]] name = "anstream" -version = "0.6.5" +version = "0.6.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d664a92ecae85fd0a7392615844904654d1d5f5514837f471ddef4a057aba1b6" +checksum = "6e2e1ebcb11de5c03c67de28a7df593d32191b44939c482e97702baaaa6ab6a5" dependencies = [ "anstyle", "anstyle-parse", @@ -100,9 +100,9 @@ checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" [[package]] name = "bitflags" -version = "2.4.1" +version = "2.4.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "327762f6e5a765692301e5bb513e0d9fef63be86bbc14528052b1cd3e6f03e07" +checksum = "ed570934406eb16438a4e976b1b4500774099c13b8cb96eec99f620f05090ddf" [[package]] name = "bookrunner" @@ -167,9 +167,9 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" [[package]] name = "clap" -version = "4.4.13" +version = "4.4.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "52bdc885e4cacc7f7c9eedc1ef6da641603180c783c41a15c264944deeaab642" +checksum = "1e578d6ec4194633722ccf9544794b71b1385c3c027efe0c55db226fc880865c" dependencies = [ "clap_builder", "clap_derive", @@ -177,9 +177,9 @@ dependencies = [ [[package]] name = "clap_builder" -version = "4.4.12" +version = "4.4.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fb7fb5e4e979aec3be7791562fcba452f94ad85e954da024396433e0e25a79e9" +checksum = "4df4df40ec50c46000231c914968278b1eb05098cf8f1b3a518a95030e71d1c7" dependencies = [ "anstream", "anstyle", @@ -242,15 +242,15 @@ dependencies = [ [[package]] name = "console" -version = "0.15.7" +version = "0.15.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c926e00cc70edefdc64d3a5ff31cc65bb97a3460097762bd23afb4d8145fccf8" +checksum = "0e1f83fc076bd6dd27517eacdf25fef6c4dfe5f1d7448bafaaf3a26f13b5e4eb" dependencies = [ "encode_unicode", "lazy_static", "libc", "unicode-width", - "windows-sys 0.45.0", + "windows-sys 0.52.0", ] [[package]] @@ -270,34 +270,28 @@ dependencies = [ [[package]] name = "crossbeam-deque" -version = "0.8.4" +version = "0.8.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fca89a0e215bab21874660c67903c5f143333cab1da83d041c7ded6053774751" +checksum = "613f8cc01fe9cf1a3eb3d7f488fd2fa8388403e97039e2f73692932e291a770d" dependencies = [ - "cfg-if", "crossbeam-epoch", "crossbeam-utils", ] [[package]] name = "crossbeam-epoch" -version = "0.9.17" +version = "0.9.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e3681d554572a651dda4186cd47240627c3d0114d45a95f6ad27f2f22e7548d" +checksum = "5b82ac4a3c2ca9c3460964f020e1402edd5753411d7737aa39c3714ad1b5420e" dependencies = [ - "autocfg", - "cfg-if", "crossbeam-utils", ] [[package]] name = "crossbeam-utils" -version = "0.8.18" +version = "0.8.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c3a430a770ebd84726f584a90ee7f020d28db52c6d02138900f22341f866d39c" -dependencies = [ - "cfg-if", -] +checksum = "248e3bacc7dc6baa3b21e405ee045c3047101a49145e7e9eca583ab4c2ca5345" [[package]] name = "crossterm" @@ -305,7 +299,7 @@ version = "0.27.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f476fe445d41c9e991fd07515a6f463074b782242ccf4a5b7b1d1012e70824df" dependencies = [ - "bitflags 2.4.1", + "bitflags 2.4.2", "crossterm_winapi", "libc", "parking_lot", @@ -366,9 +360,9 @@ dependencies = [ [[package]] name = "getrandom" -version = "0.2.11" +version = "0.2.12" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fe9006bed769170c11f845cf00c7c1e9092aeb3f268e007c3e760ac68008070f" +checksum = "190092ea657667030ac6a35e305e62fc4dd69fd98ac98631e5d3a2b1575a12b5" dependencies = [ "cfg-if", "libc", @@ -546,9 +540,9 @@ dependencies = [ [[package]] name = "linux-raw-sys" -version = "0.4.12" +version = "0.4.13" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c4cd1a83af159aa67994778be9070f0ae1bd732942279cabb14f86f986a21456" +checksum = "01cda141df6706de531b6c46c3a33ecca755538219bd484262fa09410c13539c" [[package]] name = "lock_api" @@ -821,9 +815,9 @@ dependencies = [ [[package]] name = "rayon" -version = "1.8.0" +version = "1.8.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c27db03db7734835b3f53954b534c91069375ce6ccaa2e065441e07d9b6cdb1" +checksum = "fa7237101a77a10773db45d62004a272517633fbcc3df19d96455ede1122e051" dependencies = [ "either", "rayon-core", @@ -831,9 +825,9 @@ dependencies = [ [[package]] name = "rayon-core" -version = "1.12.0" +version = "1.12.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5ce3fb6ad83f861aac485e76e1985cd109d9a3713802152be56c3b1f0e0658ed" +checksum = "1465873a3dfdaa8ae7cb14b4383657caab0b3e8a0aa9ae8e04b044854c8dfce2" dependencies = [ "crossbeam-deque", "crossbeam-utils", @@ -907,11 +901,11 @@ dependencies = [ [[package]] name = "rustix" -version = "0.38.28" +version = "0.38.30" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72e572a5e8ca657d7366229cdde4bd14c4eb5499a9573d4d366fe1b599daa316" +checksum = "322394588aaf33c24007e8bb3238ee3e4c5c09c084ab32bc73890b99ff326bca" dependencies = [ - "bitflags 2.4.1", + "bitflags 2.4.2", "errno", "libc", "linux-raw-sys", @@ -1033,9 +1027,9 @@ checksum = "24188a676b6ae68c3b2cb3a01be17fbf7240ce009799bb56d5b1409051e78fde" [[package]] name = "smallvec" -version = "1.11.2" +version = "1.13.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4dccd0940a2dcdf68d092b8cbab7dc0ad8fa938bf95787e1b916b0e3d0e8e970" +checksum = "3b187f0231d56fe41bfb12034819dd2bf336422a5866de41bc3fec4b2e3883e8" [[package]] name = "std" @@ -1367,15 +1361,6 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" -[[package]] -name = "windows-sys" -version = "0.45.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75283be5efb2831d37ea142365f009c02ec203cd29a3ebecbc093d52315b66d0" -dependencies = [ - "windows-targets 0.42.2", -] - [[package]] name = "windows-sys" version = "0.48.0" @@ -1394,21 +1379,6 @@ dependencies = [ "windows-targets 0.52.0", ] -[[package]] -name = "windows-targets" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e5180c00cd44c9b1c88adb3693291f1cd93605ded80c250a75d472756b4d071" -dependencies = [ - "windows_aarch64_gnullvm 0.42.2", - "windows_aarch64_msvc 0.42.2", - "windows_i686_gnu 0.42.2", - "windows_i686_msvc 0.42.2", - "windows_x86_64_gnu 0.42.2", - "windows_x86_64_gnullvm 0.42.2", - "windows_x86_64_msvc 0.42.2", -] - [[package]] name = "windows-targets" version = "0.48.5" @@ -1439,12 +1409,6 @@ dependencies = [ "windows_x86_64_msvc 0.52.0", ] -[[package]] -name = "windows_aarch64_gnullvm" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "597a5118570b68bc08d8d59125332c54f1ba9d9adeedeef5b99b02ba2b0698f8" - [[package]] name = "windows_aarch64_gnullvm" version = "0.48.5" @@ -1457,12 +1421,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cb7764e35d4db8a7921e09562a0304bf2f93e0a51bfccee0bd0bb0b666b015ea" -[[package]] -name = "windows_aarch64_msvc" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e08e8864a60f06ef0d0ff4ba04124db8b0fb3be5776a5cd47641e942e58c4d43" - [[package]] name = "windows_aarch64_msvc" version = "0.48.5" @@ -1475,12 +1433,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bbaa0368d4f1d2aaefc55b6fcfee13f41544ddf36801e793edbbfd7d7df075ef" -[[package]] -name = "windows_i686_gnu" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c61d927d8da41da96a81f029489353e68739737d3beca43145c8afec9a31a84f" - [[package]] name = "windows_i686_gnu" version = "0.48.5" @@ -1493,12 +1445,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a28637cb1fa3560a16915793afb20081aba2c92ee8af57b4d5f28e4b3e7df313" -[[package]] -name = "windows_i686_msvc" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44d840b6ec649f480a41c8d80f9c65108b92d89345dd94027bfe06ac444d1060" - [[package]] name = "windows_i686_msvc" version = "0.48.5" @@ -1511,12 +1457,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "ffe5e8e31046ce6230cc7215707b816e339ff4d4d67c65dffa206fd0f7aa7b9a" -[[package]] -name = "windows_x86_64_gnu" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8de912b8b8feb55c064867cf047dda097f92d51efad5b491dfb98f6bbb70cb36" - [[package]] name = "windows_x86_64_gnu" version = "0.48.5" @@ -1529,12 +1469,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3d6fa32db2bc4a2f5abeacf2b69f7992cd09dca97498da74a151a3132c26befd" -[[package]] -name = "windows_x86_64_gnullvm" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "26d41b46a36d453748aedef1486d5c7a85db22e56aff34643984ea85514e94a3" - [[package]] name = "windows_x86_64_gnullvm" version = "0.48.5" @@ -1547,12 +1481,6 @@ version = "0.52.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1a657e1e9d3f514745a572a6846d3c7aa7dbe1658c056ed9c3344c4109a6949e" -[[package]] -name = "windows_x86_64_msvc" -version = "0.42.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9aec5da331524158c6d1a4ac0ab1541149c0b9505fde06423b02f5ef0106b9f0" - [[package]] name = "windows_x86_64_msvc" version = "0.48.5" @@ -1567,9 +1495,9 @@ checksum = "dff9641d1cd4be8d1a070daf9e3773c5f67e78b4d9d42263020c057706765c04" [[package]] name = "winnow" -version = "0.5.33" +version = "0.5.34" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b7520bbdec7211caa7c4e682eb1fbe07abe20cee6756b6e00f537c82c11816aa" +checksum = "b7cf47b659b318dccbd69cc4797a39ae128f533dce7902a1096044d1967b9c16" dependencies = [ "memchr", ] diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs index 6651f72db7c2..39b3c1fd025f 100644 --- a/kani-driver/src/args/mod.rs +++ b/kani-driver/src/args/mod.rs @@ -736,7 +736,7 @@ mod tests { "kani input.rs --harness harness_1 harness_2".split(" "), ); assert!(result.is_err()); - assert_eq!(result.unwrap_err().kind(), ErrorKind::UnknownArgument); + assert_eq!(result.unwrap_err().kind(), ErrorKind::ArgumentConflict); } #[test]