charon_driver/translate/
translate_drops.rs1use 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 #[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 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 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}