charon_driver/translate/
translate_drops.rs

1use crate::translate::{translate_bodies::BodyTransCtx, translate_crate::TransItemSourceKind};
2
3use super::translate_ctx::*;
4use charon_lib::ast::{ullbc_ast_utils::BodyBuilder, *};
5use hax::FullDefKind;
6
7impl ItemTransCtx<'_, '_> {
8    /// Translate the body of the fake `Drop::drop_in_place` method we're adding to the `Drop`
9    /// trait. It contains the drop glue for the type.
10    #[tracing::instrument(skip(self, item_meta))]
11    pub fn translate_empty_drop_method(
12        mut self,
13        def_id: FunDeclId,
14        item_meta: ItemMeta,
15        def: &hax::FullDef,
16    ) -> Result<FunDecl, Error> {
17        let span = item_meta.span;
18
19        self.translate_def_generics(span, def)?;
20
21        let (FullDefKind::Adt { drop_impl, .. } | FullDefKind::Closure { drop_impl, .. }) =
22            def.kind()
23        else {
24            unreachable!()
25        };
26        let implemented_trait = self.translate_trait_predicate(span, &drop_impl.trait_pred)?;
27        let self_ty = implemented_trait
28            .self_ty(&self.t_ctx.translated)
29            .unwrap()
30            .clone();
31        let drop_impl_id = self.register_item(
32            span,
33            def.this(),
34            TransItemSourceKind::TraitImpl(TraitImplSource::ImplicitDrop),
35        );
36        let impl_ref = TraitImplRef {
37            id: drop_impl_id,
38            generics: Box::new(self.the_only_binder().params.identity_args()),
39        };
40
41        let src = ItemSource::TraitImpl {
42            impl_ref,
43            trait_ref: implemented_trait,
44            item_name: TraitItemName("drop".to_owned()),
45            reuses_default: false,
46        };
47
48        // Add the method lifetime generic.
49        assert!(self.innermost_binder_mut().bound_region_vars.is_empty());
50        let region_id = self
51            .innermost_binder_mut()
52            .push_bound_region(hax::BoundRegionKind::Anon);
53
54        let input = TyKind::Ref(
55            Region::Var(DeBruijnVar::new_at_zero(region_id)),
56            self_ty,
57            RefKind::Mut,
58        )
59        .into_ty();
60        let signature = FunSig {
61            generics: self.into_generics(),
62            is_unsafe: false,
63            inputs: vec![input.clone()],
64            output: Ty::mk_unit(),
65        };
66
67        let body = if item_meta.opacity.with_private_contents().is_opaque() {
68            Err(Opaque)
69        } else {
70            let mut builder = BodyBuilder::new(span, 1);
71            let _ret = builder.new_var(None, Ty::mk_unit());
72            let _self = builder.new_var(None, input);
73            Ok(Body::Unstructured(builder.build()))
74        };
75
76        Ok(FunDecl {
77            def_id,
78            item_meta,
79            signature,
80            src,
81            is_global_initializer: None,
82            body,
83        })
84    }
85
86    fn translate_drop_in_place_method_body(
87        &mut self,
88        span: Span,
89        def: &hax::FullDef,
90    ) -> Result<Result<Body, Opaque>, Error> {
91        let def = if let hax::FullDefKind::TraitImpl { trait_pred, .. } = def.kind()
92            && let [hax::GenericArg::Type(self_ty)] = trait_pred.trait_ref.generic_args.as_slice()
93            && let hax::TyKind::Adt(item) = self_ty.kind()
94        {
95            // `def` is a manual `impl Drop for Foo`. The requirements for such an impl are
96            // stringent (https://doc.rust-lang.org/stable/error_codes/E0367.html); in particular
97            // the impl generics must match the type generics exactly. Hence we can use the adt def
98            // instead of the impl def, which would normally mess up generics.
99            &self.hax_def(item)?
100        } else {
101            def
102        };
103
104        let (hax::FullDefKind::Adt { drop_glue, .. } | hax::FullDefKind::Closure { drop_glue, .. }) =
105            def.kind()
106        else {
107            return Ok(Err(Opaque));
108        };
109        let Some(body) = drop_glue else {
110            return Ok(Err(Opaque));
111        };
112
113        let mut bt_ctx = BodyTransCtx::new(self);
114        Ok(match bt_ctx.translate_body(span, body, &def.source_text) {
115            Ok(Ok(body)) => Ok(body),
116            Ok(Err(Opaque)) => Err(Opaque),
117            Err(_) => Err(Opaque),
118        })
119    }
120
121    /// Translate the body of the fake `Drop::drop_in_place` method we're adding to the `Drop`
122    /// trait. It contains the drop glue for the type.
123    #[tracing::instrument(skip(self, item_meta))]
124    pub fn translate_drop_in_place_method(
125        mut self,
126        def_id: FunDeclId,
127        item_meta: ItemMeta,
128        def: &hax::FullDef,
129        impl_kind: Option<TraitImplSource>,
130    ) -> Result<FunDecl, Error> {
131        let span = item_meta.span;
132
133        self.translate_def_generics(span, def)?;
134
135        let trait_pred = match def.kind() {
136            // Normal `impl Drop for ...`.
137            FullDefKind::TraitImpl { trait_pred, .. } => {
138                assert_eq!(impl_kind, Some(TraitImplSource::Normal));
139                trait_pred
140            }
141            // Charon-generated `Drop` impl for an ADT.
142            FullDefKind::Adt { drop_impl, .. } | FullDefKind::Closure { drop_impl, .. } => {
143                assert_eq!(impl_kind, Some(TraitImplSource::ImplicitDrop));
144                &drop_impl.trait_pred
145            }
146            FullDefKind::Trait { self_predicate, .. } => {
147                assert_eq!(impl_kind, None);
148                self_predicate
149            }
150            _ => unreachable!(),
151        };
152
153        let implemented_trait = self.translate_trait_predicate(span, trait_pred)?;
154        let item_name = TraitItemName("drop".to_owned());
155        let self_ty = implemented_trait
156            .self_ty(&self.t_ctx.translated)
157            .unwrap()
158            .clone();
159
160        let src = match impl_kind {
161            Some(impl_kind) => {
162                let drop_impl_id =
163                    self.register_item(span, def.this(), TransItemSourceKind::TraitImpl(impl_kind));
164                let impl_ref = TraitImplRef {
165                    id: drop_impl_id,
166                    generics: Box::new(self.the_only_binder().params.identity_args()),
167                };
168                ItemSource::TraitImpl {
169                    impl_ref,
170                    trait_ref: implemented_trait,
171                    item_name,
172                    reuses_default: false,
173                }
174            }
175            None => ItemSource::TraitDecl {
176                trait_ref: implemented_trait,
177                item_name,
178                has_default: false,
179            },
180        };
181
182        let body = if item_meta.opacity.with_private_contents().is_opaque() {
183            Err(Opaque)
184        } else {
185            self.translate_drop_in_place_method_body(span, def)?
186        };
187
188        let input = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
189        let signature = FunSig {
190            generics: self.into_generics(),
191            is_unsafe: false,
192            inputs: vec![input],
193            output: Ty::mk_unit(),
194        };
195
196        Ok(FunDecl {
197            def_id,
198            item_meta,
199            signature,
200            src,
201            is_global_initializer: None,
202            body,
203        })
204    }
205
206    // Small helper to deduplicate.
207    pub fn prepare_drop_in_trait_method(
208        &mut self,
209        def: &hax::FullDef,
210        span: Span,
211        drop_trait_id: TraitDeclId,
212        impl_kind: Option<TraitImplSource>,
213    ) -> (TraitItemName, Binder<FunDeclRef>) {
214        let method_id = self.register_item(
215            span,
216            def.this(),
217            TransItemSourceKind::DropInPlaceMethod(impl_kind),
218        );
219        let method_name = TraitItemName("drop_in_place".to_owned());
220        let method_binder = {
221            let generics = self
222                .outermost_binder()
223                .params
224                .identity_args_at_depth(DeBruijnId::one());
225            Binder::new(
226                BinderKind::TraitMethod(drop_trait_id, method_name.clone()),
227                GenericParams::empty(),
228                FunDeclRef {
229                    id: method_id,
230                    generics: Box::new(generics),
231                },
232            )
233        };
234        (method_name, method_binder)
235    }
236
237    #[tracing::instrument(skip(self, item_meta))]
238    pub fn translate_implicit_drop_impl(
239        mut self,
240        impl_id: TraitImplId,
241        item_meta: ItemMeta,
242        def: &hax::FullDef,
243    ) -> Result<TraitImpl, Error> {
244        let span = item_meta.span;
245
246        self.translate_def_generics(span, def)?;
247
248        let (FullDefKind::Adt { drop_impl, .. } | FullDefKind::Closure { drop_impl, .. }) =
249            def.kind()
250        else {
251            unreachable!("{:?}", def.def_id())
252        };
253        let mut timpl = self.translate_virtual_trait_impl(impl_id, item_meta, drop_impl)?;
254
255        // Add the `drop(&mut self)` method.
256        let drop_method_id =
257            self.register_item(span, def.this(), TransItemSourceKind::EmptyDropMethod);
258        let drop_method_name = TraitItemName("drop".to_owned());
259        let drop_method_binder = {
260            let mut method_params = GenericParams::empty();
261            method_params
262                .regions
263                .push_with(|index| RegionParam { index, name: None });
264
265            let generics = self
266                .outermost_binder()
267                .params
268                .identity_args_at_depth(DeBruijnId::one())
269                .concat(&method_params.identity_args_at_depth(DeBruijnId::zero()));
270            Binder::new(
271                BinderKind::TraitMethod(timpl.impl_trait.id, drop_method_name.clone()),
272                method_params,
273                FunDeclRef {
274                    id: drop_method_id,
275                    generics: Box::new(generics),
276                },
277            )
278        };
279        timpl.methods.push((drop_method_name, drop_method_binder));
280
281        // Add the `drop_in_place(*mut self)` method.
282        timpl.methods.push(self.prepare_drop_in_trait_method(
283            def,
284            span,
285            timpl.impl_trait.id,
286            Some(TraitImplSource::ImplicitDrop),
287        ));
288
289        Ok(timpl)
290    }
291}
charon_driver/translate/translate_drops.rs

charon_driver/translate/
translate_drops.rs
