diff --git a/.gitignore b/.gitignore index e7183a5f8..6cd42915e 100644 --- a/.gitignore +++ b/.gitignore @@ -55,3 +55,4 @@ nohup.out *# *.smt2 .#* +**/.DS_Store diff --git a/charon-ml/src/CharonVersion.ml b/charon-ml/src/CharonVersion.ml index 05165492e..d1365e871 100644 --- a/charon-ml/src/CharonVersion.ml +++ b/charon-ml/src/CharonVersion.ml @@ -1,3 +1,3 @@ (* This is an automatically generated file, generated from `charon/Cargo.toml`. *) (* To re-generate this file, rune `make` in the root directory *) -let supported_charon_version = "0.1.133" +let supported_charon_version = "0.1.134" diff --git a/charon-ml/src/PrintExpressions.ml b/charon-ml/src/PrintExpressions.ml index 1738b895c..4c57b0fff 100644 --- a/charon-ml/src/PrintExpressions.ml +++ b/charon-ml/src/PrintExpressions.ml @@ -79,6 +79,8 @@ and cast_kind_to_string (env : 'a fmt_env) (cast : cast_kind) : string = "cast<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">" | CastUnsize (src, tgt, _) -> "unsize<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">" + | CastConcretize (src, tgt) -> + "concretize<" ^ ty_to_string env src ^ "," ^ ty_to_string env tgt ^ ">" and nullop_to_string (env : 'a fmt_env) (op : nullop) : string = match op with diff --git a/charon-ml/src/generated/Generated_Expressions.ml b/charon-ml/src/generated/Generated_Expressions.ml index 1a2fdd706..3872457ec 100644 --- a/charon-ml/src/generated/Generated_Expressions.ml +++ b/charon-ml/src/generated/Generated_Expressions.ml @@ -139,6 +139,20 @@ and cast_kind = | CastTransmute of ty * ty (** Reinterprets the bits of a value of one type as another type, i.e. exactly what [[std::mem::transmute]] does. *) + | CastConcretize of ty * ty + (** Converts a receiver type with [dyn Trait<...>] to a concrete type [T], + used in vtable method shims. Valid conversions are references, raw + pointers, and (optionally) boxes: + - [&[mut] dyn Trait<...>] -> [&[mut] T] + - [*[mut] dyn Trait<...>] -> [*[mut] T] + - [Box>] -> [Box] when no [--raw-boxes] + + For possible receivers, see: + https://doc.rust-lang.org/reference/items/traits.html#dyn-compatibility. + Other receivers, e.g., [Rc] should be unpacked before the cast and + re-boxed after. FIXME(ssyram): but this is not implemented yet, + namely, there may still be something like + [Rc> -> Rc] in the types. *) and constant_expr = { kind : constant_expr_kind; ty : ty } diff --git a/charon-ml/src/generated/Generated_GAstOfJson.ml b/charon-ml/src/generated/Generated_GAstOfJson.ml index 036876592..c70a53889 100644 --- a/charon-ml/src/generated/Generated_GAstOfJson.ml +++ b/charon-ml/src/generated/Generated_GAstOfJson.ml @@ -279,6 +279,10 @@ and cast_kind_of_json (ctx : of_json_ctx) (js : json) : let* x_0 = ty_of_json ctx x_0 in let* x_1 = ty_of_json ctx x_1 in Ok (CastTransmute (x_0, x_1)) + | `Assoc [ ("Concretize", `List [ x_0; x_1 ]) ] -> + let* x_0 = ty_of_json ctx x_0 in + let* x_1 = ty_of_json ctx x_1 in + Ok (CastConcretize (x_0, x_1)) | _ -> Error "") and cli_options_of_json (ctx : of_json_ctx) (js : json) : @@ -1098,6 +1102,7 @@ and item_source_of_json (ctx : of_json_ctx) (js : json) : | `Assoc [ ("VTableInstance", `Assoc [ ("impl_ref", impl_ref) ]) ] -> let* impl_ref = trait_impl_ref_of_json ctx impl_ref in Ok (VTableInstanceItem impl_ref) + | `String "VTableMethodShim" -> Ok VTableMethodShimItem | _ -> Error "") and layout_of_json (ctx : of_json_ctx) (js : json) : (layout, string) result = diff --git a/charon-ml/src/generated/Generated_Types.ml b/charon-ml/src/generated/Generated_Types.ml index e0a79be2b..9ad65c6f7 100644 --- a/charon-ml/src/generated/Generated_Types.ml +++ b/charon-ml/src/generated/Generated_Types.ml @@ -769,6 +769,10 @@ and item_source = Fields: - [impl_ref] *) + | VTableMethodShimItem + (** The method shim wraps a concrete implementation of a method into a + function that takes [dyn Trait] as its [Self] type. This shim casts + the receiver to the known concrete type and calls the real method. *) (** Simplified type layout information. diff --git a/charon/Cargo.lock b/charon/Cargo.lock index 0180dd228..2bad35641 100644 --- a/charon/Cargo.lock +++ b/charon/Cargo.lock @@ -201,7 +201,7 @@ checksum = "9555578bc9e57714c812a1f84e4fc5b4d21fcb063490c624de019f7464c91268" [[package]] name = "charon" -version = "0.1.133" +version = "0.1.134" dependencies = [ "annotate-snippets", "anstream", diff --git a/charon/Cargo.toml b/charon/Cargo.toml index 965bad4c0..68b6527e6 100644 --- a/charon/Cargo.toml +++ b/charon/Cargo.toml @@ -1,6 +1,6 @@ [package] name = "charon" -version = "0.1.133" +version = "0.1.134" authors = [ "Son Ho ", "Guillaume Boisseau ", diff --git a/charon/src/ast/expressions.rs b/charon/src/ast/expressions.rs index 6e16a181a..420bc6ea9 100644 --- a/charon/src/ast/expressions.rs +++ b/charon/src/ast/expressions.rs @@ -202,6 +202,17 @@ pub enum CastKind { /// Reinterprets the bits of a value of one type as another type, i.e. exactly what /// [`std::mem::transmute`] does. Transmute(Ty, Ty), + /// Converts a receiver type with `dyn Trait<...>` to a concrete type `T`, used in vtable method shims. + /// Valid conversions are references, raw pointers, and (optionally) boxes: + /// - `&[mut] dyn Trait<...>` -> `&[mut] T` + /// - `*[mut] dyn Trait<...>` -> `*[mut] T` + /// - `Box>` -> `Box` when no `--raw-boxes` + /// + /// For possible receivers, see: https://doc.rust-lang.org/reference/items/traits.html#dyn-compatibility. + /// Other receivers, e.g., `Rc` should be unpacked before the cast and re-boxed after. + /// FIXME(ssyram): but this is not implemented yet, namely, there may still be + /// something like `Rc> -> Rc` in the types. + Concretize(Ty, Ty), } #[derive( diff --git a/charon/src/ast/gast.rs b/charon/src/ast/gast.rs index 5ba93bfbd..6c6e09944 100644 --- a/charon/src/ast/gast.rs +++ b/charon/src/ast/gast.rs @@ -133,6 +133,10 @@ pub enum ItemSource { }, /// This is a vtable value for an impl. VTableInstance { impl_ref: TraitImplRef }, + /// The method shim wraps a concrete implementation of a method into a function that takes `dyn + /// Trait` as its `Self` type. This shim casts the receiver to the known concrete type and + /// calls the real method. + VTableMethodShim, } /// A function definition diff --git a/charon/src/bin/charon-driver/translate/translate_bodies.rs b/charon/src/bin/charon-driver/translate/translate_bodies.rs index 44ce8292b..9291ba347 100644 --- a/charon/src/bin/charon-driver/translate/translate_bodies.rs +++ b/charon/src/bin/charon-driver/translate/translate_bodies.rs @@ -1047,7 +1047,9 @@ impl BodyTransCtx<'_, '_, '_> { // We ignore the arguments return Ok(TerminatorKind::Abort(AbortKind::Panic(Some(name)))); } else { - let fn_ptr = self.translate_fn_ptr(span, item)?.erase(); + let fn_ptr = self + .translate_fn_ptr(span, item, TransItemSourceKind::Fun)? + .erase(); FnOperand::Regular(fn_ptr) } } diff --git a/charon/src/bin/charon-driver/translate/translate_constants.rs b/charon/src/bin/charon-driver/translate/translate_constants.rs index b030d51ba..7bae02fcd 100644 --- a/charon/src/bin/charon-driver/translate/translate_constants.rs +++ b/charon/src/bin/charon-driver/translate/translate_constants.rs @@ -129,7 +129,9 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { expressions::ConstantExprKind::Var(var) } ConstantExprKind::FnPtr(item) => { - let fn_ptr = self.translate_fn_ptr(span, item)?.erase(); + let fn_ptr = self + .translate_fn_ptr(span, item, TransItemSourceKind::Fun)? + .erase(); expressions::ConstantExprKind::FnPtr(fn_ptr) } ConstantExprKind::Memory(bytes) => { diff --git a/charon/src/bin/charon-driver/translate/translate_crate.rs b/charon/src/bin/charon-driver/translate/translate_crate.rs index 562368d2e..0bb069380 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate.rs @@ -504,6 +504,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { &mut self, span: Span, item: &hax::ItemRef, + kind: TransItemSourceKind, ) -> Result { match self.recognize_builtin_fun(item)? { Some(id) => { @@ -514,7 +515,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { generics: Box::new(generics), }) } - None => self.translate_item(span, item, TransItemSourceKind::Fun), + None => self.translate_item(span, item, kind), } } @@ -525,8 +526,9 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { &mut self, span: Span, item: &hax::ItemRef, + kind: TransItemSourceKind, ) -> Result, Error> { - let fun_item = self.translate_fun_item(span, item)?; + let fun_item = self.translate_fun_item(span, item, kind)?; let late_bound = match self.hax_def(item)?.kind() { hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => { Some(sig.as_ref().rebind(())) diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index 47587105b..dafcf4c06 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -165,11 +165,11 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { self.translated.fun_decls.set_slot(id, fun_decl); } TransItemSourceKind::VTableMethod => { - // let Some(ItemId::Fun(id)) = trans_id else { - // unreachable!() - // }; - // let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def)?; - // self.translated.fun_decls.set_slot(id, fun_decl); + let Some(ItemId::Fun(id)) = trans_id else { + unreachable!() + }; + let fun_decl = bt_ctx.translate_vtable_shim(id, item_meta, &def)?; + self.translated.fun_decls.set_slot(id, fun_decl); } } Ok(()) diff --git a/charon/src/bin/charon-driver/translate/translate_meta.rs b/charon/src/bin/charon-driver/translate/translate_meta.rs index 9bc9f84cb..d7d8a7959 100644 --- a/charon/src/bin/charon-driver/translate/translate_meta.rs +++ b/charon/src/bin/charon-driver/translate/translate_meta.rs @@ -362,6 +362,12 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { name.name .push(PathElem::Ident("{vtable}".into(), Disambiguator::ZERO)); } + TransItemSourceKind::VTableMethod => { + name.name.push(PathElem::Ident( + "{vtable_method}".into(), + Disambiguator::ZERO, + )); + } _ => {} } Ok(name) 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 cd6dc366d..dd861dbb7 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -1,10 +1,13 @@ +use itertools::Itertools; +use std::mem; + use super::{ translate_crate::TransItemSourceKind, translate_ctx::*, translate_generics::BindingLevel, }; - +use charon_lib::formatter::IntoFormatter; use charon_lib::ids::Vector; +use charon_lib::pretty::FmtWithCtx; use charon_lib::ullbc_ast::*; -use itertools::Itertools; fn dummy_public_attr_info() -> AttrInfo { AttrInfo { @@ -317,11 +320,23 @@ impl ItemTransCtx<'_, '_> { Ok(fields) } + /// This is a temporary check until we support `dyn Trait` with `--monomorphize`. + pub(crate) fn check_no_monomorphize(&self, span: Span) -> Result<(), Error> { + if self.monomorphize() { + raise_error!( + self, + span, + "`dyn Trait` is not yet supported with `--monomorphize`; \ + use `--monomorphize-conservative` instead" + ) + } + Ok(()) + } + /// Construct the type of the vtable for this trait. /// /// It's a struct that has for generics the generics of the trait + one parameter for each /// associated type of the trait and its parents. - /// TODO(dyn): add the associated types. /// /// struct TraitVTable { /// size: usize, @@ -347,6 +362,7 @@ impl ItemTransCtx<'_, '_> { for a non-dyn-compatible trait" ); } + self.check_no_monomorphize(span)?; self.translate_def_generics(span, trait_def)?; @@ -503,6 +519,7 @@ impl ItemTransCtx<'_, '_> { ) -> Result { let span = item_meta.span; self.translate_def_generics(span, impl_def)?; + self.check_no_monomorphize(span)?; let (impl_ref, _, vtable_struct_ref) = self.get_vtable_instance_info(span, impl_def, impl_kind)?; @@ -547,14 +564,15 @@ impl ItemTransCtx<'_, '_> { .. } => { // The method is vtable safe so it has no generics, hence we can reuse the impl - // generics. + // 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_item(span, &item_ref, TransItemSourceKind::VTableMethod)?; + let shim_ref = self + .translate_fn_ptr(span, &item_ref, TransItemSourceKind::VTableMethod)? + .erase(); ConstantExprKind::FnPtr(shim_ref) } hax::ImplAssocItemValue::DefaultedFn { .. } => ConstantExprKind::Opaque( - "shim for provided methods \ + "shim for default methods \ aren't yet supported" .to_string(), ), @@ -721,6 +739,26 @@ impl ItemTransCtx<'_, '_> { })) } + fn generate_concretization( + &mut self, + span: Span, + statements: &mut Vec, + shim_self: &Place, + target_self: &Place, + ) -> Result<(), Error> { + let rval = Rvalue::UnaryOp( + UnOp::Cast(CastKind::Concretize( + shim_self.ty().clone(), + target_self.ty().clone(), + )), + Operand::Move(shim_self.clone()), + ); + let stmt = StatementKind::Assign(target_self.clone(), rval); + statements.push(Statement::new(span, stmt)); + + Ok(()) + } + pub(crate) fn translate_vtable_instance_init( mut self, init_func_id: FunDeclId, @@ -730,6 +768,7 @@ impl ItemTransCtx<'_, '_> { ) -> Result { let span = item_meta.span; self.translate_def_generics(span, impl_def)?; + self.check_no_monomorphize(span)?; let (impl_ref, _, vtable_struct_ref) = self.get_vtable_instance_info(span, impl_def, impl_kind)?; @@ -771,13 +810,163 @@ impl ItemTransCtx<'_, '_> { }) } - // pub(crate) fn translate_vtable_shim( - // self, - // _fun_id: FunDeclId, - // item_meta: ItemMeta, - // _impl_func_def: &hax::FullDef, - // ) -> Result { - // let span = item_meta.span; - // raise_error!(self, span, "unimplemented") - // } + /// The target vtable shim body looks like: + /// ```ignore + /// local ret@0 : ReturnTy; + /// // the shim receiver of this shim function + /// local shim_self@1 : ShimReceiverTy; + /// // the arguments of the impl function + /// local arg1@2 : Arg1Ty; + /// ... + /// local argN@N : ArgNTy; + /// // the target receiver of the impl function + /// local target_self@(N+1) : TargetReceiverTy; + /// // perform some conversion to cast / re-box the shim receiver to the target receiver + /// ... + /// target_self@(N+1) := concretize_cast(shim_self@1); + /// // call the impl function and assign the result to ret@0 + /// ret@0 := impl_func(target_self@(N+1), arg1@2, ..., argN@N); + /// ``` + fn translate_vtable_shim_body( + &mut self, + span: Span, + target_receiver: &Ty, + shim_signature: &FunSig, + impl_func_def: &hax::FullDef, + ) -> Result { + let mut locals = Locals { + arg_count: shim_signature.inputs.len(), + locals: Vector::new(), + }; + let mut statements = vec![]; + + let ret_place = locals.new_var(None, shim_signature.output.clone()); + let mut method_args = shim_signature + .inputs + .iter() + .map(|ty| locals.new_var(None, ty.clone())) + .collect_vec(); + let target_self = locals.new_var(None, target_receiver.clone()); + statements.push(Statement::new( + span, + StatementKind::StorageLive(target_self.as_local().unwrap()), + )); + + // Replace the `dyn Trait` receiver with the concrete one. + let shim_self = mem::replace(&mut method_args[0], target_self.clone()); + + // Perform the core concretization cast. + // FIXME: need to unpack & re-pack the structure for cases like `Rc`, `Arc`, `Pin` and + // (when --raw-boxes is on) `Box` + self.generate_concretization(span, &mut statements, &shim_self, &target_self)?; + + let call = { + let fun_id = self.register_item(span, &impl_func_def.this(), TransItemSourceKind::Fun); + let generics = Box::new(self.outermost_binder().params.identity_args()); + Call { + func: FnOperand::Regular(FnPtr { + kind: Box::new(FnPtrKind::Fun(fun_id)), + generics, + }), + args: method_args + .into_iter() + .map(|arg| Operand::Move(arg)) + .collect(), + dest: ret_place, + } + }; + + // Create blocks + let mut blocks = Vector::new(); + + let ret_block = BlockData { + statements: vec![], + terminator: Terminator::new(span, TerminatorKind::Return), + }; + + let unwind_block = BlockData { + statements: vec![], + terminator: Terminator::new(span, TerminatorKind::UnwindResume), + }; + + let call_block = BlockData { + statements, + terminator: Terminator::new( + span, + TerminatorKind::Call { + call, + target: BlockId::new(1), // ret_block + on_unwind: BlockId::new(2), // unwind_block + }, + ), + }; + + blocks.push(call_block); // BlockId(0) -- START_BLOCK_ID + blocks.push(ret_block); // BlockId(1) + blocks.push(unwind_block); // BlockId(2) + + Ok(Body::Unstructured(GExprBody { + span, + locals, + comments: Vec::new(), + body: blocks, + })) + } + + pub(crate) fn translate_vtable_shim( + mut self, + fun_id: FunDeclId, + item_meta: ItemMeta, + impl_func_def: &hax::FullDef, + ) -> Result { + let span = item_meta.span; + self.check_no_monomorphize(span)?; + + let hax::FullDefKind::AssocFn { + vtable_sig: Some(vtable_sig), + sig: target_signature, + .. + } = impl_func_def.kind() + else { + raise_error!( + self, + span, + "Trying to generate a vtable shim for a non-vtable-safe method" + ); + }; + + // Replace to get the true signature of the shim function. + // As `translate_function_signature` will use the `sig` field of the `hax::FullDef` + // TODO: this is a hack. + let shim_func_def = { + let mut def = impl_func_def.clone(); + let hax::FullDefKind::AssocFn { sig, .. } = &mut def.kind else { + unreachable!() + }; + *sig = vtable_sig.clone(); + def + }; + + // Compute the correct signature for the shim + let signature = self.translate_function_signature(&shim_func_def, &item_meta)?; + + let target_receiver = self.translate_ty(span, &target_signature.value.inputs[0])?; + + trace!( + "[VtableShim] Obtained dyn signature with receiver type: {}", + signature.inputs[0].with_ctx(&self.into_fmt()) + ); + + let body = + self.translate_vtable_shim_body(span, &target_receiver, &signature, impl_func_def)?; + + Ok(FunDecl { + def_id: fun_id, + item_meta, + signature, + src: ItemSource::VTableMethodShim, + is_global_initializer: None, + body: Ok(body), + }) + } } diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 04434a0e2..5733cc754 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -214,7 +214,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { TyKind::FnPtr(sig) } hax::TyKind::FnDef { item, .. } => { - let fnref = self.translate_fn_ptr(span, item)?; + let fnref = self.translate_fn_ptr(span, item, TransItemSourceKind::Fun)?; TyKind::FnDef(fnref) } hax::TyKind::Closure(args) => { @@ -223,14 +223,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { } hax::TyKind::Dynamic(self_ty, preds, region) => { - if self.monomorphize() { - raise_error!( - self, - span, - "`dyn Trait` is not yet supported with `--monomorphize`; \ - use `--monomorphize-conservative` instead" - ) - } + self.check_no_monomorphize(span)?; let pred = self.translate_existential_predicates(span, self_ty, preds, region)?; if let hax::ClauseKind::Trait(trait_predicate) = preds.predicates[0].0.kind.hax_skip_binder_ref() diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 3c140b17d..733392b38 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -288,6 +288,9 @@ impl FmtWithCtx for CastKind { CastKind::Transmute(src, tgt) => { write!(f, "transmute<{}, {}>", src.with_ctx(ctx), tgt.with_ctx(ctx)) } + CastKind::Concretize(ty, ty1) => { + write!(f, "concretize<{}, {}>", ty.with_ctx(ctx), ty1.with_ctx(ctx)) + } } } } diff --git a/charon/src/transform/check_generics.rs b/charon/src/transform/check_generics.rs index c24c6a281..b73635368 100644 --- a/charon/src/transform/check_generics.rs +++ b/charon/src/transform/check_generics.rs @@ -40,6 +40,31 @@ impl VisitorWithBinderStack for CheckGenericsVisitor<'_> { } impl CheckGenericsVisitor<'_> { + fn check_concretization_ty_match(&self, src_ty: &Ty, tar_ty: &Ty) { + match (src_ty.kind(), tar_ty.kind()) { + (TyKind::Ref(.., src_kind), TyKind::Ref(.., tar_kind)) => { + assert_eq!(src_kind, tar_kind); + } + (TyKind::RawPtr(.., src_kind), TyKind::RawPtr(.., tar_kind)) => { + assert_eq!(src_kind, tar_kind); + } + ( + TyKind::Adt(TypeDeclRef { id: src_id, .. }), + TyKind::Adt(TypeDeclRef { id: tar_id, .. }), + ) => { + assert_eq!(src_id, tar_id); + } + _ => { + let fmt = &self.ctx.into_fmt(); + self.error(format!( + "Invalid concretization targets: from \"{}\" to \"{}\"", + src_ty.with_ctx(fmt), + tar_ty.with_ctx(fmt) + )); + } + } + } + fn error(&self, message: impl Display) { let msg = format!( "Found inconsistent generics {}:\n{message}\n\ @@ -309,6 +334,15 @@ impl VisitAst for CheckGenericsVisitor<'_> { } } } + fn visit_rvalue(&mut self, x: &Rvalue) -> ::std::ops::ControlFlow { + match x { + Rvalue::UnaryOp(UnOp::Cast(CastKind::Concretize(src, tar)), _) => { + self.check_concretization_ty_match(src, tar); + } + _ => {} + } + Continue(()) + } fn enter_global_decl_ref(&mut self, x: &GlobalDeclRef) { self.assert_matches_item(x.id, &x.generics); } diff --git a/charon/src/transform/normalize/expand_associated_types.rs b/charon/src/transform/normalize/expand_associated_types.rs index ad9532c5a..1d28627e6 100644 --- a/charon/src/transform/normalize/expand_associated_types.rs +++ b/charon/src/transform/normalize/expand_associated_types.rs @@ -1163,7 +1163,8 @@ impl VisitAstMut for UpdateItemBody<'_> { ItemSource::TopLevel | ItemSource::Closure { .. } | ItemSource::VTableTy { .. } - | ItemSource::VTableInstance { .. } => {} + | ItemSource::VTableInstance { .. } + | ItemSource::VTableMethodShim => {} // Inside method declarations, the implicit `Self` clause is the first clause. ItemSource::TraitDecl { trait_ref, .. } => self.process_trait_decl_ref( trait_ref, diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out index de7033ebf..9c1cdaf93 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.out +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -301,6 +301,19 @@ fn {impl Join for i32}::join_method<'_0>(@1: &'_0 (i32)) -> (i32, i32) return } +// Full name: test_crate::{impl Join for i32}::join_method::{vtable_method} +fn {vtable_method}<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32))) -> (i32, i32) +{ + let @0: (i32, i32); // return + let @1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32)); // arg #1 + let @2: &'_0 (i32); // anonymous local + + storage_live(@2) + @2 := concretize<&'_0 ((dyn exists<_dyn> [@TraitClause0]: Join<_dyn, i32> + _dyn : '_ + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause1::parent_clause1::Internal = i32 + @TraitClause1_0::parent_clause2::Right = i32 + @TraitClause1_0::parent_clause1::Left = i32)), &'_0 (i32)>(move (@1)) + @0 := {impl Join for i32}::join_method<'_0>(move (@2)) + return +} + // Full name: test_crate::{impl Join for i32}::{vtable} fn {impl Join for i32}::{vtable}() -> test_crate::Join::{vtable} { @@ -318,7 +331,7 @@ fn {impl Join for i32}::{vtable}() -> test_crate::Join::{vtable} for i32}::{vtable} - ret@0 := test_crate::Join::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_join_method: const ({impl Join for i32}::join_method), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2), super_trait_2: move (@4) } + ret@0 := test_crate::Join::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_join_method: const ({vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2), super_trait_2: move (@4) } return } diff --git a/charon/tests/ui/monomorphization/dyn-trait.out b/charon/tests/ui/monomorphization/dyn-trait.out index f699b9a4d..908af54c2 100644 --- a/charon/tests/ui/monomorphization/dyn-trait.out +++ b/charon/tests/ui/monomorphization/dyn-trait.out @@ -89,22 +89,7 @@ note: the error occurred when translating `core::marker::MetaSized:: /rustc/library/core/src/fmt/mod.rs:1007:1 - -note: the error occurred when translating `core::fmt::Display::{vtable}::`, which is (transitively) used at the following location(s): - --> tests/ui/monomorphization/dyn-trait.rs:12:27 - | -12 | let _ = dyn_to_string(&str); - | ---- - -thread 'rustc' panicked at src/bin/charon-driver/translate/translate_trait_objects.rs:374:17: -incorrect `dyn_self` -note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace -error: Thread panicked when extracting item `core::fmt::Display`. - --> /rustc/library/core/src/fmt/mod.rs:1007:1 - -error: Failed to translate item Type(3). - --> /rustc/library/core/src/fmt/mod.rs:1007:1 + --> /rustc/library/alloc/src/string.rs:2624:1 note: the error occurred when translating `alloc::string::{impl core::fmt::Display::}::{vtable}`, which is (transitively) used at the following location(s): --> tests/ui/monomorphization/dyn-trait.rs:12:27 @@ -198,4 +183,4 @@ note: the error occurred when translating `alloc::string::ToString::to_string`, | 7 | x.to_string() | ------------- -ERROR Charon failed to translate this code (38 errors) +ERROR Charon failed to translate this code (36 errors) diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out index f74193837..48adf91ff 100644 --- a/charon/tests/ui/unsize.out +++ b/charon/tests/ui/unsize.out @@ -159,12 +159,26 @@ impl Clone for String { // Full name: alloc::string::{impl Display for String}::fmt pub fn {impl Display for String}::fmt<'_0, '_1, '_2>(@1: &'_0 (String), @2: &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized] +// Full name: alloc::string::{impl Display for String}::fmt::{vtable_method} +fn {vtable_method}<'_0, '_1, '_2>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)), @2: &'_1 mut (Formatter<'_2>)) -> Result<(), Error>[Sized<()>, Sized] +{ + let @0: Result<(), Error>[Sized<()>, Sized]; // return + let @1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)); // arg #1 + let @2: &'_1 mut (Formatter<'_2>); // arg #2 + let @3: &'_0 (String); // anonymous local + + storage_live(@3) + @3 := concretize<&'_0 ((dyn exists<_dyn> [@TraitClause0]: Display<_dyn> + _dyn : '_)), &'_0 (String)>(move (@1)) + @0 := {impl Display for String}::fmt<'_0, '_1, '_2>(move (@3), move (@2)) + return +} + // Full name: alloc::string::{impl Display for String}::{vtable} fn {impl Display for String}::{vtable}() -> core::fmt::Display::{vtable} { let ret@0: core::fmt::Display::{vtable}; // return - ret@0 := core::fmt::Display::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_fmt: const ({impl Display for String}::fmt) } + ret@0 := core::fmt::Display::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_fmt: const ({vtable_method}<'_, '_, '_>) } return } diff --git a/charon/tests/ui/vtables.out b/charon/tests/ui/vtables.out index 29f9bd001..fd6faa45e 100644 --- a/charon/tests/ui/vtables.out +++ b/charon/tests/ui/vtables.out @@ -267,6 +267,19 @@ fn {impl Checkable for i32}::check<'_0>(@1: &'_0 (i32)) -> bool return } +// Full name: test_crate::{impl Checkable for i32}::check::{vtable_method} +fn {impl Checkable for i32}::check::{vtable_method}<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_))) -> bool +{ + let @0: bool; // return + let @1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_)); // arg #1 + let @2: &'_0 (i32); // anonymous local + + storage_live(@2) + @2 := concretize<&'_0 ((dyn exists<_dyn> [@TraitClause0]: Checkable<_dyn, i32> + _dyn : '_)), &'_0 (i32)>(move (@1)) + @0 := {impl Checkable for i32}::check<'_0>(move (@2)) + return +} + // Full name: test_crate::{impl Checkable for i32}::{vtable} fn {impl Checkable for i32}::{vtable}() -> test_crate::Checkable::{vtable} { @@ -278,7 +291,7 @@ fn {impl Checkable for i32}::{vtable}() -> test_crate::Checkable::{vtable}< @1 := () storage_live(@2) @2 := &{impl Super for i32}::{vtable} - ret@0 := test_crate::Checkable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_check: const ({impl Checkable for i32}::check), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2) } + ret@0 := test_crate::Checkable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_check: const ({impl Checkable for i32}::check::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2) } return } @@ -414,6 +427,23 @@ where return } +// Full name: test_crate::{impl Modifiable for i32}::modify::{vtable_method} +fn {impl Modifiable for i32}::modify::{vtable_method}<'_0, '_1, T>(@1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)), @2: &'_1 (T)) -> T +where + [@TraitClause0]: Sized, + [@TraitClause1]: Clone, +{ + let @0: T; // return + let @1: &'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)); // arg #1 + let @2: &'_1 (T); // arg #2 + let @3: &'_0 mut (i32); // anonymous local + + storage_live(@3) + @3 := concretize<&'_0 mut ((dyn exists<_dyn> [@TraitClause0]: Modifiable<_dyn, T> + _dyn : '_)), &'_0 mut (i32)>(move (@1)) + @0 := {impl Modifiable for i32}::modify<'_0, '_1, T>[@TraitClause0, @TraitClause1](move (@3), move (@2)) + return +} + // Full name: test_crate::{impl Modifiable for i32}::{vtable} fn {impl Modifiable for i32}::{vtable}() -> test_crate::Modifiable::{vtable} where @@ -422,7 +452,7 @@ where { let ret@0: test_crate::Modifiable::{vtable}; // return - ret@0 := test_crate::Modifiable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_modify: const ({impl Modifiable for i32}::modify[@TraitClause0, @TraitClause1]), super_trait_0: const (Opaque(missing supertrait vtable)) } + ret@0 := test_crate::Modifiable::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_modify: const ({impl Modifiable for i32}::modify::{vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: const (Opaque(missing supertrait vtable)) } return } @@ -689,7 +719,7 @@ fn {impl Both32And64 for i32}::{vtable}() -> test_crate::Both32And64::{vtable} @3 := () storage_live(@4) @4 := &{impl BaseOn for i32}::{vtable} - ret@0 := test_crate::Both32And64::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_both_operate: const (Opaque(shim for provided methods aren't yet supported)), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2), super_trait_2: move (@4) } + ret@0 := test_crate::Both32And64::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_both_operate: const (Opaque(shim for default methods aren't yet supported)), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2), super_trait_2: move (@4) } return } @@ -713,6 +743,116 @@ trait Alias vtable: test_crate::Alias::{vtable} } +struct test_crate::LifetimeTrait::{vtable} { + size: usize, + align: usize, + drop: fn(*mut (dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = Ty0)), + method_lifetime_method: fn<'a, '_1>(&'_0_1 ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = Ty0)), &'a (LifetimeTrait<(dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = Ty0)>::Ty)) -> &'a (LifetimeTrait<(dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = Ty0)>::Ty), + super_trait_0: &'static (core::marker::MetaSized::{vtable}), +} + +// Full name: test_crate::LifetimeTrait +trait LifetimeTrait +{ + parent_clause0 : [@TraitClause0]: MetaSized + parent_clause1 : [@TraitClause1]: Sized + type Ty + fn lifetime_method<'a, '_1> = test_crate::LifetimeTrait::lifetime_method<'a, '_0_1, Self>[Self] + vtable: test_crate::LifetimeTrait::{vtable} +} + +fn test_crate::LifetimeTrait::lifetime_method<'a, '_1, Self>(@1: &'_1 (Self), @2: &'a (@TraitClause0::Ty)) -> &'a (@TraitClause0::Ty) +where + [@TraitClause0]: LifetimeTrait, + +// Full name: test_crate::{impl LifetimeTrait for i32}::lifetime_method +fn {impl LifetimeTrait for i32}::lifetime_method<'a, '_1>(@1: &'_1 (i32), @2: &'a (i32)) -> &'a (i32) +{ + let @0: &'_ (i32); // return + let self@1: &'_ (i32); // arg #1 + let arg@2: &'_ (i32); // arg #2 + let @3: bool; // anonymous local + let @4: i32; // anonymous local + let @5: i32; // anonymous local + + storage_live(@3) + storage_live(@4) + @4 := copy (*(self@1)) + storage_live(@5) + @5 := copy (*(arg@2)) + @3 := move (@4) > move (@5) + if move (@3) { + } + else { + storage_dead(@5) + storage_dead(@4) + panic(core::panicking::panic) + } + storage_dead(@5) + storage_dead(@4) + storage_dead(@3) + @0 := copy (arg@2) + return +} + +// Full name: test_crate::{impl LifetimeTrait for i32}::lifetime_method::{vtable_method} +fn {impl LifetimeTrait for i32}::lifetime_method::{vtable_method}<'a, '_1>(@1: &'_1 ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)), @2: &'a (i32)) -> &'a (i32) +{ + let @0: &'a (i32); // return + let @1: &'_1 ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)); // arg #1 + let @2: &'a (i32); // arg #2 + let @3: &'_1 (i32); // anonymous local + + storage_live(@3) + @3 := concretize<&'_1 ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)), &'_1 (i32)>(move (@1)) + @0 := {impl LifetimeTrait for i32}::lifetime_method<'a, '_1>(move (@3), move (@2)) + return +} + +// Full name: test_crate::{impl LifetimeTrait for i32}::{vtable} +fn {impl LifetimeTrait for i32}::{vtable}() -> test_crate::LifetimeTrait::{vtable} +{ + let ret@0: test_crate::LifetimeTrait::{vtable}; // return + + ret@0 := test_crate::LifetimeTrait::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_lifetime_method: const ({impl LifetimeTrait for i32}::lifetime_method::{vtable_method}<'_, '_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + return +} + +// Full name: test_crate::{impl LifetimeTrait for i32}::{vtable} +static {impl LifetimeTrait for i32}::{vtable}: test_crate::LifetimeTrait::{vtable} = {impl LifetimeTrait for i32}::{vtable}() + +// Full name: test_crate::{impl LifetimeTrait for i32} +impl LifetimeTrait for i32 { + parent_clause0 = MetaSized + parent_clause1 = Sized + type Ty = i32 + fn lifetime_method<'a, '_1> = {impl LifetimeTrait for i32}::lifetime_method<'a, '_0_1> + vtable: {impl LifetimeTrait for i32}::{vtable} +} + +// Full name: test_crate::use_lifetime_trait +fn use_lifetime_trait<'a, '_1>(@1: &'_1 ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_1 + @TraitClause1_0::Ty = i32)), @2: &'a (i32)) -> &'a (i32) +{ + let @0: &'_ (i32); // return + let x@1: &'_ ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)); // arg #1 + let y@2: &'_ (i32); // arg #2 + let @3: &'_ (i32); // anonymous local + let @4: &'_ ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)); // anonymous local + let @5: &'_ (i32); // anonymous local + + storage_live(@3) + storage_live(@4) + @4 := &*(x@1) with_metadata(copy (x@1.metadata)) + storage_live(@5) + @5 := &*(y@2) + @3 := LifetimeTrait<(dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)>::lifetime_method<'_, '_>(move (@4), move (@5)) + @0 := &*(@3) + storage_dead(@5) + storage_dead(@4) + storage_dead(@3) + return +} + // Full name: test_crate::use_alias fn use_alias<'_0>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: Both32And64<_dyn> + _dyn : '_0))) { @@ -819,6 +959,32 @@ fn main() let @57: &'_ (i64); // anonymous local let @58: &'_ (i64); // anonymous local let @59: i64; // anonymous local + let b@60: &'_ ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)); // local + let @61: &'_ (i32); // anonymous local + let @62: &'_ (i32); // anonymous local + let @63: i32; // anonymous local + let @64: (&'_ (i32), &'_ (i32)); // anonymous local + let @65: &'_ (i32); // anonymous local + let @66: &'_ (i32); // anonymous local + let @67: &'_ ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)); // anonymous local + let @68: &'_ ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)); // anonymous local + let @69: &'_ (i32); // anonymous local + let @70: &'_ (i32); // anonymous local + let @71: i32; // anonymous local + let @72: &'_ (i32); // anonymous local + let @73: i32; // anonymous local + let left_val@74: &'_ (i32); // local + let right_val@75: &'_ (i32); // local + let @76: bool; // anonymous local + let @77: i32; // anonymous local + let @78: i32; // anonymous local + let kind@79: AssertKind; // local + let @80: AssertKind; // anonymous local + let @81: &'_ (i32); // anonymous local + let @82: &'_ (i32); // anonymous local + let @83: &'_ (i32); // anonymous local + let @84: &'_ (i32); // anonymous local + let @85: Option>[Sized>]; // anonymous local @0 := () storage_live(x@1) @@ -1002,7 +1168,85 @@ fn main() storage_dead(@56) storage_dead(@55) storage_dead(@52) + storage_live(b@60) + storage_live(@61) + storage_live(@62) + storage_live(@63) + @63 := const (42 : i32) + @62 := &@63 + @61 := &*(@62) + b@60 := unsize_cast<&'_ (i32), &'_ ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)), {impl LifetimeTrait for i32}>(move (@61)) + storage_dead(@61) + storage_dead(@62) + storage_live(@64) + storage_live(@65) + storage_live(@66) + storage_live(@67) + storage_live(@68) + @68 := &*(b@60) with_metadata(copy (b@60.metadata)) + @67 := unsize_cast<&'_ ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)), &'_ ((dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)), LifetimeTrait<(dyn exists<_dyn> [@TraitClause0]: LifetimeTrait<_dyn> + _dyn : '_ + @TraitClause1_0::Ty = i32)>>(move (@68)) + storage_dead(@68) + storage_live(@69) + storage_live(@70) + storage_live(@71) + @71 := const (10 : i32) + @70 := &@71 + @69 := &*(@70) + @66 := use_lifetime_trait<'_, '_>(move (@67), move (@69)) + storage_dead(@69) + storage_dead(@67) + @65 := &*(@66) + storage_live(@72) + storage_live(@73) + @73 := const (10 : i32) + @72 := &@73 + @64 := (move (@65), move (@72)) + storage_dead(@72) + storage_dead(@65) + storage_live(left_val@74) + left_val@74 := copy ((@64).0) + storage_live(right_val@75) + right_val@75 := copy ((@64).1) + storage_live(@76) + storage_live(@77) + @77 := copy (*(left_val@74)) + storage_live(@78) + @78 := copy (*(right_val@75)) + @76 := move (@77) == move (@78) + if move (@76) { + } + else { + storage_dead(@78) + storage_dead(@77) + storage_live(kind@79) + kind@79 := AssertKind::Eq { } + storage_live(@80) + @80 := move (kind@79) + storage_live(@81) + storage_live(@82) + @82 := &*(left_val@74) + @81 := &*(@82) + storage_live(@83) + storage_live(@84) + @84 := &*(right_val@75) + @83 := &*(@84) + storage_live(@85) + @85 := Option::None { } + panic(core::panicking::assert_failed) + } + storage_dead(@78) + storage_dead(@77) + storage_dead(@76) + storage_dead(right_val@75) + storage_dead(left_val@74) + storage_dead(@73) + storage_dead(@71) + storage_dead(@70) + storage_dead(@66) + storage_dead(@64) @0 := () + storage_dead(@63) + storage_dead(b@60) storage_dead(@51) storage_dead(a@48) storage_dead(z@40) diff --git a/charon/tests/ui/vtables.rs b/charon/tests/ui/vtables.rs index 802dc04b5..9393d084b 100644 --- a/charon/tests/ui/vtables.rs +++ b/charon/tests/ui/vtables.rs @@ -64,6 +64,21 @@ impl BaseOn for i32 { impl Both32And64 for i32 {} trait Alias = Both32And64; +trait LifetimeTrait { + type Ty; + fn lifetime_method<'a>(&self, arg: &'a Self::Ty) -> &'a Self::Ty; +} +impl LifetimeTrait for i32 { + type Ty = i32; + fn lifetime_method<'a>(&self, arg: &'a Self::Ty) -> &'a Self::Ty { + assert!(*self > *arg); + arg + } +} +fn use_lifetime_trait<'a>(x: &dyn LifetimeTrait, y: &'a i32) -> &'a i32 { + x.lifetime_method(y) +} + fn use_alias(x: &dyn Alias) { x.both_operate(&100, &200); } @@ -78,4 +93,6 @@ fn main() { z.dummy(); let a: &dyn Both32And64 = &42; a.both_operate(&100, &200); + let b: &dyn LifetimeTrait = &42; + assert_eq!(*use_lifetime_trait(b, &10), 10); }