1use crate::translate::translate_crate::RustcItem;
3use crate::translate::translate_generics::BindingLevel;
4
5use super::translate_crate::{TransItemSource, TransItemSourceKind};
6use super::translate_ctx::{ItemTransCtx, TranslateCtx};
7use charon_lib::ast::*;
8use hax_frontend_exporter::{self as hax, DefPathItem};
9use itertools::Itertools;
10use std::cmp::Ord;
11use std::path::{Component, PathBuf};
12
13impl<'tcx, 'ctx> TranslateCtx<'tcx> {
15 fn register_file(&mut self, filename: FileName, span: rustc_span::Span) -> FileId {
18 match self.file_to_id.get(&filename) {
20 Some(id) => *id,
21 None => {
22 let source_file = self.tcx.sess.source_map().lookup_source_file(span.lo());
23 let crate_name = self.tcx.crate_name(source_file.cnum).to_string();
24 let file = File {
25 name: filename.clone(),
26 crate_name,
27 contents: source_file.src.as_deref().cloned(),
28 };
29 let id = self.translated.files.push(file);
30 self.file_to_id.insert(filename, id);
31 id
32 }
33 }
34 }
35
36 pub fn translate_filename(&mut self, name: &hax::FileName) -> meta::FileName {
37 match name {
38 hax::FileName::Real(name) => {
39 use hax::RealFileName;
40 match name {
41 RealFileName::LocalPath(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 path.clone()
59 };
60 FileName::Local(path)
61 }
62 RealFileName::Remapped { virtual_name, .. } => {
63 let mut components_iter = virtual_name.components();
67 if let Some(
68 [
69 Component::RootDir,
70 Component::Normal(rustc),
71 Component::Normal(hash),
72 ],
73 ) = components_iter.by_ref().array_chunks().next()
74 && rustc.to_str() == Some("rustc")
75 && hash.len() == 40
76 {
77 let path_without_hash = [Component::RootDir, Component::Normal(rustc)]
78 .into_iter()
79 .chain(components_iter)
80 .collect();
81 FileName::Virtual(path_without_hash)
82 } else {
83 FileName::Virtual(virtual_name.clone())
84 }
85 }
86 }
87 }
88 _ => FileName::NotReal(format!("{name:?}")),
91 }
92 }
93
94 pub fn translate_raw_span(&mut self, rspan: &hax::Span) -> meta::RawSpan {
95 let filename = self.translate_filename(&rspan.filename);
96 let rust_span = rspan.rust_span_data.unwrap().span();
97 let file_id = match &filename {
98 FileName::NotReal(_) => {
99 unimplemented!();
101 }
102 FileName::Virtual(_) | FileName::Local(_) => self.register_file(filename, rust_span),
103 };
104
105 fn convert_loc(loc: &hax::Loc) -> Loc {
106 Loc {
107 line: loc.line,
108 col: loc.col,
109 }
110 }
111 let beg = convert_loc(&rspan.lo);
112 let end = convert_loc(&rspan.hi);
113
114 meta::RawSpan { file_id, beg, end }
116 }
117
118 pub fn translate_span_from_source_info(
120 &mut self,
121 source_scopes: &hax::IndexVec<hax::SourceScope, hax::SourceScopeData>,
122 source_info: &hax::SourceInfo,
123 ) -> Span {
124 let span = self.translate_raw_span(&source_info.span);
126
127 let mut parent_span = None;
129 let mut scope_data = &source_scopes[source_info.scope];
130 while let Some(parent_scope) = scope_data.inlined_parent_scope {
131 scope_data = &source_scopes[parent_scope];
132 parent_span = Some(&scope_data.span);
133 }
134
135 if let Some(parent_span) = parent_span {
136 let parent_span = self.translate_raw_span(parent_span);
137 Span {
138 span: parent_span,
139 generated_from_span: Some(span),
140 }
141 } else {
142 Span {
143 span,
144 generated_from_span: None,
145 }
146 }
147 }
148
149 pub(crate) fn translate_span_from_hax(&mut self, span: &hax::Span) -> Span {
150 Span {
151 span: self.translate_raw_span(span),
152 generated_from_span: None,
153 }
154 }
155
156 pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
157 let span = def_id.def_span(&self.hax_state);
158 self.translate_span_from_hax(&span)
159 }
160}
161
162impl<'tcx, 'ctx> TranslateCtx<'tcx> {
164 fn path_elem_for_def(
165 &mut self,
166 span: Span,
167 item: &RustcItem,
168 ) -> Result<Option<PathElem>, Error> {
169 let def_id = item.def_id();
170 let path_elem = def_id.path_item();
171 let disambiguator = Disambiguator::new(path_elem.disambiguator as usize);
174 let path_elem = match path_elem.data {
176 DefPathItem::CrateRoot { name, .. } => {
177 error_assert!(self, span, path_elem.disambiguator == 0);
179 Some(PathElem::Ident(name.clone(), disambiguator))
180 }
181 DefPathItem::TypeNs(symbol)
184 | DefPathItem::ValueNs(symbol)
185 | DefPathItem::MacroNs(symbol) => Some(PathElem::Ident(symbol, disambiguator)),
186 DefPathItem::Impl => {
187 let full_def = self.hax_def_for_item(item)?;
188 let impl_elem = match full_def.kind() {
192 hax::FullDefKind::InherentImpl { ty, .. } => {
194 let mut bt_ctx = ItemTransCtx::new(
198 TransItemSource::new(item.clone(), TransItemSourceKind::InherentImpl),
199 None,
200 self,
201 );
202 bt_ctx.translate_def_generics(span, &full_def)?;
203 let ty = bt_ctx.translate_ty(span, &ty)?;
204 ImplElem::Ty(Binder {
205 kind: BinderKind::InherentImplBlock,
206 params: bt_ctx.into_generics(),
207 skip_binder: ty,
208 })
209 }
210 hax::FullDefKind::TraitImpl { .. } => {
212 let impl_id = {
213 let item_src =
214 TransItemSource::new(item.clone(), TransItemSourceKind::TraitImpl);
215 self.register_and_enqueue(&None, item_src).unwrap()
216 };
217 ImplElem::Trait(impl_id)
218 }
219 _ => unreachable!(),
220 };
221
222 Some(PathElem::Impl(impl_elem))
223 }
224 DefPathItem::OpaqueTy => None,
226 DefPathItem::Closure => Some(PathElem::Ident("closure".to_string(), disambiguator)),
230 DefPathItem::ForeignMod => None,
233 DefPathItem::Ctor => None,
236 DefPathItem::Use => Some(PathElem::Ident("{use}".to_string(), disambiguator)),
237 DefPathItem::AnonConst => Some(PathElem::Ident("{const}".to_string(), disambiguator)),
238 DefPathItem::PromotedConst => Some(PathElem::Ident(
239 "{promoted_const}".to_string(),
240 disambiguator,
241 )),
242 _ => {
243 raise_error!(
244 self,
245 span,
246 "Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}"
247 );
248 }
249 };
250 Ok(path_elem)
251 }
252
253 fn name_for_item(&mut self, item: &RustcItem) -> Result<Name, Error> {
297 if let Some(name) = self.cached_names.get(item) {
298 return Ok(name.clone());
299 }
300 let def_id = item.def_id();
301 trace!("Computing name for `{def_id:?}`");
302
303 let parent_name = if let Some(parent_id) = &def_id.parent {
304 let def = self.hax_def_for_item(item)?;
305 if matches!(item, RustcItem::Mono(..))
306 && let Some(parent_item) = def.typing_parent(&self.hax_state)
307 {
308 self.name_for_item(&RustcItem::Mono(parent_item.clone()))?
309 } else {
310 self.name_for_item(&RustcItem::Poly(parent_id.clone()))?
311 }
312 } else {
313 Name { name: Vec::new() }
314 };
315 let span = self.def_span(def_id);
316 let mut name = parent_name;
317 if let Some(path_elem) = self.path_elem_for_def(span, item)? {
318 name.name.push(path_elem);
319 }
320
321 trace!("Computed name for `{def_id:?}`: `{name:?}`");
322 self.cached_names.insert(item.clone(), name.clone());
323 Ok(name)
324 }
325
326 pub fn name_for_src(&mut self, src: &TransItemSource) -> Result<Name, Error> {
329 let def_id = src.def_id();
330 let mut name = if let Some(parent) = src.parent() {
331 self.name_for_src(&parent)?
332 } else {
333 self.name_for_item(&src.item)?
334 };
335 match src.kind {
336 TransItemSourceKind::ClosureTraitImpl(..) | TransItemSourceKind::DropGlueImpl => {
337 if let TransItemSourceKind::ClosureTraitImpl(_) = src.kind {
338 let _ = name.name.pop(); }
340 let impl_id = self.register_and_enqueue(&None, src.clone()).unwrap();
341 name.name.push(PathElem::Impl(ImplElem::Trait(impl_id)));
342 }
343 TransItemSourceKind::ClosureMethod(kind) => {
344 let fn_name = kind.method_name().to_string();
345 name.name
346 .push(PathElem::Ident(fn_name, Disambiguator::ZERO));
347 }
348 TransItemSourceKind::DropGlueMethod => {
349 let fn_name = "drop".to_string();
350 name.name
351 .push(PathElem::Ident(fn_name, Disambiguator::ZERO));
352 }
353 TransItemSourceKind::TraitImpl if matches!(def_id.kind, hax::DefKind::TraitAlias) => {
354 let impl_id = self.register_and_enqueue(&None, src.clone()).unwrap();
355 name.name.push(PathElem::Impl(ImplElem::Trait(impl_id)));
356 }
357 TransItemSourceKind::ClosureAsFnCast => {
358 name.name
359 .push(PathElem::Ident("as_fn".into(), Disambiguator::ZERO));
360 }
361 _ => {}
362 }
363 Ok(name)
364 }
365
366 pub fn translate_name(&mut self, src: &TransItemSource) -> Result<Name, Error> {
368 let mut name = self.name_for_src(src)?;
369 if let RustcItem::Mono(item_ref) = &src.item
371 && !item_ref.generic_args.is_empty()
372 {
373 let trans_id = self.register_and_enqueue(&None, src.clone()).unwrap();
374 let span = self.def_span(&item_ref.def_id);
375 let mut bt_ctx = ItemTransCtx::new(src.clone(), trans_id, self);
376 bt_ctx.binding_levels.push(BindingLevel::new(true));
377 let args = bt_ctx.translate_generic_args(
378 span,
379 &item_ref.generic_args,
380 &item_ref.impl_exprs,
381 )?;
382 name.name.push(PathElem::Monomorphized(Box::new(args)));
383 }
384 Ok(name)
385 }
386
387 pub(crate) fn translate_trait_item_name(
389 &mut self,
390 def_id: &hax::DefId,
391 ) -> Result<TraitItemName, Error> {
392 let def = self.poly_hax_def(def_id)?;
393 let assoc = match def.kind() {
394 hax::FullDefKind::AssocTy {
395 associated_item, ..
396 }
397 | hax::FullDefKind::AssocConst {
398 associated_item, ..
399 }
400 | hax::FullDefKind::AssocFn {
401 associated_item, ..
402 } => associated_item,
403 _ => panic!("Unexpected def for associated item: {def:?}"),
404 };
405 Ok(TraitItemName(assoc.name.clone().unwrap_or_default()))
406 }
407
408 pub(crate) fn opacity_for_name(&self, name: &Name) -> ItemOpacity {
409 self.options.opacity_for_name(&self.translated, name)
410 }
411}
412
413impl<'tcx, 'ctx> TranslateCtx<'tcx> {
415 pub(crate) fn translate_attribute(&mut self, attr: &hax::Attribute) -> Option<Attribute> {
418 use hax::Attribute as Haxttribute;
419 use hax::AttributeKind as HaxttributeKind;
420 match attr {
421 Haxttribute::Parsed(HaxttributeKind::DocComment { comment, .. }) => {
422 Some(Attribute::DocComment(comment.to_string()))
423 }
424 Haxttribute::Parsed(_) => None,
425 Haxttribute::Unparsed(attr) => {
426 let raw_attr = RawAttribute {
427 path: attr.path.clone(),
428 args: match &attr.args {
429 hax::AttrArgs::Empty => None,
430 hax::AttrArgs::Delimited(args) => Some(args.tokens.clone()),
431 hax::AttrArgs::Eq { expr, .. } => self
432 .tcx
433 .sess
434 .source_map()
435 .span_to_snippet(expr.span.rust_span_data.unwrap().span())
436 .ok(),
437 },
438 };
439 match Attribute::parse_from_raw(raw_attr) {
440 Ok(a) => Some(a),
441 Err(msg) => {
442 let span = self.translate_span_from_hax(&attr.span);
443 register_error!(self, span, "Error parsing attribute: {msg}");
444 None
445 }
446 }
447 }
448 }
449 }
450
451 pub(crate) fn translate_inline(&self, def: &hax::FullDef) -> Option<InlineAttr> {
452 match def.kind() {
453 hax::FullDefKind::Fn { inline, .. } | hax::FullDefKind::AssocFn { inline, .. } => {
454 match inline {
455 hax::InlineAttr::None => None,
456 hax::InlineAttr::Hint => Some(InlineAttr::Hint),
457 hax::InlineAttr::Never => Some(InlineAttr::Never),
458 hax::InlineAttr::Always => Some(InlineAttr::Always),
459 hax::InlineAttr::Force { .. } => Some(InlineAttr::Always),
460 }
461 }
462 _ => None,
463 }
464 }
465
466 pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef) -> AttrInfo {
467 let public = def.visibility.unwrap_or(false);
469 let inline = self.translate_inline(def);
470 let attributes = def
471 .attributes
472 .iter()
473 .filter_map(|attr| self.translate_attribute(&attr))
474 .collect_vec();
475
476 let rename = {
477 let mut renames = attributes.iter().filter_map(|a| a.as_rename()).cloned();
478 let rename = renames.next();
479 if renames.next().is_some() {
480 let span = self.translate_span_from_hax(&def.span);
481 register_error!(
482 self,
483 span,
484 "There should be at most one `charon::rename(\"...\")` \
485 or `aeneas::rename(\"...\")` attribute per declaration",
486 );
487 }
488 rename
489 };
490
491 AttrInfo {
492 attributes,
493 inline,
494 public,
495 rename,
496 }
497 }
498}
499
500impl<'tcx, 'ctx> TranslateCtx<'tcx> {
502 pub(crate) fn is_extern_item(&mut self, def: &hax::FullDef) -> bool {
504 def.def_id()
505 .parent
506 .as_ref()
507 .is_some_and(|parent| matches!(parent.kind, hax::DefKind::ForeignMod { .. }))
508 }
509
510 pub(crate) fn translate_item_meta(
512 &mut self,
513 def: &hax::FullDef,
514 item_src: &TransItemSource,
515 name: Name,
516 name_opacity: ItemOpacity,
517 ) -> ItemMeta {
518 if let Some(item_meta) = self.cached_item_metas.get(&item_src) {
519 return item_meta.clone();
520 }
521 let span = def.source_span.as_ref().unwrap_or(&def.span);
522 let span = self.translate_span_from_hax(span);
523 let is_local = def.def_id().is_local;
524 let (attr_info, lang_item) = if item_src.is_derived_item() {
525 (AttrInfo::default(), None)
526 } else {
527 let attr_info = self.translate_attr_info(def);
528 let lang_item = def
529 .lang_item
530 .clone()
531 .or_else(|| def.diagnostic_item.clone());
532 (attr_info, lang_item)
533 };
534
535 let opacity = if self.is_extern_item(def)
536 || attr_info.attributes.iter().any(|attr| attr.is_opaque())
537 {
538 ItemOpacity::Opaque.max(name_opacity)
540 } else {
541 name_opacity
542 };
543
544 let item_meta = ItemMeta {
545 name,
546 span,
547 source_text: def.source_text.clone(),
548 attr_info,
549 is_local,
550 opacity,
551 lang_item,
552 };
553 self.cached_item_metas
554 .insert(item_src.clone(), item_meta.clone());
555 item_meta
556 }
557}
558
559impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
560 pub(crate) fn translate_span_from_hax(&mut self, rspan: &hax::Span) -> Span {
561 self.t_ctx.translate_span_from_hax(rspan)
562 }
563
564 pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
565 self.t_ctx.def_span(def_id)
566 }
567}