Upgrade Rust toolchain to nightly-2024-02-09 (#3015)

Attempt to update Rust toolchain from nightly-2024-01-25 to nightly-2024-02-09. Resolves #3014. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
model-checking · Feb 13, 2024 · 17ff02c · 17ff02c
1 parent 42fcf40
commit 17ff02c
Show file tree

Hide file tree

Showing 11 changed files with 47 additions and 66 deletions.
diff --git 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
@@ -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
@@ -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<StringInterner> = Mutex::new(StringInterner::default());
+ static ref INTERNER: Mutex<StringInterner<StringBackend>> =
+ 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
@@ -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
@@ -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
@@ -60,7 +60,7 @@ static JSON_PANIC_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + 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
@@ -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
@@ -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
@@ -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
@@ -1,5 +1,4 @@
 error[E0277]: the trait bound `Void: kani::Arbitrary` is not satisfied
-
-|\
-| let _wrapper: Wrapper<Void> = kani::any();\
-| ^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`\
+ |\
+14 | let _wrapper: Wrapper<Void> = kani::any();\
+ | ^^^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`, which is required by `Wrapper<Void>: kani::Arbitrary`\
diff --git 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)]