charon_driver/translate/
translate_drops.rs

1use crate::translate::translate_crate::TransItemSourceKind;
2
3use super::translate_ctx::*;
4use charon_lib::{ast::*, formatter::IntoFormatter, pretty::FmtWithCtx};
5use hax::FullDefKind;
6
7impl ItemTransCtx<'_, '_> {
8    fn translate_drop_in_place_method_body(
9        &mut self,
10        span: Span,
11        def: &hax::FullDef,
12        self_ty: &Ty,
13    ) -> Result<Body, Error> {
14        let (hax::FullDefKind::Adt { drop_glue, .. } | hax::FullDefKind::Closure { drop_glue, .. }) =
15            def.kind()
16        else {
17            return Ok(Body::Missing);
18        };
19
20        let tmp_body;
21        let body = match drop_glue {
22            Some(body) => body,
23            None if self.options.translate_poly_drop_glue => {
24                let ctx = std::panic::AssertUnwindSafe(&mut *self);
25                // This is likely to panic, see the docs of `--precise-drops`.
26                let Ok(body) =
27                    std::panic::catch_unwind(move || def.this().drop_glue_shim(ctx.hax_state()))
28                else {
29                    let self_ty_name = if let TyKind::Adt(TypeDeclRef {
30                        id: TypeId::Adt(type_id),
31                        ..
32                    }) = self_ty.kind()
33                        && let Some(name) = self.translated.item_name(*type_id)
34                    {
35                        name.to_string_with_ctx(&self.into_fmt())
36                    } else {
37                        "crate::the::Type".to_string()
38                    };
39                    raise_error!(
40                        self,
41                        span,
42                        "rustc panicked while retrieving drop glue. \
43                        This is known to happen with `--precise-drops`; to silence this warning, \
44                        pass `--opaque '{{impl core::marker::Destruct for {}}}'` to charon",
45                        self_ty_name
46                    )
47                };
48                tmp_body = body;
49                &tmp_body
50            }
51            None => return Ok(Body::Missing),
52        };
53
54        Ok(self.translate_body(span, body, &def.source_text))
55    }
56
57    /// Translate the body of the fake `Destruct::drop_in_place` method we're adding to the
58    /// `Destruct` trait. It contains the drop glue for the type.
59    #[tracing::instrument(skip(self, item_meta))]
60    pub fn translate_drop_in_place_method(
61        mut self,
62        def_id: FunDeclId,
63        item_meta: ItemMeta,
64        def: &hax::FullDef,
65        impl_kind: Option<TraitImplSource>,
66    ) -> Result<FunDecl, Error> {
67        let span = item_meta.span;
68
69        self.translate_def_generics(span, def)?;
70
71        let trait_pred = match def.kind() {
72            // Charon-generated `Destruct` impl for an ADT.
73            FullDefKind::Adt { destruct_impl, .. } | FullDefKind::Closure { destruct_impl, .. } => {
74                assert_eq!(impl_kind, Some(TraitImplSource::ImplicitDestruct));
75                &destruct_impl.trait_pred
76            }
77            // The declaration of the method.
78            FullDefKind::Trait { self_predicate, .. } => {
79                assert_eq!(impl_kind, None);
80                self_predicate
81            }
82            _ => unreachable!(),
83        };
84
85        let implemented_trait = self.translate_trait_predicate(span, trait_pred)?;
86        let item_name = TraitItemName("drop_in_place".into());
87        let self_ty = implemented_trait
88            .self_ty(&self.t_ctx.translated)
89            .unwrap()
90            .clone();
91
92        let src = match impl_kind {
93            Some(impl_kind) => {
94                let destruct_impl_id =
95                    self.register_item(span, def.this(), TransItemSourceKind::TraitImpl(impl_kind));
96                let impl_ref = TraitImplRef {
97                    id: destruct_impl_id,
98                    generics: Box::new(self.the_only_binder().params.identity_args()),
99                };
100                ItemSource::TraitImpl {
101                    impl_ref,
102                    trait_ref: implemented_trait,
103                    item_name,
104                    reuses_default: false,
105                }
106            }
107            None => ItemSource::TraitDecl {
108                trait_ref: implemented_trait,
109                item_name,
110                has_default: false,
111            },
112        };
113
114        let body = if item_meta.opacity.with_private_contents().is_opaque() {
115            Body::Opaque
116        } else {
117            self.translate_drop_in_place_method_body(span, def, &self_ty)?
118        };
119
120        let input = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
121        let signature = FunSig {
122            generics: self.into_generics(),
123            is_unsafe: false,
124            inputs: vec![input],
125            output: Ty::mk_unit(),
126        };
127
128        Ok(FunDecl {
129            def_id,
130            item_meta,
131            signature,
132            src,
133            is_global_initializer: None,
134            body,
135        })
136    }
137
138    // Small helper to deduplicate.
139    pub fn prepare_drop_in_place_method(
140        &mut self,
141        def: &hax::FullDef,
142        span: Span,
143        destruct_trait_id: TraitDeclId,
144        impl_kind: Option<TraitImplSource>,
145    ) -> (TraitItemName, Binder<FunDeclRef>) {
146        let method_id = self.register_item(
147            span,
148            def.this(),
149            TransItemSourceKind::DropInPlaceMethod(impl_kind),
150        );
151        let method_name = TraitItemName("drop_in_place".into());
152        let method_binder = {
153            let generics = self
154                .outermost_binder()
155                .params
156                .identity_args_at_depth(DeBruijnId::one());
157            Binder::new(
158                BinderKind::TraitMethod(destruct_trait_id, method_name.clone()),
159                GenericParams::empty(),
160                FunDeclRef {
161                    id: method_id,
162                    generics: Box::new(generics),
163                },
164            )
165        };
166        (method_name, method_binder)
167    }
168
169    #[tracing::instrument(skip(self, item_meta))]
170    pub fn translate_implicit_destruct_impl(
171        mut self,
172        impl_id: TraitImplId,
173        item_meta: ItemMeta,
174        def: &hax::FullDef,
175    ) -> Result<TraitImpl, Error> {
176        let span = item_meta.span;
177
178        self.translate_def_generics(span, def)?;
179
180        let (FullDefKind::Adt { destruct_impl, .. } | FullDefKind::Closure { destruct_impl, .. }) =
181            def.kind()
182        else {
183            unreachable!("{:?}", def.def_id())
184        };
185        let mut timpl = self.translate_virtual_trait_impl(impl_id, item_meta, destruct_impl)?;
186
187        // Add the `drop_in_place(*mut self)` method.
188        timpl.methods.push(self.prepare_drop_in_place_method(
189            def,
190            span,
191            timpl.impl_trait.id,
192            Some(TraitImplSource::ImplicitDestruct),
193        ));
194
195        Ok(timpl)
196    }
197}
charon_driver/translate/translate_drops.rs

charon_driver/translate/
translate_drops.rs
