charon_driver/translate/
translate_drops.rs

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

charon_driver/translate/
translate_drops.rs
