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

charon_driver/translate/
translate_drops.rs
