charon_driver/translate/
translate_meta.rs

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

charon_driver/translate/
translate_meta.rs
