Migrate function declaration

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");
 

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

@@ -7,68 +7,52 @@ 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;
 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) {
-        self.set_current_fn(instance);
         let name = self.symbol_name_stable(instance);
         let old_sym = self.symbol_table.lookup(&name).unwrap();
 
@@ -77,11 +61,11 @@ impl<'tcx> GotocCtx<'tcx> {
             debug!("Double codegen of {:?}", old_sym);
         } else {
             assert!(old_sym.is_function());
-            // TODO: Remove this clone.
-            let body = self.current_fn().body().clone();
+            let body = instance.body().unwrap();
+            self.set_current_fn(instance, &body);
             self.print_instance(instance, &body);
-            self.codegen_function_prelude();
-            self.codegen_declare_variables();
+            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();
@@ -92,16 +76,16 @@ impl<'tcx> GotocCtx<'tcx> {
             let stmts = self.current_fn_mut().extract_block();
             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);
         }
     }
 
@@ -122,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.
@@ -171,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
@@ -190,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.
@@ -229,12 +204,13 @@ impl<'tcx> GotocCtx<'tcx> {
 
     pub fn declare_function(&mut self, instance: Instance) {
         debug!("declaring {}; {:?}", instance.name(), instance);
-        self.set_current_fn(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,
                 instance.name(),
                 ctx.codegen_span_stable(instance.def.span()),

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)
             }

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

@@ -566,7 +566,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)

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

@@ -12,7 +12,6 @@ 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;
 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))
     }
 

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,13 +42,4 @@ impl<'tcx> GotocCtx<'tcx> {
         let topmost = span.ctxt().outer_expn().expansion_cause().unwrap_or(*span);
         self.codegen_span(&topmost)
     }
-
-    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,
-            },
-        ))
-    }
 }

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

@@ -135,8 +135,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 "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(RETURN_LOCAL);
@@ -177,7 +177,8 @@ impl<'tcx> GotocCtx<'tcx> {
                 } 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().unwrap()