diff --git a/docs/src/rust-feature-support.md b/docs/src/rust-feature-support.md index eebb1def6ccca..d66636dd092d5 100644 --- a/docs/src/rust-feature-support.md +++ b/docs/src/rust-feature-support.md @@ -154,9 +154,7 @@ not formally defined which makes it harder to ensure that we can properly model all their use cases. In particular, there are some outstanding issues to note here: - * Unimplemented `PointerCast::ClosureFnPointer` in - [#274](https://github.com/model-checking/kani/issues/274) and `Variant` case - in projections type in + * Sanity check `Variant` type in projections [#448](https://github.com/model-checking/kani/issues/448). * Unexpected fat pointer results in [#277](https://github.com/model-checking/kani/issues/277), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 43d8537380e23..ced7e00479c84 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -12,7 +12,7 @@ use kani_queries::UserInput; use rustc_ast::Attribute; use rustc_hir::def::DefKind; use rustc_hir::def_id::DefId; -use rustc_middle::mir::{HasLocalDecls, Local}; +use rustc_middle::mir::{Body, HasLocalDecls, Local}; use rustc_middle::ty::layout::FnAbiOf; use rustc_middle::ty::{self, Instance}; use std::collections::BTreeMap; @@ -47,14 +47,19 @@ impl<'tcx> GotocCtx<'tcx> { let base_name = self.codegen_var_base_name(&lc); let name = self.codegen_var_name(&lc); let ldata = &ldecls[lc]; - let t = self.monomorphize(ldata.ty); - let t = self.codegen_ty(t); + let var_ty = self.monomorphize(ldata.ty); + let var_type = self.codegen_ty(var_ty); let loc = self.codegen_span(&ldata.source_info.span); // Indices [1, N] represent the function parameters where N is the number of parameters. - let sym = - Symbol::variable(name, base_name, t, self.codegen_span(&ldata.source_info.span)) - .with_is_hidden(!ldata.is_user_variable()) - .with_is_parameter(idx > 0 && idx <= num_args); + // 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(!ldata.is_user_variable()) + .with_is_parameter((idx > 0 && idx <= num_args) && !self.is_zst(var_ty)); let sym_e = sym.to_expr(); self.symbol_table.insert(sym); @@ -96,29 +101,41 @@ impl<'tcx> GotocCtx<'tcx> { 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().mir(); + if let Some(spread_arg) = mir.spread_arg { + self.codegen_spread_arg(mir, spread_arg); + } + } + /// MIR functions have a `spread_arg` field that specifies whether the /// final argument to the function is "spread" at the LLVM/codegen level /// from a tuple into its individual components. (Used for the "rust- - /// call" ABI, necessary because dynamic trait closure cannot have an + /// call" ABI, necessary because the function traits and closures cannot have an /// argument list in MIR that is both generic and variadic, so Rust /// allows a generic tuple). /// - /// If `spread_arg` is Some, then the wrapped value is the local that is - /// to be "spread"/untupled. However, the MIR function body itself expects - /// the tuple instead of the individual components, so we need to generate - /// a function prelude that _retuples_, that is, writes the components - /// back to the tuple local for use in the body. + /// These tuples are used in the MIR to invoke a shim, and it's used in the shim body. + /// + /// The `spread_arg` represents the the local variable that is to be "spread"/untupled. + /// However, the function body itself may refer to the members of + /// the tuple instead of the individual spread parameters, so we need to add to the + /// function prelude code that _retuples_, that is, writes the arguments + /// back to a local tuple that can be used in the body. /// /// See: /// - fn codegen_function_prelude(&mut self) { - let mir = self.current_fn().mir(); - if mir.spread_arg.is_none() { - // No special tuple argument, no work to be done. + 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) { + // No need to spread a ZST since it will be ignored. return; } - let spread_arg = mir.spread_arg.unwrap(); - let spread_data = &mir.local_decls()[spread_arg]; + let loc = self.codegen_span(&spread_data.source_info.span); // Get the function signature from MIR, _before_ we untuple @@ -159,7 +176,7 @@ impl<'tcx> GotocCtx<'tcx> { // }; // ``` // Note how the compiler has reordered the fields to improve packing. - let tup_typ = self.codegen_ty(self.monomorphize(spread_data.ty)); + let tup_type = self.codegen_ty(tup_ty); // We need to marshall the arguments into the tuple // The arguments themselves have been tacked onto the explicit function paramaters by @@ -192,7 +209,7 @@ impl<'tcx> GotocCtx<'tcx> { let (name, base_name) = self.codegen_spread_arg_name(&lc); let sym = Symbol::variable(name, base_name, self.codegen_ty(arg_t), loc) .with_is_hidden(false) - .with_is_parameter(true); + .with_is_parameter(!self.is_zst(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. @@ -204,12 +221,12 @@ impl<'tcx> GotocCtx<'tcx> { (arg_i.to_string().intern(), sym.to_expr()) })); let marshalled_tuple_value = - Expr::struct_expr(tup_typ.clone(), marshalled_tuple_fields, &self.symbol_table) + Expr::struct_expr(tup_type.clone(), marshalled_tuple_fields, &self.symbol_table) .with_location(loc); self.declare_variable( self.codegen_var_name(&spread_arg), self.codegen_var_base_name(&spread_arg), - tup_typ, + tup_type, Some(marshalled_tuple_value), loc, ); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 34565443dcbc7..910a842e61d08 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -53,7 +53,7 @@ impl<'tcx> GotocCtx<'tcx> { if let Some(target) = target { let loc = self.codegen_span(&span); - let fargs = self.codegen_funcall_args(args); + let fargs = self.codegen_funcall_args(args, false); Stmt::block( vec![ self.codegen_intrinsic(instance, fargs, destination, Some(span)), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 62266b273050b..d06fabd27b0e8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -640,13 +640,13 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_pointer_cast( &mut self, k: &PointerCast, - o: &Operand<'tcx>, + operand: &Operand<'tcx>, t: Ty<'tcx>, loc: Location, ) -> Expr { - debug!(cast=?k, op=?o, ?loc, "codegen_pointer_cast"); + debug!(cast=?k, op=?operand, ?loc, "codegen_pointer_cast"); match k { - PointerCast::ReifyFnPointer => match self.operand_ty(o).kind() { + PointerCast::ReifyFnPointer => match self.operand_ty(operand).kind() { ty::FnDef(def_id, substs) => { let instance = Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, substs) @@ -658,17 +658,23 @@ impl<'tcx> GotocCtx<'tcx> { } _ => unreachable!(), }, - PointerCast::UnsafeFnPointer => self.codegen_operand(o), + PointerCast::UnsafeFnPointer => self.codegen_operand(operand), PointerCast::ClosureFnPointer(_) => { - let dest_typ = self.codegen_ty(t); - self.codegen_unimplemented_expr( - "PointerCast::ClosureFnPointer", - dest_typ, - loc, - "https://github.com/model-checking/kani/issues/274", - ) + if let ty::Closure(def_id, substs) = self.operand_ty(operand).kind() { + let instance = Instance::resolve_closure( + self.tcx, + *def_id, + substs, + ty::ClosureKind::FnOnce, + ) + .expect("failed to normalize and resolve closure during codegen") + .polymorphize(self.tcx); + self.codegen_func_expr(instance, None).address_of() + } else { + unreachable!("{:?} cannot be cast to a fn ptr", operand) + } } - PointerCast::MutToConstPointer => self.codegen_operand(o), + PointerCast::MutToConstPointer => self.codegen_operand(operand), PointerCast::ArrayToPointer => { // TODO: I am not sure whether it is correct or not. // @@ -677,11 +683,11 @@ impl<'tcx> GotocCtx<'tcx> { // if we had to, then [o] necessarily has type [T; n] where *T is a fat pointer, meaning // T is either [T] or str. but neither type is sized, which shouldn't participate in // codegen. - match self.operand_ty(o).kind() { + match self.operand_ty(operand).kind() { ty::RawPtr(ty::TypeAndMut { ty, .. }) => { // ty must be an array if let ty::Array(_, _) = ty.kind() { - let oe = self.codegen_operand(o); + let oe = self.codegen_operand(operand); oe.dereference() // : struct [T; n] .member("0", &self.symbol_table) // : T[n] .array_to_ptr() // : T* @@ -693,8 +699,8 @@ impl<'tcx> GotocCtx<'tcx> { } } PointerCast::Unsize => { - let src_goto_expr = self.codegen_operand(o); - let src_mir_type = self.operand_ty(o); + let src_goto_expr = self.codegen_operand(operand); + let src_mir_type = self.operand_ty(operand); let dst_mir_type = t; self.codegen_unsized_cast(src_goto_expr, src_mir_type, dst_mir_type) } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index d5dc58714d908..ab8d250dbe73d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -33,9 +33,8 @@ impl<'tcx> GotocCtx<'tcx> { StatementKind::Assign(box (l, r)) => { let lty = self.place_ty(l); let rty = self.rvalue_ty(r); - let llayout = self.layout_of(lty); // we ignore assignment for all zero size types - if llayout.is_zst() { + if self.is_zst(lty) { Stmt::skip(location) } else if lty.is_fn_ptr() && rty.is_fn() && !rty.is_fn_ptr() { // implicit address of a function pointer, e.g. @@ -402,10 +401,19 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// As part of **calling** a function (closure actually), we may need to un-tuple arguments. + /// As part of **calling** a function (or closure), we may need to un-tuple arguments. /// - /// See [GotocCtx::ty_needs_closure_untupled] - fn codegen_untuple_closure_args( + /// This function will replace the last `fargs` argument by its un-tupled version. + /// + /// Some context: A closure / shim takes two arguments: + /// 0. a struct (or a pointer to) representing the environment + /// 1. a tuple containing the parameters (if not empty) + /// + /// However, Rust generates a function where the tuple of parameters are flattened + /// as subsequent parameters. + /// + /// See [GotocCtx::ty_needs_untupled_args] for more details. + fn codegen_untupled_args( &mut self, instance: Instance<'tcx>, fargs: &mut Vec, @@ -416,32 +424,22 @@ impl<'tcx> GotocCtx<'tcx> { self.readable_instance_name(instance), fargs ); - // A closure takes two arguments: - // 0. a struct representing the environment - // 1. a tuple containing the parameters - // - // However, for some reason, Rust decides to generate a function which still - // takes the first argument as the environment struct, but the tuple of parameters - // are flattened as subsequent parameters. - // Therefore, we have to project out the corresponding fields when we detect - // an invocation of a closure. - // - // Note: In some cases, the environment struct has type FnDef, so we skip it in - // ignore_var_ty. So the tuple is always the last arg, but it might be in the - // first or the second position. - // Note 2: For empty closures, the only argument needed is the environment struct. if !fargs.is_empty() { + let tuple_ty = self.operand_ty(last_mir_arg.unwrap()); + if self.is_zst(tuple_ty) { + // Don't pass anything if all tuple elements are ZST. + // ZST arguments are ignored. + return; + } let tupe = fargs.remove(fargs.len() - 1); - let tupled_args: Vec = match self.operand_ty(last_mir_arg.unwrap()).kind() { - ty::Tuple(tupled_args) => tupled_args.iter().map(|s| self.codegen_ty(s)).collect(), - _ => unreachable!("Argument to function with Abi::RustCall is not a tuple"), - }; - - // Unwrap as needed - for (i, _) in tupled_args.iter().enumerate() { - // Access the tupled parameters through the `member` operation - let index_param = tupe.clone().member(&i.to_string(), &self.symbol_table); - fargs.push(index_param); + if let ty::Tuple(tupled_args) = tuple_ty.kind() { + for (idx, arg_ty) in tupled_args.iter().enumerate() { + if !self.is_zst(arg_ty) { + // Access the tupled parameters through the `member` operation + let idx_expr = tupe.clone().member(&idx.to_string(), &self.symbol_table); + fargs.push(idx_expr); + } + } } } } @@ -459,16 +457,30 @@ impl<'tcx> GotocCtx<'tcx> { /// Generate Goto-C for each argument to a function call. /// /// N.B. public only because instrinsics use this directly, too. - pub(crate) fn codegen_funcall_args(&mut self, args: &[Operand<'tcx>]) -> Vec { - args.iter() - .map(|o| { - if self.operand_ty(o).is_bool() { - self.codegen_operand(o).cast_to(Type::c_bool()) + /// When `skip_zst` is set to `true`, the return value will not include any argument that is ZST. + /// This is used because we ignore ZST arguments, except for intrinsics. + pub(crate) fn codegen_funcall_args( + &mut self, + args: &[Operand<'tcx>], + skip_zst: bool, + ) -> Vec { + let fargs = args + .iter() + .filter_map(|o| { + let op_ty = self.operand_ty(o); + if op_ty.is_bool() { + Some(self.codegen_operand(o).cast_to(Type::c_bool())) + } else if !self.is_zst(op_ty) || !skip_zst { + Some(self.codegen_operand(o)) } else { - self.codegen_operand(o) + // We ignore ZST types. + debug!(arg=?o, "codegen_funcall_args ignore"); + None } }) - .collect() + .collect(); + debug!(?fargs, "codegen_funcall_args"); + fargs } /// Generates Goto-C for a MIR [TerminatorKind::Call] statement. @@ -498,7 +510,7 @@ impl<'tcx> GotocCtx<'tcx> { let loc = self.codegen_span(&span); let funct = self.operand_ty(func); - let mut fargs = self.codegen_funcall_args(args); + let mut fargs = self.codegen_funcall_args(args, true); match &funct.kind() { ty::FnDef(defid, subst) => { let instance = @@ -506,8 +518,9 @@ impl<'tcx> GotocCtx<'tcx> { .unwrap() .unwrap(); - if self.ty_needs_closure_untupled(funct) { - self.codegen_untuple_closure_args(instance, &mut fargs, args.last()); + // TODO(celina): Move this check to be inside codegen_funcall_args. + if self.ty_needs_untupled_args(funct) { + self.codegen_untupled_args(instance, &mut fargs, args.last()); } if let Some(hk) = self.hooks.hook_applies(self.tcx, instance) { @@ -608,6 +621,7 @@ impl<'tcx> GotocCtx<'tcx> { ) -> Vec { let vtable_field_name = self.vtable_field_name(def_id, idx); trace!(?self_ty, ?place, ?vtable_field_name, "codegen_virtual_funcall"); + debug!(?fargs, "codegen_virtual_funcall"); let trait_fat_ptr = self.extract_ptr(fargs[0].clone(), self_ty); assert!( diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 97d851fa511ef..fcf4d935b7c53 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -256,9 +256,9 @@ impl<'tcx> GotocCtx<'tcx> { out } - /// Closures expect their last arg untupled at call site, see comment at - /// ty_needs_closure_untupled. - fn sig_with_closure_untupled(&self, sig: ty::PolyFnSig<'tcx>) -> ty::PolyFnSig<'tcx> { + /// 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() { @@ -324,7 +324,7 @@ impl<'tcx> GotocCtx<'tcx> { ); // The parameter types are tupled, but we want to have them in a vector - self.sig_with_closure_untupled(sig) + self.sig_with_untupled_args(sig) } // Adapted from `fn_sig_for_fn_abi` in compiler/rustc_middle/src/ty/layout.rs @@ -374,11 +374,9 @@ impl<'tcx> GotocCtx<'tcx> { ty::Closure(def_id, subst) => self.closure_sig(*def_id, subst), ty::FnPtr(..) | ty::FnDef(..) => { let sig = fntyp.fn_sig(self.tcx); - // Some virtual calls through a vtable may actually be closures - // or shims that also need the arguments untupled, even though - // the kind of the trait type is not a ty::Closure. - if self.ty_needs_closure_untupled(fntyp) { - return self.sig_with_closure_untupled(sig); + // 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 } @@ -423,6 +421,11 @@ impl<'tcx> GotocCtx<'tcx> { self.monomorphize(p.ty(self.current_fn().mir().local_decls(), self.tcx).ty) } + /// Is the MIR type a zero-sized type. + pub fn is_zst(&self, t: Ty<'tcx>) -> bool { + self.layout_of(t).is_zst() + } + /// Is the MIR type an unsized type /// Unsized types can represent: /// 1- Types that rust cannot infer their type such as ForeignItems. @@ -931,7 +934,7 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_struct_fields(flds, &layout.layout, Size::ZERO) } - /// A closure in Rust MIR takes two arguments: + /// A closure / some shims in Rust MIR takes two arguments: /// /// 0. a struct representing the environment /// 1. a tuple containing the parameters @@ -955,7 +958,7 @@ impl<'tcx> GotocCtx<'tcx> { /// so we follow the example elsewhere in Rust to use the ABI call type. /// /// See `make_call_args` in `rustc_mir_transform/src/inline.rs` - pub fn ty_needs_closure_untupled(&self, ty: Ty<'tcx>) -> bool { + pub fn ty_needs_untupled_args(&self, ty: Ty<'tcx>) -> bool { // Note that [Abi::RustCall] is not [Abi::Rust]. // Documentation is sparse, but it does seem to correspond to the need for untupling. match ty.kind() { @@ -1294,7 +1297,11 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_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); - let params = sig.inputs().iter().map(|t| self.codegen_ty(*t)).collect(); + let params = sig + .inputs() + .iter() + .filter_map(|t| if self.is_zst(*t) { None } else { Some(self.codegen_ty(*t)) }) + .collect(); if sig.c_variadic { Type::variadic_code_with_unnamed_parameters(params, self.codegen_ty(sig.output())) @@ -1679,33 +1686,46 @@ impl<'tcx> GotocCtx<'tcx> { 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. + let is_vtable_shim = + matches!(self.current_fn().instance().def, ty::InstanceDef::VTableShim(..)); let mut params: Vec = sig .inputs() .iter() .enumerate() - .map(|(i, t)| { - let lc = Local::from_usize(i + 1); - let mut ident = self.codegen_var_name(&lc); - - // `spread_arg` indicates that the last argument is tupled - // at the LLVM/codegen level, so we need to declare the indivual - // 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 lc.index() >= spread.index() { - let (name, _) = self.codegen_spread_arg_name(&lc); - ident = name; + .filter_map(|(i, t)| { + let is_vtable_shim_self = i == 0 && is_vtable_shim; + if self.is_zst(*t) && !is_vtable_shim_self { + // We ignore zero-sized parameters. + // See https://github.com/model-checking/kani/issues/274 for more details. + None + } else { + let lc = Local::from_usize(i + 1); + let mut ident = self.codegen_var_name(&lc); + + // `spread_arg` indicates that the last argument is tupled + // at the LLVM/codegen level, so we need to declare the indivual + // 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 lc.index() >= spread.index() { + let (name, _) = self.codegen_spread_arg_name(&lc); + ident = name; + } } + Some( + self.codegen_ty(*t) + .as_parameter(Some(ident.clone().into()), Some(ident.into())), + ) } - self.codegen_ty(*t).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. - if let ty::InstanceDef::VTableShim(..) = self.current_fn().instance().def { + // 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(); @@ -1751,7 +1771,7 @@ impl<'tcx> GotocCtx<'tcx> { .map(|idx| { let name = fields[idx].name.to_string().intern(); let field_ty = fields[idx].ty(ctx.tcx, adt_substs); - let typ = if !ctx.layout_of(field_ty).is_zst() { + let typ = if !ctx.is_zst(field_ty) { last_type.clone() } else { ctx.codegen_ty(field_ty) @@ -1839,7 +1859,7 @@ impl<'tcx> GotocCtx<'tcx> { let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields; let mut non_zsts = fields .iter() - .filter(|field| !ctx.layout_of(field.ty(ctx.tcx, adt_substs)).is_zst()) + .filter(|field| !ctx.is_zst(field.ty(ctx.tcx, adt_substs))) .map(|non_zst| (non_zst.name.to_string(), non_zst.ty(ctx.tcx, adt_substs))); let (name, next) = non_zsts.next().expect("Expected one non-zst field."); self.curr = next; diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 858c5d4e9fd85..4d91eecf7a017 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -459,15 +459,10 @@ fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem]) { fn visible_item<'tcx>(item: &MonoItem<'tcx>) -> Option<(MonoItem<'tcx>, DefId)> { match item { // Exclude FnShims and others that cannot be dumped. - MonoItem::Fn(instance) - if matches!( - instance.def, - InstanceDef::FnPtrShim(..) | InstanceDef::ClosureOnceShim { .. } - ) => - { - None + MonoItem::Fn(instance) if matches!(instance.def, InstanceDef::Item(..)) => { + Some((*item, instance.def_id())) } - MonoItem::Fn(instance) => Some((*item, instance.def_id())), + MonoItem::Fn(..) => None, MonoItem::Static(def_id) => Some((*item, *def_id)), MonoItem::GlobalAsm(_) => None, } diff --git a/tests/kani/Closure/closure_ptr.rs b/tests/kani/Closure/closure_ptr.rs new file mode 100644 index 0000000000000..4d19cfac86f78 --- /dev/null +++ b/tests/kani/Closure/closure_ptr.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Test that we can handle passing closure as function pointer. + +/// Invoke given function with the given 'input'. +fn invoke(input: usize, f: fn(usize) -> usize) -> usize { + f(input) +} + +#[kani::proof] +fn check_closure_ptr() { + let input = kani::any(); + let output = invoke(input, |x| x); + assert_eq!(output, input); +} diff --git a/tests/kani/Closure/zst_param.rs b/tests/kani/Closure/zst_param.rs new file mode 100644 index 0000000000000..3eee1e5ac6723 --- /dev/null +++ b/tests/kani/Closure/zst_param.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Test that Kani can properly handle closure to fn ptr when some of the arguments are zero +//! size type. +//! Also ensure that we can still take the address of the arguments. + +struct Void; + +/// Invoke given function with the given 'input'. +fn invoke(input: usize, f: fn(Void, usize, Void) -> usize) -> usize { + kani::cover!(); + f(Void, input, Void) +} + +#[kani::proof] +fn check_zst_param() { + let input = kani::any(); + let closure = |a: Void, out: usize, b: Void| { + kani::cover!(); + assert!(&a as *const Void != &b as *const Void, "Should succeed"); + out + }; + let output = invoke(input, closure); + assert_eq!(output, input); +} diff --git a/tests/kani/Intrinsics/Volatile/store.rs b/tests/kani/Intrinsics/Volatile/store.rs index bd46dd81056bf..8311bd2387df1 100644 --- a/tests/kani/Intrinsics/Volatile/store.rs +++ b/tests/kani/Intrinsics/Volatile/store.rs @@ -26,3 +26,13 @@ fn main() { unsafe { std::intrinsics::volatile_store(unaligned, 42) }; assert!(packed.unaligned == 42); } + +/// Check that volatile store also works for ZST. +#[kani::proof] +pub fn check_zst_volatile_store() { + let mut dst = (); + unsafe { + std::intrinsics::volatile_store(&mut dst, ()); + } + assert_eq!(dst, ()); +} diff --git a/tests/kani/Intrinsics/black_box.rs b/tests/kani/Intrinsics/black_box.rs index 7e34e0bf55d68..9959435e3422f 100644 --- a/tests/kani/Intrinsics/black_box.rs +++ b/tests/kani/Intrinsics/black_box.rs @@ -1,13 +1,20 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT - -#![feature(bench_black_box)] +//! Check that blackbox is an identity function. use std::hint::black_box; #[kani::proof] -fn main() { +fn check_blackbox() { // black_box is an identity function that limits compiler optimizations let a = 10; let b = black_box(a); assert!(a == b); } + +/// Ensure that our intrinsics code work with ZST arguments. For intrinsics, we do not ignore them. +#[kani::proof] +fn check_zst_blackbox() { + let void = (); + let nothing = black_box(void); + assert!(void == nothing); +} diff --git a/tests/script-based-pre/check-output/check-output.sh b/tests/script-based-pre/check-output/check-output.sh index bb15f12b83daa..429bd49ac0421 100755 --- a/tests/script-based-pre/check-output/check-output.sh +++ b/tests/script-based-pre/check-output/check-output.sh @@ -26,11 +26,14 @@ else exit 0 fi +export RUST_BACKTRACE=1 cd $(dirname $0) echo "Running single-file check..." rm -rf *.c -RUST_BACKTRACE=1 kani --gen-c --enable-unstable singlefile.rs --quiet +kani --gen-c --enable-unstable singlefile.rs >& kani.log || \ + { ret=$?; echo "== Failed to run Kani"; cat kani.log; rm kani.log; exit 1; } +rm -f kani.log if ! [ -e singlefile.for-main.c ] then echo "Error: no GotoC file generated. Expected: singlefile.for-main.c" @@ -67,7 +70,9 @@ echo (cd multifile echo "Running multi-file check..." rm -rf build -RUST_BACKTRACE=1 cargo kani --target-dir build --gen-c --enable-unstable --quiet +cargo kani --target-dir build --gen-c --enable-unstable >& kani.log || \ + { ret=$?; echo "== Failed to run Kani"; cat kani.log; rm kani.log; exit 1; } +rm -f kani.log cd build/kani/${TARGET}/debug/deps/ mangled=$(ls multifile*.for-main.c) diff --git a/tests/script-based-pre/check-output/multifile/src/main.rs b/tests/script-based-pre/check-output/multifile/src/main.rs index 8b4cd8dd03f65..79a9228ae870f 100644 --- a/tests/script-based-pre/check-output/multifile/src/main.rs +++ b/tests/script-based-pre/check-output/multifile/src/main.rs @@ -1,11 +1,12 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -pub struct PrettyStruct; +// Add a dummy data so PrettyStruct doesn't get removed from arg list. +pub struct PrettyStruct(u32); #[kani::proof] fn main() { - pretty_function(PrettyStruct); + pretty_function(PrettyStruct(2)); } pub fn pretty_function(argument: PrettyStruct) -> PrettyStruct { diff --git a/tests/script-based-pre/check-output/singlefile.rs b/tests/script-based-pre/check-output/singlefile.rs index ca70944b37e01..3c47e1e8c5228 100644 --- a/tests/script-based-pre/check-output/singlefile.rs +++ b/tests/script-based-pre/check-output/singlefile.rs @@ -1,11 +1,12 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -pub struct PrettyStruct; +// Add a dummy data so PrettyStruct doesn't get removed from arg list. +pub struct PrettyStruct(u32); #[kani::proof] pub fn main() { - pretty_function(PrettyStruct); + pretty_function(PrettyStruct(5)); monomorphize::<()>(); monomorphize::(); let x = [true; 2];