diff --git a/Cargo.lock b/Cargo.lock index b00367482588..ec36c820d13c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -14,13 +14,14 @@ dependencies = [ [[package]] name = "ahash" -version = "0.7.8" +version = "0.8.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "891477e0c6a8957309ee5c45a6368af3ae14bb510732d2684ffa19af310920f9" +checksum = "77c3a9648d43b9cd48db467b3f87fdd6e146bcc88ab0180006cef2179fe11d01" dependencies = [ - "getrandom", + "cfg-if", "once_cell", "version_check", + "zerocopy", ] [[package]] @@ -378,19 +379,13 @@ checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" [[package]] name = "hashbrown" -version = "0.11.2" +version = "0.14.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ab5ef0d4909ef3724cc8cce6ccc8572c5c817592e9285f5464f8e86f8bd3726e" +checksum = "290f1a1d9242c78d09ce40a5e87e7554ee637af1351968159f4952f028f75604" dependencies = [ "ahash", ] -[[package]] -name = "hashbrown" -version = "0.14.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "290f1a1d9242c78d09ce40a5e87e7554ee637af1351968159f4952f028f75604" - [[package]] name = "heck" version = "0.4.1" @@ -413,7 +408,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "233cf39063f058ea2caae4091bf4a3ef70a653afbc026f5c4a4135d114e3c177" dependencies = [ "equivalent", - "hashbrown 0.14.3", + "hashbrown", ] [[package]] @@ -1046,12 +1041,12 @@ dependencies = [ [[package]] name = "string-interner" -version = "0.14.0" +version = "0.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "91e2531d8525b29b514d25e275a43581320d587b86db302b9a7e464bac579648" +checksum = "07f9fdfdd31a0ff38b59deb401be81b73913d76c9cc5b1aed4e1330a223420b9" dependencies = [ "cfg-if", - "hashbrown 0.11.2", + "hashbrown", "serde", ] @@ -1516,3 +1511,23 @@ checksum = "5389a154b01683d28c77f8f68f49dea75f0a4da32557a58f68ee51ebba472d29" dependencies = [ "memchr", ] + +[[package]] +name = "zerocopy" +version = "0.7.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "74d4d3961e53fa4c9a25a8637fc2bfaf2595b3d3ae34875568a5cf64787716be" +dependencies = [ + "zerocopy-derive", +] + +[[package]] +name = "zerocopy-derive" +version = "0.7.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9ce1b18ccd8e73a9321186f97e46f9f04b778851177567b1975109d26a08d2a6" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.48", +] diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml index 6f66a32952bc..c2535d20d2fe 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.14.0" +string-interner = "0.15.0" tracing = "0.1" linear-map = {version = "1.2", features = ["serde_impl"]} diff --git a/cprover_bindings/src/cbmc_string.rs b/cprover_bindings/src/cbmc_string.rs index b487b7615122..4c392f647759 100644 --- a/cprover_bindings/src/cbmc_string.rs +++ b/cprover_bindings/src/cbmc_string.rs @@ -3,6 +3,7 @@ use lazy_static::lazy_static; use std::sync::Mutex; +use string_interner::backend::StringBackend; use string_interner::symbol::SymbolU32; use string_interner::StringInterner; @@ -24,7 +25,8 @@ pub struct InternedString(SymbolU32); // Use a `Mutex` to make this thread safe. lazy_static! { - static ref INTERNER: Mutex = Mutex::new(StringInterner::default()); + static ref INTERNER: Mutex> = + Mutex::new(StringInterner::default()); } impl InternedString { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 62b5cbedd95a..c988636a390f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1,7 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT use crate::codegen_cprover_gotoc::GotocCtx; -use cbmc::btree_map; use cbmc::goto_program::{DatatypeComponent, Expr, Location, Parameter, Symbol, SymbolTable, Type}; use cbmc::utils::aggr_tag; use cbmc::{InternString, InternedString}; @@ -51,8 +50,6 @@ pub trait TypeExt { fn is_rust_fat_ptr(&self, st: &SymbolTable) -> bool; fn is_rust_slice_fat_ptr(&self, st: &SymbolTable) -> bool; fn is_rust_trait_fat_ptr(&self, st: &SymbolTable) -> bool; - fn is_unit(&self) -> bool; - fn is_unit_pointer(&self) -> bool; fn unit() -> Self; } @@ -92,42 +89,6 @@ impl TypeExt for Type { // We don't have access to the symbol table here to do it ourselves. Type::struct_tag(UNIT_TYPE_EMPTY_STRUCT_NAME) } - - fn is_unit(&self) -> bool { - match self { - Type::StructTag(name) => *name == aggr_tag(UNIT_TYPE_EMPTY_STRUCT_NAME), - _ => false, - } - } - - fn is_unit_pointer(&self) -> bool { - match self { - Type::Pointer { typ } => typ.is_unit(), - _ => false, - } - } -} - -trait ExprExt { - fn unit(symbol_table: &SymbolTable) -> Self; - - fn is_unit(&self) -> bool; - - fn is_unit_pointer(&self) -> bool; -} - -impl ExprExt for Expr { - fn unit(symbol_table: &SymbolTable) -> Self { - Expr::struct_expr(Type::unit(), btree_map![], symbol_table) - } - - fn is_unit(&self) -> bool { - self.typ().is_unit() - } - - fn is_unit_pointer(&self) -> bool { - self.typ().is_unit_pointer() - } } /// Function signatures @@ -640,7 +601,11 @@ impl<'tcx> GotocCtx<'tcx> { ty::Bound(_, _) | ty::Param(_) => unreachable!("monomorphization bug"), // type checking remnants which shouldn't be reachable - ty::CoroutineWitness(_, _) | ty::Infer(_) | ty::Placeholder(_) | ty::Error(_) => { + ty::CoroutineWitness(_, _) + | ty::CoroutineClosure(_, _) + | ty::Infer(_) + | ty::Placeholder(_) + | ty::Error(_) => { unreachable!("remnants of type checking") } } @@ -1078,6 +1043,7 @@ impl<'tcx> GotocCtx<'tcx> { ty::Bound(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), ty::Error(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), ty::CoroutineWitness(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), + ty::CoroutineClosure(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), ty::Infer(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), ty::Param(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), ty::Placeholder(_) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 94879b5b65e6..10b8c1275da6 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -253,7 +253,7 @@ fn custom_coerce_unsize_info<'tcx>( match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) { Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, .. })) => { - tcx.coerce_unsized_info(impl_def_id).custom_kind.unwrap() + tcx.coerce_unsized_info(impl_def_id).unwrap().custom_kind.unwrap() } impl_source => { unreachable!("invalid `CoerceUnsized` impl_source: {:?}", impl_source); diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index a1c3af20bb06..5b5416a5f142 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -60,7 +60,7 @@ static JSON_PANIC_HOOK: LazyLock) + Sync + Send TerminalUrl::No, ); let diagnostic = Diagnostic::new(rustc_errors::Level::Bug, msg); - emitter.emit_diagnostic(&diagnostic); + emitter.emit_diagnostic(diagnostic); (*JSON_PANIC_HOOK)(info); })); hook diff --git a/kani-driver/src/args/common.rs b/kani-driver/src/args/common.rs index d4ac0a61bd17..3333ee67badf 100644 --- a/kani-driver/src/args/common.rs +++ b/kani-driver/src/args/common.rs @@ -51,6 +51,7 @@ pub trait Verbosity { /// Note that `debug() == true` must imply `verbose() == true`. fn verbose(&self) -> bool; /// Whether we should emit debug messages. + #[allow(unused)] fn debug(&self) -> bool; /// Whether any verbosity was selected. fn is_set(&self) -> bool; diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs index 1d2afa177ca9..009f25b37b5a 100644 --- a/kani-driver/src/main.rs +++ b/kani-driver/src/main.rs @@ -1,7 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT #![feature(let_chains)] -#![feature(array_methods)] use std::ffi::OsString; use std::process::ExitCode; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index b316f181bdac..9d93e7382952 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-25" +channel = "nightly-2024-02-09" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/ui/derive-arbitrary/non_arbitrary_param/expected b/tests/ui/derive-arbitrary/non_arbitrary_param/expected index e74643f3bdb6..55f12678cf9a 100644 --- a/tests/ui/derive-arbitrary/non_arbitrary_param/expected +++ b/tests/ui/derive-arbitrary/non_arbitrary_param/expected @@ -1,5 +1,4 @@ error[E0277]: the trait bound `Void: kani::Arbitrary` is not satisfied - -|\ -| let _wrapper: Wrapper = kani::any();\ -| ^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`\ + |\ +14 | let _wrapper: Wrapper = kani::any();\ + | ^^^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`, which is required by `Wrapper: kani::Arbitrary`\ diff --git a/tools/bookrunner/librustdoc/lib.rs b/tools/bookrunner/librustdoc/lib.rs index 68bc77fa14e8..cddc369b4dc1 100644 --- a/tools/bookrunner/librustdoc/lib.rs +++ b/tools/bookrunner/librustdoc/lib.rs @@ -7,7 +7,6 @@ html_playground_url = "https://play.rust-lang.org/" )] #![feature(rustc_private)] -#![feature(array_methods)] #![feature(assert_matches)] #![feature(box_patterns)] #![feature(control_flow_enum)]