Update toolchain to 2/1 - functionality changes

  - vtable changes: rust-lang/rust#135318
  - NullPointerDereference changes: rust-lang/rust#134424

Author: carolynzech

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -1505,8 +1505,10 @@ impl GotocCtx<'_> {
             |ctx, var| {
                 // Build the vtable, using Rust's vtable_entries to determine field order
                 let vtable_entries = if let Some(principal) = trait_type.kind().trait_principal() {
-                    let trait_ref_binder = principal.with_self_ty(src_mir_type);
-                    ctx.tcx.vtable_entries(rustc_internal::internal(ctx.tcx, trait_ref_binder))
+                    let trait_ref =
+                        rustc_internal::internal(ctx.tcx, principal.with_self_ty(src_mir_type));
+                    let trait_ref = ctx.tcx.instantiate_bound_regions_with_erased(trait_ref);
+                    ctx.tcx.vtable_entries(trait_ref)
                 } else {
                     TyCtxt::COMMON_VTABLE_ENTRIES
                 };

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -371,6 +371,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // The virtual methods on the trait ref. Some auto traits have no methods.
             if let Some(principal) = binder.principal() {
                 let poly = principal.with_self_ty(self.tcx, t);
+                let poly = self.tcx.instantiate_bound_regions_with_erased(poly);
                 let poly = self.tcx.erase_regions(poly);
                 let mut flds = self
                     .tcx

kani-compiler/src/kani_middle/reachability.rs

@@ -256,11 +256,11 @@ impl MonoItemsFnCollector<'_, '_> {
             // A trait object type can have multiple trait bounds but up to one non-auto-trait
             // bound. This non-auto-trait, named principal, is the only one that can have methods.
             // https://doc.rust-lang.org/reference/special-types-and-traits.html#auto-traits
-            let poly_trait_ref = principal.with_self_ty(concrete_ty);
+            let trait_ref = rustc_internal::internal(self.tcx, principal.with_self_ty(concrete_ty));
+            let trait_ref = self.tcx.instantiate_bound_regions_with_erased(trait_ref);
 
             // Walk all methods of the trait, including those of its supertraits
-            let entries =
-                self.tcx.vtable_entries(rustc_internal::internal(self.tcx, &poly_trait_ref));
+            let entries = self.tcx.vtable_entries(trait_ref);
             let methods = entries.iter().filter_map(|entry| match entry {
                 VtblEntry::MetadataAlign
                 | VtblEntry::MetadataDropInPlace

kani-compiler/src/kani_middle/transform/internal_mir.rs

@@ -558,6 +558,9 @@ impl RustcInternalMir for AssertMessage {
                     found: found.internal_mir(tcx),
                 }
             }
+            AssertMessage::NullPointerDereference => {
+                rustc_middle::mir::AssertMessage::NullPointerDereference
+            }
         }
     }
 }

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-01-29"
+channel = "nightly-2025-02-01"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/uninit/multiple-instrumentations.expected

@@ -1,16 +1,16 @@
-multiple_instrumentations_different_vars.assertion.3\
+multiple_instrumentations_different_vars.assertion\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-multiple_instrumentations_different_vars.assertion.4\
+multiple_instrumentations_different_vars.assertion\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"
 
-multiple_instrumentations.assertion.2\
+multiple_instrumentations.assertion\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-multiple_instrumentations.assertion.3\
+multiple_instrumentations.assertion\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 

tests/expected/zst/expected

@@ -1,4 +1,5 @@
-Status: FAILURE\
-Description: "dereference failure: pointer NULL"
+assertion\
+    - Status: FAILURE\
+    - Description: "null pointer dereference occured"
 
 VERIFICATION:- FAILED