From 3c1ef5f8068166d3bce468c1d496d463b3978041 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 12 Dec 2024 19:46:31 -0500 Subject: [PATCH] Upgrade toolchain to 2024-12-12 (#3774) Upgrade toolchain to 12/12. The only substantive changes are for the 12/10 toolchain; 12/11 and 12/12 are just updating the LLBC tests. Culprit PR: https://github.com/rust-lang/rust/pull/133567 (specifically [this commit](https://github.com/rust-lang/rust/pull/133567/commits/401dd840ff301f13c4006132cc4e4eb80e9702eb) and [this commit](https://github.com/rust-lang/rust/pull/133567/commits/030545d8c3dd13735b2b88d280705d52a1ebf64d)). Resolves #3770 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../codegen_aeneas_llbc/compiler_interface.rs | 15 +--- .../compiler_interface.rs | 12 +-- kani-compiler/src/kani_compiler.rs | 14 +--- kani-compiler/src/main.rs | 7 +- kani-compiler/src/session.rs | 8 +- rust-toolchain.toml | 2 +- tests/expected/llbc/enum/expected | 37 --------- tests/expected/llbc/generic/expected | 52 ------------ tests/expected/llbc/projection/expected | 79 ------------------- tests/expected/llbc/struct/expected | 28 ------- tests/expected/llbc/tuple/expected | 28 ------- 11 files changed, 18 insertions(+), 264 deletions(-) diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs index 0cccda92f3b7..5a5f02969b01 100644 --- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs +++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs @@ -320,23 +320,15 @@ impl CodegenBackend for LlbcCodegenBackend { /// For cases where no metadata file was requested, we stub the file requested by writing the /// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata. /// See for more details. - fn link( - &self, - sess: &Session, - codegen_results: CodegenResults, - outputs: &OutputFilenames, - ) -> Result<(), ErrorGuaranteed> { + fn link(&self, sess: &Session, codegen_results: CodegenResults, outputs: &OutputFilenames) { let requested_crate_types = &codegen_results.crate_info.crate_types.clone(); let local_crate_name = codegen_results.crate_info.local_crate_name; - let link_result = link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs); + link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs); for crate_type in requested_crate_types { let out_fname = out_filename(sess, *crate_type, outputs, local_crate_name); let out_path = out_fname.as_path(); debug!(?crate_type, ?out_path, "link"); - if *crate_type == CrateType::Rlib { - // Emit the `rlib` that contains just one file: `.rmeta` - link_result? - } else { + if *crate_type != CrateType::Rlib { // Write the location of the kani metadata file in the requested compiler output file. let base_filepath = outputs.path(OutputType::Object); let base_filename = base_filepath.as_path(); @@ -347,7 +339,6 @@ impl CodegenBackend for LlbcCodegenBackend { serde_json::to_writer(out_file, &content_stub).unwrap(); } } - Ok(()) } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 6b22b246718a..a0ae5ae99eff 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -30,7 +30,7 @@ use rustc_codegen_ssa::back::link::link_binary; use rustc_codegen_ssa::traits::CodegenBackend; use rustc_codegen_ssa::{CodegenResults, CrateInfo}; use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; -use rustc_errors::{DEFAULT_LOCALE_RESOURCE, ErrorGuaranteed}; +use rustc_errors::DEFAULT_LOCALE_RESOURCE; use rustc_hir::def_id::{DefId as InternalDefId, LOCAL_CRATE}; use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; @@ -414,17 +414,12 @@ impl CodegenBackend for GotocCodegenBackend { /// For other crate types, we stub the file requested by writing the /// path of the `kani-metadata.json` file so `kani-driver` can safely find the latest metadata. /// See for more details. - fn link( - &self, - sess: &Session, - codegen_results: CodegenResults, - outputs: &OutputFilenames, - ) -> Result<(), ErrorGuaranteed> { + fn link(&self, sess: &Session, codegen_results: CodegenResults, outputs: &OutputFilenames) { let requested_crate_types = &codegen_results.crate_info.crate_types.clone(); let local_crate_name = codegen_results.crate_info.local_crate_name; // Create the rlib if one was requested. if requested_crate_types.iter().any(|crate_type| *crate_type == CrateType::Rlib) { - link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs)?; + link_binary(sess, &ArArchiveBuilderBuilder, codegen_results, outputs); } // But override all the other outputs. @@ -445,7 +440,6 @@ impl CodegenBackend for GotocCodegenBackend { serde_json::to_writer(out_file, &content_stub).unwrap(); } } - Ok(()) } } diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs index 93a394aad326..253a9b88a52c 100644 --- a/kani-compiler/src/kani_compiler.rs +++ b/kani-compiler/src/kani_compiler.rs @@ -30,19 +30,14 @@ use rustc_interface::Config; use rustc_middle::ty::TyCtxt; use rustc_session::config::ErrorOutputType; use rustc_smir::rustc_internal; -use rustc_span::ErrorGuaranteed; -use std::process::ExitCode; use std::sync::{Arc, Mutex}; use tracing::debug; /// Run the Kani flavour of the compiler. /// This may require multiple runs of the rustc driver ([RunCompiler::run]). -pub fn run(args: Vec) -> ExitCode { +pub fn run(args: Vec) { let mut kani_compiler = KaniCompiler::new(); - match kani_compiler.run(args) { - Ok(()) => ExitCode::SUCCESS, - Err(_) => ExitCode::FAILURE, - } + kani_compiler.run(args); } /// Configure the LLBC backend (Aeneas's IR). @@ -99,13 +94,12 @@ impl KaniCompiler { /// /// Since harnesses may have different attributes that affect compilation, Kani compiler can /// actually invoke the rust compiler multiple times. - pub fn run(&mut self, args: Vec) -> Result<(), ErrorGuaranteed> { + pub fn run(&mut self, args: Vec) { debug!(?args, "run_compilation_session"); let queries = self.queries.clone(); let mut compiler = RunCompiler::new(&args, self); compiler.set_make_codegen_backend(Some(Box::new(move |_cfg| backend(queries)))); - compiler.run()?; - Ok(()) + compiler.run(); } } diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs index 9558b4159224..65f1a22852b7 100644 --- a/kani-compiler/src/main.rs +++ b/kani-compiler/src/main.rs @@ -51,20 +51,19 @@ mod session; use rustc_driver::{RunCompiler, TimePassesCallbacks}; use std::env; -use std::process::ExitCode; /// Main function. Configure arguments and run the compiler. -fn main() -> ExitCode { +fn main() { session::init_panic_hook(); let (kani_compiler, rustc_args) = is_kani_compiler(env::args().collect()); // Configure and run compiler. if kani_compiler { - kani_compiler::run(rustc_args) + kani_compiler::run(rustc_args); } else { let mut callbacks = TimePassesCallbacks::default(); let compiler = RunCompiler::new(&rustc_args, &mut callbacks); - if compiler.run().is_err() { ExitCode::FAILURE } else { ExitCode::SUCCESS } + compiler.run(); } } diff --git a/kani-compiler/src/session.rs b/kani-compiler/src/session.rs index d56877d11805..f448afb801cc 100644 --- a/kani-compiler/src/session.rs +++ b/kani-compiler/src/session.rs @@ -5,10 +5,9 @@ use crate::args::Arguments; use rustc_data_structures::sync::Lrc; -use rustc_errors::emitter::Emitter; use rustc_errors::{ - ColorConfig, DiagInner, emitter::HumanReadableErrorType, fallback_fluent_bundle, - json::JsonEmitter, + ColorConfig, DiagInner, emitter::Emitter, emitter::HumanReadableErrorType, + fallback_fluent_bundle, json::JsonEmitter, registry::Registry as ErrorRegistry, }; use rustc_session::EarlyDiagCtxt; use rustc_session::config::ErrorOutputType; @@ -64,8 +63,9 @@ static JSON_PANIC_HOOK: LazyLock) + Sync + HumanReadableErrorType::Default, ColorConfig::Never, ); + let registry = ErrorRegistry::new(&[]); let diagnostic = DiagInner::new(rustc_errors::Level::Bug, msg); - emitter.emit_diagnostic(diagnostic); + emitter.emit_diagnostic(diagnostic, ®istry); (*JSON_PANIC_HOOK)(info); })); hook diff --git a/rust-toolchain.toml b/rust-toolchain.toml index b49477fe680a..845a44ebd5f4 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-12-09" +channel = "nightly-2024-12-12" components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/expected/llbc/enum/expected b/tests/expected/llbc/enum/expected index 9d35f16b5205..e69de29bb2d1 100644 --- a/tests/expected/llbc/enum/expected +++ b/tests/expected/llbc/enum/expected @@ -1,37 +0,0 @@ -enum test::MyEnum = -| A(0: i32) -| B() - - -fn test::enum_match(@1: @Adt0) -> i32 -{ - let @0: i32; // return - let e@1: @Adt0; // arg #1 - let i@2: i32; // local - - match e@1 { - 0 => { - i@2 := copy ((e@1 as variant @0).0) - @0 := copy (i@2) - drop i@2 - }, - 1 => { - @0 := const (0 : i32) - }, - } - return -} - -fn test::main() -{ - let @0: (); // return - let e@1: @Adt0; // local - let i@2: i32; // local - - e@1 := test::MyEnum::A { 0: const (1 : i32) } - i@2 := @Fun0(move (e@1)) - drop i@2 - @0 := () - return -} - diff --git a/tests/expected/llbc/generic/expected b/tests/expected/llbc/generic/expected index 8345efd371d4..e69de29bb2d1 100644 --- a/tests/expected/llbc/generic/expected +++ b/tests/expected/llbc/generic/expected @@ -1,52 +0,0 @@ -enum core::option::Option = -| None() -| Some(0: T) - - -fn test::add_opt(@1: @Adt0, @2: @Adt0) -> @Adt0 -{ - let @0: @Adt0; // return - let x@1: @Adt0; // arg #1 - let y@2: @Adt0; // arg #2 - let u@3: i32; // local - let v@4: i32; // local - let @5: i32; // anonymous local - - match x@1 { - 1 => { - u@3 := copy ((x@1 as variant @1).0) - match y@2 { - 1 => { - v@4 := copy ((y@2 as variant @1).0) - @5 := copy (u@3) + copy (v@4) - @0 := core::option::Option::Some { 0: move (@5) } - drop @5 - }, - 0 => { - @0 := core::option::Option::None { } - }, - } - }, - 0 => { - @0 := core::option::Option::None { } - }, - } - return -} - -fn test::main() -{ - let @0: (); // return - let e@1: @Adt0; // local - let @2: @Adt0; // anonymous local - let @3: @Adt0; // anonymous local - - @2 := core::option::Option::Some { 0: const (1 : i32) } - @3 := core::option::Option::Some { 0: const (2 : i32) } - e@1 := @Fun0(move (@2), move (@3)) - drop @3 - drop @2 - drop e@1 - @0 := () - return -} diff --git a/tests/expected/llbc/projection/expected b/tests/expected/llbc/projection/expected index 5753b9f18170..e69de29bb2d1 100644 --- a/tests/expected/llbc/projection/expected +++ b/tests/expected/llbc/projection/expected @@ -1,79 +0,0 @@ -struct test::MyStruct = -{ - a: i32, - b: i32, -} -enum test::MyEnum0 = -| A(0: @Adt1, 1: i32) -| B() -enum test::MyEnum = -| A(0: @Adt1, 1: @Adt2) -| B(0: (i32, i32)) - -fn test::enum_match(@1: @Adt0) -> i32 -{ - let @0: i32; // return - let e@1: @Adt0; // arg #1 - let s@2: @Adt1; // local - let e0@3: @Adt2; // local - let s1@4: @Adt1; // local - let b@5: i32; // local - let @6: i32; // anonymous local - let @7: i32; // anonymous local - let @8: i32; // anonymous local - let a@9: i32; // local - let b@10: i32; // local - match e@1 { - 0 => { - s@2 := move ((e@1 as variant @0).0) - e0@3 := move ((e@1 as variant @0).1) - match e0@3 { - 0 => { - s1@4 := move ((e0@3 as variant @0).0) - b@5 := copy ((e0@3 as variant @0).1) - @6 := copy ((s1@4).a) - @0 := copy (@6) + copy (b@5) - drop @6 - drop s1@4 - drop e0@3 - drop s@2 - }, - 1 => { - @7 := copy ((s@2).a) - @8 := copy ((s@2).b) - @0 := copy (@7) + copy (@8) - drop @8 - drop @7 - drop e0@3 - drop s@2 - }, - } - }, - 1 => { - a@9 := copy (((e@1 as variant @1).0).0) - b@10 := copy (((e@1 as variant @1).0).1) - @0 := copy (a@9) + copy (b@10) - }, - } - return -} -fn test::main() -{ - let @0: (); // return - let s@1: @Adt1; // local - let s0@2: @Adt1; // local - let e@3: @Adt0; // local - let @4: @Adt2; // anonymous local - let i@5: i32; // local - s@1 := @Adt1 { a: const (1 : i32), b: const (2 : i32) } - s0@2 := @Adt1 { a: const (1 : i32), b: const (2 : i32) } - - @4 := test::MyEnum0::A { 0: move (s0@2), 1: const (1 : i32) } - e@3 := test::MyEnum::A { 0: move (s@1), 1: move (@4) } - drop @4 - i@5 := @Fun0(move (e@3)) - drop i@5 - @0 := () - return -} - diff --git a/tests/expected/llbc/struct/expected b/tests/expected/llbc/struct/expected index a81e73b38895..e69de29bb2d1 100644 --- a/tests/expected/llbc/struct/expected +++ b/tests/expected/llbc/struct/expected @@ -1,28 +0,0 @@ -struct test::MyStruct = -{ - a: i32, - b: bool, -} - -fn test::struct_project(@1: @Adt0) -> i32 -{ - let @0: i32; // return - let s@1: @Adt0; // arg #1 - - @0 := copy ((s@1).a) - return -} - -fn test::main() -{ - let @0: (); // return - let s@1: @Adt0; // local - let a@2: i32; // local - - s@1 := @Adt0 { a: const (1 : i32), b: const (true) } - a@2 := @Fun0(move (s@1)) - drop a@2 - @0 := () - return -} - diff --git a/tests/expected/llbc/tuple/expected b/tests/expected/llbc/tuple/expected index d6fa6330ca88..e69de29bb2d1 100644 --- a/tests/expected/llbc/tuple/expected +++ b/tests/expected/llbc/tuple/expected @@ -1,28 +0,0 @@ -fn test::tuple_add(@1: (i32, i32)) -> i32 -{ - let @0: i32; // return - let t@1: (i32, i32); // arg #1 - let @2: i32; // anonymous local - let @3: i32; // anonymous local - - @2 := copy ((t@1).0) - @3 := copy ((t@1).1) - @0 := copy (@2) + copy (@3) - drop @3 - drop @2 - return -} - -fn test::main() -{ - let @0: (); // return - let s@1: i32; // local - let @2: (i32, i32); // anonymous local - - @2 := (const (1 : i32), const (2 : i32)) - s@1 := @Fun0(move (@2)) - drop @2 - drop s@1 - @0 := () - return -}