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: TraitImplSource,
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, TraitImplSource::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: AssocItemId = self
76            .translate_drop_glue_method_id(&trait_pred.trait_ref.def_id, implemented_trait.id)?
77            .into();
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            ItemSource::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            is_global_initializer: None,
117            body,
118        })
119    }
120
121    pub(crate) fn drop_glue_region(&self) -> Region {
122        Region::Var(DeBruijnVar::new_at_zero(
123            self.the_only_binder()
124                .drop_glue_region
125                .expect("drop glue item should have a borrow lifetime"),
126        ))
127    }
128
129    pub(crate) fn drop_glue_generic_args(&mut self) -> GenericArgs {
130        let mut generics = GenericArgs::empty();
131        generics.regions.push(self.translate_erased_region());
132        generics
133    }
134
135    pub(crate) fn drop_glue_params() -> GenericParams {
136        let mut params = GenericParams::empty();
137        params
138            .regions
139            .push_with(|index| RegionParam::new(index, None));
140        params
141    }
142
143    // Small helper to deduplicate. Generates the signature `&'a mut self_ty -> ()`.
144    pub fn drop_glue_method_sig(&self, self_ty: Ty, region: Region) -> FunSig {
145        let self_ref = TyKind::Ref(region, self_ty, RefKind::Mut).into_ty();
146        FunSig {
147            is_unsafe: true,
148            abi: Abi::rust(),
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            skip_binder: self.drop_glue_method_sig(self_ty, region),
161        }
162    }
163
164    #[tracing::instrument(skip(self, item_meta, def))]
165    pub fn translate_implicit_destruct_impl(
166        mut self,
167        impl_id: TraitImplId,
168        item_meta: ItemMeta,
169        def: &hax::FullDef<'tcx>,
170    ) -> Result<TraitImpl, Error> {
171        let span = item_meta.span;
172
173        let (FullDefKind::Adt { destruct_impl, .. } | FullDefKind::Closure { destruct_impl, .. }) =
174            def.kind()
175        else {
176            unreachable!("{:?}", def.def_id())
177        };
178        let mut timpl = self.translate_virtual_trait_impl(impl_id, item_meta, destruct_impl)?;
179
180        // Add the `drop_glue(&mut self)` method.
181        let destruct_trait_id = timpl.impl_trait.id;
182        let destruct_trait_def_id: &hax::DefId = &destruct_impl.trait_pred.trait_ref.def_id;
183        let method_id =
184            self.translate_drop_glue_method_id(destruct_trait_def_id, destruct_trait_id)?;
185        let method_binder = {
186            let fun_id = self.register_item(
187                span,
188                def.this(),
189                TransItemSourceKind::DropGlueMethod(TraitImplSource::ImplicitDestruct),
190            );
191            let method_params = Self::drop_glue_params();
192            let generics = self
193                .outermost_binder()
194                .params
195                .identity_args_at_depth(DeBruijnId::one())
196                .concat(&method_params.identity_args());
197            Binder::new(
198                BinderKind::TraitMethod(destruct_trait_id, method_id),
199                method_params,
200                FunDeclRef {
201                    id: fun_id,
202                    generics: Box::new(generics),
203                },
204            )
205        };
206        timpl.methods.set_slot_extend(method_id, method_binder);
207
208        Ok(timpl)
209    }
210}
charon_driver/translate/translate_drops.rs

charon_driver/translate/
translate_drops.rs
