1use super::translate_bodies::BodyTransCtx;
2use super::translate_crate::TransItemSource;
3use super::translate_ctx::*;
4use charon_lib::ast::*;
5use charon_lib::formatter::IntoFormatter;
6use charon_lib::pretty::FmtWithCtx;
7use hax_frontend_exporter as hax;
8use indexmap::IndexMap;
9use itertools::Itertools;
10use std::mem;
11use std::sync::Arc;
12
13impl<'tcx, 'ctx> TranslateCtx<'tcx> {
14 pub(crate) fn translate_item(&mut self, item_src: &TransItemSource) {
15 let trans_id = self.id_map.get(&item_src).copied();
16 let def_id = item_src.as_def_id();
17 self.with_def_id(def_id, trans_id, |mut ctx| {
18 let span = ctx.def_span(def_id);
19 let res = {
21 let mut ctx = std::panic::AssertUnwindSafe(&mut ctx);
23 std::panic::catch_unwind(move || ctx.translate_item_aux(item_src, trans_id))
24 };
25 match res {
26 Ok(Ok(())) => return,
27 Ok(Err(_)) => {
29 register_error!(ctx, span, "Item `{def_id:?}` caused errors; ignoring.")
30 }
31 Err(_) => register_error!(
33 ctx,
34 span,
35 "Thread panicked when extracting item `{def_id:?}`."
36 ),
37 };
38 })
39 }
40
41 pub(crate) fn translate_item_aux(
42 &mut self,
43 item_src: &TransItemSource,
44 trans_id: Option<AnyTransId>,
45 ) -> Result<(), Error> {
46 let name = self.translate_name(item_src)?;
48 if let Some(trans_id) = trans_id {
49 self.translated.item_names.insert(trans_id, name.clone());
50 }
51 let opacity = self.opacity_for_name(&name);
52 if opacity.is_invisible() {
53 return Ok(());
55 }
56 let def = self.hax_def(item_src.as_def_id())?;
57 let item_meta = self.translate_item_meta(&def, item_src, name, opacity);
58
59 let bt_ctx = ItemTransCtx::new(def.def_id.clone(), trans_id, self);
61 match item_src {
62 TransItemSource::Type(_) => {
63 let Some(AnyTransId::Type(id)) = trans_id else {
64 unreachable!()
65 };
66 let ty = bt_ctx.translate_type_decl(id, item_meta, &def)?;
67 self.translated.type_decls.set_slot(id, ty);
68 }
69 TransItemSource::Fun(_) => {
70 let Some(AnyTransId::Fun(id)) = trans_id else {
71 unreachable!()
72 };
73 let fun_decl = bt_ctx.translate_function(id, item_meta, &def)?;
74 self.translated.fun_decls.set_slot(id, fun_decl);
75 }
76 TransItemSource::Global(_) => {
77 let Some(AnyTransId::Global(id)) = trans_id else {
78 unreachable!()
79 };
80 let global_decl = bt_ctx.translate_global(id, item_meta, &def)?;
81 self.translated.global_decls.set_slot(id, global_decl);
82 }
83 TransItemSource::TraitDecl(_) => {
84 let Some(AnyTransId::TraitDecl(id)) = trans_id else {
85 unreachable!()
86 };
87 let trait_decl = bt_ctx.translate_trait_decl(id, item_meta, &def)?;
88 self.translated.trait_decls.set_slot(id, trait_decl);
89 }
90 TransItemSource::TraitImpl(_) => {
91 let Some(AnyTransId::TraitImpl(id)) = trans_id else {
92 unreachable!()
93 };
94 let trait_impl = bt_ctx.translate_trait_impl(id, item_meta, &def)?;
95 self.translated.trait_impls.set_slot(id, trait_impl);
96 }
97 TransItemSource::ClosureTraitImpl(_, kind) => {
98 let Some(AnyTransId::TraitImpl(id)) = trans_id else {
99 unreachable!()
100 };
101 let closure_trait_impl =
102 bt_ctx.translate_closure_trait_impl(id, item_meta, &def, *kind)?;
103 self.translated.trait_impls.set_slot(id, closure_trait_impl);
104 }
105 TransItemSource::ClosureMethod(_, kind) => {
106 let Some(AnyTransId::Fun(id)) = trans_id else {
107 unreachable!()
108 };
109 let fun_decl = bt_ctx.translate_closure_method(id, item_meta, &def, *kind)?;
110 self.translated.fun_decls.set_slot(id, fun_decl);
111 }
112 }
113 Ok(())
114 }
115}
116
117impl ItemTransCtx<'_, '_> {
118 pub(crate) fn get_item_kind(
119 &mut self,
120 span: Span,
121 def: &hax::FullDef,
122 ) -> Result<ItemKind, Error> {
123 let assoc = match def.kind() {
124 hax::FullDefKind::AssocTy {
125 associated_item, ..
126 }
127 | hax::FullDefKind::AssocConst {
128 associated_item, ..
129 }
130 | hax::FullDefKind::AssocFn {
131 associated_item, ..
132 } => associated_item,
133 hax::FullDefKind::Closure { args, .. } => {
134 let info = self.translate_closure_info(span, args)?;
135 return Ok(ItemKind::Closure { info });
136 }
137 _ => return Ok(ItemKind::TopLevel),
138 };
139 Ok(match &assoc.container {
140 hax::AssocItemContainer::InherentImplContainer { .. } => ItemKind::TopLevel,
147 hax::AssocItemContainer::TraitImplContainer {
154 impl_id,
155 impl_generics,
156 impl_required_impl_exprs,
157 implemented_trait_ref,
158 implemented_trait_item,
159 overrides_default,
160 ..
161 } => {
162 let impl_id = self.register_trait_impl_id(span, impl_id);
163 let impl_ref = TraitImplRef {
164 impl_id,
165 generics: Box::new(self.translate_generic_args(
166 span,
167 impl_generics,
168 impl_required_impl_exprs,
169 None,
170 GenericsSource::item(impl_id),
171 )?),
172 };
173 let trait_ref = self.translate_trait_ref(span, implemented_trait_ref)?;
174 if matches!(def.kind(), hax::FullDefKind::AssocFn { .. }) {
175 let _ = self.register_fun_decl_id(span, implemented_trait_item);
179 }
180 ItemKind::TraitImpl {
181 impl_ref,
182 trait_ref,
183 item_name: TraitItemName(assoc.name.clone()),
184 reuses_default: !overrides_default,
185 }
186 }
187 hax::AssocItemContainer::TraitContainer { trait_ref, .. } => {
195 let trait_ref = self.translate_trait_ref(span, trait_ref)?;
198 let item_name = TraitItemName(assoc.name.clone());
199 ItemKind::TraitDecl {
200 trait_ref,
201 item_name,
202 has_default: assoc.has_value,
203 }
204 }
205 })
206 }
207
208 #[tracing::instrument(skip(self, item_meta))]
214 pub fn translate_type_decl(
215 mut self,
216 trans_id: TypeDeclId,
217 item_meta: ItemMeta,
218 def: &hax::FullDef,
219 ) -> Result<TypeDecl, Error> {
220 let span = item_meta.span;
221
222 self.translate_def_generics(span, def)?;
224
225 let kind = match &def.kind {
227 _ if item_meta.opacity.is_opaque() => Ok(TypeDeclKind::Opaque),
228 hax::FullDefKind::OpaqueTy | hax::FullDefKind::ForeignTy => Ok(TypeDeclKind::Opaque),
229 hax::FullDefKind::TyAlias { ty, .. } => {
230 self.error_on_impl_expr_error = false;
232 let ty = ty.as_ref().unwrap();
234 self.translate_ty(span, ty).map(TypeDeclKind::Alias)
235 }
236 hax::FullDefKind::Struct { def, .. }
237 | hax::FullDefKind::Enum { def, .. }
238 | hax::FullDefKind::Union { def, .. } => {
239 self.translate_adt_def(trans_id, span, &item_meta, def)
240 }
241 hax::FullDefKind::Closure { args, .. } => {
242 self.translate_closure_adt(trans_id, span, &args)
243 }
244 _ => panic!("Unexpected item when translating types: {def:?}"),
245 };
246
247 let kind = match kind {
248 Ok(kind) => kind,
249 Err(err) => TypeDeclKind::Error(err.msg),
250 };
251 let layout = self.translate_layout();
252 let type_def = TypeDecl {
253 def_id: trans_id,
254 item_meta,
255 generics: self.into_generics(),
256 kind,
257 layout,
258 };
259
260 Ok(type_def)
261 }
262
263 #[tracing::instrument(skip(self, item_meta))]
265 pub fn translate_function(
266 mut self,
267 def_id: FunDeclId,
268 item_meta: ItemMeta,
269 def: &hax::FullDef,
270 ) -> Result<FunDecl, Error> {
271 trace!("About to translate function:\n{:?}", def.def_id);
272 let span = item_meta.span;
273
274 trace!("Translating function signature");
276 let signature = self.translate_function_signature(def, &item_meta)?;
277
278 let kind = self.get_item_kind(span, def)?;
281 let is_trait_method_decl_without_default = match &kind {
282 ItemKind::TraitDecl { has_default, .. } => !has_default,
283 _ => false,
284 };
285
286 let is_global_initializer = matches!(
287 def.kind(),
288 hax::FullDefKind::Const { .. }
289 | hax::FullDefKind::AssocConst { .. }
290 | hax::FullDefKind::AnonConst { .. }
291 | hax::FullDefKind::InlineConst { .. }
292 | hax::FullDefKind::PromotedConst { .. }
293 | hax::FullDefKind::Static { .. }
294 );
295 let is_global_initializer =
296 is_global_initializer.then(|| self.register_global_decl_id(span, &def.def_id));
297
298 let body = if item_meta.opacity.with_private_contents().is_opaque()
299 || is_trait_method_decl_without_default
300 {
301 Err(Opaque)
302 } else if let hax::FullDefKind::Ctor {
303 adt_def_id,
304 ctor_of,
305 variant_id,
306 fields,
307 output_ty,
308 ..
309 } = def.kind()
310 {
311 let body = self.build_ctor_body(
312 span,
313 &signature,
314 adt_def_id,
315 ctor_of,
316 *variant_id,
317 fields,
318 output_ty,
319 )?;
320 Ok(body)
321 } else {
322 let mut bt_ctx = BodyTransCtx::new(&mut self);
325 match bt_ctx.translate_def_body(item_meta.span, def) {
326 Ok(Ok(body)) => Ok(body),
327 Ok(Err(Opaque)) => Err(Opaque),
329 Err(_) => Err(Opaque),
332 }
333 };
334 Ok(FunDecl {
335 def_id,
336 item_meta,
337 signature,
338 kind,
339 is_global_initializer,
340 body,
341 })
342 }
343
344 #[tracing::instrument(skip(self, item_meta))]
346 pub fn translate_global(
347 mut self,
348 def_id: GlobalDeclId,
349 item_meta: ItemMeta,
350 def: &hax::FullDef,
351 ) -> Result<GlobalDecl, Error> {
352 trace!("About to translate global:\n{:?}", def.def_id);
353 let span = item_meta.span;
354
355 self.translate_def_generics(span, def)?;
363
364 let item_kind = self.get_item_kind(span, def)?;
366
367 trace!("Translating global type");
368 let ty = match &def.kind {
369 hax::FullDefKind::Const { ty, .. }
370 | hax::FullDefKind::AssocConst { ty, .. }
371 | hax::FullDefKind::AnonConst { ty, .. }
372 | hax::FullDefKind::InlineConst { ty, .. }
373 | hax::FullDefKind::PromotedConst { ty, .. }
374 | hax::FullDefKind::Static { ty, .. } => ty,
375 _ => panic!("Unexpected def for constant: {def:?}"),
376 };
377 let ty = self.translate_ty(span, ty)?;
378
379 let global_kind = match &def.kind {
380 hax::FullDefKind::Static { .. } => GlobalKind::Static,
381 hax::FullDefKind::Const { .. } | hax::FullDefKind::AssocConst { .. } => {
382 GlobalKind::NamedConst
383 }
384 hax::FullDefKind::AnonConst { .. }
385 | hax::FullDefKind::InlineConst { .. }
386 | hax::FullDefKind::PromotedConst { .. } => GlobalKind::AnonConst,
387 _ => panic!("Unexpected def for constant: {def:?}"),
388 };
389
390 let initializer = self.register_fun_decl_id(span, &def.def_id);
391
392 Ok(GlobalDecl {
393 def_id,
394 item_meta,
395 generics: self.into_generics(),
396 ty,
397 kind: item_kind,
398 global_kind,
399 init: initializer,
400 })
401 }
402
403 #[tracing::instrument(skip(self, item_meta))]
404 pub fn translate_trait_decl(
405 mut self,
406 def_id: TraitDeclId,
407 item_meta: ItemMeta,
408 def: &hax::FullDef,
409 ) -> Result<TraitDecl, Error> {
410 trace!("About to translate trait decl:\n{:?}", def.def_id);
411 trace!("Trait decl id:\n{:?}", def_id);
412
413 let span = item_meta.span;
414
415 if let hax::FullDefKind::TraitAlias { .. } = def.kind() {
416 raise_error!(self, span, "Trait aliases are not supported");
417 }
418
419 let hax::FullDefKind::Trait {
420 items,
421 self_predicate,
422 ..
423 } = &def.kind
424 else {
425 raise_error!(self, span, "Unexpected definition: {def:?}");
426 };
427 let items: Vec<(TraitItemName, &hax::AssocItem, Arc<hax::FullDef>)> = items
428 .iter()
429 .map(|(item, def)| {
430 let name = TraitItemName(item.name.clone());
431 (name, item, def.clone())
432 })
433 .collect_vec();
434
435 self.translate_def_generics(span, def)?;
440 let self_trait_ref = TraitRef {
441 kind: TraitRefKind::SelfId,
442 trait_decl_ref: RegionBinder::empty(
443 self.translate_trait_predicate(span, self_predicate)?,
444 ),
445 };
446
447 let mut consts = Vec::new();
450 let mut const_defaults = IndexMap::new();
451 let mut types = Vec::new();
452 let mut type_clauses = Vec::new();
453 let mut type_defaults = IndexMap::new();
454 let mut methods = Vec::new();
455 for (item_name, hax_item, hax_def) in &items {
456 let item_def_id = &hax_item.def_id;
457 let item_span = self.def_span(item_def_id);
458 match &hax_def.kind {
459 hax::FullDefKind::AssocFn { .. } => {
460 let fun_def = self.t_ctx.hax_def(item_def_id)?;
461 let binder_kind = BinderKind::TraitMethod(def_id, item_name.clone());
462 let fn_ref = self.translate_binder_for_def(
463 item_span,
464 binder_kind,
465 &fun_def,
466 |bt_ctx| {
467 let fun_id = if bt_ctx.t_ctx.options.translate_all_methods
475 || item_meta.opacity.is_transparent()
476 || !hax_item.has_value
477 {
478 bt_ctx.register_fun_decl_id(item_span, item_def_id)
479 } else {
480 bt_ctx.register_fun_decl_id_no_enqueue(item_span, item_def_id)
481 };
482
483 assert_eq!(bt_ctx.binding_levels.len(), 2);
484 let mut fun_generics =
485 bt_ctx.outermost_binder().params.identity_args_at_depth(
486 GenericsSource::item(def_id),
487 DeBruijnId::one(),
488 );
489 fun_generics.trait_refs.insert_and_shift_ids(
491 0.into(),
492 self_trait_ref.clone().move_under_binder(),
493 );
494 fun_generics = fun_generics.concat(
495 GenericsSource::item(fun_id),
496 &bt_ctx.innermost_binder().params.identity_args_at_depth(
497 GenericsSource::Method(def_id.into(), item_name.clone()),
498 DeBruijnId::zero(),
499 ),
500 );
501 Ok(FunDeclRef {
502 id: fun_id,
503 generics: Box::new(fun_generics),
504 })
505 },
506 )?;
507 methods.push((item_name.clone(), fn_ref));
508 }
509 hax::FullDefKind::AssocConst { ty, .. } => {
510 if hax_item.has_value {
512 let id = self.register_global_decl_id(item_span, item_def_id);
515 let generics_target = GenericsSource::item(id);
516 let mut generics =
517 self.the_only_binder().params.identity_args(generics_target);
518 generics.trait_refs.push(self_trait_ref.clone());
519 let gref = GlobalDeclRef {
520 id,
521 generics: Box::new(generics),
522 };
523 const_defaults.insert(item_name.clone(), gref);
524 };
525 let ty = self.translate_ty(item_span, ty)?;
526 consts.push((item_name.clone(), ty));
527 }
528 hax::FullDefKind::AssocTy { param_env, .. }
529 if !param_env.generics.params.is_empty() =>
530 {
531 raise_error!(
532 self,
533 item_span,
534 "Generic associated types are not supported"
535 );
536 }
537 hax::FullDefKind::AssocTy { value, .. } => {
538 if let Some(clauses) = self.item_trait_clauses.get(item_name) {
540 type_clauses.push((item_name.clone(), clauses.clone()));
541 }
542 if let Some(ty) = value {
543 let ty = self.translate_ty(item_span, &ty)?;
544 type_defaults.insert(item_name.clone(), ty);
545 };
546 types.push(item_name.clone());
547 }
548 _ => panic!("Unexpected definition for trait item: {hax_def:?}"),
549 }
550 }
551
552 Ok(TraitDecl {
556 def_id,
557 item_meta,
558 parent_clauses: mem::take(&mut self.parent_trait_clauses),
559 generics: self.into_generics(),
560 type_clauses,
561 consts,
562 const_defaults,
563 types,
564 type_defaults,
565 methods,
566 })
567 }
568
569 #[tracing::instrument(skip(self, item_meta))]
570 pub fn translate_trait_impl(
571 mut self,
572 def_id: TraitImplId,
573 item_meta: ItemMeta,
574 def: &hax::FullDef,
575 ) -> Result<TraitImpl, Error> {
576 trace!("About to translate trait impl:\n{:?}", def.def_id);
577 trace!("Trait impl id:\n{:?}", def_id);
578
579 let span = item_meta.span;
580
581 self.translate_def_generics(span, def)?;
582
583 let hax::FullDefKind::TraitImpl {
584 trait_pred,
585 implied_impl_exprs,
586 items: impl_items,
587 ..
588 } = &def.kind
589 else {
590 unreachable!()
591 };
592
593 let implemented_trait_id = &trait_pred.trait_ref.def_id;
595 let trait_id = self.register_trait_decl_id(span, implemented_trait_id);
596 let implemented_trait = {
597 let implemented_trait = &trait_pred.trait_ref;
598 let generics = self.translate_generic_args(
599 span,
600 &implemented_trait.generic_args,
601 &[],
602 None,
603 GenericsSource::item(trait_id),
604 )?;
605 TraitDeclRef {
606 trait_id,
607 generics: Box::new(generics),
608 }
609 };
610 let self_predicate = TraitRef {
612 kind: TraitRefKind::TraitImpl(
613 def_id,
614 Box::new(
615 self.the_only_binder()
616 .params
617 .identity_args(GenericsSource::item(def_id)),
618 ),
619 ),
620 trait_decl_ref: RegionBinder::empty(implemented_trait.clone()),
621 };
622
623 let parent_trait_refs = self.translate_trait_impl_exprs(span, &implied_impl_exprs)?;
625
626 {
627 let ctx = self.into_fmt();
629 let refs = parent_trait_refs
630 .iter()
631 .map(|c| c.with_ctx(&ctx))
632 .format("\n");
633 trace!(
634 "Trait impl: {:?}\n- parent_trait_refs:\n{}",
635 def.def_id,
636 refs
637 );
638 }
639
640 let mut consts = Vec::new();
642 let mut types: Vec<(TraitItemName, Ty)> = Vec::new();
643 let mut methods = Vec::new();
644 let mut type_clauses = Vec::new();
645
646 for impl_item in impl_items {
647 use hax::ImplAssocItemValue::*;
648 let name = TraitItemName(impl_item.name.clone());
649 let item_def = impl_item.def(); let item_span = self.def_span(&item_def.def_id);
651 let item_def_id = &item_def.def_id;
652 match item_def.kind() {
653 hax::FullDefKind::AssocFn { .. } => {
654 match &impl_item.value {
655 Provided { is_override, .. } => {
656 let fun_def = self.t_ctx.hax_def(item_def_id)?;
657 let binder_kind = BinderKind::TraitMethod(trait_id, name.clone());
658 let fn_ref = self.translate_binder_for_def(
659 item_span,
660 binder_kind,
661 &fun_def,
662 |bt_ctx| {
663 let fun_id = if bt_ctx.t_ctx.options.translate_all_methods
670 || item_meta.opacity.is_transparent()
671 || !*is_override
672 {
673 bt_ctx.register_fun_decl_id(item_span, item_def_id)
674 } else {
675 bt_ctx
676 .register_fun_decl_id_no_enqueue(item_span, item_def_id)
677 };
678
679 assert_eq!(bt_ctx.binding_levels.len(), 2);
681 let fun_generics = bt_ctx
682 .outermost_binder()
683 .params
684 .identity_args_at_depth(
685 GenericsSource::item(def_id),
686 DeBruijnId::one(),
687 )
688 .concat(
689 GenericsSource::item(fun_id),
690 &bt_ctx
691 .innermost_binder()
692 .params
693 .identity_args_at_depth(
694 GenericsSource::Method(
695 trait_id.into(),
696 name.clone(),
697 ),
698 DeBruijnId::zero(),
699 ),
700 );
701 Ok(FunDeclRef {
702 id: fun_id,
703 generics: Box::new(fun_generics),
704 })
705 },
706 )?;
707 methods.push((name, fn_ref));
708 }
709 DefaultedFn { .. } => {
710 }
712 _ => unreachable!(),
713 }
714 }
715 hax::FullDefKind::AssocConst { .. } => {
716 let id = self.register_global_decl_id(item_span, item_def_id);
717 let generics_target = GenericsSource::item(id);
718 let generics = match &impl_item.value {
721 Provided { .. } => {
722 self.the_only_binder().params.identity_args(generics_target)
723 }
724 _ => {
725 let mut generics = implemented_trait
726 .generics
727 .clone()
728 .with_target(generics_target);
729 generics.trait_refs.push(self_predicate.clone());
730 generics
731 }
732 };
733 let gref = GlobalDeclRef {
734 id,
735 generics: Box::new(generics),
736 };
737 consts.push((name, gref));
738 }
739 hax::FullDefKind::AssocTy { param_env, .. }
740 if !param_env.generics.params.is_empty() =>
741 {
742 }
744 hax::FullDefKind::AssocTy { value, .. } => {
745 let ty = match &impl_item.value {
746 Provided { .. } => value.as_ref().unwrap(),
747 DefaultedTy { ty, .. } => ty,
748 _ => unreachable!(),
749 };
750 let ty = self.translate_ty(item_span, &ty)?;
751 types.push((name.clone(), ty));
752
753 let trait_refs =
754 self.translate_trait_impl_exprs(item_span, &impl_item.required_impl_exprs)?;
755 type_clauses.push((name, trait_refs));
756 }
757 _ => panic!("Unexpected definition for trait item: {item_def:?}"),
758 }
759 }
760
761 Ok(TraitImpl {
762 def_id,
763 item_meta,
764 impl_trait: implemented_trait,
765 generics: self.into_generics(),
766 parent_trait_refs,
767 type_clauses,
768 consts,
769 types,
770 methods,
771 })
772 }
773}