1use super::translate_crate::{TransItemSource, TransItemSourceKind};
3use super::translate_ctx::{ItemTransCtx, TranslateCtx};
4use charon_lib::ast::*;
5use hax_frontend_exporter::{self as hax, DefPathItem};
6use itertools::Itertools;
7use std::cmp::Ord;
8use std::path::{Component, PathBuf};
9
10impl<'tcx, 'ctx> TranslateCtx<'tcx> {
12 fn register_file(&mut self, filename: FileName, span: rustc_span::Span) -> FileId {
15 match self.file_to_id.get(&filename) {
17 Some(id) => *id,
18 None => {
19 let source_file = self.tcx.sess.source_map().lookup_source_file(span.lo());
20 let crate_name = self.tcx.crate_name(source_file.cnum).to_string();
21 let file = File {
22 name: filename.clone(),
23 crate_name,
24 contents: source_file.src.as_deref().cloned(),
25 };
26 let id = self.translated.files.push(file);
27 self.file_to_id.insert(filename, id);
28 id
29 }
30 }
31 }
32
33 pub fn translate_filename(&mut self, name: &hax::FileName) -> meta::FileName {
34 match name {
35 hax::FileName::Real(name) => {
36 use hax::RealFileName;
37 match name {
38 RealFileName::LocalPath(path) => {
39 let path = if let Ok(path) = path.strip_prefix(&self.sysroot) {
40 if let Ok(path) = path.strip_prefix("lib/rustlib/src/rust") {
45 let mut rewritten_path: PathBuf = "/rustc".into();
46 rewritten_path.extend(path);
47 rewritten_path
48 } else {
49 let mut rewritten_path: PathBuf = "/toolchain".into();
51 rewritten_path.extend(path);
52 rewritten_path
53 }
54 } else {
55 path.clone()
56 };
57 FileName::Local(path)
58 }
59 RealFileName::Remapped { virtual_name, .. } => {
60 let mut components_iter = virtual_name.components();
64 if let Some(
65 [
66 Component::RootDir,
67 Component::Normal(rustc),
68 Component::Normal(hash),
69 ],
70 ) = components_iter.by_ref().array_chunks().next()
71 && rustc.to_str() == Some("rustc")
72 && hash.len() == 40
73 {
74 let path_without_hash = [Component::RootDir, Component::Normal(rustc)]
75 .into_iter()
76 .chain(components_iter)
77 .collect();
78 FileName::Virtual(path_without_hash)
79 } else {
80 FileName::Virtual(virtual_name.clone())
81 }
82 }
83 }
84 }
85 _ => FileName::NotReal(format!("{name:?}")),
88 }
89 }
90
91 pub fn translate_raw_span(&mut self, rspan: &hax::Span) -> meta::RawSpan {
92 let filename = self.translate_filename(&rspan.filename);
93 let rust_span = rspan.rust_span_data.unwrap().span();
94 let file_id = match &filename {
95 FileName::NotReal(_) => {
96 unimplemented!();
98 }
99 FileName::Virtual(_) | FileName::Local(_) => self.register_file(filename, rust_span),
100 };
101
102 fn convert_loc(loc: &hax::Loc) -> Loc {
103 Loc {
104 line: loc.line,
105 col: loc.col,
106 }
107 }
108 let beg = convert_loc(&rspan.lo);
109 let end = convert_loc(&rspan.hi);
110
111 meta::RawSpan { file_id, beg, end }
113 }
114
115 pub fn translate_span_from_source_info(
117 &mut self,
118 source_scopes: &hax::IndexVec<hax::SourceScope, hax::SourceScopeData>,
119 source_info: &hax::SourceInfo,
120 ) -> Span {
121 let span = self.translate_raw_span(&source_info.span);
123
124 let mut parent_span = None;
126 let mut scope_data = &source_scopes[source_info.scope];
127 while let Some(parent_scope) = scope_data.inlined_parent_scope {
128 scope_data = &source_scopes[parent_scope];
129 parent_span = Some(&scope_data.span);
130 }
131
132 if let Some(parent_span) = parent_span {
133 let parent_span = self.translate_raw_span(parent_span);
134 Span {
135 span: parent_span,
136 generated_from_span: Some(span),
137 }
138 } else {
139 Span {
140 span,
141 generated_from_span: None,
142 }
143 }
144 }
145
146 pub(crate) fn translate_span_from_hax(&mut self, span: &hax::Span) -> Span {
147 Span {
148 span: self.translate_raw_span(span),
149 generated_from_span: None,
150 }
151 }
152
153 pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
154 let span = def_id.def_span(&self.hax_state);
155 self.translate_span_from_hax(&span)
156 }
157}
158
159impl<'tcx, 'ctx> TranslateCtx<'tcx> {
161 fn path_elem_for_def(
162 &mut self,
163 span: Span,
164 def_id: &hax::DefId,
165 ) -> Result<Option<PathElem>, Error> {
166 let path_elem = def_id.path_item();
167 let disambiguator = Disambiguator::new(path_elem.disambiguator as usize);
170 let path_elem = match path_elem.data {
172 DefPathItem::CrateRoot { name, .. } => {
173 error_assert!(self, span, path_elem.disambiguator == 0);
175 Some(PathElem::Ident(name.clone(), disambiguator))
176 }
177 DefPathItem::TypeNs(symbol)
180 | DefPathItem::ValueNs(symbol)
181 | DefPathItem::MacroNs(symbol) => Some(PathElem::Ident(symbol, disambiguator)),
182 DefPathItem::Impl => {
183 let full_def = self.hax_def(def_id)?;
184 let impl_elem = match full_def.kind() {
188 hax::FullDefKind::InherentImpl { ty, .. } => {
190 let mut bt_ctx = ItemTransCtx::new(
194 TransItemSource::new(def_id.clone(), TransItemSourceKind::InherentImpl),
195 None,
196 self,
197 );
198 bt_ctx.translate_def_generics(span, &full_def)?;
199 let ty = bt_ctx.translate_ty(span, &ty)?;
200 ImplElem::Ty(Binder {
201 kind: BinderKind::InherentImplBlock,
202 params: bt_ctx.into_generics(),
203 skip_binder: ty,
204 })
205 }
206 hax::FullDefKind::TraitImpl { .. } => {
208 let impl_id = self.register_trait_impl_id(&None, def_id);
209 ImplElem::Trait(impl_id)
210 }
211 _ => unreachable!(),
212 };
213
214 Some(PathElem::Impl(impl_elem))
215 }
216 DefPathItem::OpaqueTy => None,
218 DefPathItem::Closure => Some(PathElem::Ident("closure".to_string(), disambiguator)),
222 DefPathItem::ForeignMod => None,
225 DefPathItem::Ctor => None,
228 DefPathItem::Use => Some(PathElem::Ident("{use}".to_string(), disambiguator)),
229 DefPathItem::AnonConst => Some(PathElem::Ident("{const}".to_string(), disambiguator)),
230 DefPathItem::PromotedConst => Some(PathElem::Ident(
231 "{promoted_const}".to_string(),
232 disambiguator,
233 )),
234 _ => {
235 raise_error!(
236 self,
237 span,
238 "Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}"
239 );
240 }
241 };
242 Ok(path_elem)
243 }
244
245 pub fn def_id_to_name(&mut self, def_id: &hax::DefId) -> Result<Name, Error> {
289 if let Some(name) = self.cached_names.get(&def_id) {
290 return Ok(name.clone());
291 }
292 trace!("Computing name for `{def_id:?}`");
293
294 let parent_name = if let Some(parent) = &def_id.parent {
295 self.def_id_to_name(parent)?
296 } else {
297 Name { name: Vec::new() }
298 };
299 let span = self.def_span(def_id);
300 let mut name = parent_name;
301 if let Some(path_elem) = self.path_elem_for_def(span, &def_id)? {
302 name.name.push(path_elem);
303 }
304
305 trace!("Computed name for `{def_id:?}`: `{name:?}`");
306 self.cached_names.insert(def_id.clone(), name.clone());
307 Ok(name)
308 }
309
310 pub fn translate_name(&mut self, src: &TransItemSource) -> Result<Name, Error> {
312 let def_id = src.as_def_id();
313 let mut name = self.def_id_to_name(def_id)?;
314 match src.kind {
315 TransItemSourceKind::ClosureTraitImpl(..)
316 | TransItemSourceKind::ClosureMethod(..)
317 | TransItemSourceKind::DropGlueImpl
318 | TransItemSourceKind::DropGlueMethod => {
319 let impl_id = match src.kind {
320 TransItemSourceKind::ClosureTraitImpl(kind)
321 | TransItemSourceKind::ClosureMethod(kind) => {
322 let _ = name.name.pop(); self.register_closure_trait_impl_id(&None, def_id, kind)
324 }
325 TransItemSourceKind::DropGlueImpl | TransItemSourceKind::DropGlueMethod => {
326 self.register_drop_trait_impl_id(&None, def_id)
327 }
328 _ => unreachable!(),
329 };
330
331 name.name.push(PathElem::Impl(ImplElem::Trait(impl_id)));
332
333 match src.kind {
334 TransItemSourceKind::ClosureMethod(kind) => {
335 let fn_name = kind.method_name().to_string();
336 name.name
337 .push(PathElem::Ident(fn_name, Disambiguator::ZERO));
338 }
339 TransItemSourceKind::DropGlueMethod => {
340 let fn_name = "drop".to_string();
341 name.name
342 .push(PathElem::Ident(fn_name, Disambiguator::ZERO));
343 }
344 _ => {}
345 }
346 }
347 TransItemSourceKind::TraitImpl if matches!(def_id.kind, hax::DefKind::TraitAlias) => {
348 let impl_id = self.register_trait_impl_id(&None, def_id);
349 name.name.push(PathElem::Impl(ImplElem::Trait(impl_id)));
350 }
351 TransItemSourceKind::ClosureAsFnCast => {
352 name.name
353 .push(PathElem::Ident("as_fn".into(), Disambiguator::ZERO));
354 }
355 _ => {}
356 }
357 Ok(name)
358 }
359
360 pub(crate) fn translate_trait_item_name(
362 &mut self,
363 def_id: &hax::DefId,
364 ) -> Result<TraitItemName, Error> {
365 let def = self.hax_def(def_id)?;
366 let assoc = match def.kind() {
367 hax::FullDefKind::AssocTy {
368 associated_item, ..
369 }
370 | hax::FullDefKind::AssocConst {
371 associated_item, ..
372 }
373 | hax::FullDefKind::AssocFn {
374 associated_item, ..
375 } => associated_item,
376 _ => panic!("Unexpected def for associated item: {def:?}"),
377 };
378 Ok(TraitItemName(assoc.name.clone().unwrap_or_default()))
379 }
380
381 pub(crate) fn opacity_for_name(&self, name: &Name) -> ItemOpacity {
382 self.options.opacity_for_name(&self.translated, name)
383 }
384}
385
386impl<'tcx, 'ctx> TranslateCtx<'tcx> {
388 pub(crate) fn translate_attribute(&mut self, attr: &hax::Attribute) -> Option<Attribute> {
391 use hax::Attribute as Haxttribute;
392 use hax::AttributeKind as HaxttributeKind;
393 match attr {
394 Haxttribute::Parsed(HaxttributeKind::DocComment { comment, .. }) => {
395 Some(Attribute::DocComment(comment.to_string()))
396 }
397 Haxttribute::Parsed(_) => None,
398 Haxttribute::Unparsed(attr) => {
399 let raw_attr = RawAttribute {
400 path: attr.path.clone(),
401 args: match &attr.args {
402 hax::AttrArgs::Empty => None,
403 hax::AttrArgs::Delimited(args) => Some(args.tokens.clone()),
404 hax::AttrArgs::Eq { expr, .. } => self
405 .tcx
406 .sess
407 .source_map()
408 .span_to_snippet(expr.span.rust_span_data.unwrap().span())
409 .ok(),
410 },
411 };
412 match Attribute::parse_from_raw(raw_attr) {
413 Ok(a) => Some(a),
414 Err(msg) => {
415 let span = self.translate_span_from_hax(&attr.span);
416 register_error!(self, span, "Error parsing attribute: {msg}");
417 None
418 }
419 }
420 }
421 }
422 }
423
424 pub(crate) fn translate_inline(&self, def: &hax::FullDef) -> Option<InlineAttr> {
425 match def.kind() {
426 hax::FullDefKind::Fn { inline, .. } | hax::FullDefKind::AssocFn { inline, .. } => {
427 match inline {
428 hax::InlineAttr::None => None,
429 hax::InlineAttr::Hint => Some(InlineAttr::Hint),
430 hax::InlineAttr::Never => Some(InlineAttr::Never),
431 hax::InlineAttr::Always => Some(InlineAttr::Always),
432 hax::InlineAttr::Force { .. } => Some(InlineAttr::Always),
433 }
434 }
435 _ => None,
436 }
437 }
438
439 pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef) -> AttrInfo {
440 let public = def.visibility.unwrap_or(false);
442 let inline = self.translate_inline(def);
443 let attributes = def
444 .attributes
445 .iter()
446 .filter_map(|attr| self.translate_attribute(&attr))
447 .collect_vec();
448
449 let rename = {
450 let mut renames = attributes.iter().filter_map(|a| a.as_rename()).cloned();
451 let rename = renames.next();
452 if renames.next().is_some() {
453 let span = self.translate_span_from_hax(&def.span);
454 register_error!(
455 self,
456 span,
457 "There should be at most one `charon::rename(\"...\")` \
458 or `aeneas::rename(\"...\")` attribute per declaration",
459 );
460 }
461 rename
462 };
463
464 AttrInfo {
465 attributes,
466 inline,
467 public,
468 rename,
469 }
470 }
471}
472
473impl<'tcx, 'ctx> TranslateCtx<'tcx> {
475 pub(crate) fn is_extern_item(&mut self, def: &hax::FullDef) -> bool {
477 def.def_id().parent.as_ref().is_some_and(|parent| {
478 self.hax_def(parent).is_ok_and(|parent_def| {
479 matches!(parent_def.kind(), hax::FullDefKind::ForeignMod { .. })
480 })
481 })
482 }
483
484 pub(crate) fn translate_item_meta(
486 &mut self,
487 def: &hax::FullDef,
488 item_src: &TransItemSource,
489 name: Name,
490 name_opacity: ItemOpacity,
491 ) -> ItemMeta {
492 if let Some(item_meta) = self.cached_item_metas.get(&item_src) {
493 return item_meta.clone();
494 }
495 let span = def.source_span.as_ref().unwrap_or(&def.span);
496 let span = self.translate_span_from_hax(span);
497 let is_local = def.def_id.is_local;
498 let (attr_info, lang_item) = if item_src.is_derived_item() {
499 (AttrInfo::default(), None)
500 } else {
501 let attr_info = self.translate_attr_info(def);
502 let lang_item = def
503 .lang_item
504 .clone()
505 .or_else(|| def.diagnostic_item.clone());
506 (attr_info, lang_item)
507 };
508
509 let opacity = if self.is_extern_item(def)
510 || attr_info.attributes.iter().any(|attr| attr.is_opaque())
511 {
512 ItemOpacity::Opaque.max(name_opacity)
514 } else {
515 name_opacity
516 };
517
518 let item_meta = ItemMeta {
519 name,
520 span,
521 source_text: def.source_text.clone(),
522 attr_info,
523 is_local,
524 opacity,
525 lang_item,
526 };
527 self.cached_item_metas
528 .insert(item_src.clone(), item_meta.clone());
529 item_meta
530 }
531}
532
533impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
534 pub(crate) fn translate_span_from_hax(&mut self, rspan: &hax::Span) -> Span {
535 self.t_ctx.translate_span_from_hax(rspan)
536 }
537
538 pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
539 self.t_ctx.def_span(def_id)
540 }
541}