charon_driver/translate/
translate_drops.rs

1use crate::translate::translate_bodies::BodyTransCtx;
2
3use super::translate_ctx::*;
4use charon_lib::ast::*;
5use hax_frontend_exporter as hax;
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::Struct { drop_glue, .. }
14        | hax::FullDefKind::Enum { drop_glue, .. }
15        | hax::FullDefKind::Union { drop_glue, .. }
16        | hax::FullDefKind::Closure { drop_glue, .. }) = def.kind()
17        else {
18            panic!("Unexpected def adt: {def:?}")
19        };
20        let Some(body) = drop_glue else {
21            return Ok(Err(Opaque));
22        };
23
24        let mut bt_ctx = BodyTransCtx::new(self);
25        Ok(match bt_ctx.translate_body(span, body, &def.source_text) {
26            Ok(Ok(body)) => Ok(body),
27            Ok(Err(Opaque)) => Err(Opaque),
28            Err(_) => Err(Opaque),
29        })
30    }
31
32    /// Construct the `Ty` corresponding to the current adt. The generics must be the generics for
33    /// that def_id.
34    fn adt_self_ty(&mut self, span: Span, def_id: &hax::DefId) -> Result<Ty, Error> {
35        // The def_id must correspond to a type definition.
36        let self_decl_id = self.register_type_decl_id(span, def_id);
37        let self_ty = TyKind::Adt(TypeDeclRef {
38            id: TypeId::Adt(self_decl_id),
39            generics: Box::new(self.the_only_binder().params.identity_args()),
40        })
41        .into_ty();
42        Ok(self_ty)
43    }
44
45    fn adt_drop_predicate(
46        &mut self,
47        span: Span,
48        def_id: &hax::DefId,
49    ) -> Result<TraitDeclRef, Error> {
50        let drop_trait = self.get_lang_item(rustc_hir::LangItem::Drop);
51        let drop_trait = self.register_trait_decl_id(span, &drop_trait);
52
53        let self_ty = self.adt_self_ty(span, def_id)?;
54        let implemented_trait = TraitDeclRef {
55            id: drop_trait,
56            generics: Box::new(GenericArgs::new_types([self_ty.clone()].into())),
57        };
58        Ok(implemented_trait)
59    }
60
61    /// Given an item that is a closure, generate the `call_once`/`call_mut`/`call` method
62    /// (depending on `target_kind`).
63    #[tracing::instrument(skip(self, item_meta))]
64    pub fn translate_drop_method(
65        mut self,
66        def_id: FunDeclId,
67        item_meta: ItemMeta,
68        def: &hax::FullDef,
69    ) -> Result<FunDecl, Error> {
70        let span = item_meta.span;
71        let drop_impl_id = self.register_drop_trait_impl_id(span, def.def_id());
72
73        self.translate_def_generics(span, def)?;
74
75        let implemented_trait = self.adt_drop_predicate(span, def.def_id())?;
76        let self_ty = implemented_trait.generics.types[0].clone();
77        let impl_ref = TraitImplRef {
78            id: drop_impl_id,
79            generics: Box::new(self.the_only_binder().params.identity_args()),
80        };
81
82        let kind = ItemKind::TraitImpl {
83            impl_ref,
84            trait_ref: implemented_trait,
85            item_name: TraitItemName("drop".to_owned()),
86            reuses_default: false,
87        };
88
89        // Add the method lifetime generic.
90        assert!(self.innermost_binder_mut().bound_region_vars.is_empty());
91        let region_id = self
92            .innermost_binder_mut()
93            .push_bound_region(hax::BoundRegionKind::Anon);
94
95        let body = if item_meta.opacity.with_private_contents().is_opaque() {
96            Err(Opaque)
97        } else {
98            self.translate_drop_method_body(span, def)?
99        };
100
101        let input = TyKind::Ref(
102            Region::Var(DeBruijnVar::new_at_zero(region_id)),
103            self_ty,
104            RefKind::Mut,
105        )
106        .into_ty();
107        let signature = FunSig {
108            generics: self.into_generics(),
109            is_unsafe: false,
110            inputs: vec![input],
111            output: Ty::mk_unit(),
112        };
113
114        Ok(FunDecl {
115            def_id,
116            item_meta,
117            signature,
118            kind,
119            is_global_initializer: None,
120            body,
121        })
122    }
123
124    #[tracing::instrument(skip(self, item_meta))]
125    pub fn translate_drop_impl(
126        mut self,
127        impl_id: TraitImplId,
128        item_meta: ItemMeta,
129        def: &hax::FullDef,
130    ) -> Result<TraitImpl, Error> {
131        let span = item_meta.span;
132
133        self.translate_def_generics(span, def)?;
134
135        let implemented_trait = self.adt_drop_predicate(span, def.def_id())?;
136        let drop_trait = implemented_trait.id;
137
138        // Construct the method reference.
139        let method_id = self.register_drop_method_id(span, &def.def_id);
140        let method_name = TraitItemName("drop".to_owned());
141        let method_binder = {
142            let mut method_params = GenericParams::empty();
143            method_params
144                .regions
145                .push_with(|index| RegionVar { index, name: None });
146
147            let generics = self
148                .outermost_binder()
149                .params
150                .identity_args_at_depth(DeBruijnId::one())
151                .concat(&method_params.identity_args_at_depth(DeBruijnId::zero()));
152            Binder::new(
153                BinderKind::TraitMethod(drop_trait, method_name.clone()),
154                method_params,
155                FunDeclRef {
156                    id: method_id,
157                    generics: Box::new(generics),
158                },
159            )
160        };
161
162        let parent_trait_refs = {
163            let meta_sized_trait = self.get_lang_item(rustc_hir::LangItem::MetaSized);
164            let meta_sized_trait = self.register_trait_decl_id(span, &meta_sized_trait);
165            let self_ty = implemented_trait.generics.types[0].clone();
166            [TraitRef::new_builtin(
167                meta_sized_trait,
168                self_ty,
169                Default::default(),
170            )]
171            .into()
172        };
173
174        Ok(TraitImpl {
175            def_id: impl_id,
176            item_meta,
177            impl_trait: implemented_trait,
178            generics: self.into_generics(),
179            methods: vec![(method_name, method_binder)],
180            parent_trait_refs,
181            type_clauses: Default::default(),
182            consts: Default::default(),
183            types: Default::default(),
184        })
185    }
186}
charon_driver/translate/translate_drops.rs

charon_driver/translate/
translate_drops.rs
