Address PR comments

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

@@ -28,7 +28,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// - 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().mir();
+        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)| {
@@ -76,7 +76,7 @@ impl<'tcx> GotocCtx<'tcx> {
             debug!("Double codegen of {:?}", old_sym);
         } else {
             assert!(old_sym.is_function());
-            let mir = self.current_fn().mir();
+            let mir = self.current_fn().body_internal();
             self.print_instance(instance, mir);
             self.codegen_function_prelude();
             self.codegen_declare_variables();
@@ -94,7 +94,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// 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().mir();
+        let mir = self.current_fn().body_internal();
         if let Some(spread_arg) = mir.spread_arg {
             self.codegen_spread_arg(mir, spread_arg);
         }
@@ -228,7 +228,7 @@ impl<'tcx> GotocCtx<'tcx> {
         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().mir();
+            let mir = ctx.current_fn().body_internal();
             Symbol::function(
                 fname,
                 ctx.fn_typ(),

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

@@ -16,6 +16,7 @@ use rustc_span::Span;
 use rustc_target::abi::{Size, TagEncoding, Variants};
 use stable_mir::mir::mono::Instance as InstanceStable;
 use stable_mir::ty::{FnDef, GenericArgs, Span as SpanStable};
+use stable_mir::CrateDef;
 use tracing::{debug, trace};
 
 enum AllocData<'a> {
@@ -709,7 +710,8 @@ impl<'tcx> GotocCtx<'tcx> {
         args: &GenericArgs,
         span: Option<SpanStable>,
     ) -> Expr {
-        let instance = InstanceStable::resolve(def, args).unwrap();
+        let instance = InstanceStable::resolve(def, args)
+            .expect(&format!("Failed to instantiate `{}` with `{args:?}`", def.name()));
         self.codegen_fn_item(
             rustc_internal::internal(instance),
             rustc_internal::internal(span).as_ref(),

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

@@ -340,15 +340,15 @@ impl<'tcx> GotocCtx<'tcx> {
     ///
     /// Since the goto representation for both is the same, we use the expected type to decide
     /// what to return.
-    fn codegen_simd_field(&mut self, parent_expr: Expr, field: FieldIdx, field_ty: Ty) -> Expr {
+    fn codegen_simd_field(&mut self, parent_expr: Expr, field_idx: FieldIdx, field_ty: Ty) -> Expr {
         if matches!(field_ty.kind(), TyKind::RigidTy(RigidTy::Array { .. })) {
             // Array based
-            assert_eq!(field, 0);
+            assert_eq!(field_idx, 0);
             let field_typ = self.codegen_ty_stable(field_ty);
             parent_expr.reinterpret_cast(field_typ)
         } else {
             // Return the given field.
-            let index_expr = Expr::int_constant(field, Type::size_t());
+            let index_expr = Expr::int_constant(field_idx, Type::size_t());
             parent_expr.index_array(index_expr)
         }
     }
@@ -378,7 +378,9 @@ impl<'tcx> GotocCtx<'tcx> {
             // A local can be a boxed function pointer
             TyKind::RigidTy(RigidTy::Adt(def, args)) if def.is_box() => {
                 let boxed_ty = self.codegen_ty_stable(ty);
-                self.codegen_local_fndef(*args.0[0].ty().unwrap())
+                // The type of `T` for `Box<T>` can be derived from the first definition args.
+                let inner_ty = args.0[0].ty().unwrap();
+                self.codegen_local_fndef(*inner_ty)
                     .map(|f| self.box_value(f.address_of(), boxed_ty))
             }
             _ => None,
@@ -603,12 +605,11 @@ impl<'tcx> GotocCtx<'tcx> {
                     Variants::Single { .. } => before.goto_expr,
                     Variants::Multiple { tag_encoding, .. } => match tag_encoding {
                         TagEncoding::Direct => {
-                            let cases =
-                                if matches!(ty_kind, TyKind::RigidTy(RigidTy::Coroutine(..))) {
-                                    before.goto_expr
-                                } else {
-                                    before.goto_expr.member("cases", &self.symbol_table)
-                                };
+                            let cases = if is_coroutine(ty_kind) {
+                                before.goto_expr
+                            } else {
+                                before.goto_expr.member("cases", &self.symbol_table)
+                            };
                             cases.member(case_name, &self.symbol_table)
                         }
                         TagEncoding::Niche { .. } => {
@@ -784,6 +785,10 @@ fn is_box(ty: Ty) -> bool {
     matches!(ty.kind(), TyKind::RigidTy(RigidTy::Adt(def, _)) if def.is_box())
 }
 
+fn is_coroutine(ty_kind: TyKind) -> bool {
+    matches!(ty_kind, TyKind::RigidTy(RigidTy::Coroutine(..)))
+}
+
 /// Extract the data pointer from a projection.
 /// The return type of the projection is not consistent today, so we need to specialize the
 /// behavior in order to get a consistent expression that represents a pointer to the projected

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

@@ -49,11 +49,11 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn find_debug_info(&self, l: &Local) -> Option<VarDebugInfo> {
-        rustc_internal::stable(self.current_fn().mir().var_debug_info.iter().find(|info| {
-            match info.value {
+        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,
-            }
-        }))
+            },
+        ))
     }
 }

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

@@ -437,19 +437,19 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     pub fn local_ty(&self, l: Local) -> Ty<'tcx> {
-        self.monomorphize(self.current_fn().mir().local_decls()[l].ty)
+        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().mir().local_decls(), self.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().mir().local_decls(), self.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().mir().local_decls(), self.tcx).ty)
+        self.monomorphize(p.ty(self.current_fn().body_internal().local_decls(), self.tcx).ty)
     }
 
     /// Is the MIR type a zero-sized type.
@@ -1711,7 +1711,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     // 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().mir().spread_arg {
+                    if let Some(spread) = self.current_fn().body_internal().spread_arg {
                         if lc.index() >= spread.index() {
                             let (name, _) = self.codegen_spread_arg_name(&lc);
                             ident = name;

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

@@ -85,8 +85,8 @@ impl<'tcx> CurrentFnCtx<'tcx> {
         self.krate.to_string()
     }
 
-    /// The MIR for the function we are currently compiling using internal APIs.
-    pub fn mir(&self) -> &'tcx InternalBody<'tcx> {
+    /// The internal MIR for the function we are currently compiling using internal APIs.
+    pub fn body_internal(&self) -> &'tcx InternalBody<'tcx> {
         self.mir
     }