1use itertools::Itertools;
3use rustc_middle::mir;
4use rustc_span::RemapPathScopeComponents;
5use std::cmp::Ord;
6use std::path::{Component, PathBuf};
7
8use super::translate_crate::RustcItem;
9use super::translate_ctx::*;
10use super::translate_generics::BindingLevel;
11use charon_lib::ast::*;
12use hax::{DefPathItem, SInto};
13
14impl<'tcx, 'ctx> TranslateCtx<'tcx> {
16 fn register_file(&mut self, filename: FileName, span: rustc_span::Span) -> FileId {
19 match self.file_to_id.get(&filename) {
21 Some(id) => *id,
22 None => {
23 let source_file = self.tcx.sess.source_map().lookup_source_file(span.lo());
24 let crate_name = self.tcx.crate_name(source_file.cnum).to_string();
25 let file = File {
26 name: filename.clone(),
27 crate_name,
28 contents: source_file.src.as_deref().cloned(),
29 };
30 let id = self.translated.files.push(file);
31 self.file_to_id.insert(filename, id);
32 id
33 }
34 }
35 }
36
37 pub fn translate_filename(&mut self, name: rustc_span::FileName) -> meta::FileName {
38 match name {
39 rustc_span::FileName::Real(name) => {
40 match name.local_path() {
41 Some(path) => {
42 let path = if let Ok(path) = path.strip_prefix(&self.sysroot) {
43 if let Ok(path) = path.strip_prefix("lib/rustlib/src/rust") {
48 let mut rewritten_path: PathBuf = "/rustc".into();
49 rewritten_path.extend(path);
50 rewritten_path
51 } else {
52 let mut rewritten_path: PathBuf = "/toolchain".into();
54 rewritten_path.extend(path);
55 rewritten_path
56 }
57 } else {
58 let cargo_home = std::env::var("CARGO_HOME")
62 .map(PathBuf::from)
63 .ok()
64 .or_else(|| std::env::home_dir().map(|p| p.join(".cargo")));
65 if let Some(cargo_home) = cargo_home
66 && let Ok(path) = path.strip_prefix(cargo_home)
67 {
68 let mut rewritten_path: PathBuf = "/cargo".into();
70 rewritten_path.extend(path);
71 rewritten_path
72 } else {
73 path.into()
74 }
75 };
76 FileName::Local(path)
77 }
78 None => {
79 let virtual_name = name.path(RemapPathScopeComponents::MACRO);
83 let mut components_iter = virtual_name.components();
84 if let Some(
85 [
86 Component::RootDir,
87 Component::Normal(rustc),
88 Component::Normal(hash),
89 ],
90 ) = components_iter.by_ref().array_chunks().next()
91 && rustc.to_str() == Some("rustc")
92 && hash.len() == 40
93 {
94 let path_without_hash = [Component::RootDir, Component::Normal(rustc)]
95 .into_iter()
96 .chain(components_iter)
97 .collect();
98 FileName::Virtual(path_without_hash)
99 } else {
100 FileName::Virtual(virtual_name.into())
101 }
102 }
103 }
104 }
105 _ => FileName::NotReal(format!("{name:?}")),
108 }
109 }
110
111 pub fn translate_span_data(&mut self, span: rustc_span::Span) -> meta::SpanData {
112 let smap: &rustc_span::source_map::SourceMap = self.tcx.sess.psess.source_map();
113 let filename = smap.span_to_filename(span);
114 let filename = self.translate_filename(filename);
115 let span = span;
116 let file_id = match &filename {
117 FileName::NotReal(_) => {
118 unimplemented!();
120 }
121 FileName::Virtual(_) | FileName::Local(_) => self.register_file(filename, span),
122 };
123
124 let convert_loc = |pos: rustc_span::BytePos| -> Loc {
125 let loc = smap.lookup_char_pos(pos);
126 Loc {
127 line: loc.line,
128 col: loc.col_display,
129 }
130 };
131 let beg = convert_loc(span.lo());
132 let end = convert_loc(span.hi());
133
134 meta::SpanData { file_id, beg, end }
136 }
137
138 pub fn translate_span_from_source_info(
140 &mut self,
141 source_scopes: &rustc_index::IndexVec<mir::SourceScope, mir::SourceScopeData>,
142 source_info: &mir::SourceInfo,
143 ) -> Span {
144 let data = self.translate_span_data(source_info.span);
146
147 let mut parent_span = None;
149 let mut scope_data = &source_scopes[source_info.scope];
150 while let Some(parent_scope) = scope_data.inlined_parent_scope {
151 scope_data = &source_scopes[parent_scope];
152 parent_span = Some(scope_data.span);
153 }
154
155 if let Some(parent_span) = parent_span {
156 let parent_span = self.translate_span_data(parent_span);
157 Span {
158 data: parent_span,
159 generated_from_span: Some(data),
160 }
161 } else {
162 Span {
163 data,
164 generated_from_span: None,
165 }
166 }
167 }
168
169 pub(crate) fn translate_span(&mut self, span: &rustc_span::Span) -> Span {
170 Span {
171 data: self.translate_span_data(*span),
172 generated_from_span: None,
173 }
174 }
175
176 pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
177 let span = def_id.def_span(&self.hax_state);
178 self.translate_span(&span)
179 }
180}
181
182impl<'tcx, 'ctx> TranslateCtx<'tcx> {
184 fn path_elem_for_def(
185 &mut self,
186 span: Span,
187 item: &RustcItem,
188 ) -> Result<Option<PathElem>, Error> {
189 let def_id = item.def_id();
190 let path_elem = def_id.path_item(&self.hax_state);
191 let disambiguator = Disambiguator::new(path_elem.disambiguator as usize);
194 let path_elem = match path_elem.data {
196 DefPathItem::CrateRoot { name, .. } => {
197 error_assert!(self, span, path_elem.disambiguator == 0);
199 Some(PathElem::Ident(name.to_string(), disambiguator))
200 }
201 DefPathItem::TypeNs(symbol)
204 | DefPathItem::ValueNs(symbol)
205 | DefPathItem::MacroNs(symbol) => {
206 Some(PathElem::Ident(symbol.to_string(), disambiguator))
207 }
208 DefPathItem::Impl => {
209 let full_def = self.hax_def_for_item(item)?;
210 let impl_elem = match full_def.kind() {
214 hax::FullDefKind::InherentImpl { ty, .. } => {
216 let item_src =
220 TransItemSource::new(item.clone(), TransItemSourceKind::InherentImpl);
221 let mut bt_ctx = ItemTransCtx::new(item_src, None, self);
222 bt_ctx.translate_item_generics(
223 span,
224 &full_def,
225 &TransItemSourceKind::InherentImpl,
226 )?;
227 let ty = bt_ctx.translate_ty(span, &ty)?;
228 ImplElem::Ty(Binder {
229 kind: BinderKind::InherentImplBlock,
230 params: bt_ctx.into_generics(),
231 skip_binder: ty,
232 })
233 }
234 hax::FullDefKind::TraitImpl { .. } => {
236 let impl_id = {
237 let item_src = TransItemSource::new(
238 item.clone(),
239 TransItemSourceKind::TraitImpl(TraitImplSource::Normal),
240 );
241 self.register_and_enqueue(&None, item_src).unwrap()
242 };
243 ImplElem::Trait(impl_id)
244 }
245 _ => unreachable!(),
246 };
247
248 Some(PathElem::Impl(impl_elem))
249 }
250 DefPathItem::OpaqueTy => None,
252 DefPathItem::Closure => Some(PathElem::Ident("closure".to_string(), disambiguator)),
256 DefPathItem::ForeignMod => None,
259 DefPathItem::Ctor => None,
262 DefPathItem::Use => Some(PathElem::Ident("{use}".to_string(), disambiguator)),
263 DefPathItem::AnonConst => Some(PathElem::Ident("{const}".to_string(), disambiguator)),
264 DefPathItem::PromotedConst => Some(PathElem::Ident(
265 "{promoted_const}".to_string(),
266 disambiguator,
267 )),
268 _ => {
269 raise_error!(
270 self,
271 span,
272 "Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}"
273 );
274 }
275 };
276 Ok(path_elem)
277 }
278
279 fn name_for_item(&mut self, item: &RustcItem) -> Result<Name, Error> {
323 if let Some(name) = self.cached_names.get(item) {
324 return Ok(name.clone());
325 }
326 let def_id = item.def_id();
327 trace!("Computing name for `{def_id:?}`");
328
329 let parent_name = if let Some(parent_id) = def_id.parent(&self.hax_state) {
330 let def = self.hax_def_for_item(item)?;
331 if matches!(item, RustcItem::Mono(..))
332 && let Some(parent_item) = def.typing_parent(&self.hax_state)
333 {
334 self.name_for_item(&RustcItem::Mono(parent_item.clone()))?
335 } else {
336 self.name_for_item(&RustcItem::Poly(parent_id.clone()))?
337 }
338 } else {
339 Name { name: Vec::new() }
340 };
341 let span = self.def_span(def_id);
342 let mut name = parent_name;
343 if let Some(path_elem) = self.path_elem_for_def(span, item)? {
344 name.name.push(path_elem);
345 }
346
347 trace!("Computed name for `{def_id:?}`: `{name:?}`");
348 self.cached_names.insert(item.clone(), name.clone());
349 Ok(name)
350 }
351
352 pub fn name_for_src(&mut self, src: &TransItemSource) -> Result<Name, Error> {
355 let mut name = if let Some(parent) = src.parent() {
356 self.name_for_src(&parent)?
357 } else {
358 self.name_for_item(&src.item)?
359 };
360 match &src.kind {
361 TransItemSourceKind::Type
363 | TransItemSourceKind::Fun
364 | TransItemSourceKind::Global
365 | TransItemSourceKind::TraitImpl(TraitImplSource::Normal)
366 | TransItemSourceKind::TraitDecl
367 | TransItemSourceKind::InherentImpl
368 | TransItemSourceKind::Module => {}
369
370 TransItemSourceKind::TraitImpl(
371 kind @ (TraitImplSource::Closure(..)
372 | TraitImplSource::ImplicitDestruct
373 | TraitImplSource::TraitAlias),
374 ) => {
375 if let TraitImplSource::Closure(..) = kind {
376 let _ = name.name.pop(); }
378 let impl_id = self.register_and_enqueue(&None, src.clone()).unwrap();
379 name.name.push(PathElem::Impl(ImplElem::Trait(impl_id)));
380 }
381 TransItemSourceKind::DefaultedMethod(_, method_name) => {
382 name.name.push(PathElem::Ident(
383 method_name.to_string(),
384 Disambiguator::ZERO,
385 ));
386 }
387 TransItemSourceKind::ClosureMethod(kind) => {
388 let fn_name = kind.method_name().to_string();
389 name.name
390 .push(PathElem::Ident(fn_name, Disambiguator::ZERO));
391 }
392 TransItemSourceKind::DropInPlaceMethod(..) => {
393 name.name.push(PathElem::Ident(
394 "drop_in_place".to_string(),
395 Disambiguator::ZERO,
396 ));
397 }
398 TransItemSourceKind::ClosureAsFnCast => {
399 name.name
400 .push(PathElem::Ident("as_fn".into(), Disambiguator::ZERO));
401 }
402 TransItemSourceKind::VTable
403 | TransItemSourceKind::VTableInstance(..)
404 | TransItemSourceKind::VTableInstanceInitializer(..) => {
405 name.name
406 .push(PathElem::Ident("{vtable}".into(), Disambiguator::ZERO));
407 }
408 TransItemSourceKind::VTableMethod => {
409 name.name.push(PathElem::Ident(
410 "{vtable_method}".into(),
411 Disambiguator::ZERO,
412 ));
413 }
414 TransItemSourceKind::VTableDropShim => {
415 name.name.push(PathElem::Ident(
416 "{vtable_drop_shim}".into(),
417 Disambiguator::ZERO,
418 ));
419 }
420 }
421 Ok(name)
422 }
423
424 pub fn translate_name(&mut self, src: &TransItemSource) -> Result<Name, Error> {
426 let mut name = self.name_for_src(src)?;
427 if let RustcItem::Mono(item_ref) = &src.item
429 && !item_ref.generic_args.is_empty()
430 {
431 let trans_id = self.register_no_enqueue(&None, src).unwrap();
432 let span = self.def_span(&item_ref.def_id);
433 let mut bt_ctx = ItemTransCtx::new(src.clone(), trans_id, self);
434 bt_ctx.binding_levels.push(BindingLevel::new(true));
435 let args = bt_ctx.translate_generic_args(
436 span,
437 &item_ref.generic_args,
438 &item_ref.impl_exprs,
439 )?;
440 name.name.push(PathElem::Instantiated(Box::new(Binder {
441 params: GenericParams::empty(),
442 skip_binder: args,
443 kind: BinderKind::Other,
444 })));
445 }
446 Ok(name)
447 }
448
449 pub(crate) fn translate_trait_item_name(
451 &mut self,
452 def_id: &hax::DefId,
453 ) -> Result<TraitItemName, Error> {
454 let def = self.poly_hax_def(def_id)?;
455 let assoc = match def.kind() {
456 hax::FullDefKind::AssocTy {
457 associated_item, ..
458 }
459 | hax::FullDefKind::AssocConst {
460 associated_item, ..
461 }
462 | hax::FullDefKind::AssocFn {
463 associated_item, ..
464 } => associated_item,
465 _ => panic!("Unexpected def for associated item: {def:?}"),
466 };
467 Ok(TraitItemName(
468 assoc
469 .name
470 .as_ref()
471 .map(|n| n.to_string().into())
472 .unwrap_or_default(),
473 ))
474 }
475
476 pub(crate) fn opacity_for_name(&self, name: &Name) -> ItemOpacity {
477 self.options.opacity_for_name(&self.translated, name)
478 }
479}
480
481impl<'tcx, 'ctx> TranslateCtx<'tcx> {
483 fn parse_attr_from_raw(
485 &mut self,
486 def_id: &hax::DefId,
487 raw_attr: RawAttribute,
488 ) -> Result<Attribute, String> {
489 let path = raw_attr.path.split("::").collect_vec();
492 let attr_name = if let &[path_start, attr_name] = path.as_slice()
493 && (path_start == "charon" || path_start == "aeneas" || path_start == "verify")
494 {
495 attr_name
496 } else {
497 return Ok(Attribute::Unknown(raw_attr));
498 };
499
500 match self.parse_special_attr(def_id, attr_name, &raw_attr)? {
501 Some(parsed) => Ok(parsed),
502 None => Err(format!(
503 "Unrecognized attribute: `{}`",
504 raw_attr.to_string()
505 )),
506 }
507 }
508
509 fn parse_special_attr(
511 &mut self,
512 def_id: &hax::DefId,
513 attr_name: &str,
514 raw_attr: &RawAttribute,
515 ) -> Result<Option<Attribute>, String> {
516 let args = raw_attr.args.as_deref();
517 let parsed = match attr_name {
518 "opaque" if args.is_none() => Attribute::Opaque,
520 "exclude" if args.is_none() => Attribute::Exclude,
522 "rename" if let Some(attr) = args => {
524 let Some(attr) = attr
525 .strip_prefix("\"")
526 .and_then(|attr| attr.strip_suffix("\""))
527 else {
528 return Err(format!(
529 "the new name should be between quotes: `rename(\"{attr}\")`."
530 ));
531 };
532
533 if attr.is_empty() {
534 return Err(format!("attribute `rename` should not be empty"));
535 }
536
537 let first_char = attr.chars().nth(0).unwrap();
538 let is_identifier = (first_char.is_alphabetic() || first_char == '_')
539 && attr.chars().all(|c| c.is_alphanumeric() || c == '_');
540 if !is_identifier {
541 return Err(format!(
542 "attribute `rename` should contain a valid identifier"
543 ));
544 }
545
546 Attribute::Rename(attr.to_string())
547 }
548 "variants_prefix" if let Some(attr) = args => {
550 let Some(attr) = attr
551 .strip_prefix("\"")
552 .and_then(|attr| attr.strip_suffix("\""))
553 else {
554 return Err(format!(
555 "the name should be between quotes: `variants_prefix(\"{attr}\")`."
556 ));
557 };
558
559 Attribute::VariantsPrefix(attr.to_string())
560 }
561 "variants_suffix" if let Some(attr) = args => {
563 let Some(attr) = attr
564 .strip_prefix("\"")
565 .and_then(|attr| attr.strip_suffix("\""))
566 else {
567 return Err(format!(
568 "the name should be between quotes: `variants_suffix(\"{attr}\")`."
569 ));
570 };
571
572 Attribute::VariantsSuffix(attr.to_string())
573 }
574 "start_from" => {
576 if matches!(def_id.kind, hax::DefKind::Mod) {
577 return Err(format!("`start_from` on modules has no effect"));
578 }
579 Attribute::Unknown(raw_attr.clone())
580 }
581 "test" if args.is_none() => Attribute::Unknown(raw_attr.clone()),
583 _ => return Ok(None),
584 };
585 Ok(Some(parsed))
586 }
587
588 pub(crate) fn translate_attribute(
591 &mut self,
592 def_id: &hax::DefId,
593 attr: &rustc_hir::Attribute,
594 ) -> Option<Attribute> {
595 use rustc_hir as hir;
596 use rustc_hir::attrs as hir_attrs;
597 match attr {
598 hir::Attribute::Parsed(hir_attrs::AttributeKind::DocComment { comment, .. }) => {
599 Some(Attribute::DocComment(comment.to_string()))
600 }
601 hir::Attribute::Parsed(_) => None,
602 hir::Attribute::Unparsed(attr) => {
603 let raw_attr = RawAttribute {
604 path: attr.path.to_string(),
605 args: match &attr.args {
606 hir::AttrArgs::Empty => None,
607 hir::AttrArgs::Delimited(args) => {
608 Some(rustc_ast_pretty::pprust::tts_to_string(&args.tokens))
609 }
610 hir::AttrArgs::Eq { expr, .. } => {
611 self.tcx.sess.source_map().span_to_snippet(expr.span).ok()
612 }
613 },
614 };
615 match self.parse_attr_from_raw(def_id, raw_attr) {
616 Ok(a) => Some(a),
617 Err(msg) => {
618 let span = self.translate_span(&attr.span.sinto(&self.hax_state));
619 register_error!(self, span, "Error parsing attribute: {msg}");
620 None
621 }
622 }
623 }
624 }
625 }
626
627 pub(crate) fn translate_inline(&self, def: &hax::FullDef) -> Option<InlineAttr> {
628 match def.kind() {
629 hax::FullDefKind::Fn { inline, .. }
630 | hax::FullDefKind::AssocFn { inline, .. }
631 | hax::FullDefKind::Closure { inline, .. } => match inline {
632 hax::InlineAttr::None => None,
633 hax::InlineAttr::Hint => Some(InlineAttr::Hint),
634 hax::InlineAttr::Never => Some(InlineAttr::Never),
635 hax::InlineAttr::Always => Some(InlineAttr::Always),
636 hax::InlineAttr::Force { .. } => Some(InlineAttr::Always),
637 },
638 _ => None,
639 }
640 }
641
642 pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef) -> AttrInfo {
643 let public = def.visibility.unwrap_or(false);
645 let inline = self.translate_inline(def);
646 let attributes = def
647 .attributes
648 .iter()
649 .filter_map(|attr| self.translate_attribute(def.def_id(), &attr))
650 .collect_vec();
651
652 let rename = {
653 let mut renames = attributes.iter().filter_map(|a| a.as_rename()).cloned();
654 let rename = renames.next();
655 if renames.next().is_some() {
656 let span = self.translate_span(&def.span);
657 register_error!(
658 self,
659 span,
660 "There should be at most one `charon::rename(\"...\")` \
661 or `aeneas::rename(\"...\")` attribute per declaration",
662 );
663 }
664 rename
665 };
666
667 AttrInfo {
668 attributes,
669 inline,
670 public,
671 rename,
672 }
673 }
674}
675
676impl<'tcx, 'ctx> TranslateCtx<'tcx> {
678 pub(crate) fn is_extern_item(&mut self, def: &hax::FullDef) -> bool {
680 def.def_id()
681 .parent(&self.hax_state)
682 .is_some_and(|parent| matches!(parent.kind, hax::DefKind::ForeignMod { .. }))
683 }
684
685 pub(crate) fn translate_item_meta(
687 &mut self,
688 def: &hax::FullDef,
689 item_src: &TransItemSource,
690 name: Name,
691 name_opacity: ItemOpacity,
692 ) -> ItemMeta {
693 if let Some(item_meta) = self.cached_item_metas.get(&item_src) {
694 return item_meta.clone();
695 }
696 let span = def.source_span.as_ref().unwrap_or(&def.span);
697 let span = self.translate_span(span);
698 let is_local = def.def_id().is_local();
699 let (attr_info, lang_item) = if !item_src.is_derived_item()
700 || matches!(item_src.kind, TransItemSourceKind::ClosureMethod(..))
701 {
702 let attr_info = self.translate_attr_info(def);
703 let lang_item = def
704 .lang_item
705 .clone()
706 .or_else(|| def.diagnostic_item.clone())
707 .map(|s| s.to_string());
708 (attr_info, lang_item)
709 } else {
710 (AttrInfo::default(), None)
711 };
712
713 let opacity = if attr_info.attributes.iter().any(|attr| attr.is_exclude()) {
714 ItemOpacity::Invisible.max(name_opacity)
715 } else if self.is_extern_item(def)
716 || attr_info.attributes.iter().any(|attr| attr.is_opaque())
717 {
718 ItemOpacity::Opaque.max(name_opacity)
720 } else {
721 name_opacity
722 };
723
724 let item_meta = ItemMeta {
725 name,
726 span,
727 source_text: def.source_text.clone(),
728 attr_info,
729 is_local,
730 opacity,
731 lang_item,
732 };
733 self.cached_item_metas
734 .insert(item_src.clone(), item_meta.clone());
735 item_meta
736 }
737}