From f5f1e94e02c02b0f0f5038ad22f5b53fbb7511e0 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Wed, 27 Mar 2024 17:18:35 -0400 Subject: [PATCH] Upgrade Rust toolchain to `nightly-2024-03-21` (#3102) Upgrades the Rust toolchain to `nightly-2024-03-21`. The relevant changes in Rust are: * https://github.com/rust-lang/rust/pull/122480 * https://github.com/rust-lang/rust/pull/122748 * https://github.com/rust-lang/cargo/pull/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 --- .../compiler_interface.rs | 6 +++-- kani-compiler/src/kani_compiler.rs | 11 +++++----- kani-compiler/src/kani_middle/reachability.rs | 3 ++- kani-compiler/src/kani_middle/stubbing/mod.rs | 3 ++- .../src/kani_middle/transform/check_values.rs | 2 +- kani-driver/src/call_cargo.rs | 22 ++++++++++++++++++- rust-toolchain.toml | 2 +- tests/cargo-ui/assess-error/expected | 2 +- ...rite_invalid.rs => write_invalid_fixme.rs} | 3 +++ 9 files changed, 41 insertions(+), 13 deletions(-) rename tests/kani/ValidValues/{write_invalid.rs => write_invalid_fixme.rs} (88%) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index d3b4ae8473de..039c50eefe18 100644 --- 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 index 48b4318db5bf..fc5f5891ecae 100644 --- 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 index b46fbdccc016..52b55d6b947c 100644 --- 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 index 0db518ceef9f..37426bfe0b77 100644 --- 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 index aefc20b46a44..4888e032af4f 100644 --- 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 index b68d18c84a40..9d27e5853696 100644 --- 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 + // + // + // 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: + 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 index 7035d1aba20f..d08e3a84f0ad 100644 --- 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 index 70754ddea192..213d811ae577 100644 --- 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 b/tests/kani/ValidValues/write_invalid_fixme.rs similarity index 88% rename from tests/kani/ValidValues/write_invalid.rs rename to tests/kani/ValidValues/write_invalid_fixme.rs index 05d3705bd69a..f04a667a47d1 100644 --- a/tests/kani/ValidValues/write_invalid.rs +++ b/tests/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]