From 6af63e8cc79d3b58f26f67343f3469adc301ba48 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 8 Dec 2023 12:21:48 -0800
Subject: [PATCH 1/5] Start to move rvalue to StableMIR

---
 .../codegen/intrinsic.rs                      |   6 +-
 .../codegen_cprover_gotoc/codegen/place.rs    |  14 +-
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 510 +++++++++---------
 .../codegen/statement.rs                      |   6 +-
 .../codegen/ty_stable.rs                      |  36 +-
 kani-compiler/src/kani_middle/coercion.rs     |  80 ++-
 6 files changed, 363 insertions(+), 289 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 88aecf947975..264f68627b7e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -426,7 +426,11 @@ impl<'tcx> GotocCtx<'tcx> {
             "cttz_nonzero" => codegen_count_intrinsic!(cttz, false),
             "discriminant_value" => {
                 let ty = instance.args.type_at(0);
-                let e = self.codegen_get_discriminant(fargs.remove(0).dereference(), ty, ret_ty);
+                let e = self.codegen_get_discriminant(
+                    fargs.remove(0).dereference(),
+                    rustc_internal::stable(ty),
+                    ret_ty,
+                );
                 self.codegen_expr_to_place(p, e)
             }
             "exact_div" => self.codegen_exact_div(fargs, p, loc),
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index beb35d469391..80c1e3ee39d6 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -14,11 +14,8 @@ use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::unwrap_or_return_codegen_unimplemented;
 use cbmc::goto_program::{Expr, Location, Type};
+use rustc_middle::mir::{Local as LocalInternal, Place as PlaceInternal};
 use rustc_middle::ty::layout::LayoutOf;
-use rustc_middle::{
-    mir::{Local as LocalInternal, Place as PlaceInternal},
-    ty::Ty as TyInternal,
-};
 use rustc_smir::rustc_internal;
 use rustc_target::abi::{TagEncoding, Variants};
 use stable_mir::mir::{FieldIdx, Local, Mutability, Place, ProjectionElem};
@@ -152,13 +149,12 @@ impl ProjectedPlace {
         }
     }
 
-    pub fn try_new_internal<'tcx>(
+    pub fn try_from_ty(
         goto_expr: Expr,
-        ty: TyInternal<'tcx>,
-        ctx: &mut GotocCtx<'tcx>,
+        ty: Ty,
+        ctx: &mut GotocCtx,
     ) -> Result<Self, UnimplementedData> {
-        let ty = ctx.monomorphize(ty);
-        Self::try_new(goto_expr, TypeOrVariant::Type(rustc_internal::stable(ty)), None, None, ctx)
+        Self::try_new(goto_expr, TypeOrVariant::Type(ty), None, None, ctx)
     }
 
     pub fn try_new(
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 697a7ba83d2d..cc3b720b033d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -3,11 +3,12 @@
 
 use super::typ::pointee_type;
 use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace;
+use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type_stable, StableConverter};
 use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::kani_middle::coercion::{
-    extract_unsize_casting, CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBase,
+    extract_unsize_casting_stable, CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBaseStable,
 };
 use crate::unwrap_or_return_codegen_unimplemented;
 use cbmc::goto_program::{
@@ -17,21 +18,24 @@ use cbmc::goto_program::{
 use cbmc::MachineModel;
 use cbmc::{btree_string_map, InternString, InternedString};
 use num::bigint::BigInt;
-use rustc_index::IndexVec;
-use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp};
-use rustc_middle::ty::adjustment::PointerCoercion;
-use rustc_middle::ty::layout::LayoutOf;
-use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry};
+use rustc_middle::mir::Rvalue as RvalueInternal;
+use rustc_middle::ty::{self, TyCtxt, VtblEntry};
 use rustc_smir::rustc_internal;
-use rustc_target::abi::{FieldIdx, FieldsShape, Size, TagEncoding, VariantIdx, Variants};
+use rustc_target::abi::{FieldsShape, TagEncoding, Variants};
+use stable_mir::mir::mono::Instance;
+use stable_mir::mir::{
+    AggregateKind, BinOp, CastKind, NullOp, Operand, Place, PointerCoercion, Rvalue, UnOp,
+};
+use stable_mir::ty::{ClosureKind, Const, IntTy, RigidTy, Size, Ty, TyKind, UintTy, VariantIdx};
 use std::collections::BTreeMap;
 use tracing::{debug, trace, warn};
 
 impl<'tcx> GotocCtx<'tcx> {
-    fn codegen_comparison(&mut self, op: &BinOp, e1: &Operand<'tcx>, e2: &Operand<'tcx>) -> Expr {
-        let left_op = self.codegen_operand(e1);
-        let right_op = self.codegen_operand(e2);
-        let is_float = self.operand_ty(e1).is_floating_point();
+    fn codegen_comparison(&mut self, op: &BinOp, e1: &Operand, e2: &Operand) -> Expr {
+        let left_op = self.codegen_operand_stable(e1);
+        let right_op = self.codegen_operand_stable(e2);
+        let is_float =
+            matches!(self.operand_ty_stable(e1).kind(), TyKind::RigidTy(RigidTy::Float(..)));
         comparison_expr(op, left_op, right_op, is_float)
     }
 
@@ -45,17 +49,17 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_comparison_fat_ptr(
         &mut self,
         op: &BinOp,
-        left_op: &Operand<'tcx>,
-        right_op: &Operand<'tcx>,
+        left_op: &Operand,
+        right_op: &Operand,
         loc: Location,
     ) -> Expr {
         debug!(?op, ?left_op, ?right_op, "codegen_comparison_fat_ptr");
-        let left_typ = self.operand_ty(left_op);
-        let right_typ = self.operand_ty(left_op);
+        let left_typ = self.operand_ty_stable(left_op);
+        let right_typ = self.operand_ty_stable(left_op);
         assert_eq!(left_typ, right_typ, "Cannot compare pointers of different types");
-        assert!(self.is_fat_pointer(left_typ));
+        assert!(self.is_fat_pointer_stable(left_typ));
 
-        if self.is_vtable_fat_pointer(left_typ) {
+        if self.is_vtable_fat_pointer_stable(left_typ) {
             // Codegen an assertion failure since vtable comparison is not stable.
             let ret_type = Type::Bool;
             let body = vec![
@@ -70,9 +74,9 @@ impl<'tcx> GotocCtx<'tcx> {
             Expr::statement_expression(body, ret_type).with_location(loc)
         } else {
             // Compare data pointer.
-            let left_ptr = self.codegen_operand(left_op);
+            let left_ptr = self.codegen_operand_stable(left_op);
             let left_data = left_ptr.clone().member("data", &self.symbol_table);
-            let right_ptr = self.codegen_operand(right_op);
+            let right_ptr = self.codegen_operand_stable(right_op);
             let right_data = right_ptr.clone().member("data", &self.symbol_table);
             let data_cmp = comparison_expr(op, left_data.clone(), right_data.clone(), false);
 
@@ -102,14 +106,9 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
-    fn codegen_unchecked_scalar_binop(
-        &mut self,
-        op: &BinOp,
-        e1: &Operand<'tcx>,
-        e2: &Operand<'tcx>,
-    ) -> Expr {
-        let ce1 = self.codegen_operand(e1);
-        let ce2 = self.codegen_operand(e2);
+    fn codegen_unchecked_scalar_binop(&mut self, op: &BinOp, e1: &Operand, e2: &Operand) -> Expr {
+        let ce1 = self.codegen_operand_stable(e1);
+        let ce2 = self.codegen_operand_stable(e2);
         match op {
             BinOp::BitAnd => ce1.bitand(ce2),
             BinOp::BitOr => ce1.bitor(ce2),
@@ -118,7 +117,7 @@ impl<'tcx> GotocCtx<'tcx> {
             BinOp::Rem => ce1.rem(ce2),
             BinOp::ShlUnchecked => ce1.shl(ce2),
             BinOp::ShrUnchecked => {
-                if self.operand_ty(e1).is_signed() {
+                if self.operand_ty_stable(e1).is_signed() {
                     ce1.ashr(ce2)
                 } else {
                     ce1.lshr(ce2)
@@ -128,16 +127,16 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
-    fn codegen_scalar_binop(&mut self, op: &BinOp, e1: &Operand<'tcx>, e2: &Operand<'tcx>) -> Expr {
-        let ce1 = self.codegen_operand(e1);
-        let ce2 = self.codegen_operand(e2);
+    fn codegen_scalar_binop(&mut self, op: &BinOp, e1: &Operand, e2: &Operand) -> Expr {
+        let ce1 = self.codegen_operand_stable(e1);
+        let ce2 = self.codegen_operand_stable(e2);
         match op {
             BinOp::Add => ce1.plus(ce2),
             BinOp::Sub => ce1.sub(ce2),
             BinOp::Mul => ce1.mul(ce2),
             BinOp::Shl => ce1.shl(ce2),
             BinOp::Shr => {
-                if self.operand_ty(e1).is_signed() {
+                if self.operand_ty_stable(e1).is_signed() {
                     ce1.ashr(ce2)
                 } else {
                     ce1.lshr(ce2)
@@ -148,25 +147,22 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Codegens expressions of the type `let a  = [4u8; 6];`
-    fn codegen_rvalue_repeat(
-        &mut self,
-        op: &Operand<'tcx>,
-        sz: ty::Const<'tcx>,
-        loc: Location,
-    ) -> Expr {
-        let op_expr = self.codegen_operand(op);
-        let width = sz.try_eval_target_usize(self.tcx, ty::ParamEnv::reveal_all()).unwrap();
+    fn codegen_rvalue_repeat(&mut self, op: &Operand, sz: Const, loc: Location) -> Expr {
+        let op_expr = self.codegen_operand_stable(op);
+        let width = sz.eval_target_usize().unwrap();
         op_expr.array_constant(width).with_location(loc)
     }
 
-    fn codegen_rvalue_len(&mut self, p: &Place<'tcx>) -> Expr {
-        let pt = self.place_ty(p);
+    fn codegen_rvalue_len(&mut self, p: &Place) -> Expr {
+        let pt = self.place_ty_stable(p);
         match pt.kind() {
-            ty::Array(_, sz) => self.codegen_const_internal(*sz, None),
-            ty::Slice(_) => unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(p))
-                .fat_ptr_goto_expr
-                .unwrap()
-                .member("len", &self.symbol_table),
+            TyKind::RigidTy(RigidTy::Array(_, sz)) => self.codegen_const_internal(*sz, None),
+            TyKind::RigidTy(RigidTy::Slice(_)) => {
+                unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(p))
+                    .fat_ptr_goto_expr
+                    .unwrap()
+                    .member("len", &self.symbol_table)
+            }
             _ => unreachable!("Len(_) called on type that has no length: {:?}", pt),
         }
     }
@@ -175,13 +171,13 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_binop_with_overflow_check(
         &mut self,
         op: &BinOp,
-        left_op: &Operand<'tcx>,
-        right_op: &Operand<'tcx>,
+        left_op: &Operand,
+        right_op: &Operand,
         loc: Location,
     ) -> Expr {
         debug!(?op, "codegen_binop_with_overflow_check");
-        let left = self.codegen_operand(left_op);
-        let right = self.codegen_operand(right_op);
+        let left = self.codegen_operand_stable(left_op);
+        let right = self.codegen_operand_stable(right_op);
         let ret_type = left.typ().clone();
         let (bin_op, op_name) = match op {
             BinOp::AddUnchecked => (BinaryOperator::OverflowResultPlus, "unchecked_add"),
@@ -251,16 +247,16 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_rvalue_checked_binary_op(
         &mut self,
         op: &BinOp,
-        e1: &Operand<'tcx>,
-        e2: &Operand<'tcx>,
-        res_ty: Ty<'tcx>,
+        e1: &Operand,
+        e2: &Operand,
+        res_ty: Ty,
     ) -> Expr {
-        let ce1 = self.codegen_operand(e1);
-        let ce2 = self.codegen_operand(e2);
+        let ce1 = self.codegen_operand_stable(e1);
+        let ce2 = self.codegen_operand_stable(e2);
 
-        fn shift_max(t: Ty<'_>, mm: &MachineModel) -> Expr {
+        fn shift_max(t: Ty, mm: &MachineModel) -> Expr {
             match t.kind() {
-                ty::Int(k) => match k {
+                TyKind::RigidTy(RigidTy::Int(k)) => match k {
                     IntTy::I8 => Expr::int_constant(7, Type::signed_int(8)),
                     IntTy::I16 => Expr::int_constant(15, Type::signed_int(16)),
                     IntTy::I32 => Expr::int_constant(31, Type::signed_int(32)),
@@ -268,7 +264,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     IntTy::I128 => Expr::int_constant(127, Type::signed_int(128)),
                     IntTy::Isize => Expr::int_constant(mm.pointer_width - 1, Type::ssize_t()),
                 },
-                ty::Uint(k) => match k {
+                TyKind::RigidTy(RigidTy::Uint(k)) => match k {
                     UintTy::U8 => Expr::int_constant(7, Type::unsigned_int(8)),
                     UintTy::U16 => Expr::int_constant(15, Type::unsigned_int(16)),
                     UintTy::U32 => Expr::int_constant(31, Type::unsigned_int(32)),
@@ -282,7 +278,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         match op {
             BinOp::Add => {
-                let res_type = self.codegen_ty(res_ty);
+                let res_type = self.codegen_ty_stable(res_ty);
                 self.codegen_binop_with_overflow(
                     BinaryOperator::OverflowResultPlus,
                     ce1,
@@ -292,7 +288,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 )
             }
             BinOp::Sub => {
-                let res_type = self.codegen_ty(res_ty);
+                let res_type = self.codegen_ty_stable(res_ty);
                 self.codegen_binop_with_overflow(
                     BinaryOperator::OverflowResultMinus,
                     ce1,
@@ -302,7 +298,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 )
             }
             BinOp::Mul => {
-                let res_type = self.codegen_ty(res_ty);
+                let res_type = self.codegen_ty_stable(res_ty);
                 self.codegen_binop_with_overflow(
                     BinaryOperator::OverflowResultMult,
                     ce1,
@@ -312,25 +308,25 @@ impl<'tcx> GotocCtx<'tcx> {
                 )
             }
             BinOp::Shl => {
-                let t1 = self.operand_ty(e1);
+                let t1 = self.operand_ty_stable(e1);
                 let max = shift_max(t1, self.symbol_table.machine_model());
                 Expr::struct_expr_from_values(
-                    self.codegen_ty(res_ty),
+                    self.codegen_ty_stable(res_ty),
                     vec![
                         ce1.shl(ce2.clone()),
-                        ce2.cast_to(self.codegen_ty(t1)).gt(max).cast_to(Type::c_bool()),
+                        ce2.cast_to(self.codegen_ty_stable(t1)).gt(max).cast_to(Type::c_bool()),
                     ],
                     &self.symbol_table,
                 )
             }
             BinOp::Shr => {
-                let t1 = self.operand_ty(e1);
+                let t1 = self.operand_ty_stable(e1);
                 let max = shift_max(t1, self.symbol_table.machine_model());
                 Expr::struct_expr_from_values(
-                    self.codegen_ty(res_ty),
+                    self.codegen_ty_stable(res_ty),
                     vec![
                         if t1.is_signed() { ce1.ashr(ce2.clone()) } else { ce1.lshr(ce2.clone()) },
-                        ce2.cast_to(self.codegen_ty(t1)).gt(max).cast_to(Type::c_bool()),
+                        ce2.cast_to(self.codegen_ty_stable(t1)).gt(max).cast_to(Type::c_bool()),
                     ],
                     &self.symbol_table,
                 )
@@ -341,10 +337,10 @@ impl<'tcx> GotocCtx<'tcx> {
 
     fn codegen_rvalue_binary_op(
         &mut self,
-        ty: Ty<'tcx>,
+        ty: Ty,
         op: &BinOp,
-        e1: &Operand<'tcx>,
-        e2: &Operand<'tcx>,
+        e1: &Operand,
+        e2: &Operand,
         loc: Location,
     ) -> Expr {
         match op {
@@ -364,7 +360,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             BinOp::Div | BinOp::Rem => {
                 let result = self.codegen_unchecked_scalar_binop(op, e1, e2);
-                if self.operand_ty(e1).is_integral() {
+                if self.operand_ty_stable(e1).is_integral() {
                     let is_rem = matches!(op, BinOp::Rem);
                     let check = self.check_div_overflow(e1, e2, is_rem, loc);
                     Expr::statement_expression(
@@ -379,7 +375,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_unchecked_scalar_binop(op, e1, e2)
             }
             BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => {
-                if self.is_fat_pointer(self.operand_ty(e1)) {
+                if self.is_fat_pointer_stable(self.operand_ty_stable(e1)) {
                     self.codegen_comparison_fat_ptr(op, e1, e2, loc)
                 } else {
                     self.codegen_comparison(op, e1, e2)
@@ -387,8 +383,8 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             // https://doc.rust-lang.org/std/primitive.pointer.html#method.offset
             BinOp::Offset => {
-                let ce1 = self.codegen_operand(e1);
-                let ce2 = self.codegen_operand(e2);
+                let ce1 = self.codegen_operand_stable(e1);
+                let ce2 = self.codegen_operand_stable(e2);
 
                 // Check that computing `offset` in bytes would not overflow
                 let (offset_bytes, bytes_overflow_check) = self.count_in_bytes(
@@ -426,12 +422,12 @@ impl<'tcx> GotocCtx<'tcx> {
     /// lowered to `BinOp::Div`. Prefer adding duplicated checks for now.
     fn check_div_overflow(
         &mut self,
-        dividend: &Operand<'tcx>,
-        divisor: &Operand<'tcx>,
+        dividend: &Operand,
+        divisor: &Operand,
         is_remainder: bool,
         loc: Location,
     ) -> Stmt {
-        let divisor_expr = self.codegen_operand(divisor);
+        let divisor_expr = self.codegen_operand_stable(divisor);
         let msg = if is_remainder {
             "attempt to calculate the remainder with a divisor of zero"
         } else {
@@ -443,8 +439,8 @@ impl<'tcx> GotocCtx<'tcx> {
             msg,
             loc,
         );
-        if self.operand_ty(dividend).is_signed() {
-            let dividend_expr = self.codegen_operand(dividend);
+        if self.operand_ty_stable(dividend).is_signed() {
+            let dividend_expr = self.codegen_operand_stable(dividend);
             let overflow_msg = if is_remainder {
                 "attempt to calculate the remainder with overflow"
             } else {
@@ -470,12 +466,12 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Shifts on an integer of type T are UB if shift distance < 0 or >= T::BITS.
     fn check_unchecked_shift_distance(
         &mut self,
-        value: &Operand<'tcx>,
-        distance: &Operand<'tcx>,
+        value: &Operand,
+        distance: &Operand,
         loc: Location,
     ) -> Stmt {
-        let value_expr = self.codegen_operand(value);
-        let distance_expr = self.codegen_operand(distance);
+        let value_expr = self.codegen_operand_stable(value);
+        let distance_expr = self.codegen_operand_stable(distance);
         let value_width = value_expr.typ().sizeof_in_bits(&self.symbol_table);
         let value_width_expr = Expr::int_constant(value_width, distance_expr.typ().clone());
 
@@ -500,19 +496,15 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Create an initializer for a coroutine struct.
-    fn codegen_rvalue_coroutine(
-        &mut self,
-        operands: &IndexVec<FieldIdx, Operand<'tcx>>,
-        ty: Ty<'tcx>,
-    ) -> Expr {
-        let layout = self.layout_of(ty);
+    fn codegen_rvalue_coroutine(&mut self, operands: &[Operand], ty: Ty) -> Expr {
+        let layout = self.layout_of_stable(ty);
         let discriminant_field = match &layout.variants {
             Variants::Multiple { tag_encoding: TagEncoding::Direct, tag_field, .. } => tag_field,
             _ => unreachable!(
                 "Expected coroutines to have multiple variants and direct encoding, but found: {layout:?}"
             ),
         };
-        let overall_t = self.codegen_ty(ty);
+        let overall_t = self.codegen_ty_stable(ty);
         let direct_fields = overall_t.lookup_field("direct_fields", &self.symbol_table).unwrap();
         let direct_fields_expr = Expr::struct_expr_from_values(
             direct_fields.typ(),
@@ -524,7 +516,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     if idx == *discriminant_field {
                         Expr::int_constant(0, self.codegen_ty(field_ty))
                     } else {
-                        self.codegen_operand(&operands[idx.into()])
+                        self.codegen_operand_stable(&operands[idx.into()])
                     }
                 })
                 .collect(),
@@ -541,12 +533,12 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_rvalue_enum_aggregate(
         &mut self,
         variant_index: VariantIdx,
-        operands: &IndexVec<FieldIdx, Operand<'tcx>>,
-        res_ty: Ty<'tcx>,
+        operands: &[Operand],
+        res_ty: Ty,
         loc: Location,
     ) -> Expr {
         let mut stmts = vec![];
-        let typ = self.codegen_ty(res_ty);
+        let typ = self.codegen_ty_stable(res_ty);
         // 1- Create a temporary value of the enum type.
         tracing::debug!(?typ, ?res_ty, "aggregate_enum");
         let (temp_var, decl) = self.decl_temp_variable(typ.clone(), None, loc);
@@ -554,11 +546,11 @@ impl<'tcx> GotocCtx<'tcx> {
         if !operands.is_empty() {
             // 2- Initialize the members of the temporary variant.
             let initial_projection =
-                ProjectedPlace::try_new_internal(temp_var.clone(), res_ty, self).unwrap();
+                ProjectedPlace::try_new_ty(temp_var.clone(), res_ty, self).unwrap();
             let variant_proj = self
                 .codegen_variant_lvalue(initial_projection, rustc_internal::stable(variant_index));
             let variant_expr = variant_proj.goto_expr.clone();
-            let layout = self.layout_of(res_ty);
+            let layout = self.layout_of_stable(res_ty);
             let fields = match &layout.variants {
                 Variants::Single { index } => {
                     if *index != variant_index {
@@ -578,7 +570,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 variant_expr.typ().clone(),
                 fields
                     .index_by_increasing_offset()
-                    .map(|idx| self.codegen_operand(&operands[idx.into()]))
+                    .map(|idx| self.codegen_operand_stable(&operands[idx.into()]))
                     .collect(),
                 &self.symbol_table,
             );
@@ -586,8 +578,12 @@ impl<'tcx> GotocCtx<'tcx> {
             stmts.push(assign_case);
         }
         // 3- Set discriminant.
-        let set_discriminant =
-            self.codegen_set_discriminant(res_ty, temp_var.clone(), variant_index, loc);
+        let set_discriminant = self.codegen_set_discriminant(
+            rustc_internal::internal(res_ty),
+            temp_var.clone(),
+            rust_target::abit::VariantIndex.from(variant_index),
+            loc,
+        );
         stmts.push(set_discriminant);
         // 4- Return temporary variable.
         stmts.push(temp_var.as_stmt(loc));
@@ -596,35 +592,38 @@ impl<'tcx> GotocCtx<'tcx> {
 
     fn codegen_rvalue_aggregate(
         &mut self,
-        aggregate: &AggregateKind<'tcx>,
-        operands: &IndexVec<FieldIdx, Operand<'tcx>>,
-        res_ty: Ty<'tcx>,
+        aggregate: &AggregateKind,
+        operands: &[Operand],
+        res_ty: Ty,
         loc: Location,
     ) -> Expr {
         match *aggregate {
             AggregateKind::Array(_et) => {
-                let typ = self.codegen_ty(res_ty);
-                Expr::array_expr(typ, operands.iter().map(|o| self.codegen_operand(o)).collect())
+                let typ = self.codegen_ty_stable(res_ty);
+                Expr::array_expr(
+                    typ,
+                    operands.iter().map(|o| self.codegen_operand_stable(o)).collect(),
+                )
             }
             AggregateKind::Adt(_, _, _, _, Some(active_field_index)) => {
                 assert!(res_ty.is_union());
                 assert_eq!(operands.len(), 1);
-                let typ = self.codegen_ty(res_ty);
+                let typ = self.codegen_ty_stable(res_ty);
                 let components = typ.lookup_components(&self.symbol_table).unwrap();
                 Expr::union_expr(
                     typ,
                     components[active_field_index.as_usize()].name(),
-                    self.codegen_operand(&operands[0usize.into()]),
+                    self.codegen_operand_stable(&operands[0usize.into()]),
                     &self.symbol_table,
                 )
             }
             AggregateKind::Adt(_, _, _, _, _) if res_ty.is_simd() => {
-                let typ = self.codegen_ty(res_ty);
-                let layout = self.layout_of(res_ty);
+                let typ = self.codegen_ty_stable(res_ty);
+                let layout = self.layout_of_stable(res_ty);
                 trace!(shape=?layout.fields, "codegen_rvalue_aggregate");
                 assert!(operands.len() > 0, "SIMD vector cannot be empty");
                 if operands.len() == 1 {
-                    let data = self.codegen_operand(&operands[0u32.into()]);
+                    let data = self.codegen_operand_stable(&operands[0u32.into()]);
                     if data.typ().is_array() {
                         // Array-based SIMD representation.
                         data.transmute_to(typ, &self.symbol_table)
@@ -639,7 +638,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         layout
                             .fields
                             .index_by_increasing_offset()
-                            .map(|idx| self.codegen_operand(&operands[idx.into()]))
+                            .map(|idx| self.codegen_operand_stable(&operands[idx.into()]))
                             .collect(),
                     )
                 }
@@ -648,14 +647,14 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_rvalue_enum_aggregate(variant_index, operands, res_ty, loc)
             }
             AggregateKind::Adt(..) | AggregateKind::Closure(..) | AggregateKind::Tuple => {
-                let typ = self.codegen_ty(res_ty);
-                let layout = self.layout_of(res_ty);
+                let typ = self.codegen_ty_stable(res_ty);
+                let layout = self.layout_of_stable(res_ty);
                 Expr::struct_expr_from_values(
                     typ,
                     layout
                         .fields
                         .index_by_increasing_offset()
-                        .map(|idx| self.codegen_operand(&operands[idx.into()]))
+                        .map(|idx| self.codegen_operand_stable(&operands[idx.into()]))
                         .collect(),
                     &self.symbol_table,
                 )
@@ -664,15 +663,16 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
-    pub fn codegen_rvalue(&mut self, rv: &Rvalue<'tcx>, loc: Location) -> Expr {
-        let res_ty = self.rvalue_ty(rv);
+    pub fn codegen_rvalue(&mut self, rv: &RvalueInternal, loc: Location) -> Expr {
+        self.codegen_rvalue_stable(&StableConverter::convert_rvalue(rv), loc)
+    }
+
+    pub fn codegen_rvalue_stable(&mut self, rv: &Rvalue, loc: Location) -> Expr {
+        let res_ty = self.rvalue_ty_stable(rv);
         debug!(?rv, "codegen_rvalue");
         match rv {
-            Rvalue::Use(p) => self.codegen_operand(p),
-            Rvalue::Repeat(op, sz) => {
-                let sz = self.monomorphize(*sz);
-                self.codegen_rvalue_repeat(op, sz, loc)
-            }
+            Rvalue::Use(p) => self.codegen_operand_stable(p),
+            Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, loc),
             Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => self.codegen_place_ref(p),
             Rvalue::Len(p) => self.codegen_rvalue_len(p),
             // Rust has begun distinguishing "ptr -> num" and "num -> ptr" (providence-relevant casts) but we do not yet:
@@ -693,7 +693,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_misc_cast(e, t)
             }
             Rvalue::Cast(CastKind::DynStar, _, _) => {
-                let ty = self.codegen_ty(res_ty);
+                let ty = self.codegen_ty_stable(res_ty);
                 self.codegen_unimplemented_expr(
                     "CastKind::DynStar",
                     ty,
@@ -706,21 +706,19 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_pointer_cast(k, e, t, loc)
             }
             Rvalue::Cast(CastKind::Transmute, operand, ty) => {
-                let goto_typ = self.codegen_ty(self.monomorphize(*ty));
-                self.codegen_operand(operand).transmute_to(goto_typ, &self.symbol_table)
+                let goto_typ = self.codegen_ty_stable(self.monomorphize(*ty));
+                self.codegen_operand_stable(operand).transmute_to(goto_typ, &self.symbol_table)
             }
-            Rvalue::BinaryOp(op, box (ref e1, ref e2)) => {
-                self.codegen_rvalue_binary_op(res_ty, op, e1, e2, loc)
-            }
-            Rvalue::CheckedBinaryOp(op, box (ref e1, ref e2)) => {
+            Rvalue::BinaryOp(op, e1, e2) => self.codegen_rvalue_binary_op(res_ty, op, e1, e2, loc),
+            Rvalue::CheckedBinaryOp(op, e1, e2) => {
                 self.codegen_rvalue_checked_binary_op(op, e1, e2, res_ty)
             }
             Rvalue::NullaryOp(k, t) => {
                 let t = self.monomorphize(*t);
-                let layout = self.layout_of(t);
+                let layout = self.layout_of_stable(t);
                 match k {
                     NullOp::SizeOf => Expr::int_constant(layout.size.bytes_usize(), Type::size_t())
-                        .with_size_of_annotation(self.codegen_ty(t)),
+                        .with_size_of_annotation(self.codegen_ty_stable(t)),
                     NullOp::AlignOf => Expr::int_constant(layout.align.abi.bytes(), Type::size_t()),
                     NullOp::OffsetOf(fields) => Expr::int_constant(
                         layout.offset_of_subfield(self, fields.iter()).bytes(),
@@ -731,28 +729,27 @@ impl<'tcx> GotocCtx<'tcx> {
             Rvalue::ShallowInitBox(ref operand, content_ty) => {
                 // The behaviour of ShallowInitBox is simply transmuting *mut u8 to Box<T>.
                 // See https://github.com/rust-lang/compiler-team/issues/460 for more details.
-                let operand = self.codegen_operand(operand);
-                let t = self.monomorphize(*content_ty);
-                let box_ty = Ty::new_box(self.tcx, t);
-                let box_ty = self.codegen_ty(box_ty);
-                let cbmc_t = self.codegen_ty(t);
+                let operand = self.codegen_operand_stable(operand);
+                let box_ty = Ty::new_box(*content_ty);
+                let box_ty = self.codegen_ty_stable(box_ty);
+                let cbmc_t = self.codegen_ty_stable(*content_ty);
                 let box_contents = operand.cast_to(cbmc_t.to_pointer());
                 self.box_value(box_contents, box_ty)
             }
             Rvalue::UnaryOp(op, e) => match op {
                 UnOp::Not => {
-                    if self.operand_ty(e).is_bool() {
-                        self.codegen_operand(e).not()
+                    if self.operand_ty_stable(e).is_bool() {
+                        self.codegen_operand_stable(e).not()
                     } else {
-                        self.codegen_operand(e).bitnot()
+                        self.codegen_operand_stable(e).bitnot()
                     }
                 }
-                UnOp::Neg => self.codegen_operand(e).neg(),
+                UnOp::Neg => self.codegen_operand_stable(e).neg(),
             },
             Rvalue::Discriminant(p) => {
                 let place =
                     unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(p)).goto_expr;
-                let pt = self.place_ty(p);
+                let pt = self.place_ty_stable(p);
                 self.codegen_get_discriminant(place, pt, res_ty)
             }
             Rvalue::Aggregate(ref k, operands) => {
@@ -766,13 +763,14 @@ impl<'tcx> GotocCtx<'tcx> {
             // A CopyForDeref is equivalent to a read from a place at the codegen level.
             // https://github.com/rust-lang/rust/blob/1673f1450eeaf4a5452e086db0fe2ae274a0144f/compiler/rustc_middle/src/mir/syntax.rs#L1055
             Rvalue::CopyForDeref(place) => {
-                unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(place)).goto_expr
+                unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place))
+                    .goto_expr
             }
         }
     }
 
-    pub fn codegen_discriminant_field(&self, place: Expr, ty: Ty<'tcx>) -> Expr {
-        let layout = self.layout_of(ty);
+    pub fn codegen_discriminant_field(&self, place: Expr, ty: Ty) -> Expr {
+        let layout = self.layout_of_stable(ty);
         assert!(
             matches!(
                 &layout.variants,
@@ -792,19 +790,19 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// e: ty
     /// get the discriminant of e, of type res_ty
-    pub fn codegen_get_discriminant(&mut self, e: Expr, ty: Ty<'tcx>, res_ty: Ty<'tcx>) -> Expr {
-        let layout = self.layout_of(ty);
+    pub fn codegen_get_discriminant(&mut self, e: Expr, ty: Ty, res_ty: Ty) -> Expr {
+        let layout = self.layout_of_stable(ty);
         match &layout.variants {
             Variants::Single { index } => {
                 let discr_val = layout
                     .ty
                     .discriminant_for_variant(self.tcx, *index)
                     .map_or(index.as_u32() as u128, |discr| discr.val);
-                Expr::int_constant(discr_val, self.codegen_ty(res_ty))
+                Expr::int_constant(discr_val, self.codegen_ty_stable(res_ty))
             }
             Variants::Multiple { tag_encoding, .. } => match tag_encoding {
                 TagEncoding::Direct => {
-                    self.codegen_discriminant_field(e, ty).cast_to(self.codegen_ty(res_ty))
+                    self.codegen_discriminant_field(e, ty).cast_to(self.codegen_ty_stable(res_ty))
                 }
                 TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
                     // This code follows the logic in the ssa codegen backend:
@@ -824,10 +822,10 @@ impl<'tcx> GotocCtx<'tcx> {
                     // https://github.com/rust-lang/rust/blob/fee75fbe11b1fad5d93c723234178b2a329a3c03/compiler/rustc_codegen_ssa/src/mir/place.rs#L247
                     //
                     // Note: niche_variants can only represent values that fit in a u32.
-                    let result_type = self.codegen_ty(res_ty);
-                    let discr_mir_ty = self.codegen_enum_discr_typ(ty);
+                    let result_type = self.codegen_ty_stable(res_ty);
+                    let discr_mir_ty = self.codegen_enum_discr_typ(rustc_internal::internal(ty));
                     let discr_type = self.codegen_ty(discr_mir_ty);
-                    let niche_val = self.codegen_get_niche(e, offset, discr_type);
+                    let niche_val = self.codegen_get_niche(e, offset.to_bytes, discr_type);
                     let relative_discr =
                         wrapping_sub(&niche_val, u64::try_from(*niche_start).unwrap());
                     let relative_max =
@@ -862,22 +860,22 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Extract the niche value from `v`. This value should be of type `niche_ty` and located
     /// at byte offset `offset`
     pub fn codegen_get_niche(&self, v: Expr, offset: Size, niche_ty: Type) -> Expr {
-        if offset == Size::ZERO {
+        if offset == 0 {
             v.reinterpret_cast(niche_ty)
         } else {
             v // t: T
                 .address_of() // &t: T*
                 .cast_to(Type::unsigned_int(8).to_pointer()) // (u8 *)&t: u8 *
-                .plus(Expr::int_constant(offset.bytes(), Type::size_t())) // ((u8 *)&t) + offset: u8 *
+                .plus(Expr::int_constant(offset, Type::size_t())) // ((u8 *)&t) + offset: u8 *
                 .cast_to(niche_ty.to_pointer()) // (N *)(((u8 *)&t) + offset): N *
                 .dereference() // *(N *)(((u8 *)&t) + offset): N
         }
     }
 
-    fn codegen_fat_ptr_to_fat_ptr_cast(&mut self, src: &Operand<'tcx>, dst_t: Ty<'tcx>) -> Expr {
+    fn codegen_fat_ptr_to_fat_ptr_cast(&mut self, src: &Operand, dst_t: Ty) -> Expr {
         debug!("codegen_fat_ptr_to_fat_ptr_cast |{:?}| |{:?}|", src, dst_t);
-        let src_goto_expr = self.codegen_operand(src);
-        let dst_goto_typ = self.codegen_ty(dst_t);
+        let src_goto_expr = self.codegen_operand_stable(src);
+        let dst_goto_typ = self.codegen_ty_stable(dst_t);
         let dst_data_type = dst_goto_typ.lookup_field_type("data", &self.symbol_table).unwrap();
         let dst_data_field = (
             "data",
@@ -900,10 +898,10 @@ impl<'tcx> GotocCtx<'tcx> {
         )
     }
 
-    fn codegen_fat_ptr_to_thin_ptr_cast(&mut self, src: &Operand<'tcx>, dst_t: Ty<'tcx>) -> Expr {
+    fn codegen_fat_ptr_to_thin_ptr_cast(&mut self, src: &Operand, dst_t: Ty) -> Expr {
         debug!("codegen_fat_ptr_to_thin_ptr_cast |{:?}| |{:?}|", src, dst_t);
-        let src_goto_expr = self.codegen_operand(src);
-        let dst_goto_typ = self.codegen_ty(dst_t);
+        let src_goto_expr = self.codegen_operand_stable(src);
+        let dst_goto_typ = self.codegen_ty_stable(dst_t);
         // In a vtable fat pointer, the data member is a void pointer,
         // so ensure the pointer has the correct type before dereferencing it.
         src_goto_expr.member("data", &self.symbol_table).cast_to(dst_goto_typ)
@@ -911,8 +909,8 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// This handles all kinds of casts, except a limited subset that are instead
     /// handled by [`Self::codegen_pointer_cast`].
-    fn codegen_misc_cast(&mut self, src: &Operand<'tcx>, dst_t: Ty<'tcx>) -> Expr {
-        let src_t = self.operand_ty(src);
+    fn codegen_misc_cast(&mut self, src: &Operand, dst_t: Ty) -> Expr {
+        let src_t = self.operand_ty_stable(src);
         debug!(
             "codegen_misc_cast: casting operand {:?} from type {:?} to type {:?}",
             src, src_t, dst_t
@@ -920,67 +918,78 @@ impl<'tcx> GotocCtx<'tcx> {
 
         // number casting
         if src_t.is_numeric() && dst_t.is_numeric() {
-            return self.codegen_operand(src).cast_to(self.codegen_ty(dst_t));
+            return self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_t));
         }
 
         // Behind the scenes, char is just a 32bit integer
         if (src_t.is_integral() && dst_t.is_char()) || (src_t.is_char() && dst_t.is_integral()) {
-            return self.codegen_operand(src).cast_to(self.codegen_ty(dst_t));
+            return self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_t));
         }
 
         // Cast an enum to its discriminant
         if src_t.is_enum() && dst_t.is_integral() {
-            let operand = self.codegen_operand(src);
+            let operand = self.codegen_operand_stable(src);
             return self.codegen_get_discriminant(operand, src_t, dst_t);
         }
 
         // Cast between fat pointers
-        if self.is_fat_pointer(src_t) && self.is_fat_pointer(dst_t) {
+        if self.is_fat_pointer_stable(src_t) && self.is_fat_pointer_stable(dst_t) {
             return self.codegen_fat_ptr_to_fat_ptr_cast(src, dst_t);
         }
 
-        if self.is_fat_pointer(src_t) && !self.is_fat_pointer(dst_t) {
+        if self.is_fat_pointer_stable(src_t) && !self.is_fat_pointer_stable(dst_t) {
             return self.codegen_fat_ptr_to_thin_ptr_cast(src, dst_t);
         }
 
         // pointer casting. from a pointer / reference to another pointer / reference
         // notice that if fat pointer is involved, it cannot be the destination, which is t.
         match dst_t.kind() {
-            ty::Ref(_, mut dst_subt, _) | ty::RawPtr(ty::TypeAndMut { ty: mut dst_subt, .. }) => {
+            TyKind::RigidTy(RigidTy::Ref(_, mut dst_subt, _))
+            | TyKind::RigidTy(RigidTy::RawPtr(mut dst_subt, ..)) => {
                 // this is a noop in the case dst_subt is a Projection or Opaque type
                 dst_subt = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), dst_subt);
                 match dst_subt.kind() {
-                    ty::Slice(_) | ty::Str | ty::Dynamic(_, _, _) => {
+                    TyKind::RigidTy(RigidTy::Slice(_))
+                    | TyKind::RigidTy(RigidTy::Str)
+                    | TyKind::RigidTy(RigidTy::Dynamic(_, _, _)) => {
                         //TODO: this does the wrong thing on Strings/fixme_boxed_str.rs
                         // if we cast to slice or string, then we know the source is also a slice or string,
                         // so there shouldn't be anything to do
                         //DSN The one time I've seen this for dynamic, it was just casting from const* to mut*
                         // TODO: see if it is accurate
-                        self.codegen_operand(src)
+                        self.codegen_operand_stable(src)
                     }
                     _ => match src_t.kind() {
-                        ty::Ref(_, mut src_subt, _)
-                        | ty::RawPtr(ty::TypeAndMut { ty: mut src_subt, .. }) => {
+                        TyKind::RigidTy(RigidTy::Ref(_, mut src_subt, _))
+                        | TyKind::RigidTy(RigidTy::RawPtr(mut src_subt, ..)) => {
                             // this is a noop in the case dst_subt is a Projection or Opaque type
                             src_subt = self
                                 .tcx
                                 .normalize_erasing_regions(ty::ParamEnv::reveal_all(), src_subt);
                             match src_subt.kind() {
-                                ty::Slice(_) | ty::Str | ty::Dynamic(..) => self
-                                    .codegen_operand(src)
+                                TyKind::RigidTy(RigidTy::Slice(_))
+                                | TyKind::RigidTy(RigidTy::Str)
+                                | TyKind::RigidTy(RigidTy::Dynamic(..)) => self
+                                    .codegen_operand_stable(src)
                                     .member("data", &self.symbol_table)
-                                    .cast_to(self.codegen_ty(dst_t)),
-                                _ => self.codegen_operand(src).cast_to(self.codegen_ty(dst_t)),
+                                    .cast_to(self.codegen_ty_stable(dst_t)),
+                                _ => self
+                                    .codegen_operand_stable(src)
+                                    .cast_to(self.codegen_ty_stable(dst_t)),
                             }
                         }
-                        ty::Int(_) | ty::Uint(_) | ty::FnPtr(..) => {
-                            self.codegen_operand(src).cast_to(self.codegen_ty(dst_t))
+                        TyKind::RigidTy(RigidTy::Int(_))
+                        | TyKind::RigidTy(RigidTy::Uint(_))
+                        | TyKind::RigidTy(RigidTy::FnPtr(..)) => {
+                            self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_t))
                         }
                         _ => unreachable!(),
                     },
                 }
             }
-            ty::Int(_) | ty::Uint(_) => self.codegen_operand(src).cast_to(self.codegen_ty(dst_t)),
+            TyKind::RigidTy(RigidTy::Int(_)) | TyKind::RigidTy(RigidTy::Uint(_)) => {
+                self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_t))
+            }
             _ => unreachable!(),
         }
     }
@@ -991,38 +1000,36 @@ impl<'tcx> GotocCtx<'tcx> {
     /// many of which are instead handled by [`Self::codegen_misc_cast`] instead.
     fn codegen_pointer_cast(
         &mut self,
-        k: &PointerCoercion,
-        operand: &Operand<'tcx>,
-        t: Ty<'tcx>,
+        coercion: &PointerCoercion,
+        operand: &Operand,
+        t: Ty,
         loc: Location,
     ) -> Expr {
-        debug!(cast=?k, op=?operand, ?loc, "codegen_pointer_cast");
-        match k {
-            PointerCoercion::ReifyFnPointer => match self.operand_ty(operand).kind() {
-                ty::FnDef(def_id, args) => {
-                    let instance =
-                        Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
-                            .unwrap()
-                            .unwrap();
-                    // We need to handle this case in a special way because `codegen_operand` compiles FnDefs to dummy structs.
+        debug!(cast=?coercion, op=?operand, ?loc, "codegen_pointer_cast");
+        match coercion {
+            PointerCoercion::ReifyFnPointer => match self.operand_ty_stable(operand).kind() {
+                TyKind::RigidTy(RigidTy::FnDef(def, args)) => {
+                    let instance = Instance::resolve(def, &args).unwrap().unwrap();
+                    // We need to handle this case in a special way because `codegen_operand_stable` compiles FnDefs to dummy structs.
                     // (cf. the function documentation)
                     self.codegen_func_expr_internal(instance, None).address_of()
                 }
                 _ => unreachable!(),
             },
-            PointerCoercion::UnsafeFnPointer => self.codegen_operand(operand),
+            PointerCoercion::UnsafeFnPointer => self.codegen_operand_stable(operand),
             PointerCoercion::ClosureFnPointer(_) => {
-                if let ty::Closure(def_id, args) = self.operand_ty(operand).kind() {
-                    let instance =
-                        Instance::resolve_closure(self.tcx, *def_id, args, ty::ClosureKind::FnOnce)
-                            .expect("failed to normalize and resolve closure during codegen")
-                            .polymorphize(self.tcx);
+                if let TyKind::RigidTy(RigidTy::Closure(def, args)) =
+                    self.operand_ty_stable(operand).kind()
+                {
+                    let instance = Instance::resolve_closure(def, &args, ClosureKind::FnOnce)
+                        .expect("failed to normalize and resolve closure during codegen")
+                        .polymorphize(self.tcx);
                     self.codegen_func_expr_internal(instance, None).address_of()
                 } else {
                     unreachable!("{:?} cannot be cast to a fn ptr", operand)
                 }
             }
-            PointerCoercion::MutToConstPointer => self.codegen_operand(operand),
+            PointerCoercion::MutToConstPointer => self.codegen_operand_stable(operand),
             PointerCoercion::ArrayToPointer => {
                 // TODO: I am not sure whether it is correct or not.
                 //
@@ -1031,11 +1038,11 @@ impl<'tcx> GotocCtx<'tcx> {
                 // if we had to, then [o] necessarily has type [T; n] where *T is a fat pointer, meaning
                 // T is either [T] or str. but neither type is sized, which shouldn't participate in
                 // codegen.
-                match self.operand_ty(operand).kind() {
-                    ty::RawPtr(ty::TypeAndMut { ty, .. }) => {
+                match self.operand_ty_stable(operand).kind() {
+                    TyKind::RigidTy(RigidTy::RawPtr(ty, ..)) => {
                         // ty must be an array
-                        if let ty::Array(_, _) = ty.kind() {
-                            let oe = self.codegen_operand(operand);
+                        if let TyKind::RigidTy(RigidTy::Array(_, _)) = ty.kind() {
+                            let oe = self.codegen_operand_stable(operand);
                             oe.dereference() // : struct [T; n]
                                 .array_to_ptr() // : T*
                         } else {
@@ -1046,8 +1053,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
             }
             PointerCoercion::Unsize => {
-                let src_goto_expr = self.codegen_operand(operand);
-                let src_mir_type = self.operand_ty(operand);
+                let src_goto_expr = self.codegen_operand_stable(operand);
+                let src_mir_type = self.operand_ty_stable(operand);
                 let dst_mir_type = t;
                 self.codegen_unsized_cast(src_goto_expr, src_mir_type, dst_mir_type)
             }
@@ -1065,8 +1072,8 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_unsized_cast(
         &mut self,
         src_goto_expr: Expr,
-        src_mir_type: Ty<'tcx>,
-        dst_mir_type: Ty<'tcx>,
+        src_mir_type: Ty,
+        dst_mir_type: Ty,
     ) -> Expr {
         // The MIR may include casting that isn't necessary. Detect this early on and return the
         // expression for the RHS.
@@ -1094,13 +1101,13 @@ impl<'tcx> GotocCtx<'tcx> {
     fn collect_unsized_cast_path(
         &self,
         src_goto_expr: Expr,
-        src_mir_type: Ty<'tcx>,
-        dst_mir_type: Ty<'tcx>,
-    ) -> Vec<(CoerceUnsizedInfo<'tcx>, Expr)> {
+        src_mir_type: Ty,
+        dst_mir_type: Ty,
+    ) -> Vec<(CoerceUnsizedInfo, Expr)> {
         let mut field_type = src_goto_expr;
         CoerceUnsizedIterator::new(self.tcx, src_mir_type, dst_mir_type)
             .map(|info| {
-                let expr = if let Some(field_symbol) = info.field {
+                let expr = if let Some(field_symbol) = &info.field {
                     // Generate the expression for the current structure and save the type for
                     // the divergent field.
                     let field_name = field_symbol.as_str().intern();
@@ -1123,12 +1130,12 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_struct_unsized_coercion(
         &mut self,
         src_expr: Expr,
-        info: CoerceUnsizedInfo<'tcx>,
+        info: CoerceUnsizedInfo,
         member_coercion: Expr,
     ) -> Expr {
         assert!(info.src_ty.is_adt(), "Expected struct. Found {:?}", info.src_ty);
         assert!(info.dst_ty.is_adt(), "Expected struct. Found {:?}", info.dst_ty);
-        let dst_goto_type = self.codegen_ty(info.dst_ty);
+        let dst_goto_type = self.codegen_ty_stable(info.dst_ty);
         let src_field_exprs = src_expr.struct_field_exprs(&self.symbol_table);
         let dst_field_exprs = src_field_exprs
             .into_iter()
@@ -1158,21 +1165,16 @@ impl<'tcx> GotocCtx<'tcx> {
         dst_expr
     }
 
-    fn codegen_vtable_method_field(
-        &mut self,
-        instance: Instance<'tcx>,
-        t: Ty<'tcx>,
-        idx: usize,
-    ) -> Expr {
+    fn codegen_vtable_method_field(&mut self, instance: Instance, t: Ty, idx: usize) -> Expr {
         debug!(?instance, typ=?t, %idx, "codegen_vtable_method_field");
         let vtable_field_name = self.vtable_field_name(idx);
-        let vtable_type = Type::struct_tag(self.vtable_name(t));
+        let vtable_type = Type::struct_tag(self.vtable_name_stable(t));
         let field_type =
             vtable_type.lookup_field_type(vtable_field_name, &self.symbol_table).unwrap();
         debug!(?vtable_field_name, ?vtable_type, "codegen_vtable_method_field");
 
         // Lookup in the symbol table using the full symbol table name/key
-        let fn_name = self.symbol_name(instance);
+        let fn_name = self.symbol_name_stable(instance);
 
         if let Some(fn_symbol) = self.symbol_table.lookup(&fn_name) {
             if self.vtable_ctx.emit_vtable_restrictions {
@@ -1194,7 +1196,7 @@ impl<'tcx> GotocCtx<'tcx> {
         } else {
             warn!(
                 "Unable to find vtable symbol for virtual function {}, attempted lookup for symbol name: {}",
-                self.readable_instance_name(instance),
+                instance.name(),
                 fn_name,
             );
             field_type.null()
@@ -1202,9 +1204,9 @@ 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<'tcx>, trait_ty: ty::Ty<'tcx>) -> Expr {
-        let drop_instance = Instance::resolve_drop_in_place(self.tcx, ty).polymorphize(self.tcx);
-        let drop_sym_name: InternedString = self.symbol_name(drop_instance).into();
+    fn codegen_vtable_drop_in_place(&mut self, ty: Ty, trait_ty: ty::Ty) -> Expr {
+        let drop_instance = Instance::resolve_drop_in_place(ty);
+        let drop_sym_name: InternedString = drop_instance.mangled_name().into();
 
         // The drop instance has the concrete object type, for consistency with
         // type codegen we need the trait type for the function parameter.
@@ -1236,15 +1238,15 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// The size and alignment for the vtable is of the underlying type.
-    /// When we get the size and align of a ty::Ref, the TyCtxt::layout_of
+    /// When we get the size and align of a ty::Ref, the TyCtxt::layout_of_stable
     /// returns the correct size to match rustc vtable values. Checked via
     /// Kani-compile-time and CBMC assertions in check_vtable_size.
-    fn codegen_vtable_size_and_align(&mut self, operand_type: Ty<'tcx>) -> (Expr, Expr) {
+    fn codegen_vtable_size_and_align(&mut self, operand_type: Ty) -> (Expr, Expr) {
         debug!("vtable_size_and_align {:?}", operand_type.kind());
-        let vtable_layout = self.layout_of(operand_type);
+        let vtable_layout = self.layout_of_stable(operand_type);
         assert!(!vtable_layout.is_unsized(), "Can't create a vtable for an unsized type");
         let vt_size = Expr::int_constant(vtable_layout.size.bytes(), Type::size_t())
-            .with_size_of_annotation(self.codegen_ty(operand_type));
+            .with_size_of_annotation(self.codegen_ty_stable(operand_type));
         let vt_align = Expr::int_constant(vtable_layout.align.abi.bytes(), Type::size_t());
 
         (vt_size, vt_align)
@@ -1253,10 +1255,10 @@ impl<'tcx> GotocCtx<'tcx> {
     // Check the size are inserting in to the vtable against two sources of
     // truth: (1) the compile-time rustc sizeof functions, and (2) the CBMC
     //  __CPROVER_OBJECT_SIZE function.
-    fn check_vtable_size(&mut self, operand_type: Ty<'tcx>, vt_size: Expr) -> Stmt {
+    fn check_vtable_size(&mut self, operand_type: Ty, vt_size: Expr) -> Stmt {
         // Check against the size we get from the layout from the what we
         // get constructing a value of that type
-        let ty: Type = self.codegen_ty(operand_type);
+        let ty: Type = self.codegen_ty_stable(operand_type);
         let codegen_size = ty.sizeof(&self.symbol_table);
         assert_eq!(vt_size.int_constant_value().unwrap(), BigInt::from(codegen_size));
 
@@ -1269,7 +1271,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // In practice, we have seen this with the Never type, which has size 0:
             // https://play.rust-lang.org/?version=nightly&mode=debug&edition=2018&gist=0f6eef4f6abeb279031444735e73d2e1
             assert!(
-                matches!(operand_type.kind(), ty::Never),
+                matches!(operand_type.kind(), TyKind::RigidTy(RigidTy::Never)),
                 "Expected Never, got: {operand_type:?}"
             );
             Type::size_t().zero()
@@ -1283,27 +1285,26 @@ impl<'tcx> GotocCtx<'tcx> {
         Stmt::block(vec![decl, size_assert], Location::none())
     }
 
-    fn codegen_vtable(&mut self, src_mir_type: Ty<'tcx>, dst_mir_type: Ty<'tcx>) -> Expr {
+    fn codegen_vtable(&mut self, src_mir_type: Ty, dst_mir_type: Ty) -> Expr {
         let trait_type = match dst_mir_type.kind() {
             // DST is pointer type
-            ty::Ref(_, pointee_type, ..) => *pointee_type,
+            TyKind::RigidTy(RigidTy::Ref(_, pointee_type, ..)) => pointee_type,
             // DST is box type
-            ty::Adt(adt_def, adt_subst) if adt_def.is_box() => {
-                adt_subst.first().unwrap().expect_ty()
+            TyKind::RigidTy(RigidTy::Adt(adt_def, adt_subst)) if adt_def.is_box() => {
+                adt_subst.0.first().unwrap().expect_ty()
             }
             // DST is dynamic type
-            ty::Dynamic(..) => dst_mir_type,
-            _ => unimplemented!("Cannot codegen_vtable for type {:?}", dst_mir_type.kind()),
+            TyKind::RigidTy(RigidTy::Dynamic(..)) => dst_mir_type,
+            _ => unreachable!("Cannot codegen_vtable for type {:?}", dst_mir_type.kind()),
         };
-        assert!(trait_type.is_trait(), "VTable trait type {trait_type} must be a trait type");
         let binders = match trait_type.kind() {
-            ty::Dynamic(binders, ..) => binders,
-            _ => unimplemented!("Cannot codegen_vtable for type {:?}", dst_mir_type.kind()),
+            TyKind::RigidTy(RigidTy::Dynamic(binders, ..)) => binders,
+            _ => unreachable!("Cannot codegen_vtable for type {:?}", dst_mir_type.kind()),
         };
 
-        let src_name = self.ty_mangled_name(src_mir_type);
+        let src_name = self.ty_mangled_name(rustc_internal::internal(src_mir_type));
         // The name needs to be the same as inserted in typ.rs
-        let vtable_name = self.vtable_name(trait_type).intern();
+        let vtable_name = self.vtable_name_stable(trait_type).intern();
         let vtable_impl_name = format!("{vtable_name}_impl_for_{src_name}");
 
         self.ensure_global_var(
@@ -1363,31 +1364,34 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_cast_to_fat_pointer(
         &mut self,
         src_goto_expr: Expr,
-        coerce_info: CoerceUnsizedInfo<'tcx>,
+        coerce_info: CoerceUnsizedInfo,
     ) -> Expr {
         assert_ne!(coerce_info.src_ty.kind(), coerce_info.dst_ty.kind());
 
         // The fat pointer type.
-        let fat_ptr_type = self.codegen_ty(coerce_info.dst_ty);
+        let fat_ptr_type = self.codegen_ty_stable(coerce_info.dst_ty);
 
         // Extract the type conversion that will require metadata to be saved.
-        let CoercionBase { src_ty: metadata_src_type, dst_ty: metadata_dst_type } =
-            extract_unsize_casting(self.tcx, coerce_info.src_ty, coerce_info.dst_ty);
+        let CoercionBaseStable { src_ty: metadata_src_type, dst_ty: metadata_dst_type } =
+            extract_unsize_casting_stable(self.tcx, coerce_info.src_ty, coerce_info.dst_ty);
 
         // Extract information about the data pointer.
-        let dst_pointee_ty = pointee_type(coerce_info.dst_ty).unwrap();
-        let dst_data_type = self.codegen_ty(dst_pointee_ty).to_pointer();
+        let dst_pointee_ty = pointee_type_stable(coerce_info.dst_ty).unwrap();
+        let dst_data_type = self.codegen_ty_stable(dst_pointee_ty).to_pointer();
 
         debug!(?coerce_info, ?metadata_src_type, ?metadata_dst_type, "codegen_thin_to_fat");
         // Generate the metadata and the fat pointer according to the target of this coercion.
         match (metadata_src_type.kind(), metadata_dst_type.kind()) {
-            (ty::Array(src_elt_type, src_elt_count), ty::Slice(dst_elt_type)) => {
+            (
+                TyKind::RigidTy(RigidTy::Array(src_elt_type, src_elt_count)),
+                TyKind::RigidTy(RigidTy::Slice(dst_elt_type)),
+            ) => {
                 // Cast to a slice fat pointer.
                 assert_eq!(src_elt_type, dst_elt_type);
-                let dst_goto_len = self.codegen_const_internal(*src_elt_count, None);
-                let src_pointee_ty = pointee_type(coerce_info.src_ty).unwrap();
+                let dst_goto_len = self.codegen_const(&src_elt_count, None);
+                let src_pointee_ty = pointee_type_stable(coerce_info.src_ty).unwrap();
                 let dst_data_expr = if src_pointee_ty.is_array() {
-                    src_goto_expr.cast_to(self.codegen_ty(*src_elt_type).to_pointer())
+                    src_goto_expr.cast_to(self.codegen_ty_stable(src_elt_type).to_pointer())
                 } else {
                     // A struct that contains the type being coerced to a slice.
                     // E.g.: Convert Src<[u8; 2]> to Src<[u8]> where struct Src<T> { member: T }
@@ -1395,21 +1399,21 @@ impl<'tcx> GotocCtx<'tcx> {
                 };
                 slice_fat_ptr(fat_ptr_type, dst_data_expr, dst_goto_len, &self.symbol_table)
             }
-            (ty::Dynamic(..), ty::Dynamic(..)) => {
+            (TyKind::RigidTy(RigidTy::Dynamic(..)), TyKind::RigidTy(RigidTy::Dynamic(..))) => {
                 // Cast between fat pointers. Cast the data and the source
                 let src_data = src_goto_expr.to_owned().member("data", &self.symbol_table);
                 let dst_data = src_data.cast_to(dst_data_type);
 
                 // Retrieve the vtable and cast the vtable type.
                 let src_vtable = src_goto_expr.member("vtable", &self.symbol_table);
-                let vtable_name = self.vtable_name(metadata_dst_type);
+                let vtable_name = self.vtable_name_stable(metadata_dst_type);
                 let vtable_ty = Type::struct_tag(vtable_name).to_pointer();
                 let dst_vtable = src_vtable.cast_to(vtable_ty);
 
                 // Construct a fat pointer with the same (casted) fields and new type
                 dynamic_fat_ptr(fat_ptr_type, dst_data, dst_vtable, &self.symbol_table)
             }
-            (_, ty::Dynamic(..)) => {
+            (_, TyKind::RigidTy(RigidTy::Dynamic(..))) => {
                 // Generate the data and vtable pointer that will be stored in the fat pointer.
                 let dst_data_expr = src_goto_expr.cast_to(dst_data_type);
                 let vtable = self.codegen_vtable(metadata_src_type, metadata_dst_type);
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 30a27f231d08..beb7df98e96d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -242,7 +242,8 @@ impl<'tcx> GotocCtx<'tcx> {
                     // The discr.ty doesn't always match the tag type. Explicitly cast if needed.
                     let discr_expr = Expr::int_constant(discr.val, self.codegen_ty(discr.ty))
                         .cast_to(self.codegen_ty(discr_t));
-                    self.codegen_discriminant_field(dest_expr, dest_ty).assign(discr_expr, location)
+                    self.codegen_discriminant_field(dest_expr, rustc_internal::stable(dest_ty))
+                        .assign(discr_expr, location)
                 }
                 TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
                     if *untagged_variant != variant_index {
@@ -262,7 +263,8 @@ impl<'tcx> GotocCtx<'tcx> {
                         } else {
                             Expr::int_constant(niche_value, discr_ty.clone())
                         };
-                        self.codegen_get_niche(dest_expr, offset, discr_ty).assign(value, location)
+                        self.codegen_get_niche(dest_expr, offset.bytes() as usize, discr_ty)
+                            .assign(value, location)
                     } else {
                         Stmt::skip(location)
                     }
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 5c9c235d3164..df6d6e79da05 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
@@ -10,11 +10,13 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Type;
 use rustc_middle::mir;
 use rustc_middle::mir::visit::{MutVisitor, NonUseContext, PlaceContext};
-use rustc_middle::mir::{Operand as OperandInternal, Place as PlaceInternal};
+use rustc_middle::mir::{
+    Operand as OperandInternal, Place as PlaceInternal, Rvalue as RvalueInternal,
+};
 use rustc_middle::ty::{self, Const as ConstInternal, Ty as TyInternal, TyCtxt};
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
-use stable_mir::mir::{Local, Operand, Place};
+use stable_mir::mir::{Local, Operand, Place, Rvalue};
 use stable_mir::ty::{Const, RigidTy, Ty, TyKind};
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -54,6 +56,22 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn use_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
         self.use_fat_pointer(rustc_internal::internal(pointer_ty))
     }
+
+    pub fn is_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
+        self.is_fat_pointer(rustc_internal::internal(pointer_ty))
+    }
+
+    pub fn is_vtable_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
+        self.is_vtable_fat_pointer(rustc_internal::internal(pointer_ty))
+    }
+
+    pub fn vtable_name_stable(&self, ty: Ty) -> String {
+        self.vtable_name(rustc_internal::internal(ty))
+    }
+
+    pub fn rvalue_ty_stable(&self, rvalue: &Rvalue) -> Ty {
+        rvalue.ty(self.current_fn().body().locals()).unwrap()
+    }
 }
 /// If given type is a Ref / Raw ref, return the pointee type.
 pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
@@ -86,6 +104,12 @@ impl<'a, 'tcx> StableConverter<'a, 'tcx> {
         rustc_internal::stable(place)
     }
 
+    pub fn convert_rvalue(gcx: &'a GotocCtx<'tcx>, mut operand: RvalueInternal<'tcx>) -> Rvalue {
+        let mut converter = StableConverter { gcx };
+        converter.visit_rvalue(&mut operand, mir::Location::START);
+        rustc_internal::stable(operand)
+    }
+
     pub fn convert_operand(gcx: &'a GotocCtx<'tcx>, mut operand: OperandInternal<'tcx>) -> Operand {
         let mut converter = StableConverter { gcx };
         converter.visit_operand(&mut operand, mir::Location::START);
@@ -99,6 +123,14 @@ impl<'a, 'tcx> StableConverter<'a, 'tcx> {
     }
 }
 
+pub fn pointee_type_stable(ty: Ty) -> Option<Ty> {
+    match ty.kind() {
+        TyKind::RigidTy(RigidTy::Ref(_, pointee_type, _))
+        | TyKind::RigidTy(RigidTy::RawPtr(ty, ..)) => Some(pointee_type),
+        _ => None,
+    }
+}
+
 impl<'a, 'tcx> MutVisitor<'tcx> for StableConverter<'a, 'tcx> {
     fn tcx(&self) -> TyCtxt<'tcx> {
         self.gcx.tcx
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 0f4be88bc29e..92e59603ae84 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -18,7 +18,9 @@ use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
 use rustc_middle::ty::{self, ParamEnv, Ty, TyCtxt};
 use rustc_middle::ty::{TraitRef, TypeAndMut};
-use rustc_span::symbol::Symbol;
+use rustc_smir::rustc_internal;
+use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
+use stable_mir::Symbol;
 use tracing::trace;
 
 /// Given an unsized coercion (e.g. from `&u8` to `&dyn Debug`), extract the pair of
@@ -57,6 +59,22 @@ use tracing::trace;
 ///    - Extract the tail element of the struct which are of type `T` and `U`, respectively.
 /// 4. Coercion between smart pointers of wrapper structs.
 ///    - Apply the logic from item 2 then item 3.
+pub fn extract_unsize_casting_stable(
+    tcx: TyCtxt,
+    src_ty: TyStable,
+    dst_ty: TyStable,
+) -> CoercionBaseStable {
+    let CoercionBase { src_ty, dst_ty } = extract_unsize_casting(
+        tcx,
+        rustc_internal::internal(src_ty),
+        rustc_internal::internal(dst_ty),
+    );
+    CoercionBaseStable {
+        src_ty: rustc_internal::stable(src_ty),
+        dst_ty: rustc_internal::stable(dst_ty),
+    }
+}
+
 pub fn extract_unsize_casting<'tcx>(
     tcx: TyCtxt<'tcx>,
     src_ty: Ty<'tcx>,
@@ -64,7 +82,13 @@ pub fn extract_unsize_casting<'tcx>(
 ) -> CoercionBase<'tcx> {
     trace!(?src_ty, ?dst_ty, "extract_unsize_casting");
     // Iterate over the pointer structure to find the builtin pointer that will store the metadata.
-    let coerce_info = CoerceUnsizedIterator::new(tcx, src_ty, dst_ty).last().unwrap();
+    let coerce_info = CoerceUnsizedIterator::new(
+        tcx,
+        rustc_internal::stable(src_ty),
+        rustc_internal::stable(dst_ty),
+    )
+    .last()
+    .unwrap();
     // Extract the pointee type that is being coerced.
     let src_pointee_ty = extract_pointee(coerce_info.src_ty).expect(&format!(
         "Expected source to be a pointer. Found {:?} instead",
@@ -100,6 +124,11 @@ pub struct CoercionBase<'tcx> {
     pub dst_ty: Ty<'tcx>,
 }
 
+#[derive(Debug)]
+pub struct CoercionBaseStable {
+    pub src_ty: TyStable,
+    pub dst_ty: TyStable,
+}
 /// Iterates over the coercion path of a structure that implements `CoerceUnsized<T>` trait.
 /// The `CoerceUnsized<T>` trait indicates that this is a pointer or a wrapper for one, where
 /// unsizing can be performed on the pointee. More details:
@@ -117,26 +146,26 @@ pub struct CoercionBase<'tcx> {
 /// After unsized element has been found, the iterator will return `None`.
 pub struct CoerceUnsizedIterator<'tcx> {
     tcx: TyCtxt<'tcx>,
-    src_ty: Option<Ty<'tcx>>,
-    dst_ty: Option<Ty<'tcx>>,
+    src_ty: Option<TyStable>,
+    dst_ty: Option<TyStable>,
 }
 
 /// Represent the information about a coercion.
-#[derive(Debug, Clone, PartialOrd, PartialEq)]
-pub struct CoerceUnsizedInfo<'tcx> {
+#[derive(Debug, Clone, PartialEq)]
+pub struct CoerceUnsizedInfo {
     /// The name of the field from the current types that differs between each other.
     pub field: Option<Symbol>,
     /// The type being coerced.
-    pub src_ty: Ty<'tcx>,
+    pub src_ty: TyStable,
     /// The type that is the result of the coercion.
-    pub dst_ty: Ty<'tcx>,
+    pub dst_ty: TyStable,
 }
 
 impl<'tcx> CoerceUnsizedIterator<'tcx> {
     pub fn new(
         tcx: TyCtxt<'tcx>,
-        src_ty: Ty<'tcx>,
-        dst_ty: Ty<'tcx>,
+        src_ty: TyStable,
+        dst_ty: TyStable,
     ) -> CoerceUnsizedIterator<'tcx> {
         CoerceUnsizedIterator { tcx, src_ty: Some(src_ty), dst_ty: Some(dst_ty) }
     }
@@ -161,7 +190,7 @@ impl<'tcx> CoerceUnsizedIterator<'tcx> {
 /// }
 /// ```
 impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> {
-    type Item = CoerceUnsizedInfo<'tcx>;
+    type Item = CoerceUnsizedInfo;
 
     fn next(&mut self) -> Option<Self::Item> {
         if self.src_ty.is_none() {
@@ -174,21 +203,28 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> {
         let src_ty = self.src_ty.take().unwrap();
         let dst_ty = self.dst_ty.take().unwrap();
         let field = match (&src_ty.kind(), &dst_ty.kind()) {
-            (&ty::Adt(src_def, src_args), &ty::Adt(dst_def, dst_args)) => {
+            (
+                &TyKind::RigidTy(RigidTy::Adt(src_def, src_args)),
+                &TyKind::RigidTy(RigidTy::Adt(dst_def, dst_args)),
+            ) => {
                 // Handle smart pointers by using CustomCoerceUnsized to find the field being
                 // coerced.
                 assert_eq!(src_def, dst_def);
-                let src_fields = &src_def.non_enum_variant().fields;
-                let dst_fields = &dst_def.non_enum_variant().fields;
+                let src_fields = &src_def.variants_iter().next().unwrap().fields();
+                let dst_fields = &dst_def.variants_iter().next().unwrap().fields();
                 assert_eq!(src_fields.len(), dst_fields.len());
 
-                let CustomCoerceUnsized::Struct(coerce_index) =
-                    custom_coerce_unsize_info(self.tcx, src_ty, dst_ty);
-                assert!(coerce_index.as_usize() < src_fields.len());
+                let CustomCoerceUnsized::Struct(coerce_index) = custom_coerce_unsize_info(
+                    self.tcx,
+                    rustc_internal::internal(src_ty),
+                    rustc_internal::internal(dst_ty),
+                );
+                let coerce_index = coerce_index.as_usize();
+                assert!(coerce_index < src_fields.len());
 
-                self.src_ty = Some(src_fields[coerce_index].ty(self.tcx, src_args));
-                self.dst_ty = Some(dst_fields[coerce_index].ty(self.tcx, dst_args));
-                Some(src_fields[coerce_index].name)
+                self.src_ty = Some(src_fields[coerce_index].ty_with_args(&src_args));
+                self.dst_ty = Some(dst_fields[coerce_index].ty_with_args(&dst_args));
+                Some(src_fields[coerce_index].name.clone())
             }
             _ => {
                 // Base case is always a pointer (Box, raw_pointer or reference).
@@ -226,6 +262,6 @@ fn custom_coerce_unsize_info<'tcx>(
 }
 
 /// Extract pointee type from builtin pointer types.
-fn extract_pointee(typ: Ty) -> Option<Ty> {
-    typ.builtin_deref(true).map(|TypeAndMut { ty, .. }| ty)
+fn extract_pointee(typ: TyStable) -> Option<Ty> {
+    rustc_internal::internal(typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty)
 }

From 387a6c9e966773918f5675d8575d23c76ab57842 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 8 Dec 2023 19:17:10 -0800
Subject: [PATCH 2/5] Converting more of rvalue stuff

---
 .../codegen/intrinsic.rs                      |   2 +-
 .../codegen_cprover_gotoc/codegen/operand.rs  |   9 +-
 .../codegen_cprover_gotoc/codegen/place.rs    |  35 ++-
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 222 +++++++++---------
 .../codegen/ty_stable.rs                      |  77 +++++-
 kani-compiler/src/kani_middle/coercion.rs     |  10 +-
 6 files changed, 212 insertions(+), 143 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 264f68627b7e..832837b0c289 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -429,7 +429,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let e = self.codegen_get_discriminant(
                     fargs.remove(0).dereference(),
                     rustc_internal::stable(ty),
-                    ret_ty,
+                    rustc_internal::stable(ret_ty),
                 );
                 self.codegen_expr_to_place(p, e)
             }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index 0f2e0ad609f4..d7d76bb54f81 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -8,7 +8,6 @@ use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Stmt, Sym
 use rustc_middle::mir::Operand as OperandInternal;
 use rustc_middle::ty::{Const as ConstInternal, Instance as InstanceInternal};
 use rustc_smir::rustc_internal;
-use rustc_span::def_id::DefId;
 use rustc_span::Span as SpanInternal;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, StaticDef};
@@ -17,7 +16,7 @@ use stable_mir::ty::{
     Allocation, Const, ConstantKind, FloatTy, FnDef, GenericArgs, IntTy, RigidTy, Size, Span, Ty,
     TyKind, UintTy,
 };
-use stable_mir::CrateDef;
+use stable_mir::{CrateDef, CrateItem};
 use tracing::{debug, trace};
 
 #[derive(Clone, Debug)]
@@ -80,7 +79,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ///   generate code for it as simple literals or constants if possible. Otherwise, we create
     ///   a memory allocation for them and access them indirectly.
     /// - ZeroSized: These are ZST constants and they just need to match the right type.
-    fn codegen_const(&mut self, constant: &Const, span: Option<Span>) -> Expr {
+    pub fn codegen_const(&mut self, constant: &Const, span: Option<Span>) -> Expr {
         trace!(?constant, "codegen_constant");
         match constant.kind() {
             ConstantKind::Allocated(alloc) => self.codegen_allocation(alloc, constant.ty(), span),
@@ -379,8 +378,8 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Generate a goto expression for a pointer to a thread-local variable.
     ///
     /// These are not initialized here, see `codegen_static`.
-    pub fn codegen_thread_local_pointer(&mut self, def_id: DefId) -> Expr {
-        let instance = rustc_internal::stable(InstanceInternal::mono(self.tcx, def_id));
+    pub fn codegen_thread_local_pointer(&mut self, def: CrateItem) -> Expr {
+        let instance = Instance::try_from(def).unwrap();
         self.codegen_instance_pointer(instance, true)
     }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index 80c1e3ee39d6..bac62a19d25e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -6,10 +6,10 @@
 //! in [GotocCtx::codegen_place] below.
 
 use super::typ::TypeExt;
-use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type, StableConverter};
-use crate::codegen_cprover_gotoc::codegen::typ::{
-    pointee_type as pointee_type_internal, std_pointee_type,
+use crate::codegen_cprover_gotoc::codegen::ty_stable::{
+    is_box, is_coroutine, pointee_type, StableConverter,
 };
+use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::unwrap_or_return_codegen_unimplemented;
@@ -411,7 +411,7 @@ impl<'tcx> GotocCtx<'tcx> {
         match proj {
             ProjectionElem::Deref => {
                 let base_type = before.mir_typ();
-                let inner_goto_expr = if is_box(base_type) {
+                let inner_goto_expr = if is_box(&base_type.kind()) {
                     self.deref_box(before.goto_expr)
                 } else {
                     before.goto_expr
@@ -601,7 +601,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     Variants::Single { .. } => before.goto_expr,
                     Variants::Multiple { tag_encoding, .. } => match tag_encoding {
                         TagEncoding::Direct => {
-                            let cases = if is_coroutine(ty_kind) {
+                            let cases = if is_coroutine(&ty_kind) {
                                 before.goto_expr
                             } else {
                                 before.goto_expr.member("cases", &self.symbol_table)
@@ -640,12 +640,17 @@ impl<'tcx> GotocCtx<'tcx> {
     /// - For `*(Wrapper<T>)` where `T: Unsized`, the projection's `goto_expr` returns an object,
     ///   and we need to take it's address and build the fat pointer.
     pub fn codegen_place_ref(&mut self, place: &PlaceInternal<'tcx>) -> Expr {
-        let place_ty = self.place_ty(place);
-        let projection = unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(place));
-        if self.use_thin_pointer(place_ty) {
+        self.codegen_place_ref_stable(&StableConverter::convert_place(self, *place))
+    }
+
+    pub fn codegen_place_ref_stable(&mut self, place: &Place) -> Expr {
+        let place_ty = self.place_ty_stable(place);
+        let projection =
+            unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(place));
+        if self.use_thin_pointer_stable(place_ty) {
             // Just return the address of the place dereferenced.
             projection.goto_expr.address_of()
-        } else if place_ty == pointee_type_internal(self.local_ty(place.local)).unwrap() {
+        } else if place_ty == pointee_type(self.local_ty_stable(place.local)).unwrap() {
             // Just return the fat pointer if this is a simple &(*local).
             projection.fat_ptr_goto_expr.unwrap()
         } else {
@@ -653,8 +658,8 @@ impl<'tcx> GotocCtx<'tcx> {
             // original fat pointer.
             let data = projection_data_ptr(&projection);
             let fat_ptr = projection.fat_ptr_goto_expr.unwrap();
-            let place_type = self.codegen_ty_ref(place_ty);
-            if self.use_vtable_fat_pointer(place_ty) {
+            let place_type = self.codegen_ty_ref_stable(place_ty);
+            if self.use_vtable_fat_pointer_stable(place_ty) {
                 let vtable = fat_ptr.member("vtable", &self.symbol_table);
                 dynamic_fat_ptr(place_type, data, vtable, &self.symbol_table)
             } else {
@@ -777,14 +782,6 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 }
 
-fn is_box(ty: Ty) -> bool {
-    matches!(ty.kind(), TyKind::RigidTy(RigidTy::Adt(def, _)) if def.is_box())
-}
-
-fn is_coroutine(ty_kind: TyKind) -> bool {
-    matches!(ty_kind, TyKind::RigidTy(RigidTy::Coroutine(..)))
-}
-
 /// Extract the data pointer from a projection.
 /// The return type of the projection is not consistent today, so we need to specialize the
 /// behavior in order to get a consistent expression that represents a pointer to the projected
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index cc3b720b033d..793844733344 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -1,9 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use super::typ::pointee_type;
 use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace;
-use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type_stable, StableConverter};
+use crate::codegen_cprover_gotoc::codegen::ty_stable::{
+    is_adt, is_array, is_char, is_coroutine, is_integral, is_numeric, is_signed, is_simd,
+    pointee_type_stable, StableConverter,
+};
 use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
@@ -19,7 +21,7 @@ use cbmc::MachineModel;
 use cbmc::{btree_string_map, InternString, InternedString};
 use num::bigint::BigInt;
 use rustc_middle::mir::Rvalue as RvalueInternal;
-use rustc_middle::ty::{self, TyCtxt, VtblEntry};
+use rustc_middle::ty::{TyCtxt, VtblEntry};
 use rustc_smir::rustc_internal;
 use rustc_target::abi::{FieldsShape, TagEncoding, Variants};
 use stable_mir::mir::mono::Instance;
@@ -117,7 +119,7 @@ impl<'tcx> GotocCtx<'tcx> {
             BinOp::Rem => ce1.rem(ce2),
             BinOp::ShlUnchecked => ce1.shl(ce2),
             BinOp::ShrUnchecked => {
-                if self.operand_ty_stable(e1).is_signed() {
+                if is_signed(&self.operand_ty_stable(e1).kind()) {
                     ce1.ashr(ce2)
                 } else {
                     ce1.lshr(ce2)
@@ -136,7 +138,7 @@ impl<'tcx> GotocCtx<'tcx> {
             BinOp::Mul => ce1.mul(ce2),
             BinOp::Shl => ce1.shl(ce2),
             BinOp::Shr => {
-                if self.operand_ty_stable(e1).is_signed() {
+                if is_signed(&self.operand_ty_stable(e1).kind()) {
                     ce1.ashr(ce2)
                 } else {
                     ce1.lshr(ce2)
@@ -147,7 +149,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Codegens expressions of the type `let a  = [4u8; 6];`
-    fn codegen_rvalue_repeat(&mut self, op: &Operand, sz: Const, loc: Location) -> Expr {
+    fn codegen_rvalue_repeat(&mut self, op: &Operand, sz: &Const, loc: Location) -> Expr {
         let op_expr = self.codegen_operand_stable(op);
         let width = sz.eval_target_usize().unwrap();
         op_expr.array_constant(width).with_location(loc)
@@ -156,9 +158,9 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_rvalue_len(&mut self, p: &Place) -> Expr {
         let pt = self.place_ty_stable(p);
         match pt.kind() {
-            TyKind::RigidTy(RigidTy::Array(_, sz)) => self.codegen_const_internal(*sz, None),
+            TyKind::RigidTy(RigidTy::Array(_, sz)) => self.codegen_const(&sz, None),
             TyKind::RigidTy(RigidTy::Slice(_)) => {
-                unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(p))
+                unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(p))
                     .fat_ptr_goto_expr
                     .unwrap()
                     .member("len", &self.symbol_table)
@@ -325,7 +327,11 @@ impl<'tcx> GotocCtx<'tcx> {
                 Expr::struct_expr_from_values(
                     self.codegen_ty_stable(res_ty),
                     vec![
-                        if t1.is_signed() { ce1.ashr(ce2.clone()) } else { ce1.lshr(ce2.clone()) },
+                        if is_signed(&t1.kind()) {
+                            ce1.ashr(ce2.clone())
+                        } else {
+                            ce1.lshr(ce2.clone())
+                        },
                         ce2.cast_to(self.codegen_ty_stable(t1)).gt(max).cast_to(Type::c_bool()),
                     ],
                     &self.symbol_table,
@@ -360,7 +366,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             BinOp::Div | BinOp::Rem => {
                 let result = self.codegen_unchecked_scalar_binop(op, e1, e2);
-                if self.operand_ty_stable(e1).is_integral() {
+                if is_integral(&self.operand_ty_stable(e1).kind()) {
                     let is_rem = matches!(op, BinOp::Rem);
                     let check = self.check_div_overflow(e1, e2, is_rem, loc);
                     Expr::statement_expression(
@@ -375,7 +381,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_unchecked_scalar_binop(op, e1, e2)
             }
             BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => {
-                if self.is_fat_pointer_stable(self.operand_ty_stable(e1)) {
+                let op_ty = self.operand_ty_stable(e1);
+                if self.is_fat_pointer_stable(op_ty) {
                     self.codegen_comparison_fat_ptr(op, e1, e2, loc)
                 } else {
                     self.codegen_comparison(op, e1, e2)
@@ -389,7 +396,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // Check that computing `offset` in bytes would not overflow
                 let (offset_bytes, bytes_overflow_check) = self.count_in_bytes(
                     ce2.clone().cast_to(Type::ssize_t()),
-                    ty,
+                    rustc_internal::internal(ty),
                     Type::ssize_t(),
                     "offset",
                     loc,
@@ -439,7 +446,7 @@ impl<'tcx> GotocCtx<'tcx> {
             msg,
             loc,
         );
-        if self.operand_ty_stable(dividend).is_signed() {
+        if is_signed(&self.operand_ty_stable(dividend).kind()) {
             let dividend_expr = self.codegen_operand_stable(dividend);
             let overflow_msg = if is_remainder {
                 "attempt to calculate the remainder with overflow"
@@ -516,7 +523,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     if idx == *discriminant_field {
                         Expr::int_constant(0, self.codegen_ty(field_ty))
                     } else {
-                        self.codegen_operand_stable(&operands[idx.into()])
+                        self.codegen_operand_stable(&operands[idx])
                     }
                 })
                 .collect(),
@@ -546,14 +553,13 @@ impl<'tcx> GotocCtx<'tcx> {
         if !operands.is_empty() {
             // 2- Initialize the members of the temporary variant.
             let initial_projection =
-                ProjectedPlace::try_new_ty(temp_var.clone(), res_ty, self).unwrap();
-            let variant_proj = self
-                .codegen_variant_lvalue(initial_projection, rustc_internal::stable(variant_index));
+                ProjectedPlace::try_from_ty(temp_var.clone(), res_ty, self).unwrap();
+            let variant_proj = self.codegen_variant_lvalue(initial_projection, variant_index);
             let variant_expr = variant_proj.goto_expr.clone();
             let layout = self.layout_of_stable(res_ty);
             let fields = match &layout.variants {
                 Variants::Single { index } => {
-                    if *index != variant_index {
+                    if *index != rustc_internal::internal(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.
@@ -562,7 +568,9 @@ impl<'tcx> GotocCtx<'tcx> {
                     }
                     &layout.fields
                 }
-                Variants::Multiple { variants, .. } => &variants[variant_index].fields,
+                Variants::Multiple { variants, .. } => {
+                    &variants[rustc_internal::internal(variant_index)].fields
+                }
             };
 
             trace!(?variant_expr, ?fields, ?operands, "codegen_aggregate enum");
@@ -570,7 +578,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 variant_expr.typ().clone(),
                 fields
                     .index_by_increasing_offset()
-                    .map(|idx| self.codegen_operand_stable(&operands[idx.into()]))
+                    .map(|idx| self.codegen_operand_stable(&operands[idx]))
                     .collect(),
                 &self.symbol_table,
             );
@@ -581,7 +589,7 @@ impl<'tcx> GotocCtx<'tcx> {
         let set_discriminant = self.codegen_set_discriminant(
             rustc_internal::internal(res_ty),
             temp_var.clone(),
-            rust_target::abit::VariantIndex.from(variant_index),
+            rustc_internal::internal(variant_index),
             loc,
         );
         stmts.push(set_discriminant);
@@ -606,24 +614,24 @@ impl<'tcx> GotocCtx<'tcx> {
                 )
             }
             AggregateKind::Adt(_, _, _, _, Some(active_field_index)) => {
-                assert!(res_ty.is_union());
+                assert!(res_ty.kind().is_union());
                 assert_eq!(operands.len(), 1);
                 let typ = self.codegen_ty_stable(res_ty);
                 let components = typ.lookup_components(&self.symbol_table).unwrap();
                 Expr::union_expr(
                     typ,
-                    components[active_field_index.as_usize()].name(),
-                    self.codegen_operand_stable(&operands[0usize.into()]),
+                    components[active_field_index].name(),
+                    self.codegen_operand_stable(&operands[0usize]),
                     &self.symbol_table,
                 )
             }
-            AggregateKind::Adt(_, _, _, _, _) if res_ty.is_simd() => {
+            AggregateKind::Adt(_, _, _, _, _) if is_simd(&res_ty.kind()) => {
                 let typ = self.codegen_ty_stable(res_ty);
                 let layout = self.layout_of_stable(res_ty);
                 trace!(shape=?layout.fields, "codegen_rvalue_aggregate");
-                assert!(operands.len() > 0, "SIMD vector cannot be empty");
+                assert!(!operands.is_empty(), "SIMD vector cannot be empty");
                 if operands.len() == 1 {
-                    let data = self.codegen_operand_stable(&operands[0u32.into()]);
+                    let data = self.codegen_operand_stable(&operands[0]);
                     if data.typ().is_array() {
                         // Array-based SIMD representation.
                         data.transmute_to(typ, &self.symbol_table)
@@ -638,12 +646,12 @@ impl<'tcx> GotocCtx<'tcx> {
                         layout
                             .fields
                             .index_by_increasing_offset()
-                            .map(|idx| self.codegen_operand_stable(&operands[idx.into()]))
+                            .map(|idx| self.codegen_operand_stable(&operands[idx]))
                             .collect(),
                     )
                 }
             }
-            AggregateKind::Adt(_, variant_index, ..) if res_ty.is_enum() => {
+            AggregateKind::Adt(_, variant_index, ..) if res_ty.kind().is_enum() => {
                 self.codegen_rvalue_enum_aggregate(variant_index, operands, res_ty, loc)
             }
             AggregateKind::Adt(..) | AggregateKind::Closure(..) | AggregateKind::Tuple => {
@@ -654,7 +662,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     layout
                         .fields
                         .index_by_increasing_offset()
-                        .map(|idx| self.codegen_operand_stable(&operands[idx.into()]))
+                        .map(|idx| self.codegen_operand_stable(&operands[idx]))
                         .collect(),
                     &self.symbol_table,
                 )
@@ -663,17 +671,17 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
-    pub fn codegen_rvalue(&mut self, rv: &RvalueInternal, loc: Location) -> Expr {
-        self.codegen_rvalue_stable(&StableConverter::convert_rvalue(rv), loc)
+    pub fn codegen_rvalue(&mut self, rv: &RvalueInternal<'tcx>, loc: Location) -> Expr {
+        self.codegen_rvalue_stable(&StableConverter::convert_rvalue(self, rv.clone()), loc)
     }
 
     pub fn codegen_rvalue_stable(&mut self, rv: &Rvalue, loc: Location) -> Expr {
         let res_ty = self.rvalue_ty_stable(rv);
-        debug!(?rv, "codegen_rvalue");
+        debug!(?rv, ?res_ty, "codegen_rvalue");
         match rv {
             Rvalue::Use(p) => self.codegen_operand_stable(p),
             Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, loc),
-            Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => self.codegen_place_ref(p),
+            Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => self.codegen_place_ref_stable(&p),
             Rvalue::Len(p) => self.codegen_rvalue_len(p),
             // Rust has begun distinguishing "ptr -> num" and "num -> ptr" (providence-relevant casts) but we do not yet:
             // Should we? Tracking ticket: https://github.com/model-checking/kani/issues/1274
@@ -688,10 +696,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 | CastKind::PointerFromExposedAddress,
                 e,
                 t,
-            ) => {
-                let t = self.monomorphize(*t);
-                self.codegen_misc_cast(e, t)
-            }
+            ) => self.codegen_misc_cast(e, *t),
             Rvalue::Cast(CastKind::DynStar, _, _) => {
                 let ty = self.codegen_ty_stable(res_ty);
                 self.codegen_unimplemented_expr(
@@ -702,11 +707,10 @@ impl<'tcx> GotocCtx<'tcx> {
                 )
             }
             Rvalue::Cast(CastKind::PointerCoercion(k), e, t) => {
-                let t = self.monomorphize(*t);
-                self.codegen_pointer_cast(k, e, t, loc)
+                self.codegen_pointer_cast(k, e, *t, loc)
             }
             Rvalue::Cast(CastKind::Transmute, operand, ty) => {
-                let goto_typ = self.codegen_ty_stable(self.monomorphize(*ty));
+                let goto_typ = self.codegen_ty_stable(*ty);
                 self.codegen_operand_stable(operand).transmute_to(goto_typ, &self.symbol_table)
             }
             Rvalue::BinaryOp(op, e1, e2) => self.codegen_rvalue_binary_op(res_ty, op, e1, e2, loc),
@@ -714,14 +718,20 @@ impl<'tcx> GotocCtx<'tcx> {
                 self.codegen_rvalue_checked_binary_op(op, e1, e2, res_ty)
             }
             Rvalue::NullaryOp(k, t) => {
-                let t = self.monomorphize(*t);
-                let layout = self.layout_of_stable(t);
+                let layout = self.layout_of_stable(*t);
                 match k {
                     NullOp::SizeOf => Expr::int_constant(layout.size.bytes_usize(), Type::size_t())
-                        .with_size_of_annotation(self.codegen_ty_stable(t)),
+                        .with_size_of_annotation(self.codegen_ty_stable(*t)),
                     NullOp::AlignOf => Expr::int_constant(layout.align.abi.bytes(), Type::size_t()),
                     NullOp::OffsetOf(fields) => Expr::int_constant(
-                        layout.offset_of_subfield(self, fields.iter()).bytes(),
+                        layout
+                            .offset_of_subfield(
+                                self,
+                                fields.iter().map(|(var_idx, field_idx)| {
+                                    (rustc_internal::internal(var_idx), (*field_idx).into())
+                                }),
+                            )
+                            .bytes(),
                         Type::size_t(),
                     ),
                 }
@@ -738,7 +748,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             Rvalue::UnaryOp(op, e) => match op {
                 UnOp::Not => {
-                    if self.operand_ty_stable(e).is_bool() {
+                    if self.operand_ty_stable(e).kind().is_bool() {
                         self.codegen_operand_stable(e).not()
                     } else {
                         self.codegen_operand_stable(e).bitnot()
@@ -748,7 +758,8 @@ impl<'tcx> GotocCtx<'tcx> {
             },
             Rvalue::Discriminant(p) => {
                 let place =
-                    unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(p)).goto_expr;
+                    unwrap_or_return_codegen_unimplemented!(self, self.codegen_place_stable(p))
+                        .goto_expr;
                 let pt = self.place_ty_stable(p);
                 self.codegen_get_discriminant(place, pt, res_ty)
             }
@@ -778,7 +789,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ),
             "discriminant field (`case`) only exists for multiple variants and direct encoding"
         );
-        let expr = if ty.is_coroutine() {
+        let expr = if is_coroutine(&ty.kind()) {
             // Coroutines are translated somewhat differently from enums (see [`GotoCtx::codegen_ty_coroutine`]).
             // As a consequence, the discriminant is accessed as `.direct_fields.case` instead of just `.case`.
             place.member("direct_fields", &self.symbol_table)
@@ -825,7 +836,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     let result_type = self.codegen_ty_stable(res_ty);
                     let discr_mir_ty = self.codegen_enum_discr_typ(rustc_internal::internal(ty));
                     let discr_type = self.codegen_ty(discr_mir_ty);
-                    let niche_val = self.codegen_get_niche(e, offset.to_bytes, discr_type);
+                    let niche_val = self.codegen_get_niche(e, offset.bytes() as usize, discr_type);
                     let relative_discr =
                         wrapping_sub(&niche_val, u64::try_from(*niche_start).unwrap());
                     let relative_max =
@@ -909,45 +920,48 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// This handles all kinds of casts, except a limited subset that are instead
     /// handled by [`Self::codegen_pointer_cast`].
-    fn codegen_misc_cast(&mut self, src: &Operand, dst_t: Ty) -> Expr {
-        let src_t = self.operand_ty_stable(src);
+    fn codegen_misc_cast(&mut self, src: &Operand, dst_ty: Ty) -> Expr {
+        let src_ty = self.operand_ty_stable(src);
         debug!(
             "codegen_misc_cast: casting operand {:?} from type {:?} to type {:?}",
-            src, src_t, dst_t
+            src, src_ty, dst_ty
         );
+        let src_ty_kind = src_ty.kind();
+        let dst_ty_kind = dst_ty.kind();
 
         // number casting
-        if src_t.is_numeric() && dst_t.is_numeric() {
-            return self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_t));
+        if is_numeric(&src_ty_kind) && is_numeric(&dst_ty_kind) {
+            return self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_ty));
         }
 
         // Behind the scenes, char is just a 32bit integer
-        if (src_t.is_integral() && dst_t.is_char()) || (src_t.is_char() && dst_t.is_integral()) {
-            return self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_t));
+        if (is_integral(&src_ty_kind) && is_char(&dst_ty_kind))
+            || (is_char(&src_ty_kind) && is_integral(&dst_ty_kind))
+        {
+            return self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_ty));
         }
 
         // Cast an enum to its discriminant
-        if src_t.is_enum() && dst_t.is_integral() {
+        if src_ty_kind.is_enum() && is_integral(&dst_ty_kind) {
             let operand = self.codegen_operand_stable(src);
-            return self.codegen_get_discriminant(operand, src_t, dst_t);
+            return self.codegen_get_discriminant(operand, src_ty, dst_ty);
         }
 
         // Cast between fat pointers
-        if self.is_fat_pointer_stable(src_t) && self.is_fat_pointer_stable(dst_t) {
-            return self.codegen_fat_ptr_to_fat_ptr_cast(src, dst_t);
+        if self.is_fat_pointer_stable(src_ty) && self.is_fat_pointer_stable(dst_ty) {
+            return self.codegen_fat_ptr_to_fat_ptr_cast(src, dst_ty);
         }
 
-        if self.is_fat_pointer_stable(src_t) && !self.is_fat_pointer_stable(dst_t) {
-            return self.codegen_fat_ptr_to_thin_ptr_cast(src, dst_t);
+        if self.is_fat_pointer_stable(src_ty) && !self.is_fat_pointer_stable(dst_ty) {
+            return self.codegen_fat_ptr_to_thin_ptr_cast(src, dst_ty);
         }
 
         // pointer casting. from a pointer / reference to another pointer / reference
         // notice that if fat pointer is involved, it cannot be the destination, which is t.
-        match dst_t.kind() {
-            TyKind::RigidTy(RigidTy::Ref(_, mut dst_subt, _))
-            | TyKind::RigidTy(RigidTy::RawPtr(mut dst_subt, ..)) => {
+        match dst_ty_kind {
+            TyKind::RigidTy(RigidTy::Ref(_, dst_subt, _))
+            | TyKind::RigidTy(RigidTy::RawPtr(dst_subt, ..)) => {
                 // this is a noop in the case dst_subt is a Projection or Opaque type
-                dst_subt = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), dst_subt);
                 match dst_subt.kind() {
                     TyKind::RigidTy(RigidTy::Slice(_))
                     | TyKind::RigidTy(RigidTy::Str)
@@ -959,38 +973,35 @@ impl<'tcx> GotocCtx<'tcx> {
                         // TODO: see if it is accurate
                         self.codegen_operand_stable(src)
                     }
-                    _ => match src_t.kind() {
-                        TyKind::RigidTy(RigidTy::Ref(_, mut src_subt, _))
-                        | TyKind::RigidTy(RigidTy::RawPtr(mut src_subt, ..)) => {
+                    _ => match src_ty_kind {
+                        TyKind::RigidTy(RigidTy::Ref(_, src_subt, _))
+                        | TyKind::RigidTy(RigidTy::RawPtr(src_subt, ..)) => {
                             // this is a noop in the case dst_subt is a Projection or Opaque type
-                            src_subt = self
-                                .tcx
-                                .normalize_erasing_regions(ty::ParamEnv::reveal_all(), src_subt);
                             match src_subt.kind() {
                                 TyKind::RigidTy(RigidTy::Slice(_))
                                 | TyKind::RigidTy(RigidTy::Str)
                                 | TyKind::RigidTy(RigidTy::Dynamic(..)) => self
                                     .codegen_operand_stable(src)
                                     .member("data", &self.symbol_table)
-                                    .cast_to(self.codegen_ty_stable(dst_t)),
+                                    .cast_to(self.codegen_ty_stable(dst_ty)),
                                 _ => self
                                     .codegen_operand_stable(src)
-                                    .cast_to(self.codegen_ty_stable(dst_t)),
+                                    .cast_to(self.codegen_ty_stable(dst_ty)),
                             }
                         }
                         TyKind::RigidTy(RigidTy::Int(_))
                         | TyKind::RigidTy(RigidTy::Uint(_))
                         | TyKind::RigidTy(RigidTy::FnPtr(..)) => {
-                            self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_t))
+                            self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_ty))
                         }
                         _ => unreachable!(),
                     },
                 }
             }
             TyKind::RigidTy(RigidTy::Int(_)) | TyKind::RigidTy(RigidTy::Uint(_)) => {
-                self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_t))
+                self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_ty))
             }
-            _ => unreachable!(),
+            _ => unreachable!("Unexpected cast destination type: `{dst_ty:?}`"),
         }
     }
 
@@ -1009,10 +1020,10 @@ impl<'tcx> GotocCtx<'tcx> {
         match coercion {
             PointerCoercion::ReifyFnPointer => match self.operand_ty_stable(operand).kind() {
                 TyKind::RigidTy(RigidTy::FnDef(def, args)) => {
-                    let instance = Instance::resolve(def, &args).unwrap().unwrap();
+                    let instance = Instance::resolve(def, &args).unwrap();
                     // We need to handle this case in a special way because `codegen_operand_stable` compiles FnDefs to dummy structs.
                     // (cf. the function documentation)
-                    self.codegen_func_expr_internal(instance, None).address_of()
+                    self.codegen_func_expr(instance, None).address_of()
                 }
                 _ => unreachable!(),
             },
@@ -1022,9 +1033,8 @@ impl<'tcx> GotocCtx<'tcx> {
                     self.operand_ty_stable(operand).kind()
                 {
                     let instance = Instance::resolve_closure(def, &args, ClosureKind::FnOnce)
-                        .expect("failed to normalize and resolve closure during codegen")
-                        .polymorphize(self.tcx);
-                    self.codegen_func_expr_internal(instance, None).address_of()
+                        .expect("failed to normalize and resolve closure during codegen");
+                    self.codegen_func_expr(instance, None).address_of()
                 } else {
                     unreachable!("{:?} cannot be cast to a fn ptr", operand)
                 }
@@ -1133,14 +1143,14 @@ impl<'tcx> GotocCtx<'tcx> {
         info: CoerceUnsizedInfo,
         member_coercion: Expr,
     ) -> Expr {
-        assert!(info.src_ty.is_adt(), "Expected struct. Found {:?}", info.src_ty);
-        assert!(info.dst_ty.is_adt(), "Expected struct. Found {:?}", info.dst_ty);
+        assert!(is_adt(&info.src_ty.kind()), "Expected struct. Found {:?}", info.src_ty);
+        assert!(is_adt(&info.dst_ty.kind()), "Expected struct. Found {:?}", info.dst_ty);
         let dst_goto_type = self.codegen_ty_stable(info.dst_ty);
         let src_field_exprs = src_expr.struct_field_exprs(&self.symbol_table);
         let dst_field_exprs = src_field_exprs
             .into_iter()
             .map(|(key, val)| {
-                let new_val = if info.field.unwrap().as_str().intern() == key {
+                let new_val = if info.field.as_ref().unwrap().as_str().intern() == key {
                     // The type being coerced. Use the provided expression.
                     member_coercion.clone()
                 } else {
@@ -1165,10 +1175,10 @@ impl<'tcx> GotocCtx<'tcx> {
         dst_expr
     }
 
-    fn codegen_vtable_method_field(&mut self, instance: Instance, t: Ty, idx: usize) -> Expr {
-        debug!(?instance, typ=?t, %idx, "codegen_vtable_method_field");
+    fn codegen_vtable_method_field(&mut self, instance: Instance, ty: Ty, idx: usize) -> Expr {
+        debug!(?instance, typ=?ty, %idx, "codegen_vtable_method_field");
         let vtable_field_name = self.vtable_field_name(idx);
-        let vtable_type = Type::struct_tag(self.vtable_name_stable(t));
+        let vtable_type = Type::struct_tag(self.vtable_name_stable(ty));
         let field_type =
             vtable_type.lookup_field_type(vtable_field_name, &self.symbol_table).unwrap();
         debug!(?vtable_field_name, ?vtable_type, "codegen_vtable_method_field");
@@ -1180,7 +1190,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(t).into(),
+                    self.normalized_trait_name(rustc_internal::internal(ty)).into(),
                     idx,
                     fn_name.into(),
                 );
@@ -1204,7 +1214,8 @@ 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::Ty) -> Expr {
+    fn codegen_vtable_drop_in_place(&mut self, ty: Ty, trait_ty: Ty) -> Expr {
+        let trait_ty = rustc_internal::internal(trait_ty);
         let drop_instance = Instance::resolve_drop_in_place(ty);
         let drop_sym_name: InternedString = drop_instance.mangled_name().into();
 
@@ -1230,10 +1241,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 .address_of()
                 .cast_to(trait_fn_ty)
         } else {
-            unreachable!(
-                "Missing drop implementation for {}",
-                self.readable_instance_name(drop_instance)
-            );
+            unreachable!("Missing drop implementation for {}", drop_instance.name())
         }
     }
 
@@ -1291,16 +1299,12 @@ impl<'tcx> GotocCtx<'tcx> {
             TyKind::RigidTy(RigidTy::Ref(_, pointee_type, ..)) => pointee_type,
             // DST is box type
             TyKind::RigidTy(RigidTy::Adt(adt_def, adt_subst)) if adt_def.is_box() => {
-                adt_subst.0.first().unwrap().expect_ty()
+                *adt_subst.0.first().unwrap().expect_ty()
             }
             // DST is dynamic type
             TyKind::RigidTy(RigidTy::Dynamic(..)) => dst_mir_type,
             _ => unreachable!("Cannot codegen_vtable for type {:?}", dst_mir_type.kind()),
         };
-        let binders = match trait_type.kind() {
-            TyKind::RigidTy(RigidTy::Dynamic(binders, ..)) => binders,
-            _ => unreachable!("Cannot codegen_vtable for type {:?}", dst_mir_type.kind()),
-        };
 
         let src_name = self.ty_mangled_name(rustc_internal::internal(src_mir_type));
         // The name needs to be the same as inserted in typ.rs
@@ -1314,11 +1318,9 @@ impl<'tcx> GotocCtx<'tcx> {
             Location::none(),
             |ctx, var| {
                 // Build the vtable, using Rust's vtable_entries to determine field order
-                let vtable_entries = if let Some(principal) = binders.principal() {
-                    let trait_ref_binder = principal.with_self_ty(ctx.tcx, src_mir_type);
-                    let trait_ref_binder = ctx.tcx.erase_regions(trait_ref_binder);
-
-                    ctx.tcx.vtable_entries(trait_ref_binder)
+                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))
                 } else {
                     TyCtxt::COMMON_VTABLE_ENTRIES
                 };
@@ -1339,9 +1341,11 @@ impl<'tcx> GotocCtx<'tcx> {
                         // TODO: trait upcasting
                         // https://github.com/model-checking/kani/issues/358
                         VtblEntry::TraitVPtr(_trait_ref) => None,
-                        VtblEntry::Method(instance) => {
-                            Some(ctx.codegen_vtable_method_field(*instance, trait_type, idx))
-                        }
+                        VtblEntry::Method(instance) => Some(ctx.codegen_vtable_method_field(
+                            rustc_internal::stable(instance),
+                            trait_type,
+                            idx,
+                        )),
                     })
                     .collect();
 
@@ -1390,7 +1394,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 assert_eq!(src_elt_type, dst_elt_type);
                 let dst_goto_len = self.codegen_const(&src_elt_count, None);
                 let src_pointee_ty = pointee_type_stable(coerce_info.src_ty).unwrap();
-                let dst_data_expr = if src_pointee_ty.is_array() {
+                let dst_data_expr = if is_array(&src_pointee_ty.kind()) {
                     src_goto_expr.cast_to(self.codegen_ty_stable(src_elt_type).to_pointer())
                 } else {
                     // A struct that contains the type being coerced to a slice.
@@ -1476,6 +1480,6 @@ fn get_strict_operator(op: &BinOp) -> BinOp {
     match op {
         BinOp::Le => BinOp::Lt,
         BinOp::Ge => BinOp::Gt,
-        _ => *op,
+        _ => op.clone(),
     }
 }
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 df6d6e79da05..bee7b1bd2e10 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
@@ -11,14 +11,17 @@ use cbmc::goto_program::Type;
 use rustc_middle::mir;
 use rustc_middle::mir::visit::{MutVisitor, NonUseContext, PlaceContext};
 use rustc_middle::mir::{
-    Operand as OperandInternal, Place as PlaceInternal, Rvalue as RvalueInternal,
+    Location, Operand as OperandInternal, Place as PlaceInternal, Rvalue as RvalueInternal,
 };
-use rustc_middle::ty::{self, Const as ConstInternal, Ty as TyInternal, TyCtxt};
+use rustc_middle::ty::layout::{LayoutOf, TyAndLayout};
+use rustc_middle::ty::{self, Const as ConstInternal, GenericArgsRef, Ty as TyInternal, TyCtxt};
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Local, Operand, Place, Rvalue};
 use stable_mir::ty::{Const, RigidTy, Ty, TyKind};
 
+pub use self::ty_utils::*;
+
 impl<'tcx> GotocCtx<'tcx> {
     pub fn place_ty_stable(&self, place: &Place) -> Ty {
         place.ty(self.current_fn().body().locals()).unwrap()
@@ -28,6 +31,10 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_ty(rustc_internal::internal(ty))
     }
 
+    pub fn codegen_ty_ref_stable(&mut self, ty: Ty) -> Type {
+        self.codegen_ty_ref(rustc_internal::internal(ty))
+    }
+
     pub fn local_ty_stable(&mut self, local: Local) -> Ty {
         self.current_fn().body().local_decl(local).unwrap().ty
     }
@@ -40,6 +47,10 @@ impl<'tcx> GotocCtx<'tcx> {
         self.is_zst(rustc_internal::internal(ty))
     }
 
+    pub fn layout_of_stable(&self, ty: Ty) -> TyAndLayout<'tcx> {
+        self.layout_of(rustc_internal::internal(ty))
+    }
+
     pub fn codegen_fndef_type_stable(&mut self, instance: Instance) -> Type {
         let func = self.symbol_name_stable(instance);
         self.ensure_struct(
@@ -57,6 +68,10 @@ impl<'tcx> GotocCtx<'tcx> {
         self.use_fat_pointer(rustc_internal::internal(pointer_ty))
     }
 
+    pub fn use_thin_pointer_stable(&self, pointer_ty: Ty) -> bool {
+        self.use_thin_pointer(rustc_internal::internal(pointer_ty))
+    }
+
     pub fn is_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
         self.is_fat_pointer(rustc_internal::internal(pointer_ty))
     }
@@ -65,6 +80,10 @@ impl<'tcx> GotocCtx<'tcx> {
         self.is_vtable_fat_pointer(rustc_internal::internal(pointer_ty))
     }
 
+    pub fn use_vtable_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
+        self.use_vtable_fat_pointer(rustc_internal::internal(pointer_ty))
+    }
+
     pub fn vtable_name_stable(&self, ty: Ty) -> String {
         self.vtable_name(rustc_internal::internal(ty))
     }
@@ -125,8 +144,8 @@ impl<'a, 'tcx> StableConverter<'a, 'tcx> {
 
 pub fn pointee_type_stable(ty: Ty) -> Option<Ty> {
     match ty.kind() {
-        TyKind::RigidTy(RigidTy::Ref(_, pointee_type, _))
-        | TyKind::RigidTy(RigidTy::RawPtr(ty, ..)) => Some(pointee_type),
+        TyKind::RigidTy(RigidTy::Ref(_, pointee_ty, _))
+        | TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, ..)) => Some(pointee_ty),
         _ => None,
     }
 }
@@ -144,6 +163,10 @@ impl<'a, 'tcx> MutVisitor<'tcx> for StableConverter<'a, 'tcx> {
         *ct = self.gcx.monomorphize(*ct);
     }
 
+    fn visit_args(&mut self, args: &mut GenericArgsRef<'tcx>, _: Location) {
+        *args = self.gcx.monomorphize(*args);
+    }
+
     fn visit_constant(&mut self, constant: &mut mir::ConstOperand<'tcx>, location: mir::Location) {
         let const_ = self.gcx.monomorphize(constant.const_);
         let val = match const_.eval(self.gcx.tcx, ty::ParamEnv::reveal_all(), None) {
@@ -158,3 +181,49 @@ impl<'a, 'tcx> MutVisitor<'tcx> for StableConverter<'a, 'tcx> {
         self.super_constant(constant, location);
     }
 }
+
+/// Utility methods for types that we expect to be incorporated into StableMIR.
+pub mod ty_utils {
+    use rustc_smir::rustc_internal;
+    use stable_mir::ty::{RigidTy, TyKind};
+
+    pub fn is_signed(kind: &TyKind) -> bool {
+        matches!(kind, TyKind::RigidTy(RigidTy::Int(..)))
+    }
+
+    pub fn is_integral(kind: &TyKind) -> bool {
+        matches!(kind, TyKind::RigidTy(RigidTy::Int(..) | RigidTy::Uint(..)))
+    }
+
+    pub fn is_array(kind: &TyKind) -> bool {
+        matches!(kind, TyKind::RigidTy(RigidTy::Array(..)))
+    }
+
+    pub fn is_adt(kind: &TyKind) -> bool {
+        matches!(kind, TyKind::RigidTy(RigidTy::Adt(..)))
+    }
+
+    pub fn is_char(kind: &TyKind) -> bool {
+        matches!(kind, TyKind::RigidTy(RigidTy::Char))
+    }
+
+    pub fn is_float(kind: &TyKind) -> bool {
+        matches!(kind, TyKind::RigidTy(RigidTy::Float(..)))
+    }
+
+    pub fn is_numeric(kind: &TyKind) -> bool {
+        is_integral(kind) || is_float(kind)
+    }
+
+    pub fn is_coroutine(kind: &TyKind) -> bool {
+        matches!(kind, TyKind::RigidTy(RigidTy::Coroutine(..)))
+    }
+
+    pub fn is_simd(kind: &TyKind) -> bool {
+        matches!(kind, TyKind::RigidTy(RigidTy::Adt(def, ..)) if rustc_internal::internal(def).repr().simd() )
+    }
+
+    pub fn is_box(kind: &TyKind) -> bool {
+        matches!(kind, TyKind::RigidTy(RigidTy::Adt(def, _)) if def.is_box())
+    }
+}
diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs
index 92e59603ae84..85d59215d661 100644
--- a/kani-compiler/src/kani_middle/coercion.rs
+++ b/kani-compiler/src/kani_middle/coercion.rs
@@ -16,7 +16,7 @@
 use rustc_hir::lang_items::LangItem;
 use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
-use rustc_middle::ty::{self, ParamEnv, Ty, TyCtxt};
+use rustc_middle::ty::{ParamEnv, Ty, TyCtxt};
 use rustc_middle::ty::{TraitRef, TypeAndMut};
 use rustc_smir::rustc_internal;
 use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
@@ -202,10 +202,10 @@ impl<'tcx> Iterator for CoerceUnsizedIterator<'tcx> {
         // the conversion.
         let src_ty = self.src_ty.take().unwrap();
         let dst_ty = self.dst_ty.take().unwrap();
-        let field = match (&src_ty.kind(), &dst_ty.kind()) {
+        let field = match (src_ty.kind(), dst_ty.kind()) {
             (
-                &TyKind::RigidTy(RigidTy::Adt(src_def, src_args)),
-                &TyKind::RigidTy(RigidTy::Adt(dst_def, dst_args)),
+                TyKind::RigidTy(RigidTy::Adt(src_def, ref src_args)),
+                TyKind::RigidTy(RigidTy::Adt(dst_def, ref dst_args)),
             ) => {
                 // Handle smart pointers by using CustomCoerceUnsized to find the field being
                 // coerced.
@@ -262,6 +262,6 @@ fn custom_coerce_unsize_info<'tcx>(
 }
 
 /// Extract pointee type from builtin pointer types.
-fn extract_pointee(typ: TyStable) -> Option<Ty> {
+fn extract_pointee<'tcx>(typ: TyStable) -> Option<Ty<'tcx>> {
     rustc_internal::internal(typ).builtin_deref(true).map(|TypeAndMut { ty, .. }| ty)
 }

From 10af130c8aa7dc67c5ac7c009ecea039659cb639 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Mon, 11 Dec 2023 16:32:43 -0800
Subject: [PATCH 3/5] Update tests after toolchain change

---
 tests/expected/panic/panic-2018/expected | 2 +-
 tests/expected/panic/panic-2021/expected | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/expected/panic/panic-2018/expected b/tests/expected/panic/panic-2018/expected
index 72637a772604..92a9e47ad8ce 100644
--- a/tests/expected/panic/panic-2018/expected
+++ b/tests/expected/panic/panic-2018/expected
@@ -1,4 +1,4 @@
-Failed Checks: concat! ("Panic: {} code: ", 10), msg
+Failed Checks: concat!("Panic: {} code: ", 10), msg
 Failed Checks: msg
 Failed Checks: explicit panic
 Failed Checks: Panic message
diff --git a/tests/expected/panic/panic-2021/expected b/tests/expected/panic/panic-2021/expected
index 72637a772604..92a9e47ad8ce 100644
--- a/tests/expected/panic/panic-2021/expected
+++ b/tests/expected/panic/panic-2021/expected
@@ -1,4 +1,4 @@
-Failed Checks: concat! ("Panic: {} code: ", 10), msg
+Failed Checks: concat!("Panic: {} code: ", 10), msg
 Failed Checks: msg
 Failed Checks: explicit panic
 Failed Checks: Panic message

From 9969ec1822f8c2eac594c90efae84ba699bcee2b Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 12 Dec 2023 11:10:58 -0800
Subject: [PATCH 4/5] Replace TyKind utility methods with StableMIR ones

---
 .../codegen_cprover_gotoc/codegen/place.rs    |  8 ++--
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 33 ++++++-------
 .../codegen/ty_stable.rs                      | 48 -------------------
 3 files changed, 18 insertions(+), 71 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index bac62a19d25e..75f184660765 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -6,9 +6,7 @@
 //! in [GotocCtx::codegen_place] below.
 
 use super::typ::TypeExt;
-use crate::codegen_cprover_gotoc::codegen::ty_stable::{
-    is_box, is_coroutine, pointee_type, StableConverter,
-};
+use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type, StableConverter};
 use crate::codegen_cprover_gotoc::codegen::typ::std_pointee_type;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::GotocCtx;
@@ -411,7 +409,7 @@ impl<'tcx> GotocCtx<'tcx> {
         match proj {
             ProjectionElem::Deref => {
                 let base_type = before.mir_typ();
-                let inner_goto_expr = if is_box(&base_type.kind()) {
+                let inner_goto_expr = if base_type.kind().is_box() {
                     self.deref_box(before.goto_expr)
                 } else {
                     before.goto_expr
@@ -601,7 +599,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     Variants::Single { .. } => before.goto_expr,
                     Variants::Multiple { tag_encoding, .. } => match tag_encoding {
                         TagEncoding::Direct => {
-                            let cases = if is_coroutine(&ty_kind) {
+                            let cases = if ty_kind.is_coroutine() {
                                 before.goto_expr
                             } else {
                                 before.goto_expr.member("cases", &self.symbol_table)
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 793844733344..30ebf514edd5 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -2,10 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace;
-use crate::codegen_cprover_gotoc::codegen::ty_stable::{
-    is_adt, is_array, is_char, is_coroutine, is_integral, is_numeric, is_signed, is_simd,
-    pointee_type_stable, StableConverter,
-};
+use crate::codegen_cprover_gotoc::codegen::ty_stable::{pointee_type_stable, StableConverter};
 use crate::codegen_cprover_gotoc::codegen::PropertyClass;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
@@ -119,7 +116,7 @@ impl<'tcx> GotocCtx<'tcx> {
             BinOp::Rem => ce1.rem(ce2),
             BinOp::ShlUnchecked => ce1.shl(ce2),
             BinOp::ShrUnchecked => {
-                if is_signed(&self.operand_ty_stable(e1).kind()) {
+                if self.operand_ty_stable(e1).kind().is_signed() {
                     ce1.ashr(ce2)
                 } else {
                     ce1.lshr(ce2)
@@ -138,7 +135,7 @@ impl<'tcx> GotocCtx<'tcx> {
             BinOp::Mul => ce1.mul(ce2),
             BinOp::Shl => ce1.shl(ce2),
             BinOp::Shr => {
-                if is_signed(&self.operand_ty_stable(e1).kind()) {
+                if self.operand_ty_stable(e1).kind().is_signed() {
                     ce1.ashr(ce2)
                 } else {
                     ce1.lshr(ce2)
@@ -327,7 +324,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 Expr::struct_expr_from_values(
                     self.codegen_ty_stable(res_ty),
                     vec![
-                        if is_signed(&t1.kind()) {
+                        if t1.kind().is_signed() {
                             ce1.ashr(ce2.clone())
                         } else {
                             ce1.lshr(ce2.clone())
@@ -366,7 +363,7 @@ impl<'tcx> GotocCtx<'tcx> {
             }
             BinOp::Div | BinOp::Rem => {
                 let result = self.codegen_unchecked_scalar_binop(op, e1, e2);
-                if is_integral(&self.operand_ty_stable(e1).kind()) {
+                if self.operand_ty_stable(e1).kind().is_integral() {
                     let is_rem = matches!(op, BinOp::Rem);
                     let check = self.check_div_overflow(e1, e2, is_rem, loc);
                     Expr::statement_expression(
@@ -446,7 +443,7 @@ impl<'tcx> GotocCtx<'tcx> {
             msg,
             loc,
         );
-        if is_signed(&self.operand_ty_stable(dividend).kind()) {
+        if self.operand_ty_stable(dividend).kind().is_signed() {
             let dividend_expr = self.codegen_operand_stable(dividend);
             let overflow_msg = if is_remainder {
                 "attempt to calculate the remainder with overflow"
@@ -625,7 +622,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     &self.symbol_table,
                 )
             }
-            AggregateKind::Adt(_, _, _, _, _) if is_simd(&res_ty.kind()) => {
+            AggregateKind::Adt(_, _, _, _, _) if res_ty.kind().is_simd() => {
                 let typ = self.codegen_ty_stable(res_ty);
                 let layout = self.layout_of_stable(res_ty);
                 trace!(shape=?layout.fields, "codegen_rvalue_aggregate");
@@ -789,7 +786,7 @@ impl<'tcx> GotocCtx<'tcx> {
             ),
             "discriminant field (`case`) only exists for multiple variants and direct encoding"
         );
-        let expr = if is_coroutine(&ty.kind()) {
+        let expr = if ty.kind().is_coroutine() {
             // Coroutines are translated somewhat differently from enums (see [`GotoCtx::codegen_ty_coroutine`]).
             // As a consequence, the discriminant is accessed as `.direct_fields.case` instead of just `.case`.
             place.member("direct_fields", &self.symbol_table)
@@ -930,19 +927,19 @@ impl<'tcx> GotocCtx<'tcx> {
         let dst_ty_kind = dst_ty.kind();
 
         // number casting
-        if is_numeric(&src_ty_kind) && is_numeric(&dst_ty_kind) {
+        if src_ty_kind.is_numeric() && dst_ty_kind.is_numeric() {
             return self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_ty));
         }
 
         // Behind the scenes, char is just a 32bit integer
-        if (is_integral(&src_ty_kind) && is_char(&dst_ty_kind))
-            || (is_char(&src_ty_kind) && is_integral(&dst_ty_kind))
+        if (src_ty_kind.is_integral() && dst_ty_kind.is_char())
+            || (src_ty_kind.is_char() && dst_ty_kind.is_integral())
         {
             return self.codegen_operand_stable(src).cast_to(self.codegen_ty_stable(dst_ty));
         }
 
         // Cast an enum to its discriminant
-        if src_ty_kind.is_enum() && is_integral(&dst_ty_kind) {
+        if src_ty_kind.is_enum() && dst_ty_kind.is_integral() {
             let operand = self.codegen_operand_stable(src);
             return self.codegen_get_discriminant(operand, src_ty, dst_ty);
         }
@@ -1143,8 +1140,8 @@ impl<'tcx> GotocCtx<'tcx> {
         info: CoerceUnsizedInfo,
         member_coercion: Expr,
     ) -> Expr {
-        assert!(is_adt(&info.src_ty.kind()), "Expected struct. Found {:?}", info.src_ty);
-        assert!(is_adt(&info.dst_ty.kind()), "Expected struct. Found {:?}", info.dst_ty);
+        assert!(info.src_ty.kind().is_adt(), "Expected struct. Found {:?}", info.src_ty);
+        assert!(info.dst_ty.kind().is_adt(), "Expected struct. Found {:?}", info.dst_ty);
         let dst_goto_type = self.codegen_ty_stable(info.dst_ty);
         let src_field_exprs = src_expr.struct_field_exprs(&self.symbol_table);
         let dst_field_exprs = src_field_exprs
@@ -1394,7 +1391,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 assert_eq!(src_elt_type, dst_elt_type);
                 let dst_goto_len = self.codegen_const(&src_elt_count, None);
                 let src_pointee_ty = pointee_type_stable(coerce_info.src_ty).unwrap();
-                let dst_data_expr = if is_array(&src_pointee_ty.kind()) {
+                let dst_data_expr = if src_pointee_ty.kind().is_array() {
                     src_goto_expr.cast_to(self.codegen_ty_stable(src_elt_type).to_pointer())
                 } else {
                     // A struct that contains the type being coerced to a slice.
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 bee7b1bd2e10..d214463f0759 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
@@ -20,8 +20,6 @@ use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{Local, Operand, Place, Rvalue};
 use stable_mir::ty::{Const, RigidTy, Ty, TyKind};
 
-pub use self::ty_utils::*;
-
 impl<'tcx> GotocCtx<'tcx> {
     pub fn place_ty_stable(&self, place: &Place) -> Ty {
         place.ty(self.current_fn().body().locals()).unwrap()
@@ -181,49 +179,3 @@ impl<'a, 'tcx> MutVisitor<'tcx> for StableConverter<'a, 'tcx> {
         self.super_constant(constant, location);
     }
 }
-
-/// Utility methods for types that we expect to be incorporated into StableMIR.
-pub mod ty_utils {
-    use rustc_smir::rustc_internal;
-    use stable_mir::ty::{RigidTy, TyKind};
-
-    pub fn is_signed(kind: &TyKind) -> bool {
-        matches!(kind, TyKind::RigidTy(RigidTy::Int(..)))
-    }
-
-    pub fn is_integral(kind: &TyKind) -> bool {
-        matches!(kind, TyKind::RigidTy(RigidTy::Int(..) | RigidTy::Uint(..)))
-    }
-
-    pub fn is_array(kind: &TyKind) -> bool {
-        matches!(kind, TyKind::RigidTy(RigidTy::Array(..)))
-    }
-
-    pub fn is_adt(kind: &TyKind) -> bool {
-        matches!(kind, TyKind::RigidTy(RigidTy::Adt(..)))
-    }
-
-    pub fn is_char(kind: &TyKind) -> bool {
-        matches!(kind, TyKind::RigidTy(RigidTy::Char))
-    }
-
-    pub fn is_float(kind: &TyKind) -> bool {
-        matches!(kind, TyKind::RigidTy(RigidTy::Float(..)))
-    }
-
-    pub fn is_numeric(kind: &TyKind) -> bool {
-        is_integral(kind) || is_float(kind)
-    }
-
-    pub fn is_coroutine(kind: &TyKind) -> bool {
-        matches!(kind, TyKind::RigidTy(RigidTy::Coroutine(..)))
-    }
-
-    pub fn is_simd(kind: &TyKind) -> bool {
-        matches!(kind, TyKind::RigidTy(RigidTy::Adt(def, ..)) if rustc_internal::internal(def).repr().simd() )
-    }
-
-    pub fn is_box(kind: &TyKind) -> bool {
-        matches!(kind, TyKind::RigidTy(RigidTy::Adt(def, _)) if def.is_box())
-    }
-}

From ac8dec3858384929c0f985bb3657d2be5d004bf4 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Tue, 12 Dec 2023 18:32:56 -0800
Subject: [PATCH 5/5] Bump nightly version and address comments

---
 kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 4 +++-
 rust-toolchain.toml                                       | 2 +-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 30ebf514edd5..af6fa32acba6 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -867,6 +867,8 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Extract the niche value from `v`. This value should be of type `niche_ty` and located
     /// at byte offset `offset`
+    ///
+    /// The `offset` in bytes of the niche value.
     pub fn codegen_get_niche(&self, v: Expr, offset: Size, niche_ty: Type) -> Expr {
         if offset == 0 {
             v.reinterpret_cast(niche_ty)
@@ -1477,6 +1479,6 @@ fn get_strict_operator(op: &BinOp) -> BinOp {
     match op {
         BinOp::Le => BinOp::Lt,
         BinOp::Ge => BinOp::Gt,
-        _ => op.clone(),
+        _ => *op,
     }
 }
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index c674a2730710..34e9eda66018 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-12-11"
+channel = "nightly-2023-12-13"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]