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        let trait_pred = match def.kind() {
70            // Charon-generated `Destruct` impl for an ADT.
71            FullDefKind::Adt { destruct_impl, .. } | FullDefKind::Closure { destruct_impl, .. } => {
72                assert_eq!(impl_kind, Some(TraitImplSource::ImplicitDestruct));
73                &destruct_impl.trait_pred
74            }
75            // The declaration of the method.
76            FullDefKind::Trait { self_predicate, .. } => {
77                assert_eq!(impl_kind, None);
78                self_predicate
79            }
80            _ => unreachable!(),
81        };
82
83        let implemented_trait = self.translate_trait_predicate(span, trait_pred)?;
84        let item_name = TraitItemName("drop_in_place".into());
85        let self_ty = implemented_trait
86            .self_ty(&self.t_ctx.translated)
87            .unwrap()
88            .clone();
89
90        let src = match impl_kind {
91            Some(impl_kind) => {
92                let destruct_impl_id =
93                    self.register_item(span, def.this(), TransItemSourceKind::TraitImpl(impl_kind));
94                let impl_ref = TraitImplRef {
95                    id: destruct_impl_id,
96                    generics: Box::new(self.the_only_binder().params.identity_args()),
97                };
98                ItemSource::TraitImpl {
99                    impl_ref,
100                    trait_ref: implemented_trait,
101                    item_name,
102                    reuses_default: false,
103                }
104            }
105            None => ItemSource::TraitDecl {
106                trait_ref: implemented_trait,
107                item_name,
108                has_default: false,
109            },
110        };
111
112        let body = if item_meta.opacity.with_private_contents().is_opaque() {
113            Body::Opaque
114        } else {
115            self.translate_drop_in_place_method_body(span, def, &self_ty)?
116        };
117
118        let input = TyKind::RawPtr(self_ty, RefKind::Mut).into_ty();
119        let signature = FunSig {
120            is_unsafe: true,
121            inputs: vec![input],
122            output: Ty::mk_unit(),
123        };
124
125        Ok(FunDecl {
126            def_id,
127            item_meta,
128            generics: self.into_generics(),
129            signature,
130            src,
131            is_global_initializer: None,
132            body,
133        })
134    }
135
136    // Small helper to deduplicate.
137    pub fn prepare_drop_in_place_method(
138        &mut self,
139        def: &hax::FullDef,
140        span: Span,
141        destruct_trait_id: TraitDeclId,
142        impl_kind: Option<TraitImplSource>,
143    ) -> (TraitItemName, Binder<FunDeclRef>) {
144        let method_id = self.register_item(
145            span,
146            def.this(),
147            TransItemSourceKind::DropInPlaceMethod(impl_kind),
148        );
149        let method_name = TraitItemName("drop_in_place".into());
150        let method_binder = {
151            let generics = self
152                .outermost_binder()
153                .params
154                .identity_args_at_depth(DeBruijnId::one());
155            Binder::new(
156                BinderKind::TraitMethod(destruct_trait_id, method_name.clone()),
157                GenericParams::empty(),
158                FunDeclRef {
159                    id: method_id,
160                    generics: Box::new(generics),
161                },
162            )
163        };
164        (method_name, method_binder)
165    }
166
167    #[tracing::instrument(skip(self, item_meta))]
168    pub fn translate_implicit_destruct_impl(
169        mut self,
170        impl_id: TraitImplId,
171        item_meta: ItemMeta,
172        def: &hax::FullDef,
173    ) -> Result<TraitImpl, Error> {
174        let span = item_meta.span;
175
176        let (FullDefKind::Adt { destruct_impl, .. } | FullDefKind::Closure { destruct_impl, .. }) =
177            def.kind()
178        else {
179            unreachable!("{:?}", def.def_id())
180        };
181        let mut timpl = self.translate_virtual_trait_impl(impl_id, item_meta, destruct_impl)?;
182
183        // Add the `drop_in_place(*mut self)` method.
184        timpl.methods.push(self.prepare_drop_in_place_method(
185            def,
186            span,
187            timpl.impl_trait.id,
188            Some(TraitImplSource::ImplicitDestruct),
189        ));
190
191        Ok(timpl)
192    }
193}
charon_driver/translate/translate_drops.rs

charon_driver/translate/
translate_drops.rs
