Update the rust toolchain to nightly-2023-12-03

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -33,14 +33,14 @@ use rustc_data_structures::temp_dir::MaybeTempDir;
 use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE};
 use rustc_hir::def_id::LOCAL_CRATE;
 use rustc_hir::definitions::DefPathHash;
+use rustc_metadata::creader::MetadataLoaderDyn;
 use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME};
 use rustc_metadata::EncodedMetadata;
 use rustc_middle::dep_graph::{WorkProduct, WorkProductId};
 use rustc_middle::mir::mono::MonoItem;
 use rustc_middle::ty::TyCtxt;
 use rustc_middle::util::Providers;
 use rustc_session::config::{CrateType, OutputFilenames, OutputType};
-use rustc_session::cstore::MetadataLoaderDyn;
 use rustc_session::output::out_filename;
 use rustc_session::Session;
 use rustc_smir::rustc_internal;

kani-compiler/src/kani_middle/analysis.rs

@@ -151,7 +151,6 @@ impl From<&Terminator> for Key {
  TerminatorKind::Assert { .. } => Key("Assert"),
  TerminatorKind::Call { .. } => Key("Call"),
  TerminatorKind::Drop { .. } => Key("Drop"),
- TerminatorKind::CoroutineDrop => Key("CoroutineDrop"),
  TerminatorKind::Goto { .. } => Key("Goto"),
  TerminatorKind::InlineAsm { .. } => Key("InlineAsm"),
  TerminatorKind::Resume { .. } => Key("Resume"),

kani-compiler/src/kani_middle/reachability.rs

@@ -266,7 +266,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
  /// Collect an instance depending on how it is used (invoked directly or via fn_ptr).
  fn collect_instance(&mut self, instance: Instance, is_direct_call: bool) {
  let should_collect = match instance.kind {
- InstanceKind::Virtual | InstanceKind::Intrinsic => {
+ InstanceKind::Virtual { .. } | InstanceKind::Intrinsic => {
  // Instance definition has no body.
  assert!(is_direct_call, "Expected direct call {instance:?}");
  false
@@ -453,8 +453,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
  TerminatorKind::Abort { .. } | TerminatorKind::Assert { .. } => {
  // We generate code for this without invoking any lang item.
  }
- TerminatorKind::CoroutineDrop { .. }
- | TerminatorKind::Goto { .. }
+ TerminatorKind::Goto { .. }
  | TerminatorKind::SwitchInt { .. }
  | TerminatorKind::Resume
  | TerminatorKind::Return

kani-driver/src/concrete_playback/test_generator.rs

@@ -163,7 +163,7 @@ impl KaniSession {
  let mut curr_line_num = 0;
 
  // Use a buffered reader/writer to generate the unit test line by line
- for line in source_reader.lines().flatten() {
+ for line in source_reader.lines().map_while(Result::ok) {
  curr_line_num += 1;
  writeln!(temp_file, "{line}")?;
  if curr_line_num == proof_harness_end_line {

library/kani/src/models/mod.rs

@@ -184,20 +184,6 @@ mod test {
  check_bitmask::<_, [u8; 9], i128, 70>(CustomMask([-1i128; 70]));
  }
 
- /// Compare the value returned by our model and the portable simd representation.
- fn check_portable_bitmask<T, E, const LANES: usize>(mask: T)
- where
- T: ToBitMask + Clone,
- T::BitMask: Debug + PartialEq,
- E: kani_intrinsic::MaskElement,
- [u8; kani_intrinsic::mask_len(LANES)]: Sized,
- {
- assert_eq!(
- unsafe { kani_intrinsic::simd_bitmask::<_, T::BitMask, E, LANES>(mask.clone()) },
- mask.to_bitmask()
- );
- }
-
  /// Compare the value returned by our model and the simd_bitmask intrinsic.
  fn check_bitmask<T, U, E, const LANES: usize>(mask: T)
  where

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-12-01"
+channel = "nightly-2023-12-03"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

tests/kani/SIMD/portable_simd.rs

@@ -4,7 +4,7 @@
 //! Ensure we have basic support of portable SIMD.
 #![feature(portable_simd)]
 
-use std::simd::{mask32x4, u64x16, ToBitMask};
+use std::simd::{mask32x4, u64x16};
 
 #[kani::proof]
 fn check_sum_any() {