From d8936d639597d507ee00401e240459d65abadcb2 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Mon, 22 Jan 2024 14:33:03 -0800
Subject: [PATCH 01/10] Update calls to internal to pass TyCtxt

  - This is due to the safety fix to the internal function, which was
    done here: https://github.com/rust-lang/rust/pull/120128
---
 .../codegen/foreign_function.rs               |  7 +--
 .../codegen/intrinsic.rs                      | 50 ++++++++++---------
 .../codegen_cprover_gotoc/codegen/place.rs    |  9 ++--
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 17 ++++---
 .../src/codegen_cprover_gotoc/codegen/span.rs |  2 +-
 .../codegen/statement.rs                      |  8 +--
 .../codegen/ty_stable.rs                      | 42 ++++++++--------
 .../compiler_interface.rs                     |  2 +-
 .../context/current_fn.rs                     | 19 ++++---
 .../codegen_cprover_gotoc/overrides/hooks.rs  |  4 +-
 .../src/codegen_cprover_gotoc/utils/utils.rs  |  2 +-
 kani-compiler/src/kani_middle/attributes.rs   |  8 +--
 kani-compiler/src/kani_middle/coercion.rs     | 18 +++----
 kani-compiler/src/kani_middle/mod.rs          | 12 +++--
 kani-compiler/src/kani_middle/reachability.rs | 20 ++++----
 kani-compiler/src/kani_middle/stubbing/mod.rs |  8 +--
 16 files changed, 123 insertions(+), 105 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
index 2eb1610ab4d8..e9ad04a93130 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
@@ -48,7 +48,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// handled later.
     pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol {
         debug!(?instance, "codegen_foreign_function");
-        let instance_internal = rustc_internal::internal(instance);
+        let instance_internal = rustc_internal::internal(self.tcx, instance);
         let fn_name = self.symbol_name_stable(instance).intern();
         if self.symbol_table.contains(fn_name) {
             // Symbol has been added (either a built-in CBMC function or a Rust allocation function).
@@ -102,7 +102,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Generate type for the given foreign instance.
     fn codegen_ffi_type(&mut self, instance: Instance) -> Type {
         let fn_name = self.symbol_name_stable(instance);
-        let fn_abi = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance));
+        let fn_abi = kani_middle::fn_abi(self.tcx, rustc_internal::internal(self.tcx, instance));
         let loc = self.codegen_span_stable(instance.def.span());
         let params = fn_abi
             .args
@@ -140,7 +140,8 @@ impl<'tcx> GotocCtx<'tcx> {
         let entry = self.unsupported_constructs.entry("foreign function".into()).or_default();
         entry.push(loc);
 
-        let call_conv = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance)).conv;
+        let call_conv =
+            kani_middle::fn_abi(self.tcx, rustc_internal::internal(self.tcx, instance)).conv;
         let msg = format!("call to foreign \"{call_conv:?}\" function `{fn_name}`");
         let url = if call_conv == Conv::C {
             "https://github.com/model-checking/kani/issues/2423"
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 3412cba290d2..5419a55e27e3 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -3,7 +3,7 @@
 //! this module handles intrinsics
 use super::typ;
 use super::{bb_label, PropertyClass};
-use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type_stable, pretty_ty};
+use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
 use crate::codegen_cprover_gotoc::{utils, GotocCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{
@@ -646,7 +646,7 @@ impl<'tcx> GotocCtx<'tcx> {
             span,
             format!(
                 "Type check failed for intrinsic `{name}`: Expected {expected}, found {}",
-                pretty_ty(actual)
+                self.pretty_ty(actual)
             ),
         );
         self.tcx.dcx().abort_if_errors();
@@ -779,12 +779,16 @@ impl<'tcx> GotocCtx<'tcx> {
         if layout.abi.is_uninhabited() {
             return self.codegen_fatal_error(
                 PropertyClass::SafetyCheck,
-                &format!("attempted to instantiate uninhabited type `{}`", pretty_ty(*target_ty)),
+                &format!(
+                    "attempted to instantiate uninhabited type `{}`",
+                    self.pretty_ty(*target_ty)
+                ),
                 span,
             );
         }
 
-        let param_env_and_type = ParamEnv::reveal_all().and(rustc_internal::internal(target_ty));
+        let param_env_and_type =
+            ParamEnv::reveal_all().and(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
@@ -798,7 +802,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 PropertyClass::SafetyCheck,
                 &format!(
                     "attempted to zero-initialize type `{}`, which is invalid",
-                    pretty_ty(*target_ty)
+                    self.pretty_ty(*target_ty)
                 ),
                 span,
             );
@@ -817,7 +821,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 PropertyClass::SafetyCheck,
                 &format!(
                     "attempted to leave type `{}` uninitialized, which is invalid",
-                    pretty_ty(*target_ty)
+                    self.pretty_ty(*target_ty)
                 ),
                 span,
             );
@@ -1285,7 +1289,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 _ => {
                     let err_msg = format!(
                         "simd_shuffle index must be an array of `u32`, got `{}`",
-                        pretty_ty(farg_types[2])
+                        self.pretty_ty(farg_types[2])
                     );
                     utils::span_err(self.tcx, span, err_msg);
                     // Return a dummy value
@@ -1378,7 +1382,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
                 // Packed types ignore the alignment of their fields.
                 if let TyKind::RigidTy(RigidTy::Adt(def, _)) = ty.kind() {
-                    if rustc_internal::internal(def).repr().packed() {
+                    if rustc_internal::internal(self.tcx, def).repr().packed() {
                         unsized_align = sized_align.clone();
                     }
                 }
@@ -1426,9 +1430,9 @@ impl<'tcx> GotocCtx<'tcx> {
         if rust_ret_type != vector_base_type {
             let err_msg = format!(
                 "expected return type `{}` (element of input `{}`), found `{}`",
-                pretty_ty(vector_base_type),
-                pretty_ty(rust_arg_types[0]),
-                pretty_ty(rust_ret_type)
+                self.pretty_ty(vector_base_type),
+                self.pretty_ty(rust_arg_types[0]),
+                self.pretty_ty(rust_ret_type)
             );
             utils::span_err(self.tcx, span, err_msg);
         }
@@ -1466,9 +1470,9 @@ impl<'tcx> GotocCtx<'tcx> {
         if vector_base_type != rust_arg_types[2] {
             let err_msg = format!(
                 "expected inserted type `{}` (element of input `{}`), found `{}`",
-                pretty_ty(vector_base_type),
-                pretty_ty(rust_arg_types[0]),
-                pretty_ty(rust_arg_types[2]),
+                self.pretty_ty(vector_base_type),
+                self.pretty_ty(rust_arg_types[0]),
+                self.pretty_ty(rust_arg_types[2]),
             );
             utils::span_err(self.tcx, span, err_msg);
         }
@@ -1534,8 +1538,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 "expected return type with length {} (same as input type `{}`), \
                 found `{}` with length {}",
                 arg1.typ().len().unwrap(),
-                pretty_ty(rust_arg_types[0]),
-                pretty_ty(rust_ret_type),
+                self.pretty_ty(rust_arg_types[0]),
+                self.pretty_ty(rust_ret_type),
                 ret_typ.len().unwrap()
             );
             utils::span_err(self.tcx, span, err_msg);
@@ -1545,8 +1549,8 @@ impl<'tcx> GotocCtx<'tcx> {
             let (_, rust_base_type) = self.simd_size_and_type(rust_ret_type);
             let err_msg = format!(
                 "expected return type with integer elements, found `{}` with non-integer `{}`",
-                pretty_ty(rust_ret_type),
-                pretty_ty(rust_base_type),
+                self.pretty_ty(rust_ret_type),
+                self.pretty_ty(rust_base_type),
             );
             utils::span_err(self.tcx, span, err_msg);
         }
@@ -1740,7 +1744,7 @@ impl<'tcx> GotocCtx<'tcx> {
         if ret_type_len != n {
             let err_msg = format!(
                 "expected return type of length {n}, found `{}` with length {ret_type_len}",
-                pretty_ty(rust_ret_type),
+                self.pretty_ty(rust_ret_type),
             );
             utils::span_err(self.tcx, span, err_msg);
         }
@@ -1748,10 +1752,10 @@ impl<'tcx> GotocCtx<'tcx> {
             let err_msg = format!(
                 "expected return element type `{}` (element of input `{}`), \
                  found `{}` with element type `{}`",
-                pretty_ty(vec_subtype),
-                pretty_ty(rust_arg_types[0]),
-                pretty_ty(rust_ret_type),
-                pretty_ty(ret_type_subtype),
+                self.pretty_ty(vec_subtype),
+                self.pretty_ty(rust_arg_types[0]),
+                self.pretty_ty(rust_ret_type),
+                self.pretty_ty(ret_type_subtype),
             );
             utils::span_err(self.tcx, span, err_msg);
         }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index fd9ff33e164e..9296b713c862 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -260,7 +260,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         Ok(parent_expr.member(Self::tuple_fld_name(field_idx), &self.symbol_table))
                     }
                     TyKind::RigidTy(RigidTy::Adt(def, _))
-                        if rustc_internal::internal(def).repr().simd() =>
+                        if rustc_internal::internal(self.tcx, def).repr().simd() =>
                     {
                         Ok(self.codegen_simd_field(
                             parent_expr,
@@ -415,7 +415,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 };
 
                 let inner_mir_typ_internal =
-                    std_pointee_type(rustc_internal::internal(base_type)).unwrap();
+                    std_pointee_type(rustc_internal::internal(self.tcx, base_type)).unwrap();
                 let inner_mir_typ = rustc_internal::stable(inner_mir_typ_internal);
                 let (fat_ptr_mir_typ, fat_ptr_goto_expr) = if self
                     .use_thin_pointer(inner_mir_typ_internal)
@@ -436,6 +436,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     );
                     assert!(
                         self.use_fat_pointer(rustc_internal::internal(
+                            self.tcx,
                             pointee_type(fat_ptr_mir_typ.unwrap()).unwrap()
                         )),
                         "Unexpected type: {:?} -- {:?}",
@@ -582,7 +583,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         (variant.name().into(), TypeOrVariant::Variant(variant))
                     }
                     TyKind::RigidTy(RigidTy::Coroutine(..)) => {
-                        let idx_internal = rustc_internal::internal(idx);
+                        let idx_internal = rustc_internal::internal(self.tcx, idx);
                         (
                             self.coroutine_variant_name(idx_internal),
                             TypeOrVariant::CoroutineVariant(*idx),
@@ -593,7 +594,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         &ty.kind()
                     ),
                 };
-                let layout = self.layout_of(rustc_internal::internal(ty));
+                let layout = self.layout_of(rustc_internal::internal(self.tcx, ty));
                 let expr = match &layout.variants {
                     Variants::Single { .. } => before.goto_expr,
                     Variants::Multiple { tag_encoding, .. } => match tag_encoding {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index c4ea258fe79e..e7501df3aac4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -555,7 +555,7 @@ impl<'tcx> GotocCtx<'tcx> {
             let layout = self.layout_of_stable(res_ty);
             let fields = match &layout.variants {
                 Variants::Single { index } => {
-                    if *index != rustc_internal::internal(variant_index) {
+                    if *index != rustc_internal::internal(self.tcx, variant_index) {
                         // This may occur if all variants except for the one pointed by
                         // index can never be constructed. Generic code might still try
                         // to initialize the non-existing invariant.
@@ -565,7 +565,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     &layout.fields
                 }
                 Variants::Multiple { variants, .. } => {
-                    &variants[rustc_internal::internal(variant_index)].fields
+                    &variants[rustc_internal::internal(self.tcx, variant_index)].fields
                 }
             };
 
@@ -716,7 +716,10 @@ impl<'tcx> GotocCtx<'tcx> {
                             .offset_of_subfield(
                                 self,
                                 fields.iter().map(|(var_idx, field_idx)| {
-                                    (rustc_internal::internal(var_idx), (*field_idx).into())
+                                    (
+                                        rustc_internal::internal(self.tcx, var_idx),
+                                        (*field_idx).into(),
+                                    )
                                 }),
                             )
                             .bytes(),
@@ -1180,7 +1183,7 @@ impl<'tcx> GotocCtx<'tcx> {
             if self.vtable_ctx.emit_vtable_restrictions {
                 // Add to the possible method names for this trait type
                 self.vtable_ctx.add_possible_method(
-                    self.normalized_trait_name(rustc_internal::internal(ty)).into(),
+                    self.normalized_trait_name(rustc_internal::internal(self.tcx, ty)).into(),
                     idx,
                     fn_name.into(),
                 );
@@ -1205,7 +1208,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Generate a function pointer to drop_in_place for entry into the vtable
     fn codegen_vtable_drop_in_place(&mut self, ty: Ty, trait_ty: Ty) -> Expr {
-        let trait_ty = rustc_internal::internal(trait_ty);
+        let trait_ty = rustc_internal::internal(self.tcx, trait_ty);
         let drop_instance = Instance::resolve_drop_in_place(ty);
         let drop_sym_name: InternedString = drop_instance.mangled_name().into();
 
@@ -1296,7 +1299,7 @@ impl<'tcx> GotocCtx<'tcx> {
             _ => unreachable!("Cannot codegen_vtable for type {:?}", dst_mir_type.kind()),
         };
 
-        let src_name = self.ty_mangled_name(rustc_internal::internal(src_mir_type));
+        let src_name = self.ty_mangled_name(rustc_internal::internal(self.tcx, src_mir_type));
         // The name needs to be the same as inserted in typ.rs
         let vtable_name = self.vtable_name_stable(trait_type).intern();
         let vtable_impl_name = format!("{vtable_name}_impl_for_{src_name}");
@@ -1310,7 +1313,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // 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(trait_ref_binder))
+                    ctx.tcx.vtable_entries(rustc_internal::internal(ctx.tcx, trait_ref_binder))
                 } else {
                     TyCtxt::COMMON_VTABLE_ENTRIES
                 };
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
index c06d64d298c4..d06829822274 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
@@ -31,7 +31,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn codegen_caller_span_stable(&self, sp: SpanStable) -> Location {
-        self.codegen_caller_span(&rustc_internal::internal(sp))
+        self.codegen_caller_span(&rustc_internal::internal(self.tcx, sp))
     }
 
     /// Get the location of the caller. This will attempt to reach the macro caller.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index e7b7ee5a376a..ddda5519b598 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -219,8 +219,8 @@ impl<'tcx> GotocCtx<'tcx> {
         location: Location,
     ) -> Stmt {
         // this requires place points to an enum type.
-        let dest_ty_internal = rustc_internal::internal(dest_ty);
-        let variant_index_internal = rustc_internal::internal(variant_index);
+        let dest_ty_internal = rustc_internal::internal(self.tcx, dest_ty);
+        let variant_index_internal = rustc_internal::internal(self.tcx, variant_index);
         let layout = self.layout_of(dest_ty_internal);
         match &layout.variants {
             Variants::Single { .. } => Stmt::skip(location),
@@ -532,7 +532,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let instance = Instance::resolve(def, &subst).unwrap();
 
                 // TODO(celina): Move this check to be inside codegen_funcall_args.
-                if self.ty_needs_untupled_args(rustc_internal::internal(funct)) {
+                if self.ty_needs_untupled_args(rustc_internal::internal(self.tcx, funct)) {
                     self.codegen_untupled_args(instance, &mut fargs, args.last());
                 }
 
@@ -587,7 +587,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn extract_ptr(&self, arg_expr: Expr, arg_ty: Ty) -> Expr {
         // Generate an expression that indexes the pointer.
         let expr = self
-            .receiver_data_path(rustc_internal::internal(arg_ty))
+            .receiver_data_path(rustc_internal::internal(self.tcx, arg_ty))
             .fold(arg_expr, |curr_expr, (name, _)| curr_expr.member(name, &self.symbol_table));
 
         trace!(?arg_ty, gotoc_ty=?expr.typ(), gotoc_expr=?expr.value(), "extract_ptr");
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 2213676d5a63..548cd8cbf048 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
@@ -21,11 +21,11 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn codegen_ty_stable(&mut self, ty: Ty) -> Type {
-        self.codegen_ty(rustc_internal::internal(ty))
+        self.codegen_ty(rustc_internal::internal(self.tcx, ty))
     }
 
     pub fn codegen_ty_ref_stable(&mut self, ty: Ty) -> Type {
-        self.codegen_ty_ref(rustc_internal::internal(ty))
+        self.codegen_ty_ref(rustc_internal::internal(self.tcx, ty))
     }
 
     pub fn local_ty_stable(&self, local: Local) -> Ty {
@@ -37,11 +37,11 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn is_zst_stable(&self, ty: Ty) -> bool {
-        self.is_zst(rustc_internal::internal(ty))
+        self.is_zst(rustc_internal::internal(self.tcx, ty))
     }
 
     pub fn layout_of_stable(&self, ty: Ty) -> TyAndLayout<'tcx> {
-        self.layout_of(rustc_internal::internal(ty))
+        self.layout_of(rustc_internal::internal(self.tcx, ty))
     }
 
     pub fn codegen_fndef_type_stable(&mut self, instance: Instance) -> Type {
@@ -54,34 +54,34 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn fn_sig_of_instance_stable(&self, instance: Instance) -> FnSig {
-        let fn_sig = self.fn_sig_of_instance(rustc_internal::internal(instance));
+        let fn_sig = self.fn_sig_of_instance(rustc_internal::internal(self.tcx, instance));
         let fn_sig =
             self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), fn_sig);
         rustc_internal::stable(fn_sig)
     }
 
     pub fn use_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
-        self.use_fat_pointer(rustc_internal::internal(pointer_ty))
+        self.use_fat_pointer(rustc_internal::internal(self.tcx, pointer_ty))
     }
 
     pub fn use_thin_pointer_stable(&self, pointer_ty: Ty) -> bool {
-        self.use_thin_pointer(rustc_internal::internal(pointer_ty))
+        self.use_thin_pointer(rustc_internal::internal(self.tcx, pointer_ty))
     }
 
     pub fn is_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
-        self.is_fat_pointer(rustc_internal::internal(pointer_ty))
+        self.is_fat_pointer(rustc_internal::internal(self.tcx, pointer_ty))
     }
 
     pub fn is_vtable_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
-        self.is_vtable_fat_pointer(rustc_internal::internal(pointer_ty))
+        self.is_vtable_fat_pointer(rustc_internal::internal(self.tcx, pointer_ty))
     }
 
     pub fn use_vtable_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
-        self.use_vtable_fat_pointer(rustc_internal::internal(pointer_ty))
+        self.use_vtable_fat_pointer(rustc_internal::internal(self.tcx, pointer_ty))
     }
 
     pub fn vtable_name_stable(&self, ty: Ty) -> String {
-        self.vtable_name(rustc_internal::internal(ty))
+        self.vtable_name(rustc_internal::internal(self.tcx, ty))
     }
 
     pub fn rvalue_ty_stable(&self, rvalue: &Rvalue) -> Ty {
@@ -89,12 +89,12 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn simd_size_and_type(&self, ty: Ty) -> (u64, Ty) {
-        let (sz, ty) = rustc_internal::internal(ty).simd_size_and_type(self.tcx);
+        let (sz, ty) = rustc_internal::internal(self.tcx, ty).simd_size_and_type(self.tcx);
         (sz, rustc_internal::stable(ty))
     }
 
     pub fn codegen_enum_discr_typ_stable(&self, ty: Ty) -> Ty {
-        rustc_internal::stable(self.codegen_enum_discr_typ(rustc_internal::internal(ty)))
+        rustc_internal::stable(self.codegen_enum_discr_typ(rustc_internal::internal(self.tcx, ty)))
     }
 
     pub fn codegen_function_sig_stable(&mut self, sig: FnSig) -> Type {
@@ -115,6 +115,14 @@ impl<'tcx> GotocCtx<'tcx> {
             Type::code_with_unnamed_parameters(params, self.codegen_ty_stable(sig.output()))
         }
     }
+
+    /// Convert a type into a user readable type representation.
+    ///
+    /// 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()
+    }
 }
 /// If given type is a Ref / Raw ref, return the pointee type.
 pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
@@ -125,14 +133,6 @@ pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
     }
 }
 
-/// Convert a type into a user readable type representation.
-///
-/// This should be replaced by StableMIR `pretty_ty()` after
-/// <https://github.com/rust-lang/rust/pull/118364> is merged.
-pub fn pretty_ty(ty: Ty) -> String {
-    rustc_internal::internal(ty).to_string()
-}
-
 pub fn pointee_type_stable(ty: Ty) -> Option<Ty> {
     match ty.kind() {
         TyKind::RigidTy(RigidTy::Ref(_, pointee_ty, _))
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 8b21093f4667..50f17eff9fe9 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -285,7 +285,7 @@ impl CodegenBackend for GotocCodegenBackend {
                     let main_instance =
                         stable_mir::entry_fn().map(|main_fn| Instance::try_from(main_fn).unwrap());
                     let local_reachable = filter_crate_items(tcx, |_, instance| {
-                        let def_id = rustc_internal::internal(instance.def.def_id());
+                        let def_id = rustc_internal::internal(tcx, instance.def.def_id());
                         Some(instance) == main_instance || tcx.is_reachable_non_generic(def_id)
                     })
                     .into_iter()
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
index e73a4756a581..f05b7bcc161b 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
@@ -4,8 +4,8 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Stmt;
 use cbmc::InternedString;
-use rustc_middle::mir::Body as InternalBody;
-use rustc_middle::ty::Instance as InternalInstance;
+use rustc_middle::mir::Body as BodyInternal;
+use rustc_middle::ty::Instance as InstanceInternal;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Body, Local, LocalDecl};
@@ -25,7 +25,9 @@ pub struct CurrentFnCtx<'tcx> {
     /// The crate this function is from
     krate: String,
     /// The MIR for the current instance. This is using the internal representation.
-    mir: &'tcx InternalBody<'tcx>,
+    mir: &'tcx BodyInternal<'tcx>,
+    /// The current instance. This is using the internal representation.
+    instance_internal: InstanceInternal<'tcx>,
     /// A list of local declarations used to retrieve MIR component types.
     locals: Vec<LocalDecl>,
     /// A list of pretty names for locals that corrspond to user variables.
@@ -41,7 +43,7 @@ pub struct CurrentFnCtx<'tcx> {
 /// Constructor
 impl<'tcx> CurrentFnCtx<'tcx> {
     pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>, body: &Body) -> Self {
-        let internal_instance = rustc_internal::internal(instance);
+        let instance_internal = rustc_internal::internal(gcx.tcx, instance);
         let readable_name = instance.name();
         let name =
             if &readable_name == "main" { readable_name.clone() } else { instance.mangled_name() };
@@ -56,7 +58,8 @@ impl<'tcx> CurrentFnCtx<'tcx> {
             block: vec![],
             instance,
             fn_sig,
-            mir: gcx.tcx.instance_mir(internal_instance.def),
+            mir: gcx.tcx.instance_mir(instance_internal.def),
+            instance_internal,
             krate: instance.def.krate().name,
             locals,
             local_names,
@@ -88,8 +91,8 @@ impl<'tcx> CurrentFnCtx<'tcx> {
 /// Getters
 impl<'tcx> CurrentFnCtx<'tcx> {
     /// The function we are currently compiling
-    pub fn instance(&self) -> InternalInstance<'tcx> {
-        rustc_internal::internal(self.instance)
+    pub fn instance(&self) -> InstanceInternal<'tcx> {
+        self.instance_internal
     }
 
     pub fn instance_stable(&self) -> Instance {
@@ -97,7 +100,7 @@ impl<'tcx> CurrentFnCtx<'tcx> {
     }
 
     /// The internal MIR for the function we are currently compiling using internal APIs.
-    pub fn body_internal(&self) -> &'tcx InternalBody<'tcx> {
+    pub fn body_internal(&self) -> &'tcx BodyInternal<'tcx> {
         self.mir
     }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index 97606688d1ed..0141c2886539 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -38,7 +38,7 @@ pub trait GotocHook {
 fn matches_function(tcx: TyCtxt, instance: Instance, attr_name: &str) -> bool {
     let attr_sym = rustc_span::symbol::Symbol::intern(attr_name);
     if let Some(attr_id) = tcx.all_diagnostic_items(()).name_to_id.get(&attr_sym) {
-        if rustc_internal::internal(instance.def.def_id()) == *attr_id {
+        if rustc_internal::internal(tcx, instance.def.def_id()) == *attr_id {
             debug!("matched: {:?} {:?}", attr_id, attr_sym);
             return true;
         }
@@ -196,7 +196,7 @@ struct Panic;
 
 impl GotocHook for Panic {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        let def_id = rustc_internal::internal(instance.def.def_id());
+        let def_id = rustc_internal::internal(tcx, instance.def.def_id());
         Some(def_id) == tcx.lang_items().panic_fn()
             || tcx.has_attr(def_id, rustc_span::sym::rustc_const_panic_str)
             || Some(def_id) == tcx.lang_items().panic_fmt()
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
index d81839ea097c..e369f64beda9 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs
@@ -194,5 +194,5 @@ impl<'tcx> GotocCtx<'tcx> {
 }
 
 pub fn span_err(tcx: TyCtxt, span: Span, msg: String) {
-    tcx.dcx().span_err(rustc_internal::internal(span), msg);
+    tcx.dcx().span_err(rustc_internal::internal(tcx, span), msg);
 }
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 3bfef9a409f4..65d1a6d34a5d 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -115,7 +115,7 @@ impl<'tcx> KaniAttributes<'tcx> {
     /// Perform preliminary parsing and checking for the attributes on this
     /// function
     pub fn for_instance(tcx: TyCtxt<'tcx>, instance: InstanceStable) -> Self {
-        KaniAttributes::for_item(tcx, rustc_internal::internal(instance.def.def_id()))
+        KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, instance.def.def_id()))
     }
 
     pub fn for_item(tcx: TyCtxt<'tcx>, def_id: DefId) -> Self {
@@ -520,7 +520,7 @@ pub fn is_function_contract_generated(tcx: TyCtxt, def_id: DefId) -> bool {
 /// Same as [`KaniAttributes::is_harness`] but more efficient because less
 /// attribute parsing is performed.
 pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool {
-    let def_id = rustc_internal::internal(instance.def.def_id());
+    let def_id = rustc_internal::internal(tcx, instance.def.def_id());
     has_kani_attribute(tcx, def_id, |a| {
         matches!(a, KaniAttributeKind::Proof | KaniAttributeKind::ProofForContract)
     })
@@ -528,14 +528,14 @@ pub fn is_proof_harness(tcx: TyCtxt, instance: InstanceStable) -> bool {
 
 /// Does this `def_id` have `#[rustc_test_marker]`?
 pub fn is_test_harness_description(tcx: TyCtxt, item: impl CrateDef) -> bool {
-    let def_id = rustc_internal::internal(item.def_id());
+    let def_id = rustc_internal::internal(tcx, item.def_id());
     let attrs = tcx.get_attrs_unchecked(def_id);
     attr::contains_name(attrs, rustc_span::symbol::sym::rustc_test_marker)
 }
 
 /// Extract the test harness name from the `#[rustc_test_maker]`
 pub fn test_harness_name(tcx: TyCtxt, def: &impl CrateDef) -> String {
-    let def_id = rustc_internal::internal(def.def_id());
+    let def_id = rustc_internal::internal(tcx, def.def_id());
     let attrs = tcx.get_attrs_unchecked(def_id);
     let marker = attr::find_by_name(attrs, rustc_span::symbol::sym::rustc_test_marker).unwrap();
     parse_str_value(&marker).unwrap()
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 85d59215d661..42c28f92e4fa 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -66,8 +66,8 @@ pub fn extract_unsize_casting_stable(
 ) -> CoercionBaseStable {
     let CoercionBase { src_ty, dst_ty } = extract_unsize_casting(
         tcx,
-        rustc_internal::internal(src_ty),
-        rustc_internal::internal(dst_ty),
+        rustc_internal::internal(tcx, src_ty),
+        rustc_internal::internal(tcx, dst_ty),
     );
     CoercionBaseStable {
         src_ty: rustc_internal::stable(src_ty),
@@ -90,11 +90,11 @@ pub fn extract_unsize_casting<'tcx>(
     .last()
     .unwrap();
     // Extract the pointee type that is being coerced.
-    let src_pointee_ty = extract_pointee(coerce_info.src_ty).expect(&format!(
+    let src_pointee_ty = extract_pointee(tcx, coerce_info.src_ty).expect(&format!(
         "Expected source to be a pointer. Found {:?} instead",
         coerce_info.src_ty
     ));
-    let dst_pointee_ty = extract_pointee(coerce_info.dst_ty).expect(&format!(
+    let dst_pointee_ty = extract_pointee(tcx, coerce_info.dst_ty).expect(&format!(
         "Expected destination to be a pointer. Found {:?} instead",
         coerce_info.dst_ty
     ));
@@ -216,8 +216,8 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> {
 
                 let CustomCoerceUnsized::Struct(coerce_index) = custom_coerce_unsize_info(
                     self.tcx,
-                    rustc_internal::internal(src_ty),
-                    rustc_internal::internal(dst_ty),
+                    rustc_internal::internal(self.tcx, src_ty),
+                    rustc_internal::internal(self.tcx, dst_ty),
                 );
                 let coerce_index = coerce_index.as_usize();
                 assert!(coerce_index < src_fields.len());
@@ -229,7 +229,7 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> {
             _ => {
                 // Base case is always a pointer (Box, raw_pointer or reference).
                 assert!(
-                    extract_pointee(src_ty).is_some(),
+                    extract_pointee(self.tcx, src_ty).is_some(),
                     "Expected a pointer, but found {src_ty:?}"
                 );
                 None
@@ -262,6 +262,6 @@ fn custom_coerce_unsize_info<'tcx>(
 }
 
 /// Extract pointee type from builtin pointer types.
-fn extract_pointee<'tcx>(typ: TyStable) -> Option<Ty<'tcx>> {
-    rustc_internal::internal(typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty)
+fn extract_pointee<'tcx>(tcx: TyCtxt<'tcx>, typ: TyStable) -> Option<Ty<'tcx>> {
+    rustc_internal::internal(tcx, typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty)
 }
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 4ccac4f485fe..19cab34b7a52 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -84,7 +84,7 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
         };
         if !def_ids.contains(&def_id) {
             // Check if any unstable attribute was reached.
-            KaniAttributes::for_item(tcx, rustc_internal::internal(def_id))
+            KaniAttributes::for_item(tcx, rustc_internal::internal(tcx, def_id))
                 .check_unstable_features(&queries.args().unstable_features);
             def_ids.insert(def_id);
         }
@@ -92,7 +92,10 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem])
         // We don't short circuit here since this is a type check and can shake
         // out differently depending on generic parameters.
         if let MonoItem::Fn(instance) = item {
-            if attributes::is_function_contract_generated(tcx, rustc_internal::internal(def_id)) {
+            if attributes::is_function_contract_generated(
+                tcx,
+                rustc_internal::internal(tcx, def_id),
+            ) {
                 check_is_contract_safe(tcx, *instance);
             }
         }
@@ -167,7 +170,7 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) {
     for var in &bound_fn_sig.bound_vars {
         if let BoundVariableKind::Ty(t) = var {
             tcx.dcx().span_err(
-                rustc_internal::internal(instance.def.span()),
+                rustc_internal::internal(tcx, instance.def.span()),
                 format!("Found a bound type variable {t:?} after monomorphization"),
             );
         }
@@ -211,7 +214,8 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) {
         // For each def_id, dump their MIR
         for (item, def_id) in items.iter().filter_map(visible_item) {
             writeln!(writer, "// Item: {item:?}").unwrap();
-            write_mir_pretty(tcx, Some(rustc_internal::internal(def_id)), &mut writer).unwrap();
+            write_mir_pretty(tcx, Some(rustc_internal::internal(tcx, def_id)), &mut writer)
+                .unwrap();
         }
     }
 }
diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
index 424077a622f9..63ed41bfd4c1 100644
--- a/kani-compiler/src/kani_middle/reachability.rs
+++ b/kani-compiler/src/kani_middle/reachability.rs
@@ -75,7 +75,7 @@ where
         .filter_map(|item| {
             // Only collect monomorphic items.
             // TODO: Remove the def_kind check once https://github.com/rust-lang/rust/pull/119135 has been released.
-            let def_id = rustc_internal::internal(item.def_id());
+            let def_id = rustc_internal::internal(tcx, item.def_id());
             (matches!(tcx.def_kind(def_id), rustc_hir::def::DefKind::Ctor(..))
                 || matches!(item.kind(), ItemKind::Fn))
             .then(|| {
@@ -237,7 +237,8 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
             let poly_trait_ref = principal.with_self_ty(concrete_ty);
 
             // Walk all methods of the trait, including those of its supertraits
-            let entries = self.tcx.vtable_entries(rustc_internal::internal(&poly_trait_ref));
+            let entries =
+                self.tcx.vtable_entries(rustc_internal::internal(self.tcx, &poly_trait_ref));
             let methods = entries.iter().filter_map(|entry| match entry {
                 VtblEntry::MetadataAlign
                 | VtblEntry::MetadataDropInPlace
@@ -395,9 +396,10 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
                             let caller = CrateItem::try_from(*self.instance).unwrap().name();
                             let callee = fn_def.name();
                             // Check if the current function has been stubbed.
-                            if let Some(stub) =
-                                get_stub(self.tcx, rustc_internal::internal(self.instance).def_id())
-                            {
+                            if let Some(stub) = get_stub(
+                                self.tcx,
+                                rustc_internal::internal(self.tcx, self.instance).def_id(),
+                            ) {
                                 // During the MIR stubbing transformation, we do not
                                 // force type variables in the stub's signature to
                                 // implement the same traits as those in the
@@ -413,7 +415,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
                                 let sep = callee.rfind("::").unwrap();
                                 let trait_ = &callee[..sep];
                                 self.tcx.dcx().span_err(
-                                    rustc_internal::internal(terminator.span),
+                                    rustc_internal::internal(self.tcx, terminator.span),
                                     format!(
                                         "`{}` doesn't implement \
                                         `{}`. The function `{}` \
@@ -465,8 +467,8 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
 fn extract_unsize_coercion(tcx: TyCtxt, orig_ty: Ty, dst_trait: Ty) -> (Ty, Ty) {
     let CoercionBase { src_ty, dst_ty } = coercion::extract_unsize_casting(
         tcx,
-        rustc_internal::internal(orig_ty),
-        rustc_internal::internal(dst_trait),
+        rustc_internal::internal(tcx, orig_ty),
+        rustc_internal::internal(tcx, dst_trait),
     );
     (rustc_internal::stable(src_ty), rustc_internal::stable(dst_ty))
 }
@@ -476,7 +478,7 @@ fn extract_unsize_coercion(tcx: TyCtxt, orig_ty: Ty, dst_trait: Ty) -> (Ty, Ty)
 fn to_fingerprint(tcx: TyCtxt, item: &MonoItem) -> Fingerprint {
     tcx.with_stable_hashing_context(|mut hcx| {
         let mut hasher = StableHasher::new();
-        rustc_internal::internal(item).hash_stable(&mut hcx, &mut hasher);
+        rustc_internal::internal(tcx, item).hash_stable(&mut hcx, &mut hasher);
         hasher.finish()
     })
 }
diff --git a/kani-compiler/src/kani_middle/stubbing/mod.rs b/kani-compiler/src/kani_middle/stubbing/mod.rs
index 9dda0144eda4..0db518ceef9f 100644
--- a/kani-compiler/src/kani_middle/stubbing/mod.rs
+++ b/kani-compiler/src/kani_middle/stubbing/mod.rs
@@ -27,7 +27,7 @@ pub fn harness_stub_map(
     harness: Instance,
     metadata: &HarnessMetadata,
 ) -> BTreeMap<DefPathHash, DefPathHash> {
-    let def_id = rustc_internal::internal(harness.def.def_id());
+    let def_id = rustc_internal::internal(tcx, harness.def.def_id());
     let attrs = &metadata.attributes;
     let mut stub_pairs = BTreeMap::default();
     for stubs in &attrs.stubs {
@@ -44,7 +44,7 @@ pub fn harness_stub_map(
 /// In stable MIR, trying to retrieve an `Instance::body()` will ICE if we cannot evaluate a
 /// constant as expected. For now, use internal APIs to anticipate this issue.
 pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool {
-    let internal_instance = rustc_internal::internal(instance);
+    let internal_instance = rustc_internal::internal(tcx, instance);
     if get_stub(tcx, internal_instance.def_id()).is_some() {
         debug!(?instance, "validate_instance");
         let item = CrateItem::try_from(instance).unwrap();
@@ -87,7 +87,7 @@ impl<'tcx> StubConstChecker<'tcx> {
 impl<'tcx> MirVisitor for StubConstChecker<'tcx> {
     /// Collect constants that are represented as static variables.
     fn visit_constant(&mut self, constant: &Constant, location: Location) {
-        let const_ = self.monomorphize(rustc_internal::internal(&constant.literal));
+        let const_ = self.monomorphize(rustc_internal::internal(self.tcx, &constant.literal));
         debug!(?constant, ?location, ?const_, "visit_constant");
         match const_ {
             Const::Val(..) | Const::Ty(..) => {}
@@ -109,7 +109,7 @@ impl<'tcx> MirVisitor for StubConstChecker<'tcx> {
                         tcx.def_path_str(trait_),
                         self.source.name()
                     );
-                    tcx.dcx().span_err(rustc_internal::internal(location.span()), msg);
+                    tcx.dcx().span_err(rustc_internal::internal(self.tcx, location.span()), msg);
                     self.is_valid = false;
                 }
             }

From 59d592124148a4c6ae42aa9842507bcf63526540 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 23 Jan 2024 12:46:12 -0800
Subject: [PATCH 02/10] Upgrade toolchain to nightly-2024-01-23

---
 kani-compiler/src/kani_middle/attributes.rs | 2 +-
 kani-compiler/src/kani_middle/coercion.rs   | 2 +-
 kani-compiler/src/kani_middle/resolve.rs    | 9 ++++-----
 rust-toolchain.toml                         | 2 +-
 4 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 65d1a6d34a5d..0dc7cb69d505 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -793,7 +793,7 @@ fn parse_integer(attr: &Attribute) -> Option<u128> {
     if attr_args.len() == 1 {
         let x = attr_args[0].lit()?;
         match x.kind {
-            LitKind::Int(y, ..) => Some(y),
+            LitKind::Int(y, ..) => Some(y.get()),
             _ => None,
         }
     }
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 42c28f92e4fa..94879b5b65e6 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -262,6 +262,6 @@ fn custom_coerce_unsize_info<'tcx>(
 }
 
 /// Extract pointee type from builtin pointer types.
-fn extract_pointee<'tcx>(tcx: TyCtxt<'tcx>, typ: TyStable) -> Option<Ty<'tcx>> {
+fn extract_pointee(tcx: TyCtxt<'_>, typ: TyStable) -> Option<Ty<'_>> {
     rustc_internal::internal(tcx, typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty)
 }
diff --git a/kani-compiler/src/kani_middle/resolve.rs b/kani-compiler/src/kani_middle/resolve.rs
index 1d3b1a2c2f06..303e027395fd 100644
--- a/kani-compiler/src/kani_middle/resolve.rs
+++ b/kani-compiler/src/kani_middle/resolve.rs
@@ -399,8 +399,11 @@ fn resolve_in_type<'tcx>(
     name: &str,
 ) -> Result<DefId, ResolveError<'tcx>> {
     debug!(?name, ?type_id, "resolve_in_type");
+    let missing_item_err =
+        || ResolveError::MissingItem { tcx, base: type_id, unresolved: name.to_string() };
     // Try the inherent `impl` blocks (i.e., non-trait `impl`s).
     tcx.inherent_impls(type_id)
+        .map_err(|_| missing_item_err())?
         .iter()
         .flat_map(|impl_id| tcx.associated_item_def_ids(impl_id))
         .cloned()
@@ -409,9 +412,5 @@ fn resolve_in_type<'tcx>(
             let last = item_path.split("::").last().unwrap();
             last == name
         })
-        .ok_or_else(|| ResolveError::MissingItem {
-            tcx,
-            base: type_id,
-            unresolved: name.to_string(),
-        })
+        .ok_or_else(missing_item_err)
 }
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 620fdc1efa29..510d3e13b50b 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-01-08"
+channel = "nightly-2024-01-23"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

From 75c58be51d2b1c18babbf744daf7af36d2d1391a Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 23 Jan 2024 16:25:53 -0800
Subject: [PATCH 03/10] Add missing changes after a bad rebase

---
 .../src/codegen_cprover_gotoc/codegen/typ.rs       |  6 +++++-
 .../src/codegen_cprover_gotoc/utils/debug.rs       |  2 +-
 kani-compiler/src/kani_middle/attributes.rs        | 14 +++++++-------
 kani-compiler/src/kani_middle/intrinsics.rs        |  5 +++--
 4 files changed, 16 insertions(+), 11 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index bdddd8ce9f26..7694feb0dbbf 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -302,7 +302,11 @@ impl<'tcx> GotocCtx<'tcx> {
             kind: ty::BoundRegionKind::BrEnv,
         };
         let env_region = ty::Region::new_bound(self.tcx, ty::INNERMOST, br);
-        let env_ty = self.tcx.closure_env_ty(def_id, args, env_region).unwrap();
+        let env_ty = self.tcx.closure_env_ty(
+            Ty::new_closure(self.tcx, def_id, args),
+            args.as_closure().kind(),
+            env_region,
+        );
 
         let sig = sig.skip_binder();
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
index c30d1539bda2..aeaf8e0e2d10 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
@@ -16,7 +16,7 @@ use tracing::debug;
 // Use a thread-local global variable to track the current codegen item for debugging.
 // If Kani panics during codegen, we can grab this item to include the problematic
 // codegen item in the panic trace.
-thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<(Option<String>, Option<Location>)> = RefCell::new((None, None)));
+thread_local!(static CURRENT_CODEGEN_ITEM: RefCell<(Option<String>, Option<Location>)> = const { RefCell::new((None, None)) });
 
 pub fn init() {
     // Install panic hook
diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 0dc7cb69d505..d41007c1c3f1 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/kani-compiler/src/kani_middle/attributes.rs
@@ -348,12 +348,12 @@ impl<'tcx> KaniAttributes<'tcx> {
                 "Use of unstable feature `{}`: {}",
                 unstable_attr.feature, unstable_attr.reason
             ))
-            .span_note(
+            .with_span_note(
                 self.tcx.def_span(self.item),
                 format!("the function `{fn_name}` is unstable:"),
             )
-            .note(format!("see issue {} for more information", unstable_attr.issue))
-            .help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature))
+            .with_note(format!("see issue {} for more information", unstable_attr.issue))
+            .with_help(format!("use `-Z {}` to enable using this function.", unstable_attr.feature))
             .emit()
     }
 
@@ -422,7 +422,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                     self.item_name(),
                 ),
             )
-            .span_note(self.tcx.def_span(id), "Try adding a contract to this function.")
+            .with_span_note(self.tcx.def_span(id), "Try adding a contract to this function.")
             .emit();
             return;
         };
@@ -448,7 +448,7 @@ impl<'tcx> KaniAttributes<'tcx> {
                             self.item_name(),
                         ),
                     )
-                    .span_note(
+                    .with_span_note(
                         self.tcx.def_span(def_id),
                         format!(
                             "Try adding a contract to this function or use the unsound `{}` attribute instead.", 
@@ -624,7 +624,7 @@ impl<'a> UnstableAttrParseError<'a> {
                 self.attr.span,
                 format!("failed to parse `#[kani::unstable]`: {}", self.reason),
             )
-            .note(format!(
+            .with_note(format!(
                 "expected format: #[kani::unstable({}, {}, {})]",
                 r#"feature="<IDENTIFIER>""#, r#"issue="<ISSUE>""#, r#"reason="<DESCRIPTION>""#
             ))
@@ -665,7 +665,7 @@ fn expect_no_args(tcx: TyCtxt, kind: KaniAttributeKind, attr: &Attribute) {
     if !attr.is_word() {
         tcx.dcx()
             .struct_span_err(attr.span, format!("unexpected argument for `{}`", kind.as_ref()))
-            .help("remove the extra argument")
+            .with_help("remove the extra argument")
             .emit();
     }
 }
diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs
index c4785ac98b81..8a7fc16d8e9f 100644
--- a/kani-compiler/src/kani_middle/intrinsics.rs
+++ b/kani-compiler/src/kani_middle/intrinsics.rs
@@ -7,6 +7,7 @@ use rustc_middle::mir::{Body, Const as mirConst, ConstValue, Operand, Terminator
 use rustc_middle::mir::{Local, LocalDecl};
 use rustc_middle::ty::{self, Ty, TyCtxt};
 use rustc_middle::ty::{Const, GenericArgsRef};
+use rustc_span::source_map::Spanned;
 use rustc_span::symbol::{sym, Symbol};
 use tracing::{debug, trace};
 
@@ -48,12 +49,12 @@ impl<'tcx> ModelIntrinsics<'tcx> {
     fn replace_simd_bitmask(
         &self,
         func: &mut Operand<'tcx>,
-        args: &[Operand<'tcx>],
+        args: &[Spanned<Operand<'tcx>>],
         gen_args: GenericArgsRef<'tcx>,
     ) {
         assert_eq!(args.len(), 1);
         let tcx = self.tcx;
-        let arg_ty = args[0].ty(&self.local_decls, tcx);
+        let arg_ty = args[0].node.ty(&self.local_decls, tcx);
         if arg_ty.is_simd() {
             // Get the stub definition.
             let stub_id = tcx.get_diagnostic_item(Symbol::intern("KaniModelSimdBitmask")).unwrap();

From 20bbb5101005e96633c2b00c58199418739a37e6 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Wed, 24 Jan 2024 10:55:22 -0600
Subject: [PATCH 04/10] Automatic cargo update to 2024-01-22 (#2980)

Dependency upgrade resulting from `cargo update`.

Co-authored-by: tautschnig <tautschnig@users.noreply.github.com>
---
 Cargo.lock | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/Cargo.lock b/Cargo.lock
index ff64b733a145..29c7228537d0 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -756,9 +756,9 @@ dependencies = [
 
 [[package]]
 name = "proc-macro2"
-version = "1.0.76"
+version = "1.0.78"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "95fc56cda0b5c3325f5fbbd7ff9fda9e02bb00bb3dac51252d2f1bfa1cb8cc8c"
+checksum = "e2422ad645d89c99f8f3e6b88a9fdeca7fabeac836b1002371c4367c8f984aae"
 dependencies = [
  "unicode-ident",
 ]
@@ -844,13 +844,13 @@ dependencies = [
 
 [[package]]
 name = "regex"
-version = "1.10.2"
+version = "1.10.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "380b951a9c5e80ddfd6136919eef32310721aa4aacd4889a8d39124b026ab343"
+checksum = "b62dbe01f0b06f9d8dc7d49e05a0785f153b00b2c227856282f671e0318c9b15"
 dependencies = [
  "aho-corasick",
  "memchr",
- "regex-automata 0.4.3",
+ "regex-automata 0.4.4",
  "regex-syntax 0.8.2",
 ]
 
@@ -865,9 +865,9 @@ dependencies = [
 
 [[package]]
 name = "regex-automata"
-version = "0.4.3"
+version = "0.4.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5f804c7828047e88b2d32e2d7fe5a105da8ee3264f01902f796c8e067dc2483f"
+checksum = "3b7fa1134405e2ec9353fd416b17f8dacd46c473d7d3fd1cf202706a14eb792a"
 dependencies = [
  "aho-corasick",
  "memchr",
@@ -1027,9 +1027,9 @@ checksum = "24188a676b6ae68c3b2cb3a01be17fbf7240ce009799bb56d5b1409051e78fde"
 
 [[package]]
 name = "smallvec"
-version = "1.13.0"
+version = "1.13.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "3b187f0231d56fe41bfb12034819dd2bf336422a5866de41bc3fec4b2e3883e8"
+checksum = "e6ecd384b10a64542d77071bd64bd7b231f4ed5940fba55e98c3de13824cf3d7"
 
 [[package]]
 name = "std"

From 68fba17cc61b2ef3b026f503ef7901da54cc421d Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Wed, 24 Jan 2024 13:16:32 -0600
Subject: [PATCH 05/10] Bump Kani version to 0.45.0 (#2984)

These are the auto-generated release notes for comparison purposes:

## What's Changed
* Rethink `should_panic` and `fail_uncoverable` options as global
conditions by @adpaco-aws in
https://github.com/model-checking/kani/pull/2967
* Upgrade toolchain to nightly-2024-01-17 by @celinval in
https://github.com/model-checking/kani/pull/2976
* Benchcomp visualize: fix missing import by @tautschnig in
https://github.com/model-checking/kani/pull/2977
* Cargo update 2024-01-18 by @remi-delmas-3000 in
https://github.com/model-checking/kani/pull/2978

**Full Changelog**:
https://github.com/model-checking/kani/compare/kani-0.44.0...kani-0.45.0

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---
 CHANGELOG.md                   |  7 +++++++
 Cargo.lock                     | 18 +++++++++---------
 Cargo.toml                     |  2 +-
 cprover_bindings/Cargo.toml    |  2 +-
 kani-compiler/Cargo.toml       |  2 +-
 kani-driver/Cargo.toml         |  2 +-
 kani_metadata/Cargo.toml       |  2 +-
 library/kani/Cargo.toml        |  2 +-
 library/kani_macros/Cargo.toml |  2 +-
 library/std/Cargo.toml         |  2 +-
 tools/build-kani/Cargo.toml    |  2 +-
 11 files changed, 25 insertions(+), 18 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 722e05aff154..33baeb1ef5af 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,13 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)
 
 This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
 
+## [0.45.0]
+
+## What's Changed
+* Upgrade toolchain to nightly-2024-01-17 by @celinval in https://github.com/model-checking/kani/pull/2976
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.44.0...kani-0.45.0
+
 ## [0.44.0]
 
 ### What's Changed
diff --git a/Cargo.lock b/Cargo.lock
index 29c7228537d0..ebc785f221ae 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -119,7 +119,7 @@ dependencies = [
 
 [[package]]
 name = "build-kani"
-version = "0.44.0"
+version = "0.45.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -255,7 +255,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.44.0"
+version = "0.45.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -432,14 +432,14 @@ checksum = "b1a46d1a171d865aa5f83f92695765caa047a9b4cbae2cbf37dbd613a793fd4c"
 
 [[package]]
 name = "kani"
-version = "0.44.0"
+version = "0.45.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani-compiler"
-version = "0.44.0"
+version = "0.45.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -460,7 +460,7 @@ dependencies = [
 
 [[package]]
 name = "kani-driver"
-version = "0.44.0"
+version = "0.45.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -488,7 +488,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.44.0"
+version = "0.45.0"
 dependencies = [
  "anyhow",
  "home",
@@ -497,7 +497,7 @@ dependencies = [
 
 [[package]]
 name = "kani_macros"
-version = "0.44.0"
+version = "0.45.0"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
@@ -507,7 +507,7 @@ dependencies = [
 
 [[package]]
 name = "kani_metadata"
-version = "0.44.0"
+version = "0.45.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -1033,7 +1033,7 @@ checksum = "e6ecd384b10a64542d77071bd64bd7b231f4ed5940fba55e98c3de13824cf3d7"
 
 [[package]]
 name = "std"
-version = "0.44.0"
+version = "0.45.0"
 dependencies = [
  "kani",
 ]
diff --git a/Cargo.toml b/Cargo.toml
index 4830f3095573..df9559e378b6 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-verifier"
-version = "0.44.0"
+version = "0.45.0"
 edition = "2021"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"
diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml
index 149b6f521eeb..5205872f6788 100644
--- a/cprover_bindings/Cargo.toml
+++ b/cprover_bindings/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "cprover_bindings"
-version = "0.44.0"
+version = "0.45.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
index 9548dfd4b580..b93ce2d135b8 100644
--- a/kani-compiler/Cargo.toml
+++ b/kani-compiler/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-compiler"
-version = "0.44.0"
+version = "0.45.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
index eaf4e6df98ee..2a19030840d2 100644
--- a/kani-driver/Cargo.toml
+++ b/kani-driver/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-driver"
-version = "0.44.0"
+version = "0.45.0"
 edition = "2021"
 description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"
diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml
index 993ae66fd43a..2d40d61c898b 100644
--- a/kani_metadata/Cargo.toml
+++ b/kani_metadata/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_metadata"
-version = "0.44.0"
+version = "0.45.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml
index 18e8e295b09a..d50717ca97c6 100644
--- a/library/kani/Cargo.toml
+++ b/library/kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani"
-version = "0.44.0"
+version = "0.45.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml
index c940f20a91a0..473d0fc7e5b6 100644
--- a/library/kani_macros/Cargo.toml
+++ b/library/kani_macros/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_macros"
-version = "0.44.0"
+version = "0.45.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml
index 6112e0d3025c..b37ea4de7d4c 100644
--- a/library/std/Cargo.toml
+++ b/library/std/Cargo.toml
@@ -5,7 +5,7 @@
 # Note: this package is intentionally named std to make sure the names of
 # standard library symbols are preserved
 name = "std"
-version = "0.44.0"
+version = "0.45.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml
index 5e741c5ec975..cfaa4a6c48ad 100644
--- a/tools/build-kani/Cargo.toml
+++ b/tools/build-kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "build-kani"
-version = "0.44.0"
+version = "0.45.0"
 edition = "2021"
 description = "Builds Kani, Sysroot and release bundle."
 license = "MIT OR Apache-2.0"

From 58e919b104ab96863bd6fb5d71331957ef532bc1 Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Fri, 26 Jan 2024 16:37:37 -0600
Subject: [PATCH 06/10] Make __kani__workaround_core_assert pub in lib.rs

---
 library/std/src/lib.rs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
index 92ff9216da95..1296d2982efc 100644
--- a/library/std/src/lib.rs
+++ b/library/std/src/lib.rs
@@ -17,7 +17,7 @@ pub use std::*;
 // https://github.com/model-checking/kani/issues/1949
 #[cfg(not(feature = "concrete_playback"))]
 #[allow(unused_imports)]
-use core::assert as __kani__workaround_core_assert;
+pub use core::assert as __kani__workaround_core_assert;
 
 #[cfg(not(feature = "concrete_playback"))]
 // Override process calls with stubs.

From 0a7b26948acf680765d060d54603ac5c4566b5fd Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Fri, 26 Jan 2024 16:38:17 -0600
Subject: [PATCH 07/10] Update align of u128 to 16

---
 tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs   | 4 ++--
 tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs | 2 +-
 tests/kani/Intrinsics/ConstEval/min_align_of.rs      | 4 ++--
 tests/kani/Intrinsics/ConstEval/pref_align_of.rs     | 4 ++--
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs
index 9e76a55a2cb3..ba482248898c 100644
--- a/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs
+++ b/tests/kani/Intrinsics/AlignOfVal/align_of_basic.rs
@@ -30,13 +30,13 @@ fn main() {
         assert!(min_align_of_val(&0i16) == 2);
         assert!(min_align_of_val(&0i32) == 4);
         assert!(min_align_of_val(&0i64) == 8);
-        assert!(min_align_of_val(&0i128) == 8);
+        assert!(min_align_of_val(&0i128) == 16);
         assert!(min_align_of_val(&0isize) == 8);
         assert!(min_align_of_val(&0u8) == 1);
         assert!(min_align_of_val(&0u16) == 2);
         assert!(min_align_of_val(&0u32) == 4);
         assert!(min_align_of_val(&0u64) == 8);
-        assert!(min_align_of_val(&0u128) == 8);
+        assert!(min_align_of_val(&0u128) == 16);
         assert!(min_align_of_val(&0usize) == 8);
         assert!(min_align_of_val(&0f32) == 4);
         assert!(min_align_of_val(&0f64) == 8);
diff --git a/tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs b/tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs
index e1b3e1dd4491..426f09de1a59 100644
--- a/tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs
+++ b/tests/kani/Intrinsics/AlignOfVal/align_of_fat_ptr.rs
@@ -19,7 +19,7 @@ fn check_align_simple() {
     let a = A { id: 0 };
     let t: &dyn T = &a;
     #[cfg(target_arch = "x86_64")]
-    assert_eq!(align_of_val(t), 8);
+    assert_eq!(align_of_val(t), 16);
     #[cfg(target_arch = "aarch64")]
     assert_eq!(align_of_val(t), 16);
     assert_eq!(align_of_val(&t), 8);
diff --git a/tests/kani/Intrinsics/ConstEval/min_align_of.rs b/tests/kani/Intrinsics/ConstEval/min_align_of.rs
index eed572b8dc9f..425f27084076 100644
--- a/tests/kani/Intrinsics/ConstEval/min_align_of.rs
+++ b/tests/kani/Intrinsics/ConstEval/min_align_of.rs
@@ -19,13 +19,13 @@ fn main() {
         assert!(min_align_of::<i16>() == 2);
         assert!(min_align_of::<i32>() == 4);
         assert!(min_align_of::<i64>() == 8);
-        assert!(min_align_of::<i128>() == 8);
+        assert!(min_align_of::<i128>() == 16);
         assert!(min_align_of::<isize>() == 8);
         assert!(min_align_of::<u8>() == 1);
         assert!(min_align_of::<u16>() == 2);
         assert!(min_align_of::<u32>() == 4);
         assert!(min_align_of::<u64>() == 8);
-        assert!(min_align_of::<u128>() == 8);
+        assert!(min_align_of::<u128>() == 16);
         assert!(min_align_of::<usize>() == 8);
         assert!(min_align_of::<f32>() == 4);
         assert!(min_align_of::<f64>() == 8);
diff --git a/tests/kani/Intrinsics/ConstEval/pref_align_of.rs b/tests/kani/Intrinsics/ConstEval/pref_align_of.rs
index 22ff342a8198..d495bffef5f8 100644
--- a/tests/kani/Intrinsics/ConstEval/pref_align_of.rs
+++ b/tests/kani/Intrinsics/ConstEval/pref_align_of.rs
@@ -19,13 +19,13 @@ fn main() {
         assert!(unsafe { pref_align_of::<i16>() } == 2);
         assert!(unsafe { pref_align_of::<i32>() } == 4);
         assert!(unsafe { pref_align_of::<i64>() } == 8);
-        assert!(unsafe { pref_align_of::<i128>() } == 8);
+        assert!(unsafe { pref_align_of::<i128>() } == 16);
         assert!(unsafe { pref_align_of::<isize>() } == 8);
         assert!(unsafe { pref_align_of::<u8>() } == 1);
         assert!(unsafe { pref_align_of::<u16>() } == 2);
         assert!(unsafe { pref_align_of::<u32>() } == 4);
         assert!(unsafe { pref_align_of::<u64>() } == 8);
-        assert!(unsafe { pref_align_of::<u128>() } == 8);
+        assert!(unsafe { pref_align_of::<u128>() } == 16);
         assert!(unsafe { pref_align_of::<usize>() } == 8);
         assert!(unsafe { pref_align_of::<f32>() } == 4);
         assert!(unsafe { pref_align_of::<f64>() } == 8);

From a27d8a693259c7954fbccd6c730572bb317c34f2 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Tue, 6 Feb 2024 17:08:19 +0000
Subject: [PATCH 08/10] Avoid extra warnings with simple clean ups

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 tests/perf/hashset/src/lib.rs | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tests/perf/hashset/src/lib.rs b/tests/perf/hashset/src/lib.rs
index fb29db5c7ed6..462e0d5fc108 100644
--- a/tests/perf/hashset/src/lib.rs
+++ b/tests/perf/hashset/src/lib.rs
@@ -6,6 +6,7 @@
 use std::collections::{hash_map::RandomState, HashSet};
 use std::mem::{size_of, size_of_val, transmute};
 
+#[allow(dead_code)]
 fn concrete_state() -> RandomState {
     let keys: [u64; 2] = [0, 0];
     assert_eq!(size_of_val(&keys), size_of::<RandomState>());
@@ -30,7 +31,7 @@ fn check_insert() {
 #[kani::solver(kissat)]
 fn check_contains() {
     let first = kani::any();
-    let mut set: HashSet<i8> = HashSet::from([first]);
+    let set: HashSet<i8> = HashSet::from([first]);
     assert!(set.contains(&first));
 }
 
@@ -38,7 +39,7 @@ fn check_contains() {
 #[kani::stub(RandomState::new, concrete_state)]
 #[kani::unwind(2)]
 fn check_contains_str() {
-    let mut set = HashSet::from(["s"]);
+    let set = HashSet::from(["s"]);
     assert!(set.contains(&"s"));
 }
 

From 15999c20bd793da45e32a6badc72a407c7fb102f Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Thu, 8 Feb 2024 01:08:42 +0000
Subject: [PATCH 09/10] Move check_insert_two_concrete to list of slow tests

Some change has dramatically increase the memory usage for this harness.
For now, we should include this harness in the list of slow tests until
we are able to identify the cause.
We also fix the unwind in the remaning harnesses.

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 tests/perf/hashset/src/lib.rs | 37 ++++++++++++++++++-----------------
 1 file changed, 19 insertions(+), 18 deletions(-)

diff --git a/tests/perf/hashset/src/lib.rs b/tests/perf/hashset/src/lib.rs
index 462e0d5fc108..e2f1fc16666a 100644
--- a/tests/perf/hashset/src/lib.rs
+++ b/tests/perf/hashset/src/lib.rs
@@ -1,6 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: --enable-stubbing --enable-unstable
+// kani-flags: -Z stubbing
 //! Try to verify HashSet basic behavior.
 
 use std::collections::{hash_map::RandomState, HashSet};
@@ -15,7 +15,7 @@ fn concrete_state() -> RandomState {
 
 #[kani::proof]
 #[kani::stub(RandomState::new, concrete_state)]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(kissat)]
 fn check_insert() {
     let mut set: HashSet<i32> = HashSet::default();
@@ -27,7 +27,7 @@ fn check_insert() {
 
 #[kani::proof]
 #[kani::stub(RandomState::new, concrete_state)]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
 #[kani::solver(kissat)]
 fn check_contains() {
     let first = kani::any();
@@ -37,31 +37,19 @@ fn check_contains() {
 
 #[kani::proof]
 #[kani::stub(RandomState::new, concrete_state)]
-#[kani::unwind(2)]
+#[kani::unwind(5)]
+#[kani::solver(kissat)]
 fn check_contains_str() {
     let set = HashSet::from(["s"]);
     assert!(set.contains(&"s"));
 }
 
-#[kani::proof]
-#[kani::stub(RandomState::new, concrete_state)]
-#[kani::unwind(2)]
-#[kani::solver(kissat)]
-fn check_insert_two_concrete() {
-    let mut set: HashSet<i32> = HashSet::default();
-    let first = 10;
-    let second = 20;
-    set.insert(first);
-    set.insert(second);
-    assert_eq!(set.len(), 2);
-}
-
 // too slow so don't run in the regression for now
 #[cfg(slow)]
 mod slow {
     #[kani::proof]
     #[kani::stub(RandomState::new, concrete_state)]
-    #[kani::unwind(3)]
+    #[kani::unwind(5)]
     fn check_insert_two_elements() {
         let mut set: HashSet<i8> = HashSet::default();
         let first = kani::any();
@@ -72,4 +60,17 @@ mod slow {
 
         if first == second { assert_eq!(set.len(), 1) } else { assert_eq!(set.len(), 2) }
     }
+
+    #[kani::proof]
+    #[kani::stub(RandomState::new, concrete_state)]
+    #[kani::unwind(5)]
+    #[kani::solver(kissat)]
+    fn check_insert_two_concrete() {
+        let mut set: HashSet<i32> = HashSet::default();
+        let first = 10;
+        let second = 20;
+        set.insert(first);
+        set.insert(second);
+        assert_eq!(set.len(), 2);
+    }
 }

From 5537c02f63002dadf840ce5d0cfe4997f0de6b15 Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Thu, 8 Feb 2024 02:34:51 +0000
Subject: [PATCH 10/10] Update expected perf/hashset result

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 tests/perf/hashset/expected | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/perf/hashset/expected b/tests/perf/hashset/expected
index 8ba783d580f9..1fbcbbd13c25 100644
--- a/tests/perf/hashset/expected
+++ b/tests/perf/hashset/expected
@@ -1 +1 @@
-4 successfully verified harnesses, 0 failures, 4 total
+3 successfully verified harnesses, 0 failures, 3 total