charon_driver/translate/
translate_meta.rs

1//! Translate information about items: name, attributes, etc.
2use itertools::Itertools;
3use rustc_middle::mir;
4use std::cmp::Ord;
5use std::path::{Component, PathBuf};
6
7use super::translate_crate::RustcItem;
8use super::translate_ctx::*;
9use super::translate_generics::BindingLevel;
10use charon_lib::ast::*;
11use hax::{DefPathItem, SInto};
12
13// Spans
14impl<'tcx, 'ctx> TranslateCtx<'tcx> {
15    /// Register a file if it is a "real" file and was not already registered
16    /// `span` must be a span from which we obtained that filename.
17    fn register_file(&mut self, filename: FileName, span: rustc_span::Span) -> FileId {
18        // Lookup the file if it was already registered
19        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: rustc_span::FileName) -> meta::FileName {
37        match name {
38            rustc_span::FileName::Real(name) => {
39                use rustc_span::RealFileName;
40                match name {
41                    RealFileName::LocalPath(path) => {
42                        let path = if let Ok(path) = path.strip_prefix(&self.sysroot) {
43                            // The path to files in the standard library may be full paths to somewhere
44                            // in the sysroot. This may depend on how the toolchain is installed
45                            // (rustup vs nix), so we normalize the paths here to avoid
46                            // inconsistencies in the translation.
47                            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                                // Unclear if this can happen, but just in case.
53                                let mut rewritten_path: PathBuf = "/toolchain".into();
54                                rewritten_path.extend(path);
55                                rewritten_path
56                            }
57                        } else {
58                            // Find the cargo home directory: according to cargo docs and having a
59                            // look at the cargo source, it's either the `$CARGO_HOME` var or
60                            // `$HOME/.cargo`
61                            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                                // Avoid some more machine-dependent paths in the llbc output.
69                                let mut rewritten_path: PathBuf = "/cargo".into();
70                                rewritten_path.extend(path);
71                                rewritten_path
72                            } else {
73                                path.clone()
74                            }
75                        };
76                        FileName::Local(path)
77                    }
78                    RealFileName::Remapped { virtual_name, .. } => {
79                        // We use the virtual name because it is always available.
80                        // That name normally starts with `/rustc/<hash>/`. For our purposes we hide
81                        // the hash.
82                        let mut components_iter = virtual_name.components();
83                        if let Some(
84                            [
85                                Component::RootDir,
86                                Component::Normal(rustc),
87                                Component::Normal(hash),
88                            ],
89                        ) = components_iter.by_ref().array_chunks().next()
90                            && rustc.to_str() == Some("rustc")
91                            && hash.len() == 40
92                        {
93                            let path_without_hash = [Component::RootDir, Component::Normal(rustc)]
94                                .into_iter()
95                                .chain(components_iter)
96                                .collect();
97                            FileName::Virtual(path_without_hash)
98                        } else {
99                            FileName::Virtual(virtual_name.clone())
100                        }
101                    }
102                }
103            }
104            // We use the debug formatter to generate a filename.
105            // This is not ideal, but filenames are for debugging anyway.
106            _ => FileName::NotReal(format!("{name:?}")),
107        }
108    }
109
110    pub fn translate_span_data(&mut self, span: rustc_span::Span) -> meta::SpanData {
111        let smap: &rustc_span::source_map::SourceMap = self.tcx.sess.psess.source_map();
112        let filename = smap.span_to_filename(span);
113        let filename = self.translate_filename(filename);
114        let span = span;
115        let file_id = match &filename {
116            FileName::NotReal(_) => {
117                // For now we forbid not real filenames
118                unimplemented!();
119            }
120            FileName::Virtual(_) | FileName::Local(_) => self.register_file(filename, span),
121        };
122
123        let convert_loc = |pos: rustc_span::BytePos| -> Loc {
124            let loc = smap.lookup_char_pos(pos);
125            Loc {
126                line: loc.line,
127                col: loc.col_display,
128            }
129        };
130        let beg = convert_loc(span.lo());
131        let end = convert_loc(span.hi());
132
133        // Put together
134        meta::SpanData { file_id, beg, end }
135    }
136
137    /// Compute span data from a Rust source scope
138    pub fn translate_span_from_source_info(
139        &mut self,
140        source_scopes: &rustc_index::IndexVec<mir::SourceScope, mir::SourceScopeData>,
141        source_info: &mir::SourceInfo,
142    ) -> Span {
143        // Translate the span
144        let data = self.translate_span_data(source_info.span);
145
146        // Lookup the top-most inlined parent scope.
147        let mut parent_span = None;
148        let mut scope_data = &source_scopes[source_info.scope];
149        while let Some(parent_scope) = scope_data.inlined_parent_scope {
150            scope_data = &source_scopes[parent_scope];
151            parent_span = Some(scope_data.span);
152        }
153
154        if let Some(parent_span) = parent_span {
155            let parent_span = self.translate_span_data(parent_span);
156            Span {
157                data: parent_span,
158                generated_from_span: Some(data),
159            }
160        } else {
161            Span {
162                data,
163                generated_from_span: None,
164            }
165        }
166    }
167
168    pub(crate) fn translate_span(&mut self, span: &rustc_span::Span) -> Span {
169        Span {
170            data: self.translate_span_data(*span),
171            generated_from_span: None,
172        }
173    }
174
175    pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
176        let span = def_id.def_span(&self.hax_state);
177        self.translate_span(&span)
178    }
179}
180
181// Names
182impl<'tcx, 'ctx> TranslateCtx<'tcx> {
183    fn path_elem_for_def(
184        &mut self,
185        span: Span,
186        item: &RustcItem,
187    ) -> Result<Option<PathElem>, Error> {
188        let def_id = item.def_id();
189        let path_elem = def_id.path_item(&self.hax_state);
190        // Disambiguator disambiguates identically-named (but distinct) identifiers. This happens
191        // notably with macros and inherent impl blocks.
192        let disambiguator = Disambiguator::new(path_elem.disambiguator as usize);
193        // Match over the key data
194        let path_elem = match path_elem.data {
195            DefPathItem::CrateRoot { name, .. } => {
196                // Sanity check
197                error_assert!(self, span, path_elem.disambiguator == 0);
198                Some(PathElem::Ident(name.to_string(), disambiguator))
199            }
200            // We map the three namespaces onto a single one. We can always disambiguate by looking
201            // at the definition.
202            DefPathItem::TypeNs(symbol)
203            | DefPathItem::ValueNs(symbol)
204            | DefPathItem::MacroNs(symbol) => {
205                Some(PathElem::Ident(symbol.to_string(), disambiguator))
206            }
207            DefPathItem::Impl => {
208                let full_def = self.hax_def_for_item(item)?;
209                // Two cases, depending on whether the impl block is
210                // a "regular" impl block (`impl Foo { ... }`) or a trait
211                // implementation (`impl Bar for Foo { ... }`).
212                let impl_elem = match full_def.kind() {
213                    // Inherent impl ("regular" impl)
214                    hax::FullDefKind::InherentImpl { ty, .. } => {
215                        // We need to convert the type, which may contain quantified
216                        // substs and bounds. In order to properly do so, we introduce
217                        // a body translation context.
218                        let item_src =
219                            TransItemSource::new(item.clone(), TransItemSourceKind::InherentImpl);
220                        let mut bt_ctx = ItemTransCtx::new(item_src, None, self);
221                        bt_ctx.translate_item_generics(
222                            span,
223                            &full_def,
224                            &TransItemSourceKind::InherentImpl,
225                        )?;
226                        let ty = bt_ctx.translate_ty(span, &ty)?;
227                        ImplElem::Ty(Binder {
228                            kind: BinderKind::InherentImplBlock,
229                            params: bt_ctx.into_generics(),
230                            skip_binder: ty,
231                        })
232                    }
233                    // Trait implementation
234                    hax::FullDefKind::TraitImpl { .. } => {
235                        let impl_id = {
236                            let item_src = TransItemSource::new(
237                                item.clone(),
238                                TransItemSourceKind::TraitImpl(TraitImplSource::Normal),
239                            );
240                            self.register_and_enqueue(&None, item_src).unwrap()
241                        };
242                        ImplElem::Trait(impl_id)
243                    }
244                    _ => unreachable!(),
245                };
246
247                Some(PathElem::Impl(impl_elem))
248            }
249            // TODO: do nothing for now
250            DefPathItem::OpaqueTy => None,
251            // TODO: this is not very satisfactory, but on the other hand
252            // we should be able to extract closures in local let-bindings
253            // (i.e., we shouldn't have to introduce top-level let-bindings).
254            DefPathItem::Closure => Some(PathElem::Ident("closure".to_string(), disambiguator)),
255            // Do nothing, functions in `extern` blocks are in the same namespace as the
256            // block.
257            DefPathItem::ForeignMod => None,
258            // Do nothing, the constructor of a struct/variant has the same name as the
259            // struct/variant.
260            DefPathItem::Ctor => None,
261            DefPathItem::Use => Some(PathElem::Ident("{use}".to_string(), disambiguator)),
262            DefPathItem::AnonConst => Some(PathElem::Ident("{const}".to_string(), disambiguator)),
263            DefPathItem::PromotedConst => Some(PathElem::Ident(
264                "{promoted_const}".to_string(),
265                disambiguator,
266            )),
267            _ => {
268                raise_error!(
269                    self,
270                    span,
271                    "Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}"
272                );
273            }
274        };
275        Ok(path_elem)
276    }
277
278    /// Retrieve the name for this [`hax::DefId`]. Because a given `DefId` may give rise to several
279    /// charon items, prefer to use `translate_name` when possible.
280    ///
281    /// We lookup the path associated to an id, and convert it to a name.
282    /// Paths very precisely identify where an item is. There are important
283    /// subcases, like the items in an `Impl` block:
284    /// ```ignore
285    /// impl<T> List<T> {
286    ///   fn new() ...
287    /// }
288    /// ```
289    ///
290    /// One issue here is that "List" *doesn't appear* in the path, which would
291    /// look like the following:
292    ///
293    ///   `TypeNS("Crate") :: Impl :: ValueNs("new")`
294    ///                       ^^^
295    ///           This is where "List" should be
296    ///
297    /// For this reason, whenever we find an `Impl` path element, we actually
298    /// lookup the type of the sub-path, from which we can derive a name.
299    ///
300    /// Besides, as there may be several "impl" blocks for one type, each impl
301    /// block is identified by a unique number (rustc calls this a
302    /// "disambiguator"), which we grab.
303    ///
304    /// Example:
305    /// ========
306    /// For instance, if we write the following code in crate `test` and module
307    /// `bla`:
308    /// ```ignore
309    /// impl<T> Foo<T> {
310    ///   fn foo() { ... }
311    /// }
312    ///
313    /// impl<T> Foo<T> {
314    ///   fn bar() { ... }
315    /// }
316    /// ```
317    ///
318    /// The names we will generate for `foo` and `bar` are:
319    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(0)), Ident("foo")]`
320    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(1)), Ident("bar")]`
321    fn name_for_item(&mut self, item: &RustcItem) -> Result<Name, Error> {
322        if let Some(name) = self.cached_names.get(item) {
323            return Ok(name.clone());
324        }
325        let def_id = item.def_id();
326        trace!("Computing name for `{def_id:?}`");
327
328        let parent_name = if let Some(parent_id) = &def_id.parent {
329            let def = self.hax_def_for_item(item)?;
330            if matches!(item, RustcItem::Mono(..))
331                && let Some(parent_item) = def.typing_parent(&self.hax_state)
332            {
333                self.name_for_item(&RustcItem::Mono(parent_item.clone()))?
334            } else {
335                self.name_for_item(&RustcItem::Poly(parent_id.clone()))?
336            }
337        } else {
338            Name { name: Vec::new() }
339        };
340        let span = self.def_span(def_id);
341        let mut name = parent_name;
342        if let Some(path_elem) = self.path_elem_for_def(span, item)? {
343            name.name.push(path_elem);
344        }
345
346        trace!("Computed name for `{def_id:?}`: `{name:?}`");
347        self.cached_names.insert(item.clone(), name.clone());
348        Ok(name)
349    }
350
351    /// Compute the name for an item.
352    /// Internal function, use `translate_name`.
353    pub fn name_for_src(&mut self, src: &TransItemSource) -> Result<Name, Error> {
354        let mut name = if let Some(parent) = src.parent() {
355            self.name_for_src(&parent)?
356        } else {
357            self.name_for_item(&src.item)?
358        };
359        match &src.kind {
360            // Nothing to do for the real items.
361            TransItemSourceKind::Type
362            | TransItemSourceKind::Fun
363            | TransItemSourceKind::Global
364            | TransItemSourceKind::TraitImpl(TraitImplSource::Normal)
365            | TransItemSourceKind::TraitDecl
366            | TransItemSourceKind::InherentImpl
367            | TransItemSourceKind::Module => {}
368
369            TransItemSourceKind::TraitImpl(
370                kind @ (TraitImplSource::Closure(..)
371                | TraitImplSource::ImplicitDestruct
372                | TraitImplSource::TraitAlias),
373            ) => {
374                if let TraitImplSource::Closure(..) = kind {
375                    let _ = name.name.pop(); // Pop the `{closure}`
376                }
377                let impl_id = self.register_and_enqueue(&None, src.clone()).unwrap();
378                name.name.push(PathElem::Impl(ImplElem::Trait(impl_id)));
379            }
380            TransItemSourceKind::DefaultedMethod(_, method_name) => {
381                name.name.push(PathElem::Ident(
382                    method_name.to_string(),
383                    Disambiguator::ZERO,
384                ));
385            }
386            TransItemSourceKind::ClosureMethod(kind) => {
387                let fn_name = kind.method_name().to_string();
388                name.name
389                    .push(PathElem::Ident(fn_name, Disambiguator::ZERO));
390            }
391            TransItemSourceKind::DropInPlaceMethod(..) => {
392                name.name.push(PathElem::Ident(
393                    "drop_in_place".to_string(),
394                    Disambiguator::ZERO,
395                ));
396            }
397            TransItemSourceKind::ClosureAsFnCast => {
398                name.name
399                    .push(PathElem::Ident("as_fn".into(), Disambiguator::ZERO));
400            }
401            TransItemSourceKind::VTable
402            | TransItemSourceKind::VTableInstance(..)
403            | TransItemSourceKind::VTableInstanceInitializer(..) => {
404                name.name
405                    .push(PathElem::Ident("{vtable}".into(), Disambiguator::ZERO));
406            }
407            TransItemSourceKind::VTableMethod => {
408                name.name.push(PathElem::Ident(
409                    "{vtable_method}".into(),
410                    Disambiguator::ZERO,
411                ));
412            }
413            TransItemSourceKind::VTableDropShim => {
414                name.name.push(PathElem::Ident(
415                    "{vtable_drop_shim}".into(),
416                    Disambiguator::ZERO,
417                ));
418            }
419        }
420        Ok(name)
421    }
422
423    /// Retrieve the name for an item.
424    pub fn translate_name(&mut self, src: &TransItemSource) -> Result<Name, Error> {
425        let mut name = self.name_for_src(src)?;
426        // Push the generics used for monomorphization, if any.
427        if let RustcItem::Mono(item_ref) = &src.item
428            && !item_ref.generic_args.is_empty()
429        {
430            let trans_id = self.register_no_enqueue(&None, src).unwrap();
431            let span = self.def_span(&item_ref.def_id);
432            let mut bt_ctx = ItemTransCtx::new(src.clone(), trans_id, self);
433            bt_ctx.binding_levels.push(BindingLevel::new(true));
434            let args = bt_ctx.translate_generic_args(
435                span,
436                &item_ref.generic_args,
437                &item_ref.impl_exprs,
438            )?;
439            name.name.push(PathElem::Instantiated(Box::new(Binder {
440                params: GenericParams::empty(),
441                skip_binder: args,
442                kind: BinderKind::Other,
443            })));
444        }
445        Ok(name)
446    }
447
448    /// Remark: this **doesn't** register the def id (on purpose)
449    pub(crate) fn translate_trait_item_name(
450        &mut self,
451        def_id: &hax::DefId,
452    ) -> Result<TraitItemName, Error> {
453        let def = self.poly_hax_def(def_id)?;
454        let assoc = match def.kind() {
455            hax::FullDefKind::AssocTy {
456                associated_item, ..
457            }
458            | hax::FullDefKind::AssocConst {
459                associated_item, ..
460            }
461            | hax::FullDefKind::AssocFn {
462                associated_item, ..
463            } => associated_item,
464            _ => panic!("Unexpected def for associated item: {def:?}"),
465        };
466        Ok(TraitItemName(
467            assoc
468                .name
469                .as_ref()
470                .map(|n| n.to_string().into())
471                .unwrap_or_default(),
472        ))
473    }
474
475    pub(crate) fn opacity_for_name(&self, name: &Name) -> ItemOpacity {
476        self.options.opacity_for_name(&self.translated, name)
477    }
478}
479
480// Attributes
481impl<'tcx, 'ctx> TranslateCtx<'tcx> {
482    /// Translates a rust attribute. Returns `None` if the attribute is a doc comment (rustc
483    /// encodes them as attributes). For now we use `String`s for `Attributes`.
484    pub(crate) fn translate_attribute(&mut self, attr: &rustc_hir::Attribute) -> Option<Attribute> {
485        use rustc_hir as hir;
486        use rustc_hir::attrs as hir_attrs;
487        match attr {
488            hir::Attribute::Parsed(hir_attrs::AttributeKind::DocComment { comment, .. }) => {
489                Some(Attribute::DocComment(comment.to_string()))
490            }
491            hir::Attribute::Parsed(_) => None,
492            hir::Attribute::Unparsed(attr) => {
493                let raw_attr = RawAttribute {
494                    path: attr.path.to_string(),
495                    args: match &attr.args {
496                        hir::AttrArgs::Empty => None,
497                        hir::AttrArgs::Delimited(args) => {
498                            Some(rustc_ast_pretty::pprust::tts_to_string(&args.tokens))
499                        }
500                        hir::AttrArgs::Eq { expr, .. } => {
501                            self.tcx.sess.source_map().span_to_snippet(expr.span).ok()
502                        }
503                    },
504                };
505                match Attribute::parse_from_raw(raw_attr) {
506                    Ok(a) => Some(a),
507                    Err(msg) => {
508                        let span = self.translate_span(&attr.span.sinto(&self.hax_state));
509                        register_error!(self, span, "Error parsing attribute: {msg}");
510                        None
511                    }
512                }
513            }
514        }
515    }
516
517    pub(crate) fn translate_inline(&self, def: &hax::FullDef) -> Option<InlineAttr> {
518        match def.kind() {
519            hax::FullDefKind::Fn { inline, .. }
520            | hax::FullDefKind::AssocFn { inline, .. }
521            | hax::FullDefKind::Closure { inline, .. } => match inline {
522                hax::InlineAttr::None => None,
523                hax::InlineAttr::Hint => Some(InlineAttr::Hint),
524                hax::InlineAttr::Never => Some(InlineAttr::Never),
525                hax::InlineAttr::Always => Some(InlineAttr::Always),
526                hax::InlineAttr::Force { .. } => Some(InlineAttr::Always),
527            },
528            _ => None,
529        }
530    }
531
532    pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef) -> AttrInfo {
533        // Default to `false` for impl blocks and closures.
534        let public = def.visibility.unwrap_or(false);
535        let inline = self.translate_inline(def);
536        let attributes = def
537            .attributes
538            .iter()
539            .filter_map(|attr| self.translate_attribute(&attr))
540            .collect_vec();
541
542        let rename = {
543            let mut renames = attributes.iter().filter_map(|a| a.as_rename()).cloned();
544            let rename = renames.next();
545            if renames.next().is_some() {
546                let span = self.translate_span(&def.span);
547                register_error!(
548                    self,
549                    span,
550                    "There should be at most one `charon::rename(\"...\")` \
551                    or `aeneas::rename(\"...\")` attribute per declaration",
552                );
553            }
554            rename
555        };
556
557        AttrInfo {
558            attributes,
559            inline,
560            public,
561            rename,
562        }
563    }
564}
565
566// `ItemMeta`
567impl<'tcx, 'ctx> TranslateCtx<'tcx> {
568    /// Whether this item is in an `extern { .. }` block, in which case it has no body.
569    pub(crate) fn is_extern_item(&mut self, def: &hax::FullDef) -> bool {
570        def.def_id()
571            .parent
572            .as_ref()
573            .is_some_and(|parent| matches!(parent.kind, hax::DefKind::ForeignMod { .. }))
574    }
575
576    /// Compute the meta information for a Rust item.
577    pub(crate) fn translate_item_meta(
578        &mut self,
579        def: &hax::FullDef,
580        item_src: &TransItemSource,
581        name: Name,
582        name_opacity: ItemOpacity,
583    ) -> ItemMeta {
584        if let Some(item_meta) = self.cached_item_metas.get(&item_src) {
585            return item_meta.clone();
586        }
587        let span = def.source_span.as_ref().unwrap_or(&def.span);
588        let span = self.translate_span(span);
589        let is_local = def.def_id().is_local();
590        let (attr_info, lang_item) = if !item_src.is_derived_item()
591            || matches!(item_src.kind, TransItemSourceKind::ClosureMethod(..))
592        {
593            let attr_info = self.translate_attr_info(def);
594            let lang_item = def
595                .lang_item
596                .clone()
597                .or_else(|| def.diagnostic_item.clone())
598                .map(|s| s.to_string());
599            (attr_info, lang_item)
600        } else {
601            (AttrInfo::default(), None)
602        };
603
604        let opacity = if attr_info.attributes.iter().any(|attr| attr.is_exclude()) {
605            ItemOpacity::Invisible.max(name_opacity)
606        } else if self.is_extern_item(def)
607            || attr_info.attributes.iter().any(|attr| attr.is_opaque())
608        {
609            // Force opaque in these cases.
610            ItemOpacity::Opaque.max(name_opacity)
611        } else {
612            name_opacity
613        };
614
615        let item_meta = ItemMeta {
616            name,
617            span,
618            source_text: def.source_text.clone(),
619            attr_info,
620            is_local,
621            opacity,
622            lang_item,
623        };
624        self.cached_item_metas
625            .insert(item_src.clone(), item_meta.clone());
626        item_meta
627    }
628}
charon_driver/translate/translate_meta.rs

charon_driver/translate/
translate_meta.rs
