charon_driver/translate/
translate_drops.rs

1use rustc_middle::ty;
2
3use super::translate_ctx::*;
4use crate::hax;
5use crate::hax::FullDefKind;
6use crate::translate::translate_crate::TransItemSourceKind;
7use charon_lib::ast::*;
8
9impl<'tcx> ItemTransCtx<'tcx, '_> {
10    pub fn translate_drop_glue_method_id(
11        &mut self,
12        destruct_trait_def_id: &hax::DefId,
13        destruct_trait_id: TraitDeclId,
14    ) -> Result<TraitMethodId, Error> {
15        self.register_assoc_items(destruct_trait_def_id, destruct_trait_id)?;
16        let method_id = TraitMethodId::ZERO; // It's the only method
17        Ok(method_id)
18    }
19
20    /// Translate a call to `drop_glue` for that type.
21    pub fn translate_drop_glue_method_call(
22        &mut self,
23        span: Span,
24        ty: ty::Ty<'tcx>,
25    ) -> Result<FnPtr, Error> {
26        let trait_proof = hax::solve_destruct(self.hax_state_with_id(), ty);
27        let tref = self
28            .translate_trait_proof(span, &trait_proof)?
29            .no_bound_vars();
30        let method_id = self.translate_drop_glue_method_id(
31            &trait_proof.pred.hax_skip_binder_ref().def_id,
32            tref.trait_id(),
33        )?;
34        let fn_ptr = FnPtr::new(
35            FnPtrKind::Trait(tref, method_id),
36            self.drop_glue_generic_args(),
37        );
38        Ok(fn_ptr)
39    }
40
41    fn translate_drop_glue_method_body(
42        &mut self,
43        span: Span,
44        def: &hax::FullDef<'tcx>,
45    ) -> Result<Body, Error> {
46        let (hax::FullDefKind::Adt(_) | hax::FullDefKind::Closure(_)) = def.kind() else {
47            return Ok(Body::Missing);
48        };
49
50        let body = def.this().drop_glue_shim(self.hax_state());
51        Ok(self.translate_body(span, body, &def.source_text))
52    }
53
54    /// Translate the body of the fake `Destruct::drop_glue` method we're adding to the
55    /// `Destruct` trait. It contains the drop glue for the type.
56    #[tracing::instrument(skip(self, item_meta, def))]
57    pub fn translate_drop_glue_method(
58        mut self,
59        def_id: FunDeclId,
60        item_meta: ItemMeta,
61        def: &hax::FullDef<'tcx>,
62        impl_kind: TransImplSource,
63    ) -> Result<FunDecl, Error> {
64        let span = item_meta.span;
65        let borrow_region = self.drop_glue_region();
66
67        // Charon-generated `Destruct` impl for an ADT.
68        assert_eq!(impl_kind, TransImplSource::ImplicitDestruct);
69        let trait_pred = match def.kind() {
70            FullDefKind::Adt(adt) => &adt.destruct_impl(self.hax_state()).trait_pred,
71            FullDefKind::Closure(c) => &c.destruct_impl(self.hax_state()).trait_pred,
72            _ => unreachable!(),
73        };
74
75        let implemented_trait = self.translate_trait_predicate(span, trait_pred)?;
76        let item_id =
77            self.translate_drop_glue_method_id(&trait_pred.trait_ref.def_id, implemented_trait.id)?;
78        let self_ty = implemented_trait
79            .self_ty(&self.t_ctx.translated)
80            .unwrap()
81            .clone();
82
83        let signature = self.drop_glue_method_sig(self_ty.clone(), borrow_region);
84        let src = {
85            let mut impl_generics = self.the_only_binder().params.identity_args();
86            impl_generics
87                .regions
88                .pop()
89                .expect("drop glue method should have a borrow lifetime");
90            let destruct_impl_id =
91                self.register_item(span, def.this(), TransItemSourceKind::TraitImpl(impl_kind));
92            let impl_ref = TraitImplRef {
93                id: destruct_impl_id,
94                generics: Box::new(impl_generics),
95            };
96            FunSource::TraitImpl {
97                impl_ref,
98                trait_ref: implemented_trait,
99                item_id,
100                reuses_default: false,
101            }
102        };
103
104        let body = if item_meta.opacity.with_private_contents().is_opaque() {
105            Body::Opaque
106        } else {
107            self.translate_drop_glue_method_body(span, def)?
108        };
109
110        Ok(FunDecl {
111            def_id,
112            item_meta,
113            generics: self.into_generics(),
114            signature: Box::new(signature),
115            src,
116            body,
117        })
118    }
119
120    pub(crate) fn drop_glue_region(&self) -> Region {
121        Region::Var(DeBruijnVar::new_at_zero(
122            self.the_only_binder()
123                .drop_glue_region
124                .expect("drop glue item should have a borrow lifetime"),
125        ))
126    }
127
128    pub(crate) fn drop_glue_generic_args(&mut self) -> GenericArgs {
129        let mut generics = GenericArgs::empty();
130        generics.regions.push(self.translate_erased_region());
131        generics
132    }
133
134    pub(crate) fn drop_glue_params() -> GenericParams {
135        let mut params = GenericParams::empty();
136        params
137            .regions
138            .push_with(|index| RegionParam::new(index, None, Variance::Covariant));
139        params
140    }
141
142    // Small helper to deduplicate. Generates the signature `&'a mut self_ty -> ()`.
143    pub fn drop_glue_method_sig(&self, self_ty: Ty, region: Region) -> FunSig {
144        let self_ref = TyKind::Ref(region, self_ty, RefKind::Mut).into_ty();
145        FunSig {
146            is_unsafe: true,
147            abi: Abi::rust(),
148            is_variadic: false,
149            inputs: [self_ref].into(),
150            output: Ty::mk_unit(),
151        }
152    }
153
154    pub fn drop_glue_fn_ptr_sig(&self, self_ty: Ty) -> RegionBinder<FunSig> {
155        let params = Self::drop_glue_params();
156        let region = Region::Var(DeBruijnVar::new_at_zero(RegionId::ZERO));
157        let self_ty = self_ty.move_under_binder();
158        RegionBinder {
159            regions: params.regions,
160            outlives: params.outlives,
161            skip_binder: self.drop_glue_method_sig(self_ty, region),
162        }
163    }
164
165    #[tracing::instrument(skip(self, item_meta, def))]
166    pub fn translate_implicit_destruct_impl(
167        mut self,
168        impl_id: TraitImplId,
169        item_meta: ItemMeta,
170        def: &hax::FullDef<'tcx>,
171    ) -> Result<TraitImpl, Error> {
172        let span = item_meta.span;
173
174        let destruct_impl = match def.kind() {
175            FullDefKind::Adt(adt) => adt.destruct_impl(self.hax_state()),
176            FullDefKind::Closure(c) => c.destruct_impl(self.hax_state()),
177            _ => unreachable!("{:?}", def.def_id()),
178        };
179        let mut timpl = self.translate_virtual_trait_impl(
180            impl_id,
181            item_meta,
182            def.this(),
183            TransImplSource::ImplicitDestruct,
184            destruct_impl,
185        )?;
186
187        // Add the `drop_glue(&mut self)` method.
188        let destruct_trait_id = timpl.impl_trait.id;
189        let destruct_trait_def_id: &hax::DefId = &destruct_impl.trait_pred.trait_ref.def_id;
190        let method_id =
191            self.translate_drop_glue_method_id(destruct_trait_def_id, destruct_trait_id)?;
192        let method_binder = {
193            let fun_id = self.register_item(
194                span,
195                def.this(),
196                TransItemSourceKind::DropGlueMethod(TransImplSource::ImplicitDestruct),
197            );
198            let method_params = Self::drop_glue_params();
199            let generics = self
200                .outermost_binder()
201                .params
202                .identity_args_at_depth(DeBruijnId::one())
203                .concat(&method_params.identity_args());
204            Binder::new(
205                BinderKind::TraitMethod(destruct_trait_id, method_id),
206                method_params,
207                FunDeclRef {
208                    id: fun_id,
209                    generics: Box::new(generics),
210                },
211            )
212        };
213        timpl.methods.set_slot_extend(method_id, method_binder);
214
215        Ok(timpl)
216    }
217}
charon_driver/translate/translate_drops.rs

charon_driver/translate/
translate_drops.rs
