1use super::translate_ctx::*;
18use charon_lib::ast::*;
19use charon_lib::options::{CliOpts, TranslateOptions};
20use charon_lib::transform::TransformCtx;
21use hax::SInto;
22use itertools::Itertools;
23use macros::VariantIndexArity;
24use rustc_middle::ty::TyCtxt;
25use std::cell::RefCell;
26use std::path::PathBuf;
27
28#[derive(Clone, Debug, PartialEq, Eq, Hash)]
32pub struct TransItemSource {
33 pub item: RustcItem,
34 pub kind: TransItemSourceKind,
35}
36
37#[derive(Clone, Debug, PartialEq, Eq, Hash)]
40pub enum RustcItem {
41 Poly(hax::DefId),
42 Mono(hax::ItemRef),
43}
44
45#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, VariantIndexArity)]
47pub enum TransItemSourceKind {
48 Global,
49 TraitDecl,
50 TraitImpl(TraitImplSource),
51 Fun,
52 Type,
53 InherentImpl,
55 Module,
57 ClosureMethod(ClosureKind),
59 ClosureAsFnCast,
61 EmptyDropMethod,
64 DropInPlaceMethod(Option<TraitImplSource>),
70 VTable,
72 VTableInstance(TraitImplSource),
74 VTableInstanceInitializer(TraitImplSource),
76 VTableMethod,
80}
81
82#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, VariantIndexArity)]
84pub enum TraitImplSource {
85 Normal,
87 TraitAlias,
89 Closure(ClosureKind),
91 ImplicitDrop,
94}
95
96impl TransItemSource {
97 pub fn new(item: RustcItem, kind: TransItemSourceKind) -> Self {
98 if let RustcItem::Mono(item) = &item {
99 if item.has_param {
100 panic!("Item is not monomorphic: {item:?}")
101 }
102 }
103 Self { item, kind }
104 }
105
106 pub fn from_item(item: &hax::ItemRef, kind: TransItemSourceKind, monomorphize: bool) -> Self {
109 if monomorphize {
110 Self::monomorphic(item, kind)
111 } else {
112 Self::polymorphic(&item.def_id, kind)
113 }
114 }
115
116 pub fn polymorphic(def_id: &hax::DefId, kind: TransItemSourceKind) -> Self {
118 Self::new(RustcItem::Poly(def_id.clone()), kind)
119 }
120
121 pub fn monomorphic(item: &hax::ItemRef, kind: TransItemSourceKind) -> Self {
123 Self::new(RustcItem::Mono(item.clone()), kind)
124 }
125
126 pub fn def_id(&self) -> &hax::DefId {
127 self.item.def_id()
128 }
129
130 pub(crate) fn with_kind(&self, kind: TransItemSourceKind) -> Self {
132 let mut ret = self.clone();
133 ret.kind = kind;
134 ret
135 }
136
137 pub(crate) fn parent(&self) -> Option<Self> {
140 let parent_kind = match self.kind {
141 TransItemSourceKind::ClosureMethod(kind) => {
142 TransItemSourceKind::TraitImpl(TraitImplSource::Closure(kind))
143 }
144 TransItemSourceKind::EmptyDropMethod => {
145 TransItemSourceKind::TraitImpl(TraitImplSource::ImplicitDrop)
146 }
147 TransItemSourceKind::DropInPlaceMethod(Some(impl_kind))
148 | TransItemSourceKind::VTableInstance(impl_kind)
149 | TransItemSourceKind::VTableInstanceInitializer(impl_kind) => {
150 TransItemSourceKind::TraitImpl(impl_kind)
151 }
152 TransItemSourceKind::DropInPlaceMethod(None) => TransItemSourceKind::TraitDecl,
153 _ => return None,
154 };
155 Some(self.with_kind(parent_kind))
156 }
157
158 pub(crate) fn is_derived_item(&self) -> bool {
161 use TransItemSourceKind::*;
162 match self.kind {
163 Global
164 | TraitDecl
165 | TraitImpl(TraitImplSource::Normal)
166 | InherentImpl
167 | Module
168 | Fun
169 | Type => false,
170 _ => true,
171 }
172 }
173
174 fn sort_key(&self) -> impl Ord + '_ {
176 let item_id = match &self.item {
177 RustcItem::Poly(_) => None,
178 RustcItem::Mono(item) => Some(item.id()),
179 };
180 (self.def_id().index, &self.kind, item_id)
181 }
182}
183
184impl RustcItem {
185 pub fn def_id(&self) -> &hax::DefId {
186 match self {
187 RustcItem::Poly(def_id) => def_id,
188 RustcItem::Mono(item_ref) => &item_ref.def_id,
189 }
190 }
191}
192
193impl PartialOrd for TransItemSource {
195 fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
196 Some(self.cmp(other))
197 }
198}
199impl Ord for TransItemSource {
200 fn cmp(&self, other: &Self) -> std::cmp::Ordering {
201 self.sort_key().cmp(&other.sort_key())
202 }
203}
204
205impl<'tcx, 'ctx> TranslateCtx<'tcx> {
206 pub fn base_kind_for_item(&mut self, def_id: &hax::DefId) -> Option<TransItemSourceKind> {
209 use hax::DefKind::*;
210 Some(match &def_id.kind {
211 Enum { .. } | Struct { .. } | Union { .. } | TyAlias { .. } | ForeignTy => {
212 TransItemSourceKind::Type
213 }
214 Fn { .. } | AssocFn { .. } => TransItemSourceKind::Fun,
215 Const { .. } | Static { .. } | AssocConst { .. } => TransItemSourceKind::Global,
216 Trait { .. } | TraitAlias { .. } => TransItemSourceKind::TraitDecl,
217 Impl { of_trait: true } => TransItemSourceKind::TraitImpl(TraitImplSource::Normal),
218 Impl { of_trait: false } => TransItemSourceKind::InherentImpl,
219 Mod { .. } | ForeignMod { .. } => TransItemSourceKind::Module,
220
221 ExternCrate { .. } | GlobalAsm { .. } | Macro { .. } | Use { .. } => return None,
223 AnonConst { .. }
225 | AssocTy { .. }
226 | Closure { .. }
227 | ConstParam { .. }
228 | Ctor { .. }
229 | Field { .. }
230 | InlineConst { .. }
231 | PromotedConst { .. }
232 | LifetimeParam { .. }
233 | OpaqueTy { .. }
234 | SyntheticCoroutineBody { .. }
235 | TyParam { .. }
236 | Variant { .. } => {
237 let span = self.def_span(def_id);
238 register_error!(
239 self,
240 span,
241 "Cannot register item `{def_id:?}` with kind `{:?}`",
242 def_id.kind
243 );
244 return None;
245 }
246 })
247 }
248
249 #[tracing::instrument(skip(self))]
253 pub fn enqueue_module_item(&mut self, def_id: &hax::DefId) {
254 let Some(kind) = self.base_kind_for_item(def_id) else {
255 return;
256 };
257 let item_src = if self.options.monomorphize_with_hax {
258 if let Ok(def) = self.poly_hax_def(def_id)
259 && !def.has_any_generics()
260 {
261 TransItemSource::monomorphic(def.this(), kind)
263 } else {
264 return;
266 }
267 } else {
268 TransItemSource::polymorphic(def_id, kind)
269 };
270 let _: Option<ItemId> = self.register_and_enqueue(&None, item_src);
271 }
272
273 pub(crate) fn register_no_enqueue<T: TryFrom<ItemId>>(
274 &mut self,
275 dep_src: &Option<DepSource>,
276 src: &TransItemSource,
277 ) -> Option<T> {
278 let item_id = match self.id_map.get(src) {
279 Some(tid) => *tid,
280 None => {
281 use TransItemSourceKind::*;
282 let trans_id = match src.kind {
283 Type | VTable => ItemId::Type(self.translated.type_decls.reserve_slot()),
284 TraitDecl => ItemId::TraitDecl(self.translated.trait_decls.reserve_slot()),
285 TraitImpl(..) => ItemId::TraitImpl(self.translated.trait_impls.reserve_slot()),
286 Global | VTableInstance(..) => {
287 ItemId::Global(self.translated.global_decls.reserve_slot())
288 }
289 Fun
290 | ClosureMethod(..)
291 | ClosureAsFnCast
292 | EmptyDropMethod
293 | DropInPlaceMethod(..)
294 | VTableInstanceInitializer(..)
295 | VTableMethod => ItemId::Fun(self.translated.fun_decls.reserve_slot()),
296 InherentImpl | Module => return None,
297 };
298 self.id_map.insert(src.clone(), trans_id);
300 self.reverse_id_map.insert(trans_id, src.clone());
301 if let Ok(name) = self.translate_name(src) {
303 self.translated.item_names.insert(trans_id, name);
304 }
305 trans_id
306 }
307 };
308 self.errors
309 .borrow_mut()
310 .register_dep_source(dep_src, item_id, src.def_id().is_local);
311 item_id.try_into().ok()
312 }
313
314 pub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>(
316 &mut self,
317 dep_src: &Option<DepSource>,
318 item_src: TransItemSource,
319 ) -> Option<T> {
320 let id = self.register_no_enqueue(dep_src, &item_src);
321 self.items_to_translate.insert(item_src);
322 id
323 }
324
325 pub(crate) fn register_target_info(&mut self) {
326 let target_data = &self.tcx.data_layout;
327 self.translated.target_information = krate::TargetInfo {
328 target_pointer_size: target_data.pointer_size().bytes(),
329 is_little_endian: matches!(target_data.endian, rustc_abi::Endian::Little),
330 }
331 }
332}
333
334pub struct ItemRef<Id> {
335 id: Id,
336 generics: BoxedArgs,
337}
338
339macro_rules! convert_item_ref {
341 ($item_ref_ty:ident($id:ident)) => {
342 impl TryFrom<ItemRef<ItemId>> for $item_ref_ty {
343 type Error = ();
344 fn try_from(item: ItemRef<ItemId>) -> Result<Self, ()> {
345 Ok($item_ref_ty {
346 id: item.id.try_into()?,
347 generics: item.generics,
348 })
349 }
350 }
351 impl From<ItemRef<$id>> for $item_ref_ty {
352 fn from(item: ItemRef<$id>) -> Self {
353 $item_ref_ty {
354 id: item.id,
355 generics: item.generics,
356 }
357 }
358 }
359 };
360}
361convert_item_ref!(TypeDeclRef(TypeId));
362convert_item_ref!(FunDeclRef(FunDeclId));
363convert_item_ref!(MaybeBuiltinFunDeclRef(FunId));
364convert_item_ref!(GlobalDeclRef(GlobalDeclId));
365convert_item_ref!(TraitDeclRef(TraitDeclId));
366convert_item_ref!(TraitImplRef(TraitImplId));
367impl TryFrom<ItemRef<ItemId>> for FnPtr {
368 type Error = ();
369 fn try_from(item: ItemRef<ItemId>) -> Result<Self, ()> {
370 let id: FunId = item.id.try_into()?;
371 Ok(FnPtr::new(id.into(), item.generics))
372 }
373}
374
375impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
377 pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
378 Some(DepSource {
379 src_id: self.item_id?,
380 span: self.item_src.def_id().is_local.then_some(span),
381 })
382 }
383
384 pub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>(
386 &mut self,
387 span: Span,
388 item_src: TransItemSource,
389 ) -> T {
390 let dep_src = self.make_dep_source(span);
391 self.t_ctx.register_and_enqueue(&dep_src, item_src).unwrap()
392 }
393
394 pub(crate) fn register_no_enqueue<T: TryFrom<ItemId>>(
395 &mut self,
396 span: Span,
397 src: &TransItemSource,
398 ) -> T {
399 let dep_src = self.make_dep_source(span);
400 self.t_ctx.register_no_enqueue(&dep_src, src).unwrap()
401 }
402
403 pub(crate) fn register_item_maybe_enqueue<T: TryFrom<ItemId>>(
405 &mut self,
406 span: Span,
407 enqueue: bool,
408 item: &hax::ItemRef,
409 kind: TransItemSourceKind,
410 ) -> T {
411 let item = if self.monomorphize() && item.has_param {
412 item.erase(self.hax_state_with_id())
413 } else {
414 item.clone()
415 };
416 let item_src = TransItemSource::from_item(&item, kind, self.monomorphize());
417 if enqueue {
418 self.register_and_enqueue(span, item_src)
419 } else {
420 self.register_no_enqueue(span, &item_src)
421 }
422 }
423
424 pub(crate) fn register_item<T: TryFrom<ItemId>>(
426 &mut self,
427 span: Span,
428 item: &hax::ItemRef,
429 kind: TransItemSourceKind,
430 ) -> T {
431 self.register_item_maybe_enqueue(span, true, item, kind)
432 }
433
434 #[expect(dead_code)]
436 pub(crate) fn register_item_no_enqueue<T: TryFrom<ItemId>>(
437 &mut self,
438 span: Span,
439 item: &hax::ItemRef,
440 kind: TransItemSourceKind,
441 ) -> T {
442 self.register_item_maybe_enqueue(span, false, item, kind)
443 }
444
445 pub(crate) fn translate_item_maybe_enqueue<T: TryFrom<ItemRef<ItemId>>>(
447 &mut self,
448 span: Span,
449 enqueue: bool,
450 item: &hax::ItemRef,
451 kind: TransItemSourceKind,
452 ) -> Result<T, Error> {
453 let id: ItemId = self.register_item_maybe_enqueue(span, enqueue, item, kind);
454 let generics = if self.monomorphize() {
455 Ok(GenericArgs::empty())
456 } else {
457 self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)
458 }?;
459 let item = ItemRef {
460 id,
461 generics: Box::new(generics),
462 };
463 Ok(item.try_into().ok().unwrap())
464 }
465
466 pub(crate) fn translate_item<T: TryFrom<ItemRef<ItemId>>>(
472 &mut self,
473 span: Span,
474 item: &hax::ItemRef,
475 kind: TransItemSourceKind,
476 ) -> Result<T, Error> {
477 self.translate_item_maybe_enqueue(span, true, item, kind)
478 }
479
480 #[expect(dead_code)]
482 pub(crate) fn translate_item_no_enqueue<T: TryFrom<ItemRef<ItemId>>>(
483 &mut self,
484 span: Span,
485 item: &hax::ItemRef,
486 kind: TransItemSourceKind,
487 ) -> Result<T, Error> {
488 self.translate_item_maybe_enqueue(span, false, item, kind)
489 }
490
491 pub(crate) fn translate_type_decl_ref(
493 &mut self,
494 span: Span,
495 item: &hax::ItemRef,
496 ) -> Result<TypeDeclRef, Error> {
497 match self.recognize_builtin_type(item)? {
498 Some(id) => {
499 let generics =
500 self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
501 Ok(TypeDeclRef {
502 id: TypeId::Builtin(id),
503 generics: Box::new(generics),
504 })
505 }
506 None => self.translate_item(span, item, TransItemSourceKind::Type),
507 }
508 }
509
510 pub(crate) fn translate_fun_item(
512 &mut self,
513 span: Span,
514 item: &hax::ItemRef,
515 kind: TransItemSourceKind,
516 ) -> Result<MaybeBuiltinFunDeclRef, Error> {
517 match self.recognize_builtin_fun(item)? {
518 Some(id) => {
519 let generics =
520 self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
521 Ok(MaybeBuiltinFunDeclRef {
522 id: FunId::Builtin(id),
523 generics: Box::new(generics),
524 })
525 }
526 None => self.translate_item(span, item, kind),
527 }
528 }
529
530 #[tracing::instrument(skip(self, span))]
533 pub(crate) fn translate_fn_ptr(
534 &mut self,
535 span: Span,
536 item: &hax::ItemRef,
537 kind: TransItemSourceKind,
538 ) -> Result<RegionBinder<FnPtr>, Error> {
539 let fun_item = self.translate_fun_item(span, item, kind)?;
540 let late_bound = match self.hax_def(item)?.kind() {
541 hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
542 Some(sig.as_ref().rebind(()))
543 }
544 _ => None,
545 };
546 let bound_generics =
547 self.append_late_bound_to_generics(span, *fun_item.generics, late_bound)?;
548 let fun_id = match &item.in_trait {
549 None => FnPtrKind::Fun(fun_item.id),
551 Some(impl_expr) => {
553 let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
554 let name = self.t_ctx.translate_trait_item_name(&item.def_id)?;
555 let method_decl_id = *fun_item
556 .id
557 .as_regular()
558 .expect("methods are not builtin functions");
559 FnPtrKind::Trait(trait_ref.move_under_binder(), name, method_decl_id)
560 }
561 };
562 Ok(bound_generics.map(|generics| FnPtr::new(fun_id, generics)))
563 }
564
565 pub(crate) fn translate_global_decl_ref(
566 &mut self,
567 span: Span,
568 item: &hax::ItemRef,
569 ) -> Result<GlobalDeclRef, Error> {
570 self.translate_item(span, item, TransItemSourceKind::Global)
571 }
572
573 pub(crate) fn translate_trait_decl_ref(
574 &mut self,
575 span: Span,
576 item: &hax::ItemRef,
577 ) -> Result<TraitDeclRef, Error> {
578 self.translate_item(span, item, TransItemSourceKind::TraitDecl)
579 }
580
581 pub(crate) fn translate_trait_impl_ref(
582 &mut self,
583 span: Span,
584 item: &hax::ItemRef,
585 kind: TraitImplSource,
586 ) -> Result<TraitImplRef, Error> {
587 self.translate_item(span, item, TransItemSourceKind::TraitImpl(kind))
588 }
589}
590
591#[tracing::instrument(skip(tcx))]
592pub fn translate<'tcx, 'ctx>(
593 options: &CliOpts,
594 tcx: TyCtxt<'tcx>,
595 sysroot: PathBuf,
596) -> TransformCtx {
597 let hax_state = hax::state::State::new(
598 tcx,
599 hax::options::Options {
600 inline_anon_consts: true,
601 bounds_options: hax::options::BoundsOptions {
602 resolve_drop: options.add_drop_bounds,
603 prune_sized: false,
604 },
605 },
606 );
607
608 let crate_def_id: hax::DefId = rustc_span::def_id::CRATE_DEF_ID
609 .to_def_id()
610 .sinto(&hax_state);
611 let crate_name = crate_def_id.krate.clone();
612 trace!("# Crate: {}", crate_name);
613
614 let mut error_ctx = ErrorCtx::new(!options.abort_on_error, options.error_on_warnings);
615 let translate_options = TranslateOptions::new(&mut error_ctx, options);
616 let mut ctx = TranslateCtx {
617 tcx,
618 sysroot,
619 hax_state,
620 options: translate_options,
621 errors: RefCell::new(error_ctx),
622 translated: TranslatedCrate {
623 crate_name,
624 options: options.clone(),
625 ..TranslatedCrate::default()
626 },
627 id_map: Default::default(),
628 reverse_id_map: Default::default(),
629 file_to_id: Default::default(),
630 items_to_translate: Default::default(),
631 processed: Default::default(),
632 translate_stack: Default::default(),
633 cached_item_metas: Default::default(),
634 cached_names: Default::default(),
635 };
636 ctx.register_target_info();
637
638 if options.start_from.is_empty() {
639 ctx.enqueue_module_item(&crate_def_id);
641 } else {
642 for path in options.start_from.iter() {
644 let path = path.split("::").collect_vec();
645 let resolved = super::resolve_path::def_path_def_ids(&ctx.hax_state, &path);
646 match resolved {
647 Ok(resolved) => {
648 for def_id in resolved {
649 let def_id: hax::DefId = def_id.sinto(&ctx.hax_state);
650 ctx.enqueue_module_item(&def_id);
651 }
652 }
653 Err(path) => {
654 let path = path.join("::");
655 register_error!(
656 ctx,
657 Span::dummy(),
658 "path {path} does not correspond to any item"
659 );
660 }
661 }
662 }
663 }
664
665 trace!(
666 "Queue after we explored the crate:\n{:?}",
667 &ctx.items_to_translate
668 );
669
670 ctx.translate_unit_metadata_const();
671
672 while let Some(item_src) = ctx.items_to_translate.pop_first() {
682 trace!("About to translate item: {:?}", item_src);
683 if ctx.processed.insert(item_src.clone()) {
684 ctx.translate_item(&item_src);
685 }
686 }
687
688 TransformCtx {
690 options: ctx.options,
691 translated: ctx.translated,
692 errors: ctx.errors,
693 }
694}