charon_driver/translate/
translate_meta.rs

1//! Translate information about items: name, attributes, etc.
2use 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
10// Spans
11impl<'tcx, 'ctx> TranslateCtx<'tcx> {
12    /// Register a file if it is a "real" file and was not already registered
13    /// `span` must be a span from which we obtained that filename.
14    fn register_file(&mut self, filename: FileName, span: rustc_span::Span) -> FileId {
15        // Lookup the file if it was already registered
16        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                            // The path to files in the standard library may be full paths to somewhere
41                            // in the sysroot. This may depend on how the toolchain is installed
42                            // (rustup vs nix), so we normalize the paths here to avoid
43                            // inconsistencies in the translation.
44                            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                                // Unclear if this can happen, but just in case.
50                                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                        // We use the virtual name because it is always available.
61                        // That name normally starts with `/rustc/<hash>/`. For our purposes we hide
62                        // the hash.
63                        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            // We use the debug formatter to generate a filename.
86            // This is not ideal, but filenames are for debugging anyway.
87            _ => 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                // For now we forbid not real filenames
97                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        // Put together
112        meta::RawSpan { file_id, beg, end }
113    }
114
115    /// Compute span data from a Rust source scope
116    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        // Translate the span
122        let span = self.translate_raw_span(&source_info.span);
123
124        // Lookup the top-most inlined parent scope.
125        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
159// Names
160impl<'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        // Disambiguator disambiguates identically-named (but distinct) identifiers. This happens
168        // notably with macros and inherent impl blocks.
169        let disambiguator = Disambiguator::new(path_elem.disambiguator as usize);
170        // Match over the key data
171        let path_elem = match path_elem.data {
172            DefPathItem::CrateRoot { name, .. } => {
173                // Sanity check
174                error_assert!(self, span, path_elem.disambiguator == 0);
175                Some(PathElem::Ident(name.clone(), disambiguator))
176            }
177            // We map the three namespaces onto a single one. We can always disambiguate by looking
178            // at the definition.
179            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                // Two cases, depending on whether the impl block is
185                // a "regular" impl block (`impl Foo { ... }`) or a trait
186                // implementation (`impl Bar for Foo { ... }`).
187                let impl_elem = match full_def.kind() {
188                    // Inherent impl ("regular" impl)
189                    hax::FullDefKind::InherentImpl { ty, .. } => {
190                        // We need to convert the type, which may contain quantified
191                        // substs and bounds. In order to properly do so, we introduce
192                        // a body translation context.
193                        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                    // Trait implementation
207                    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            // TODO: do nothing for now
217            DefPathItem::OpaqueTy => None,
218            // TODO: this is not very satisfactory, but on the other hand
219            // we should be able to extract closures in local let-bindings
220            // (i.e., we shouldn't have to introduce top-level let-bindings).
221            DefPathItem::Closure => Some(PathElem::Ident("closure".to_string(), disambiguator)),
222            // Do nothing, functions in `extern` blocks are in the same namespace as the
223            // block.
224            DefPathItem::ForeignMod => None,
225            // Do nothing, the constructor of a struct/variant has the same name as the
226            // struct/variant.
227            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    /// Retrieve the name for this [`hax::DefId`]. Because a given `DefId` may give rise to several
246    /// charon items, prefer to use `translate_name` when possible.
247    ///
248    /// We lookup the path associated to an id, and convert it to a name.
249    /// Paths very precisely identify where an item is. There are important
250    /// subcases, like the items in an `Impl` block:
251    /// ```ignore
252    /// impl<T> List<T> {
253    ///   fn new() ...
254    /// }
255    /// ```
256    ///
257    /// One issue here is that "List" *doesn't appear* in the path, which would
258    /// look like the following:
259    ///
260    ///   `TypeNS("Crate") :: Impl :: ValueNs("new")`
261    ///                       ^^^
262    ///           This is where "List" should be
263    ///
264    /// For this reason, whenever we find an `Impl` path element, we actually
265    /// lookup the type of the sub-path, from which we can derive a name.
266    ///
267    /// Besides, as there may be several "impl" blocks for one type, each impl
268    /// block is identified by a unique number (rustc calls this a
269    /// "disambiguator"), which we grab.
270    ///
271    /// Example:
272    /// ========
273    /// For instance, if we write the following code in crate `test` and module
274    /// `bla`:
275    /// ```ignore
276    /// impl<T> Foo<T> {
277    ///   fn foo() { ... }
278    /// }
279    ///
280    /// impl<T> Foo<T> {
281    ///   fn bar() { ... }
282    /// }
283    /// ```
284    ///
285    /// The names we will generate for `foo` and `bar` are:
286    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(0)), Ident("foo")]`
287    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(1)), Ident("bar")]`
288    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    /// Retrieve the name for an item.
311    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(); // Pop the `{closure}`
323                        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    /// Remark: this **doesn't** register the def id (on purpose)
361    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
386// Attributes
387impl<'tcx, 'ctx> TranslateCtx<'tcx> {
388    /// Translates a rust attribute. Returns `None` if the attribute is a doc comment (rustc
389    /// encodes them as attributes). For now we use `String`s for `Attributes`.
390    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        // Default to `false` for impl blocks and closures.
441        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
473// `ItemMeta`
474impl<'tcx, 'ctx> TranslateCtx<'tcx> {
475    /// Whether this item is in an `extern { .. }` block, in which case it has no body.
476    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    /// Compute the meta information for a Rust item.
485    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            // Force opaque in these cases.
513            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}
charon_driver/translate/translate_meta.rs

charon_driver/translate/
translate_meta.rs
