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

charon_driver/translate/
translate_drops.rs
