charon_driver/translate/
translate_drops.rs

1use crate::translate::{translate_bodies::BodyTransCtx, translate_crate::TransItemSourceKind};
2
3use super::translate_ctx::*;
4use charon_lib::ast::*;
5use hax_frontend_exporter::{self as hax, FullDefKind};
6
7impl ItemTransCtx<'_, '_> {
8    fn translate_drop_method_body(
9        &mut self,
10        span: Span,
11        def: &hax::FullDef,
12    ) -> Result<Result<Body, Opaque>, Error> {
13        let (hax::FullDefKind::Adt { drop_glue, .. } | hax::FullDefKind::Closure { drop_glue, .. }) =
14            def.kind()
15        else {
16            panic!("Unexpected def adt: {def:?}")
17        };
18        let Some(body) = drop_glue else {
19            return Ok(Err(Opaque));
20        };
21
22        let mut bt_ctx = BodyTransCtx::new(self);
23        Ok(match bt_ctx.translate_body(span, body, &def.source_text) {
24            Ok(Ok(body)) => Ok(body),
25            Ok(Err(Opaque)) => Err(Opaque),
26            Err(_) => Err(Opaque),
27        })
28    }
29
30    /// Given an item that is a closure, generate the `call_once`/`call_mut`/`call` method
31    /// (depending on `target_kind`).
32    #[tracing::instrument(skip(self, item_meta))]
33    pub fn translate_drop_method(
34        mut self,
35        def_id: FunDeclId,
36        item_meta: ItemMeta,
37        def: &hax::FullDef,
38    ) -> Result<FunDecl, Error> {
39        let span = item_meta.span;
40
41        self.translate_def_generics(span, def)?;
42
43        let (FullDefKind::Adt { drop_impl, .. } | FullDefKind::Closure { drop_impl, .. }) =
44            def.kind()
45        else {
46            unreachable!()
47        };
48        let implemented_trait = self.translate_trait_predicate(span, &drop_impl.trait_pred)?;
49        let self_ty = implemented_trait
50            .self_ty(&self.t_ctx.translated)
51            .unwrap()
52            .clone();
53        let drop_impl_id = self.register_item(
54            span,
55            def.this(),
56            TransItemSourceKind::TraitImpl(TraitImplSource::DropGlue),
57        );
58        let impl_ref = TraitImplRef {
59            id: drop_impl_id,
60            generics: Box::new(self.the_only_binder().params.identity_args()),
61        };
62
63        let kind = ItemKind::TraitImpl {
64            impl_ref,
65            trait_ref: implemented_trait,
66            item_name: TraitItemName("drop".to_owned()),
67            reuses_default: false,
68        };
69
70        // Add the method lifetime generic.
71        assert!(self.innermost_binder_mut().bound_region_vars.is_empty());
72        let region_id = self
73            .innermost_binder_mut()
74            .push_bound_region(hax::BoundRegionKind::Anon);
75
76        let body = if item_meta.opacity.with_private_contents().is_opaque() {
77            Err(Opaque)
78        } else {
79            self.translate_drop_method_body(span, def)?
80        };
81
82        let input = TyKind::Ref(
83            Region::Var(DeBruijnVar::new_at_zero(region_id)),
84            self_ty,
85            RefKind::Mut,
86        )
87        .into_ty();
88        let signature = FunSig {
89            generics: self.into_generics(),
90            is_unsafe: false,
91            inputs: vec![input],
92            output: Ty::mk_unit(),
93        };
94
95        Ok(FunDecl {
96            def_id,
97            item_meta,
98            signature,
99            kind,
100            is_global_initializer: None,
101            body,
102        })
103    }
104
105    #[tracing::instrument(skip(self, item_meta))]
106    pub fn translate_drop_impl(
107        mut self,
108        impl_id: TraitImplId,
109        item_meta: ItemMeta,
110        def: &hax::FullDef,
111    ) -> Result<TraitImpl, Error> {
112        let span = item_meta.span;
113
114        self.translate_def_generics(span, def)?;
115
116        let (FullDefKind::Adt { drop_impl, .. } | FullDefKind::Closure { drop_impl, .. }) =
117            def.kind()
118        else {
119            unreachable!()
120        };
121        let mut timpl = self.translate_virtual_trait_impl(impl_id, item_meta, drop_impl)?;
122
123        // Construct the method reference.
124        let method_id = self.register_item(span, def.this(), TransItemSourceKind::DropGlueMethod);
125        let method_name = TraitItemName("drop".to_owned());
126        let method_binder = {
127            let mut method_params = GenericParams::empty();
128            method_params
129                .regions
130                .push_with(|index| RegionVar { index, name: None });
131
132            let generics = self
133                .outermost_binder()
134                .params
135                .identity_args_at_depth(DeBruijnId::one())
136                .concat(&method_params.identity_args_at_depth(DeBruijnId::zero()));
137            Binder::new(
138                BinderKind::TraitMethod(timpl.impl_trait.id, method_name.clone()),
139                method_params,
140                FunDeclRef {
141                    id: method_id,
142                    generics: Box::new(generics),
143                },
144            )
145        };
146        timpl.methods.push((method_name, method_binder));
147
148        Ok(timpl)
149    }
150}
charon_driver/translate/translate_drops.rs

charon_driver/translate/
translate_drops.rs
