From b9f695c57ba73ec4b254bf8ac40ea4c756882333 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 26 Nov 2024 12:21:29 -0800
Subject: [PATCH 1/3] Cleanup a few internal compiler deps

Some of this code was broken by the toolchain update.
Instead of changing it, replace it by StableMIR APIs.
---
 .../codegen/ty_stable.rs                      |  8 +-
 kani-compiler/src/kani_middle/abi.rs          |  5 ++
 kani-compiler/src/kani_middle/attributes.rs   |  5 +-
 kani-compiler/src/kani_middle/mod.rs          | 85 +------------------
 4 files changed, 14 insertions(+), 89 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
index 7e644cdecb77..7262f55a0719 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
@@ -7,8 +7,9 @@
 //! `typ.rs`.
 
 use crate::codegen_cprover_gotoc::GotocCtx;
+use crate::kani_middle::abi::LayoutOf;
 use cbmc::goto_program::Type;
-use rustc_middle::ty::layout::{LayoutOf, TyAndLayout};
+use rustc_middle::ty::layout::{LayoutOf as _, TyAndLayout};
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Local, Operand, Place, Rvalue};
@@ -36,7 +37,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn is_zst_stable(&self, ty: Ty) -> bool {
-        self.is_zst(rustc_internal::internal(self.tcx, ty))
+        LayoutOf::new(ty).is_zst()
     }
 
     pub fn layout_of_stable(&self, ty: Ty) -> TyAndLayout<'tcx> {
@@ -113,7 +114,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// This should be replaced by StableMIR `pretty_ty()` after
     /// <https://github.com/rust-lang/rust/pull/118364> is merged.
     pub fn pretty_ty(&self, ty: Ty) -> String {
-        rustc_internal::internal(self.tcx, ty).to_string()
+        ty.to_string()
     }
 
     pub fn requires_caller_location(&self, instance: Instance) -> bool {
@@ -121,6 +122,7 @@ impl<'tcx> GotocCtx<'tcx> {
         instance_internal.def.requires_caller_location(self.tcx)
     }
 }
+
 /// If given type is a Ref / Raw ref, return the pointee type.
 pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
     match mir_type.kind() {
diff --git a/kani-compiler/src/kani_middle/abi.rs b/kani-compiler/src/kani_middle/abi.rs
index 88068458a028..12fac6c8a43f 100644
--- a/kani-compiler/src/kani_middle/abi.rs
+++ b/kani-compiler/src/kani_middle/abi.rs
@@ -24,6 +24,11 @@ impl LayoutOf {
         self.layout.is_sized()
     }
 
+    /// Return whether this is a zero-sized type
+    pub fn is_zst(&self) -> bool {
+        self.is_sized() && self.layout.size.bytes() == 0
+    }
+
     /// Return whether the type is unsized and its tail is a foreign item.
     ///
     /// This will also return `true` if the type is foreign.
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 3ee695e6f481..c699ced8a0ab 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -622,8 +622,9 @@ impl<'tcx> KaniAttributes<'tcx> {
                 ),
             );
         } else {
-            let instance = Instance::mono(tcx, self.item);
-            if !super::fn_abi(tcx, instance).args.is_empty() {
+            let instance = rustc_internal::stable(Instance::mono(tcx, self.item));
+            let fn_abi = instance.fn_abi().unwrap();
+            if !fn_abi.args.is_empty() {
                 tcx.dcx().span_err(span, "functions used as harnesses cannot have any arguments");
             }
         }
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 62714bbe477c..dbdd421fcc36 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -7,17 +7,8 @@ use std::collections::HashSet;
 
 use crate::kani_queries::QueryDb;
 use rustc_hir::{def::DefKind, def_id::DefId as InternalDefId, def_id::LOCAL_CRATE};
-use rustc_middle::span_bug;
-use rustc_middle::ty::layout::{
-    FnAbiError, FnAbiOf, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError,
-    LayoutOfHelpers, TyAndLayout,
-};
-use rustc_middle::ty::{self, Instance as InstanceInternal, Ty as TyInternal, TyCtxt};
+use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
-use rustc_span::Span;
-use rustc_span::source_map::respan;
-use rustc_target::abi::call::FnAbi;
-use rustc_target::abi::{HasDataLayout, TargetDataLayout};
 use stable_mir::CrateDef;
 use stable_mir::mir::mono::MonoItem;
 use stable_mir::ty::{FnDef, RigidTy, Span as SpanStable, Ty, TyKind};
@@ -155,80 +146,6 @@ impl SourceLocation {
     }
 }
 
-/// Get the FnAbi of a given instance with no extra variadic arguments.
-/// TODO: Get rid of this. Use instance.fn_abi() instead.
-/// <https://github.com/model-checking/kani/issues/1365>
-pub fn fn_abi<'tcx>(
-    tcx: TyCtxt<'tcx>,
-    instance: InstanceInternal<'tcx>,
-) -> &'tcx FnAbi<'tcx, TyInternal<'tcx>> {
-    let helper = CompilerHelpers { tcx };
-    helper.fn_abi_of_instance(instance, ty::List::empty())
-}
-
-struct CompilerHelpers<'tcx> {
-    tcx: TyCtxt<'tcx>,
-}
-
-impl<'tcx> HasParamEnv<'tcx> for CompilerHelpers<'tcx> {
-    fn param_env(&self) -> ty::ParamEnv<'tcx> {
-        ty::ParamEnv::reveal_all()
-    }
-}
-
-impl<'tcx> HasTyCtxt<'tcx> for CompilerHelpers<'tcx> {
-    fn tcx(&self) -> TyCtxt<'tcx> {
-        self.tcx
-    }
-}
-
-impl HasDataLayout for CompilerHelpers<'_> {
-    fn data_layout(&self) -> &TargetDataLayout {
-        self.tcx.data_layout()
-    }
-}
-
-impl<'tcx> LayoutOfHelpers<'tcx> for CompilerHelpers<'tcx> {
-    type LayoutOfResult = TyAndLayout<'tcx>;
-
-    #[inline]
-    fn handle_layout_err(&self, err: LayoutError<'tcx>, span: Span, ty: TyInternal<'tcx>) -> ! {
-        span_bug!(span, "failed to get layout for `{}`: {}", ty, err)
-    }
-}
-
-/// Implement error handling for extracting function ABI information.
-impl<'tcx> FnAbiOfHelpers<'tcx> for CompilerHelpers<'tcx> {
-    type FnAbiOfResult = &'tcx FnAbi<'tcx, TyInternal<'tcx>>;
-
-    #[inline]
-    fn handle_fn_abi_err(
-        &self,
-        err: FnAbiError<'tcx>,
-        span: Span,
-        fn_abi_request: FnAbiRequest<'tcx>,
-    ) -> ! {
-        if let FnAbiError::Layout(LayoutError::SizeOverflow(_)) = err {
-            self.tcx.dcx().emit_fatal(respan(span, err))
-        } else {
-            match fn_abi_request {
-                FnAbiRequest::OfFnPtr { sig, extra_args } => {
-                    span_bug!(
-                        span,
-                        "Error: {err:?}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`",
-                    );
-                }
-                FnAbiRequest::OfInstance { instance, extra_args } => {
-                    span_bug!(
-                        span,
-                        "Error: {err:?}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`",
-                    );
-                }
-            }
-        }
-    }
-}
-
 /// Try to convert an internal `DefId` to a `FnDef`.
 pub fn stable_fn_def(tcx: TyCtxt, def_id: InternalDefId) -> Option<FnDef> {
     if let TyKind::RigidTy(RigidTy::FnDef(def, _)) =

From 7cef50cebe2c40044b281a1ab4e135521e3bf079 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 26 Nov 2024 12:48:20 -0800
Subject: [PATCH 2/3] Update toolchain to nightly-2024-11-26

---
 .../codegen_aeneas_llbc/mir_to_ullbc/mod.rs   |  5 ++--
 .../codegen/intrinsic.rs                      | 10 ++++----
 .../codegen_cprover_gotoc/codegen/rvalue.rs   |  4 +--
 .../codegen/statement.rs                      |  5 ++--
 .../src/codegen_cprover_gotoc/codegen/typ.rs  | 25 ++++++++++++-------
 .../codegen_cprover_gotoc/context/goto_ctx.rs | 10 ++++----
 kani-compiler/src/kani_middle/coercion.rs     |  9 ++++---
 .../points_to/points_to_analysis.rs           | 11 ++++++--
 kani-compiler/src/kani_middle/stubbing/mod.rs | 10 +++++---
 rust-toolchain.toml                           |  2 +-
 10 files changed, 57 insertions(+), 34 deletions(-)

diff --git a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
index 62a772fc6873..24cb007be0b8 100644
--- a/kani-compiler/src/codegen_aeneas_llbc/mir_to_ullbc/mod.rs
+++ b/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),
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 3a72fd45fa35..a1daeec5f88b 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/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()
         {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index c5f2f9fd2c08..f84e0a89f937 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/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)| {
                                     (
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 8171c5ffdda3..12a61c45b558 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/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(),
                 );
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index ff553c67a738..903baf8eaced 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/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))
     }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index 6fd9da651002..0e5e72af70b6 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/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()
     }
 }
 
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index ebef669e0f5d..afb0ff5e6c73 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/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()
         }
diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
index 8d9f14b3f969..369296db6ed4 100644
--- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
+++ b/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."
diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs
index 90bb0173ac55..d70e884400bb 100644
--- a/kani-compiler/src/kani_middle/stubbing/mod.rs
+++ b/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;
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index a2d54d0caf15..e216a29bcbd0 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-11-19"
+channel = "nightly-2024-11-26"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]

From 543be1bbf077b718942867375d606136001cc059 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Wed, 27 Nov 2024 16:05:14 -0800
Subject: [PATCH 3/3] Update llbc test expectations

---
 tests/expected/llbc/enum/expected       |  3 ++-
 tests/expected/llbc/projection/expected | 25 +++++++++++++------------
 tests/expected/llbc/struct/expected     |  3 ++-
 3 files changed, 17 insertions(+), 14 deletions(-)

diff --git a/tests/expected/llbc/enum/expected b/tests/expected/llbc/enum/expected
index 6c86139a52e8..10409fdab8e8 100644
--- a/tests/expected/llbc/enum/expected
+++ b/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
 }
+
diff --git a/tests/expected/llbc/projection/expected b/tests/expected/llbc/projection/expected
index 5f71248c8d44..50f7758ad86f 100644
--- a/tests/expected/llbc/projection/expected
+++ b/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
 }
+
diff --git a/tests/expected/llbc/struct/expected b/tests/expected/llbc/struct/expected
index e686cfaed0bc..a81e73b38895 100644
--- a/tests/expected/llbc/struct/expected
+++ b/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
 }
+