1use super::translate_ctx::*;
18use charon_lib::ast::*;
19use charon_lib::options::{CliOpts, TranslateOptions};
20use charon_lib::transform::TransformCtx;
21use hax_frontend_exporter::{self as 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 def_id: hax::DefId,
34 pub kind: TransItemSourceKind,
35}
36
37#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash, VariantIndexArity)]
38pub enum TransItemSourceKind {
39 Global,
40 TraitDecl,
41 TraitImpl,
42 Fun,
43 Type,
44 InherentImpl,
46 Module,
48 ClosureTraitImpl(ClosureKind),
50 ClosureMethod(ClosureKind),
52 ClosureAsFnCast,
54 DropGlueImpl,
56 DropGlueMethod,
58}
59
60impl TransItemSource {
61 pub fn new(def_id: hax::DefId, kind: TransItemSourceKind) -> Self {
62 Self { def_id, kind }
63 }
64
65 pub fn as_def_id(&self) -> &hax::DefId {
66 &self.def_id
67 }
68
69 pub(crate) fn is_derived_item(&self) -> bool {
72 use TransItemSourceKind::*;
73 match self.kind {
74 Global | TraitDecl | TraitImpl | InherentImpl | Module | Fun | Type => false,
75 ClosureTraitImpl(..) | ClosureMethod(..) | ClosureAsFnCast | DropGlueImpl
76 | DropGlueMethod => true,
77 }
78 }
79
80 fn sort_key(&self) -> impl Ord + '_ {
82 (self.def_id.index, &self.kind)
83 }
84}
85
86impl PartialOrd for TransItemSource {
88 fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
89 Some(self.cmp(other))
90 }
91}
92impl Ord for TransItemSource {
93 fn cmp(&self, other: &Self) -> std::cmp::Ordering {
94 self.sort_key().cmp(&other.sort_key())
95 }
96}
97
98impl<'tcx, 'ctx> TranslateCtx<'tcx> {
99 pub fn base_kind_for_item(&mut self, def_id: &hax::DefId) -> Option<TransItemSourceKind> {
102 use hax::DefKind::*;
103 Some(match &def_id.kind {
104 Enum { .. } | Struct { .. } | Union { .. } | TyAlias { .. } | ForeignTy => {
105 TransItemSourceKind::Type
106 }
107 Fn { .. } | AssocFn { .. } => TransItemSourceKind::Fun,
108 Const { .. } | Static { .. } | AssocConst { .. } => TransItemSourceKind::Global,
109 Trait { .. } | TraitAlias { .. } => TransItemSourceKind::TraitDecl,
110 Impl { of_trait: true } => TransItemSourceKind::TraitImpl,
111 Impl { of_trait: false } => TransItemSourceKind::InherentImpl,
112 Mod { .. } | ForeignMod { .. } => TransItemSourceKind::Module,
113
114 ExternCrate { .. } | GlobalAsm { .. } | Macro { .. } | Use { .. } => return None,
116 AnonConst { .. }
118 | AssocTy { .. }
119 | Closure { .. }
120 | ConstParam { .. }
121 | Ctor { .. }
122 | Field { .. }
123 | InlineConst { .. }
124 | PromotedConst { .. }
125 | LifetimeParam { .. }
126 | OpaqueTy { .. }
127 | SyntheticCoroutineBody { .. }
128 | TyParam { .. }
129 | Variant { .. } => {
130 let span = self.def_span(def_id);
131 register_error!(
132 self,
133 span,
134 "Cannot register item `{def_id:?}` with kind `{:?}`",
135 def_id.kind
136 );
137 return None;
138 }
139 })
140 }
141
142 #[tracing::instrument(skip(self))]
146 pub fn enqueue_item(&mut self, def_id: &hax::DefId) -> Option<AnyTransId> {
147 let kind = self.base_kind_for_item(def_id)?;
148 self.register_and_enqueue_id(&None, def_id, kind)
149 }
150
151 pub(crate) fn register_id_no_enqueue(
152 &mut self,
153 dep_src: &Option<DepSource>,
154 src: &TransItemSource,
155 ) -> Option<AnyTransId> {
156 let item_id = match self.id_map.get(src) {
157 Some(tid) => *tid,
158 None => {
159 use TransItemSourceKind::*;
160 let trans_id = match src.kind {
161 Type => AnyTransId::Type(self.translated.type_decls.reserve_slot()),
162 TraitDecl => AnyTransId::TraitDecl(self.translated.trait_decls.reserve_slot()),
163 TraitImpl | ClosureTraitImpl(..) | DropGlueImpl => {
164 AnyTransId::TraitImpl(self.translated.trait_impls.reserve_slot())
165 }
166 Global => AnyTransId::Global(self.translated.global_decls.reserve_slot()),
167 Fun | ClosureMethod(..) | ClosureAsFnCast | DropGlueMethod => {
168 AnyTransId::Fun(self.translated.fun_decls.reserve_slot())
169 }
170 InherentImpl | Module => return None,
171 };
172 self.id_map.insert(src.clone(), trans_id);
174 self.reverse_id_map.insert(trans_id, src.clone());
175 if !matches!(src.kind, TraitImpl) {
178 if let Ok(name) = self.def_id_to_name(src.as_def_id()) {
179 self.translated.item_names.insert(trans_id, name);
180 }
181 }
182 trans_id
183 }
184 };
185 self.errors
186 .borrow_mut()
187 .register_dep_source(dep_src, item_id, src.as_def_id().is_local);
188 Some(item_id)
189 }
190
191 pub(crate) fn register_and_enqueue_id(
193 &mut self,
194 dep_src: &Option<DepSource>,
195 def_id: &hax::DefId,
196 kind: TransItemSourceKind,
197 ) -> Option<AnyTransId> {
198 let item_src = TransItemSource::new(def_id.clone(), kind);
199 let id = self.register_id_no_enqueue(dep_src, &item_src);
200 self.items_to_translate.insert(item_src);
201 id
202 }
203
204 pub(crate) fn register_type_decl_id(
205 &mut self,
206 src: &Option<DepSource>,
207 def_id: &hax::DefId,
208 ) -> TypeDeclId {
209 *self
210 .register_and_enqueue_id(src, def_id, TransItemSourceKind::Type)
211 .unwrap()
212 .as_type()
213 .unwrap()
214 }
215
216 pub(crate) fn register_fun_decl_id(
217 &mut self,
218 src: &Option<DepSource>,
219 def_id: &hax::DefId,
220 ) -> FunDeclId {
221 *self
222 .register_and_enqueue_id(src, def_id, TransItemSourceKind::Fun)
223 .unwrap()
224 .as_fun()
225 .unwrap()
226 }
227
228 pub(crate) fn register_trait_decl_id(
229 &mut self,
230 src: &Option<DepSource>,
231 def_id: &hax::DefId,
232 ) -> TraitDeclId {
233 *self
234 .register_and_enqueue_id(src, def_id, TransItemSourceKind::TraitDecl)
235 .unwrap()
236 .as_trait_decl()
237 .unwrap()
238 }
239
240 pub(crate) fn register_trait_impl_id(
241 &mut self,
242 src: &Option<DepSource>,
243 def_id: &hax::DefId,
244 ) -> TraitImplId {
245 if let Ok(def) = self.hax_def(def_id) {
247 let trait_id = match def.kind() {
248 hax::FullDefKind::TraitImpl { trait_pred, .. } => &trait_pred.trait_ref.def_id,
249 hax::FullDefKind::TraitAlias { .. } => def_id,
250 _ => unreachable!(),
251 };
252 let _ = self.register_trait_decl_id(src, trait_id);
253 }
254
255 *self
256 .register_and_enqueue_id(src, def_id, TransItemSourceKind::TraitImpl)
257 .unwrap()
258 .as_trait_impl()
259 .unwrap()
260 }
261
262 pub(crate) fn register_closure_trait_impl_id(
263 &mut self,
264 src: &Option<DepSource>,
265 def_id: &hax::DefId,
266 kind: ClosureKind,
267 ) -> TraitImplId {
268 *self
269 .register_and_enqueue_id(src, def_id, TransItemSourceKind::ClosureTraitImpl(kind))
270 .unwrap()
271 .as_trait_impl()
272 .unwrap()
273 }
274
275 pub(crate) fn register_closure_method_decl_id(
276 &mut self,
277 src: &Option<DepSource>,
278 def_id: &hax::DefId,
279 kind: ClosureKind,
280 ) -> FunDeclId {
281 *self
282 .register_and_enqueue_id(src, def_id, TransItemSourceKind::ClosureMethod(kind))
283 .unwrap()
284 .as_fun()
285 .unwrap()
286 }
287
288 pub(crate) fn register_closure_as_fun_decl_id(
289 &mut self,
290 src: &Option<DepSource>,
291 def_id: &hax::DefId,
292 ) -> FunDeclId {
293 *self
294 .register_and_enqueue_id(src, def_id, TransItemSourceKind::ClosureAsFnCast)
295 .unwrap()
296 .as_fun()
297 .unwrap()
298 }
299
300 pub(crate) fn register_global_decl_id(
301 &mut self,
302 src: &Option<DepSource>,
303 def_id: &hax::DefId,
304 ) -> GlobalDeclId {
305 *self
306 .register_and_enqueue_id(src, def_id, TransItemSourceKind::Global)
307 .unwrap()
308 .as_global()
309 .unwrap()
310 }
311
312 pub(crate) fn register_drop_trait_impl_id(
313 &mut self,
314 src: &Option<DepSource>,
315 def_id: &hax::DefId,
316 ) -> TraitImplId {
317 *self
318 .register_and_enqueue_id(src, def_id, TransItemSourceKind::DropGlueImpl)
319 .unwrap()
320 .as_trait_impl()
321 .unwrap()
322 }
323
324 pub(crate) fn register_drop_method_id(
325 &mut self,
326 src: &Option<DepSource>,
327 def_id: &hax::DefId,
328 ) -> FunDeclId {
329 *self
330 .register_and_enqueue_id(src, def_id, TransItemSourceKind::DropGlueMethod)
331 .unwrap()
332 .as_fun()
333 .unwrap()
334 }
335
336 pub(crate) fn register_target_info(&mut self) {
337 let target_data = &self.tcx.data_layout;
338 self.translated.target_information = krate::TargetInfo {
339 target_pointer_size: target_data.pointer_size().bytes(),
340 is_little_endian: matches!(target_data.endian, rustc_abi::Endian::Little),
341 }
342 }
343}
344
345impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
347 pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
348 Some(DepSource {
349 src_id: self.item_id?,
350 span: self.item_src.as_def_id().is_local.then_some(span),
351 })
352 }
353
354 pub(crate) fn register_id_no_enqueue(
355 &mut self,
356 span: Span,
357 id: TransItemSource,
358 ) -> Option<AnyTransId> {
359 let src = self.make_dep_source(span);
360 self.t_ctx.register_id_no_enqueue(&src, &id)
361 }
362
363 pub(crate) fn register_type_decl_id(&mut self, span: Span, id: &hax::DefId) -> TypeDeclId {
364 let src = self.make_dep_source(span);
365 self.t_ctx.register_type_decl_id(&src, id)
366 }
367
368 pub(crate) fn translate_type_id(
370 &mut self,
371 span: Span,
372 def_id: &hax::DefId,
373 ) -> Result<TypeId, Error> {
374 Ok(match self.recognize_builtin_type(def_id)? {
375 Some(id) => TypeId::Builtin(id),
376 None => TypeId::Adt(self.register_type_decl_id(span, def_id)),
377 })
378 }
379
380 pub(crate) fn translate_type_decl_ref(
381 &mut self,
382 span: Span,
383 item: &hax::ItemRef,
384 ) -> Result<TypeDeclRef, Error> {
385 let id = self.translate_type_id(span, &item.def_id)?;
386 let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
387 Ok(TypeDeclRef {
388 id,
389 generics: Box::new(generics),
390 })
391 }
392
393 pub(crate) fn register_fun_decl_id(&mut self, span: Span, id: &hax::DefId) -> FunDeclId {
394 let src = self.make_dep_source(span);
395 self.t_ctx.register_fun_decl_id(&src, id)
396 }
397
398 pub(crate) fn register_fun_decl_id_no_enqueue(
399 &mut self,
400 span: Span,
401 def_id: &hax::DefId,
402 ) -> FunDeclId {
403 self.register_id_no_enqueue(
404 span,
405 TransItemSource::new(def_id.clone(), TransItemSourceKind::Fun),
406 )
407 .unwrap()
408 .as_fun()
409 .copied()
410 .unwrap()
411 }
412
413 pub(crate) fn translate_fun_id(
415 &mut self,
416 span: Span,
417 def_id: &hax::DefId,
418 ) -> Result<FunId, Error> {
419 Ok(match self.recognize_builtin_fun(def_id)? {
420 Some(id) => FunId::Builtin(id),
421 None => FunId::Regular(self.register_fun_decl_id(span, def_id)),
422 })
423 }
424
425 #[tracing::instrument(skip(self, span))]
428 pub(crate) fn translate_fn_ptr(
429 &mut self,
430 span: Span,
431 item: &hax::ItemRef,
432 ) -> Result<RegionBinder<FnPtr>, Error> {
433 let fun_id = self.translate_fun_id(span, &item.def_id)?;
434 let late_bound = match self.hax_def(&item.def_id)?.kind() {
435 hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
436 Some(sig.as_ref().rebind(()))
437 }
438 _ => None,
439 };
440 let bound_generics = self.translate_generic_args_with_late_bound(
441 span,
442 &item.generic_args,
443 &item.impl_exprs,
444 late_bound,
445 )?;
446 let fun_id = match &item.in_trait {
447 None => FunIdOrTraitMethodRef::Fun(fun_id),
449 Some(impl_expr) => {
451 let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
452 let name = self.t_ctx.translate_trait_item_name(&item.def_id)?;
453 let method_decl_id = *fun_id
454 .as_regular()
455 .expect("methods are not builtin functions");
456 FunIdOrTraitMethodRef::Trait(trait_ref.move_under_binder(), name, method_decl_id)
457 }
458 };
459 Ok(bound_generics.map(|generics| FnPtr {
460 func: Box::new(fun_id),
461 generics: Box::new(generics),
462 }))
463 }
464
465 pub(crate) fn register_global_decl_id(&mut self, span: Span, id: &hax::DefId) -> GlobalDeclId {
466 let src = self.make_dep_source(span);
467 self.t_ctx.register_global_decl_id(&src, id)
468 }
469
470 pub(crate) fn translate_global_decl_ref(
471 &mut self,
472 span: Span,
473 item: &hax::ItemRef,
474 ) -> Result<GlobalDeclRef, Error> {
475 let id = self.register_global_decl_id(span, &item.def_id);
476 let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
477 Ok(GlobalDeclRef {
478 id,
479 generics: Box::new(generics),
480 })
481 }
482
483 pub(crate) fn register_trait_decl_id(&mut self, span: Span, id: &hax::DefId) -> TraitDeclId {
484 let src = self.make_dep_source(span);
485 self.t_ctx.register_trait_decl_id(&src, id)
486 }
487
488 pub(crate) fn translate_trait_decl_ref(
489 &mut self,
490 span: Span,
491 item: &hax::ItemRef,
492 ) -> Result<TraitDeclRef, Error> {
493 let id = self.register_trait_decl_id(span, &item.def_id);
494 let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
495 Ok(TraitDeclRef {
496 id,
497 generics: Box::new(generics),
498 })
499 }
500
501 pub(crate) fn register_trait_impl_id(&mut self, span: Span, id: &hax::DefId) -> TraitImplId {
502 let src = self.make_dep_source(span);
503 self.t_ctx.register_trait_impl_id(&src, id)
504 }
505
506 pub(crate) fn translate_trait_impl_ref(
507 &mut self,
508 span: Span,
509 item: &hax::ItemRef,
510 ) -> Result<TraitImplRef, Error> {
511 let id = self.register_trait_impl_id(span, &item.def_id);
512 let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
513 Ok(TraitImplRef {
514 id,
515 generics: Box::new(generics),
516 })
517 }
518
519 pub(crate) fn register_closure_trait_impl_id(
520 &mut self,
521 span: Span,
522 id: &hax::DefId,
523 kind: ClosureKind,
524 ) -> TraitImplId {
525 let src = self.make_dep_source(span);
526 self.t_ctx.register_closure_trait_impl_id(&src, id, kind)
527 }
528
529 pub(crate) fn register_closure_method_decl_id(
530 &mut self,
531 span: Span,
532 id: &hax::DefId,
533 kind: ClosureKind,
534 ) -> FunDeclId {
535 let src = self.make_dep_source(span);
536 self.t_ctx.register_closure_method_decl_id(&src, id, kind)
537 }
538
539 pub(crate) fn register_closure_as_fun_decl_id(
540 &mut self,
541 span: Span,
542 id: &hax::DefId,
543 ) -> FunDeclId {
544 let src = self.make_dep_source(span);
545 self.t_ctx.register_closure_as_fun_decl_id(&src, id)
546 }
547
548 pub(crate) fn register_drop_trait_impl_id(
549 &mut self,
550 span: Span,
551 id: &hax::DefId,
552 ) -> TraitImplId {
553 let src = self.make_dep_source(span);
554 self.t_ctx.register_drop_trait_impl_id(&src, id)
555 }
556
557 pub(crate) fn translate_drop_trait_impl_ref(
558 &mut self,
559 span: Span,
560 item: &hax::ItemRef,
561 ) -> Result<TraitImplRef, Error> {
562 let id = self.register_drop_trait_impl_id(span, &item.def_id);
563 let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
564 Ok(TraitImplRef {
565 id,
566 generics: Box::new(generics),
567 })
568 }
569
570 pub(crate) fn register_drop_method_id(&mut self, span: Span, id: &hax::DefId) -> FunDeclId {
571 let src = self.make_dep_source(span);
572 self.t_ctx.register_drop_method_id(&src, id)
573 }
574}
575
576#[tracing::instrument(skip(tcx))]
577pub fn translate<'tcx, 'ctx>(
578 options: &CliOpts,
579 tcx: TyCtxt<'tcx>,
580 sysroot: PathBuf,
581) -> TransformCtx {
582 let hax_state = hax::state::State::new(
583 tcx,
584 hax::options::Options {
585 inline_anon_consts: true,
586 resolve_drop_bounds: options.add_drop_bounds,
587 },
588 );
589
590 let crate_def_id: hax::DefId = rustc_span::def_id::CRATE_DEF_ID
591 .to_def_id()
592 .sinto(&hax_state);
593 let crate_name = crate_def_id.krate.clone();
594 trace!("# Crate: {}", crate_name);
595
596 let mut error_ctx = ErrorCtx::new(!options.abort_on_error, options.error_on_warnings);
597 let translate_options = TranslateOptions::new(&mut error_ctx, options);
598 let mut ctx = TranslateCtx {
599 tcx,
600 sysroot,
601 hax_state,
602 options: translate_options,
603 errors: RefCell::new(error_ctx),
604 translated: TranslatedCrate {
605 crate_name,
606 options: options.clone(),
607 ..TranslatedCrate::default()
608 },
609 id_map: Default::default(),
610 reverse_id_map: Default::default(),
611 file_to_id: Default::default(),
612 items_to_translate: Default::default(),
613 processed: Default::default(),
614 cached_item_metas: Default::default(),
615 cached_names: Default::default(),
616 };
617 ctx.register_target_info();
618
619 if options.start_from.is_empty() {
620 ctx.enqueue_item(&crate_def_id);
622 } else {
623 for path in options.start_from.iter() {
625 let path = path.split("::").collect_vec();
626 let resolved = super::resolve_path::def_path_def_ids(&ctx.hax_state, &path);
627 match resolved {
628 Ok(resolved) => {
629 for def_id in resolved {
630 let def_id: hax::DefId = def_id.sinto(&ctx.hax_state);
631 ctx.enqueue_item(&def_id);
632 }
633 }
634 Err(path) => {
635 let path = path.join("::");
636 register_error!(
637 ctx,
638 Span::dummy(),
639 "path {path} does not correspond to any item"
640 );
641 }
642 }
643 }
644 }
645
646 trace!(
647 "Queue after we explored the crate:\n{:?}",
648 &ctx.items_to_translate
649 );
650
651 while let Some(item_src) = ctx.items_to_translate.pop_first() {
661 trace!("About to translate item: {:?}", item_src);
662 if ctx.processed.insert(item_src.clone()) {
663 ctx.translate_item(&item_src);
664 }
665 }
666
667 TransformCtx {
669 options: ctx.options,
670 translated: ctx.translated,
671 errors: ctx.errors,
672 }
673}