diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index e670dfea9..82672ba2e 100644 --- a/charon/src/bin/charon-driver/translate/translate_bodies.rs +++ b/charon/src/bin/charon-driver/translate/translate_bodies.rs @@ -582,7 +582,49 @@ impl BodyTransCtx<'_, '_, '_> { ), )?) } - // TODO(dyn): more ways of registering vtable instance? + hax::ImplExprAtom::Builtin { .. } => { + // Handle built-in implementations, including closures + let tref = &impl_expr.r#trait; + let hax_state = self.hax_state_with_id().clone(); + let trait_def = self.hax_def( + &tref.hax_skip_binder_ref().erase(&hax_state), + )?; + let closure_kind = + trait_def.lang_item.as_deref().and_then(|lang| { + match lang { + "fn_once" => Some(ClosureKind::FnOnce), + "fn_mut" => Some(ClosureKind::FnMut), + "fn" | "r#fn" => Some(ClosureKind::Fn), + _ => None, + } + }); + + // Check if this is a closure trait implementation + if let Some(closure_kind) = closure_kind + && let Some(hax::GenericArg::Type(closure_ty)) = + impl_expr + .r#trait + .hax_skip_binder_ref() + .generic_args + .first() + && let hax::TyKind::Closure(closure_args) = + closure_ty.kind() + { + Some(self.translate_item( + span, + &closure_args.item, + TransItemSourceKind::VTableInstance( + TraitImplSource::Closure(closure_kind), + ), + )?) + } else { + raise_error!( + self.i_ctx, + span, + "Handle non-closure virtual trait implementations." + ); + } + } _ => { trace!( "impl_expr not triggering registering vtable: {:?}", diff --git a/charon/src/bin/charon-driver/translate/translate_closures.rs b/charon/src/bin/charon-driver/translate/translate_closures.rs index 8500d8be0..77965f9dd 100644 --- a/charon/src/bin/charon-driver/translate/translate_closures.rs +++ b/charon/src/bin/charon-driver/translate/translate_closures.rs @@ -349,7 +349,7 @@ impl ItemTransCtx<'_, '_> { /// Given an item that is a closure, generate the signature of the /// `call_once`/`call_mut`/`call` method (depending on `target_kind`). - fn translate_closure_method_sig( + pub fn translate_closure_method_sig( &mut self, def: &hax::FullDef, span: Span, @@ -745,4 +745,43 @@ impl ItemTransCtx<'_, '_> { body, }) } + + pub fn generate_closure_method_shim_ref( + &mut self, + span: Span, + impl_def: &hax::FullDef, + closure_kind: ClosureKind, + ) -> Result { + // Register the closure method shim + let shim_id: FunDeclId = self.register_item( + span, + impl_def.this(), + TransItemSourceKind::VTableMethod(TraitImplSource::Closure(closure_kind)), + ); + + let mut generics = Box::new(self.the_only_binder().params.identity_args()); + + // Add the arguments for region binders of the closure + let hax::FullDefKind::Closure { args, .. } = impl_def.kind() else { + unreachable!() + }; + // The signature can only contain region binders + let sig = &args.fn_sig; + for _ in &sig.bound_vars { + // The late-bound region binders are at last, for the whole closure, as per `translate_closures`, use push + generics.regions.push(Region::Erased); + } + // Finally, one more region for the receiver, this is at first, as it is the region of the function itself, use insert at head + generics + .regions + .insert_and_shift_ids(RegionId::ZERO, Region::Erased); + + // Create function pointer to the shim + let fn_ptr = FnPtr { + kind: Box::new(shim_id.into()), + generics, + }; + + Ok(ConstantExprKind::FnPtr(fn_ptr)) + } } diff --git a/charon/src/bin/charon-driver/translate/translate_crate.rs b/charon/src/bin/charon-driver/translate/translate_crate.rs index 3a6e28bdf..ca47ccd46 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate.rs @@ -77,9 +77,9 @@ pub enum TransItemSourceKind { /// Shim function to store a method in a vtable; give a method with `self: Ptr` argument, /// this takes a `Ptr` and forwards to the method. The `DefId` refers to the method /// implementation. - VTableMethod, + VTableMethod(TraitImplSource), /// The drop shim function to be used in the vtable as a field, the ID is an `impl`. - VTableDropShim, + VTableDropShim(TraitImplSource), } /// The kind of a [`TransItemSourceKind::TraitImpl`]. @@ -294,8 +294,8 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { | ClosureAsFnCast | DropInPlaceMethod(..) | VTableInstanceInitializer(..) - | VTableMethod - | VTableDropShim => ItemId::Fun(self.translated.fun_decls.reserve_slot()), + | VTableMethod(..) + | VTableDropShim(..) => ItemId::Fun(self.translated.fun_decls.reserve_slot()), InherentImpl | Module => return None, }; // Add the id to the queue of declarations to translate diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index 0c7a99f15..79522ab7c 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -188,18 +188,31 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { bt_ctx.translate_vtable_instance_init(id, item_meta, &def, impl_kind)?; self.translated.fun_decls.set_slot(id, fun_decl); } - TransItemSourceKind::VTableMethod => { + TransItemSourceKind::VTableMethod(impl_kind) => { let Some(ItemId::Fun(id)) = trans_id else { unreachable!() }; - let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def)?; + // let TraitImplSource::Closure(target_kind) = + let fun_decl = match impl_kind { + TraitImplSource::Closure(target_kind) => { + let ret = bt_ctx.translate_closure_vtable_shim( + id, + item_meta, + &def, + target_kind, + )?; + // eprintln!("{}", self.translated); + ret + } + _ => bt_ctx.translate_vtable_shim(id, item_meta, &def, impl_kind)?, + }; self.translated.fun_decls.set_slot(id, fun_decl); } - TransItemSourceKind::VTableDropShim => { + TransItemSourceKind::VTableDropShim(impl_kind) => { let Some(ItemId::Fun(id)) = trans_id else { unreachable!() }; - let fun_decl = bt_ctx.translate_vtable_drop_shim(id, item_meta, &def)?; + let fun_decl = bt_ctx.translate_vtable_drop_shim(id, item_meta, &def, impl_kind)?; self.translated.fun_decls.set_slot(id, fun_decl); } } diff --git a/charon/src/bin/charon-driver/translate/translate_meta.rs b/charon/src/bin/charon-driver/translate/translate_meta.rs index 48b4edaa5..099930c3d 100644 --- a/charon/src/bin/charon-driver/translate/translate_meta.rs +++ b/charon/src/bin/charon-driver/translate/translate_meta.rs @@ -397,13 +397,13 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { name.name .push(PathElem::Ident("{vtable}".into(), Disambiguator::ZERO)); } - TransItemSourceKind::VTableMethod => { + TransItemSourceKind::VTableMethod(..) => { name.name.push(PathElem::Ident( "{vtable_method}".into(), Disambiguator::ZERO, )); } - TransItemSourceKind::VTableDropShim => { + TransItemSourceKind::VTableDropShim(..) => { name.name.push(PathElem::Ident( "{vtable_drop_shim}".into(), Disambiguator::ZERO, diff --git a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs index 5ccac9581..e60d79023 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -1,7 +1,7 @@ use charon_lib::ast::ullbc_ast_utils::BodyBuilder; use hax::TraitPredicate; use itertools::Itertools; -use std::mem; +use std::{mem, vec}; use super::{ translate_crate::TransItemSourceKind, translate_ctx::*, translate_generics::BindingLevel, @@ -247,6 +247,24 @@ impl ItemTransCtx<'_, '_> { fields.push(TrVTableField::Align); fields.push(TrVTableField::Drop); + // The `FnOnce::call_once` is not compatible with the dyn-compatibility as described in: + // https://doc.rust-lang.org/reference/items/traits.html#dyn-compatibility + // But the Rustc offers a special backdoor for this and allows this method to be `vtable_safe`. + // The only way to call such a function seems to be with `Box`. + // The implementation of `Box::call_once` is a special case and should translate specially with some special magic. + // TODO(ssyram): in the future we may implement the function with type `fn call_once(self: Box, Args) -> Output` + // This function is the vtable-specific version of the `call_once` method. + // A very special case that the type signature differs from the original signature. + // Anyway, if we allow this to happen, there will be a severe breakage in that we can perform concretization on `dyn FnOnce`, + // This will make the life in backend tools, especially Eurydice much harder. + // Likewise, we skip translation of the `call_once` method below in the instance. + if trait_def.lang_item == Some("fn_once".into()) { + return Ok(VTableData { + fields, + supertrait_map, + }); + } + // Method fields. if let hax::FullDefKind::Trait { items, .. } = trait_def.kind() { for item in items { @@ -439,7 +457,15 @@ impl ItemTransCtx<'_, '_> { (0..implied_predicates.predicates.len()) .map(|_| None) .collect(); - let (mut kind, layout) = if item_meta.opacity.with_private_contents().is_opaque() { + let is_closure = |lang_item: &Option| match lang_item { + Some(name) => name == "r#fn" || name == "fn_mut" || name == "fn_once", + None => false, + }; + + // Translate normal traits and Closure traits. + let (mut kind, layout) = if item_meta.opacity.with_private_contents().is_opaque() + && !is_closure(&trait_def.lang_item) + { (TypeDeclKind::Opaque, None) } else { // First construct fields that use the real method signatures (which may use the `Self` @@ -541,22 +567,44 @@ impl ItemTransCtx<'_, '_> { fn get_vtable_instance_info<'a>( &mut self, span: Span, - impl_def: &'a hax::FullDef, + def: &'a hax::FullDef, impl_kind: &TraitImplSource, - ) -> Result<(TraitImplRef, TypeDeclRef), Error> { - let implemented_trait = match impl_def.kind() { - hax::FullDefKind::TraitImpl { trait_pred, .. } => &trait_pred.trait_ref, - _ => unreachable!(), + ) -> Result<(TraitImplRef, TraitDeclRef, TypeDeclRef), Error> { + let (implemented_trait, impl_ref) = match def.kind() { + hax::FullDefKind::TraitImpl { trait_pred, .. } => ( + &trait_pred.trait_ref, + self.translate_item(span, def.this(), TransItemSourceKind::TraitImpl(*impl_kind))?, + ), + hax::FullDefKind::Closure { + fn_once_impl, + fn_mut_impl, + fn_impl, + args, + .. + } => { + let target_kind = match impl_kind { + TraitImplSource::Closure(kind) => *kind, + _ => unreachable!(), + }; + // For closures, get the trait implementation based on the closure kind + let closure_trait_impl = match target_kind { + ClosureKind::FnOnce => fn_once_impl, + ClosureKind::FnMut => fn_mut_impl.as_ref().expect("FnMut impl should exist"), + ClosureKind::Fn => fn_impl.as_ref().expect("Fn impl should exist"), + }; + ( + &closure_trait_impl.trait_pred.trait_ref, + self.translate_closure_bound_impl_ref(span, args, target_kind)? + .erase(), + ) + } + _ => panic!("Unknown type of impl full def: {:?}", def.kind()), }; let vtable_struct_ref = self .translate_vtable_struct_ref(span, implemented_trait)? .expect("trait should be dyn-compatible"); - let impl_ref = self.translate_item( - span, - impl_def.this(), - TransItemSourceKind::TraitImpl(*impl_kind), - )?; - Ok((impl_ref, vtable_struct_ref)) + let implemented_trait = self.translate_trait_decl_ref(span, implemented_trait)?; + Ok((impl_ref, implemented_trait, vtable_struct_ref)) } /// E.g., @@ -583,7 +631,7 @@ impl ItemTransCtx<'_, '_> { let span = item_meta.span; self.check_no_monomorphize(span)?; - let (impl_ref, vtable_struct_ref) = + let (impl_ref, _, vtable_struct_ref) = self.get_vtable_instance_info(span, impl_def, impl_kind)?; // Initializer function for this global. let init = self.register_item( @@ -629,7 +677,11 @@ impl ItemTransCtx<'_, '_> { // generics -- the lifetime binder will be added as `Erased` in `translate_fn_ptr`. let item_ref = impl_def.this().with_def_id(self.hax_state(), item_def_id); let shim_ref = self - .translate_fn_ptr(span, &item_ref, TransItemSourceKind::VTableMethod)? + .translate_fn_ptr( + span, + &item_ref, + TransItemSourceKind::VTableMethod(TraitImplSource::Normal), + )? .erase(); ConstantExprKind::FnDef(shim_ref) } @@ -653,12 +705,29 @@ impl ItemTransCtx<'_, '_> { impl_def: &hax::FullDef, mut mk_field: impl FnMut(ConstantExprKind), ) -> Result<(), Error> { - let hax::FullDefKind::TraitImpl { - implied_impl_exprs, .. - } = impl_def.kind() - else { - unreachable!() + let implied_impl_exprs = match impl_def.kind() { + hax::FullDefKind::TraitImpl { + implied_impl_exprs, .. + } => implied_impl_exprs, + hax::FullDefKind::Closure { + fn_once_impl, + fn_mut_impl, + fn_impl, + .. + } => match trait_def.lang_item { + Some("fn") | Some("r#fn") => &fn_impl.as_ref().unwrap().implied_impl_exprs, + Some("fn_once") => &fn_once_impl.as_ref().implied_impl_exprs, + Some("fn_mut") => &fn_mut_impl.as_ref().unwrap().implied_impl_exprs, + _ => unreachable!(), + }, + kind => raise_error!(self, span, "TODO: Unknown type of impl full def: {kind:?}"), }; + // let hax::FullDefKind::TraitImpl { + // implied_impl_exprs, .. + // } = impl_def.kind() + // else { + // unreachable!() + // }; let hax::FullDefKind::Trait { implied_predicates, .. } = trait_def.kind() @@ -696,8 +765,90 @@ impl ItemTransCtx<'_, '_> { }); ConstantExprKind::Ref(global) } - // TODO(dyn): builtin impls - _ => ConstantExprKind::Opaque("missing supertrait vtable".into()), + hax::ImplExprAtom::Builtin { trait_data, .. } => { + // Handle built-in implementations, including closures + let tref = &impl_expr.r#trait; + let hax_state = self.hax_state_with_id(); + let trait_def = self.hax_def(&tref.hax_skip_binder_ref().erase(hax_state))?; + + trace!( + "Processing builtin impl for trait {:?}, lang_item: {:?}, trait_data: {:?}", + trait_def.def_id(), + trait_def.lang_item, + trait_data + ); + + let closure_kind = trait_def.lang_item.as_deref().and_then(|lang| match lang { + "fn_once" => Some(ClosureKind::FnOnce), + "fn_mut" => Some(ClosureKind::FnMut), + "fn" | "r#fn" => Some(ClosureKind::Fn), + _ => None, + }); + + // Check if this is a closure trait implementation + if let Some(closure_kind) = closure_kind + && let Some(hax::GenericArg::Type(closure_ty)) = + impl_expr.r#trait.hax_skip_binder_ref().generic_args.first() + && let hax::TyKind::Closure(closure_args) = closure_ty.kind() + { + // Register the closure vtable instance + let vtable_instance_ref: GlobalDeclRef = self.translate_item( + span, + &closure_args.item, + TransItemSourceKind::VTableInstance(TraitImplSource::Closure( + closure_kind, + )), + )?; + let global = Box::new(ConstantExpr { + kind: ConstantExprKind::Global(vtable_instance_ref), + ty: fn_ptr_ty, + }); + ConstantExprKind::Ref(global) + } else if self + .translate_vtable_struct_ref(span, impl_expr.r#trait.hax_skip_binder_ref())? + .is_some() + { + // TODO: other builtin impls + trace!( + "Handling dyn-compatible builtin trait: {:?}", + trait_def.lang_item + ); + + ConstantExprKind::Opaque("missing supertrait vtable".into()) + } else { + // For non-dyn-compatible builtin traits, this branch should not happen + raise_error!( + self, + span, + "`non-dyn-compatible builtin traits` should not appear in vtable construction" + ) + } + } + hax::ImplExprAtom::LocalBound { .. } => { + // No need to register anything here as there is no concrete impl + // This results in that: the vtable instance in generic case might not exist + // But this case should not happen in the monomorphized case + if self.monomorphize() { + raise_error!( + self, + span, + "Unexpected `LocalBound` in monomorphized context" + ) + } else { + ConstantExprKind::Opaque("generic supertrait vtable".into()) + } + } + hax::ImplExprAtom::Dyn | hax::ImplExprAtom::Error(..) => { + // No need to register anything for these cases + ConstantExprKind::Opaque("dyn or error supertrait vtable".into()) + } + hax::ImplExprAtom::SelfImpl { .. } => { + raise_error!( + self, + span, + "`SelfImpl` should not appear in vtable construction" + ) + } }; mk_field(kind); } @@ -705,7 +856,7 @@ impl ItemTransCtx<'_, '_> { } /// Generate the body of the vtable instance function. - /// This is for `impl Trait for T` implementation, it does NOT handle builtin impls. + /// It handles `impl Trait for T` implementation and builtin impls (including closure). /// ```ignore /// let ret@0 : VTable; /// ret@0 = VTable { ... }; @@ -716,15 +867,49 @@ impl ItemTransCtx<'_, '_> { span: Span, impl_def: &hax::FullDef, vtable_struct_ref: TypeDeclRef, + impl_kind: &TraitImplSource, ) -> Result { - let hax::FullDefKind::TraitImpl { - trait_pred, items, .. - } = impl_def.kind() - else { - unreachable!() + // Get trait reference (`trait_ref`) + let trait_ref = { + match impl_kind { + TraitImplSource::Normal => { + let hax::FullDefKind::TraitImpl { trait_pred, .. } = impl_def.kind() else { + unreachable!() + }; + &trait_pred.trait_ref + } + TraitImplSource::Closure(closure_kind) => { + let hax::FullDefKind::Closure { + fn_once_impl, + fn_mut_impl, + fn_impl, + .. + } = impl_def.kind() + else { + unreachable!() + }; + // Get the appropriate trait implementation for this closure kind + let trait_impl = match closure_kind { + ClosureKind::FnOnce => fn_once_impl, + ClosureKind::FnMut => { + fn_mut_impl.as_ref().expect("FnMut impl should exist") + } + ClosureKind::Fn => fn_impl.as_ref().expect("Fn impl should exist"), + }; + &trait_impl.trait_pred.trait_ref + } + _ => { + raise_error!( + self, + span, + "Don't know how to generate a vtable for a virtual impl {impl_kind:?}" + ); + } + } }; - let trait_def = self.hax_def(&trait_pred.trait_ref)?; - let implemented_trait = self.translate_trait_decl_ref(span, &trait_pred.trait_ref)?; + + let trait_def = self.hax_def(trait_ref)?; + let implemented_trait = self.translate_trait_decl_ref(span, trait_ref)?; // The type this impl is for. let self_ty = &implemented_trait.generics.types[0]; @@ -773,21 +958,39 @@ impl ItemTransCtx<'_, '_> { // Helper to fill in the remaining fields with constant values. let mut mk_field = |kind| { - let ty = field_ty_iter.next().unwrap(); - aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { kind, ty }))); + // Check whether there are remaining fields. + // Special case: FnOnce does not have supertrait. + if let Some(ty) = field_ty_iter.next() { + aggregate_fields.push(Operand::Const(Box::new(ConstantExpr { kind, ty }))); + } }; - let drop_shim = - self.translate_item(span, impl_def.this(), TransItemSourceKind::VTableDropShim)?; + let drop_shim = self.translate_item( + span, + impl_def.this(), + TransItemSourceKind::VTableDropShim(*impl_kind), + )?; mk_field(ConstantExprKind::FnDef(drop_shim)); - for item in items { - self.add_method_to_vtable_value(span, impl_def, item, &mut mk_field)?; + // Add methods + if let hax::FullDefKind::TraitImpl { items, .. } = impl_def.kind() { + // Add the normal method + for item in items { + self.add_method_to_vtable_value(span, impl_def, item, &mut mk_field)?; + } + } else if let TraitImplSource::Closure(closure_kind) = *impl_kind + && !matches!(closure_kind, ClosureKind::FnOnce) + { + // Add the closure method (call, call_mut) + // We do not translate `call_once` for the reason discussed above -- the function is not dyn-compatible + mk_field(self.generate_closure_method_shim_ref(span, impl_def, closure_kind)?); } + // Add supertraits to vtable value. self.add_supertraits_to_vtable_value(span, &trait_def, impl_def, &mut mk_field)?; + // Check if every field is filled if field_ty_iter.next().is_some() { raise_error!( self, @@ -818,7 +1021,7 @@ impl ItemTransCtx<'_, '_> { let span = item_meta.span; self.check_no_monomorphize(span)?; - let (impl_ref, vtable_struct_ref) = + let (impl_ref, _, vtable_struct_ref) = self.get_vtable_instance_info(span, impl_def, impl_kind)?; let init_for = self.register_item( span, @@ -833,18 +1036,10 @@ impl ItemTransCtx<'_, '_> { output: Ty::new(TyKind::Adt(vtable_struct_ref.clone())), }; - let body = match impl_kind { - _ if item_meta.opacity.with_private_contents().is_opaque() => Body::Opaque, - TraitImplSource::Normal => { - self.gen_vtable_instance_init_body(span, impl_def, vtable_struct_ref)? - } - _ => { - raise_error!( - self, - span, - "Don't know how to generate a vtable for a virtual impl {impl_kind:?}" - ); - } + let body = if item_meta.opacity.with_private_contents().is_opaque() { + Body::Opaque + } else { + self.gen_vtable_instance_init_body(span, impl_def, vtable_struct_ref, impl_kind)? }; Ok(FunDecl { @@ -881,6 +1076,7 @@ impl ItemTransCtx<'_, '_> { target_receiver: &Ty, shim_signature: &FunSig, impl_func_def: &hax::FullDef, + impl_kind: &TraitImplSource, ) -> Result { let mut builder = BodyBuilder::new(span, shim_signature.inputs.len()); @@ -907,8 +1103,18 @@ impl ItemTransCtx<'_, '_> { ); builder.push_statement(StatementKind::Assign(target_self.clone(), rval)); - let fun_id = self.register_item(span, &impl_func_def.this(), TransItemSourceKind::Fun); + let fun_id = self.register_item( + span, + &impl_func_def.this(), + match impl_kind { + TraitImplSource::Normal => TransItemSourceKind::Fun, + TraitImplSource::Closure(kind) => TransItemSourceKind::ClosureMethod(*kind), + _ => unreachable!(), + }, + ); + let generics = self.outermost_binder().params.identity_args(); + builder.call(Call { func: FnOperand::Regular(FnPtr::new(FnPtrKind::Fun(fun_id), generics)), args: method_args @@ -982,20 +1188,56 @@ impl ItemTransCtx<'_, '_> { fun_id: FunDeclId, item_meta: ItemMeta, impl_def: &hax::FullDef, + impl_kind: &TraitImplSource, ) -> Result { let span = item_meta.span; - let hax::FullDefKind::TraitImpl { - dyn_self: Some(dyn_self), - trait_pred, - .. - } = impl_def.kind() - else { - raise_error!( - self, - span, - "Trying to generate a vtable drop shim for a non-trait impl" - ); + let (dyn_self, trait_pred) = match impl_def.kind() { + hax::FullDefKind::TraitImpl { + dyn_self: Some(dyn_self), + trait_pred, + .. + } => (dyn_self, trait_pred), + hax::FullDefKind::Closure { + fn_mut_vtable_sig, + fn_vtable_sig, + fn_once_impl, + fn_mut_impl, + fn_impl, + .. + } => { + let TraitImplSource::Closure(target_kind) = *impl_kind else { + unreachable!() + }; + let vtable_sig = match target_kind { + ClosureKind::Fn => fn_vtable_sig, + ClosureKind::FnMut => fn_mut_vtable_sig, + ClosureKind::FnOnce => { + // Teporarily use fn_vtable_sig to pass the compilation + // TODO: The vtable_sig (or at least dyn_self) for FnOnce should be added in hax + fn_vtable_sig + } + }; + + let signature = vtable_sig.as_ref().unwrap(); + let hax::TyKind::Ref(_, dyn_self, _) = signature.value.inputs[0].kind() else { + unreachable!() + }; + + let vimpl = match target_kind { + ClosureKind::FnOnce => fn_once_impl, + ClosureKind::FnMut => fn_mut_impl.as_ref().unwrap(), + ClosureKind::Fn => fn_impl.as_ref().unwrap(), + }; + (dyn_self.as_ref(), &vimpl.trait_pred) + } + _ => { + raise_error!( + self, + span, + "Trying to generate a vtable drop shim for a non-trait impl" + ); + } }; // `*mut dyn Trait` @@ -1037,6 +1279,7 @@ impl ItemTransCtx<'_, '_> { fun_id: FunDeclId, item_meta: ItemMeta, impl_func_def: &hax::FullDef, + impl_kind: &TraitImplSource, ) -> Result { let span = item_meta.span; self.check_no_monomorphize(span)?; @@ -1067,7 +1310,155 @@ impl ItemTransCtx<'_, '_> { let body = if item_meta.opacity.with_private_contents().is_opaque() { Body::Opaque } else { - self.translate_vtable_shim_body(span, &target_receiver, &signature, impl_func_def)? + self.translate_vtable_shim_body( + span, + &target_receiver, + &signature, + impl_func_def, + impl_kind, + )? + }; + + Ok(FunDecl { + def_id: fun_id, + item_meta, + generics: self.into_generics(), + signature, + src: ItemSource::VTableMethodShim, + is_global_initializer: None, + body, + }) + } + + // Given `self_ty` with erased Ref region (e.g., &'_ dyn exists<_dyn> ...), + // generate `ref_self` with explicit Reg region + // according to RegionId `rid` (e.g., &'_0 dyn exists<_dyn> ...). + fn generate_ref_self_from_erased_region( + &mut self, + self_ty: &hax::Ty, + rid: RegionId, + span: Span, + target_kind: &ClosureKind, + ) -> Result { + let hax::TyKind::Ref(_, raw_self, _) = self_ty.kind() else { + unreachable!() + }; + + let raw_self = self.translate_ty(span, raw_self)?; + let ref_self = { + let r = Region::Var(DeBruijnVar::new_at_zero(rid)); + let mutability = if *target_kind == ClosureKind::Fn { + RefKind::Shared + } else { + RefKind::Mut + }; + TyKind::Ref(r, raw_self, mutability).into_ty() + }; + Ok(ref_self) + } + + // This follows `translate_vtable_shim`. + // Specific vtable_sig and target_signature are fetched according to `target_kind` (Fn or FnMut). + // Additionally, lifetime generics coming from the higher-kindedness and + // the closure itself are separately dealt with. + pub(crate) fn translate_closure_vtable_shim( + mut self, + fun_id: FunDeclId, + item_meta: ItemMeta, + impl_func_def: &hax::FullDef, + target_kind: &ClosureKind, + ) -> Result { + let span = item_meta.span; + self.check_no_monomorphize(span)?; + + let hax::FullDefKind::Closure { + fn_mut_vtable_sig, + fn_vtable_sig, + fn_mut_sig, + fn_sig, + args, + .. + } = impl_func_def.kind() + else { + raise_error!( + self, + span, + "Trying to generate a vtable shim for a non-vtable-safe method" + ); + }; + + let (vtable_sig, target_signature) = match target_kind { + ClosureKind::Fn => (fn_vtable_sig, &fn_sig.clone().unwrap()), + ClosureKind::FnMut => (fn_mut_vtable_sig, &fn_mut_sig.clone().unwrap()), + ClosureKind::FnOnce => { + raise_error!(self, span, "Trying to generate a vtable shim for FnOnce"); + } + }; + + // Compute the correct signature for the shim + // Add the lifetime generics coming from the higher-kindedness of the signature. + assert!(self.innermost_binder_mut().bound_region_vars.is_empty(),); + self.innermost_binder_mut() + .push_params_from_binder(args.fn_sig.rebind(()))?; + + let signature = vtable_sig.as_ref().unwrap(); + + // translate dyn_self + let rid = self + .innermost_generics_mut() + .regions + .push_with(|index| RegionParam { index, name: None }); + let dyn_self = self.generate_ref_self_from_erased_region( + &signature.value.inputs[0], + rid, + span, + target_kind, + )?; + + // translate Args + let input_tys: Vec = signature + .value + .inputs + .iter() + .skip(1) + .map(|ty| self.translate_ty(span, ty)) + .try_collect()?; + let inputs = vec![dyn_self, Ty::mk_tuple(input_tys)]; + let output = self.translate_ty(span, &signature.value.output)?; + + let is_unsafe = match signature.value.safety { + hax::Safety::Unsafe => true, + hax::Safety::Safe => false, + }; + + let signature = FunSig { + is_unsafe, + inputs, + output, + }; + + let target_receiver = self.generate_ref_self_from_erased_region( + &target_signature.value.inputs[0], + rid, + span, + target_kind, + )?; + + trace!( + "[VtableShim] Obtained dyn signature with receiver type: {}", + signature.inputs[0].with_ctx(&self.into_fmt()) + ); + + let body = if item_meta.opacity.with_private_contents().is_opaque() { + Body::Opaque + } else { + self.translate_vtable_shim_body( + span, + &target_receiver, + &signature, + impl_func_def, + &TraitImplSource::Closure(*target_kind), + )? }; Ok(FunDecl { diff --git a/charon/tests/ui/dyn-closure-regions.out b/charon/tests/ui/dyn-closure-regions.out new file mode 100644 index 000000000..c133c6c82 --- /dev/null +++ b/charon/tests/ui/dyn-closure-regions.out @@ -0,0 +1,454 @@ +# Final LLBC before serialization: + +opaque type core::marker::MetaSized::{vtable} + +// Full name: core::marker::MetaSized +#[lang_item("meta_sized")] +pub trait MetaSized + +// Full name: core::marker::Sized +#[lang_item("sized")] +pub trait Sized +{ + parent_clause0 : [@TraitClause0]: MetaSized + non-dyn-compatible +} + +// Full name: core::marker::Destruct +#[lang_item("destruct")] +pub trait Destruct +{ + fn drop_in_place = core::marker::Destruct::drop_in_place + vtable: core::marker::Destruct::{vtable} +} + +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) += + +// Full name: core::marker::Tuple +#[lang_item("tuple_trait")] +pub trait Tuple +{ + parent_clause0 : [@TraitClause0]: MetaSized + vtable: core::marker::Tuple::{vtable} +} + +// Full name: core::ops::function::FnOnce +#[lang_item("fn_once")] +pub trait FnOnce +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Sized + parent_clause2 : [@TraitClause2]: Tuple + parent_clause3 : [@TraitClause3]: Sized + type Output + fn call_once = core::ops::function::FnOnce::call_once[Self] + vtable: core::ops::function::FnOnce::{vtable} +} + +struct core::ops::function::FnOnce::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn FnOnce)), +} + +// Full name: core::ops::function::FnMut +#[lang_item("fn_mut")] +pub trait FnMut +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnOnce + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call_mut<'_0_1> = core::ops::function::FnMut::call_mut<'_0_1, Self, Args>[Self] + vtable: core::ops::function::FnMut::{vtable} +} + +struct core::ops::function::FnMut::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn FnMut)), + method_call_mut: fn<'_0_1>(&'_0_1 mut ((dyn FnMut)), Args) -> Ty0, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnOnce::{vtable}), +} + +struct core::ops::function::Fn::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn Fn)), + method_call: fn<'_0_1>(&'_0_1 ((dyn Fn)), Args) -> Ty0, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnMut::{vtable}), +} + +// Full name: core::ops::function::Fn +#[lang_item("r#fn")] +pub trait Fn +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnMut + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call<'_0_1> = core::ops::function::Fn::call<'_0_1, Self, Args>[Self] + vtable: core::ops::function::Fn::{vtable} +} + +pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output +where + [@TraitClause0]: Fn, += + +pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output +where + [@TraitClause0]: FnMut, += + +pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> @TraitClause0::Output +where + [@TraitClause0]: FnOnce, += + +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + +// Full name: test_crate::call_test +fn call_test<'b, 'c, '_2, T>(@1: &'_2 ((dyn for<'a> Fn<(&'a (bool)), parent_clause1::parent_clause1::Output = (T, bool, &'b (T))> + '_2)), @2: &'c (bool)) -> (T, bool, &'b (T)) +where + [@TraitClause0]: Sized, + 'c : 'b, +{ + let @0: (T, bool, &'0 (T)); // return + let f@1: &'1 ((dyn for<'a> Fn<(&'a (bool)), parent_clause1::parent_clause1::Output = (T, bool, &'5 (T))> + '2)); // arg #1 + let arg@2: &'6 (bool); // arg #2 + let @3: &'1 ((dyn for<'a> Fn<(&'a (bool)), parent_clause1::parent_clause1::Output = (T, bool, &'5 (T))> + '2)); // anonymous local + let @4: (&'6 (bool)); // anonymous local + let @5: &'6 (bool); // anonymous local + + storage_live(@3) + @3 := &*(f@1) with_metadata(copy (f@1.metadata)) + storage_live(@4) + storage_live(@5) + @5 := &*(arg@2) + @4 := (move (@5)) + @0 := (copy ((*(@3.metadata)).method_call))(move (@3), move (@4)) + storage_dead(@5) + storage_dead(@4) + storage_dead(@3) + return +} + +// Full name: test_crate::main::closure +struct closure<'_0, '_1> { + &'_0 (i32), + &'_1 (i32), +} + +// Full name: test_crate::main::{impl Fn<(&'_ (bool))> for closure<'_0, '_1>}::call +fn {impl Fn<(&'_ (bool))> for closure<'_0, '_1>}::call<'_0, '_1, '_2, '_3>(@1: &'_3 (closure<'_0, '_1>), @2: (&'_2 (bool))) -> (i32, bool, &'_ (i32)) +{ + let @0: (i32, bool, &'_ (i32)); // return + let @1: &'0 (closure<'_0, '_1>); // arg #1 + let tupled_args@2: (&'_2 (bool)); // arg #2 + let a@3: &'_ (bool); // local + let @4: i32; // anonymous local + let @5: bool; // anonymous local + let @6: &'_ (i32); // anonymous local + let @7: &'_ (i32); // anonymous local + + storage_live(a@3) + a@3 := move ((tupled_args@2).0) + storage_live(@4) + @4 := copy (*((*(@1)).0)) + storage_live(@5) + @5 := copy (*(a@3)) + storage_live(@6) + storage_live(@7) + @7 := &*((*(@1)).1) + @6 := &*(@7) + @0 := (move (@4), move (@5), move (@6)) + storage_dead(@7) + storage_dead(@6) + storage_dead(@5) + storage_dead(@4) + return +} + +// Full name: test_crate::main::{impl FnMut<(&'_ (bool))> for closure<'_0, '_1>}::call_mut +fn {impl FnMut<(&'_ (bool))> for closure<'_0, '_1>}::call_mut<'_0, '_1, '_2, '_3>(@1: &'_3 mut (closure<'_0, '_1>), @2: (&'_2 (bool))) -> (i32, bool, &'_ (i32)) +{ + let @0: (i32, bool, &'0 (i32)); // return + let state@1: &'_3 mut (closure<'_0, '_1>); // arg #1 + let args@2: (&'_2 (bool)); // arg #2 + let @3: &'1 (closure<'_0, '_1>); // anonymous local + + storage_live(@3) + @3 := &*(state@1) + @0 := {impl Fn<(&'_ (bool))> for closure<'_0, '_1>}::call<'_0, '_1, '_2, '3>(move (@3), move (args@2)) + return +} + +// Full name: test_crate::main::closure::{impl Destruct for closure<'_0, '_1>}::drop_in_place +unsafe fn {impl Destruct for closure<'_0, '_1>}::drop_in_place<'_0, '_1>(@1: *mut closure<'_0, '_1>) += + +// Full name: test_crate::main::closure::{impl Destruct for closure<'_0, '_1>} +impl<'_0, '_1> Destruct for closure<'_0, '_1> { + fn drop_in_place = {impl Destruct for closure<'_0, '_1>}::drop_in_place<'_0, '_1> + non-dyn-compatible +} + +// Full name: test_crate::main::{impl FnOnce<(&'_ (bool))> for closure<'_0, '_1>}::call_once +fn {impl FnOnce<(&'_ (bool))> for closure<'_0, '_1>}::call_once<'_0, '_1, '_2>(@1: closure<'_0, '_1>, @2: (&'_2 (bool))) -> (i32, bool, &'_ (i32)) +{ + let @0: (i32, bool, &'_ (i32)); // return + let @1: closure<'_0, '_1>; // arg #1 + let @2: (&'_ (bool)); // arg #2 + let @3: &'0 mut (closure<'_0, '_1>); // anonymous local + + storage_live(@3) + @3 := &mut @1 + @0 := {impl FnMut<(&'_ (bool))> for closure<'_0, '_1>}::call_mut<'_0, '_1, '_2, '_>(move (@3), move (@2)) + drop[{impl Destruct for closure<'_0, '_1>}<'_, '_>] @1 + return +} + +// Full name: test_crate::main::{impl FnOnce<(&'_ (bool))> for closure<'_0, '_1>} +impl<'_0, '_1, '_2> FnOnce<(&'_ (bool))> for closure<'_0, '_1> { + parent_clause0 = {built_in impl MetaSized for closure<'_0, '_1>} + parent_clause1 = {built_in impl Sized for (&'_ (bool))} + parent_clause2 = {built_in impl Tuple for (&'_ (bool))} + parent_clause3 = {built_in impl Sized for (i32, bool, &'_ (i32))} + type Output = (i32, bool, &'_ (i32)) + fn call_once = {impl FnOnce<(&'_ (bool))> for closure<'_0, '_1>}::call_once<'_0, '_1, '_2> + non-dyn-compatible +} + +// Full name: test_crate::main::{impl FnMut<(&'_ (bool))> for closure<'_0, '_1>} +impl<'_0, '_1, '_2> FnMut<(&'_ (bool))> for closure<'_0, '_1> { + parent_clause0 = {built_in impl MetaSized for closure<'_0, '_1>} + parent_clause1 = {impl FnOnce<(&'_ (bool))> for closure<'_0, '_1>}<'_0, '_1, '_2> + parent_clause2 = {built_in impl Sized for (&'_ (bool))} + parent_clause3 = {built_in impl Tuple for (&'_ (bool))} + fn call_mut<'_0_1> = {impl FnMut<(&'_ (bool))> for closure<'_0, '_1>}::call_mut<'_0, '_1, '_2, '_0_1> + non-dyn-compatible +} + +// Full name: test_crate::main::{impl Fn<(&'_ (bool))> for closure<'_0, '_1>} +impl<'_0, '_1, '_2> Fn<(&'_ (bool))> for closure<'_0, '_1> { + parent_clause0 = {built_in impl MetaSized for closure<'_0, '_1>} + parent_clause1 = {impl FnMut<(&'_ (bool))> for closure<'_0, '_1>}<'_0, '_1, '_2> + parent_clause2 = {built_in impl Sized for (&'_ (bool))} + parent_clause3 = {built_in impl Tuple for (&'_ (bool))} + fn call<'_0_1> = {impl Fn<(&'_ (bool))> for closure<'_0, '_1>}::call<'_0, '_1, '_2, '_0_1> + non-dyn-compatible +} + +// Full name: test_crate::main::closure::{vtable_method} +fn {vtable_method}<'_0, '_1, '_2, '_3>(@1: &'_3 ((dyn Fn<(&'_ (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'_ (i32))>)), @2: ((&'_ (bool)))) -> (i32, bool, &'_ (i32)) +{ + let @0: (i32, bool, &'0 (i32)); // return + let @1: &'_3 ((dyn Fn<(&'1 (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'6 (i32))> + '2)); // arg #1 + let @2: ((&'7 (bool))); // arg #2 + let @3: &'_3 (closure<'_0, '_1>); // anonymous local + + storage_live(@3) + @3 := concretize<&'_3 ((dyn Fn<(&'8 (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'13 (i32))> + '9)), &'_3 (closure<'_0, '_1>)>(move (@1)) + @0 := {impl Fn<(&'_ (bool))> for closure<'_0, '_1>}::call<'_0, '_1, '_2, '_3>(move (@3), move (@2)) + return +} + +// Full name: test_crate::main::closure::{vtable_method} +fn {vtable_method}<'_0, '_1, '_2, '_3>(@1: &'_3 mut ((dyn FnMut<(&'_ (bool)), parent_clause1::Output = (i32, bool, &'_ (i32))>)), @2: ((&'_ (bool)))) -> (i32, bool, &'_ (i32)) +{ + let @0: (i32, bool, &'0 (i32)); // return + let @1: &'_3 mut ((dyn FnMut<(&'1 (bool)), parent_clause1::Output = (i32, bool, &'5 (i32))> + '2)); // arg #1 + let @2: ((&'6 (bool))); // arg #2 + let @3: &'_3 mut (closure<'_0, '_1>); // anonymous local + + storage_live(@3) + @3 := concretize<&'_3 mut ((dyn FnMut<(&'7 (bool)), parent_clause1::Output = (i32, bool, &'11 (i32))> + '8)), &'_3 mut (closure<'_0, '_1>)>(move (@1)) + @0 := {impl FnMut<(&'_ (bool))> for closure<'_0, '_1>}::call_mut<'_0, '_1, '_2, '_3>(move (@3), move (@2)) + return +} + +// Full name: test_crate::main::closure::{vtable_drop_shim} +unsafe fn {vtable_drop_shim}<'_0, '_1>(@1: *mut (dyn Fn<(&'_ (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'_ (i32))>)) +{ + let ret@0: (); // return + let dyn_self@1: *mut (dyn Fn<(&'0 (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'5 (i32))> + '1); // arg #1 + let target_self@2: *mut closure<'_0, '_1>; // local + + ret@0 := () + storage_live(target_self@2) + target_self@2 := concretize<*mut (dyn Fn<(&'6 (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'11 (i32))> + '7), *mut closure<'_0, '_1>>(move (dyn_self@1)) + drop[{impl Destruct for closure<'_0, '_1>}<'18, '19>] *(target_self@2) + return +} + +// Full name: test_crate::main::{impl FnOnce<(&'_ (bool))> for closure<'_0, '_1>}::{vtable} +fn {impl FnOnce<(&'_ (bool))> for closure<'_0, '_1>}::{vtable}<'_0, '_1>() -> core::ops::function::FnOnce::{vtable}<(&'_ (bool)), (i32, bool, &'_ (i32))> +{ + let ret@0: core::ops::function::FnOnce::{vtable}<(&'0 (bool)), (i32, bool, &'1 (i32))>; // return + let size@1: usize; // local + let align@2: usize; // local + + storage_live(size@1) + size@1 := size_of> + storage_live(align@2) + align@2 := align_of> + ret@0 := core::ops::function::FnOnce::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}) } + return +} + +// Full name: test_crate::main::{impl FnOnce<(&'_ (bool))> for closure<'_0, '_1>}::{vtable} +static {impl FnOnce<(&'_ (bool))> for closure<'_0, '_1>}::{vtable}<'_0, '_1>: core::ops::function::FnOnce::{vtable}<(&'_ (bool)), (i32, bool, &'_ (i32))> = {impl FnOnce<(&'_ (bool))> for closure<'_0, '_1>}::{vtable}() + +// Full name: test_crate::main::closure::{vtable_drop_shim} +unsafe fn {vtable_drop_shim}<'_0, '_1>(@1: *mut (dyn FnMut<(&'_ (bool)), parent_clause1::Output = (i32, bool, &'_ (i32))>)) +{ + let ret@0: (); // return + let dyn_self@1: *mut (dyn FnMut<(&'0 (bool)), parent_clause1::Output = (i32, bool, &'4 (i32))> + '1); // arg #1 + let target_self@2: *mut closure<'_0, '_1>; // local + + ret@0 := () + storage_live(target_self@2) + target_self@2 := concretize<*mut (dyn FnMut<(&'5 (bool)), parent_clause1::Output = (i32, bool, &'9 (i32))> + '6), *mut closure<'_0, '_1>>(move (dyn_self@1)) + drop[{impl Destruct for closure<'_0, '_1>}<'15, '16>] *(target_self@2) + return +} + +// Full name: test_crate::main::{impl FnMut<(&'_ (bool))> for closure<'_0, '_1>}::{vtable} +fn {impl FnMut<(&'_ (bool))> for closure<'_0, '_1>}::{vtable}<'_0, '_1>() -> core::ops::function::FnMut::{vtable}<(&'_ (bool)), (i32, bool, &'_ (i32))> +{ + let ret@0: core::ops::function::FnMut::{vtable}<(&'0 (bool)), (i32, bool, &'1 (i32))>; // return + let size@1: usize; // local + let align@2: usize; // local + let @3: fn<'_0_1>(&'_0_1 mut ((dyn FnMut<(&'13 (bool)), parent_clause1::Output = (i32, bool, &'17 (i32))> + '14)), (&'18 (bool))) -> (i32, bool, &'23 (i32)); // anonymous local + let @4: &'static (core::ops::function::FnOnce::{vtable}<(&'33 (bool)), (i32, bool, &'38 (i32))>); // anonymous local + + storage_live(size@1) + size@1 := size_of> + storage_live(align@2) + align@2 := align_of> + storage_live(@3) + @3 := cast {vtable_method}<'11, '_0, '_1, '12>, fn<'_0_1>(&'_0_1 mut ((dyn FnMut<(&'13 (bool)), parent_clause1::Output = (i32, bool, &'17 (i32))> + '14)), (&'18 (bool))) -> (i32, bool, &'23 (i32))>(const ({vtable_method}<'11, '_0, '_1, '12>)) + storage_live(@4) + @4 := &{impl FnOnce<(&'_ (bool))> for closure<'_0, '_1>}::{vtable} + ret@0 := core::ops::function::FnMut::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}), method_call_mut: move (@3), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4) } + return +} + +// Full name: test_crate::main::{impl FnMut<(&'_ (bool))> for closure<'_0, '_1>}::{vtable} +static {impl FnMut<(&'_ (bool))> for closure<'_0, '_1>}::{vtable}<'_0, '_1>: core::ops::function::FnMut::{vtable}<(&'_ (bool)), (i32, bool, &'_ (i32))> = {impl FnMut<(&'_ (bool))> for closure<'_0, '_1>}::{vtable}() + +// Full name: test_crate::main::closure::{vtable_drop_shim} +unsafe fn {vtable_drop_shim}<'_0, '_1>(@1: *mut (dyn Fn<(&'_ (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'_ (i32))>)) +{ + let ret@0: (); // return + let dyn_self@1: *mut (dyn Fn<(&'0 (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'5 (i32))> + '1); // arg #1 + let target_self@2: *mut closure<'_0, '_1>; // local + + ret@0 := () + storage_live(target_self@2) + target_self@2 := concretize<*mut (dyn Fn<(&'6 (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'11 (i32))> + '7), *mut closure<'_0, '_1>>(move (dyn_self@1)) + drop[{impl Destruct for closure<'_0, '_1>}<'18, '19>] *(target_self@2) + return +} + +// Full name: test_crate::main::{impl Fn<(&'_ (bool))> for closure<'_0, '_1>}::{vtable} +fn {impl Fn<(&'_ (bool))> for closure<'_0, '_1>}::{vtable}<'_0, '_1>() -> core::ops::function::Fn::{vtable}<(&'_ (bool)), (i32, bool, &'_ (i32))> +{ + let ret@0: core::ops::function::Fn::{vtable}<(&'0 (bool)), (i32, bool, &'1 (i32))>; // return + let size@1: usize; // local + let align@2: usize; // local + let @3: fn<'_0_1>(&'_0_1 ((dyn Fn<(&'14 (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'19 (i32))> + '15)), (&'20 (bool))) -> (i32, bool, &'26 (i32)); // anonymous local + let @4: &'static (core::ops::function::FnMut::{vtable}<(&'44 (bool)), (i32, bool, &'50 (i32))>); // anonymous local + + storage_live(size@1) + size@1 := size_of> + storage_live(align@2) + align@2 := align_of> + storage_live(@3) + @3 := cast {vtable_method}<'12, '_0, '_1, '13>, fn<'_0_1>(&'_0_1 ((dyn Fn<(&'14 (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'19 (i32))> + '15)), (&'20 (bool))) -> (i32, bool, &'26 (i32))>(const ({vtable_method}<'12, '_0, '_1, '13>)) + storage_live(@4) + @4 := &{impl FnMut<(&'_ (bool))> for closure<'_0, '_1>}::{vtable} + ret@0 := core::ops::function::Fn::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}), method_call: move (@3), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4) } + return +} + +// Full name: test_crate::main::{impl Fn<(&'_ (bool))> for closure<'_0, '_1>}::{vtable} +static {impl Fn<(&'_ (bool))> for closure<'_0, '_1>}::{vtable}<'_0, '_1>: core::ops::function::Fn::{vtable}<(&'_ (bool)), (i32, bool, &'_ (i32))> = {impl Fn<(&'_ (bool))> for closure<'_0, '_1>}::{vtable}() + +// Full name: test_crate::main +fn main() +{ + let @0: (); // return + let x@1: i32; // local + let y@2: i32; // local + let @3: (i32, bool, &'0 (i32)); // anonymous local + let @4: &'1 ((dyn for<'a> Fn<(&'a (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'5 (i32))> + '2)); // anonymous local + let @5: &'6 (closure<'_, '_>); // anonymous local + let @6: &'6 (closure<'_, '_>); // anonymous local + let @7: closure<'_, '_>; // anonymous local + let @8: &'0 (i32); // anonymous local + let @9: &'0 (i32); // anonymous local + let @10: &'7 (bool); // anonymous local + let @11: &'7 (bool); // anonymous local + let @12: &'7 (bool); // anonymous local + let @13: &'_ (bool); // anonymous local + let @14: bool; // anonymous local + + storage_live(@13) + storage_live(@14) + @14 := const (false) + @13 := &@14 + storage_live(@12) + @0 := () + storage_live(x@1) + x@1 := const (2 : i32) + storage_live(y@2) + y@2 := const (3 : i32) + storage_live(@3) + storage_live(@4) + storage_live(@5) + storage_live(@6) + storage_live(@7) + storage_live(@8) + @8 := &x@1 + storage_live(@9) + @9 := &y@2 + @7 := closure { 0: move (@8), 1: move (@9) } + storage_dead(@9) + storage_dead(@8) + @6 := &@7 + @5 := &*(@6) + @4 := unsize_cast<&'6 (closure<'_, '_>), &'1 ((dyn for<'a> Fn<(&'a (bool)), parent_clause1::parent_clause1::Output = (i32, bool, &'5 (i32))> + '2)), {impl Fn<(&'_ (bool))> for closure<'_0, '_1>}<'_, '_, '_> with {impl Fn<(&'_ (bool))> for closure<'_0, '_1>}::{vtable}>(move (@5)) + storage_dead(@5) + storage_live(@10) + storage_live(@11) + @12 := move (@13) + @11 := &*(@12) + @10 := &*(@11) + @3 := call_test<'8, '9, '_, i32>[{built_in impl Sized for i32}](move (@4), move (@10)) + storage_dead(@10) + storage_dead(@4) + storage_dead(@11) + storage_dead(@7) + storage_dead(@6) + storage_dead(@3) + @0 := () + storage_dead(y@2) + storage_dead(x@1) + return +} + + + diff --git a/charon/tests/ui/dyn-closure-regions.rs b/charon/tests/ui/dyn-closure-regions.rs new file mode 100644 index 000000000..4bc8bb976 --- /dev/null +++ b/charon/tests/ui/dyn-closure-regions.rs @@ -0,0 +1,9 @@ +fn call_test<'b, 'c : 'b, T>(f : &dyn for<'a> Fn(&'a bool) -> (T, bool, &'b T), arg: &'c bool) -> (T, bool, &'b T) { + f(arg) +} + +fn main() { + let x = 2; + let y = 3; + call_test(&|a| (x, *a, &y), &false); +} \ No newline at end of file diff --git a/charon/tests/ui/dyn-trait.out b/charon/tests/ui/dyn-trait.out index afe13c4e7..3c0589890 100644 --- a/charon/tests/ui/dyn-trait.out +++ b/charon/tests/ui/dyn-trait.out @@ -22,6 +22,8 @@ pub struct Error {} opaque type core::fmt::Display::{vtable} +opaque type core::marker::MetaSized::{vtable} + // Full name: core::marker::MetaSized #[lang_item("meta_sized")] pub trait MetaSized @@ -67,8 +69,6 @@ pub trait Tuple vtable: core::marker::Tuple::{vtable} } -opaque type core::ops::function::Fn::{vtable} - // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -82,6 +82,12 @@ pub trait FnOnce vtable: core::ops::function::FnOnce::{vtable} } +struct core::ops::function::FnOnce::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn FnOnce)), +} + // Full name: core::ops::function::FnMut #[lang_item("fn_mut")] pub trait FnMut @@ -94,6 +100,24 @@ pub trait FnMut vtable: core::ops::function::FnMut::{vtable} } +struct core::ops::function::FnMut::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn FnMut)), + method_call_mut: fn<'_0_1>(&'_0_1 mut ((dyn FnMut)), Args) -> Ty0, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnOnce::{vtable}), +} + +struct core::ops::function::Fn::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn Fn)), + method_call: fn<'_0_1>(&'_0_1 ((dyn Fn)), Args) -> Ty0, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnMut::{vtable}), +} + // Full name: core::ops::function::Fn #[lang_item("r#fn")] pub trait Fn diff --git a/charon/tests/ui/simple/closure_ref.out b/charon/tests/ui/simple/closure_ref.out new file mode 100644 index 000000000..6adea4f1e --- /dev/null +++ b/charon/tests/ui/simple/closure_ref.out @@ -0,0 +1,383 @@ +# Final LLBC before serialization: + +opaque type core::marker::MetaSized::{vtable} + +// Full name: core::marker::MetaSized +#[lang_item("meta_sized")] +pub trait MetaSized + +// Full name: core::marker::Sized +#[lang_item("sized")] +pub trait Sized +{ + parent_clause0 : [@TraitClause0]: MetaSized + non-dyn-compatible +} + +// Full name: core::marker::Destruct +#[lang_item("destruct")] +pub trait Destruct +{ + fn drop_in_place = core::marker::Destruct::drop_in_place + vtable: core::marker::Destruct::{vtable} +} + +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) += + +// Full name: core::marker::Tuple +#[lang_item("tuple_trait")] +pub trait Tuple +{ + parent_clause0 : [@TraitClause0]: MetaSized + vtable: core::marker::Tuple::{vtable} +} + +// Full name: core::ops::function::FnOnce +#[lang_item("fn_once")] +pub trait FnOnce +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Sized + parent_clause2 : [@TraitClause2]: Tuple + parent_clause3 : [@TraitClause3]: Sized + type Output + fn call_once = core::ops::function::FnOnce::call_once[Self] + vtable: core::ops::function::FnOnce::{vtable} +} + +struct core::ops::function::FnOnce::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn FnOnce)), +} + +// Full name: core::ops::function::FnMut +#[lang_item("fn_mut")] +pub trait FnMut +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnOnce + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call_mut<'_0_1> = core::ops::function::FnMut::call_mut<'_0_1, Self, Args>[Self] + vtable: core::ops::function::FnMut::{vtable} +} + +struct core::ops::function::FnMut::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn FnMut)), + method_call_mut: fn<'_0_1>(&'_0_1 mut ((dyn FnMut)), Args) -> Ty0, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnOnce::{vtable}), +} + +struct core::ops::function::Fn::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn Fn)), + method_call: fn<'_0_1>(&'_0_1 ((dyn Fn)), Args) -> Ty0, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnMut::{vtable}), +} + +// Full name: core::ops::function::Fn +#[lang_item("r#fn")] +pub trait Fn +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnMut + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call<'_0_1> = core::ops::function::Fn::call<'_0_1, Self, Args>[Self] + vtable: core::ops::function::Fn::{vtable} +} + +pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output +where + [@TraitClause0]: Fn, += + +pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output +where + [@TraitClause0]: FnMut, += + +pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> @TraitClause0::Output +where + [@TraitClause0]: FnOnce, += + +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + +// Full name: test_crate::main::closure +struct closure<'_0> { + &'_0 (i32), +} + +// Full name: test_crate::main::{impl Fn<()> for closure<'_0>}::call +fn {impl Fn<()> for closure<'_0>}::call<'_0, '_1>(@1: &'_1 (closure<'_0>), @2: ()) -> i32 +{ + let @0: i32; // return + let @1: &'0 (closure<'_0>); // arg #1 + let tupled_args@2: (); // arg #2 + + @0 := copy (*((*(@1)).0)) + return +} + +// Full name: test_crate::main::{impl FnMut<()> for closure<'_0>}::call_mut +fn {impl FnMut<()> for closure<'_0>}::call_mut<'_0, '_1>(@1: &'_1 mut (closure<'_0>), @2: ()) -> i32 +{ + let @0: i32; // return + let state@1: &'_1 mut (closure<'_0>); // arg #1 + let args@2: (); // arg #2 + let @3: &'0 (closure<'_0>); // anonymous local + + storage_live(@3) + @3 := &*(state@1) + @0 := {impl Fn<()> for closure<'_0>}::call<'_0, '2>(move (@3), move (args@2)) + return +} + +// Full name: test_crate::main::closure::{impl Destruct for closure<'_0>}::drop_in_place +unsafe fn {impl Destruct for closure<'_0>}::drop_in_place<'_0>(@1: *mut closure<'_0>) += + +// Full name: test_crate::main::closure::{impl Destruct for closure<'_0>} +impl<'_0> Destruct for closure<'_0> { + fn drop_in_place = {impl Destruct for closure<'_0>}::drop_in_place<'_0> + non-dyn-compatible +} + +// Full name: test_crate::main::{impl FnOnce<()> for closure<'_0>}::call_once +fn {impl FnOnce<()> for closure<'_0>}::call_once<'_0>(@1: closure<'_0>, @2: ()) -> i32 +{ + let @0: i32; // return + let @1: closure<'_0>; // arg #1 + let @2: (); // arg #2 + let @3: &'0 mut (closure<'_0>); // anonymous local + + storage_live(@3) + @3 := &mut @1 + @0 := {impl FnMut<()> for closure<'_0>}::call_mut<'_0, '_>(move (@3), move (@2)) + drop[{impl Destruct for closure<'_0>}<'_>] @1 + return +} + +// Full name: test_crate::main::{impl FnOnce<()> for closure<'_0>} +impl<'_0> FnOnce<()> for closure<'_0> { + parent_clause0 = {built_in impl MetaSized for closure<'_0>} + parent_clause1 = {built_in impl Sized for ()} + parent_clause2 = {built_in impl Tuple for ()} + parent_clause3 = {built_in impl Sized for i32} + type Output = i32 + fn call_once = {impl FnOnce<()> for closure<'_0>}::call_once<'_0> + non-dyn-compatible +} + +// Full name: test_crate::main::{impl FnMut<()> for closure<'_0>} +impl<'_0> FnMut<()> for closure<'_0> { + parent_clause0 = {built_in impl MetaSized for closure<'_0>} + parent_clause1 = {impl FnOnce<()> for closure<'_0>}<'_0> + parent_clause2 = {built_in impl Sized for ()} + parent_clause3 = {built_in impl Tuple for ()} + fn call_mut<'_0_1> = {impl FnMut<()> for closure<'_0>}::call_mut<'_0, '_0_1> + non-dyn-compatible +} + +// Full name: test_crate::main::{impl Fn<()> for closure<'_0>} +impl<'_0> Fn<()> for closure<'_0> { + parent_clause0 = {built_in impl MetaSized for closure<'_0>} + parent_clause1 = {impl FnMut<()> for closure<'_0>}<'_0> + parent_clause2 = {built_in impl Sized for ()} + parent_clause3 = {built_in impl Tuple for ()} + fn call<'_0_1> = {impl Fn<()> for closure<'_0>}::call<'_0, '_0_1> + non-dyn-compatible +} + +// Full name: test_crate::main::closure::{vtable_method} +fn {vtable_method}<'_0, '_1>(@1: &'_1 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32>)), @2: (())) -> i32 +{ + let @0: i32; // return + let @1: &'_1 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '0)); // arg #1 + let @2: (()); // arg #2 + let @3: &'_1 (closure<'_0>); // anonymous local + + storage_live(@3) + @3 := concretize<&'_1 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '1)), &'_1 (closure<'_0>)>(move (@1)) + @0 := {impl Fn<()> for closure<'_0>}::call<'_0, '_1>(move (@3), move (@2)) + return +} + +// Full name: test_crate::main::closure::{vtable_method} +fn {vtable_method}<'_0, '_1>(@1: &'_1 mut ((dyn FnMut<(), parent_clause1::Output = i32>)), @2: (())) -> i32 +{ + let @0: i32; // return + let @1: &'_1 mut ((dyn FnMut<(), parent_clause1::Output = i32> + '0)); // arg #1 + let @2: (()); // arg #2 + let @3: &'_1 mut (closure<'_0>); // anonymous local + + storage_live(@3) + @3 := concretize<&'_1 mut ((dyn FnMut<(), parent_clause1::Output = i32> + '1)), &'_1 mut (closure<'_0>)>(move (@1)) + @0 := {impl FnMut<()> for closure<'_0>}::call_mut<'_0, '_1>(move (@3), move (@2)) + return +} + +// Full name: test_crate::main::closure::{vtable_drop_shim} +unsafe fn {vtable_drop_shim}<'_0>(@1: *mut (dyn Fn<(), parent_clause1::parent_clause1::Output = i32>)) +{ + let ret@0: (); // return + let dyn_self@1: *mut (dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '0); // arg #1 + let target_self@2: *mut closure<'_0>; // local + + ret@0 := () + storage_live(target_self@2) + target_self@2 := concretize<*mut (dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '1), *mut closure<'_0>>(move (dyn_self@1)) + drop[{impl Destruct for closure<'_0>}<'3>] *(target_self@2) + return +} + +// Full name: test_crate::main::{impl FnOnce<()> for closure<'_0>}::{vtable} +fn {impl FnOnce<()> for closure<'_0>}::{vtable}<'_0>() -> core::ops::function::FnOnce::{vtable}<(), i32> +{ + let ret@0: core::ops::function::FnOnce::{vtable}<(), i32>; // return + let size@1: usize; // local + let align@2: usize; // local + + storage_live(size@1) + size@1 := size_of> + storage_live(align@2) + align@2 := align_of> + ret@0 := core::ops::function::FnOnce::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}) } + return +} + +// Full name: test_crate::main::{impl FnOnce<()> for closure<'_0>}::{vtable} +static {impl FnOnce<()> for closure<'_0>}::{vtable}<'_0>: core::ops::function::FnOnce::{vtable}<(), i32> = {impl FnOnce<()> for closure<'_0>}::{vtable}() + +// Full name: test_crate::main::closure::{vtable_drop_shim} +unsafe fn {vtable_drop_shim}<'_0>(@1: *mut (dyn FnMut<(), parent_clause1::Output = i32>)) +{ + let ret@0: (); // return + let dyn_self@1: *mut (dyn FnMut<(), parent_clause1::Output = i32> + '0); // arg #1 + let target_self@2: *mut closure<'_0>; // local + + ret@0 := () + storage_live(target_self@2) + target_self@2 := concretize<*mut (dyn FnMut<(), parent_clause1::Output = i32> + '1), *mut closure<'_0>>(move (dyn_self@1)) + drop[{impl Destruct for closure<'_0>}<'3>] *(target_self@2) + return +} + +// Full name: test_crate::main::{impl FnMut<()> for closure<'_0>}::{vtable} +fn {impl FnMut<()> for closure<'_0>}::{vtable}<'_0>() -> core::ops::function::FnMut::{vtable}<(), i32> +{ + let ret@0: core::ops::function::FnMut::{vtable}<(), i32>; // return + let size@1: usize; // local + let align@2: usize; // local + let @3: fn<'_0_1>(&'_0_1 mut ((dyn FnMut<(), parent_clause1::Output = i32> + '2)), ()) -> i32; // anonymous local + let @4: &'static (core::ops::function::FnOnce::{vtable}<(), i32>); // anonymous local + + storage_live(size@1) + size@1 := size_of> + storage_live(align@2) + align@2 := align_of> + storage_live(@3) + @3 := cast {vtable_method}<'1, '_0>, fn<'_0_1>(&'_0_1 mut ((dyn FnMut<(), parent_clause1::Output = i32> + '2)), ()) -> i32>(const ({vtable_method}<'1, '_0>)) + storage_live(@4) + @4 := &{impl FnOnce<()> for closure<'_0>}::{vtable} + ret@0 := core::ops::function::FnMut::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}), method_call_mut: move (@3), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4) } + return +} + +// Full name: test_crate::main::{impl FnMut<()> for closure<'_0>}::{vtable} +static {impl FnMut<()> for closure<'_0>}::{vtable}<'_0>: core::ops::function::FnMut::{vtable}<(), i32> = {impl FnMut<()> for closure<'_0>}::{vtable}() + +// Full name: test_crate::main::closure::{vtable_drop_shim} +unsafe fn {vtable_drop_shim}<'_0>(@1: *mut (dyn Fn<(), parent_clause1::parent_clause1::Output = i32>)) +{ + let ret@0: (); // return + let dyn_self@1: *mut (dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '0); // arg #1 + let target_self@2: *mut closure<'_0>; // local + + ret@0 := () + storage_live(target_self@2) + target_self@2 := concretize<*mut (dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '1), *mut closure<'_0>>(move (dyn_self@1)) + drop[{impl Destruct for closure<'_0>}<'3>] *(target_self@2) + return +} + +// Full name: test_crate::main::{impl Fn<()> for closure<'_0>}::{vtable} +fn {impl Fn<()> for closure<'_0>}::{vtable}<'_0>() -> core::ops::function::Fn::{vtable}<(), i32> +{ + let ret@0: core::ops::function::Fn::{vtable}<(), i32>; // return + let size@1: usize; // local + let align@2: usize; // local + let @3: fn<'_0_1>(&'_0_1 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '2)), ()) -> i32; // anonymous local + let @4: &'static (core::ops::function::FnMut::{vtable}<(), i32>); // anonymous local + + storage_live(size@1) + size@1 := size_of> + storage_live(align@2) + align@2 := align_of> + storage_live(@3) + @3 := cast {vtable_method}<'1, '_0>, fn<'_0_1>(&'_0_1 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '2)), ()) -> i32>(const ({vtable_method}<'1, '_0>)) + storage_live(@4) + @4 := &{impl FnMut<()> for closure<'_0>}::{vtable} + ret@0 := core::ops::function::Fn::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}), method_call: move (@3), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4) } + return +} + +// Full name: test_crate::main::{impl Fn<()> for closure<'_0>}::{vtable} +static {impl Fn<()> for closure<'_0>}::{vtable}<'_0>: core::ops::function::Fn::{vtable}<(), i32> = {impl Fn<()> for closure<'_0>}::{vtable}() + +// Full name: test_crate::main +fn main() +{ + let @0: (); // return + let i@1: i32; // local + let ref_i@2: &'0 (i32); // local + let f@3: closure<'_>; // local + let @4: &'0 (i32); // anonymous local + let dyn_f@5: &'1 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '2)); // local + let @6: &'3 (closure<'_>); // anonymous local + let @7: &'3 (closure<'_>); // anonymous local + + @0 := () + storage_live(i@1) + i@1 := const (42 : i32) + storage_live(ref_i@2) + ref_i@2 := &i@1 + storage_live(f@3) + storage_live(@4) + @4 := &*(ref_i@2) + f@3 := closure { 0: move (@4) } + storage_dead(@4) + storage_live(dyn_f@5) + storage_live(@6) + storage_live(@7) + @7 := &f@3 + @6 := &*(@7) + dyn_f@5 := unsize_cast<&'3 (closure<'_>), &'1 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '2)), {impl Fn<()> for closure<'_0>}<'_> with {impl Fn<()> for closure<'_0>}::{vtable}>(move (@6)) + storage_dead(@6) + storage_dead(@7) + @0 := () + storage_dead(dyn_f@5) + storage_dead(f@3) + storage_dead(ref_i@2) + storage_dead(i@1) + return +} + + + diff --git a/charon/tests/ui/simple/closure_ref.rs b/charon/tests/ui/simple/closure_ref.rs new file mode 100644 index 000000000..0d9f0f438 --- /dev/null +++ b/charon/tests/ui/simple/closure_ref.rs @@ -0,0 +1,6 @@ +fn main() { + let i = 42; + let ref_i = &i; + let f = || *ref_i; + let dyn_f: &dyn Fn() -> i32 = &f; +} \ No newline at end of file diff --git a/charon/tests/ui/simple/dyn-broken-assoc-type-constraint.out b/charon/tests/ui/simple/dyn-broken-assoc-type-constraint.out index 861c99bb4..714c68cf8 100644 --- a/charon/tests/ui/simple/dyn-broken-assoc-type-constraint.out +++ b/charon/tests/ui/simple/dyn-broken-assoc-type-constraint.out @@ -132,7 +132,7 @@ where size@1 := size_of storage_live(align@2) align@2 := align_of - ret@0 := test_crate::Broken::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}[@TraitClause0]), method_broken: const ({vtable_method}<'1, T>[@TraitClause0]), super_trait_0: const (Opaque(missing supertrait vtable)) } + ret@0 := test_crate::Broken::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}[@TraitClause0]), method_broken: const ({vtable_method}<'1, T>[@TraitClause0]), super_trait_0: const (Opaque(generic supertrait vtable)) } return } diff --git a/charon/tests/ui/simple/dyn-fn.out b/charon/tests/ui/simple/dyn-fn.out index 8e019ef8d..72170e69d 100644 --- a/charon/tests/ui/simple/dyn-fn.out +++ b/charon/tests/ui/simple/dyn-fn.out @@ -1,5 +1,7 @@ # Final LLBC before serialization: +opaque type core::marker::MetaSized::{vtable} + // Full name: core::marker::MetaSized #[lang_item("meta_sized")] pub trait MetaSized @@ -31,8 +33,6 @@ pub trait Tuple vtable: core::marker::Tuple::{vtable} } -opaque type core::ops::function::Fn::{vtable} - // Full name: core::ops::function::FnOnce #[lang_item("fn_once")] pub trait FnOnce @@ -46,6 +46,12 @@ pub trait FnOnce vtable: core::ops::function::FnOnce::{vtable} } +struct core::ops::function::FnOnce::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn FnOnce)), +} + // Full name: core::ops::function::FnMut #[lang_item("fn_mut")] pub trait FnMut @@ -58,6 +64,24 @@ pub trait FnMut vtable: core::ops::function::FnMut::{vtable} } +struct core::ops::function::FnMut::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn FnMut)), + method_call_mut: fn<'_0_1>(&'_0_1 mut ((dyn FnMut)), Args) -> Ty0, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnOnce::{vtable}), +} + +struct core::ops::function::Fn::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn Fn)), + method_call: fn<'_0_1>(&'_0_1 ((dyn Fn)), Args) -> Ty0, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnMut::{vtable}), +} + // Full name: core::ops::function::Fn #[lang_item("r#fn")] pub trait Fn @@ -119,7 +143,7 @@ fn takes_fn<'_0>(@1: &'_0 ((dyn for<'a> Fn<(&'a mut (u32)), parent_clause1::pare @7 := &mut counter@2 @6 := &two-phase-mut *(@7) @5 := (move (@6)) - @3 := Fn<(dyn for<'a> Fn<(&'a mut (u32)), parent_clause1::parent_clause1::Output = bool> + '5), (&'8 mut (u32))>::call<'_>(move (@4), move (@5)) + @3 := (copy ((*(@4.metadata)).method_call))(move (@4), move (@5)) if move (@3) { storage_dead(@7) storage_dead(@6) @@ -229,6 +253,142 @@ impl<'_0> Fn<(&'_ mut (u32))> for closure { non-dyn-compatible } +// Full name: test_crate::gives_fn::closure::{vtable_method} +fn {vtable_method}<'_0, '_1>(@1: &'_1 ((dyn Fn<(&'_ mut (u32)), parent_clause1::parent_clause1::Output = bool>)), @2: ((&'_ mut (u32)))) -> bool +{ + let @0: bool; // return + let @1: &'_1 ((dyn Fn<(&'0 mut (u32)), parent_clause1::parent_clause1::Output = bool> + '1)); // arg #1 + let @2: ((&'5 mut (u32))); // arg #2 + let @3: &'_1 (closure); // anonymous local + + storage_live(@3) + @3 := concretize<&'_1 ((dyn Fn<(&'6 mut (u32)), parent_clause1::parent_clause1::Output = bool> + '7)), &'_1 (closure)>(move (@1)) + @0 := {impl Fn<(&'_ mut (u32))> for closure}::call<'_0, '_1>(move (@3), move (@2)) + return +} + +// Full name: test_crate::gives_fn::closure::{vtable_method} +fn {vtable_method}<'_0, '_1>(@1: &'_1 mut ((dyn FnMut<(&'_ mut (u32)), parent_clause1::Output = bool>)), @2: ((&'_ mut (u32)))) -> bool +{ + let @0: bool; // return + let @1: &'_1 mut ((dyn FnMut<(&'0 mut (u32)), parent_clause1::Output = bool> + '1)); // arg #1 + let @2: ((&'4 mut (u32))); // arg #2 + let @3: &'_1 mut (closure); // anonymous local + + storage_live(@3) + @3 := concretize<&'_1 mut ((dyn FnMut<(&'5 mut (u32)), parent_clause1::Output = bool> + '6)), &'_1 mut (closure)>(move (@1)) + @0 := {impl FnMut<(&'_ mut (u32))> for closure}::call_mut<'_0, '_1>(move (@3), move (@2)) + return +} + +// Full name: test_crate::gives_fn::closure::{vtable_drop_shim} +unsafe fn {vtable_drop_shim}(@1: *mut (dyn Fn<(&'_ mut (u32)), parent_clause1::parent_clause1::Output = bool>)) +{ + let ret@0: (); // return + let dyn_self@1: *mut (dyn Fn<(&'0 mut (u32)), parent_clause1::parent_clause1::Output = bool> + '1); // arg #1 + let target_self@2: *mut closure; // local + + ret@0 := () + storage_live(target_self@2) + target_self@2 := concretize<*mut (dyn Fn<(&'5 mut (u32)), parent_clause1::parent_clause1::Output = bool> + '6), *mut closure>(move (dyn_self@1)) + drop[{impl Destruct for closure}] *(target_self@2) + return +} + +// Full name: test_crate::gives_fn::{impl FnOnce<(&'_ mut (u32))> for closure}::{vtable} +fn {impl FnOnce<(&'_ mut (u32))> for closure}::{vtable}() -> core::ops::function::FnOnce::{vtable}<(&'_ mut (u32)), bool> +{ + let ret@0: core::ops::function::FnOnce::{vtable}<(&'0 mut (u32)), bool>; // return + let size@1: usize; // local + let align@2: usize; // local + + storage_live(size@1) + size@1 := size_of + storage_live(align@2) + align@2 := align_of + ret@0 := core::ops::function::FnOnce::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}) } + return +} + +// Full name: test_crate::gives_fn::{impl FnOnce<(&'_ mut (u32))> for closure}::{vtable} +static {impl FnOnce<(&'_ mut (u32))> for closure}::{vtable}: core::ops::function::FnOnce::{vtable}<(&'_ mut (u32)), bool> = {impl FnOnce<(&'_ mut (u32))> for closure}::{vtable}() + +// Full name: test_crate::gives_fn::closure::{vtable_drop_shim} +unsafe fn {vtable_drop_shim}(@1: *mut (dyn FnMut<(&'_ mut (u32)), parent_clause1::Output = bool>)) +{ + let ret@0: (); // return + let dyn_self@1: *mut (dyn FnMut<(&'0 mut (u32)), parent_clause1::Output = bool> + '1); // arg #1 + let target_self@2: *mut closure; // local + + ret@0 := () + storage_live(target_self@2) + target_self@2 := concretize<*mut (dyn FnMut<(&'4 mut (u32)), parent_clause1::Output = bool> + '5), *mut closure>(move (dyn_self@1)) + drop[{impl Destruct for closure}] *(target_self@2) + return +} + +// Full name: test_crate::gives_fn::{impl FnMut<(&'_ mut (u32))> for closure}::{vtable} +fn {impl FnMut<(&'_ mut (u32))> for closure}::{vtable}() -> core::ops::function::FnMut::{vtable}<(&'_ mut (u32)), bool> +{ + let ret@0: core::ops::function::FnMut::{vtable}<(&'0 mut (u32)), bool>; // return + let size@1: usize; // local + let align@2: usize; // local + let @3: fn<'_0_1>(&'_0_1 mut ((dyn FnMut<(&'9 mut (u32)), parent_clause1::Output = bool> + '10)), (&'13 mut (u32))) -> bool; // anonymous local + let @4: &'static (core::ops::function::FnOnce::{vtable}<(&'25 mut (u32)), bool>); // anonymous local + + storage_live(size@1) + size@1 := size_of + storage_live(align@2) + align@2 := align_of + storage_live(@3) + @3 := cast {vtable_method}<'7, '8>, fn<'_0_1>(&'_0_1 mut ((dyn FnMut<(&'9 mut (u32)), parent_clause1::Output = bool> + '10)), (&'13 mut (u32))) -> bool>(const ({vtable_method}<'7, '8>)) + storage_live(@4) + @4 := &{impl FnOnce<(&'_ mut (u32))> for closure}::{vtable} + ret@0 := core::ops::function::FnMut::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}), method_call_mut: move (@3), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4) } + return +} + +// Full name: test_crate::gives_fn::{impl FnMut<(&'_ mut (u32))> for closure}::{vtable} +static {impl FnMut<(&'_ mut (u32))> for closure}::{vtable}: core::ops::function::FnMut::{vtable}<(&'_ mut (u32)), bool> = {impl FnMut<(&'_ mut (u32))> for closure}::{vtable}() + +// Full name: test_crate::gives_fn::closure::{vtable_drop_shim} +unsafe fn {vtable_drop_shim}(@1: *mut (dyn Fn<(&'_ mut (u32)), parent_clause1::parent_clause1::Output = bool>)) +{ + let ret@0: (); // return + let dyn_self@1: *mut (dyn Fn<(&'0 mut (u32)), parent_clause1::parent_clause1::Output = bool> + '1); // arg #1 + let target_self@2: *mut closure; // local + + ret@0 := () + storage_live(target_self@2) + target_self@2 := concretize<*mut (dyn Fn<(&'5 mut (u32)), parent_clause1::parent_clause1::Output = bool> + '6), *mut closure>(move (dyn_self@1)) + drop[{impl Destruct for closure}] *(target_self@2) + return +} + +// Full name: test_crate::gives_fn::{impl Fn<(&'_ mut (u32))> for closure}::{vtable} +fn {impl Fn<(&'_ mut (u32))> for closure}::{vtable}() -> core::ops::function::Fn::{vtable}<(&'_ mut (u32)), bool> +{ + let ret@0: core::ops::function::Fn::{vtable}<(&'0 mut (u32)), bool>; // return + let size@1: usize; // local + let align@2: usize; // local + let @3: fn<'_0_1>(&'_0_1 ((dyn Fn<(&'10 mut (u32)), parent_clause1::parent_clause1::Output = bool> + '11)), (&'15 mut (u32))) -> bool; // anonymous local + let @4: &'static (core::ops::function::FnMut::{vtable}<(&'35 mut (u32)), bool>); // anonymous local + + storage_live(size@1) + size@1 := size_of + storage_live(align@2) + align@2 := align_of + storage_live(@3) + @3 := cast {vtable_method}<'8, '9>, fn<'_0_1>(&'_0_1 ((dyn Fn<(&'10 mut (u32)), parent_clause1::parent_clause1::Output = bool> + '11)), (&'15 mut (u32))) -> bool>(const ({vtable_method}<'8, '9>)) + storage_live(@4) + @4 := &{impl FnMut<(&'_ mut (u32))> for closure}::{vtable} + ret@0 := core::ops::function::Fn::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}), method_call: move (@3), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4) } + return +} + +// Full name: test_crate::gives_fn::{impl Fn<(&'_ mut (u32))> for closure}::{vtable} +static {impl Fn<(&'_ mut (u32))> for closure}::{vtable}: core::ops::function::Fn::{vtable}<(&'_ mut (u32)), bool> = {impl Fn<(&'_ mut (u32))> for closure}::{vtable}() + // Full name: test_crate::gives_fn fn gives_fn() { @@ -252,7 +412,7 @@ fn gives_fn() @4 := move (@5) @3 := &*(@4) @2 := &*(@3) - @1 := unsize_cast<&'4 (closure), &'0 ((dyn for<'a> Fn<(&'a mut (u32)), parent_clause1::parent_clause1::Output = bool> + '1)), {impl Fn<(&'_ mut (u32))> for closure}<'_> with ?>(move (@2)) + @1 := unsize_cast<&'4 (closure), &'0 ((dyn for<'a> Fn<(&'a mut (u32)), parent_clause1::parent_clause1::Output = bool> + '1)), {impl Fn<(&'_ mut (u32))> for closure}<'_> with {impl Fn<(&'_ mut (u32))> for closure}::{vtable}>(move (@2)) storage_dead(@2) @0 := takes_fn<'_>(move (@1)) storage_dead(@1) diff --git a/charon/tests/ui/simple/simple_closure.out b/charon/tests/ui/simple/simple_closure.out new file mode 100644 index 000000000..cf22461b0 --- /dev/null +++ b/charon/tests/ui/simple/simple_closure.out @@ -0,0 +1,369 @@ +# Final LLBC before serialization: + +opaque type core::marker::MetaSized::{vtable} + +// Full name: core::marker::MetaSized +#[lang_item("meta_sized")] +pub trait MetaSized + +// Full name: core::marker::Sized +#[lang_item("sized")] +pub trait Sized +{ + parent_clause0 : [@TraitClause0]: MetaSized + non-dyn-compatible +} + +// Full name: core::marker::Destruct +#[lang_item("destruct")] +pub trait Destruct +{ + fn drop_in_place = core::marker::Destruct::drop_in_place + vtable: core::marker::Destruct::{vtable} +} + +unsafe fn core::marker::Destruct::drop_in_place(@1: *mut Self) += + +// Full name: core::marker::Tuple +#[lang_item("tuple_trait")] +pub trait Tuple +{ + parent_clause0 : [@TraitClause0]: MetaSized + vtable: core::marker::Tuple::{vtable} +} + +// Full name: core::ops::function::FnOnce +#[lang_item("fn_once")] +pub trait FnOnce +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Sized + parent_clause2 : [@TraitClause2]: Tuple + parent_clause3 : [@TraitClause3]: Sized + type Output + fn call_once = core::ops::function::FnOnce::call_once[Self] + vtable: core::ops::function::FnOnce::{vtable} +} + +struct core::ops::function::FnOnce::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn FnOnce)), +} + +// Full name: core::ops::function::FnMut +#[lang_item("fn_mut")] +pub trait FnMut +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnOnce + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call_mut<'_0_1> = core::ops::function::FnMut::call_mut<'_0_1, Self, Args>[Self] + vtable: core::ops::function::FnMut::{vtable} +} + +struct core::ops::function::FnMut::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn FnMut)), + method_call_mut: fn<'_0_1>(&'_0_1 mut ((dyn FnMut)), Args) -> Ty0, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnOnce::{vtable}), +} + +struct core::ops::function::Fn::{vtable} { + size: usize, + align: usize, + drop: unsafe fn(*mut (dyn Fn)), + method_call: fn<'_0_1>(&'_0_1 ((dyn Fn)), Args) -> Ty0, + super_trait_0: &'static (core::marker::MetaSized::{vtable}), + super_trait_1: &'static (core::ops::function::FnMut::{vtable}), +} + +// Full name: core::ops::function::Fn +#[lang_item("r#fn")] +pub trait Fn +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: FnMut + parent_clause2 : [@TraitClause2]: Sized + parent_clause3 : [@TraitClause3]: Tuple + fn call<'_0_1> = core::ops::function::Fn::call<'_0_1, Self, Args>[Self] + vtable: core::ops::function::Fn::{vtable} +} + +pub fn core::ops::function::Fn::call<'_0, Self, Args>(@1: &'_0 (Self), @2: Args) -> @TraitClause0::parent_clause1::parent_clause1::Output +where + [@TraitClause0]: Fn, += + +pub fn core::ops::function::FnMut::call_mut<'_0, Self, Args>(@1: &'_0 mut (Self), @2: Args) -> @TraitClause0::parent_clause1::Output +where + [@TraitClause0]: FnMut, += + +pub fn core::ops::function::FnOnce::call_once(@1: Self, @2: Args) -> @TraitClause0::Output +where + [@TraitClause0]: FnOnce, += + +fn UNIT_METADATA() +{ + let @0: (); // return + + @0 := () + return +} + +const UNIT_METADATA: () = @Fun0() + +// Full name: test_crate::main::closure +struct closure {} + +// Full name: test_crate::main::{impl Fn<()> for closure}::call +fn {impl Fn<()> for closure}::call<'_0>(@1: &'_0 (closure), @2: ()) -> i32 +{ + let @0: i32; // return + let @1: &'0 (closure); // arg #1 + let tupled_args@2: (); // arg #2 + + @0 := const (42 : i32) + return +} + +// Full name: test_crate::main::{impl FnMut<()> for closure}::call_mut +fn {impl FnMut<()> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: ()) -> i32 +{ + let @0: i32; // return + let state@1: &'_0 mut (closure); // arg #1 + let args@2: (); // arg #2 + let @3: &'0 (closure); // anonymous local + + storage_live(@3) + @3 := &*(state@1) + @0 := {impl Fn<()> for closure}::call<'2>(move (@3), move (args@2)) + return +} + +// Full name: test_crate::main::closure::{impl Destruct for closure}::drop_in_place +unsafe fn {impl Destruct for closure}::drop_in_place(@1: *mut closure) += + +// Full name: test_crate::main::closure::{impl Destruct for closure} +impl Destruct for closure { + fn drop_in_place = {impl Destruct for closure}::drop_in_place + non-dyn-compatible +} + +// Full name: test_crate::main::{impl FnOnce<()> for closure}::call_once +fn {impl FnOnce<()> for closure}::call_once(@1: closure, @2: ()) -> i32 +{ + let @0: i32; // return + let @1: closure; // arg #1 + let @2: (); // arg #2 + let @3: &'0 mut (closure); // anonymous local + + storage_live(@3) + @3 := &mut @1 + @0 := {impl FnMut<()> for closure}::call_mut<'_>(move (@3), move (@2)) + drop[{impl Destruct for closure}] @1 + return +} + +// Full name: test_crate::main::{impl FnOnce<()> for closure} +impl FnOnce<()> for closure { + parent_clause0 = {built_in impl MetaSized for closure} + parent_clause1 = {built_in impl Sized for ()} + parent_clause2 = {built_in impl Tuple for ()} + parent_clause3 = {built_in impl Sized for i32} + type Output = i32 + fn call_once = {impl FnOnce<()> for closure}::call_once + non-dyn-compatible +} + +// Full name: test_crate::main::{impl FnMut<()> for closure} +impl FnMut<()> for closure { + parent_clause0 = {built_in impl MetaSized for closure} + parent_clause1 = {impl FnOnce<()> for closure} + parent_clause2 = {built_in impl Sized for ()} + parent_clause3 = {built_in impl Tuple for ()} + fn call_mut<'_0_1> = {impl FnMut<()> for closure}::call_mut<'_0_1> + non-dyn-compatible +} + +// Full name: test_crate::main::{impl Fn<()> for closure} +impl Fn<()> for closure { + parent_clause0 = {built_in impl MetaSized for closure} + parent_clause1 = {impl FnMut<()> for closure} + parent_clause2 = {built_in impl Sized for ()} + parent_clause3 = {built_in impl Tuple for ()} + fn call<'_0_1> = {impl Fn<()> for closure}::call<'_0_1> + non-dyn-compatible +} + +// Full name: test_crate::main::closure::{vtable_method} +fn {vtable_method}<'_0>(@1: &'_0 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32>)), @2: (())) -> i32 +{ + let @0: i32; // return + let @1: &'_0 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '0)); // arg #1 + let @2: (()); // arg #2 + let @3: &'_0 (closure); // anonymous local + + storage_live(@3) + @3 := concretize<&'_0 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '1)), &'_0 (closure)>(move (@1)) + @0 := {impl Fn<()> for closure}::call<'_0>(move (@3), move (@2)) + return +} + +// Full name: test_crate::main::closure::{vtable_method} +fn {vtable_method}<'_0>(@1: &'_0 mut ((dyn FnMut<(), parent_clause1::Output = i32>)), @2: (())) -> i32 +{ + let @0: i32; // return + let @1: &'_0 mut ((dyn FnMut<(), parent_clause1::Output = i32> + '0)); // arg #1 + let @2: (()); // arg #2 + let @3: &'_0 mut (closure); // anonymous local + + storage_live(@3) + @3 := concretize<&'_0 mut ((dyn FnMut<(), parent_clause1::Output = i32> + '1)), &'_0 mut (closure)>(move (@1)) + @0 := {impl FnMut<()> for closure}::call_mut<'_0>(move (@3), move (@2)) + return +} + +// Full name: test_crate::main::closure::{vtable_drop_shim} +unsafe fn {vtable_drop_shim}(@1: *mut (dyn Fn<(), parent_clause1::parent_clause1::Output = i32>)) +{ + let ret@0: (); // return + let dyn_self@1: *mut (dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '0); // arg #1 + let target_self@2: *mut closure; // local + + ret@0 := () + storage_live(target_self@2) + target_self@2 := concretize<*mut (dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '1), *mut closure>(move (dyn_self@1)) + drop[{impl Destruct for closure}] *(target_self@2) + return +} + +// Full name: test_crate::main::{impl FnOnce<()> for closure}::{vtable} +fn {impl FnOnce<()> for closure}::{vtable}() -> core::ops::function::FnOnce::{vtable}<(), i32> +{ + let ret@0: core::ops::function::FnOnce::{vtable}<(), i32>; // return + let size@1: usize; // local + let align@2: usize; // local + + storage_live(size@1) + size@1 := size_of + storage_live(align@2) + align@2 := align_of + ret@0 := core::ops::function::FnOnce::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}) } + return +} + +// Full name: test_crate::main::{impl FnOnce<()> for closure}::{vtable} +static {impl FnOnce<()> for closure}::{vtable}: core::ops::function::FnOnce::{vtable}<(), i32> = {impl FnOnce<()> for closure}::{vtable}() + +// Full name: test_crate::main::closure::{vtable_drop_shim} +unsafe fn {vtable_drop_shim}(@1: *mut (dyn FnMut<(), parent_clause1::Output = i32>)) +{ + let ret@0: (); // return + let dyn_self@1: *mut (dyn FnMut<(), parent_clause1::Output = i32> + '0); // arg #1 + let target_self@2: *mut closure; // local + + ret@0 := () + storage_live(target_self@2) + target_self@2 := concretize<*mut (dyn FnMut<(), parent_clause1::Output = i32> + '1), *mut closure>(move (dyn_self@1)) + drop[{impl Destruct for closure}] *(target_self@2) + return +} + +// Full name: test_crate::main::{impl FnMut<()> for closure}::{vtable} +fn {impl FnMut<()> for closure}::{vtable}() -> core::ops::function::FnMut::{vtable}<(), i32> +{ + let ret@0: core::ops::function::FnMut::{vtable}<(), i32>; // return + let size@1: usize; // local + let align@2: usize; // local + let @3: fn<'_0_1>(&'_0_1 mut ((dyn FnMut<(), parent_clause1::Output = i32> + '2)), ()) -> i32; // anonymous local + let @4: &'static (core::ops::function::FnOnce::{vtable}<(), i32>); // anonymous local + + storage_live(size@1) + size@1 := size_of + storage_live(align@2) + align@2 := align_of + storage_live(@3) + @3 := cast {vtable_method}<'1>, fn<'_0_1>(&'_0_1 mut ((dyn FnMut<(), parent_clause1::Output = i32> + '2)), ()) -> i32>(const ({vtable_method}<'1>)) + storage_live(@4) + @4 := &{impl FnOnce<()> for closure}::{vtable} + ret@0 := core::ops::function::FnMut::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}), method_call_mut: move (@3), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4) } + return +} + +// Full name: test_crate::main::{impl FnMut<()> for closure}::{vtable} +static {impl FnMut<()> for closure}::{vtable}: core::ops::function::FnMut::{vtable}<(), i32> = {impl FnMut<()> for closure}::{vtable}() + +// Full name: test_crate::main::closure::{vtable_drop_shim} +unsafe fn {vtable_drop_shim}(@1: *mut (dyn Fn<(), parent_clause1::parent_clause1::Output = i32>)) +{ + let ret@0: (); // return + let dyn_self@1: *mut (dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '0); // arg #1 + let target_self@2: *mut closure; // local + + ret@0 := () + storage_live(target_self@2) + target_self@2 := concretize<*mut (dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '1), *mut closure>(move (dyn_self@1)) + drop[{impl Destruct for closure}] *(target_self@2) + return +} + +// Full name: test_crate::main::{impl Fn<()> for closure}::{vtable} +fn {impl Fn<()> for closure}::{vtable}() -> core::ops::function::Fn::{vtable}<(), i32> +{ + let ret@0: core::ops::function::Fn::{vtable}<(), i32>; // return + let size@1: usize; // local + let align@2: usize; // local + let @3: fn<'_0_1>(&'_0_1 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '2)), ()) -> i32; // anonymous local + let @4: &'static (core::ops::function::FnMut::{vtable}<(), i32>); // anonymous local + + storage_live(size@1) + size@1 := size_of + storage_live(align@2) + align@2 := align_of + storage_live(@3) + @3 := cast {vtable_method}<'1>, fn<'_0_1>(&'_0_1 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '2)), ()) -> i32>(const ({vtable_method}<'1>)) + storage_live(@4) + @4 := &{impl FnMut<()> for closure}::{vtable} + ret@0 := core::ops::function::Fn::{vtable} { size: move (size@1), align: move (align@2), drop: const ({vtable_drop_shim}), method_call: move (@3), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4) } + return +} + +// Full name: test_crate::main::{impl Fn<()> for closure}::{vtable} +static {impl Fn<()> for closure}::{vtable}: core::ops::function::Fn::{vtable}<(), i32> = {impl Fn<()> for closure}::{vtable}() + +// Full name: test_crate::main +fn main() +{ + let @0: (); // return + let a@1: closure; // local + let dyn_a@2: &'0 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '1)); // local + let @3: &'2 (closure); // anonymous local + let @4: &'2 (closure); // anonymous local + + @0 := () + storage_live(a@1) + a@1 := closure { } + storage_live(dyn_a@2) + storage_live(@3) + storage_live(@4) + @4 := &a@1 + @3 := &*(@4) + dyn_a@2 := unsize_cast<&'2 (closure), &'0 ((dyn Fn<(), parent_clause1::parent_clause1::Output = i32> + '1)), {impl Fn<()> for closure} with {impl Fn<()> for closure}::{vtable}>(move (@3)) + storage_dead(@3) + storage_dead(@4) + @0 := () + storage_dead(dyn_a@2) + storage_dead(a@1) + return +} + + + diff --git a/charon/tests/ui/simple/simple_closure.rs b/charon/tests/ui/simple/simple_closure.rs new file mode 100644 index 000000000..d07149e23 --- /dev/null +++ b/charon/tests/ui/simple/simple_closure.rs @@ -0,0 +1,4 @@ +fn main() { + let a = || 42; + let dyn_a: &dyn Fn() -> i32 = &a; +} \ No newline at end of file