From f11e591185b6ca525843bc05157c34f66a22fa47 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Thu, 21 Mar 2024 21:13:32 +0000 Subject: [PATCH 1/7] Upgrade toolchain to `nightly-2024-03-21` --- .../src/codegen_cprover_gotoc/compiler_interface.rs | 6 ++++-- kani-compiler/src/kani_compiler.rs | 9 +++++---- kani-compiler/src/kani_middle/reachability.rs | 3 ++- kani-compiler/src/kani_middle/stubbing/mod.rs | 3 ++- rust-toolchain.toml | 2 +- 5 files changed, 14 insertions(+), 9 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index cad8bcbfb9ce..7e93d2307887 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/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), }; diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 48b4318db5bf..f74c67bb8bbe 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() @@ -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 2fa1bf057c1c..f4134a097df5 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/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 {{")?; 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/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"] From fd5c742c5be86954343054c2d0f4d538509861d1 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Fri, 22 Mar 2024 15:32:18 +0000 Subject: [PATCH 2/7] Change lib name expected from `cargo` error --- tests/cargo-ui/assess-error/expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 From 1890d6e28e1d39058692ef13244150285cf8f15f Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 26 Mar 2024 22:24:48 +0000 Subject: [PATCH 3/7] Allow weaker comparison for targets --- kani-compiler/src/kani_compiler.rs | 2 +- kani-driver/src/call_cargo.rs | 21 ++++++++++++++++++++- 2 files changed, 21 insertions(+), 2 deletions(-) diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index f74c67bb8bbe..fc5f5891ecae 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -377,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 { diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index b68d18c84a40..4981a0f2c466 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -211,7 +211,26 @@ 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. + if same_target(&rustc_artifact.target, target) { debug_assert!( artifact.is_none(), "expected only one artifact for `{target:?}`", From d7ad90979ab264ad0a994cc8925668342fcfc918 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 26 Mar 2024 22:33:58 +0000 Subject: [PATCH 4/7] Add issue and make `clippy` happy --- kani-driver/src/call_cargo.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index 4981a0f2c466..d033c5ea00d4 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -215,7 +215,7 @@ impl KaniSession { /// 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.name.replace('-', '_') == t2.name.replace('-', '_') && t1.kind == t2.kind && t1.src_path == t2.src_path && t1.edition == t2.edition @@ -230,6 +230,7 @@ impl KaniSession { // 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(), From 4a426c6eb858d8cf4e7b4625adac4fda31a8a31e Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 26 Mar 2024 22:40:18 +0000 Subject: [PATCH 5/7] Last fixes --- kani-driver/src/call_cargo.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs index d033c5ea00d4..9d27e5853696 100644 --- a/kani-driver/src/call_cargo.rs +++ b/kani-driver/src/call_cargo.rs @@ -215,7 +215,7 @@ impl KaniSession { /// 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.name.replace('-', "_") == t2.name.replace('-', "_") && t1.kind == t2.kind && t1.src_path == t2.src_path && t1.edition == t2.edition From 623cb88337f46605fd98c140b79810ad9f3ccace Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Tue, 26 Mar 2024 23:10:12 +0000 Subject: [PATCH 6/7] add `expect` to validity check --- kani-compiler/src/kani_middle/transform/check_values.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 => { From 8f977a33e152b141b9b84f7bd7e43d6472cb730d Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Wed, 27 Mar 2024 19:20:16 +0000 Subject: [PATCH 7/7] Convert into "fixme" and refer to issue --- .../ValidValues/{write_invalid.rs => write_invalid_fixme.rs} | 3 +++ 1 file changed, 3 insertions(+) rename tests/kani/ValidValues/{write_invalid.rs => write_invalid_fixme.rs} (88%) 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]