charon_driver/translate/
translate_meta.rs

1//! Translate information about items: name, attributes, etc.
2use super::translate_crate::TransItemSource;
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 file = File {
21                    name: filename.clone(),
22                    contents: source_file.src.as_deref().cloned(),
23                };
24                let id = self.translated.files.push(file);
25                self.file_to_id.insert(filename, id);
26                id
27            }
28        }
29    }
30
31    pub fn translate_filename(&mut self, name: &hax::FileName) -> meta::FileName {
32        match name {
33            hax::FileName::Real(name) => {
34                use hax::RealFileName;
35                match name {
36                    RealFileName::LocalPath(path) => {
37                        let path = if let Ok(path) = path.strip_prefix(&self.sysroot) {
38                            // The path to files in the standard library may be full paths to somewhere
39                            // in the sysroot. This may depend on how the toolchain is installed
40                            // (rustup vs nix), so we normalize the paths here to avoid
41                            // inconsistencies in the translation.
42                            if let Ok(path) = path.strip_prefix("lib/rustlib/src/rust") {
43                                let mut rewritten_path: PathBuf = "/rustc".into();
44                                rewritten_path.extend(path);
45                                rewritten_path
46                            } else {
47                                // Unclear if this can happen, but just in case.
48                                let mut rewritten_path: PathBuf = "/toolchain".into();
49                                rewritten_path.extend(path);
50                                rewritten_path
51                            }
52                        } else {
53                            path.clone()
54                        };
55                        FileName::Local(path)
56                    }
57                    RealFileName::Remapped { virtual_name, .. } => {
58                        // We use the virtual name because it is always available.
59                        // That name normally starts with `/rustc/<hash>/`. For our purposes we hide
60                        // the hash.
61                        let mut components_iter = virtual_name.components();
62                        if let Some(
63                            [Component::RootDir, Component::Normal(rustc), Component::Normal(hash)],
64                        ) = components_iter.by_ref().array_chunks().next()
65                            && rustc.to_str() == Some("rustc")
66                            && hash.len() == 40
67                        {
68                            let path_without_hash = [Component::RootDir, Component::Normal(rustc)]
69                                .into_iter()
70                                .chain(components_iter)
71                                .collect();
72                            FileName::Virtual(path_without_hash)
73                        } else {
74                            FileName::Virtual(virtual_name.clone())
75                        }
76                    }
77                }
78            }
79            // We use the debug formatter to generate a filename.
80            // This is not ideal, but filenames are for debugging anyway.
81            _ => FileName::NotReal(format!("{name:?}")),
82        }
83    }
84
85    pub fn translate_raw_span(&mut self, rspan: &hax::Span) -> meta::RawSpan {
86        let filename = self.translate_filename(&rspan.filename);
87        let rust_span = rspan.rust_span_data.unwrap().span();
88        let file_id = match &filename {
89            FileName::NotReal(_) => {
90                // For now we forbid not real filenames
91                unimplemented!();
92            }
93            FileName::Virtual(_) | FileName::Local(_) => self.register_file(filename, rust_span),
94        };
95
96        fn convert_loc(loc: &hax::Loc) -> Loc {
97            Loc {
98                line: loc.line,
99                col: loc.col,
100            }
101        }
102        let beg = convert_loc(&rspan.lo);
103        let end = convert_loc(&rspan.hi);
104
105        // Put together
106        meta::RawSpan { file_id, beg, end }
107    }
108
109    /// Compute span data from a Rust source scope
110    pub fn translate_span_from_source_info(
111        &mut self,
112        source_scopes: &hax::IndexVec<hax::SourceScope, hax::SourceScopeData>,
113        source_info: &hax::SourceInfo,
114    ) -> Span {
115        // Translate the span
116        let span = self.translate_raw_span(&source_info.span);
117
118        // Lookup the top-most inlined parent scope.
119        let mut parent_span = None;
120        let mut scope_data = &source_scopes[source_info.scope];
121        while let Some(parent_scope) = scope_data.inlined_parent_scope {
122            scope_data = &source_scopes[parent_scope];
123            parent_span = Some(&scope_data.span);
124        }
125
126        if let Some(parent_span) = parent_span {
127            let parent_span = self.translate_raw_span(parent_span);
128            Span {
129                span: parent_span,
130                generated_from_span: Some(span),
131            }
132        } else {
133            Span {
134                span,
135                generated_from_span: None,
136            }
137        }
138    }
139
140    pub(crate) fn translate_span_from_hax(&mut self, span: &hax::Span) -> Span {
141        Span {
142            span: self.translate_raw_span(span),
143            generated_from_span: None,
144        }
145    }
146
147    pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
148        let span = def_id.def_span(&self.hax_state);
149        self.translate_span_from_hax(&span)
150    }
151}
152
153// Names
154impl<'tcx, 'ctx> TranslateCtx<'tcx> {
155    fn path_elem_for_def(
156        &mut self,
157        span: Span,
158        def_id: &hax::DefId,
159    ) -> Result<Option<PathElem>, Error> {
160        let path_elem = def_id.path_item();
161        // Disambiguator disambiguates identically-named (but distinct) identifiers. This happens
162        // notably with macros and inherent impl blocks.
163        let disambiguator = Disambiguator::new(path_elem.disambiguator as usize);
164        // Match over the key data
165        let path_elem = match path_elem.data {
166            DefPathItem::CrateRoot { name, .. } => {
167                // Sanity check
168                error_assert!(self, span, path_elem.disambiguator == 0);
169                Some(PathElem::Ident(name.clone(), disambiguator))
170            }
171            // We map the three namespaces onto a single one. We can always disambiguate by looking
172            // at the definition.
173            DefPathItem::TypeNs(None) => None,
174            DefPathItem::TypeNs(Some(symbol))
175            | DefPathItem::ValueNs(symbol)
176            | DefPathItem::MacroNs(symbol) => Some(PathElem::Ident(symbol, disambiguator)),
177            DefPathItem::Impl => {
178                let full_def = self.hax_def(def_id)?;
179                // Two cases, depending on whether the impl block is
180                // a "regular" impl block (`impl Foo { ... }`) or a trait
181                // implementation (`impl Bar for Foo { ... }`).
182                let impl_elem = match full_def.kind() {
183                    // Inherent impl ("regular" impl)
184                    hax::FullDefKind::InherentImpl { ty, .. } => {
185                        // We need to convert the type, which may contain quantified
186                        // substs and bounds. In order to properly do so, we introduce
187                        // a body translation context.
188                        let mut bt_ctx = ItemTransCtx::new(def_id.clone(), None, self);
189                        bt_ctx.translate_def_generics(span, &full_def)?;
190                        let ty = bt_ctx.translate_ty(span, &ty)?;
191                        ImplElem::Ty(Binder {
192                            kind: BinderKind::InherentImplBlock,
193                            params: bt_ctx.into_generics(),
194                            skip_binder: ty,
195                        })
196                    }
197                    // Trait implementation
198                    hax::FullDefKind::TraitImpl { .. } => {
199                        let impl_id = self.register_trait_impl_id(&None, def_id);
200                        ImplElem::Trait(impl_id)
201                    }
202                    _ => unreachable!(),
203                };
204
205                Some(PathElem::Impl(impl_elem, disambiguator))
206            }
207            // TODO: do nothing for now
208            DefPathItem::OpaqueTy => None,
209            // TODO: this is not very satisfactory, but on the other hand
210            // we should be able to extract closures in local let-bindings
211            // (i.e., we shouldn't have to introduce top-level let-bindings).
212            DefPathItem::Closure => Some(PathElem::Ident("closure".to_string(), disambiguator)),
213            // Do nothing, functions in `extern` blocks are in the same namespace as the
214            // block.
215            DefPathItem::ForeignMod => None,
216            // Do nothing, the constructor of a struct/variant has the same name as the
217            // struct/variant.
218            DefPathItem::Ctor => None,
219            DefPathItem::Use => Some(PathElem::Ident("{use}".to_string(), disambiguator)),
220            DefPathItem::AnonConst => Some(PathElem::Ident("{const}".to_string(), disambiguator)),
221            DefPathItem::PromotedConst => Some(PathElem::Ident(
222                "{promoted_const}".to_string(),
223                disambiguator,
224            )),
225            _ => {
226                raise_error!(
227                    self,
228                    span,
229                    "Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}"
230                );
231            }
232        };
233        Ok(path_elem)
234    }
235
236    /// Retrieve the name for this [`hax::DefId`]. Because a given `DefId` may give rise to several
237    /// charon items, prefer to use `translate_name` when possible.
238    ///
239    /// We lookup the path associated to an id, and convert it to a name.
240    /// Paths very precisely identify where an item is. There are important
241    /// subcases, like the items in an `Impl` block:
242    /// ```ignore
243    /// impl<T> List<T> {
244    ///   fn new() ...
245    /// }
246    /// ```
247    ///
248    /// One issue here is that "List" *doesn't appear* in the path, which would
249    /// look like the following:
250    ///
251    ///   `TypeNS("Crate") :: Impl :: ValueNs("new")`
252    ///                       ^^^
253    ///           This is where "List" should be
254    ///
255    /// For this reason, whenever we find an `Impl` path element, we actually
256    /// lookup the type of the sub-path, from which we can derive a name.
257    ///
258    /// Besides, as there may be several "impl" blocks for one type, each impl
259    /// block is identified by a unique number (rustc calls this a
260    /// "disambiguator"), which we grab.
261    ///
262    /// Example:
263    /// ========
264    /// For instance, if we write the following code in crate `test` and module
265    /// `bla`:
266    /// ```ignore
267    /// impl<T> Foo<T> {
268    ///   fn foo() { ... }
269    /// }
270    ///
271    /// impl<T> Foo<T> {
272    ///   fn bar() { ... }
273    /// }
274    /// ```
275    ///
276    /// The names we will generate for `foo` and `bar` are:
277    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(0)), Ident("foo")]`
278    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(1)), Ident("bar")]`
279    pub fn def_id_to_name(&mut self, def_id: &hax::DefId) -> Result<Name, Error> {
280        if let Some(name) = self.cached_names.get(&def_id) {
281            return Ok(name.clone());
282        }
283        trace!("Computing name for `{def_id:?}`");
284
285        let parent_name = if let Some(parent) = &def_id.parent {
286            self.def_id_to_name(parent)?
287        } else {
288            Name { name: Vec::new() }
289        };
290        let span = self.def_span(def_id);
291        let mut name = parent_name;
292        if let Some(path_elem) = self.path_elem_for_def(span, &def_id)? {
293            name.name.push(path_elem);
294        }
295
296        trace!("Computed name for `{def_id:?}`: `{name:?}`");
297        self.cached_names.insert(def_id.clone(), name.clone());
298        Ok(name)
299    }
300
301    /// Retrieve the name for an item.
302    pub fn translate_name(&mut self, src: &TransItemSource) -> Result<Name, Error> {
303        let def_id = src.as_def_id();
304        let mut name = self.def_id_to_name(def_id)?;
305        match src {
306            TransItemSource::ClosureTraitImpl(id, kind)
307            | TransItemSource::ClosureMethod(id, kind) => {
308                let _ = name.name.pop(); // Pop the `{closure}` path item
309                let impl_id = self.register_closure_trait_impl_id(&None, id, *kind);
310                name.name.push(PathElem::Impl(
311                    ImplElem::Trait(impl_id),
312                    Disambiguator::ZERO,
313                ));
314
315                if matches!(src, TransItemSource::ClosureMethod(..)) {
316                    let fn_name = kind.method_name().to_string();
317                    name.name
318                        .push(PathElem::Ident(fn_name, Disambiguator::ZERO));
319                }
320            }
321            _ => {}
322        }
323        Ok(name)
324    }
325
326    /// Remark: this **doesn't** register the def id (on purpose)
327    pub(crate) fn translate_trait_item_name(
328        &mut self,
329        def_id: &hax::DefId,
330    ) -> Result<TraitItemName, Error> {
331        // Translate the name
332        let name = self.def_id_to_name(def_id)?;
333        let (name, id) = name.name.last().unwrap().as_ident().unwrap();
334        assert!(id.is_zero());
335        Ok(TraitItemName(name.to_string()))
336    }
337
338    pub(crate) fn opacity_for_name(&self, name: &Name) -> ItemOpacity {
339        self.options.opacity_for_name(&self.translated, name)
340    }
341}
342
343// Attributes
344impl<'tcx, 'ctx> TranslateCtx<'tcx> {
345    /// Translates a rust attribute. Returns `None` if the attribute is a doc comment (rustc
346    /// encodes them as attributes). For now we use `String`s for `Attributes`.
347    pub(crate) fn translate_attribute(&mut self, attr: &hax::Attribute) -> Option<Attribute> {
348        use hax::Attribute as Haxttribute;
349        use hax::AttributeKind as HaxttributeKind;
350        match attr {
351            Haxttribute::Parsed(HaxttributeKind::DocComment { comment, .. }) => {
352                Some(Attribute::DocComment(comment.to_string()))
353            }
354            Haxttribute::Parsed(_) => None,
355            Haxttribute::Unparsed(attr) => {
356                let raw_attr = RawAttribute {
357                    path: attr.path.clone(),
358                    args: match &attr.args {
359                        hax::AttrArgs::Empty => None,
360                        hax::AttrArgs::Delimited(args) => Some(args.tokens.clone()),
361                        hax::AttrArgs::Eq { expr, .. } => self
362                            .tcx
363                            .sess
364                            .source_map()
365                            .span_to_snippet(expr.span.rust_span_data.unwrap().span())
366                            .ok(),
367                    },
368                };
369                match Attribute::parse_from_raw(raw_attr) {
370                    Ok(a) => Some(a),
371                    Err(msg) => {
372                        let span = self.translate_span_from_hax(&attr.span);
373                        register_error!(self, span, "Error parsing attribute: {msg}");
374                        None
375                    }
376                }
377            }
378        }
379    }
380
381    pub(crate) fn translate_inline(&self, def: &hax::FullDef) -> Option<InlineAttr> {
382        match def.kind() {
383            hax::FullDefKind::Fn { inline, .. } | hax::FullDefKind::AssocFn { inline, .. } => {
384                match inline {
385                    hax::InlineAttr::None => None,
386                    hax::InlineAttr::Hint => Some(InlineAttr::Hint),
387                    hax::InlineAttr::Never => Some(InlineAttr::Never),
388                    hax::InlineAttr::Always => Some(InlineAttr::Always),
389                    hax::InlineAttr::Force { .. } => Some(InlineAttr::Always),
390                }
391            }
392            _ => None,
393        }
394    }
395
396    pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef) -> AttrInfo {
397        // Default to `false` for impl blocks and closures.
398        let public = def.visibility.unwrap_or(false);
399        let inline = self.translate_inline(def);
400        let attributes = def
401            .attributes
402            .iter()
403            .filter_map(|attr| self.translate_attribute(&attr))
404            .collect_vec();
405
406        let rename = {
407            let mut renames = attributes.iter().filter_map(|a| a.as_rename()).cloned();
408            let rename = renames.next();
409            if renames.next().is_some() {
410                let span = self.translate_span_from_hax(&def.span);
411                register_error!(
412                    self,
413                    span,
414                    "There should be at most one `charon::rename(\"...\")` \
415                    or `aeneas::rename(\"...\")` attribute per declaration",
416                );
417            }
418            rename
419        };
420
421        AttrInfo {
422            attributes,
423            inline,
424            public,
425            rename,
426        }
427    }
428}
429
430// `ItemMeta`
431impl<'tcx, 'ctx> TranslateCtx<'tcx> {
432    /// Whether this item is in an `extern { .. }` block, in which case it has no body.
433    pub(crate) fn is_extern_item(&mut self, def: &hax::FullDef) -> bool {
434        def.parent.as_ref().is_some_and(|parent| {
435            self.hax_def(parent).is_ok_and(|parent_def| {
436                matches!(parent_def.kind(), hax::FullDefKind::ForeignMod { .. })
437            })
438        })
439    }
440
441    /// Compute the meta information for a Rust item.
442    pub(crate) fn translate_item_meta(
443        &mut self,
444        def: &hax::FullDef,
445        item_src: &TransItemSource,
446        name: Name,
447        name_opacity: ItemOpacity,
448    ) -> ItemMeta {
449        if let Some(item_meta) = self.cached_item_metas.get(&item_src) {
450            return item_meta.clone();
451        }
452        let span = def.source_span.as_ref().unwrap_or(&def.span);
453        let span = self.translate_span_from_hax(span);
454        let attr_info = self.translate_attr_info(def);
455        let is_local = def.def_id.is_local;
456        let lang_item = def
457            .lang_item
458            .clone()
459            .or_else(|| def.diagnostic_item.clone());
460
461        let opacity = if self.is_extern_item(def)
462            || attr_info.attributes.iter().any(|attr| attr.is_opaque())
463        {
464            // Force opaque in these cases.
465            ItemOpacity::Opaque.max(name_opacity)
466        } else {
467            name_opacity
468        };
469
470        let item_meta = ItemMeta {
471            name,
472            span,
473            source_text: def.source_text.clone(),
474            attr_info,
475            is_local,
476            opacity,
477            lang_item,
478        };
479        self.cached_item_metas
480            .insert(item_src.clone(), item_meta.clone());
481        item_meta
482    }
483}
484
485impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
486    pub(crate) fn translate_span_from_hax(&mut self, rspan: &hax::Span) -> Span {
487        self.t_ctx.translate_span_from_hax(rspan)
488    }
489
490    pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
491        self.t_ctx.def_span(def_id)
492    }
493}
charon_driver/translate/translate_meta.rs

charon_driver/translate/
translate_meta.rs
