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

charon_driver/translate/
translate_meta.rs
