From a82bad4a9cb46c5c008a25f8b6281532565de148 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 6 Feb 2024 11:30:05 -0800 Subject: [PATCH] Fix ICEs due to mismatched arguments (#2994) Use FnAbi instead of function signature when generating code for function types. Properly check the `PassMode::Ignore`. For foreign functions, instead of ignoring the declaration type, cast the arguments and return value. For now, we also ignore the caller location, since we don't currently support tracking caller location. This change makes it easier for us to do so. We might want to wait for this issue to get fixed so we can easily add support using stable APIs: https://github.com/rust-lang/project-stable-mir/issues/62 Resolves #2260 Resolves #2312 Resolves #1365 Resolves #1350 --- cprover_bindings/src/goto_program/expr.rs | 5 +- .../codegen/foreign_function.rs | 57 +++- .../codegen_cprover_gotoc/codegen/function.rs | 2 +- .../codegen_cprover_gotoc/codegen/operand.rs | 16 +- .../codegen/statement.rs | 18 +- .../codegen/ty_stable.rs | 8 - .../src/codegen_cprover_gotoc/codegen/typ.rs | 265 ++++-------------- .../context/current_fn.rs | 10 - tests/kani/FunctionCall/marker_tuple.rs | 13 + tests/kani/FunctionCall/type_check.rs | 31 ++ 10 files changed, 164 insertions(+), 261 deletions(-) create mode 100644 tests/kani/FunctionCall/marker_tuple.rs create mode 100644 tests/kani/FunctionCall/type_check.rs 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::()); +}