Upgrade Rust toolchain to nightly-2024-03-21 (#3102)

Upgrades the Rust toolchain to `nightly-2024-03-21`. The relevant changes in Rust are: * rust-lang/rust#122480 * rust-lang/rust#122748 * rust-lang/cargo#12783 I wasn't confident that our regression testing could detect differences in the file paths being generated with the new logic, so I added code similar to the following just to check they were equivalent: ```rust let base_filename = tcx.output_filenames(()).output_path(OutputType::Object); + let binding = tcx.output_filenames(()).path(OutputType::Object); + let base_filename2 = binding.as_path(); + assert_eq!(base_filename, base_filename2); ``` Note that this was done for each instance where we used `output_path`, and completed regression testing with the previous toolchain version. I also checked manually the instance where we generate a `.dot` graph for debug purposes following the instructions [here](https://model-checking.github.io/kani/cheat-sheets.html?highlight=dot#debug) (a `libmain.dot` file was generated for the `main.rs` in one of my projects). --------- Co-authored-by: Celina G. Val <[email protected]>
model-checking · Mar 27, 2024 · f5f1e94 · f5f1e94
1 parent 1c3d0f3
commit f5f1e94
Show file tree

Hide file tree

Showing 9 changed files with 41 additions and 13 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -228,7 +228,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 transformer = BodyTransformation::new(&queries, tcx);
             let mut results = GotoCodegenResults::new(tcx, reachability);
@@ -412,7 +413,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),
                 };

diff --git a/kani-compiler/src/kani_compiler.rs b/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()
@@ -376,7 +377,7 @@ impl KaniCompiler {
 
     /// Write the metadata to a file
     fn store_metadata(&self, metadata: &KaniMetadata, filename: &Path) {
-        debug!(?filename, "write_metadata");
+        debug!(?filename, "store_metadata");
         let out_file = File::create(filename).unwrap();
         let writer = BufWriter::new(out_file);
         if self.queries.lock().unwrap().args().output_pretty_json {
@@ -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)]

diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
@@ -584,7 +584,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 {{")?;

diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/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;

diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs
@@ -807,7 +807,7 @@ fn ty_validity_per_offset(
             Ok(result)
         }
         FieldsShape::Arbitrary { ref offsets } => {
-            match ty.kind().rigid().unwrap() {
+            match ty.kind().rigid().expect(&format!("unexpected type: {ty:?}")) {
                 RigidTy::Adt(def, args) => {
                     match def.kind() {
                         AdtKind::Enum => {

diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
@@ -211,7 +211,27 @@ impl KaniSession {
                         }
                     },
                     Message::CompilerArtifact(rustc_artifact) => {
-                        if rustc_artifact.target == *target {
+                        /// Compares two targets, and falls back to a weaker
+                        /// comparison where we avoid dashes in their names.
+                        fn same_target(t1: &Target, t2: &Target) -> bool {
+                            (t1 == t2)
+                                || (t1.name.replace('-', "_") == t2.name.replace('-', "_")
+                                    && t1.kind == t2.kind
+                                    && t1.src_path == t2.src_path
+                                    && t1.edition == t2.edition
+                                    && t1.doctest == t2.doctest
+                                    && t1.test == t2.test
+                                    && t1.doc == t2.doc)
+                        }
+                        // This used to be `rustc_artifact == *target`, but it
+                        // started to fail after the `cargo` change in
+                        // <https://github.com/rust-lang/cargo/pull/12783>
+                        //
+                        // We should revisit this check after a while to see if
+                        // it's not needed anymore or it can be restricted to
+                        // certain cases.
+                        // TODO: <https://github.com/model-checking/kani/issues/3111>
+                        if same_target(&rustc_artifact.target, target) {
                             debug_assert!(
                                 artifact.is_none(),
                                 "expected only one artifact for `{target:?}`",

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-03-15"
+channel = "nightly-2024-03-21"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/cargo-ui/assess-error/expected b/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
diff --git a/tests/kani/ValidValues/write_invalid.rs → ...s/kani/ValidValues/write_invalid_fixme.rs b/tests/kani/ValidValues/write_invalid.rs → ...s/kani/ValidValues/write_invalid_fixme.rs
@@ -6,6 +6,9 @@
 //! Writing invalid bytes is not UB as long as the incorrect value is not read.
 //! However, we over-approximate for sake of simplicity and performance.
 
+// Note: We're getting an unexpected compilation error because the type returned
+// from StableMIR is `Alias`: https://github.com/model-checking/kani/issues/3113
+
 use std::num::NonZeroU8;
 
 #[kani::proof]