From d4af992e92ecb0eef6934928c13902530d386820 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 13 Jan 2023 13:13:36 -0800 Subject: [PATCH 1/4] Add support to casting closure to function pointer Change function declaration and call to ignore arguments that are ZST, and implement the closure to function pointer by reifying it to its FnOnce implementation. The casting of closures to function pointers rely on the fact that the closures do not capture anything. Those closures are represented by empty structures, which should get pruned from its argument list of the FnOnce::call_once implementation. --- docs/src/rust-feature-support.md | 4 +- .../codegen_cprover_gotoc/codegen/function.rs | 59 +++++++++----- .../codegen_cprover_gotoc/codegen/rvalue.rs | 41 +++++----- .../codegen/statement.rs | 55 ++++++++----- .../src/codegen_cprover_gotoc/codegen/typ.rs | 80 ++++++++++++------- .../compiler_interface.rs | 11 +-- tests/kani/Closure/closure_ptr.rs | 15 ++++ tests/kani/Closure/zst_param.rs | 25 ++++++ .../check-output/check-output.sh | 6 +- .../check-output/multifile/src/main.rs | 5 +- .../check-output/singlefile.rs | 5 +- 11 files changed, 199 insertions(+), 107 deletions(-) create mode 100644 tests/kani/Closure/closure_ptr.rs create mode 100644 tests/kani/Closure/zst_param.rs diff --git a/docs/src/rust-feature-support.md b/docs/src/rust-feature-support.md index eebb1def6ccc..d66636dd092d 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 3ecfafe10542..a6e7ef919935 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::{self, Instance}; use std::collections::BTreeMap; use std::convert::TryInto; @@ -46,14 +46,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); @@ -95,29 +100,39 @@ impl<'tcx> GotocCtx<'tcx> { self.reset_current_fn(); } + 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 cannot have an /// argument list in MIR that is both generic and variadic, so Rust /// allows a generic tuple). /// + /// These tuples are used in the MIR to invoke a shim, and it's used in the shim body. + /// /// 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. + /// to be "spread"/untupled. However, the shim body itself will 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 parameters + /// back to the local tuple that will 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 @@ -158,7 +173,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 @@ -191,7 +206,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. @@ -203,12 +218,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/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 4e58b82237cd..407879230f22 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,22 @@ impl<'tcx> GotocCtx<'tcx> { } _ => unreachable!(), }, - PointerCast::UnsafeFnPointer => self.codegen_operand(o), - 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", - ) - } - PointerCast::MutToConstPointer => self.codegen_operand(o), + PointerCast::UnsafeFnPointer => self.codegen_operand(operand), + PointerCast::ClosureFnPointer(_) => match self.operand_ty(operand).kind() { + ty::Closure(def_id, substs) => { + 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() + } + _ => unreachable!("{:?} cannot be cast to a fn ptr", operand), + }, + PointerCast::MutToConstPointer => self.codegen_operand(operand), PointerCast::ArrayToPointer => { // TODO: I am not sure whether it is correct or not. // @@ -677,11 +682,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 +698,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 d5dc58714d90..8f1a0f61e959 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. @@ -405,7 +404,7 @@ impl<'tcx> GotocCtx<'tcx> { /// As part of **calling** a function (closure actually), we may need to un-tuple arguments. /// /// See [GotocCtx::ty_needs_closure_untupled] - fn codegen_untuple_closure_args( + fn codegen_untupled_args( &mut self, instance: Instance<'tcx>, fargs: &mut Vec, @@ -431,17 +430,21 @@ impl<'tcx> GotocCtx<'tcx> { // 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); + } + } } } } @@ -460,15 +463,23 @@ impl<'tcx> GotocCtx<'tcx> { /// /// 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()) + 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) { + 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. @@ -506,8 +517,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 +620,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 97d851fa511e..0df46a9fbdd3 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 expect their last arg untupled at call site, see comment at + /// ty_needs_untupled_shim. + fn sig_with_untupled_shim(&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_shim(sig) } // Adapted from `fn_sig_for_fn_abi` in compiler/rustc_middle/src/ty/layout.rs @@ -374,11 +374,10 @@ 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 may actually be shims that also need the + // arguments untupled. + if self.ty_needs_untupled_args(fntyp) { + return self.sig_with_untupled_shim(sig); } sig } @@ -423,6 +422,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 +935,9 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_struct_fields(flds, &layout.layout, Size::ZERO) } - /// A closure in Rust MIR takes two arguments: + /// TODO: Is this really the case?? It seems to me that things that require some sort of Fn + /// shims are the ones that really need untuple. + /// A closure in Rust MIR takes two arguments: /// /// 0. a struct representing the environment /// 1. a tuple containing the parameters @@ -955,7 +961,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 +1300,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 +1689,45 @@ 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)| { + if self.is_zst(*t) && !(i == 0 && is_vtable_shim) { + // 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 +1773,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 +1861,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 6491c9da05d4..ffb2b391eef3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -448,15 +448,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 000000000000..4d19cfac86f7 --- /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 000000000000..3eee1e5ac672 --- /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/script-based-pre/check-output/check-output.sh b/tests/script-based-pre/check-output/check-output.sh index bb15f12b83da..bd839e1d3793 100755 --- a/tests/script-based-pre/check-output/check-output.sh +++ b/tests/script-based-pre/check-output/check-output.sh @@ -30,7 +30,8 @@ cd $(dirname $0) echo "Running single-file check..." rm -rf *.c -RUST_BACKTRACE=1 kani --gen-c --enable-unstable singlefile.rs --quiet +RUST_BACKTRACE=1 kani --gen-c --enable-unstable singlefile.rs >& kani.log || \ + { ret=$?; echo "== Failed to run Kani"; cat kani.log; exit 1; } if ! [ -e singlefile.for-main.c ] then echo "Error: no GotoC file generated. Expected: singlefile.for-main.c" @@ -67,7 +68,8 @@ echo (cd multifile echo "Running multi-file check..." rm -rf build -RUST_BACKTRACE=1 cargo kani --target-dir build --gen-c --enable-unstable --quiet +RUST_BACKTRACE=1 cargo kani --target-dir build --gen-c --enable-unstable >& kani.log || \ + { ret=$?; echo "== Failed to run Kani"; cat kani.log; exit 1; } 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 8b4cd8dd03f6..79a9228ae870 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 ca70944b37e0..3c47e1e8c522 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]; From f088d237d6c2f75c1e244764da47ea17bad4ac77 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 13 Jan 2023 16:17:31 -0800 Subject: [PATCH 2/4] Fix intrinsics --- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/statement.rs | 12 +++++++++--- tests/kani/Intrinsics/Volatile/store.rs | 10 ++++++++++ tests/kani/Intrinsics/black_box.rs | 13 ++++++++++--- 4 files changed, 30 insertions(+), 7 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index a906b5567714..b1edafb0add6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -68,7 +68,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/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 8f1a0f61e959..fbc112419ce1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -462,14 +462,20 @@ 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 { + /// 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) { + } else if !self.is_zst(op_ty) || !skip_zst { Some(self.codegen_operand(o)) } else { // We ignore ZST types. @@ -509,7 +515,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 = diff --git a/tests/kani/Intrinsics/Volatile/store.rs b/tests/kani/Intrinsics/Volatile/store.rs index bd46dd81056b..8311bd2387df 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 7e34e0bf55d6..9959435e3422 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); +} From c2c3ab92be65140160a28b56ce0147013eb9682b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 13 Jan 2023 17:16:52 -0800 Subject: [PATCH 3/4] Polish the code and comments --- .../codegen_cprover_gotoc/codegen/function.rs | 10 ++++++---- .../codegen_cprover_gotoc/codegen/statement.rs | 15 +++++++-------- .../src/codegen_cprover_gotoc/codegen/typ.rs | 17 +++++++---------- 3 files changed, 20 insertions(+), 22 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index a6e7ef919935..2ac8c957ef27 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -100,6 +100,8 @@ 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 { @@ -110,17 +112,17 @@ impl<'tcx> GotocCtx<'tcx> { /// 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 the function traits 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). /// /// These tuples are used in the MIR to invoke a shim, and it's used in the shim body. /// /// If `spread_arg` is Some, then the wrapped value is the local that is - /// to be "spread"/untupled. However, the shim body itself will refer to the members of + /// 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 parameters - /// back to the local tuple that will be used in the body. + /// function prelude code that _retuples_, that is, writes the arguments + /// back to a local tuple that can be used in the body. /// /// See: /// diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index fbc112419ce1..050f176c6323 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -401,9 +401,9 @@ 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] + /// See [GotocCtx::ty_needs_untupled_args] fn codegen_untupled_args( &mut self, instance: Instance<'tcx>, @@ -415,15 +415,14 @@ impl<'tcx> GotocCtx<'tcx> { self.readable_instance_name(instance), fargs ); - // A closure takes two arguments: - // 0. a struct representing the environment + // A closure / shim takes two arguments: + // 0. a struct (or a pointer to) 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. + // However, Rust generates a function which 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. + // an invocation of a RustCall ABI function. // // 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 diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 0df46a9fbdd3..d507ae62833a 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 } - /// Function shims expect their last arg untupled at call site, see comment at - /// ty_needs_untupled_shim. - fn sig_with_untupled_shim(&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_untupled_shim(sig) + self.sig_with_untupled_args(sig) } // Adapted from `fn_sig_for_fn_abi` in compiler/rustc_middle/src/ty/layout.rs @@ -374,10 +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); - // Calls through vtable or Fn pointer may actually be shims that also need the - // arguments untupled. + // 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_shim(sig); + return self.sig_with_untupled_args(sig); } sig } @@ -935,9 +934,7 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_struct_fields(flds, &layout.layout, Size::ZERO) } - /// TODO: Is this really the case?? It seems to me that things that require some sort of Fn - /// shims are the ones that really need untuple. - /// 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 From dc159af2e9ca9db29f2ab35861bfd1d4d7bce0eb Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 18 Jan 2023 12:46:04 -0800 Subject: [PATCH 4/4] Address PR feedback --- .../codegen_cprover_gotoc/codegen/function.rs | 4 ++-- .../codegen_cprover_gotoc/codegen/rvalue.rs | 9 +++---- .../codegen/statement.rs | 24 ++++++++----------- .../src/codegen_cprover_gotoc/codegen/typ.rs | 3 ++- .../check-output/check-output.sh | 11 +++++---- 5 files changed, 26 insertions(+), 25 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 2ac8c957ef27..afe6c8cfbe94 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -118,8 +118,8 @@ impl<'tcx> GotocCtx<'tcx> { /// /// These tuples are used in the MIR to invoke a shim, and it's used in the shim body. /// - /// If `spread_arg` is Some, then the wrapped value is the local that is - /// to be "spread"/untupled. However, the function body itself may refer to the members of + /// 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. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 407879230f22..12bfe861bbc6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -659,8 +659,8 @@ impl<'tcx> GotocCtx<'tcx> { _ => unreachable!(), }, PointerCast::UnsafeFnPointer => self.codegen_operand(operand), - PointerCast::ClosureFnPointer(_) => match self.operand_ty(operand).kind() { - ty::Closure(def_id, substs) => { + PointerCast::ClosureFnPointer(_) => { + if let ty::Closure(def_id, substs) = self.operand_ty(operand).kind() { let instance = Instance::resolve_closure( self.tcx, *def_id, @@ -670,9 +670,10 @@ impl<'tcx> GotocCtx<'tcx> { .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) } - _ => unreachable!("{:?} cannot be cast to a fn ptr", operand), - }, + } PointerCast::MutToConstPointer => self.codegen_operand(operand), PointerCast::ArrayToPointer => { // TODO: I am not sure whether it is correct or not. diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 050f176c6323..ab8d250dbe73 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -403,7 +403,16 @@ impl<'tcx> GotocCtx<'tcx> { /// As part of **calling** a function (or closure), we may need to un-tuple arguments. /// - /// See [GotocCtx::ty_needs_untupled_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>, @@ -415,19 +424,6 @@ impl<'tcx> GotocCtx<'tcx> { self.readable_instance_name(instance), fargs ); - // A closure / shim takes two arguments: - // 0. a struct (or a pointer to) representing the environment - // 1. a tuple containing the parameters - // - // However, Rust generates a function which 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 RustCall ABI function. - // - // 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) { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index d507ae62833a..fcf4d935b7c5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1693,7 +1693,8 @@ impl<'tcx> GotocCtx<'tcx> { .iter() .enumerate() .filter_map(|(i, t)| { - if self.is_zst(*t) && !(i == 0 && is_vtable_shim) { + 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 diff --git a/tests/script-based-pre/check-output/check-output.sh b/tests/script-based-pre/check-output/check-output.sh index bd839e1d3793..429bd49ac042 100755 --- a/tests/script-based-pre/check-output/check-output.sh +++ b/tests/script-based-pre/check-output/check-output.sh @@ -26,12 +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 >& kani.log || \ - { ret=$?; echo "== Failed to run Kani"; cat kani.log; exit 1; } +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" @@ -68,8 +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 >& kani.log || \ - { ret=$?; echo "== Failed to run Kani"; cat kani.log; exit 1; } +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)