Update toolchain to nightly-2024-11-26

kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs

@@ -46,7 +46,7 @@ use charon_lib::ullbc_ast::{
 use charon_lib::{error_assert, error_or_panic};
 use core::panic;
 use rustc_data_structures::fx::FxHashMap;
-use rustc_middle::ty::TyCtxt;
+use rustc_middle::ty::{TyCtxt, TypingEnv};
 use rustc_smir::rustc_internal;
 use stable_mir::abi::PassMode;
 use stable_mir::mir::mono::{Instance, InstanceDef};
@@ -226,7 +226,8 @@ impl<'a, 'tcx> Context<'a, 'tcx> {
                 GenericArgKind::Const(tc) => match tc.kind() {
                     TyConstKind::Param(paramtc) => {
                         let def_id_internal = rustc_internal::internal(self.tcx, adtdef.def_id());
-                        let paramenv = self.tcx.param_env(def_id_internal);
+                        let paramenv =
+                            TypingEnv::post_analysis(self.tcx, def_id_internal).param_env;
                         let pc_internal = rustc_middle::ty::ParamConst {
                             index: paramtc.index,
                             name: rustc_span::Symbol::intern(&paramtc.name),

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

@@ -10,7 +10,7 @@ use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{
     ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type,
 };
-use rustc_middle::ty::ParamEnv;
+use rustc_middle::ty::TypingEnv;
 use rustc_middle::ty::layout::ValidityRequirement;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
@@ -730,15 +730,15 @@ impl GotocCtx<'_> {
             );
         }
 
-        let param_env_and_type =
-            ParamEnv::reveal_all().and(rustc_internal::internal(self.tcx, target_ty));
+        let typing_env_and_type = TypingEnv::fully_monomorphized()
+            .as_query_input(rustc_internal::internal(self.tcx, target_ty));
 
         // Then we check if the type allows "raw" initialization for the cases
         // where memory is zero-initialized or entirely uninitialized
         if intrinsic == "assert_zero_valid"
             && !self
                 .tcx
-                .check_validity_requirement((ValidityRequirement::Zero, param_env_and_type))
+                .check_validity_requirement((ValidityRequirement::Zero, typing_env_and_type))
                 .unwrap()
         {
             return self.codegen_fatal_error(
@@ -756,7 +756,7 @@ impl GotocCtx<'_> {
                 .tcx
                 .check_validity_requirement((
                     ValidityRequirement::UninitMitigated0x01Fill,
-                    param_env_and_type,
+                    typing_env_and_type,
                 ))
                 .unwrap()
         {

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

@@ -18,7 +18,7 @@ use cbmc::goto_program::{
 };
 use cbmc::{InternString, InternedString, btree_string_map};
 use num::bigint::BigInt;
-use rustc_middle::ty::{ParamEnv, TyCtxt, VtblEntry};
+use rustc_middle::ty::{TyCtxt, TypingEnv, VtblEntry};
 use rustc_smir::rustc_internal;
 use rustc_target::abi::{FieldsShape, TagEncoding, Variants};
 use stable_mir::abi::{Primitive, Scalar, ValueAbi};
@@ -832,7 +832,7 @@ impl GotocCtx<'_> {
                     NullOp::OffsetOf(fields) => Expr::int_constant(
                         self.tcx
                             .offset_of_subfield(
-                                ParamEnv::reveal_all(),
+                                TypingEnv::fully_monomorphized(),
                                 layout,
                                 fields.iter().map(|(var_idx, field_idx)| {
                                     (

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

@@ -8,7 +8,7 @@ use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use rustc_middle::ty::layout::LayoutOf;
-use rustc_middle::ty::{List, ParamEnv};
+use rustc_middle::ty::{List, TypingEnv};
 use rustc_smir::rustc_internal;
 use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
 use stable_mir::abi::{ArgAbi, FnAbi, PassMode};
@@ -663,7 +663,8 @@ impl GotocCtx<'_> {
                 let fn_ptr_abi = rustc_internal::stable(
                     self.tcx
                         .fn_abi_of_fn_ptr(
-                            ParamEnv::reveal_all().and((fn_sig_internal, &List::empty())),
+                            TypingEnv::fully_monomorphized()
+                                .as_query_input((fn_sig_internal, &List::empty())),
                         )
                         .unwrap(),
                 );

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

@@ -229,7 +229,7 @@ impl<'tcx> GotocCtx<'tcx> {
         if let Some(current_fn) = &self.current_fn {
             current_fn.instance().instantiate_mir_and_normalize_erasing_regions(
                 self.tcx,
-                ty::ParamEnv::reveal_all(),
+                ty::TypingEnv::fully_monomorphized(),
                 ty::EarlyBinder::bind(value),
             )
         } else {
@@ -251,7 +251,7 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn is_unsized(&self, t: Ty<'tcx>) -> bool {
         !self
             .monomorphize(t)
-            .is_sized(*self.tcx.at(rustc_span::DUMMY_SP), ty::ParamEnv::reveal_all())
+            .is_sized(*self.tcx.at(rustc_span::DUMMY_SP), ty::TypingEnv::fully_monomorphized())
     }
 
     /// Generates the type for a single field for a dynamic vtable.
@@ -523,7 +523,8 @@ impl<'tcx> GotocCtx<'tcx> {
     ///      c.f. <https://rust-lang.github.io/unsafe-code-guidelines/introduction.html>
     pub fn codegen_ty(&mut self, ty: Ty<'tcx>) -> Type {
         // TODO: Remove all monomorphize calls
-        let normalized = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), ty);
+        let normalized =
+            self.tcx.normalize_erasing_regions(ty::TypingEnv::fully_monomorphized(), ty);
         let goto_typ = self.codegen_ty_inner(normalized);
         if let Some(tag) = goto_typ.tag() {
             self.type_map.entry(tag).or_insert_with(|| {
@@ -573,10 +574,14 @@ impl<'tcx> GotocCtx<'tcx> {
             ty::Str => Type::unsigned_int(8).flexible_array_of(),
             ty::Ref(_, t, _) | ty::RawPtr(t, _) => self.codegen_ty_ref(*t),
             ty::FnDef(def_id, args) => {
-                let instance =
-                    Instance::try_resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
-                        .unwrap()
-                        .unwrap();
+                let instance = Instance::try_resolve(
+                    self.tcx,
+                    ty::TypingEnv::fully_monomorphized(),
+                    *def_id,
+                    args,
+                )
+                .unwrap()
+                .unwrap();
                 self.codegen_fndef_type(instance)
             }
             ty::FnPtr(sig_tys, hdr) => {
@@ -980,7 +985,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // Normalize pointee_type to remove projection and opaque types
         trace!(?pointee_type, "codegen_ty_ref");
         let pointee_type =
-            self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), pointee_type);
+            self.tcx.normalize_erasing_regions(ty::TypingEnv::fully_monomorphized(), pointee_type);
 
         if !self.use_thin_pointer(pointee_type) {
             return self.codegen_fat_ptr(pointee_type);
@@ -1076,7 +1081,9 @@ impl<'tcx> GotocCtx<'tcx> {
     /// one can only apply this function to a monomorphized signature
     pub fn codegen_function_sig(&mut self, sig: PolyFnSig<'tcx>) -> Type {
         let sig = self.monomorphize(sig);
-        let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig);
+        let sig = self
+            .tcx
+            .normalize_erasing_late_bound_regions(ty::TypingEnv::fully_monomorphized(), sig);
         self.codegen_function_sig_stable(rustc_internal::stable(sig))
     }
 

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -29,8 +29,8 @@ use cbmc::{InternedString, MachineModel};
 use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::span_bug;
 use rustc_middle::ty::layout::{
-    FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers,
-    TyAndLayout,
+    FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasTyCtxt, HasTypingEnv, LayoutError,
+    LayoutOfHelpers, TyAndLayout,
 };
 use rustc_middle::ty::{self, Ty, TyCtxt};
 use rustc_span::Span;
@@ -337,9 +337,9 @@ impl<'tcx> LayoutOfHelpers<'tcx> for GotocCtx<'tcx> {
     }
 }
 
-impl<'tcx> HasParamEnv<'tcx> for GotocCtx<'tcx> {
-    fn param_env(&self) -> ty::ParamEnv<'tcx> {
-        ty::ParamEnv::reveal_all()
+impl<'tcx> HasTypingEnv<'tcx> for GotocCtx<'tcx> {
+    fn typing_env(&self) -> ty::TypingEnv<'tcx> {
+        ty::TypingEnv::fully_monomorphized()
     }
 }
 

kani-compiler/src/kani_middle/coercion.rs

@@ -17,7 +17,7 @@ use rustc_hir::lang_items::LangItem;
 use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::TraitRef;
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
-use rustc_middle::ty::{ParamEnv, Ty, TyCtxt};
+use rustc_middle::ty::{PseudoCanonicalInput, Ty, TyCtxt, TypingEnv};
 use rustc_smir::rustc_internal;
 use stable_mir::Symbol;
 use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
@@ -102,7 +102,7 @@ pub fn extract_unsize_casting<'tcx>(
     let (src_base_ty, dst_base_ty) = tcx.struct_lockstep_tails_for_codegen(
         src_pointee_ty,
         dst_pointee_ty,
-        ParamEnv::reveal_all(),
+        TypingEnv::fully_monomorphized(),
     );
     trace!(?src_base_ty, ?dst_base_ty, "extract_unsize_casting result");
     assert!(
@@ -251,7 +251,10 @@ fn custom_coerce_unsize_info<'tcx>(
 
     let trait_ref = TraitRef::new(tcx, def_id, tcx.mk_args_trait(source_ty, [target_ty.into()]));
 
-    match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) {
+    match tcx.codegen_select_candidate(PseudoCanonicalInput {
+        typing_env: TypingEnv::fully_monomorphized(),
+        value: trait_ref,
+    }) {
         Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, .. })) => {
             tcx.coerce_unsized_info(impl_def_id).unwrap().custom_kind.unwrap()
         }

kani-compiler/src/kani_middle/points_to/points_to_analysis.rs

@@ -38,7 +38,7 @@ use rustc_middle::{
         ProjectionElem, Rvalue, Statement, StatementKind, Terminator, TerminatorEdges,
         TerminatorKind,
     },
-    ty::{Instance, InstanceKind, List, ParamEnv, TyCtxt, TyKind},
+    ty::{Instance, InstanceKind, List, TyCtxt, TyKind, TypingEnv},
 };
 use rustc_mir_dataflow::{Analysis, Forward, JoinSemiLattice};
 use rustc_smir::rustc_internal;
@@ -179,6 +179,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> {
             | StatementKind::AscribeUserType(..)
             | StatementKind::Coverage(..)
             | StatementKind::ConstEvalCounter
+            | StatementKind::BackwardIncompatibleDropHint { .. }
             | StatementKind::Nop => { /* This is a no-op with regard to aliasing. */ }
         }
     }
@@ -356,7 +357,13 @@ fn try_resolve_instance<'tcx>(
         TyKind::FnDef(def, args) => {
             // Span here is used for error-reporting, which we don't expect to encounter anyway, so
             // it is ok to use a dummy.
-            Ok(Instance::expect_resolve(tcx, ParamEnv::reveal_all(), *def, &args, DUMMY_SP))
+            Ok(Instance::expect_resolve(
+                tcx,
+                TypingEnv::fully_monomorphized(),
+                *def,
+                &args,
+                DUMMY_SP,
+            ))
         }
         _ => Err(format!(
             "Kani was not able to resolve the instance of the function operand `{ty:?}`. Currently, memory initialization checks in presence of function pointers and vtable calls are not supported. For more information about planned support, see https://github.com/model-checking/kani/issues/3300."

kani-compiler/src/kani_middle/stubbing/mod.rs

@@ -12,7 +12,7 @@ use tracing::{debug, trace};
 use kani_metadata::HarnessMetadata;
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::Const;
-use rustc_middle::ty::{self, EarlyBinder, ParamEnv, TyCtxt, TypeFoldable};
+use rustc_middle::ty::{self, EarlyBinder, TyCtxt, TypeFoldable, TypingEnv};
 use rustc_smir::rustc_internal;
 use stable_mir::mir::ConstOperand;
 use stable_mir::mir::mono::Instance;
@@ -152,7 +152,7 @@ impl<'tcx> StubConstChecker<'tcx> {
         trace!(instance=?self.instance, ?value, "monomorphize");
         self.instance.instantiate_mir_and_normalize_erasing_regions(
             self.tcx,
-            ParamEnv::reveal_all(),
+            TypingEnv::fully_monomorphized(),
             EarlyBinder::bind(value),
         )
     }
@@ -171,7 +171,11 @@ impl MirVisitor for StubConstChecker<'_> {
             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, DUMMY_SP).is_err() {
+                if self
+                    .tcx
+                    .const_eval_resolve(TypingEnv::fully_monomorphized(), un_eval, DUMMY_SP)
+                    .is_err()
+                {
                     // The `monomorphize` call should have evaluated that constant already.
                     let tcx = self.tcx;
                     let mono_const = &un_eval;

rust-toolchain.toml

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

tests/expected/llbc/enum/expected

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

tests/expected/llbc/projection/expected

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

tests/expected/llbc/struct/expected

@@ -20,8 +20,9 @@ fn test::main()
     let a@2: i32; // local
 
     s@1 := @Adt0 { a: const (1 : i32), b: const (true) }
-    a@2 := @Fun1(move (s@1))
+    a@2 := @Fun0(move (s@1))
     drop a@2
     @0 := ()
     return
 }
+