charon_lib/transform/normalize/
transform_dyn_trait_calls.rs1use super::super::ctx::UllbcPass;
20use crate::{
21 errors::Error,
22 formatter::IntoFormatter,
23 pretty::FmtWithCtx,
24 raise_error, register_error,
25 transform::{
26 TransformCtx,
27 ctx::{BodyTransformCtx, UllbcStatementTransformCtx},
28 },
29 ullbc_ast::*,
30};
31
32fn transform_dyn_trait_call(
34 ctx: &mut UllbcStatementTransformCtx<'_>,
35 call: &mut Call,
36) -> Result<(), Error> {
37 let fmt_ctx = &ctx.ctx.into_fmt();
38
39 let FnOperand::Regular(fn_ptr) = &call.func else {
41 return Ok(()); };
43 let FnPtrKind::Trait(trait_ref, method_id) = fn_ptr.kind.as_ref() else {
44 return Ok(()); };
46 let mut dyn_proof = trait_ref;
47 let mut supertrait_path = vec![];
48 while let TraitRefKind::ParentClause(parent, clause_id, _) = &dyn_proof.kind {
49 supertrait_path.push(*clause_id);
50 dyn_proof = parent;
51 }
52 let TraitRefKind::Dyn = &dyn_proof.kind else {
53 return Ok(()); };
55 supertrait_path.reverse();
56
57 let is_drop_glue = ctx
60 .ctx
61 .translated
62 .trait_decls
63 .get(trait_ref.trait_id())
64 .and_then(|decl| decl.item_meta.lang_item.as_ref())
65 == Some(&from_rustc::LangItem::Destruct);
66
67 let vtable_tref = if is_drop_glue {
68 supertrait_path.clear(); dyn_proof
70 } else {
71 trait_ref
72 };
73
74 let vtable_decl_ref: TypeDeclRef = {
76 let Some(trait_decl) = ctx.ctx.translated.trait_decls.get(vtable_tref.trait_id()) else {
78 return Ok(()); };
80 let Some(vtable_ty) = &trait_decl.vtable else {
82 raise_error!(
83 ctx.ctx,
84 ctx.span,
85 "Found a `dyn Trait` method call for non-dyn-compatible trait `{}`!",
86 vtable_tref.trait_id().with_ctx(fmt_ctx)
87 );
88 };
89 vtable_ty.clone().substitute_with_tref(vtable_tref)
90 };
91
92 let Some(vtable_decl) = ctx.ctx.translated.type_decls.get(vtable_decl_ref.id) else {
93 return Ok(()); };
95
96 let TypeDeclKind::Struct(fields) = &vtable_decl.kind else {
97 return Ok(()); };
99 let TypeSource::VTable { field_map, .. } = &vtable_decl.src else {
100 return Ok(()); };
102 let Some((method_field_id, target_field)) =
104 field_map.iter_enumerated().find(|(_, field)| match field {
105 VTableField::Drop => is_drop_glue,
106 VTableField::Method(id, _) => !is_drop_glue && id == method_id,
107 _ => false,
108 })
109 else {
110 let vtable_name = vtable_decl_ref.id.with_ctx(fmt_ctx).to_string();
111 raise_error!(
112 ctx.ctx,
113 ctx.span,
114 "Could not determine method index for method {} in vtable {}",
115 method_id,
116 vtable_name
117 );
118 };
119
120 let receiver_path = match target_field {
121 VTableField::Method(_, path) => path.clone(),
122 _ => vec![],
123 };
124
125 let method_field = &fields[method_field_id];
126 let method_ty = method_field
127 .ty
128 .clone()
129 .substitute(&vtable_decl_ref.generics);
130
131 if call.args.is_empty() {
133 raise_error!(ctx.ctx, ctx.span, "Dyn trait call has no arguments!");
134 }
135 let mut dyn_trait_place = match &call.args[0] {
136 Operand::Copy(place) | Operand::Move(place) => place.clone(),
137 Operand::Const(_) => {
138 panic!("Unexpected constant as receiver for dyn trait method call")
139 }
140 };
141
142 if let TyKind::DynTrait(..) = dyn_trait_place.ty().kind()
147 && let PlaceKind::Local(local) = dyn_trait_place.kind
148 && let Some(last) = ctx.statements.last()
149 && let StatementKind::Assign(dest, Rvalue::Use(src, _)) = &last.kind
150 && let Operand::Copy(place) | Operand::Move(place) = src
151 && dest.local_id() == Some(local)
152 {
153 call.args[0] = src.clone();
154 dyn_trait_place = place.clone();
155 ctx.statements.pop();
156 }
157
158 if let TyKind::DynTrait(..) = dyn_trait_place.ty().kind() {
162 let ptr_ty = TyKind::RawPtr(dyn_trait_place.ty().clone(), RefKind::Mut).into_ty();
163 let rvalue = ctx.raw_borrow(dyn_trait_place, RefKind::Mut);
164 dyn_trait_place = ctx.fresh_var(None, ptr_ty);
165 ctx.insert_assn_stmt(dyn_trait_place.clone(), rvalue);
166 call.args[0] = Operand::Move(dyn_trait_place.clone());
167 }
168
169 let dyn_pred = dyn_proof.trait_decl_ref.clone();
170 let dyn_ty = &dyn_pred.generics.types[0];
171 let PtrMetadata::VTable(receiver_vtable_ref) = dyn_ty.get_ptr_metadata(&ctx.ctx.translated)
172 else {
173 raise_error!(
174 ctx.ctx,
175 ctx.span,
176 "Dyn trait receiver does not have vtable metadata"
177 );
178 };
179
180 let receiver_vtable_ty = TyKind::Adt(receiver_vtable_ref).into_ty();
181 let ptr_to_vtable_ty = Ty::new(TyKind::RawPtr(receiver_vtable_ty.clone(), RefKind::Shared));
182 let Some(receiver_ptr) = receiver_path.iter().try_fold(dyn_trait_place, |p, field| {
183 p.project_auto_ty(&ctx.ctx.translated, ProjectionElem::Field(None, *field))
184 }) else {
185 raise_error!(ctx.ctx, ctx.span, "Could not project into dyn receiver");
186 };
187 let mut method_vtable_place = receiver_ptr
188 .project(ProjectionElem::PtrMetadata, ptr_to_vtable_ty)
189 .project(ProjectionElem::Deref, receiver_vtable_ty);
190
191 for clause_id in supertrait_path {
192 let current_vtable_ref = method_vtable_place
193 .ty()
194 .as_adt()
195 .expect("vtable place should have an ADT type");
196 let current_vtable = ctx
197 .ctx
198 .translated
199 .type_decls
200 .get(current_vtable_ref.id)
201 .expect("vtable declaration should have been translated");
202 let TypeDeclKind::Struct(fields) = ¤t_vtable.kind else {
203 panic!("vtable declaration should be a struct")
204 };
205 let TypeSource::VTable { supertrait_map, .. } = ¤t_vtable.src else {
206 panic!("vtable declaration should have a vtable source")
207 };
208 let Some(supertrait_field_id) = supertrait_map[clause_id] else {
209 raise_error!(
210 ctx.ctx,
211 ctx.span,
212 "Dyn trait proof uses a parent clause without a vtable"
213 );
214 };
215 let field_ty = fields[supertrait_field_id]
216 .ty
217 .clone()
218 .substitute(¤t_vtable_ref.generics);
219 method_vtable_place = method_vtable_place
220 .project(ProjectionElem::Field(None, supertrait_field_id), field_ty)
221 .deref();
222 }
223 let method_field_place =
224 method_vtable_place.project(ProjectionElem::Field(None, method_field_id), method_ty);
225
226 let fn_ptr_place = if ctx.ctx.options.monomorphize_with_hax {
227 let is_unsafe = is_drop_glue || call.safety.is_unsafe();
230 call.safety = if is_drop_glue {
231 CallSafety::Safe
232 } else {
233 CallSafety::Inherit
234 };
235 let real_sig_ty = TyKind::FnPtr(RegionBinder::empty(FunSig {
236 is_unsafe,
237 abi: Abi::rust(),
238 is_variadic: false,
239 inputs: call.args.iter().map(|op| op.ty().clone()).collect(),
240 output: call.dest.ty.clone(),
241 }))
242 .into_ty();
243 let fn_ptr_place = ctx.fresh_var(None, real_sig_ty);
244 let rval_cast = Rvalue::UnaryOp(
245 UnOp::Cast(CastKind::RawPtr(fn_ptr_place.ty().clone())),
246 Operand::Copy(method_field_place),
247 );
248 ctx.insert_assn_stmt(fn_ptr_place.clone(), rval_cast);
249 fn_ptr_place
250 } else {
251 method_field_place
252 };
253
254 let TyKind::FnPtr(sig) = fn_ptr_place.ty().kind() else {
256 unreachable!("vtable method is not a function pointer")
257 };
258 let method_region_count = sig.regions.len();
259 let regions: RegionArgs = fn_ptr
260 .generics
261 .regions
262 .iter()
263 .rev()
264 .take(method_region_count)
265 .rev()
266 .copied()
267 .collect();
268
269 call.func = FnOperand::Dynamic(Operand::Copy(fn_ptr_place), regions);
271
272 Ok(())
273}
274
275pub struct Transform;
276impl UllbcPass for Transform {
277 fn transform_function(&self, ctx: &mut TransformCtx, decl: &mut FunDecl) {
278 decl.transform_ullbc_terminators(ctx, |ctx, term| {
279 if let TerminatorKind::Call { call, .. } = &mut term.kind {
280 let _ = transform_dyn_trait_call(ctx, call);
281 }
282 });
283 }
284}