Upgrade Rust toolchain to nightly-2024-03-21

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -225,7 +225,8 @@ impl CodegenBackend for GotocCodegenBackend {
             // - Tests: Generate one model per test harnesses.
             // - PubFns: Generate code for all reachable logic starting from the local public functions.
             // - None: Don't generate code. This is used to compile dependencies.
-            let base_filename = tcx.output_filenames(()).output_path(OutputType::Object);
+            let base_filepath = tcx.output_filenames(()).path(OutputType::Object);
+            let base_filename = base_filepath.as_path();
             let reachability = queries.args().reachability_analysis;
             let mut results = GotoCodegenResults::new(tcx, reachability);
             match reachability {
@@ -405,7 +406,8 @@ impl CodegenBackend for GotocCodegenBackend {
                 builder.build(&out_path);
             } else {
                 // Write the location of the kani metadata file in the requested compiler output file.
-                let base_filename = outputs.output_path(OutputType::Object);
+                let base_filepath = outputs.path(OutputType::Object);
+                let base_filename = base_filepath.as_path();
                 let content_stub = CompilerArtifactStub {
                     metadata_path: base_filename.with_extension(ArtifactType::Metadata),
                 };

kani-compiler/src/kani_compiler.rs

@@ -304,7 +304,8 @@ impl KaniCompiler {
         };
         if self.queries.lock().unwrap().args().reachability_analysis == ReachabilityType::Harnesses
         {
-            let base_filename = tcx.output_filenames(()).output_path(OutputType::Object);
+            let base_filepath = tcx.output_filenames(()).path(OutputType::Object);
+            let base_filename = base_filepath.as_path();
             let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance));
             let all_harnesses = harnesses
                 .into_iter()
@@ -457,9 +458,9 @@ fn generate_metadata(
 
 /// Extract the filename for the metadata file.
 fn metadata_output_path(tcx: TyCtxt) -> PathBuf {
-    let mut filename = tcx.output_filenames(()).output_path(OutputType::Object);
-    filename.set_extension(ArtifactType::Metadata);
-    filename
+    let filepath = tcx.output_filenames(()).path(OutputType::Object);
+    let filename = filepath.as_path();
+    filename.with_extension(ArtifactType::Metadata).to_path_buf()
 }
 
 #[cfg(test)]

kani-compiler/src/kani_middle/reachability.rs

@@ -572,7 +572,8 @@ mod debug {
             if let Ok(target) = std::env::var("KANI_REACH_DEBUG") {
                 debug!(?target, "dump_dot");
                 let outputs = tcx.output_filenames(());
-                let path = outputs.output_path(OutputType::Metadata).with_extension("dot");
+                let base_path = outputs.path(OutputType::Metadata);
+                let path = base_path.as_path().with_extension("dot");
                 let out_file = File::create(path)?;
                 let mut writer = BufWriter::new(out_file);
                 writeln!(writer, "digraph ReachabilityGraph {{")?;

kani-compiler/src/kani_middle/stubbing/mod.rs

@@ -5,6 +5,7 @@
 mod annotations;
 mod transform;
 
+use rustc_span::DUMMY_SP;
 use std::collections::BTreeMap;
 use tracing::{debug, trace};
 
@@ -93,7 +94,7 @@ impl<'tcx> MirVisitor for StubConstChecker<'tcx> {
             Const::Val(..) | Const::Ty(..) => {}
             Const::Unevaluated(un_eval, _) => {
                 // Thread local fall into this category.
-                if self.tcx.const_eval_resolve(ParamEnv::reveal_all(), un_eval, None).is_err() {
+                if self.tcx.const_eval_resolve(ParamEnv::reveal_all(), un_eval, DUMMY_SP).is_err() {
                     // The `monomorphize` call should have evaluated that constant already.
                     let tcx = self.tcx;
                     let mono_const = &un_eval;

rust-toolchain.toml

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

tests/cargo-ui/assess-error/expected

@@ -1,2 +1,2 @@
-error: Failed to compile lib `compilation-error`
+error: Failed to compile lib `compilation_error`
 error: Failed to assess project: Failed to build all targets