diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
index 2658b75812a7..68573cd2a1cd 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs
@@ -21,7 +21,6 @@
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
 use cbmc::InternedString;
-use rustc_span::Span;
 use stable_mir::ty::Span as SpanStable;
 use std::convert::AsRef;
 use strum_macros::{AsRefStr, EnumString};
@@ -149,8 +148,8 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// Generate a cover statement for code coverage reports.
-    pub fn codegen_coverage(&self, span: Span) -> Stmt {
-        let loc = self.codegen_caller_span(&span);
+    pub fn codegen_coverage(&self, span: SpanStable) -> Stmt {
+        let loc = self.codegen_caller_span_stable(span);
         // Should use Stmt::cover, but currently this doesn't work with CBMC
         // unless it is run with '--cover cover' (see
         // https://github.com/diffblue/cbmc/issues/6613). So for now use
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
index 11cdf47f4ed2..692fdb9c385b 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/block.rs
@@ -2,8 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::codegen_cprover_gotoc::GotocCtx;
-use rustc_middle::mir::{BasicBlock, BasicBlockData};
-use stable_mir::mir::BasicBlockIdx;
+use stable_mir::mir::{BasicBlock, BasicBlockIdx};
 use tracing::debug;
 
 pub fn bb_label(bb: BasicBlockIdx) -> String {
@@ -17,20 +16,20 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// This function does not return a value, but mutates state with
     /// `self.current_fn_mut().push_onto_block(...)`
-    pub fn codegen_block(&mut self, bb: BasicBlock, bbd: &BasicBlockData<'tcx>) {
-        debug!(?bb, "Codegen basicblock");
-        let label: String = self.current_fn().find_label(&bb);
+    pub fn codegen_block(&mut self, bb: BasicBlockIdx, bbd: &BasicBlock) {
+        debug!(?bb, "codegen_block");
+        let label = bb_label(bb);
         let check_coverage = self.queries.args().check_coverage;
         // the first statement should be labelled. if there is no statements, then the
         // terminator should be labelled.
         match bbd.statements.len() {
             0 => {
-                let term = bbd.terminator();
+                let term = &bbd.terminator;
                 let tcode = self.codegen_terminator(term);
                 // When checking coverage, the `coverage` check should be
                 // labelled instead.
                 if check_coverage {
-                    let span = term.source_info.span;
+                    let span = term.span;
                     let cover = self.codegen_coverage(span);
                     self.current_fn_mut().push_onto_block(cover.with_label(label));
                     self.current_fn_mut().push_onto_block(tcode);
@@ -44,7 +43,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // When checking coverage, the `coverage` check should be
                 // labelled instead.
                 if check_coverage {
-                    let span = stmt.source_info.span;
+                    let span = stmt.span;
                     let cover = self.codegen_coverage(span);
                     self.current_fn_mut().push_onto_block(cover.with_label(label));
                     self.current_fn_mut().push_onto_block(scode);
@@ -54,16 +53,16 @@ impl<'tcx> GotocCtx<'tcx> {
 
                 for s in &bbd.statements[1..] {
                     if check_coverage {
-                        let span = s.source_info.span;
+                        let span = s.span;
                         let cover = self.codegen_coverage(span);
                         self.current_fn_mut().push_onto_block(cover);
                     }
                     let stmt = self.codegen_statement(s);
                     self.current_fn_mut().push_onto_block(stmt);
                 }
-                let term = bbd.terminator();
+                let term = &bbd.terminator;
                 if check_coverage {
-                    let span = term.source_info.span;
+                    let span = term.span;
                     let cover = self.codegen_coverage(span);
                     self.current_fn_mut().push_onto_block(cover);
                 }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
index 617eeb8af506..22546be18909 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs
@@ -137,7 +137,7 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// This will behave like `codegen_unimplemented_stmt` but print a message that includes
     /// the name of the function not supported and the calling convention.
-    pub fn codegen_ffi_unsupported(&mut self, instance: Instance<'tcx>, loc: Location) -> Stmt {
+    fn codegen_ffi_unsupported(&mut self, instance: Instance<'tcx>, loc: Location) -> Stmt {
         let fn_name = &self.symbol_name(instance);
         debug!(?fn_name, ?loc, "codegen_ffi_unsupported");
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
index f3d79c7f06c5..52bf778ab235 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs
@@ -7,96 +7,85 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::{Expr, Stmt, Symbol};
 use cbmc::InternString;
 use rustc_middle::mir::traversal::reverse_postorder;
-use rustc_middle::mir::{Body, HasLocalDecls, Local};
-use rustc_middle::ty::{self, Instance};
+use stable_mir::mir::mono::Instance;
+use stable_mir::mir::{Body, Local};
+use stable_mir::ty::{RigidTy, TyKind};
+use stable_mir::CrateDef;
 use std::collections::BTreeMap;
 use std::iter::FromIterator;
 use tracing::{debug, debug_span};
 
 /// Codegen MIR functions into gotoc
 impl<'tcx> GotocCtx<'tcx> {
-    /// Get the number of parameters that the current function expects.
-    fn get_params_size(&self) -> usize {
-        let sig = self.current_fn().sig();
-        let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig);
-        // we don't call [codegen_function_sig] because we want to get a bit more metainformation.
-        sig.inputs().len()
-    }
-
     /// Declare variables according to their index.
     /// - Index 0 represents the return value.
     /// - Indices [1, N] represent the function parameters where N is the number of parameters.
     /// - Indices that are greater than N represent local variables.
-    fn codegen_declare_variables(&mut self) {
-        let mir = self.current_fn().body_internal();
-        let ldecls = mir.local_decls();
-        let num_args = self.get_params_size();
-        ldecls.indices().enumerate().for_each(|(idx, lc)| {
-            if Some(lc) == mir.spread_arg {
+    fn codegen_declare_variables(&mut self, body: &Body) {
+        let ldecls = body.local_decls();
+        let num_args = body.arg_locals().len();
+        for (lc, ldata) in ldecls {
+            if Some(lc) == body.spread_arg() {
                 // We have already added this local in the function prelude, so
                 // skip adding it again here.
-                return;
+                continue;
             }
             let base_name = self.codegen_var_base_name(&lc);
             let name = self.codegen_var_name(&lc);
-            let ldata = &ldecls[lc];
-            let var_ty = self.monomorphize(ldata.ty);
-            let var_type = self.codegen_ty(var_ty);
-            let loc = self.codegen_span(&ldata.source_info.span);
+            let var_type = self.codegen_ty_stable(ldata.ty);
+            let loc = self.codegen_span_stable(ldata.span);
             // Indices [1, N] represent the function parameters where N is the number of parameters.
             // Except that ZST fields are not included as parameters.
-            let sym = Symbol::variable(
-                name,
-                base_name,
-                var_type,
-                self.codegen_span(&ldata.source_info.span),
-            )
-            .with_is_hidden(!self.is_user_variable(&lc))
-            .with_is_parameter((idx > 0 && idx <= num_args) && !self.is_zst(var_ty));
+            let sym =
+                Symbol::variable(name, base_name, var_type, self.codegen_span_stable(ldata.span))
+                    .with_is_hidden(!self.is_user_variable(&lc))
+                    .with_is_parameter((lc > 0 && lc <= num_args) && !self.is_zst_stable(ldata.ty));
             let sym_e = sym.to_expr();
             self.symbol_table.insert(sym);
 
             // Index 0 represents the return value, which does not need to be
             // declared in the first block
-            if lc.index() < 1 || lc.index() > mir.arg_count {
+            if lc < 1 || lc > body.arg_locals().len() {
                 let init = self.codegen_default_initializer(&sym_e);
                 self.current_fn_mut().push_onto_block(Stmt::decl(sym_e, init, loc));
             }
-        });
+        }
     }
 
-    pub fn codegen_function(&mut self, instance: Instance<'tcx>) {
-        self.set_current_fn(instance);
-        let name = self.current_fn().name();
+    pub fn codegen_function(&mut self, instance: Instance) {
+        let name = self.symbol_name_stable(instance);
         let old_sym = self.symbol_table.lookup(&name).unwrap();
 
-        let _trace_span =
-            debug_span!("CodegenFunction", name = self.current_fn().readable_name()).entered();
+        let _trace_span = debug_span!("CodegenFunction", name = instance.name()).entered();
         if old_sym.is_function_definition() {
             debug!("Double codegen of {:?}", old_sym);
         } else {
             assert!(old_sym.is_function());
-            let mir = self.current_fn().body_internal();
-            self.print_instance(instance, mir);
-            self.codegen_function_prelude();
-            self.codegen_declare_variables();
-
-            reverse_postorder(mir).for_each(|(bb, bbd)| self.codegen_block(bb, bbd));
-
-            let loc = self.codegen_span(&mir.span);
+            let body = instance.body().unwrap();
+            self.set_current_fn(instance, &body);
+            self.print_instance(instance, &body);
+            self.codegen_function_prelude(&body);
+            self.codegen_declare_variables(&body);
+
+            // Get the order from internal body for now.
+            let internal_body = self.current_fn().body_internal();
+            reverse_postorder(internal_body)
+                .for_each(|(bb, _)| self.codegen_block(bb.index(), &body.blocks[bb.index()]));
+
+            let loc = self.codegen_span_stable(instance.def.span());
             let stmts = self.current_fn_mut().extract_block();
-            let body = Stmt::block(stmts, loc);
-            self.symbol_table.update_fn_declaration_with_definition(&name, body);
+            let goto_body = Stmt::block(stmts, loc);
+            self.symbol_table.update_fn_declaration_with_definition(&name, goto_body);
+            self.reset_current_fn();
         }
-        self.reset_current_fn();
     }
 
     /// Codegen changes required due to the function ABI.
     /// We currently untuple arguments for RustCall ABI where the `spread_arg` is set.
-    fn codegen_function_prelude(&mut self) {
-        let mir = self.current_fn().body_internal();
-        if let Some(spread_arg) = mir.spread_arg {
-            self.codegen_spread_arg(mir, spread_arg);
+    fn codegen_function_prelude(&mut self, body: &Body) {
+        debug!(spread_arg=?body.spread_arg(), "codegen_function_prelude");
+        if let Some(spread_arg) = body.spread_arg() {
+            self.codegen_spread_arg(body, spread_arg);
         }
     }
 
@@ -117,34 +106,27 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// See:
     /// <https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/Determine.20untupled.20closure.20args.20from.20Instance.3F>
-    fn codegen_spread_arg(&mut self, mir: &Body<'tcx>, spread_arg: Local) {
-        tracing::debug!(current=?self.current_fn, "codegen_spread_arg");
-        let spread_data = &mir.local_decls()[spread_arg];
-        let tup_ty = self.monomorphize(spread_data.ty);
-        if self.is_zst(tup_ty) {
+    fn codegen_spread_arg(&mut self, body: &Body, spread_arg: Local) {
+        debug!(current=?self.current_fn().name(), "codegen_spread_arg");
+        let spread_data = &body.locals()[spread_arg];
+        let tup_ty = spread_data.ty;
+        if self.is_zst_stable(tup_ty) {
             // No need to spread a ZST since it will be ignored.
             return;
         }
 
-        let loc = self.codegen_span(&spread_data.source_info.span);
+        let loc = self.codegen_span_stable(spread_data.span);
 
         // Get the function signature from MIR, _before_ we untuple
-        let fntyp = self.current_fn().instance().ty(self.tcx, ty::ParamEnv::reveal_all());
-        let sig = match fntyp.kind() {
-            ty::FnPtr(..) | ty::FnDef(..) => fntyp.fn_sig(self.tcx).skip_binder(),
-            // Closures themselves will have their arguments already untupled,
-            // see Zulip link above.
-            ty::Closure(..) => unreachable!(
-                "Unexpected `spread arg` set for closure, got: {:?}, {:?}",
-                fntyp,
-                self.current_fn().readable_name()
-            ),
-            _ => unreachable!(
-                "Expected function type for `spread arg` prelude, got: {:?}, {:?}",
-                fntyp,
-                self.current_fn().readable_name()
-            ),
-        };
+        let instance = self.current_fn().instance_stable();
+        // Closures themselves will have their arguments already untupled,
+        // see Zulip link above.
+        assert!(
+            !instance.ty().kind().is_closure(),
+            "Unexpected spread arg `{}` set for closure `{}`",
+            spread_arg,
+            instance.name()
+        );
 
         // When we codegen the function signature elsewhere, we will codegen the untupled version.
         // We then marshall the arguments into a local variable holding the expected tuple.
@@ -166,7 +148,7 @@ impl<'tcx> GotocCtx<'tcx> {
         // };
         // ```
         // Note how the compiler has reordered the fields to improve packing.
-        let tup_type = self.codegen_ty(tup_ty);
+        let tup_type = self.codegen_ty_stable(tup_ty);
 
         // We need to marshall the arguments into the tuple
         // The arguments themselves have been tacked onto the explicit function paramaters by
@@ -185,21 +167,19 @@ impl<'tcx> GotocCtx<'tcx> {
         // }
         // ```
 
-        let tupe = sig.inputs().last().unwrap();
-        let args = match tupe.kind() {
-            ty::Tuple(args) => *args,
-            _ => unreachable!("a function's spread argument must be a tuple"),
+        let TyKind::RigidTy(RigidTy::Tuple(args)) = tup_ty.kind() else {
+            unreachable!("a function's spread argument must be a tuple")
         };
-        let starting_idx = sig.inputs().len();
+        let starting_idx = spread_arg;
         let marshalled_tuple_fields =
             BTreeMap::from_iter(args.iter().enumerate().map(|(arg_i, arg_t)| {
                 // The components come at the end, so offset by the untupled length.
                 // This follows the naming convention defined in `typ.rs`.
-                let lc = Local::from_usize(arg_i + starting_idx);
+                let lc = arg_i + starting_idx;
                 let (name, base_name) = self.codegen_spread_arg_name(&lc);
-                let sym = Symbol::variable(name, base_name, self.codegen_ty(arg_t), loc)
+                let sym = Symbol::variable(name, base_name, self.codegen_ty_stable(*arg_t), loc)
                     .with_is_hidden(false)
-                    .with_is_parameter(!self.is_zst(arg_t));
+                    .with_is_parameter(!self.is_zst_stable(*arg_t));
                 // The spread arguments are additional function paramaters that are patched in
                 // They are to the function signature added in the `fn_typ` function.
                 // But they were never added to the symbol table, which we currently do here.
@@ -222,19 +202,18 @@ impl<'tcx> GotocCtx<'tcx> {
         );
     }
 
-    pub fn declare_function(&mut self, instance: Instance<'tcx>) {
-        debug!("declaring {}; {:?}", instance, instance);
-        self.set_current_fn(instance);
-        debug!(krate = self.current_fn().krate().as_str());
-        debug!(is_std = self.current_fn().is_std());
-        self.ensure(&self.current_fn().name(), |ctx, fname| {
-            let mir = ctx.current_fn().body_internal();
+    pub fn declare_function(&mut self, instance: Instance) {
+        debug!("declaring {}; {:?}", instance.name(), instance);
+        let body = instance.body().unwrap();
+        self.set_current_fn(instance, &body);
+        debug!(krate=?instance.def.krate(), is_std=self.current_fn().is_std(), "declare_function");
+        self.ensure(&self.symbol_name_stable(instance), |ctx, fname| {
             Symbol::function(
                 fname,
-                ctx.fn_typ(),
+                ctx.fn_typ(&body),
                 None,
-                ctx.current_fn().readable_name(),
-                ctx.codegen_span(&mir.span),
+                instance.name(),
+                ctx.codegen_span_stable(instance.def.span()),
             )
         });
         self.reset_current_fn();
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 8869b01bc65a..fa23b85c18f1 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -138,7 +138,7 @@ impl<'tcx> GotocCtx<'tcx> {
         debug!(?fargs, "codegen_intrinsic");
         debug!(?place, "codegen_intrinsic");
         debug!(?span, "codegen_intrinsic");
-        let sig = instance.fn_sig();
+        let sig = instance.ty().kind().fn_sig().unwrap().skip_binder();
         let ret_ty = sig.output();
         let farg_types = sig.inputs();
         let cbmc_ret_ty = self.codegen_ty_stable(ret_ty);
@@ -414,7 +414,8 @@ impl<'tcx> GotocCtx<'tcx> {
             "cttz" => codegen_count_intrinsic!(cttz, true),
             "cttz_nonzero" => codegen_count_intrinsic!(cttz, false),
             "discriminant_value" => {
-                let ty = pointee_type_stable(instance.fn_sig().inputs()[0]).unwrap();
+                let sig = instance.ty().kind().fn_sig().unwrap().skip_binder();
+                let ty = pointee_type_stable(sig.inputs()[0]).unwrap();
                 let e = self.codegen_get_discriminant(fargs.remove(0).dereference(), ty, ret_ty);
                 self.codegen_expr_to_place_stable(place, e)
             }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
index 148318f1c33e..aaec506edf6e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -1,12 +1,10 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::codegen_cprover_gotoc::codegen::ty_stable::StableConverter;
 use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
 use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::unwrap_or_return_codegen_unimplemented;
 use cbmc::goto_program::{DatatypeComponent, Expr, ExprValue, Location, Stmt, Symbol, Type};
-use rustc_middle::mir::Operand as OperandInternal;
-use rustc_middle::ty::{Const as ConstInternal, Instance as InstanceInternal};
+use rustc_middle::ty::Const as ConstInternal;
 use rustc_smir::rustc_internal;
 use rustc_span::Span as SpanInternal;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
@@ -34,10 +32,6 @@ impl<'tcx> GotocCtx<'tcx> {
     /// A MIR operand is either a constant (literal or `const` declaration) or a place
     /// (being moved or copied for this operation).
     /// An "operand" in MIR is the argument to an "Rvalue" (and is also used by some statements.)
-    pub fn codegen_operand(&mut self, operand: &OperandInternal<'tcx>) -> Expr {
-        self.codegen_operand_stable(&StableConverter::convert_operand(self, operand.clone()))
-    }
-
     pub fn codegen_operand_stable(&mut self, operand: &Operand) -> Expr {
         trace!(?operand, "codegen_operand");
         match operand {
@@ -67,7 +61,7 @@ impl<'tcx> GotocCtx<'tcx> {
         constant: ConstInternal<'tcx>,
         span: Option<SpanInternal>,
     ) -> Expr {
-        let stable_const = StableConverter::convert_constant(self, constant);
+        let stable_const = rustc_internal::stable(constant);
         let stable_span = rustc_internal::stable(span);
         self.codegen_const(&stable_const, stable_span)
     }
@@ -586,7 +580,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// sometimes subtly differs from the type that codegen_function_sig returns.
     /// This is tracked in <https://github.com/model-checking/kani/issues/1350>.
     fn codegen_func_symbol(&mut self, instance: Instance) -> (&Symbol, Type) {
-        let funct = self.codegen_function_sig(self.fn_sig_of_instance_stable(instance));
+        let funct = self.codegen_function_sig_stable(self.fn_sig_of_instance_stable(instance));
         let sym = if instance.is_foreign_item() {
             // Get the symbol that represents a foreign instance.
             self.codegen_foreign_fn(instance)
@@ -606,16 +600,6 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Note: In general with this `Expr` you should immediately either `.address_of()` or `.call(...)`.
     ///
     /// This should not be used where Rust expects a "function item" (See `codegen_fn_item`)
-    pub fn codegen_func_expr_internal(
-        &mut self,
-        instance: InstanceInternal<'tcx>,
-        span: Option<&SpanInternal>,
-    ) -> Expr {
-        let (func_symbol, func_typ) = self.codegen_func_symbol(rustc_internal::stable(instance));
-        Expr::symbol_expression(func_symbol.name, func_typ)
-            .with_location(self.codegen_span_option(span.cloned()))
-    }
-
     pub fn codegen_func_expr(&mut self, instance: Instance, span: Option<Span>) -> Expr {
         let (func_symbol, func_typ) = self.codegen_func_symbol(instance);
         Expr::symbol_expression(func_symbol.name, func_typ)
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
index 75f184660765..fd9ff33e164e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -6,13 +6,12 @@
 //! 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::ty_stable::pointee_type;
 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;
 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_smir::rustc_internal;
 use rustc_target::abi::{TagEncoding, Variants};
@@ -390,7 +389,7 @@ impl<'tcx> GotocCtx<'tcx> {
         }
 
         // Otherwise, simply look up the local by the var name.
-        let vname = self.codegen_var_name(&LocalInternal::from(l));
+        let vname = self.codegen_var_name(&l);
         Expr::symbol_expression(vname, self.codegen_ty_stable(local_ty))
     }
 
@@ -637,10 +636,6 @@ impl<'tcx> GotocCtx<'tcx> {
     ///   build the fat pointer from there.
     /// - 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 {
-        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 =
@@ -698,13 +693,6 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
-    pub fn codegen_place(
-        &mut self,
-        place: &PlaceInternal<'tcx>,
-    ) -> Result<ProjectedPlace, UnimplementedData> {
-        self.codegen_place_stable(&StableConverter::convert_place(self, *place))
-    }
-
     /// Given a projection, generate an lvalue that represents the given variant index.
     pub fn codegen_variant_lvalue(
         &mut self,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 71c8e97420b8..c4ea258fe79e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -2,7 +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::{pointee_type_stable, StableConverter};
+use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
 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};
@@ -17,7 +17,6 @@ use cbmc::goto_program::{
 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::{TyCtxt, VtblEntry};
 use rustc_smir::rustc_internal;
 use rustc_target::abi::{FieldsShape, TagEncoding, Variants};
@@ -583,12 +582,8 @@ impl<'tcx> GotocCtx<'tcx> {
             stmts.push(assign_case);
         }
         // 3- Set discriminant.
-        let set_discriminant = self.codegen_set_discriminant(
-            rustc_internal::internal(res_ty),
-            temp_var.clone(),
-            rustc_internal::internal(variant_index),
-            loc,
-        );
+        let set_discriminant =
+            self.codegen_set_discriminant(res_ty, temp_var.clone(), variant_index, loc);
         stmts.push(set_discriminant);
         // 4- Return temporary variable.
         stmts.push(temp_var.as_stmt(loc));
@@ -668,10 +663,6 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
-    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, ?res_ty, "codegen_rvalue");
@@ -831,8 +822,8 @@ impl<'tcx> GotocCtx<'tcx> {
                     //
                     // Note: niche_variants can only represent values that fit in a u32.
                     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 discr_mir_ty = self.codegen_enum_discr_typ_stable(ty);
+                    let discr_type = self.codegen_ty_stable(discr_mir_ty);
                     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());
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
index 9e81ffa57898..c06d64d298c4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs
@@ -5,10 +5,8 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Location;
-use rustc_middle::mir::{Local, VarDebugInfoContents};
 use rustc_smir::rustc_internal;
 use rustc_span::Span;
-use stable_mir::mir::VarDebugInfo;
 use stable_mir::ty::Span as SpanStable;
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -44,17 +42,4 @@ impl<'tcx> GotocCtx<'tcx> {
         let topmost = span.ctxt().outer_expn().expansion_cause().unwrap_or(*span);
         self.codegen_span(&topmost)
     }
-
-    pub fn codegen_span_option(&self, sp: Option<Span>) -> Location {
-        sp.map_or(Location::none(), |x| self.codegen_span(&x))
-    }
-
-    pub fn find_debug_info(&self, l: &Local) -> Option<VarDebugInfo> {
-        rustc_internal::stable(self.current_fn().body_internal().var_debug_info.iter().find(
-            |info| match info.value {
-                VarDebugInfoContents::Place(p) => p.local == *l && p.projection.len() == 0,
-                VarDebugInfoContents::Const(_) => false,
-            },
-        ))
-    }
 }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
index 9034b6a37783..e7b7ee5a376a 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs
@@ -2,24 +2,19 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::typ::TypeExt;
 use super::typ::FN_RETURN_VOID_VAR_NAME;
-use super::PropertyClass;
-use crate::codegen_cprover_gotoc::codegen::ty_stable::StableConverter;
+use super::{bb_label, PropertyClass};
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{Expr, Location, Stmt, Type};
-use rustc_middle::mir;
-use rustc_middle::mir::{
-    AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind,
-    SwitchTargets, Terminator, TerminatorKind,
-};
-use rustc_middle::ty;
 use rustc_middle::ty::layout::LayoutOf;
-use rustc_middle::ty::{Instance, InstanceDef, Ty};
 use rustc_smir::rustc_internal;
-use rustc_span::Span;
-use rustc_target::abi::VariantIdx;
 use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants};
-use stable_mir::mir::{Operand as OperandStable, Place as PlaceStable};
+use stable_mir::mir::mono::{Instance, InstanceKind};
+use stable_mir::mir::{
+    AssertMessage, BasicBlockIdx, CopyNonOverlapping, NonDivergingIntrinsic, Operand, Place,
+    Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, RETURN_LOCAL,
+};
+use stable_mir::ty::{RigidTy, Span, Ty, TyKind, VariantIdx};
 use tracing::{debug, debug_span, trace};
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -28,57 +23,70 @@ impl<'tcx> GotocCtx<'tcx> {
     /// statements and [Terminator]s, which can exclusively appear at the end of a basic block.
     ///
     /// See [GotocCtx::codegen_terminator] for those.
-    pub fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt {
+    pub fn codegen_statement(&mut self, stmt: &Statement) -> Stmt {
         let _trace_span = debug_span!("CodegenStatement", statement = ?stmt).entered();
         debug!(?stmt, kind=?stmt.kind, "handling_statement");
-        let location = self.codegen_span(&stmt.source_info.span);
+        let location = self.codegen_span_stable(stmt.span);
         match &stmt.kind {
-            StatementKind::Assign(box (l, r)) => {
-                let lty = self.place_ty(l);
-                let rty = self.rvalue_ty(r);
+            StatementKind::Assign(lhs, rhs) => {
+                let lty = self.place_ty_stable(lhs);
+                let rty = self.rvalue_ty_stable(rhs);
                 // we ignore assignment for all zero size types
-                if self.is_zst(lty) {
+                if self.is_zst_stable(lty) {
                     Stmt::skip(location)
-                } else if lty.is_fn_ptr() && rty.is_fn() && !rty.is_fn_ptr() {
+                } else if lty.kind().is_fn_ptr() && rty.kind().is_fn() && !rty.kind().is_fn_ptr() {
                     // implicit address of a function pointer, e.g.
                     // let fp: fn() -> i32 = foo;
                     // where the reference is implicit.
-                    unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
-                        .goto_expr
-                        .assign(self.codegen_rvalue(r, location).address_of(), location)
-                } else if rty.is_bool() {
-                    unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
-                        .goto_expr
-                        .assign(self.codegen_rvalue(r, location).cast_to(Type::c_bool()), location)
+                    unwrap_or_return_codegen_unimplemented_stmt!(
+                        self,
+                        self.codegen_place_stable(lhs)
+                    )
+                    .goto_expr
+                    .assign(self.codegen_rvalue_stable(rhs, location).address_of(), location)
+                } else if rty.kind().is_bool() {
+                    unwrap_or_return_codegen_unimplemented_stmt!(
+                        self,
+                        self.codegen_place_stable(lhs)
+                    )
+                    .goto_expr
+                    .assign(
+                        self.codegen_rvalue_stable(rhs, location).cast_to(Type::c_bool()),
+                        location,
+                    )
                 } else {
-                    unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l))
-                        .goto_expr
-                        .assign(self.codegen_rvalue(r, location), location)
+                    unwrap_or_return_codegen_unimplemented_stmt!(
+                        self,
+                        self.codegen_place_stable(lhs)
+                    )
+                    .goto_expr
+                    .assign(self.codegen_rvalue_stable(rhs, location), location)
                 }
             }
             StatementKind::Deinit(place) => self.codegen_deinit(place, location),
             StatementKind::SetDiscriminant { place, variant_index } => {
-                let dest_ty = self.place_ty(place);
-                let dest_expr =
-                    unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
-                        .goto_expr;
+                let dest_ty = self.place_ty_stable(place);
+                let dest_expr = unwrap_or_return_codegen_unimplemented_stmt!(
+                    self,
+                    self.codegen_place_stable(place)
+                )
+                .goto_expr;
                 self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location)
             }
             StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me
             StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me
-            StatementKind::Intrinsic(box NonDivergingIntrinsic::CopyNonOverlapping(
-                mir::CopyNonOverlapping { ref src, ref dst, ref count },
+            StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(
+                CopyNonOverlapping { src, dst, count },
             )) => {
-                let operands =
-                    [src, dst, count].map(|op| StableConverter::convert_operand(self, op.clone()));
+                let operands = [src, dst, count];
                 // Pack the operands and their types, then call `codegen_copy`
                 let fargs =
                     operands.iter().map(|op| self.codegen_operand_stable(op)).collect::<Vec<_>>();
                 let farg_types = operands.map(|op| self.operand_ty_stable(&op));
                 self.codegen_copy("copy_nonoverlapping", true, fargs, &farg_types, None, location)
             }
-            StatementKind::Intrinsic(box NonDivergingIntrinsic::Assume(ref op)) => {
-                let cond = self.codegen_operand(op).cast_to(Type::bool());
+            StatementKind::Intrinsic(NonDivergingIntrinsic::Assume(ref op)) => {
+                let cond = self.codegen_operand_stable(op).cast_to(Type::bool());
                 self.codegen_assert_assume(
                     cond,
                     PropertyClass::Assume,
@@ -87,9 +95,9 @@ impl<'tcx> GotocCtx<'tcx> {
                 )
             }
             StatementKind::PlaceMention(_) => todo!(),
-            StatementKind::FakeRead(_)
+            StatementKind::FakeRead(..)
             | StatementKind::Retag(_, _)
-            | StatementKind::AscribeUserType(_, _)
+            | StatementKind::AscribeUserType { .. }
             | StatementKind::Nop
             | StatementKind::Coverage { .. }
             | StatementKind::ConstEvalCounter => Stmt::skip(location),
@@ -102,15 +110,13 @@ impl<'tcx> GotocCtx<'tcx> {
     /// because of the need for unwinding/drop. For instance, function calls.
     ///
     /// See also [`GotocCtx::codegen_statement`] for ordinary [Statement]s.
-    pub fn codegen_terminator(&mut self, term: &Terminator<'tcx>) -> Stmt {
-        let loc = self.codegen_span(&term.source_info.span);
+    pub fn codegen_terminator(&mut self, term: &Terminator) -> Stmt {
+        let loc = self.codegen_span_stable(term.span);
         let _trace_span = debug_span!("CodegenTerminator", statement = ?term.kind).entered();
         debug!("handling terminator {:?}", term);
         //TODO: Instead of doing location::none(), and updating, just putit in when we make the stmt.
         match &term.kind {
-            TerminatorKind::Goto { target } => {
-                Stmt::goto(self.current_fn().find_label(target), loc)
-            }
+            TerminatorKind::Goto { target } => Stmt::goto(bb_label(*target), loc),
             TerminatorKind::SwitchInt { discr, targets } => {
                 self.codegen_switch_int(discr, targets, loc)
             }
@@ -118,29 +124,31 @@ impl<'tcx> GotocCtx<'tcx> {
             // because we don't want to raise the warning during compilation.
             // These operations will normally be codegen'd but normally be unreachable
             // since we make use of `-C unwind=abort`.
-            TerminatorKind::UnwindResume => self.codegen_mimic_unimplemented(
+            TerminatorKind::Resume => self.codegen_mimic_unimplemented(
                 "TerminatorKind::Resume",
                 loc,
                 "https://github.com/model-checking/kani/issues/692",
             ),
-            TerminatorKind::UnwindTerminate(_) => self.codegen_mimic_unimplemented(
-                "TerminatorKind::UnwindTerminate",
+            TerminatorKind::Abort => self.codegen_mimic_unimplemented(
+                "TerminatorKind::Abort",
                 loc,
                 "https://github.com/model-checking/kani/issues/692",
             ),
             TerminatorKind::Return => {
-                let rty = self.current_fn().sig().skip_binder().output();
-                if rty.is_unit() {
+                let rty = self.current_fn().sig().output();
+                if rty.kind().is_unit() {
                     self.codegen_ret_unit()
                 } else {
-                    let p = Place::from(mir::RETURN_PLACE);
-                    let v =
-                        unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(&p))
-                            .goto_expr;
-                    if self.place_ty(&p).is_bool() {
-                        v.cast_to(Type::c_bool()).ret(loc)
+                    let place = Place::from(RETURN_LOCAL);
+                    let place_expr = unwrap_or_return_codegen_unimplemented_stmt!(
+                        self,
+                        self.codegen_place_stable(&place)
+                    )
+                    .goto_expr;
+                    if self.place_ty_stable(&place).kind().is_bool() {
+                        place_expr.cast_to(Type::c_bool()).ret(loc)
                     } else {
-                        v.ret(loc)
+                        place_expr.ret(loc)
                     }
                 }
             }
@@ -149,36 +157,35 @@ impl<'tcx> GotocCtx<'tcx> {
                 "unreachable code",
                 loc,
             ),
-            TerminatorKind::Drop { place, target, unwind: _, replace: _ } => {
+            TerminatorKind::Drop { place, target, unwind: _ } => {
                 self.codegen_drop(place, target, loc)
             }
             TerminatorKind::Call { func, args, destination, target, .. } => {
-                self.codegen_funcall(func, args, destination, target, term.source_info.span)
+                self.codegen_funcall(func, args, destination, target, term.span)
             }
             TerminatorKind::Assert { cond, expected, msg, target, .. } => {
                 let cond = {
-                    let r = self.codegen_operand(cond);
+                    let r = self.codegen_operand_stable(cond);
                     if *expected { r } else { Expr::not(r) }
                 };
 
-                let msg = if let AssertKind::BoundsCheck { .. } = &**msg {
+                let msg = if let AssertMessage::BoundsCheck { .. } = msg {
                     // For bounds check the following panic message is generated at runtime:
                     // "index out of bounds: the length is {len} but the index is {index}",
                     // but CBMC only accepts static messages so we don't add values to the message.
                     "index out of bounds: the length is less than or equal to the given index"
-                } else if let AssertKind::MisalignedPointerDereference { .. } = &**msg {
+                } else if let AssertMessage::MisalignedPointerDereference { .. } = msg {
                     // Misaligned pointer dereference check messages is also a runtime messages.
                     // Generate a generic one here.
-                    "misaligned pointer dereference: address must be a multiple of its type's alignment"
+                    "misaligned pointer dereference: address must be a multiple of its type's \
+                    alignment"
                 } else {
                     // For all other assert kind we can get the static message.
-                    msg.description()
+                    msg.description().unwrap()
                 };
 
-                let (msg_str, reach_stmt) = self.codegen_reachability_check(
-                    msg.to_owned(),
-                    rustc_internal::stable(term.source_info.span),
-                );
+                let (msg_str, reach_stmt) =
+                    self.codegen_reachability_check(msg.to_owned(), term.span);
 
                 Stmt::block(
                     vec![
@@ -189,17 +196,11 @@ impl<'tcx> GotocCtx<'tcx> {
                             &msg_str,
                             loc,
                         ),
-                        Stmt::goto(self.current_fn().find_label(target), loc),
+                        Stmt::goto(bb_label(*target), loc),
                     ],
                     loc,
                 )
             }
-            TerminatorKind::FalseEdge { .. } | TerminatorKind::FalseUnwind { .. } => {
-                unreachable!("drop elaboration removes these TerminatorKind")
-            }
-            TerminatorKind::Yield { .. } | TerminatorKind::CoroutineDrop => {
-                unreachable!("we should not hit these cases") // why?
-            }
             TerminatorKind::InlineAsm { .. } => self.codegen_unimplemented_stmt(
                 "TerminatorKind::InlineAsm",
                 loc,
@@ -212,19 +213,23 @@ impl<'tcx> GotocCtx<'tcx> {
     /// variant index.
     pub fn codegen_set_discriminant(
         &mut self,
-        dest_ty: Ty<'tcx>,
+        dest_ty: Ty,
         dest_expr: Expr,
         variant_index: VariantIdx,
         location: Location,
     ) -> Stmt {
         // this requires place points to an enum type.
-        let layout = self.layout_of(dest_ty);
+        let dest_ty_internal = rustc_internal::internal(dest_ty);
+        let variant_index_internal = rustc_internal::internal(variant_index);
+        let layout = self.layout_of(dest_ty_internal);
         match &layout.variants {
             Variants::Single { .. } => Stmt::skip(location),
             Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding {
                 TagEncoding::Direct => {
-                    let discr = dest_ty.discriminant_for_variant(self.tcx, variant_index).unwrap();
-                    let discr_t = self.codegen_enum_discr_typ(dest_ty);
+                    let discr = dest_ty_internal
+                        .discriminant_for_variant(self.tcx, variant_index_internal)
+                        .unwrap();
+                    let discr_t = self.codegen_enum_discr_typ(dest_ty_internal);
                     // The constant created below may not fit into the type.
                     // https://github.com/model-checking/kani/issues/996
                     //
@@ -241,18 +246,18 @@ 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, rustc_internal::stable(dest_ty))
-                        .assign(discr_expr, location)
+                    self.codegen_discriminant_field(dest_expr, dest_ty).assign(discr_expr, location)
                 }
                 TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => {
-                    if *untagged_variant != variant_index {
+                    if *untagged_variant != variant_index_internal {
                         let offset = match &layout.fields {
                             FieldsShape::Arbitrary { offsets, .. } => offsets[0usize.into()],
                             _ => unreachable!("niche encoding must have arbitrary fields"),
                         };
-                        let discr_ty = self.codegen_enum_discr_typ(dest_ty);
+                        let discr_ty = self.codegen_enum_discr_typ(dest_ty_internal);
                         let discr_ty = self.codegen_ty(discr_ty);
-                        let niche_value = variant_index.as_u32() - niche_variants.start().as_u32();
+                        let niche_value =
+                            variant_index_internal.as_u32() - niche_variants.start().as_u32();
                         let niche_value = (niche_value as u128).wrapping_add(*niche_start);
                         trace!(val=?niche_value, typ=?discr_ty, "codegen_set_discriminant niche");
                         let value = if niche_value == 0
@@ -276,15 +281,15 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Our model of GotoC has a similar statement, which is later lowered
     /// to assigning a Nondet in CBMC, with a comment specifying that it
     /// corresponds to a Deinit.
-    fn codegen_deinit(&mut self, place: &Place<'tcx>, loc: Location) -> Stmt {
-        let dst_mir_ty = self.place_ty(place);
-        let dst_type = self.codegen_ty(dst_mir_ty);
-        let layout = self.layout_of(dst_mir_ty);
+    fn codegen_deinit(&mut self, place: &Place, loc: Location) -> Stmt {
+        let dst_mir_ty = self.place_ty_stable(place);
+        let dst_type = self.codegen_ty_stable(dst_mir_ty);
+        let layout = self.layout_of_stable(dst_mir_ty);
         if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 {
             // We ignore assignment for all zero size types
             Stmt::skip(loc)
         } else {
-            unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place))
+            unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place_stable(place))
                 .goto_expr
                 .deinit(loc)
         }
@@ -311,20 +316,20 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// TODO: this function doesn't handle unwinding which begins if the destructor panics
     /// <https://github.com/model-checking/kani/issues/221>
-    fn codegen_drop(&mut self, place: &Place<'tcx>, target: &BasicBlock, loc: Location) -> Stmt {
-        let place_ty = self.place_ty(place);
-        let drop_instance = Instance::resolve_drop_in_place(self.tcx, place_ty);
+    fn codegen_drop(&mut self, place: &Place, target: &BasicBlockIdx, loc: Location) -> Stmt {
+        let place_ty = self.place_ty_stable(place);
+        let drop_instance = Instance::resolve_drop_in_place(place_ty);
         debug!(?place_ty, ?drop_instance, "codegen_drop");
         // Once upon a time we did a `hook_applies` check here, but we no longer seem to hook drops
-        let drop_implementation = match drop_instance.def {
-            InstanceDef::DropGlue(_, None) => {
+        let drop_implementation = match drop_instance.kind {
+            InstanceKind::Shim if drop_instance.is_empty_shim() => {
                 // We can skip empty DropGlue functions
                 Stmt::skip(loc)
             }
-            InstanceDef::DropGlue(_def_id, Some(_)) => {
-                let place_ref = self.codegen_place_ref(place);
+            InstanceKind::Shim => {
+                let place_ref = self.codegen_place_ref_stable(place);
                 match place_ty.kind() {
-                    ty::Dynamic(..) => {
+                    TyKind::RigidTy(RigidTy::Dynamic(..)) => {
                         // Virtual drop via a vtable lookup.
                         // Pull the drop function off of the fat pointer's vtable pointer
                         let vtable_ref = place_ref.to_owned().member("vtable", &self.symbol_table);
@@ -346,9 +351,9 @@ impl<'tcx> GotocCtx<'tcx> {
                     }
                     _ => {
                         // Non-virtual, direct drop_in_place call
-                        assert!(!matches!(drop_instance.def, InstanceDef::Virtual(_, _)));
+                        assert!(!matches!(drop_instance.kind, InstanceKind::Virtual { .. }));
 
-                        let func = self.codegen_func_expr_internal(drop_instance, None);
+                        let func = self.codegen_func_expr(drop_instance, None);
                         // The only argument should be a self reference
                         let args = vec![place_ref];
 
@@ -363,11 +368,11 @@ impl<'tcx> GotocCtx<'tcx> {
                     }
                 }
             }
-            _ => unreachable!(
-                "TerminatorKind::Drop but not InstanceDef::DropGlue should be impossible"
+            kind => unreachable!(
+                "Expected a `InstanceKind::Shim` for `TerminatorKind::Drop`, but found {kind:?}"
             ),
         };
-        let goto_target = Stmt::goto(self.current_fn().find_label(target), loc);
+        let goto_target = Stmt::goto(bb_label(*target), loc);
         let block = vec![drop_implementation, goto_target];
         Stmt::block(block, loc)
     }
@@ -378,37 +383,38 @@ impl<'tcx> GotocCtx<'tcx> {
     /// The otherwise value is stores as the last value of targets.
     fn codegen_switch_int(
         &mut self,
-        discr: &Operand<'tcx>,
+        discr: &Operand,
         targets: &SwitchTargets,
         loc: Location,
     ) -> Stmt {
-        let v = self.codegen_operand(discr);
+        let v = self.codegen_operand_stable(discr);
         let switch_ty = v.typ().clone();
-        if targets.all_targets().len() == 1 {
+
+        // Switches with empty branches should've been eliminated already.
+        assert!(targets.len() > 1);
+        if targets.len() == 2 {
             // Translate to a guarded goto
-            let first_target = targets.iter().next().unwrap();
+            let (case, first_target) = targets.branches().next().unwrap();
             Stmt::block(
                 vec![
-                    v.eq(Expr::int_constant(first_target.0, switch_ty)).if_then_else(
-                        Stmt::goto(self.current_fn().find_label(&first_target.1), loc),
+                    v.eq(Expr::int_constant(case, switch_ty)).if_then_else(
+                        Stmt::goto(bb_label(first_target), loc),
                         None,
                         loc,
                     ),
-                    Stmt::goto(self.current_fn().find_label(&targets.otherwise()), loc),
+                    Stmt::goto(bb_label(targets.otherwise()), loc),
                 ],
                 loc,
             )
         } else {
-            // Switches with empty targets should've been eliminated already.
-            assert!(targets.all_targets().len() > 1);
             let cases = targets
-                .iter()
+                .branches()
                 .map(|(c, bb)| {
                     Expr::int_constant(c, switch_ty.clone())
-                        .switch_case(Stmt::goto(self.current_fn().find_label(&bb), loc))
+                        .switch_case(Stmt::goto(bb_label(bb), loc))
                 })
                 .collect();
-            let default = Stmt::goto(self.current_fn().find_label(&targets.otherwise()), loc);
+            let default = Stmt::goto(bb_label(targets.otherwise()), loc);
             v.switch(cases, Some(default), loc)
         }
     }
@@ -427,26 +433,22 @@ impl<'tcx> GotocCtx<'tcx> {
     /// See [GotocCtx::ty_needs_untupled_args] for more details.
     fn codegen_untupled_args(
         &mut self,
-        instance: Instance<'tcx>,
+        instance: Instance,
         fargs: &mut Vec<Expr>,
-        last_mir_arg: Option<&Operand<'tcx>>,
+        last_mir_arg: Option<&Operand>,
     ) {
-        debug!(
-            "codegen_untuple_closure_args instance: {:?}, fargs {:?}",
-            self.readable_instance_name(instance),
-            fargs
-        );
+        debug!("codegen_untuple_closure_args instance: {:?}, fargs {:?}", instance.name(), fargs);
         if !fargs.is_empty() {
-            let tuple_ty = self.operand_ty(last_mir_arg.unwrap());
-            if self.is_zst(tuple_ty) {
+            let tuple_ty = self.operand_ty_stable(last_mir_arg.unwrap());
+            if self.is_zst_stable(tuple_ty) {
                 // Don't pass anything if all tuple elements are ZST.
                 // ZST arguments are ignored.
                 return;
             }
             let tupe = fargs.remove(fargs.len() - 1);
-            if let ty::Tuple(tupled_args) = tuple_ty.kind() {
+            if let TyKind::RigidTy(RigidTy::Tuple(tupled_args)) = tuple_ty.kind() {
                 for (idx, arg_ty) in tupled_args.iter().enumerate() {
-                    if !self.is_zst(arg_ty) {
+                    if !self.is_zst_stable(*arg_ty) {
                         // Access the tupled parameters through the `member` operation
                         let idx_expr = tupe.clone().member(&idx.to_string(), &self.symbol_table);
                         fargs.push(idx_expr);
@@ -458,9 +460,9 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Because function calls terminate basic blocks, to "end" a function call, we
     /// must jump to the next basic block.
-    fn codegen_end_call(&self, target: Option<&BasicBlock>, loc: Location) -> Stmt {
+    fn codegen_end_call(&self, target: Option<BasicBlockIdx>, loc: Location) -> Stmt {
         if let Some(next_bb) = target {
-            Stmt::goto(self.current_fn().find_label(next_bb), loc)
+            Stmt::goto(bb_label(next_bb), loc)
         } else {
             self.codegen_sanity(Expr::bool_false(), "Unexpected return from Never function", loc)
         }
@@ -471,11 +473,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// N.B. public only because instrinsics use this directly, too.
     /// When `skip_zst` is set to `true`, the return value will not include any argument that is ZST.
     /// This is used because we ignore ZST arguments, except for intrinsics.
-    pub(crate) fn codegen_funcall_args(
-        &mut self,
-        args: &[OperandStable],
-        skip_zst: bool,
-    ) -> Vec<Expr> {
+    pub(crate) fn codegen_funcall_args(&mut self, args: &[Operand], skip_zst: bool) -> Vec<Expr> {
         let fargs = args
             .iter()
             .filter_map(|op| {
@@ -509,99 +507,72 @@ impl<'tcx> GotocCtx<'tcx> {
     /// 2. If a Kani hook applies, do that instead.
     fn codegen_funcall(
         &mut self,
-        func: &Operand<'tcx>,
-        args: &[Operand<'tcx>],
-        destination: &Place<'tcx>,
-        target: &Option<BasicBlock>,
+        func: &Operand,
+        args: &[Operand],
+        destination: &Place,
+        target: &Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
         debug!(?func, ?args, ?destination, ?span, "codegen_funcall");
-        let func_stable = StableConverter::convert_operand(self, func.clone());
-        let args_stable = args
-            .iter()
-            .map(|arg| StableConverter::convert_operand(self, arg.clone()))
-            .collect::<Vec<_>>();
-        let destination_stable = StableConverter::convert_place(self, *destination);
-
-        if self.is_intrinsic(&func_stable) {
+        if self.is_intrinsic(&func) {
             return self.codegen_funcall_of_intrinsic(
-                &func_stable,
-                &args_stable,
-                &destination_stable,
-                target.map(|bb| bb.index()),
-                rustc_internal::stable(span),
+                &func,
+                &args,
+                &destination,
+                target.map(|bb| bb),
+                span,
             );
         }
 
-        let loc = self.codegen_span(&span);
-        let funct = self.operand_ty(func);
-        let mut fargs = self.codegen_funcall_args(&args_stable, true);
-        match &funct.kind() {
-            ty::FnDef(defid, subst) => {
-                let instance =
-                    Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *defid, subst)
-                        .unwrap()
-                        .unwrap();
+        let loc = self.codegen_span_stable(span);
+        let funct = self.operand_ty_stable(func);
+        let mut fargs = self.codegen_funcall_args(&args, true);
+        match funct.kind() {
+            TyKind::RigidTy(RigidTy::FnDef(def, subst)) => {
+                let instance = Instance::resolve(def, &subst).unwrap();
 
                 // TODO(celina): Move this check to be inside codegen_funcall_args.
-                if self.ty_needs_untupled_args(funct) {
+                if self.ty_needs_untupled_args(rustc_internal::internal(funct)) {
                     self.codegen_untupled_args(instance, &mut fargs, args.last());
                 }
 
-                let stable_instance = rustc_internal::stable(instance);
-                if let Some(hk) = self.hooks.hook_applies(self.tcx, stable_instance) {
-                    return hk.handle(
-                        self,
-                        stable_instance,
-                        fargs,
-                        rustc_internal::stable(destination),
-                        target.map(BasicBlock::as_usize),
-                        rustc_internal::stable(span),
-                    );
+                if let Some(hk) = self.hooks.hook_applies(self.tcx, instance) {
+                    return hk.handle(self, instance, fargs, destination, *target, span);
                 }
 
-                let mut stmts: Vec<Stmt> = match instance.def {
+                let mut stmts: Vec<Stmt> = match instance.kind {
                     // Here an empty drop glue is invoked; we just ignore it.
-                    InstanceDef::DropGlue(_, None) => {
-                        return Stmt::goto(self.current_fn().find_label(&target.unwrap()), loc);
+                    InstanceKind::Shim if instance.is_empty_shim() => {
+                        return Stmt::goto(bb_label(target.unwrap()), loc);
                     }
                     // Handle a virtual function call via a vtable lookup
-                    InstanceDef::Virtual(_, idx) => {
-                        let self_ty = self.operand_ty(&args[0]);
+                    InstanceKind::Virtual { idx } => {
+                        let self_ty = self.operand_ty_stable(&args[0]);
                         self.codegen_virtual_funcall(self_ty, idx, destination, &mut fargs, loc)
                     }
                     // Normal, non-virtual function calls
-                    InstanceDef::Item(..)
-                    | InstanceDef::DropGlue(_, Some(_))
-                    | InstanceDef::FnPtrAddrShim(_, _)
-                    | InstanceDef::Intrinsic(..)
-                    | InstanceDef::FnPtrShim(..)
-                    | InstanceDef::VTableShim(..)
-                    | InstanceDef::ReifyShim(..)
-                    | InstanceDef::ClosureOnceShim { .. }
-                    | InstanceDef::CloneShim(..) => {
+                    InstanceKind::Item | InstanceKind::Intrinsic | InstanceKind::Shim => {
                         // We need to handle FnDef items in a special way because `codegen_operand` compiles them to dummy structs.
                         // (cf. the function documentation)
-                        let func_exp = self.codegen_func_expr_internal(instance, None);
+                        let func_exp = self.codegen_func_expr(instance, None);
                         vec![
-                            self.codegen_expr_to_place(destination, func_exp.call(fargs))
+                            self.codegen_expr_to_place_stable(destination, func_exp.call(fargs))
                                 .with_location(loc),
                         ]
                     }
-                    InstanceDef::ThreadLocalShim(_) => todo!(),
                 };
-                stmts.push(self.codegen_end_call(target.as_ref(), loc));
+                stmts.push(self.codegen_end_call(*target, loc));
                 Stmt::block(stmts, loc)
             }
             // Function call through a pointer
-            ty::FnPtr(_) => {
-                let func_expr = self.codegen_operand(func).dereference();
+            TyKind::RigidTy(RigidTy::FnPtr(_)) => {
+                let func_expr = self.codegen_operand_stable(func).dereference();
                 // Actually generate the function call and return.
                 Stmt::block(
                     vec![
-                        self.codegen_expr_to_place(destination, func_expr.call(fargs))
+                        self.codegen_expr_to_place_stable(destination, func_expr.call(fargs))
                             .with_location(loc),
-                        Stmt::goto(self.current_fn().find_label(&target.unwrap()), loc),
+                        Stmt::goto(bb_label(target.unwrap()), loc),
                     ],
                     loc,
                 )
@@ -613,10 +584,10 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Extract a reference to self for virtual method calls.
     ///
     /// See [GotocCtx::codegen_dynamic_function_sig] for more details.
-    fn extract_ptr(&self, arg_expr: Expr, arg_ty: Ty<'tcx>) -> Expr {
+    fn extract_ptr(&self, arg_expr: Expr, arg_ty: Ty) -> Expr {
         // Generate an expression that indexes the pointer.
         let expr = self
-            .receiver_data_path(arg_ty)
+            .receiver_data_path(rustc_internal::internal(arg_ty))
             .fold(arg_expr, |curr_expr, (name, _)| curr_expr.member(name, &self.symbol_table));
 
         trace!(?arg_ty, gotoc_ty=?expr.typ(), gotoc_expr=?expr.value(), "extract_ptr");
@@ -640,9 +611,9 @@ impl<'tcx> GotocCtx<'tcx> {
     /// 4. Generate the function call.
     fn codegen_virtual_funcall(
         &mut self,
-        self_ty: Ty<'tcx>,
+        self_ty: Ty,
         idx: usize,
-        place: &Place<'tcx>,
+        place: &Place,
         fargs: &mut [Expr],
         loc: Location,
     ) -> Vec<Stmt> {
@@ -664,7 +635,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         let data_ptr = trait_fat_ptr.to_owned().member("data", &self.symbol_table);
         let mut ret_stmts = vec![];
-        fargs[0] = if self_ty.is_adt() {
+        fargs[0] = if self_ty.kind().is_adt() {
             // Generate a temp variable and assign its inner pointer to the fat_ptr.data.
             match fn_ptr.typ() {
                 Type::Pointer { typ: box Type::Code { parameters, .. } } => {
@@ -697,7 +668,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
         // Virtual function call and corresponding nonnull assertion.
         let call = fn_ptr.dereference().call(fargs.to_vec());
-        let call_stmt = self.codegen_expr_to_place(place, call).with_location(loc);
+        let call_stmt = self.codegen_expr_to_place_stable(place, call).with_location(loc);
         let call_stmt = if self.vtable_ctx.emit_vtable_restrictions {
             self.virtual_call_with_restricted_fn_ptr(trait_fat_ptr.typ().clone(), idx, call_stmt)
         } else {
@@ -712,7 +683,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// A MIR [Place] is an L-value (i.e. the LHS of an assignment).
     ///
     /// In Kani, we slightly optimize the special case for Unit and don't assign anything.
-    pub(crate) fn codegen_expr_to_place_stable(&mut self, place: &PlaceStable, expr: Expr) -> Stmt {
+    pub(crate) fn codegen_expr_to_place_stable(&mut self, place: &Place, expr: Expr) -> Stmt {
         if self.place_ty_stable(place).kind().is_unit() {
             expr.as_stmt(Location::none())
         } else {
@@ -721,14 +692,4 @@ impl<'tcx> GotocCtx<'tcx> {
                 .assign(expr, Location::none())
         }
     }
-
-    pub(crate) fn codegen_expr_to_place(&mut self, p: &Place<'tcx>, e: Expr) -> Stmt {
-        if self.place_ty(p).is_unit() {
-            e.as_stmt(Location::none())
-        } else {
-            unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(p))
-                .goto_expr
-                .assign(e, Location::none())
-        }
-    }
 }
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 a32de2040f75..2213676d5a63 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs
@@ -8,21 +8,16 @@
 
 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::{
-    Location, Operand as OperandInternal, Place as PlaceInternal, Rvalue as RvalueInternal,
-};
 use rustc_middle::ty::layout::{LayoutOf, TyAndLayout};
-use rustc_middle::ty::{self, Const as ConstInternal, GenericArgsRef, Ty as TyInternal, TyCtxt};
+use rustc_middle::ty::{self};
 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};
+use stable_mir::ty::{FnSig, RigidTy, Ty, TyKind};
 
 impl<'tcx> GotocCtx<'tcx> {
     pub fn place_ty_stable(&self, place: &Place) -> Ty {
-        place.ty(self.current_fn().body().locals()).unwrap()
+        place.ty(self.current_fn().locals()).unwrap()
     }
 
     pub fn codegen_ty_stable(&mut self, ty: Ty) -> Type {
@@ -34,11 +29,11 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn local_ty_stable(&self, local: Local) -> Ty {
-        self.current_fn().body().local_decl(local).unwrap().ty
+        self.current_fn().locals()[local].ty
     }
 
     pub fn operand_ty_stable(&self, operand: &Operand) -> Ty {
-        operand.ty(self.current_fn().body().locals()).unwrap()
+        operand.ty(self.current_fn().locals()).unwrap()
     }
 
     pub fn is_zst_stable(&self, ty: Ty) -> bool {
@@ -58,8 +53,11 @@ impl<'tcx> GotocCtx<'tcx> {
         )
     }
 
-    pub fn fn_sig_of_instance_stable(&self, instance: Instance) -> ty::PolyFnSig<'tcx> {
-        self.fn_sig_of_instance(rustc_internal::internal(instance))
+    pub fn fn_sig_of_instance_stable(&self, instance: Instance) -> FnSig {
+        let fn_sig = self.fn_sig_of_instance(rustc_internal::internal(instance));
+        let fn_sig =
+            self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), fn_sig);
+        rustc_internal::stable(fn_sig)
     }
 
     pub fn use_fat_pointer_stable(&self, pointer_ty: Ty) -> bool {
@@ -87,13 +85,36 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn rvalue_ty_stable(&self, rvalue: &Rvalue) -> Ty {
-        rvalue.ty(self.current_fn().body().locals()).unwrap()
+        rvalue.ty(self.current_fn().locals()).unwrap()
     }
 
     pub fn simd_size_and_type(&self, ty: Ty) -> (u64, Ty) {
         let (sz, ty) = rustc_internal::internal(ty).simd_size_and_type(self.tcx);
         (sz, rustc_internal::stable(ty))
     }
+
+    pub fn codegen_enum_discr_typ_stable(&self, ty: Ty) -> Ty {
+        rustc_internal::stable(self.codegen_enum_discr_typ(rustc_internal::internal(ty)))
+    }
+
+    pub fn codegen_function_sig_stable(&mut self, sig: FnSig) -> Type {
+        let params = sig
+            .inputs()
+            .iter()
+            .filter_map(|ty| {
+                if self.is_zst_stable(*ty) { None } else { Some(self.codegen_ty_stable(*ty)) }
+            })
+            .collect();
+
+        if sig.c_variadic {
+            Type::variadic_code_with_unnamed_parameters(
+                params,
+                self.codegen_ty_stable(sig.output()),
+            )
+        } else {
+            Type::code_with_unnamed_parameters(params, self.codegen_ty_stable(sig.output()))
+        }
+    }
 }
 /// If given type is a Ref / Raw ref, return the pointee type.
 pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
@@ -112,47 +133,6 @@ pub fn pretty_ty(ty: Ty) -> String {
     rustc_internal::internal(ty).to_string()
 }
 
-/// Convert internal rustc's structs into StableMIR ones.
-///
-/// The body of a StableMIR instance already comes monomorphized, which is different from rustc's
-/// internal representation. To allow us to migrate parts of the code generation stage with
-/// smaller PRs, we have to instantiate rustc's components when converting them to stable.
-///
-/// Once we finish migrating the entire function code generation, we can remove this code.
-pub struct StableConverter<'a, 'tcx> {
-    gcx: &'a GotocCtx<'tcx>,
-}
-
-impl<'a, 'tcx> StableConverter<'a, 'tcx> {
-    pub fn convert_place(gcx: &'a GotocCtx<'tcx>, mut place: PlaceInternal<'tcx>) -> Place {
-        let mut converter = StableConverter { gcx };
-        converter.visit_place(
-            &mut place,
-            PlaceContext::NonUse(NonUseContext::VarDebugInfo),
-            mir::Location::START,
-        );
-        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);
-        rustc_internal::stable(operand)
-    }
-
-    pub fn convert_constant(gcx: &'a GotocCtx<'tcx>, mut constant: ConstInternal<'tcx>) -> Const {
-        let mut converter = StableConverter { gcx };
-        converter.visit_ty_const(&mut constant, mir::Location::START);
-        rustc_internal::stable(constant)
-    }
-}
-
 pub fn pointee_type_stable(ty: Ty) -> Option<Ty> {
     match ty.kind() {
         TyKind::RigidTy(RigidTy::Ref(_, pointee_ty, _))
@@ -160,35 +140,3 @@ pub fn pointee_type_stable(ty: Ty) -> Option<Ty> {
         _ => None,
     }
 }
-
-impl<'a, 'tcx> MutVisitor<'tcx> for StableConverter<'a, 'tcx> {
-    fn tcx(&self) -> TyCtxt<'tcx> {
-        self.gcx.tcx
-    }
-
-    fn visit_ty(&mut self, ty: &mut TyInternal<'tcx>, _: mir::visit::TyContext) {
-        *ty = self.gcx.monomorphize(*ty);
-    }
-
-    fn visit_ty_const(&mut self, ct: &mut ty::Const<'tcx>, _location: mir::Location) {
-        *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) {
-            Ok(v) => v,
-            Err(mir::interpret::ErrorHandled::Reported(..)) => return,
-            Err(mir::interpret::ErrorHandled::TooGeneric(..)) => {
-                unreachable!("Failed to evaluate instance constant: {:?}", const_)
-            }
-        };
-        let ty = constant.ty();
-        constant.const_ = mir::Const::Val(val, ty);
-        self.super_constant(constant, location);
-    }
-}
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
index 9f99801e95b9..661d6da38b6d 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -8,7 +8,6 @@ use cbmc::{InternString, InternedString};
 use rustc_ast::ast::Mutability;
 use rustc_hir::{LangItem, Unsafety};
 use rustc_index::IndexVec;
-use rustc_middle::mir::{HasLocalDecls, Local, Operand, Place, Rvalue};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::print::FmtPrinter;
@@ -25,6 +24,7 @@ use rustc_target::abi::{
     TyAndLayout, VariantIdx, Variants,
 };
 use rustc_target::spec::abi::Abi;
+use stable_mir::mir::Body;
 use std::iter;
 use tracing::{debug, trace, warn};
 
@@ -436,22 +436,6 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
-    pub fn local_ty(&self, l: Local) -> Ty<'tcx> {
-        self.monomorphize(self.current_fn().body_internal().local_decls()[l].ty)
-    }
-
-    pub fn rvalue_ty(&self, rv: &Rvalue<'tcx>) -> Ty<'tcx> {
-        self.monomorphize(rv.ty(self.current_fn().body_internal().local_decls(), self.tcx))
-    }
-
-    pub fn operand_ty(&self, o: &Operand<'tcx>) -> Ty<'tcx> {
-        self.monomorphize(o.ty(self.current_fn().body_internal().local_decls(), self.tcx))
-    }
-
-    pub fn place_ty(&self, p: &Place<'tcx>) -> Ty<'tcx> {
-        self.monomorphize(p.ty(self.current_fn().body_internal().local_decls(), self.tcx).ty)
-    }
-
     /// Is the MIR type a zero-sized type.
     pub fn is_zst(&self, t: Ty<'tcx>) -> bool {
         self.layout_of(t).is_zst()
@@ -735,6 +719,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// also c.f. <https://www.ralfj.de/blog/2020/04/04/layout-debugging.html>
     ///      c.f. <https://rust-lang.github.io/unsafe-code-guidelines/introduction.html>
     pub fn codegen_ty(&mut self, ty: Ty<'tcx>) -> Type {
+        // TODO: Remove all monomorphize calls
         let normalized = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), ty);
         let goto_typ = self.codegen_ty_inner(normalized);
         if let Some(tag) = goto_typ.tag() {
@@ -1303,17 +1288,7 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_function_sig(&mut self, sig: PolyFnSig<'tcx>) -> Type {
         let sig = self.monomorphize(sig);
         let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig);
-        let params = sig
-            .inputs()
-            .iter()
-            .filter_map(|t| if self.is_zst(*t) { None } else { Some(self.codegen_ty(*t)) })
-            .collect();
-
-        if sig.c_variadic {
-            Type::variadic_code_with_unnamed_parameters(params, self.codegen_ty(sig.output()))
-        } else {
-            Type::code_with_unnamed_parameters(params, self.codegen_ty(sig.output()))
-        }
+        self.codegen_function_sig_stable(rustc_internal::stable(sig))
     }
 
     /// Creates a zero-sized struct for a FnDef.
@@ -1681,39 +1656,39 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// the function type of the current instance
-    pub fn fn_typ(&mut self) -> Type {
-        let sig = self.current_fn().sig();
-        let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig);
-        // we don't call [codegen_function_sig] because we want to get a bit more metainformation.
-        let is_vtable_shim =
-            matches!(self.current_fn().instance().def, ty::InstanceDef::VTableShim(..));
+    pub fn fn_typ(&mut self, body: &Body) -> Type {
+        let sig = self.current_fn().sig().clone();
+        let internal_instance = self.current_fn().instance();
+        let is_vtable_shim = matches!(internal_instance.def, ty::InstanceDef::VTableShim(..));
         let mut params: Vec<Parameter> = sig
             .inputs()
             .iter()
             .enumerate()
-            .filter_map(|(i, t)| {
+            .filter_map(|(i, ty)| {
+                debug!(?i, ?ty, "fn_typ");
                 let is_vtable_shim_self = i == 0 && is_vtable_shim;
-                if self.is_zst(*t) && !is_vtable_shim_self {
+                if self.is_zst_stable(*ty) && !is_vtable_shim_self {
                     // We ignore zero-sized parameters.
                     // See https://github.com/model-checking/kani/issues/274 for more details.
                     None
                 } else {
-                    let lc = Local::from_usize(i + 1);
+                    // An arg is the local with index offset by one (return value is always local 0)
+                    let lc = i + 1;
                     let mut ident = self.codegen_var_name(&lc);
 
                     // `spread_arg` indicates that the last argument is tupled
-                    // at the LLVM/codegen level, so we need to declare the indivual
+                    // at the LLVM/codegen level, so we need to declare the individual
                     // components as parameters with a special naming convention
                     // so that we can "retuple" them in the function prelude.
                     // See: compiler/rustc_codegen_llvm/src/gotoc/mod.rs:codegen_function_prelude
-                    if let Some(spread) = self.current_fn().body_internal().spread_arg {
-                        if lc.index() >= spread.index() {
+                    if let Some(spread) = body.spread_arg() {
+                        if lc >= spread {
                             let (name, _) = self.codegen_spread_arg_name(&lc);
                             ident = name;
                         }
                     }
                     Some(
-                        self.codegen_ty(*t)
+                        self.codegen_ty_stable(*ty)
                             .as_parameter(Some(ident.clone().into()), Some(ident.into())),
                     )
                 }
@@ -1734,9 +1709,9 @@ impl<'tcx> GotocCtx<'tcx> {
 
         debug!(?params, signature=?sig, "function_type");
         if sig.c_variadic {
-            Type::variadic_code(params, self.codegen_ty(sig.output()))
+            Type::variadic_code(params, self.codegen_ty_stable(sig.output()))
         } else {
-            Type::code(params, self.codegen_ty(sig.output()))
+            Type::code(params, self.codegen_ty_stable(sig.output()))
         }
     }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 5d27375de54f..21dea6160536 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -47,6 +47,7 @@ use rustc_smir::rustc_internal;
 use rustc_target::abi::Endian;
 use rustc_target::spec::PanicStrategy;
 use stable_mir::mir::mono::MonoItem as MonoItemStable;
+use stable_mir::CrateDef;
 use std::any::Any;
 use std::collections::BTreeMap;
 use std::collections::HashSet;
@@ -102,23 +103,21 @@ impl GotocCodegenBackend {
                 for item in &items {
                     match *item {
                         MonoItem::Fn(instance) => {
+                            let instance = rustc_internal::stable(instance);
                             gcx.call_with_panic_debug_info(
                                 |ctx| ctx.declare_function(instance),
-                                format!(
-                                    "declare_function: {}",
-                                    gcx.readable_instance_name(instance)
-                                ),
-                                instance.def_id(),
+                                format!("declare_function: {}", instance.name()),
+                                instance.def,
                             );
                         }
-                        MonoItem::Static(def_id) => {
+                        MonoItem::Static(_) => {
                             let MonoItemStable::Static(def) = rustc_internal::stable(item) else {
                                 unreachable!()
                             };
                             gcx.call_with_panic_debug_info(
                                 |ctx| ctx.declare_static(def),
-                                format!("declare_static: {def_id:?}"),
-                                def_id,
+                                format!("declare_static: {}", def.name()),
+                                def,
                             );
                         }
                         MonoItem::GlobalAsm(_) => {} // Ignore this. We have already warned about it.
@@ -129,24 +128,25 @@ impl GotocCodegenBackend {
                 for item in &items {
                     match *item {
                         MonoItem::Fn(instance) => {
+                            let instance = rustc_internal::stable(instance);
                             gcx.call_with_panic_debug_info(
                                 |ctx| ctx.codegen_function(instance),
                                 format!(
                                     "codegen_function: {}\n{}",
-                                    gcx.readable_instance_name(instance),
-                                    gcx.symbol_name(instance)
+                                    instance.name(),
+                                    gcx.symbol_name_stable(instance)
                                 ),
-                                instance.def_id(),
+                                instance.def,
                             );
                         }
-                        MonoItem::Static(def_id) => {
+                        MonoItem::Static(_) => {
                             let MonoItemStable::Static(def) = rustc_internal::stable(item) else {
                                 unreachable!()
                             };
                             gcx.call_with_panic_debug_info(
                                 |ctx| ctx.codegen_static(def),
-                                format!("codegen_static: {def_id:?}"),
-                                def_id,
+                                format!("codegen_static: {}", def.name()),
+                                def,
                             );
                         }
                         MonoItem::GlobalAsm(_) => {} // We have already warned above
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
index e39d44743c5f..e73a4756a581 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs
@@ -3,12 +3,15 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Stmt;
-use rustc_middle::mir::{BasicBlock, Body as InternalBody};
-use rustc_middle::ty::{Instance as InternalInstance, PolyFnSig};
+use cbmc::InternedString;
+use rustc_middle::mir::Body as InternalBody;
+use rustc_middle::ty::Instance as InternalInstance;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
-use stable_mir::mir::Body;
+use stable_mir::mir::{Body, Local, LocalDecl};
+use stable_mir::ty::FnSig;
 use stable_mir::CrateDef;
+use std::collections::HashMap;
 
 /// This structure represents useful data about the function we are currently compiling.
 #[derive(Debug)]
@@ -17,39 +20,48 @@ pub struct CurrentFnCtx<'tcx> {
     block: Vec<Stmt>,
     /// The codegen instance for the current function
     instance: Instance,
+    /// The current function signature.
+    fn_sig: FnSig,
     /// The crate this function is from
     krate: String,
     /// The MIR for the current instance. This is using the internal representation.
     mir: &'tcx InternalBody<'tcx>,
-    /// The MIR for the current instance.
-    body: Body,
+    /// A list of local declarations used to retrieve MIR component types.
+    locals: Vec<LocalDecl>,
+    /// A list of pretty names for locals that corrspond to user variables.
+    local_names: HashMap<Local, InternedString>,
     /// The symbol name of the current function
     name: String,
     /// A human readable pretty name for the current function
     readable_name: String,
-    /// The signature of the current function
-    sig: PolyFnSig<'tcx>,
     /// A counter to enable creating temporary variables
     temp_var_counter: u64,
 }
 
 /// Constructor
 impl<'tcx> CurrentFnCtx<'tcx> {
-    pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>) -> Self {
+    pub fn new(instance: Instance, gcx: &GotocCtx<'tcx>, body: &Body) -> Self {
         let internal_instance = rustc_internal::internal(instance);
-        let body = instance.body().unwrap();
         let readable_name = instance.name();
         let name =
             if &readable_name == "main" { readable_name.clone() } else { instance.mangled_name() };
+        let locals = body.locals().to_vec();
+        let local_names = body
+            .var_debug_info
+            .iter()
+            .filter_map(|info| info.local().map(|local| (local, (&info.name).into())))
+            .collect::<HashMap<_, _>>();
+        let fn_sig = gcx.fn_sig_of_instance_stable(instance);
         Self {
             block: vec![],
             instance,
+            fn_sig,
             mir: gcx.tcx.instance_mir(internal_instance.def),
             krate: instance.def.krate().name,
-            body,
+            locals,
+            local_names,
             name,
             readable_name,
-            sig: gcx.fn_sig_of_instance(internal_instance),
             temp_var_counter: 0,
         }
     }
@@ -80,9 +92,8 @@ impl<'tcx> CurrentFnCtx<'tcx> {
         rustc_internal::internal(self.instance)
     }
 
-    /// The crate that function came from
-    pub fn krate(&self) -> String {
-        self.krate.to_string()
+    pub fn instance_stable(&self) -> Instance {
+        self.instance
     }
 
     /// The internal MIR for the function we are currently compiling using internal APIs.
@@ -101,13 +112,16 @@ impl<'tcx> CurrentFnCtx<'tcx> {
     }
 
     /// The signature of the function we are currently compiling
-    pub fn sig(&self) -> PolyFnSig<'tcx> {
-        self.sig
+    pub fn sig(&self) -> &FnSig {
+        &self.fn_sig
     }
 
-    /// The body of the function.
-    pub fn body(&self) -> &Body {
-        &self.body
+    pub fn locals(&self) -> &[LocalDecl] {
+        &self.locals
+    }
+
+    pub fn local_name(&self, local: Local) -> Option<InternedString> {
+        self.local_names.get(&local).copied()
     }
 }
 
@@ -117,8 +131,4 @@ impl CurrentFnCtx<'_> {
     pub fn is_std(&self) -> bool {
         self.krate == "std" || self.krate == "core"
     }
-
-    pub fn find_label(&self, bb: &BasicBlock) -> String {
-        format!("{bb:?}")
-    }
 }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index 61861827df96..4a30837ae812 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -29,12 +29,13 @@ use rustc_middle::ty::layout::{
     FnAbiError, FnAbiOfHelpers, FnAbiRequest, HasParamEnv, HasTyCtxt, LayoutError, LayoutOfHelpers,
     TyAndLayout,
 };
-use rustc_middle::ty::{self, Instance, Ty, TyCtxt};
-use rustc_smir::rustc_internal;
+use rustc_middle::ty::{self, Ty, TyCtxt};
 use rustc_span::source_map::respan;
 use rustc_span::Span;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
+use stable_mir::mir::mono::Instance;
+use stable_mir::mir::Body;
 use stable_mir::ty::Allocation;
 
 pub struct GotocCtx<'tcx> {
@@ -298,8 +299,8 @@ impl<'tcx> GotocCtx<'tcx> {
 
 /// Mutators
 impl<'tcx> GotocCtx<'tcx> {
-    pub fn set_current_fn(&mut self, instance: Instance<'tcx>) {
-        self.current_fn = Some(CurrentFnCtx::new(rustc_internal::stable(instance), self));
+    pub fn set_current_fn(&mut self, instance: Instance, body: &Body) {
+        self.current_fn = Some(CurrentFnCtx::new(instance, self, body));
     }
 
     pub fn reset_current_fn(&mut self) {
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index b914c46c0f6c..97606688d1ed 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -29,7 +29,7 @@ pub trait GotocHook {
         gcx: &mut GotocCtx,
         instance: Instance,
         fargs: Vec<Expr>,
-        assign_to: Place,
+        assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt;
@@ -65,7 +65,7 @@ impl GotocHook for Cover {
         gcx: &mut GotocCtx,
         _instance: Instance,
         mut fargs: Vec<Expr>,
-        _assign_to: Place,
+        _assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
@@ -100,7 +100,7 @@ impl GotocHook for Assume {
         gcx: &mut GotocCtx,
         _instance: Instance,
         mut fargs: Vec<Expr>,
-        _assign_to: Place,
+        _assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
@@ -124,7 +124,7 @@ impl GotocHook for Assert {
         gcx: &mut GotocCtx,
         _instance: Instance,
         mut fargs: Vec<Expr>,
-        _assign_to: Place,
+        _assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
@@ -165,20 +165,20 @@ impl GotocHook for Nondet {
         gcx: &mut GotocCtx,
         _instance: Instance,
         fargs: Vec<Expr>,
-        assign_to: Place,
+        assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
         assert!(fargs.is_empty());
         let loc = gcx.codegen_span_stable(span);
         let target = target.unwrap();
-        let pt = gcx.place_ty_stable(&assign_to);
+        let pt = gcx.place_ty_stable(assign_to);
         if pt.kind().is_unit() {
             Stmt::goto(bb_label(target), loc)
         } else {
             let pe = unwrap_or_return_codegen_unimplemented_stmt!(
                 gcx,
-                gcx.codegen_place_stable(&assign_to)
+                gcx.codegen_place_stable(assign_to)
             )
             .goto_expr;
             Stmt::block(
@@ -209,7 +209,7 @@ impl GotocHook for Panic {
         gcx: &mut GotocCtx,
         _instance: Instance,
         fargs: Vec<Expr>,
-        _assign_to: Place,
+        _assign_to: &Place,
         _target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
@@ -231,7 +231,7 @@ impl GotocHook for RustAlloc {
         gcx: &mut GotocCtx,
         instance: Instance,
         mut fargs: Vec<Expr>,
-        assign_to: Place,
+        assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
@@ -243,7 +243,7 @@ impl GotocHook for RustAlloc {
             vec![
                 unwrap_or_return_codegen_unimplemented_stmt!(
                     gcx,
-                    gcx.codegen_place_stable(&assign_to)
+                    gcx.codegen_place_stable(assign_to)
                 )
                 .goto_expr
                 .assign(
@@ -282,7 +282,7 @@ impl GotocHook for MemCmp {
         gcx: &mut GotocCtx,
         instance: Instance,
         mut fargs: Vec<Expr>,
-        assign_to: Place,
+        assign_to: &Place,
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
@@ -304,7 +304,7 @@ impl GotocHook for MemCmp {
         let is_second_ok = second_var.clone().is_nonnull();
         let should_skip_pointer_checks = is_count_zero.and(is_first_ok).and(is_second_ok);
         let place_expr =
-            unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(&assign_to))
+            unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(assign_to))
                 .goto_expr;
         let rhs = should_skip_pointer_checks.ternary(
             Expr::int_constant(0, place_expr.typ().clone()), // zero bytes are always equal (as long as pointers are nonnull and aligned)
@@ -338,7 +338,7 @@ impl GotocHook for UntrackedDeref {
         gcx: &mut GotocCtx,
         _instance: Instance,
         mut fargs: Vec<Expr>,
-        assign_to: Place,
+        assign_to: &Place,
         _target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
@@ -354,7 +354,7 @@ impl GotocHook for UntrackedDeref {
             vec![Stmt::assign(
                 unwrap_or_return_codegen_unimplemented_stmt!(
                     gcx,
-                    gcx.codegen_place_stable(&assign_to)
+                    gcx.codegen_place_stable(assign_to)
                 )
                 .goto_expr,
                 fargs.pop().unwrap().dereference(),
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
index a6204ad2a57f..c30d1539bda2 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/debug.rs
@@ -5,10 +5,9 @@
 
 use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::goto_program::Location;
-use rustc_middle::mir::Body;
-use rustc_middle::ty::print::with_no_trimmed_paths;
-use rustc_middle::ty::Instance;
-use rustc_span::def_id::DefId;
+use stable_mir::mir::mono::Instance;
+use stable_mir::mir::Body;
+use stable_mir::CrateDef;
 use std::cell::RefCell;
 use std::panic;
 use std::sync::LazyLock;
@@ -56,37 +55,32 @@ static DEFAULT_HOOK: LazyLock<Box<dyn Fn(&panic::PanicInfo<'_>) + Sync + Send +
 impl<'tcx> GotocCtx<'tcx> {
     // Calls the closure while updating the tracked global variable marking the
     // codegen item for panic debugging.
-    pub fn call_with_panic_debug_info<F: FnOnce(&mut GotocCtx<'tcx>)>(
+    pub fn call_with_panic_debug_info<D: CrateDef, F: FnOnce(&mut GotocCtx<'tcx>)>(
         &mut self,
         call: F,
         panic_debug: String,
-        def_id: DefId,
+        def: D,
     ) {
         CURRENT_CODEGEN_ITEM.with(|odb_cell| {
-            odb_cell
-                .replace((Some(panic_debug), Some(self.codegen_span(&self.tcx.def_span(def_id)))));
+            odb_cell.replace((Some(panic_debug), Some(self.codegen_span_stable(def.span()))));
             call(self);
             odb_cell.replace((None, None));
         });
     }
 
-    pub fn print_instance(&self, instance: Instance<'_>, mir: &'tcx Body<'tcx>) {
+    pub fn print_instance(&self, instance: Instance, body: &Body) {
         if cfg!(debug_assertions) {
-            debug!(
-                "handling {}, {}",
-                instance,
-                with_no_trimmed_paths!(self.tcx.def_path_str(instance.def_id()))
-            );
+            debug!("handling {}", instance.name(),);
             debug!("variables: ");
-            for l in mir.args_iter().chain(mir.vars_and_temps_iter()) {
-                debug!("let {:?}: {:?}", l, self.local_ty(l));
+            for (idx, decl) in body.locals().iter().enumerate() {
+                debug!("let _{idx}: {:?}", decl.ty);
             }
-            for (bb, bbd) in mir.basic_blocks.iter_enumerated() {
+            for (bb, bbd) in body.blocks.iter().enumerate() {
                 debug!("block {:?}", bb);
                 for stmt in &bbd.statements {
                     debug!("{:?}", stmt);
                 }
-                debug!("{:?}", bbd.terminator().kind);
+                debug!("{:?}", bbd.terminator.kind);
             }
         }
     }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
index 587eef72a645..1b6d3da65cbd 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
@@ -7,10 +7,10 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use cbmc::InternedString;
 use rustc_hir::def_id::LOCAL_CRATE;
 use rustc_middle::mir::mono::CodegenUnitNameBuilder;
-use rustc_middle::mir::Local;
 use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::{Instance, TyCtxt};
 use stable_mir::mir::mono::Instance as InstanceStable;
+use stable_mir::mir::Local;
 use tracing::debug;
 
 impl<'tcx> GotocCtx<'tcx> {
@@ -20,22 +20,22 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn codegen_var_base_name(&self, l: &Local) -> String {
-        match self.find_debug_info(l) {
-            None => format!("var_{}", l.index()),
-            Some(info) => info.name,
+        match self.current_fn().local_name(*l) {
+            None => format!("var_{l}"),
+            Some(name) => name.to_string(),
         }
     }
 
     pub fn codegen_var_name(&self, l: &Local) -> String {
         let fname = self.current_fn().name();
-        match self.find_debug_info(l) {
-            Some(info) => format!("{fname}::1::var{l:?}::{}", info.name),
-            None => format!("{fname}::1::var{l:?}"),
+        match self.current_fn().local_name(*l) {
+            Some(name) => format!("{fname}::1::var_{l}::{name}"),
+            None => format!("{fname}::1::var_{l}"),
         }
     }
 
     pub fn is_user_variable(&self, var: &Local) -> bool {
-        self.find_debug_info(var).is_some()
+        self.current_fn().local_name(*var).is_some()
     }
 
     // Special naming conventions for parameters that are spread from a tuple
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 0aec0c448219..c63b8303de17 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -231,6 +231,8 @@ impl SourceLocation {
 }
 
 /// Get the FnAbi of a given instance with no extra variadic arguments.
+/// TODO: Get rid of this. Use instance.fn_sig() instead.
+/// <https://github.com/model-checking/kani/issues/1365>
 pub fn fn_abi<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> &'tcx FnAbi<'tcx, Ty<'tcx>> {
     let helper = CompilerHelpers { tcx };
     helper.fn_abi_of_instance(instance, ty::List::empty())
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index 5c17a2e4df62..b4d1d71ec9f8 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-15"
+channel = "nightly-2023-12-16"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]