Skip to content

Commit

Permalink
Upgrade Rust toolchain to nightly-2024-03-21 (#3102)
Browse files Browse the repository at this point in the history
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 <celinval@amazon.com>
  • Loading branch information
adpaco-aws and celinval authored Mar 27, 2024
1 parent 1c3d0f3 commit f5f1e94
Show file tree
Hide file tree
Showing 9 changed files with 41 additions and 13 deletions.
6 changes: 4 additions & 2 deletions kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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),
};
Expand Down
11 changes: 6 additions & 5 deletions kani-compiler/src/kani_compiler.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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)]
Expand Down
3 changes: 2 additions & 1 deletion kani-compiler/src/kani_middle/reachability.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {{")?;
Expand Down
3 changes: 2 additions & 1 deletion kani-compiler/src/kani_middle/stubbing/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
mod annotations;
mod transform;

use rustc_span::DUMMY_SP;
use std::collections::BTreeMap;
use tracing::{debug, trace};

Expand Down Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/transform/check_values.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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 => {
Expand Down
22 changes: 21 additions & 1 deletion kani-driver/src/call_cargo.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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:?}`",
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
2 changes: 1 addition & 1 deletion tests/cargo-ui/assess-error/expected
Original file line number Diff line number Diff line change
@@ -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
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down

0 comments on commit f5f1e94

Please sign in to comment.