diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index b6ad7a041d11..09adbdb20df3 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -508,13 +508,13 @@ impl Expr { /// `(typ) self`. pub fn cast_to(self, typ: Type) -> Self { - assert!(self.can_cast_to(&typ), "Can't cast\n\n{self:?} ({:?})\n\n{typ:?}", self.typ); if self.typ == typ { self } else if typ.is_bool() { let zero = self.typ.zero(); self.neq(zero) } else { + assert!(self.can_cast_to(&typ), "Can't cast\n\n{self:?} ({:?})\n\n{typ:?}", self.typ); expr!(Typecast(self), typ) } } @@ -688,7 +688,8 @@ impl Expr { pub fn call(self, arguments: Vec) -> Self { assert!( Expr::typecheck_call(&self, &arguments), - "Function call does not type check:\nfunc: {self:?}\nargs: {arguments:?}" + "Function call does not type check:\nfunc params: {:?}\nargs: {arguments:?}", + self.typ().parameters().unwrap_or(&vec![]) ); let typ = self.typ().return_type().unwrap().clone(); expr!(FunctionCall { function: self, arguments }, typ) 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 2eb1610ab4d8..4ab72eb3a705 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/foreign_function.rs @@ -11,13 +11,14 @@ use std::collections::HashSet; use crate::codegen_cprover_gotoc::codegen::PropertyClass; use crate::codegen_cprover_gotoc::GotocCtx; -use crate::kani_middle; +use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type}; use cbmc::{InternString, InternedString}; use lazy_static::lazy_static; -use rustc_smir::rustc_internal; -use rustc_target::abi::call::Conv; +use stable_mir::abi::{CallConvention, PassMode}; use stable_mir::mir::mono::Instance; +use stable_mir::mir::Place; +use stable_mir::ty::{RigidTy, TyKind}; use stable_mir::CrateDef; use tracing::{debug, trace}; @@ -48,14 +49,12 @@ impl<'tcx> GotocCtx<'tcx> { /// handled later. pub fn codegen_foreign_fn(&mut self, instance: Instance) -> &Symbol { debug!(?instance, "codegen_foreign_function"); - let instance_internal = rustc_internal::internal(instance); let fn_name = self.symbol_name_stable(instance).intern(); if self.symbol_table.contains(fn_name) { // Symbol has been added (either a built-in CBMC function or a Rust allocation function). self.symbol_table.lookup(fn_name).unwrap() } else if RUST_ALLOC_FNS.contains(&fn_name) - || (self.is_cffi_enabled() - && kani_middle::fn_abi(self.tcx, instance_internal).conv == Conv::C) + || (self.is_cffi_enabled() && instance.fn_abi().unwrap().conv == CallConvention::C) { // Add a Rust alloc lib function as is declared by core. // When C-FFI feature is enabled, we just trust the rust declaration. @@ -84,6 +83,40 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Generate a function call to a foreign function by potentially casting arguments and return value, since + /// the external function definition may not match exactly its Rust declaration. + /// See for more details. + pub fn codegen_foreign_call( + &mut self, + fn_expr: Expr, + args: Vec, + ret_place: &Place, + loc: Location, + ) -> Stmt { + let expected_args = fn_expr + .typ() + .parameters() + .unwrap() + .iter() + .zip(args) + .map(|(param, arg)| arg.cast_to(param.typ().clone())) + .collect::>(); + let call_expr = fn_expr.call(expected_args); + + let ret_kind = self.place_ty_stable(ret_place).kind(); + if ret_kind.is_unit() || matches!(ret_kind, TyKind::RigidTy(RigidTy::Never)) { + call_expr.as_stmt(loc) + } else { + let ret_expr = unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place_stable(ret_place) + ) + .goto_expr; + let ret_type = ret_expr.typ().clone(); + ret_expr.assign(call_expr.cast_to(ret_type), loc) + } + } + /// Checks whether C-FFI has been enabled or not. /// When enabled, we blindly encode the function type as is. fn is_cffi_enabled(&self) -> bool { @@ -102,24 +135,24 @@ impl<'tcx> GotocCtx<'tcx> { /// Generate type for the given foreign instance. fn codegen_ffi_type(&mut self, instance: Instance) -> Type { let fn_name = self.symbol_name_stable(instance); - let fn_abi = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance)); + let fn_abi = instance.fn_abi().unwrap(); let loc = self.codegen_span_stable(instance.def.span()); let params = fn_abi .args .iter() .enumerate() - .filter(|&(_, arg)| (!arg.is_ignore())) + .filter(|&(_, arg)| (arg.mode != PassMode::Ignore)) .map(|(idx, arg)| { let arg_name = format!("{fn_name}::param_{idx}"); let base_name = format!("param_{idx}"); - let arg_type = self.codegen_ty(arg.layout.ty); + let arg_type = self.codegen_ty_stable(arg.ty); let sym = Symbol::variable(&arg_name, &base_name, arg_type.clone(), loc) .with_is_parameter(true); self.symbol_table.insert(sym); arg_type.as_parameter(Some(arg_name.into()), Some(base_name.into())) }) .collect(); - let ret_type = self.codegen_ty(fn_abi.ret.layout.ty); + let ret_type = self.codegen_ty_stable(fn_abi.ret.ty); if fn_abi.c_variadic { Type::variadic_code(params, ret_type) @@ -140,9 +173,9 @@ impl<'tcx> GotocCtx<'tcx> { let entry = self.unsupported_constructs.entry("foreign function".into()).or_default(); entry.push(loc); - let call_conv = kani_middle::fn_abi(self.tcx, rustc_internal::internal(instance)).conv; + let call_conv = instance.fn_abi().unwrap().conv; let msg = format!("call to foreign \"{call_conv:?}\" function `{fn_name}`"); - let url = if call_conv == Conv::C { + let url = if call_conv == CallConvention::C { "https://github.com/model-checking/kani/issues/2423" } else { "https://github.com/model-checking/kani/issues/new/choose" diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 52bf778ab235..d4061d4271db 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -210,7 +210,7 @@ impl<'tcx> GotocCtx<'tcx> { self.ensure(&self.symbol_name_stable(instance), |ctx, fname| { Symbol::function( fname, - ctx.fn_typ(&body), + ctx.fn_typ(instance, &body), None, instance.name(), ctx.codegen_span_stable(instance.def.span()), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index aaec506edf6e..517609bb0b4c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -574,13 +574,7 @@ impl<'tcx> GotocCtx<'tcx> { } /// Ensure that the given instance is in the symbol table, returning the symbol. - /// - /// FIXME: The function should not have to return the type of the function symbol as well - /// because the symbol should have the type. The problem is that the type in the symbol table - /// sometimes subtly differs from the type that codegen_function_sig returns. - /// This is tracked in . - fn codegen_func_symbol(&mut self, instance: Instance) -> (&Symbol, Type) { - let funct = self.codegen_function_sig_stable(self.fn_sig_of_instance_stable(instance)); + fn codegen_func_symbol(&mut self, instance: Instance) -> &Symbol { let sym = if instance.is_foreign_item() { // Get the symbol that represents a foreign instance. self.codegen_foreign_fn(instance) @@ -592,7 +586,7 @@ impl<'tcx> GotocCtx<'tcx> { .lookup(&func) .unwrap_or_else(|| panic!("Function `{func}` should've been declared before usage")) }; - (sym, funct) + sym } /// Generate a goto expression that references the function identified by `instance`. @@ -601,8 +595,8 @@ impl<'tcx> GotocCtx<'tcx> { /// /// This should not be used where Rust expects a "function item" (See `codegen_fn_item`) pub fn codegen_func_expr(&mut self, instance: Instance, span: Option) -> Expr { - let (func_symbol, func_typ) = self.codegen_func_symbol(instance); - Expr::symbol_expression(func_symbol.name, func_typ) + let func_symbol = self.codegen_func_symbol(instance); + Expr::symbol_expression(func_symbol.name, func_symbol.typ.clone()) .with_location(self.codegen_span_option_stable(span)) } @@ -612,7 +606,7 @@ impl<'tcx> GotocCtx<'tcx> { /// This is the Rust "function item". See /// This is not the function pointer, for that use `codegen_func_expr`. fn codegen_fn_item(&mut self, instance: Instance, span: Option) -> Expr { - let (func_symbol, _) = self.codegen_func_symbol(instance); + let func_symbol = self.codegen_func_symbol(instance); let mangled_name = func_symbol.name; let fn_item_struct_ty = self.codegen_fndef_type_stable(instance); // This zero-sized object that a function name refers to in Rust is globally unique, so we create such a global object. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index e7b7ee5a376a..3a62a3f91d1a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -135,7 +135,7 @@ impl<'tcx> GotocCtx<'tcx> { "https://github.com/model-checking/kani/issues/692", ), TerminatorKind::Return => { - let rty = self.current_fn().sig().output(); + let rty = self.current_fn().instance_stable().fn_abi().unwrap().ret.ty; if rty.kind().is_unit() { self.codegen_ret_unit() } else { @@ -145,7 +145,8 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_place_stable(&place) ) .goto_expr; - if self.place_ty_stable(&place).kind().is_bool() { + assert_eq!(rty, self.place_ty_stable(&place), "Unexpected return type"); + if rty.kind().is_bool() { place_expr.cast_to(Type::c_bool()).ret(loc) } else { place_expr.ret(loc) @@ -555,10 +556,17 @@ impl<'tcx> GotocCtx<'tcx> { // 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(instance, None); - vec![ - self.codegen_expr_to_place_stable(destination, func_exp.call(fargs)) + if instance.is_foreign_item() { + vec![self.codegen_foreign_call(func_exp, fargs, destination, loc)] + } else { + vec![ + self.codegen_expr_to_place_stable( + destination, + func_exp.call(fargs), + ) .with_location(loc), - ] + ] + } } }; stmts.push(self.codegen_end_call(*target, loc)); 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 2213676d5a63..c4f03e6c2cef 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/ty_stable.rs @@ -9,7 +9,6 @@ use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::Type; use rustc_middle::ty::layout::{LayoutOf, TyAndLayout}; -use rustc_middle::ty::{self}; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::{Local, Operand, Place, Rvalue}; @@ -53,13 +52,6 @@ impl<'tcx> GotocCtx<'tcx> { ) } - 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 { self.use_fat_pointer(rustc_internal::internal(pointer_ty)) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 7694feb0dbbf..83ec6c3374ae 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -6,7 +6,6 @@ use cbmc::goto_program::{DatatypeComponent, Expr, Location, Parameter, Symbol, S use cbmc::utils::aggr_tag; use cbmc::{InternString, InternedString}; use rustc_ast::ast::Mutability; -use rustc_hir::{LangItem, Unsafety}; use rustc_index::IndexVec; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::print::with_no_trimmed_paths; @@ -24,8 +23,9 @@ use rustc_target::abi::{ TyAndLayout, VariantIdx, Variants, }; use rustc_target::spec::abi::Abi; +use stable_mir::abi::{ArgAbi, FnAbi, PassMode}; +use stable_mir::mir::mono::Instance as InstanceStable; use stable_mir::mir::Body; -use std::iter; use tracing::{debug, trace, warn}; /// Map the unit type to an empty struct @@ -256,169 +256,6 @@ impl<'tcx> GotocCtx<'tcx> { debug_write_type(self, ty, &mut out, 0).unwrap(); out } - - /// Function shims and closures expect their last arg untupled at call site, see comment at - /// ty_needs_untupled_args. - fn sig_with_untupled_args(&self, sig: ty::PolyFnSig<'tcx>) -> ty::PolyFnSig<'tcx> { - debug!("sig_with_closure_untupled sig: {:?}", sig); - let fn_sig = sig.skip_binder(); - if let Some((tupe, prev_args)) = fn_sig.inputs().split_last() { - let args = match *tupe.kind() { - ty::Tuple(args) => args, - _ => unreachable!("the final argument of a closure must be a tuple"), - }; - - // The leading argument should be exactly the environment - assert!(prev_args.len() == 1); - let env = prev_args[0]; - - // Recombine arguments: environment first, then the flattened tuple elements - let recombined_args = iter::once(env).chain(args); - - return ty::Binder::bind_with_vars( - self.tcx.mk_fn_sig( - recombined_args, - fn_sig.output(), - fn_sig.c_variadic, - fn_sig.unsafety, - fn_sig.abi, - ), - sig.bound_vars(), - ); - } - sig - } - - fn closure_sig(&self, def_id: DefId, args: ty::GenericArgsRef<'tcx>) -> ty::PolyFnSig<'tcx> { - let sig = self.monomorphize(args.as_closure().sig()); - - // In addition to `def_id` and `args`, we need to provide the kind of region `env_region` - // in `closure_env_ty`, which we can build from the bound variables as follows - let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter( - sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))), - ); - let br = ty::BoundRegion { - var: ty::BoundVar::from_usize(bound_vars.len() - 1), - kind: ty::BoundRegionKind::BrEnv, - }; - let env_region = ty::Region::new_bound(self.tcx, ty::INNERMOST, br); - let env_ty = self.tcx.closure_env_ty( - Ty::new_closure(self.tcx, def_id, args), - args.as_closure().kind(), - env_region, - ); - - let sig = sig.skip_binder(); - - // We build a binder from `sig` where: - // * `inputs` contains a sequence with the closure and parameter types - // * the rest of attributes are obtained from `sig` - let sig = ty::Binder::bind_with_vars( - self.tcx.mk_fn_sig( - [env_ty, sig.inputs()[0]], - sig.output(), - sig.c_variadic, - sig.unsafety, - sig.abi, - ), - bound_vars, - ); - - // The parameter types are tupled, but we want to have them in a vector - self.sig_with_untupled_args(sig) - } - - // Adapted from `fn_sig_for_fn_abi` in - // https://github.com/rust-lang/rust/blob/739d68a76e35b22341d9930bb6338bf202ba05ba/compiler/rustc_ty_utils/src/abi.rs#L88 - // Code duplication tracked here: https://github.com/model-checking/kani/issues/1365 - fn coroutine_sig( - &self, - did: &DefId, - ty: Ty<'tcx>, - args: ty::GenericArgsRef<'tcx>, - ) -> ty::PolyFnSig<'tcx> { - let sig = args.as_coroutine().sig(); - - let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(iter::once( - ty::BoundVariableKind::Region(ty::BrEnv), - )); - let br = ty::BoundRegion { - var: ty::BoundVar::from_usize(bound_vars.len() - 1), - kind: ty::BoundRegionKind::BrEnv, - }; - let env_region = ty::ReBound(ty::INNERMOST, br); - let env_ty = Ty::new_mut_ref(self.tcx, ty::Region::new_from_kind(self.tcx, env_region), ty); - - let pin_did = self.tcx.require_lang_item(LangItem::Pin, None); - let pin_adt_ref = self.tcx.adt_def(pin_did); - let pin_args = self.tcx.mk_args(&[env_ty.into()]); - let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_args); - - // The `FnSig` and the `ret_ty` here is for a coroutines main - // `coroutine::resume(...) -> CoroutineState` function in case we - // have an ordinary coroutine, or the `Future::poll(...) -> Poll` - // function in case this is a special coroutine backing an async construct. - let tcx = self.tcx; - let (resume_ty, ret_ty) = if tcx.coroutine_is_async(*did) { - // The signature should be `Future::poll(_, &mut Context<'_>) -> Poll` - let poll_did = tcx.require_lang_item(LangItem::Poll, None); - let poll_adt_ref = tcx.adt_def(poll_did); - let poll_args = tcx.mk_args(&[sig.return_ty.into()]); - // TODO figure out where this one went - let ret_ty = Ty::new_adt(tcx, poll_adt_ref, poll_args); - - // We have to replace the `ResumeTy` that is used for type and borrow checking - // with `&mut Context<'_>` which is used in codegen. - #[cfg(debug_assertions)] - { - if let ty::Adt(resume_ty_adt, _) = sig.resume_ty.kind() { - let expected_adt = tcx.adt_def(tcx.require_lang_item(LangItem::ResumeTy, None)); - assert_eq!(*resume_ty_adt, expected_adt); - } else { - panic!("expected `ResumeTy`, found `{:?}`", sig.resume_ty); - }; - } - let context_mut_ref = Ty::new_task_context(tcx); - - (context_mut_ref, ret_ty) - } else { - // The signature should be `Coroutine::resume(_, Resume) -> CoroutineState` - let state_did = tcx.require_lang_item(LangItem::CoroutineState, None); - let state_adt_ref = tcx.adt_def(state_did); - let state_args = tcx.mk_args(&[sig.yield_ty.into(), sig.return_ty.into()]); - let ret_ty = Ty::new_adt(tcx, state_adt_ref, state_args); - - (sig.resume_ty, ret_ty) - }; - - ty::Binder::bind_with_vars( - tcx.mk_fn_sig( - [env_ty, resume_ty], - ret_ty, - false, - Unsafety::Normal, - rustc_target::spec::abi::Abi::Rust, - ), - bound_vars, - ) - } - - pub fn fn_sig_of_instance(&self, instance: Instance<'tcx>) -> ty::PolyFnSig<'tcx> { - let fntyp = instance.ty(self.tcx, ty::ParamEnv::reveal_all()); - self.monomorphize(match fntyp.kind() { - ty::Closure(def_id, subst) => self.closure_sig(*def_id, subst), - ty::FnPtr(..) | ty::FnDef(..) => { - let sig = fntyp.fn_sig(self.tcx); - // Calls through vtable or Fn pointer for an ABI that may require untupled arguments. - if self.ty_needs_untupled_args(fntyp) { - return self.sig_with_untupled_args(sig); - } - sig - } - ty::Coroutine(did, args) => self.coroutine_sig(did, fntyp, args), - _ => unreachable!("Can't get function signature of type: {:?}", fntyp), - }) - } } impl<'tcx> GotocCtx<'tcx> { @@ -463,10 +300,10 @@ impl<'tcx> GotocCtx<'tcx> { idx: usize, ) -> DatatypeComponent { // Gives a binder with function signature - let sig = self.fn_sig_of_instance(instance); + let instance = rustc_internal::stable(instance); // Gives an Irep Pointer object for the signature - let fn_ty = self.codegen_dynamic_function_sig(sig); + let fn_ty = self.codegen_dynamic_function_sig(instance); let fn_ptr = fn_ty.to_pointer(); // vtable field name, i.e., 3_vol (idx_method) @@ -1256,36 +1093,37 @@ impl<'tcx> GotocCtx<'tcx> { /// `S = P | Pin

` /// /// See for more details. - fn codegen_dynamic_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); + fn codegen_dynamic_function_sig(&mut self, instance: InstanceStable) -> Type { let mut is_first = true; - let params = sig - .inputs() - .iter() - .map(|arg_type| { + let fn_abi = instance.fn_abi().unwrap(); + let args = self.codegen_args(instance, &fn_abi); + let params = args + .map(|(_, arg_abi)| { + let arg_ty_stable = arg_abi.ty; + let kind = arg_ty_stable.kind(); + let arg_ty = rustc_internal::internal(arg_ty_stable); if is_first { is_first = false; - debug!(self_type=?arg_type, fn_signature=?sig, "codegen_dynamic_function_sig"); - if arg_type.is_ref() { + debug!(self_type=?arg_ty, ?fn_abi, "codegen_dynamic_function_sig"); + if kind.is_ref() { // Convert fat pointer to thin pointer to data portion. - let first_ty = pointee_type(*arg_type).unwrap(); + let first_ty = pointee_type(arg_ty).unwrap(); self.codegen_trait_data_pointer(first_ty) - } else if arg_type.is_trait() { + } else if kind.is_trait() { // Convert dyn T to thin pointer. - self.codegen_trait_data_pointer(*arg_type) + self.codegen_trait_data_pointer(arg_ty) } else { // Codegen type with thin pointer (E.g.: Box -> Box). - self.codegen_trait_receiver(*arg_type) + self.codegen_trait_receiver(arg_ty) } } else { - debug!("Using type {:?} in function signature", arg_type); - self.codegen_ty(*arg_type) + debug!("Using type {:?} in function signature", arg_ty); + self.codegen_ty(arg_ty) } }) .collect(); - Type::code_with_unnamed_parameters(params, self.codegen_ty(sig.output())) + Type::code_with_unnamed_parameters(params, self.codegen_ty_stable(fn_abi.ret.ty)) } /// one can only apply this function to a monomorphized signature @@ -1660,18 +1498,14 @@ impl<'tcx> GotocCtx<'tcx> { } /// the function type of the current instance - 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 = sig - .inputs() - .iter() - .enumerate() - .filter_map(|(i, ty)| { - debug!(?i, ?ty, "fn_typ"); - let is_vtable_shim_self = i == 0 && is_vtable_shim; - if self.is_zst_stable(*ty) && !is_vtable_shim_self { + pub fn fn_typ(&mut self, instance: InstanceStable, body: &Body) -> Type { + let fn_abi = instance.fn_abi().unwrap(); + let params: Vec = self + .codegen_args(instance, &fn_abi) + .filter_map(|(i, arg_abi)| { + let ty = arg_abi.ty; + debug!(?i, ?arg_abi, "fn_typ"); + if arg_abi.mode == PassMode::Ignore { // We ignore zero-sized parameters. // See https://github.com/model-checking/kani/issues/274 for more details. None @@ -1692,30 +1526,19 @@ impl<'tcx> GotocCtx<'tcx> { } } Some( - self.codegen_ty_stable(*ty) + self.codegen_ty_stable(ty) .as_parameter(Some(ident.clone().into()), Some(ident.into())), ) } }) .collect(); - // For vtable shims, we need to modify fn(self, ...) to fn(self: *mut Self, ...), - // since the vtable functions expect a pointer as the first argument. See the comment - // and similar code in compiler/rustc_mir/src/shim.rs. - // TODO(celina): Use fn_abi_of_instance instead of sig so we don't need to do this manually. - if is_vtable_shim { - if let Some(self_param) = params.first() { - let ident = self_param.identifier(); - let ty = self_param.typ().clone(); - params[0] = ty.to_pointer().as_parameter(ident, ident); - } - } - - debug!(?params, signature=?sig, "function_type"); - if sig.c_variadic { - Type::variadic_code(params, self.codegen_ty_stable(sig.output())) + debug!(?params, ?fn_abi, "function_type"); + let ret_type = self.codegen_ty_stable(fn_abi.ret.ty); + if fn_abi.c_variadic { + Type::variadic_code(params, ret_type) } else { - Type::code(params, self.codegen_ty_stable(sig.output())) + Type::code(params, ret_type) } } @@ -1852,6 +1675,24 @@ impl<'tcx> GotocCtx<'tcx> { ReceiverIter { ctx: self, curr: typ } } + + /// Allow us to retrieve the instance arguments in a consistent way. + /// There are two corner cases that we currently handle: + /// 1. In some cases, an argument can be ignored (e.g.: ZST arguments in regular Rust calls). + /// 2. We currently don't support `track_caller`, so we ignore the extra argument that is added to support that. + /// Tracked here: + fn codegen_args<'a>( + &self, + instance: InstanceStable, + fn_abi: &'a FnAbi, + ) -> impl Iterator { + let instance_internal = rustc_internal::internal(instance); + let requires_caller_location = instance_internal.def.requires_caller_location(self.tcx); + let num_args = fn_abi.args.len(); + fn_abi.args.iter().enumerate().filter(move |(idx, arg_abi)| { + arg_abi.mode != PassMode::Ignore && !(requires_caller_location && idx + 1 == num_args) + }) + } } /// Return the datatype components for fields are present in every vtable struct. 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 e73a4756a581..b8251b153e5a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs @@ -9,7 +9,6 @@ use rustc_middle::ty::Instance as InternalInstance; use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; use stable_mir::mir::{Body, Local, LocalDecl}; -use stable_mir::ty::FnSig; use stable_mir::CrateDef; use std::collections::HashMap; @@ -20,8 +19,6 @@ pub struct CurrentFnCtx<'tcx> { block: Vec, /// 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. @@ -51,11 +48,9 @@ impl<'tcx> CurrentFnCtx<'tcx> { .iter() .filter_map(|info| info.local().map(|local| (local, (&info.name).into()))) .collect::>(); - 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, locals, @@ -111,11 +106,6 @@ impl<'tcx> CurrentFnCtx<'tcx> { &self.readable_name } - /// The signature of the function we are currently compiling - pub fn sig(&self) -> &FnSig { - &self.fn_sig - } - pub fn locals(&self) -> &[LocalDecl] { &self.locals } diff --git a/tests/kani/FunctionCall/marker_tuple.rs b/tests/kani/FunctionCall/marker_tuple.rs new file mode 100644 index 000000000000..ec8b98a9d640 --- /dev/null +++ b/tests/kani/FunctionCall/marker_tuple.rs @@ -0,0 +1,13 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Test that Kani can properly handle the "rust-call" ABI with an empty tuple. +//! Issue first reported here: + +#![feature(unboxed_closures, tuple_trait)] + +extern "rust-call" fn foo(_: T) {} + +#[kani::proof] +fn main() { + foo(()); +} diff --git a/tests/kani/FunctionCall/type_check.rs b/tests/kani/FunctionCall/type_check.rs new file mode 100644 index 000000000000..6694cabdbb94 --- /dev/null +++ b/tests/kani/FunctionCall/type_check.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Test that Kani can properly handle the ABI of virtual calls with ZST arguments. +//! Issue first reported here: +use std::any::TypeId; +use std::error::Error; +use std::fmt::{Debug, Display, Formatter}; + +struct MyError; + +impl Debug for MyError { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + todo!() + } +} + +impl Display for MyError { + fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result { + todo!() + } +} + +impl Error for MyError {} + +#[kani::proof] +fn is_same_error() { + let e = MyError; + let d = &e as &(dyn Error); + assert!(d.is::()); + assert!(!d.is::()); +}