charon_driver/translate/
translate_meta.rs

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

charon_driver/translate/
translate_meta.rs
