Upgrade toolchain to 2024-12-09 (model-checking#3768)

Upgrade toolchain to 12/09.

Culprit PRs:
- rust-lang/rust#132410
- rust-lang/rust#133746
- Unnecessary `map_or` [clippy
lint](https://rust-lang.github.io/rust-clippy/master/index.html#unnecessary_map_or)

As with previous toolchain upgrades, it's unclear why the LLBC tests
regressed.

Resolves model-checking#3754

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

kani-compiler/src/kani_compiler.rs

@@ -27,6 +27,7 @@ use clap::Parser;
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_driver::{Callbacks, Compilation, RunCompiler};
 use rustc_interface::Config;
+use rustc_middle::ty::TyCtxt;
 use rustc_session::config::ErrorOutputType;
 use rustc_smir::rustc_internal;
 use rustc_span::ErrorGuaranteed;
@@ -124,17 +125,15 @@ impl Callbacks for KaniCompiler {
     }
 
     /// After analysis, we check the crate items for Kani API misuse or configuration issues.
-    fn after_analysis<'tcx>(
+    fn after_analysis(
         &mut self,
         _compiler: &rustc_interface::interface::Compiler,
-        rustc_queries: &'tcx rustc_interface::Queries<'tcx>,
+        tcx: TyCtxt<'_>,
     ) -> Compilation {
-        rustc_queries.global_ctxt().unwrap().enter(|tcx| {
-            rustc_internal::run(tcx, || {
-                check_crate_items(tcx, self.queries.lock().unwrap().args().ignore_global_asm);
-            })
-            .unwrap()
-        });
+        rustc_internal::run(tcx, || {
+            check_crate_items(tcx, self.queries.lock().unwrap().args().ignore_global_asm);
+        })
+        .unwrap();
         Compilation::Continue
     }
 }

kani-compiler/src/kani_middle/attributes.rs

@@ -673,12 +673,12 @@ fn expect_key_string_value(
     attr: &Attribute,
 ) -> Result<rustc_span::Symbol, ErrorGuaranteed> {
     let span = attr.span;
-    let AttrArgs::Eq(_, it) = &attr.get_normal_item().args else {
+    let AttrArgs::Eq { eq_span: _, value } = &attr.get_normal_item().args else {
         return Err(sess
             .dcx()
             .span_err(span, "Expected attribute of the form #[attr = \"value\"]"));
     };
-    let maybe_str = match it {
+    let maybe_str = match value {
         AttrArgsEq::Ast(expr) => {
             if let ExprKind::Lit(tok) = expr.kind {
                 match LitKind::from_token_lit(tok) {

kani-driver/src/project.rs

@@ -76,7 +76,7 @@ impl Project {
         trace!(?harness.goto_file, ?expected_path, ?typ, "get_harness_artifact");
         self.artifacts.iter().find(|artifact| {
             artifact.has_type(typ)
-                && expected_path.as_ref().map_or(true, |goto_file| *goto_file == artifact.path)
+                && expected_path.as_ref().is_none_or(|goto_file| *goto_file == artifact.path)
         })
     }
 

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-11-28"
+channel = "nightly-2024-12-09"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/llbc/enum/expected

@@ -29,7 +29,7 @@ fn test::main()
     let i@2: i32; // local
 
     e@1 := test::MyEnum::A { 0: const (1 : i32) }
-    i@2 := @Fun1(move (e@1))
+    i@2 := @Fun0(move (e@1))
     drop i@2
     @0 := ()
     return

tests/expected/llbc/generic/expected

@@ -43,7 +43,7 @@ fn test::main()
 
     @2 := core::option::Option::Some { 0: const (1 : i32) }
     @3 := core::option::Option::Some { 0: const (2 : i32) }
-    e@1 := @Fun1(move (@2), move (@3))
+    e@1 := @Fun0(move (@2), move (@3))
     drop @3
     drop @2
     drop e@1

tests/expected/llbc/projection/expected

@@ -4,18 +4,19 @@ struct test::MyStruct =
   b: i32,
 }
 enum test::MyEnum0 =
-|  A(0: @Adt0, 1: i32)
+|  A(0: @Adt1, 1: i32)
 |  B()
 enum test::MyEnum =
-|  A(0: @Adt0, 1: @Adt2)
+|  A(0: @Adt1, 1: @Adt2)
 |  B(0: (i32, i32))
-fn test::enum_match(@1: @Adt1) -> i32
+
+fn test::enum_match(@1: @Adt0) -> i32
 {
     let @0: i32; // return
-    let e@1: @Adt1; // arg #1
-    let s@2: @Adt0; // local
+    let e@1: @Adt0; // arg #1
+    let s@2: @Adt1; // local
     let e0@3: @Adt2; // local
-    let s1@4: @Adt0; // local
+    let s1@4: @Adt1; // local
     let b@5: i32; // local
     let @6: i32; // anonymous local
     let @7: i32; // anonymous local
@@ -59,17 +60,18 @@ fn test::enum_match(@1: @Adt1) -> i32
 fn test::main()
 {
     let @0: (); // return
-    let s@1: @Adt0; // local
-    let s0@2: @Adt0; // local
-    let e@3: @Adt1; // local
+    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 := @Adt0 { a: const (1 : i32), b: const (2 : i32) }
-    s0@2 := @Adt0 { a: const (1 : i32), b: const (2 : i32) }
+    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 := @Fun1(move (e@3))
+    i@5 := @Fun0(move (e@3))
     drop i@5
     @0 := ()
     return

tests/expected/llbc/tuple/expected

@@ -20,7 +20,7 @@ fn test::main()
     let @2: (i32, i32); // anonymous local
 
     @2 := (const (1 : i32), const (2 : i32))
-    s@1 := @Fun1(move (@2))
+    s@1 := @Fun0(move (@2))
     drop @2
     drop s@1
     @0 := ()