From 917dd14896a2da1ce49f1e779e2686c38facb402 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 13 Oct 2025 13:37:30 +0200 Subject: [PATCH 1/4] Add helper for building ullbc bodies --- charon/src/ast/gast_utils.rs | 5 + charon/src/ast/ullbc_ast_utils.rs | 88 +++++++++++ .../translate/translate_closures.rs | 125 +++++---------- .../translate/translate_functions.rs | 27 ++-- .../translate/translate_items.rs | 16 +- .../translate/translate_trait_objects.rs | 142 +++++------------- charon/src/pretty/fmt_with_ctx.rs | 7 +- .../insert_storage_lives.rs | 2 +- .../simplify_output/remove_unused_locals.rs | 2 +- charon/tests/ui/closure-as-fn.out | 4 +- ...e-inside-impl-with-bound-with-assoc-ty.out | 2 +- charon/tests/ui/rvalues.out | 4 +- .../tests/ui/simple/closure-inside-impl.out | 2 +- .../closure-uses-ambient-self-clause.out | 2 +- charon/tests/ui/simple/closure-with-drops.out | 2 +- 15 files changed, 196 insertions(+), 234 deletions(-) diff --git a/charon/src/ast/gast_utils.rs b/charon/src/ast/gast_utils.rs index 6810910cd..abc9e0598 100644 --- a/charon/src/ast/gast_utils.rs +++ b/charon/src/ast/gast_utils.rs @@ -74,6 +74,11 @@ impl Locals { Place::new(local_id, ty) } + /// Returns whether this local is the special return local or one of the input argument locals. + pub fn is_return_or_arg(&self, lid: LocalId) -> bool { + lid.index() <= self.arg_count + } + /// The place where we write the return value. pub fn return_place(&self) -> Place { self.place_for_var(LocalId::new(0)) diff --git a/charon/src/ast/ullbc_ast_utils.rs b/charon/src/ast/ullbc_ast_utils.rs index 994732fac..61dbe7e3e 100644 --- a/charon/src/ast/ullbc_ast_utils.rs +++ b/charon/src/ast/ullbc_ast_utils.rs @@ -209,3 +209,91 @@ impl ExprBody { } } } + +/// Helper to construct a small ullbc body. +pub struct BodyBuilder { + /// The span to use for everything. + pub span: Span, + /// Body under construction. + pub body: ExprBody, + /// Block onto which we're adding statements. Its terminator is always `Return`. + pub current_block: BlockId, + /// Block to unwind to; created on demand. + pub unwind_block: Option, +} + +fn mk_block(span: Span, term: TerminatorKind) -> BlockData { + BlockData { + statements: vec![], + terminator: Terminator::new(span, term), + } +} + +impl BodyBuilder { + pub fn new(span: Span, arg_count: usize) -> Self { + let mut body: ExprBody = GExprBody { + span, + locals: Locals::new(arg_count), + comments: vec![], + body: Vector::new(), + }; + let current_block = body.body.push(BlockData { + statements: Default::default(), + terminator: Terminator::new(span, TerminatorKind::Return), + }); + Self { + span, + body, + current_block, + unwind_block: None, + } + } + + /// Finalize the builder by returning the built body. + pub fn build(self) -> ExprBody { + self.body + } + + /// Create a new local. Adds a `StorageLive` statement if the local is not one of the special + /// ones (return or function argument). + pub fn new_var(&mut self, name: Option, ty: Ty) -> Place { + let place = self.body.locals.new_var(name, ty); + let local_id = place.as_local().unwrap(); + if !self.body.locals.is_return_or_arg(local_id) { + self.push_statement(StatementKind::StorageLive(local_id)); + } + place + } + + /// Helper. + fn current_block(&mut self) -> &mut BlockData { + &mut self.body.body[self.current_block] + } + + pub fn push_statement(&mut self, kind: StatementKind) { + let st = Statement::new(self.span, kind); + self.current_block().statements.push(st); + } + + fn unwind_block(&mut self) -> BlockId { + *self.unwind_block.get_or_insert_with(|| { + self.body + .body + .push(mk_block(self.span, TerminatorKind::UnwindResume)) + }) + } + + pub fn call(&mut self, call: Call) { + let next_block = self + .body + .body + .push(mk_block(self.span, TerminatorKind::Return)); + let term = TerminatorKind::Call { + target: next_block, + call, + on_unwind: self.unwind_block(), + }; + self.current_block().terminator.kind = term; + self.current_block = next_block; + } +} diff --git a/charon/src/bin/charon-driver/translate/translate_closures.rs b/charon/src/bin/charon-driver/translate/translate_closures.rs index 4e384d0db..1783aceae 100644 --- a/charon/src/bin/charon-driver/translate/translate_closures.rs +++ b/charon/src/bin/charon-driver/translate/translate_closures.rs @@ -44,6 +44,7 @@ use crate::translate::translate_bodies::BodyTransCtx; use super::translate_crate::TransItemSourceKind; use super::translate_ctx::*; +use charon_lib::ast::ullbc_ast_utils::BodyBuilder; use charon_lib::ast::*; use charon_lib::ids::Vector; use charon_lib::ullbc_ast::*; @@ -350,14 +351,6 @@ impl ItemTransCtx<'_, '_> { ) -> Result, Error> { use ClosureKind::*; let closure_kind = translate_closure_kind(&args.kind); - let mk_stt = |content| Statement::new(span, content); - let mk_block = |statements, terminator| -> BlockData { - BlockData { - statements, - terminator: Terminator::new(span, terminator), - } - }; - Ok(match (target_kind, closure_kind) { (Fn, Fn) | (FnMut, FnMut) | (FnOnce, FnOnce) => { // Translate the function's body normally @@ -379,9 +372,8 @@ impl ItemTransCtx<'_, '_> { } = body.as_unstructured_mut().unwrap(); blocks.dyn_visit_mut(|local: &mut LocalId| { - let idx = local.index(); - if idx >= 2 { - *local = LocalId::new(idx + 1) + if local.index() >= 2 { + *local += 1; } }); @@ -406,10 +398,14 @@ impl ItemTransCtx<'_, '_> { ), ty, ); - mk_stt(StatementKind::Assign( - locals.place_for_var(LocalId::new(i + 3)), - Rvalue::Use(Operand::Move(nth_field)), - )) + let local_id = LocalId::new(i + 3); + Statement::new( + span, + StatementKind::Assign( + locals.place_for_var(local_id), + Rvalue::Use(Operand::Move(nth_field)), + ), + ) }); blocks[BlockId::ZERO].statements.splice(0..0, new_stts); @@ -467,19 +463,17 @@ impl ItemTransCtx<'_, '_> { })), }); - let mut locals = Locals::new(2); - let mut statements = vec![]; - let mut blocks = Vector::default(); + let mut builder = BodyBuilder::new(span, 2); - let output = locals.new_var(None, signature.output.clone()); - let state = locals.new_var(Some("state".to_string()), signature.inputs[0].clone()); - let args = locals.new_var(Some("args".to_string()), signature.inputs[1].clone()); + let output = builder.new_var(None, signature.output.clone()); + let state = builder.new_var(Some("state".to_string()), signature.inputs[0].clone()); + let args = builder.new_var(Some("args".to_string()), signature.inputs[1].clone()); let deref_state = state.deref(); let reborrow_ty = TyKind::Ref(Region::Erased, deref_state.ty.clone(), RefKind::Shared).into_ty(); - let reborrow = locals.new_var(None, reborrow_ty); + let reborrow = builder.new_var(None, reborrow_ty); - statements.push(mk_stt(StatementKind::Assign( + builder.push_statement(StatementKind::Assign( reborrow.clone(), // the state must be Sized, hence `()` as ptr-metadata Rvalue::Ref { @@ -487,29 +481,15 @@ impl ItemTransCtx<'_, '_> { kind: BorrowKind::Shared, ptr_metadata: Operand::mk_const_unit(), }, - ))); - - let start_block = blocks.reserve_slot(); - let ret_block = blocks.push(mk_block(vec![], TerminatorKind::Return)); - let unwind_block = blocks.push(mk_block(vec![], TerminatorKind::UnwindResume)); - let call = TerminatorKind::Call { - target: ret_block, - call: Call { - func: fn_op, - args: vec![Operand::Move(reborrow), Operand::Move(args)], - dest: output, - }, - on_unwind: unwind_block, - }; - blocks.set_slot(start_block, mk_block(statements, call)); + )); - let body: ExprBody = GExprBody { - span, - locals, - comments: vec![], - body: blocks, - }; - Ok(Body::Unstructured(body)) + builder.call(Call { + func: fn_op, + args: vec![Operand::Move(reborrow), Operand::Move(args)], + dest: output, + }); + + Ok(Body::Unstructured(builder.build())) } (Fn, FnOnce) | (Fn, FnMut) | (FnMut, FnOnce) => { panic!( @@ -700,13 +680,6 @@ impl ItemTransCtx<'_, '_> { // let args = (arg0, ..., argN); // closure.call(args) // } - let mk_stt = |content| Statement::new(span, content); - let mk_block = |statements, terminator| -> BlockData { - BlockData { - statements, - terminator: Terminator::new(span, terminator), - } - }; let fun_id: FunDeclId = self.register_item( span, def.this(), @@ -718,55 +691,39 @@ impl ItemTransCtx<'_, '_> { generics: impl_ref.generics.clone(), }); - let mut locals = Locals::new(signature.inputs.len()); - let mut statements = vec![]; - let mut blocks = Vector::default(); + let mut builder = BodyBuilder::new(span, signature.inputs.len()); - let output = locals.new_var(None, signature.output.clone()); + let output = builder.new_var(None, signature.output.clone()); let args: Vec = signature .inputs .iter() .enumerate() - .map(|(i, ty)| locals.new_var(Some(format!("arg{}", i + 1)), ty.clone())) + .map(|(i, ty)| builder.new_var(Some(format!("arg{}", i + 1)), ty.clone())) .collect(); - let args_tupled = locals.new_var(Some("args".to_string()), args_tuple_ty.clone()); - let state = locals.new_var(Some("state".to_string()), state_ty.clone()); + let args_tupled = builder.new_var(Some("args".to_string()), args_tuple_ty.clone()); + let state = builder.new_var(Some("state".to_string()), state_ty.clone()); - statements.push(mk_stt(StatementKind::Assign( + builder.push_statement(StatementKind::Assign( args_tupled.clone(), Rvalue::Aggregate( AggregateKind::Adt(args_tuple_ty.as_adt().unwrap().clone(), None, None), args.into_iter().map(Operand::Move).collect(), ), - ))); + )); let state_ty_adt = state_ty.as_adt().unwrap(); - statements.push(mk_stt(StatementKind::Assign( + builder.push_statement(StatementKind::Assign( state.clone(), Rvalue::Aggregate(AggregateKind::Adt(state_ty_adt.clone(), None, None), vec![]), - ))); - - let start_block = blocks.reserve_slot(); - let ret_block = blocks.push(mk_block(vec![], TerminatorKind::Return)); - let unwind_block = blocks.push(mk_block(vec![], TerminatorKind::UnwindResume)); - let call = TerminatorKind::Call { - target: ret_block, - call: Call { - func: fn_op, - args: vec![Operand::Move(state), Operand::Move(args_tupled)], - dest: output, - }, - on_unwind: unwind_block, - }; - blocks.set_slot(start_block, mk_block(statements, call)); + )); - let body: ExprBody = GExprBody { - span, - locals, - comments: vec![], - body: blocks, - }; - Ok(Body::Unstructured(body)) + builder.call(Call { + func: fn_op, + args: vec![Operand::Move(state), Operand::Move(args_tupled)], + dest: output, + }); + + Ok(Body::Unstructured(builder.build())) }; Ok(FunDecl { diff --git a/charon/src/bin/charon-driver/translate/translate_functions.rs b/charon/src/bin/charon-driver/translate/translate_functions.rs index 28baee089..ddb8fb908 100644 --- a/charon/src/bin/charon-driver/translate/translate_functions.rs +++ b/charon/src/bin/charon-driver/translate/translate_functions.rs @@ -6,6 +6,7 @@ use std::panic; use super::translate_ctx::*; +use charon_lib::ast::ullbc_ast_utils::BodyBuilder; use charon_lib::ast::*; use charon_lib::common::*; use charon_lib::formatter::IntoFormatter; @@ -106,13 +107,14 @@ impl ItemTransCtx<'_, '_> { let tref = self .translate_type_decl_ref(span, &def.this().with_def_id(self.hax_state(), adt_def_id))?; let output_ty = self.translate_ty(span, output_ty)?; - let mut locals = Locals::new(fields.len()); - locals.new_var(None, output_ty); + + let mut builder = BodyBuilder::new(span, fields.len()); + let return_place = builder.new_var(None, output_ty); let args: Vec<_> = fields .iter() .map(|field| -> Result { let ty = self.translate_ty(span, &field.ty)?; - let place = locals.new_var(None, ty); + let place = builder.new_var(None, ty); Ok(Operand::Move(place)) }) .try_collect()?; @@ -120,22 +122,11 @@ impl ItemTransCtx<'_, '_> { hax::CtorOf::Struct => None, hax::CtorOf::Variant => Some(VariantId::from(variant_id)), }; - let st_kind = StatementKind::Assign( - locals.return_place(), + builder.push_statement(StatementKind::Assign( + return_place, Rvalue::Aggregate(AggregateKind::Adt(tref, variant, None), args), - ); - let statement = Statement::new(span, st_kind); - let block = BlockData { - statements: vec![statement], - terminator: Terminator::new(span, TerminatorKind::Return), - }; - let body = Body::Unstructured(GExprBody { - span, - locals, - comments: Default::default(), - body: [block].into_iter().collect(), - }); - Ok(body) + )); + Ok(Body::Unstructured(builder.build())) } /// Checks whether the given id corresponds to a built-in type. diff --git a/charon/src/bin/charon-driver/translate/translate_items.rs b/charon/src/bin/charon-driver/translate/translate_items.rs index bfd82dd27..4be227fa0 100644 --- a/charon/src/bin/charon-driver/translate/translate_items.rs +++ b/charon/src/bin/charon-driver/translate/translate_items.rs @@ -1,6 +1,7 @@ use super::translate_bodies::BodyTransCtx; use super::translate_crate::*; use super::translate_ctx::*; +use charon_lib::ast::ullbc_ast_utils::BodyBuilder; use charon_lib::ast::*; use charon_lib::formatter::IntoFormatter; use charon_lib::pretty::FmtWithCtx; @@ -209,18 +210,9 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> { }; let body = { - let mut body = GExprBody { - span: Span::dummy(), - locals: Locals::new(0), - comments: Default::default(), - body: Vector::default(), - }; - let _ = body.locals.new_var(None, Ty::mk_unit()); - body.body.push(BlockData { - statements: Default::default(), - terminator: Terminator::new(Span::dummy(), TerminatorKind::Return), - }); - body + let mut builder = BodyBuilder::new(Span::dummy(), 0); + let _ = builder.new_var(None, Ty::mk_unit()); + builder.build() }; let global_id = self.translated.global_decls.reserve_slot(); 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 7acc03a82..c2ee9a0f3 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -1,3 +1,4 @@ +use charon_lib::ast::ullbc_ast_utils::BodyBuilder; use itertools::Itertools; use std::mem; @@ -695,9 +696,9 @@ impl ItemTransCtx<'_, '_> { impl_def: &hax::FullDef, vtable_struct_ref: TypeDeclRef, ) -> Result { - let mut locals = Locals::new(0); + let mut builder = BodyBuilder::new(span, 0); let ret_ty = Ty::new(TyKind::Adt(vtable_struct_ref.clone())); - let ret_place = locals.new_var(Some("ret".into()), ret_ty.clone()); + let ret_place = builder.new_var(Some("ret".into()), ret_ty.clone()); let hax::FullDefKind::TraitImpl { trait_pred, items, .. @@ -726,7 +727,6 @@ impl ItemTransCtx<'_, '_> { .collect_vec() }; - let mut statements = vec![]; let mut aggregate_fields = vec![]; // For each vtable field, assign the desired value to a new local. let mut field_ty_iter = field_tys.into_iter(); @@ -755,48 +755,15 @@ impl ItemTransCtx<'_, '_> { } // Construct the final struct. - statements.push(Statement::new( - span, - StatementKind::Assign( - ret_place, - Rvalue::Aggregate( - AggregateKind::Adt(vtable_struct_ref.clone(), None, None), - aggregate_fields, - ), + builder.push_statement(StatementKind::Assign( + ret_place, + Rvalue::Aggregate( + AggregateKind::Adt(vtable_struct_ref.clone(), None, None), + aggregate_fields, ), )); - let block = BlockData { - statements, - terminator: Terminator::new(span, TerminatorKind::Return), - }; - - Ok(Body::Unstructured(GExprBody { - span, - locals, - comments: Vec::new(), - body: [block].into(), - })) - } - - 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(()) + Ok(Body::Unstructured(builder.build())) } pub(crate) fn translate_vtable_instance_init( @@ -874,23 +841,15 @@ impl ItemTransCtx<'_, '_> { 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 mut builder = BodyBuilder::new(span, shim_signature.inputs.len()); - let ret_place = locals.new_var(None, shim_signature.output.clone()); + let ret_place = builder.new_var(None, shim_signature.output.clone()); let mut method_args = shim_signature .inputs .iter() - .map(|ty| locals.new_var(None, ty.clone())) + .map(|ty| builder.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()), - )); + let target_self = builder.new_var(None, target_receiver.clone()); // Replace the `dyn Trait` receiver with the concrete one. let shim_self = mem::replace(&mut method_args[0], target_self.clone()); @@ -898,59 +857,30 @@ impl ItemTransCtx<'_, '_> { // 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) + let rval = Rvalue::UnaryOp( + UnOp::Cast(CastKind::Concretize( + shim_self.ty().clone(), + target_self.ty().clone(), + )), + Operand::Move(shim_self.clone()), + ); + builder.push_statement(StatementKind::Assign(target_self.clone(), rval)); + + let fun_id = self.register_item(span, &impl_func_def.this(), TransItemSourceKind::Fun); + let generics = Box::new(self.outermost_binder().params.identity_args()); + builder.call(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, + }); - Ok(Body::Unstructured(GExprBody { - span, - locals, - comments: Vec::new(), - body: blocks, - })) + Ok(Body::Unstructured(builder.build())) } pub(crate) fn translate_vtable_shim( diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs index 733392b38..f2c7edfae 100644 --- a/charon/src/pretty/fmt_with_ctx.rs +++ b/charon/src/pretty/fmt_with_ctx.rs @@ -697,11 +697,10 @@ impl GExprBody { write!(f, "let {v}: {};", v.ty.with_ctx(ctx))?; write!(f, " // ")?; - let index = v.index.index(); - if index == 0 { + if v.index.is_zero() { write!(f, "return")?; - } else if index <= self.locals.arg_count { - write!(f, "arg #{index}")? + } else if self.locals.is_return_or_arg(v.index) { + write!(f, "arg #{}", v.index.index())? } else { match &v.name { Some(_) => write!(f, "local")?, diff --git a/charon/src/transform/finish_translation/insert_storage_lives.rs b/charon/src/transform/finish_translation/insert_storage_lives.rs index 4d9a065ec..208728621 100644 --- a/charon/src/transform/finish_translation/insert_storage_lives.rs +++ b/charon/src/transform/finish_translation/insert_storage_lives.rs @@ -23,7 +23,7 @@ enum LocalStatus { impl StorageVisitor { fn new(locals: &Locals) -> Self { let local_status = locals.locals.map_ref(|local| { - if local.index <= locals.arg_count { + if locals.is_return_or_arg(local.index) { // The return and argument places count as having a `StorageLive` already. LocalStatus::UsedAndHasExplicitStorage } else { diff --git a/charon/src/transform/simplify_output/remove_unused_locals.rs b/charon/src/transform/simplify_output/remove_unused_locals.rs index 7b752b293..8b74f3db3 100644 --- a/charon/src/transform/simplify_output/remove_unused_locals.rs +++ b/charon/src/transform/simplify_output/remove_unused_locals.rs @@ -79,7 +79,7 @@ fn remove_unused_locals(body: &mut GExprBody) { used_locals: body .locals .locals - .map_ref(|local| local.index <= body.locals.arg_count), + .map_ref(|local| body.locals.is_return_or_arg(local.index)), }; let _ = body.body.drive_body(&mut visitor); let used_locals = visitor.used_locals; diff --git a/charon/tests/ui/closure-as-fn.out b/charon/tests/ui/closure-as-fn.out index d030f2887..f20f5975b 100644 --- a/charon/tests/ui/closure-as-fn.out +++ b/charon/tests/ui/closure-as-fn.out @@ -120,8 +120,8 @@ fn {impl FnMut<()> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: ()) let args@2: (); // arg #2 let @3: &'_ (closure); // anonymous local - storage_live(@3) @0 := () + storage_live(@3) @3 := &*(state@1) @0 := {impl Fn<()> for closure}::call<'_>(move (@3), move (args@2)) return @@ -150,9 +150,9 @@ fn as_fn() let args@1: (); // local let state@2: closure; // local + @0 := () storage_live(args@1) storage_live(state@2) - @0 := () args@1 := () state@2 := closure { } @0 := {impl FnOnce<()> for closure}::call_once(move (state@2), move (args@1)) diff --git a/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out b/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out index e97743dc1..dba40b831 100644 --- a/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out +++ b/charon/tests/ui/regressions/closure-inside-impl-with-bound-with-assoc-ty.out @@ -161,8 +161,8 @@ where let args@2: (()); // arg #2 let @3: &'_ (closure[@TraitClause0, @TraitClause1]); // anonymous local - storage_live(@3) @0 := () + storage_live(@3) @3 := &*(state@1) @0 := {impl Fn<(()), ()> for closure[@TraitClause0, @TraitClause1]}::call<'_, F, Clause1_Repr>[@TraitClause0, @TraitClause1](move (@3), move (args@2)) return diff --git a/charon/tests/ui/rvalues.out b/charon/tests/ui/rvalues.out index 38c3ef2f4..b5caa7f68 100644 --- a/charon/tests/ui/rvalues.out +++ b/charon/tests/ui/rvalues.out @@ -333,8 +333,8 @@ fn {impl FnMut<(u8)> for closure}::call_mut<'_0>(@1: &'_0 mut (closure), @2: (u8 let args@2: (u8); // arg #2 let @3: &'_ (closure); // anonymous local - storage_live(@3) @0 := () + storage_live(@3) @3 := &*(state@1) @0 := {impl Fn<(u8)> for closure}::call<'_>(move (@3), move (args@2)) return @@ -364,9 +364,9 @@ fn as_fn(@1: u8) let args@2: (u8); // local let state@3: closure; // local + @0 := () storage_live(args@2) storage_live(state@3) - @0 := () args@2 := (move (arg1@1)) state@3 := closure { } @0 := {impl FnOnce<(u8)> for closure}::call_once(move (state@3), move (args@2)) diff --git a/charon/tests/ui/simple/closure-inside-impl.out b/charon/tests/ui/simple/closure-inside-impl.out index c7666e522..8336fc0af 100644 --- a/charon/tests/ui/simple/closure-inside-impl.out +++ b/charon/tests/ui/simple/closure-inside-impl.out @@ -154,8 +154,8 @@ where let args@2: (()); // arg #2 let @3: &'_ (closure[@TraitClause0, @TraitClause1]); // anonymous local - storage_live(@3) @0 := () + storage_live(@3) @3 := &*(state@1) @0 := {impl Fn<(())> for closure[@TraitClause0, @TraitClause1]}::call<'_, F, T>[@TraitClause0, @TraitClause1](move (@3), move (args@2)) return diff --git a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out index eb917492d..2f3cc58b2 100644 --- a/charon/tests/ui/simple/closure-uses-ambient-self-clause.out +++ b/charon/tests/ui/simple/closure-uses-ambient-self-clause.out @@ -168,8 +168,8 @@ where let args@2: (@TraitClause0::Item); // arg #2 let @3: &'_ (closure[@TraitClause0]); // anonymous local - storage_live(@3) @0 := () + storage_live(@3) @3 := &*(state@1) @0 := {impl Fn<(@TraitClause0::Item)> for closure[@TraitClause0]}::call<'_, Self>[@TraitClause0](move (@3), move (args@2)) return diff --git a/charon/tests/ui/simple/closure-with-drops.out b/charon/tests/ui/simple/closure-with-drops.out index e71a96851..13312b94d 100644 --- a/charon/tests/ui/simple/closure-with-drops.out +++ b/charon/tests/ui/simple/closure-with-drops.out @@ -207,8 +207,8 @@ fn {impl FnMut<()> for test_crate::bar::closure}::call_mut<'_0>(@1: &'_0 mut (te let args@2: (); // arg #2 let @3: &'_ (test_crate::bar::closure); // anonymous local - storage_live(@3) @0 := () + storage_live(@3) @3 := &*(state@1) @0 := {impl Fn<()> for test_crate::bar::closure}::call<'_>(move (@3), move (args@2)) return From 3205b23b44823801ff54f4b1531e07ea1d51eb7c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 13 Oct 2025 13:47:44 +0200 Subject: [PATCH 2/4] drive-by: add test for coinductive trait ref --- .../ui/simple/coinductive-perfect-derive.out | 17 +++++++++++++ .../ui/simple/coinductive-perfect-derive.rs | 25 +++++++++++++++++++ 2 files changed, 42 insertions(+) create mode 100644 charon/tests/ui/simple/coinductive-perfect-derive.out create mode 100644 charon/tests/ui/simple/coinductive-perfect-derive.rs diff --git a/charon/tests/ui/simple/coinductive-perfect-derive.out b/charon/tests/ui/simple/coinductive-perfect-derive.out new file mode 100644 index 000000000..040250f3a --- /dev/null +++ b/charon/tests/ui/simple/coinductive-perfect-derive.out @@ -0,0 +1,17 @@ +error[E0599]: no method named `clone` found for enum `List` in the current scope + --> tests/ui/simple/coinductive-perfect-derive.rs:24:18 + | +2 | enum List { + | ------------ method `clone` not found for this enum +... +24 | let _ = list.clone(); + | ^^^^^ method not found in `List` + | + = help: items from traits can only be used if the trait is implemented and in scope + = note: the following trait defines an item `clone`, perhaps you need to implement it: + candidate #1: `std::clone::Clone` + +error: aborting due to 1 previous error + +For more information about this error, try `rustc --explain E0599`. +ERROR Code failed to compile diff --git a/charon/tests/ui/simple/coinductive-perfect-derive.rs b/charon/tests/ui/simple/coinductive-perfect-derive.rs new file mode 100644 index 000000000..70627a2da --- /dev/null +++ b/charon/tests/ui/simple/coinductive-perfect-derive.rs @@ -0,0 +1,25 @@ +//@ known-failure +enum List { + Nil, + Cons(T, Box>), +} + +// This is the code emitted by "perfect derive" macros. The second where bound forces any proof of +// `List: Clone` to be coinductive. +impl Clone for List +where + T: Clone, + Box>: Clone, +{ + fn clone(&self) -> Self { + match self { + Self::Nil => Self::Nil, + Self::Cons(x, q) => Self::Cons(x.clone(), q.clone()), + } + } +} + +fn main() { + let list: List = List::Nil; + let _ = list.clone(); +} From e27e91196c07dcdc2f24c3d8d05a4fef46348b94 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 13 Oct 2025 14:01:23 +0200 Subject: [PATCH 3/4] Fill in missing fields in vtables --- .../charon-driver/translate/translate_ctx.rs | 13 +++ .../translate/translate_trait_objects.rs | 54 +++++++--- .../tests/ui/dyn-with-diamond-supertraits.out | 96 +++++++++++------ charon/tests/ui/unsize.out | 14 ++- charon/tests/ui/vtable-simple.out | 14 ++- charon/tests/ui/vtables.out | 100 +++++++++++++----- 6 files changed, 216 insertions(+), 75 deletions(-) diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index 2f1351c57..f409647af 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -11,6 +11,7 @@ use std::borrow::Cow; use std::cell::RefCell; use std::collections::{BTreeSet, HashMap, HashSet}; use std::fmt::Debug; +use std::ops::{Deref, DerefMut}; use std::path::PathBuf; use std::sync::Arc; use std::{fmt, mem}; @@ -213,6 +214,18 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { } } +impl<'tcx> Deref for ItemTransCtx<'tcx, '_> { + type Target = TranslateCtx<'tcx>; + fn deref(&self) -> &Self::Target { + self.t_ctx + } +} +impl<'tcx> DerefMut for ItemTransCtx<'tcx, '_> { + fn deref_mut(&mut self) -> &mut Self::Target { + self.t_ctx + } +} + impl<'a> IntoFormatter for &'a TranslateCtx<'_> { type C = FmtCtx<'a>; fn into_fmt(self) -> Self::C { 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 c2ee9a0f3..b2f50ada7 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -520,7 +520,7 @@ impl ItemTransCtx<'_, '_> { span: Span, impl_def: &'a hax::FullDef, impl_kind: &TraitImplSource, - ) -> Result<(TraitImplRef, TraitDeclRef, TypeDeclRef), Error> { + ) -> Result<(TraitImplRef, TypeDeclRef), Error> { let implemented_trait = match impl_def.kind() { hax::FullDefKind::TraitImpl { trait_pred, .. } => &trait_pred.trait_ref, _ => unreachable!(), @@ -528,13 +528,12 @@ impl ItemTransCtx<'_, '_> { let vtable_struct_ref = self .translate_vtable_struct_ref(span, implemented_trait)? .expect("trait should be dyn-compatible"); - let implemented_trait = self.translate_trait_decl_ref(span, implemented_trait)?; let impl_ref = self.translate_item( span, impl_def.this(), TransItemSourceKind::TraitImpl(*impl_kind), )?; - Ok((impl_ref, implemented_trait, vtable_struct_ref)) + Ok((impl_ref, vtable_struct_ref)) } /// E.g., @@ -562,7 +561,7 @@ impl ItemTransCtx<'_, '_> { self.translate_def_generics(span, impl_def)?; 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( @@ -696,10 +695,6 @@ impl ItemTransCtx<'_, '_> { impl_def: &hax::FullDef, vtable_struct_ref: TypeDeclRef, ) -> Result { - let mut builder = BodyBuilder::new(span, 0); - let ret_ty = Ty::new(TyKind::Adt(vtable_struct_ref.clone())); - let ret_place = builder.new_var(Some("ret".into()), ret_ty.clone()); - let hax::FullDefKind::TraitImpl { trait_pred, items, .. } = impl_def.kind() @@ -707,6 +702,13 @@ impl ItemTransCtx<'_, '_> { unreachable!() }; let trait_def = self.hax_def(&trait_pred.trait_ref)?; + let implemented_trait = self.translate_trait_decl_ref(span, &trait_pred.trait_ref)?; + // The type this impl is for. + let self_ty = &implemented_trait.generics.types[0]; + + let mut builder = BodyBuilder::new(span, 0); + let ret_ty = Ty::new(TyKind::Adt(vtable_struct_ref.clone())); + let ret_place = builder.new_var(Some("ret".into()), ret_ty.clone()); // Retreive the expected field types from the struct definition. This avoids complicated // substitutions. @@ -730,15 +732,41 @@ impl ItemTransCtx<'_, '_> { let mut aggregate_fields = vec![]; // For each vtable field, assign the desired value to a new local. let mut field_ty_iter = field_tys.into_iter(); + + let size_ty = field_ty_iter.next().unwrap(); + let size_local = builder.new_var(Some("size".to_string()), size_ty); + builder.push_statement(StatementKind::Assign( + size_local.clone(), + Rvalue::NullaryOp(NullOp::SizeOf, self_ty.clone()), + )); + aggregate_fields.push(Operand::Move(size_local)); + + let align_ty = field_ty_iter.next().unwrap(); + let align_local = builder.new_var(Some("align".to_string()), align_ty); + builder.push_statement(StatementKind::Assign( + align_local.clone(), + Rvalue::NullaryOp(NullOp::AlignOf, self_ty.clone()), + )); + aggregate_fields.push(Operand::Move(align_local)); + + // 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 }))); }; - // TODO(dyn): provide values - mk_field(ConstantExprKind::Opaque("unknown size".to_string())); - mk_field(ConstantExprKind::Opaque("unknown align".to_string())); - mk_field(ConstantExprKind::Opaque("unknown drop".to_string())); + // Build a reference to `std::ptr::drop_in_place`. + let drop_in_place: hax::ItemRef = { + let hax_state = self.hax_state_with_id(); + let drop_in_place = self.tcx.lang_items().drop_in_place_fn().unwrap(); + let rustc_trait_args = trait_pred.trait_ref.rustc_args(&hax_state); + let generics = self.tcx.mk_args(&rustc_trait_args[..1]); // keep only the `Self` type + hax::ItemRef::translate(&hax_state, drop_in_place, generics) + }; + let fn_ptr = self + .translate_fn_ptr(span, &drop_in_place, TransItemSourceKind::Fun)? + .erase(); + mk_field(ConstantExprKind::FnPtr(fn_ptr)); for item in items { self.add_method_to_vtable_value(span, impl_def, item, &mut mk_field)?; @@ -777,7 +805,7 @@ impl ItemTransCtx<'_, '_> { self.translate_def_generics(span, impl_def)?; 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, diff --git a/charon/tests/ui/dyn-with-diamond-supertraits.out b/charon/tests/ui/dyn-with-diamond-supertraits.out index 0945e5e50..ddede4251 100644 --- a/charon/tests/ui/dyn-with-diamond-supertraits.out +++ b/charon/tests/ui/dyn-with-diamond-supertraits.out @@ -48,6 +48,10 @@ pub fn core::ops::arith::Add::add(@1: Self, @2: Rhs) -> @TraitClause0 where [@TraitClause0]: Add, +// Full name: core::ptr::drop_in_place +#[lang_item("drop_in_place")] +pub unsafe fn drop_in_place(@1: *mut T) + fn UNIT_METADATA() { let @0: (); // return @@ -214,8 +218,14 @@ fn {impl Super for i32}::super_method::{vtable_method}<'_0>(@1: &'_0 ((dyn fn {impl Super for i32}::{vtable}() -> test_crate::Super::{vtable} { let ret@0: test_crate::Super::{vtable}; // return - - ret@0 := test_crate::Super::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_super_method: const ({impl Super for i32}::super_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + 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 := test_crate::Super::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_super_method: const ({impl Super for i32}::super_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)) } return } @@ -264,8 +274,14 @@ fn {impl Internal for i32}::internal_method::{vtable_method}<'_0>(@1: &'_0 ((dyn fn {impl Internal for i32}::{vtable}() -> test_crate::Internal::{vtable} { let ret@0: test_crate::Internal::{vtable}; // return - - ret@0 := test_crate::Internal::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_internal_method: const ({impl Internal for i32}::internal_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + 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 := test_crate::Internal::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_internal_method: const ({impl Internal for i32}::internal_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)) } return } @@ -315,14 +331,20 @@ fn {impl Left for i32}::left_method::{vtable_method}<'_0>(@1: &'_0 ((dyn exists< fn {impl Left for i32}::{vtable}() -> test_crate::Left::{vtable} { let ret@0: test_crate::Left::{vtable}; // return - let @1: (); // anonymous local - let @2: &'static (test_crate::Internal::{vtable}); // anonymous local + let size@1: usize; // local + let align@2: usize; // local + let @3: (); // anonymous local + let @4: &'static (test_crate::Internal::{vtable}); // anonymous local - storage_live(@1) - @1 := () - storage_live(@2) - @2 := &{impl Internal for i32}::{vtable} - ret@0 := test_crate::Left::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_left_method: const ({impl Left for i32}::left_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2) } + storage_live(size@1) + size@1 := size_of + storage_live(align@2) + align@2 := align_of + storage_live(@3) + @3 := () + storage_live(@4) + @4 := &{impl Internal for i32}::{vtable} + ret@0 := test_crate::Left::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_left_method: const ({impl Left for i32}::left_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4) } return } @@ -403,20 +425,26 @@ fn {impl Right for i32}::right_method::{vtable_method}<'_0>(@1: &'_0 ((dyn fn {impl Right for i32}::{vtable}() -> test_crate::Right::{vtable} { let ret@0: test_crate::Right::{vtable}; // return - let @1: (); // anonymous local - let @2: &'static (test_crate::Internal::{vtable}); // anonymous local + let size@1: usize; // local + let align@2: usize; // local let @3: (); // anonymous local - let @4: &'static (test_crate::Super::{vtable}); // anonymous local - - storage_live(@1) - @1 := () - storage_live(@2) - @2 := &{impl Internal for i32}::{vtable} + let @4: &'static (test_crate::Internal::{vtable}); // anonymous local + let @5: (); // anonymous local + let @6: &'static (test_crate::Super::{vtable}); // anonymous local + + storage_live(size@1) + size@1 := size_of + storage_live(align@2) + align@2 := align_of storage_live(@3) @3 := () storage_live(@4) - @4 := &{impl Super for i32}::{vtable} - ret@0 := test_crate::Right::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_right_method: const ({impl Right for i32}::right_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2), super_trait_2: move (@4) } + @4 := &{impl Internal for i32}::{vtable} + storage_live(@5) + @5 := () + storage_live(@6) + @6 := &{impl Super for i32}::{vtable} + ret@0 := test_crate::Right::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_right_method: const ({impl Right for i32}::right_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4), super_trait_2: move (@6) } return } @@ -478,20 +506,26 @@ fn {impl Join for i32}::join_method::{vtable_method}<'_0>(@1: &'_0 ((dyn ex fn {impl Join for i32}::{vtable}() -> test_crate::Join::{vtable} { let ret@0: test_crate::Join::{vtable}; // return - let @1: (); // anonymous local - let @2: &'static (test_crate::Left::{vtable}); // anonymous local + let size@1: usize; // local + let align@2: usize; // local let @3: (); // anonymous local - let @4: &'static (test_crate::Right::{vtable}); // anonymous local - - storage_live(@1) - @1 := () - storage_live(@2) - @2 := &{impl Left for i32}::{vtable} + let @4: &'static (test_crate::Left::{vtable}); // anonymous local + let @5: (); // anonymous local + let @6: &'static (test_crate::Right::{vtable}); // anonymous local + + storage_live(size@1) + size@1 := size_of + storage_live(align@2) + align@2 := align_of storage_live(@3) @3 := () storage_live(@4) - @4 := &{impl Right 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::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2), super_trait_2: move (@4) } + @4 := &{impl Left for i32}::{vtable} + storage_live(@5) + @5 := () + storage_live(@6) + @6 := &{impl Right for i32}::{vtable} + ret@0 := test_crate::Join::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_join_method: const ({impl Join for i32}::join_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4), super_trait_2: move (@6) } return } diff --git a/charon/tests/ui/unsize.out b/charon/tests/ui/unsize.out index 48adf91ff..99e6fa8e0 100644 --- a/charon/tests/ui/unsize.out +++ b/charon/tests/ui/unsize.out @@ -80,6 +80,10 @@ pub fn core::ops::drop::Drop::drop<'_0, Self>(@1: &'_0 mut (Self)) where [@TraitClause0]: Drop, +// Full name: core::ptr::drop_in_place +#[lang_item("drop_in_place")] +pub unsafe fn drop_in_place(@1: *mut T) + // Full name: alloc::alloc::Global #[lang_item("global_alloc_ty")] pub struct Global {} @@ -177,8 +181,14 @@ fn {vtable_method}<'_0, '_1, '_2>(@1: &'_0 ((dyn exists<_dyn> [@TraitClause0]: D 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 ({vtable_method}<'_, '_, '_>) } + 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::fmt::Display::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_fmt: const ({vtable_method}<'_, '_, '_>) } return } diff --git a/charon/tests/ui/vtable-simple.out b/charon/tests/ui/vtable-simple.out index 22e313b3b..ee6369a68 100644 --- a/charon/tests/ui/vtable-simple.out +++ b/charon/tests/ui/vtable-simple.out @@ -50,6 +50,10 @@ pub trait Destruct vtable: core::marker::Destruct::{vtable} } +// Full name: core::ptr::drop_in_place +#[lang_item("drop_in_place")] +pub unsafe fn drop_in_place(@1: *mut T) + fn UNIT_METADATA() { let @0: (); // return @@ -127,8 +131,14 @@ where [@TraitClause1]: Clone, { 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 ({vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: const (Opaque(missing supertrait vtable)) } + 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 := test_crate::Modifiable::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_modify: const ({vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: const (Opaque(missing supertrait vtable)) } return } diff --git a/charon/tests/ui/vtables.out b/charon/tests/ui/vtables.out index 427c992b5..993cc2203 100644 --- a/charon/tests/ui/vtables.out +++ b/charon/tests/ui/vtables.out @@ -121,6 +121,10 @@ pub enum AssertKind { Match, } +// Full name: core::ptr::drop_in_place +#[lang_item("drop_in_place")] +pub unsafe fn drop_in_place(@1: *mut T) + // Full name: alloc::string::String #[lang_item("String")] pub opaque type String @@ -273,8 +277,14 @@ fn {impl Super for i32}::super_method::{vtable_method}<'_0>(@1: &'_0 ((dyn fn {impl Super for i32}::{vtable}() -> test_crate::Super::{vtable} { let ret@0: test_crate::Super::{vtable}; // return - - ret@0 := test_crate::Super::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_super_method: const ({impl Super for i32}::super_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + 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 := test_crate::Super::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_super_method: const ({impl Super for i32}::super_method::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)) } return } @@ -324,14 +334,20 @@ fn {impl Checkable for i32}::check::{vtable_method}<'_0>(@1: &'_0 ((dyn exi fn {impl Checkable for i32}::{vtable}() -> test_crate::Checkable::{vtable} { let ret@0: test_crate::Checkable::{vtable}; // return - let @1: (); // anonymous local - let @2: &'static (test_crate::Super::{vtable}); // anonymous local + let size@1: usize; // local + let align@2: usize; // local + let @3: (); // anonymous local + let @4: &'static (test_crate::Super::{vtable}); // anonymous local - storage_live(@1) - @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::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2) } + storage_live(size@1) + size@1 := size_of + storage_live(align@2) + align@2 := align_of + storage_live(@3) + @3 := () + storage_live(@4) + @4 := &{impl Super for i32}::{vtable} + ret@0 := test_crate::Checkable::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_check: const ({impl Checkable for i32}::check::{vtable_method}<'_>), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@4) } return } @@ -491,8 +507,14 @@ where [@TraitClause1]: Clone, { 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::{vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: const (Opaque(missing supertrait vtable)) } + 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 := test_crate::Modifiable::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_modify: const ({impl Modifiable for i32}::modify::{vtable_method}<'_, '_, T>[@TraitClause0, @TraitClause1]), super_trait_0: const (Opaque(missing supertrait vtable)) } return } @@ -682,8 +704,14 @@ fn {impl BaseOn for i32}::operate_on::{vtable_method}<'_0, '_1>(@1: &'_0 (( fn {impl BaseOn for i32}::{vtable}() -> test_crate::BaseOn::{vtable} { let ret@0: test_crate::BaseOn::{vtable}; // return - - ret@0 := test_crate::BaseOn::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_operate_on: const ({impl BaseOn for i32}::operate_on::{vtable_method}<'_, '_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + 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 := test_crate::BaseOn::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_operate_on: const ({impl BaseOn for i32}::operate_on::{vtable_method}<'_, '_>), super_trait_0: const (Opaque(missing supertrait vtable)) } return } @@ -752,8 +780,14 @@ fn {impl BaseOn for i32}::operate_on::{vtable_method}<'_0, '_1>(@1: &'_0 (( fn {impl BaseOn for i32}::{vtable}() -> test_crate::BaseOn::{vtable} { let ret@0: test_crate::BaseOn::{vtable}; // return - - ret@0 := test_crate::BaseOn::{vtable} { size: const (Opaque(unknown size)), align: const (Opaque(unknown align)), drop: const (Opaque(unknown drop)), method_operate_on: const ({impl BaseOn for i32}::operate_on::{vtable_method}<'_, '_>), super_trait_0: const (Opaque(missing supertrait vtable)) } + 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 := test_crate::BaseOn::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_operate_on: const ({impl BaseOn for i32}::operate_on::{vtable_method}<'_, '_>), super_trait_0: const (Opaque(missing supertrait vtable)) } return } @@ -808,20 +842,26 @@ fn test_crate::{impl Both32And64 for i32}::both_operate<'_0, '_1, '_2>(@1: &'_0 fn {impl Both32And64 for i32}::{vtable}() -> test_crate::Both32And64::{vtable} { let ret@0: test_crate::Both32And64::{vtable}; // return - let @1: (); // anonymous local - let @2: &'static (test_crate::BaseOn::{vtable}); // anonymous local + let size@1: usize; // local + let align@2: usize; // local let @3: (); // anonymous local - let @4: &'static (test_crate::BaseOn::{vtable}); // anonymous local - - storage_live(@1) - @1 := () - storage_live(@2) - @2 := &{impl BaseOn for i32}::{vtable} + let @4: &'static (test_crate::BaseOn::{vtable}); // anonymous local + let @5: (); // anonymous local + let @6: &'static (test_crate::BaseOn::{vtable}); // anonymous local + + storage_live(size@1) + size@1 := size_of + storage_live(align@2) + align@2 := align_of storage_live(@3) @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 default methods aren't yet supported)), super_trait_0: const (Opaque(missing supertrait vtable)), super_trait_1: move (@2), super_trait_2: move (@4) } + @4 := &{impl BaseOn for i32}::{vtable} + storage_live(@5) + @5 := () + storage_live(@6) + @6 := &{impl BaseOn for i32}::{vtable} + ret@0 := test_crate::Both32And64::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), 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 (@4), super_trait_2: move (@6) } return } @@ -915,8 +955,14 @@ fn {impl LifetimeTrait for i32}::lifetime_method::{vtable_method}<'a, '_1>(@1: & 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)) } + 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 := test_crate::LifetimeTrait::{vtable} { size: move (size@1), align: move (align@2), drop: const (drop_in_place), method_lifetime_method: const ({impl LifetimeTrait for i32}::lifetime_method::{vtable_method}<'_, '_>), super_trait_0: const (Opaque(missing supertrait vtable)) } return } From 49680adcd1e72467ba766014d5fd529325c68d5a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 13 Oct 2025 15:57:46 +0200 Subject: [PATCH 4/4] Cache the hax state with added owner --- charon/src/bin/charon-driver/translate/get_mir.rs | 8 ++++---- .../bin/charon-driver/translate/translate_crate.rs | 2 +- .../src/bin/charon-driver/translate/translate_ctx.rs | 12 ++++++++---- .../charon-driver/translate/translate_predicates.rs | 2 +- .../translate/translate_trait_objects.rs | 8 ++++---- .../bin/charon-driver/translate/translate_types.rs | 4 ++-- 6 files changed, 20 insertions(+), 16 deletions(-) diff --git a/charon/src/bin/charon-driver/translate/get_mir.rs b/charon/src/bin/charon-driver/translate/get_mir.rs index b4c895caf..24ed07efe 100644 --- a/charon/src/bin/charon-driver/translate/get_mir.rs +++ b/charon/src/bin/charon-driver/translate/get_mir.rs @@ -42,17 +42,17 @@ impl ItemTransCtx<'_, '_> { let def_id = &item_ref.def_id; Ok(match get_mir_for_def_id_and_level(tcx, def_id, mir_level) { Some(body) => { - let state = self.hax_state_with_id(); + let s = self.hax_state_with_id(); let body = if self.monomorphize() { - let typing_env = state.typing_env(); - let args = item_ref.rustc_args(&state); + let typing_env = s.typing_env(); + let args = item_ref.rustc_args(s); hax::substitute(tcx, typing_env, Some(args), body) } else { body }; // Here, we have to create a MIR state, which contains the body. let body = Rc::new(body); - let state = state.with_mir(body.clone()); + let state = s.with_mir(body.clone()); // Translate let body: hax::MirBody = self.t_ctx.catch_sinto(&state, span, body.as_ref())?; diff --git a/charon/src/bin/charon-driver/translate/translate_crate.rs b/charon/src/bin/charon-driver/translate/translate_crate.rs index 5333b018b..9839a2e5b 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate.rs @@ -402,7 +402,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { kind: TransItemSourceKind, ) -> T { let item = if self.monomorphize() && item.has_param { - item.erase(&self.hax_state_with_id()) + item.erase(self.hax_state_with_id()) } else { item.clone() }; diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index f409647af..948b17abe 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -66,6 +66,8 @@ pub(crate) struct ItemTransCtx<'tcx, 'ctx> { pub item_id: Option, /// The translation context containing the top-level definitions/ids. pub t_ctx: &'ctx mut TranslateCtx<'tcx>, + /// The Hax context with the current `DefId`. + pub hax_state_with_id: hax::StateWithOwner<'tcx>, /// Whether to consider a `ImplExprAtom::Error` as an error for us. True except inside type /// aliases, because rust does not enforce correct trait bounds on type aliases. pub error_on_impl_expr_error: bool, @@ -170,10 +172,14 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { item_id: Option, t_ctx: &'ctx mut TranslateCtx<'tcx>, ) -> Self { + use hax::BaseState; + let def_id = item_src.def_id().underlying_rust_def_id(); + let hax_state_with_id = t_ctx.hax_state.clone().with_owner_id(def_id); ItemTransCtx { item_src, item_id, t_ctx, + hax_state_with_id, error_on_impl_expr_error: true, binding_levels: Default::default(), } @@ -192,10 +198,8 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { &self.t_ctx.hax_state } - pub fn hax_state_with_id(&self) -> hax::StateWithOwner<'tcx> { - use hax::BaseState; - let def_id = self.item_src.def_id().underlying_rust_def_id(); - self.t_ctx.hax_state.clone().with_owner_id(def_id) + pub fn hax_state_with_id(&self) -> &hax::StateWithOwner<'tcx> { + &self.hax_state_with_id } /// Return the definition for this item. This uses the polymorphic or monomorphic definition diff --git a/charon/src/bin/charon-driver/translate/translate_predicates.rs b/charon/src/bin/charon-driver/translate/translate_predicates.rs index 4ed136e90..653d3a518 100644 --- a/charon/src/bin/charon-driver/translate/translate_predicates.rs +++ b/charon/src/bin/charon-driver/translate/translate_predicates.rs @@ -278,7 +278,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { } => { let tref = &impl_source.r#trait; let trait_def = - self.hax_def(&tref.hax_skip_binder_ref().erase(&self.hax_state_with_id()))?; + self.hax_def(&tref.hax_skip_binder_ref().erase(self.hax_state_with_id()))?; let closure_kind = trait_def.lang_item.as_deref().and_then(|lang| match lang { "fn_once" => Some(ClosureKind::FnOnce), "fn_mut" => Some(ClosureKind::FnMut), 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 b2f50ada7..8f303cf7d 100644 --- a/charon/src/bin/charon-driver/translate/translate_trait_objects.rs +++ b/charon/src/bin/charon-driver/translate/translate_trait_objects.rs @@ -221,7 +221,7 @@ impl ItemTransCtx<'_, '_> { // The vtable type also takes associated types as parameters. let assoc_tys: Vec<_> = tref - .trait_associated_types(&self.hax_state_with_id()) + .trait_associated_types(self.hax_state_with_id()) .iter() .map(|ty| self.translate_ty(span, ty)) .try_collect()?; @@ -757,11 +757,11 @@ impl ItemTransCtx<'_, '_> { // Build a reference to `std::ptr::drop_in_place`. let drop_in_place: hax::ItemRef = { - let hax_state = self.hax_state_with_id(); + let s = self.hax_state_with_id(); let drop_in_place = self.tcx.lang_items().drop_in_place_fn().unwrap(); - let rustc_trait_args = trait_pred.trait_ref.rustc_args(&hax_state); + let rustc_trait_args = trait_pred.trait_ref.rustc_args(s); let generics = self.tcx.mk_args(&rustc_trait_args[..1]); // keep only the `Self` type - hax::ItemRef::translate(&hax_state, drop_in_place, generics) + hax::ItemRef::translate(s, drop_in_place, generics) }; let fn_ptr = self .translate_fn_ptr(span, &drop_in_place, TransItemSourceKind::Fun)? diff --git a/charon/src/bin/charon-driver/translate/translate_types.rs b/charon/src/bin/charon-driver/translate/translate_types.rs index 7cecef460..d8b8c0486 100644 --- a/charon/src/bin/charon-driver/translate/translate_types.rs +++ b/charon/src/bin/charon-driver/translate/translate_types.rs @@ -363,7 +363,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { use rustc_middle::ty; let tcx = self.t_ctx.tcx; let rdefid = item.def_id.as_rust_def_id().unwrap(); - let hax_state = &self.hax_state_with_id(); + let hax_state = &self.hax_state_with_id; let ty_env = hax_state.typing_env(); let ty = tcx .type_of(rdefid) @@ -462,7 +462,7 @@ impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> { let tcx = self.t_ctx.tcx; let rdefid = item.def_id.as_rust_def_id().unwrap(); - let hax_state = &self.hax_state_with_id(); + let hax_state = self.hax_state_with_id(); let ty_env = hax_state.typing_env(); let ty = tcx .type_of(rdefid)