Upgrade toolchain to 2024-12-12

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 <https://github.com/model-checking/kani/issues/2234> 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: `<crate>.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(())
     }
 }
 

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 <https://github.com/model-checking/kani/issues/2234> 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(())
     }
 }
 

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<String>) -> ExitCode {
+pub fn run(args: Vec<String>) {
     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<String>) -> Result<(), ErrorGuaranteed> {
+    pub fn run(&mut self, args: Vec<String>) {
         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();
     }
 }
 

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();
     }
 }
 

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<Box<dyn Fn(&panic::PanicHookInfo<'_>) + 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, &registry);
             (*JSON_PANIC_HOOK)(info);
         }));
         hook

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"]

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
-}
-

tests/expected/llbc/generic/expected

@@ -1,52 +0,0 @@
-enum core::option::Option<T> =
-|  None()
-|  Some(0: T)
-
-
-fn test::add_opt(@1: @Adt0<i32>, @2: @Adt0<i32>) -> @Adt0<i32>
-{
-    let @0: @Adt0<i32>; // return
-    let x@1: @Adt0<i32>; // arg #1
-    let y@2: @Adt0<i32>; // 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<i32>; // local
-    let @2: @Adt0<i32>; // anonymous local
-    let @3: @Adt0<i32>; // 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
-}

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
-}
-

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
-}
-

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
-}