charon_driver/translate/
translate_drops.rs

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

charon_driver/translate/
translate_drops.rs
