diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 77d68af745ae..f3d79c7f06c5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/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(), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 90adafb04fbb..78b9a7d49c28 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/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, ) -> 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(), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 9392a2bba556..5056d9d006ad 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/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` 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 diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs index 33f5bafd44de..70b00357d264 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/span.rs +++ b/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 { - 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, - } - })) + }, + )) } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index aec9d8143818..7d63c021c828 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/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; 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 1f1b8c08f2ff..e39d44743c5f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs +++ b/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 }