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_frontend_exporter::{self as 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_raw_span(&mut self, rspan: &hax::Span) -> meta::RawSpan {
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::RawSpan { 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 span = self.translate_raw_span(&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_raw_span(parent_span);
135            Span {
136                span: parent_span,
137                generated_from_span: Some(span),
138            }
139        } else {
140            Span {
141                span,
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            span: self.translate_raw_span(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::DropGlue
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::DropGlueMethod => {
352                name.name
353                    .push(PathElem::Ident("drop".to_string(), Disambiguator::ZERO));
354            }
355            TransItemSourceKind::ClosureAsFnCast => {
356                name.name
357                    .push(PathElem::Ident("as_fn".into(), Disambiguator::ZERO));
358            }
359            TransItemSourceKind::VTable
360            | TransItemSourceKind::VTableInstance(..)
361            | TransItemSourceKind::VTableInstanceInitializer(..) => {
362                name.name
363                    .push(PathElem::Ident("{vtable}".into(), Disambiguator::ZERO));
364            }
365            _ => {}
366        }
367        Ok(name)
368    }
369
370    /// Retrieve the name for an item.
371    pub fn translate_name(&mut self, src: &TransItemSource) -> Result<Name, Error> {
372        let mut name = self.name_for_src(src)?;
373        // Push the generics used for monomorphization, if any.
374        if let RustcItem::Mono(item_ref) = &src.item
375            && !item_ref.generic_args.is_empty()
376        {
377            let trans_id = self.register_no_enqueue(&None, src).unwrap();
378            let span = self.def_span(&item_ref.def_id);
379            let mut bt_ctx = ItemTransCtx::new(src.clone(), trans_id, self);
380            bt_ctx.binding_levels.push(BindingLevel::new(true));
381            let args = bt_ctx.translate_generic_args(
382                span,
383                &item_ref.generic_args,
384                &item_ref.impl_exprs,
385            )?;
386            name.name.push(PathElem::Monomorphized(Box::new(args)));
387        }
388        Ok(name)
389    }
390
391    /// Remark: this **doesn't** register the def id (on purpose)
392    pub(crate) fn translate_trait_item_name(
393        &mut self,
394        def_id: &hax::DefId,
395    ) -> Result<TraitItemName, Error> {
396        let def = self.poly_hax_def(def_id)?;
397        let assoc = match def.kind() {
398            hax::FullDefKind::AssocTy {
399                associated_item, ..
400            }
401            | hax::FullDefKind::AssocConst {
402                associated_item, ..
403            }
404            | hax::FullDefKind::AssocFn {
405                associated_item, ..
406            } => associated_item,
407            _ => panic!("Unexpected def for associated item: {def:?}"),
408        };
409        Ok(TraitItemName(assoc.name.clone().unwrap_or_default()))
410    }
411
412    pub(crate) fn opacity_for_name(&self, name: &Name) -> ItemOpacity {
413        self.options.opacity_for_name(&self.translated, name)
414    }
415}
416
417// Attributes
418impl<'tcx, 'ctx> TranslateCtx<'tcx> {
419    /// Translates a rust attribute. Returns `None` if the attribute is a doc comment (rustc
420    /// encodes them as attributes). For now we use `String`s for `Attributes`.
421    pub(crate) fn translate_attribute(&mut self, attr: &hax::Attribute) -> Option<Attribute> {
422        use hax::Attribute as Haxttribute;
423        use hax::AttributeKind as HaxttributeKind;
424        match attr {
425            Haxttribute::Parsed(HaxttributeKind::DocComment { comment, .. }) => {
426                Some(Attribute::DocComment(comment.to_string()))
427            }
428            Haxttribute::Parsed(_) => None,
429            Haxttribute::Unparsed(attr) => {
430                let raw_attr = RawAttribute {
431                    path: attr.path.clone(),
432                    args: match &attr.args {
433                        hax::AttrArgs::Empty => None,
434                        hax::AttrArgs::Delimited(args) => Some(args.tokens.clone()),
435                        hax::AttrArgs::Eq { expr, .. } => self
436                            .tcx
437                            .sess
438                            .source_map()
439                            .span_to_snippet(expr.span.rust_span_data.unwrap().span())
440                            .ok(),
441                    },
442                };
443                match Attribute::parse_from_raw(raw_attr) {
444                    Ok(a) => Some(a),
445                    Err(msg) => {
446                        let span = self.translate_span_from_hax(&attr.span);
447                        register_error!(self, span, "Error parsing attribute: {msg}");
448                        None
449                    }
450                }
451            }
452        }
453    }
454
455    pub(crate) fn translate_inline(&self, def: &hax::FullDef) -> Option<InlineAttr> {
456        match def.kind() {
457            hax::FullDefKind::Fn { inline, .. } | hax::FullDefKind::AssocFn { inline, .. } => {
458                match inline {
459                    hax::InlineAttr::None => None,
460                    hax::InlineAttr::Hint => Some(InlineAttr::Hint),
461                    hax::InlineAttr::Never => Some(InlineAttr::Never),
462                    hax::InlineAttr::Always => Some(InlineAttr::Always),
463                    hax::InlineAttr::Force { .. } => Some(InlineAttr::Always),
464                }
465            }
466            _ => None,
467        }
468    }
469
470    pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef) -> AttrInfo {
471        // Default to `false` for impl blocks and closures.
472        let public = def.visibility.unwrap_or(false);
473        let inline = self.translate_inline(def);
474        let attributes = def
475            .attributes
476            .iter()
477            .filter_map(|attr| self.translate_attribute(&attr))
478            .collect_vec();
479
480        let rename = {
481            let mut renames = attributes.iter().filter_map(|a| a.as_rename()).cloned();
482            let rename = renames.next();
483            if renames.next().is_some() {
484                let span = self.translate_span_from_hax(&def.span);
485                register_error!(
486                    self,
487                    span,
488                    "There should be at most one `charon::rename(\"...\")` \
489                    or `aeneas::rename(\"...\")` attribute per declaration",
490                );
491            }
492            rename
493        };
494
495        AttrInfo {
496            attributes,
497            inline,
498            public,
499            rename,
500        }
501    }
502}
503
504// `ItemMeta`
505impl<'tcx, 'ctx> TranslateCtx<'tcx> {
506    /// Whether this item is in an `extern { .. }` block, in which case it has no body.
507    pub(crate) fn is_extern_item(&mut self, def: &hax::FullDef) -> bool {
508        def.def_id()
509            .parent
510            .as_ref()
511            .is_some_and(|parent| matches!(parent.kind, hax::DefKind::ForeignMod { .. }))
512    }
513
514    /// Compute the meta information for a Rust item.
515    pub(crate) fn translate_item_meta(
516        &mut self,
517        def: &hax::FullDef,
518        item_src: &TransItemSource,
519        name: Name,
520        name_opacity: ItemOpacity,
521    ) -> ItemMeta {
522        if let Some(item_meta) = self.cached_item_metas.get(&item_src) {
523            return item_meta.clone();
524        }
525        let span = def.source_span.as_ref().unwrap_or(&def.span);
526        let span = self.translate_span_from_hax(span);
527        let is_local = def.def_id().is_local;
528        let (attr_info, lang_item) = if item_src.is_derived_item() {
529            (AttrInfo::default(), None)
530        } else {
531            let attr_info = self.translate_attr_info(def);
532            let lang_item = def
533                .lang_item
534                .clone()
535                .or_else(|| def.diagnostic_item.clone());
536            (attr_info, lang_item)
537        };
538
539        let opacity = if self.is_extern_item(def)
540            || attr_info.attributes.iter().any(|attr| attr.is_opaque())
541        {
542            // Force opaque in these cases.
543            ItemOpacity::Opaque.max(name_opacity)
544        } else {
545            name_opacity
546        };
547
548        let item_meta = ItemMeta {
549            name,
550            span,
551            source_text: def.source_text.clone(),
552            attr_info,
553            is_local,
554            opacity,
555            lang_item,
556        };
557        self.cached_item_metas
558            .insert(item_src.clone(), item_meta.clone());
559        item_meta
560    }
561}
562
563impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
564    pub(crate) fn translate_span_from_hax(&mut self, rspan: &hax::Span) -> Span {
565        self.t_ctx.translate_span_from_hax(rspan)
566    }
567
568    pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
569        self.t_ctx.def_span(def_id)
570    }
571}
charon_driver/translate/translate_meta.rs

charon_driver/translate/
translate_meta.rs
