From 660b1f856c140c3f8d1260947a38c91b3b37a0b4 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 3 Dec 2023 21:59:39 +0000
Subject: [PATCH] Update the rust toolchain to nightly-2023-12-03

Changes required due to:
- rust-lang/rust@99ac405b96 Move MetadataLoader{,Dyn} to rustc_metadata.
- rust-lang/rust@c997c6d822 Add more information to stable Instance
---
 .../src/codegen_cprover_gotoc/compiler_interface.rs          | 2 +-
 kani-compiler/src/kani_middle/analysis.rs                    | 1 -
 kani-compiler/src/kani_middle/reachability.rs                | 5 ++---
 kani-driver/src/concrete_playback/test_generator.rs          | 2 +-
 rust-toolchain.toml                                          | 2 +-
 5 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index df472518c9a3..720e9d8ab423 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -40,7 +40,7 @@ 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_metadata::creader::MetadataLoaderDyn;
 use rustc_session::output::out_filename;
 use rustc_session::Session;
 use rustc_smir::rustc_internal;
diff --git a/kani-compiler/src/kani_middle/analysis.rs b/kani-compiler/src/kani_middle/analysis.rs
index 011907c14ea4..b23fb99f83ff 100644
--- a/kani-compiler/src/kani_middle/analysis.rs
+++ b/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"),
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index d56b7b5db65d..216feb66fb87 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/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
diff --git a/kani-driver/src/concrete_playback/test_generator.rs b/kani-driver/src/concrete_playback/test_generator.rs
index 492369fb32eb..53c3a92dd94c 100644
--- a/kani-driver/src/concrete_playback/test_generator.rs
+++ b/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 {
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index e016b6b50492..1399eae195ec 100644
--- a/rust-toolchain.toml
+++ b/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"]