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                            // Find the cargo home directory: according to cargo docs and having a
57                            // look at the cargo source, it's either the `$CARGO_HOME` var or
58                            // `$HOME/.cargo`
59                            let cargo_home = std::env::var("CARGO_HOME")
60                                .map(PathBuf::from)
61                                .ok()
62                                .or_else(|| std::env::home_dir().map(|p| p.join(".cargo")));
63                            if let Some(cargo_home) = cargo_home
64                                && let Ok(path) = path.strip_prefix(cargo_home)
65                            {
66                                // Avoid some more machine-dependent paths in the llbc output.
67                                let mut rewritten_path: PathBuf = "/cargo".into();
68                                rewritten_path.extend(path);
69                                rewritten_path
70                            } else {
71                                path.clone()
72                            }
73                        };
74                        FileName::Local(path)
75                    }
76                    RealFileName::Remapped { virtual_name, .. } => {
77                        // We use the virtual name because it is always available.
78                        // That name normally starts with `/rustc/<hash>/`. For our purposes we hide
79                        // the hash.
80                        let mut components_iter = virtual_name.components();
81                        if let Some(
82                            [
83                                Component::RootDir,
84                                Component::Normal(rustc),
85                                Component::Normal(hash),
86                            ],
87                        ) = components_iter.by_ref().array_chunks().next()
88                            && rustc.to_str() == Some("rustc")
89                            && hash.len() == 40
90                        {
91                            let path_without_hash = [Component::RootDir, Component::Normal(rustc)]
92                                .into_iter()
93                                .chain(components_iter)
94                                .collect();
95                            FileName::Virtual(path_without_hash)
96                        } else {
97                            FileName::Virtual(virtual_name.clone())
98                        }
99                    }
100                }
101            }
102            // We use the debug formatter to generate a filename.
103            // This is not ideal, but filenames are for debugging anyway.
104            _ => FileName::NotReal(format!("{name:?}")),
105        }
106    }
107
108    pub fn translate_span_data(&mut self, rspan: &hax::Span) -> meta::SpanData {
109        let filename = self.translate_filename(&rspan.filename);
110        let rust_span = rspan.rust_span_data.unwrap().span();
111        let file_id = match &filename {
112            FileName::NotReal(_) => {
113                // For now we forbid not real filenames
114                unimplemented!();
115            }
116            FileName::Virtual(_) | FileName::Local(_) => self.register_file(filename, rust_span),
117        };
118
119        fn convert_loc(loc: &hax::Loc) -> Loc {
120            Loc {
121                line: loc.line,
122                col: loc.col,
123            }
124        }
125        let beg = convert_loc(&rspan.lo);
126        let end = convert_loc(&rspan.hi);
127
128        // Put together
129        meta::SpanData { file_id, beg, end }
130    }
131
132    /// Compute span data from a Rust source scope
133    pub fn translate_span_from_source_info(
134        &mut self,
135        source_scopes: &hax::IndexVec<hax::SourceScope, hax::SourceScopeData>,
136        source_info: &hax::SourceInfo,
137    ) -> Span {
138        // Translate the span
139        let data = self.translate_span_data(&source_info.span);
140
141        // Lookup the top-most inlined parent scope.
142        let mut parent_span = None;
143        let mut scope_data = &source_scopes[source_info.scope];
144        while let Some(parent_scope) = scope_data.inlined_parent_scope {
145            scope_data = &source_scopes[parent_scope];
146            parent_span = Some(&scope_data.span);
147        }
148
149        if let Some(parent_span) = parent_span {
150            let parent_span = self.translate_span_data(parent_span);
151            Span {
152                data: parent_span,
153                generated_from_span: Some(data),
154            }
155        } else {
156            Span {
157                data,
158                generated_from_span: None,
159            }
160        }
161    }
162
163    pub(crate) fn translate_span_from_hax(&mut self, span: &hax::Span) -> Span {
164        Span {
165            data: self.translate_span_data(span),
166            generated_from_span: None,
167        }
168    }
169
170    pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
171        let span = def_id.def_span(&self.hax_state);
172        self.translate_span_from_hax(&span)
173    }
174}
175
176// Names
177impl<'tcx, 'ctx> TranslateCtx<'tcx> {
178    fn path_elem_for_def(
179        &mut self,
180        span: Span,
181        item: &RustcItem,
182    ) -> Result<Option<PathElem>, Error> {
183        let def_id = item.def_id();
184        let path_elem = def_id.path_item();
185        // Disambiguator disambiguates identically-named (but distinct) identifiers. This happens
186        // notably with macros and inherent impl blocks.
187        let disambiguator = Disambiguator::new(path_elem.disambiguator as usize);
188        // Match over the key data
189        let path_elem = match path_elem.data {
190            DefPathItem::CrateRoot { name, .. } => {
191                // Sanity check
192                error_assert!(self, span, path_elem.disambiguator == 0);
193                Some(PathElem::Ident(name.clone(), disambiguator))
194            }
195            // We map the three namespaces onto a single one. We can always disambiguate by looking
196            // at the definition.
197            DefPathItem::TypeNs(symbol)
198            | DefPathItem::ValueNs(symbol)
199            | DefPathItem::MacroNs(symbol) => Some(PathElem::Ident(symbol, disambiguator)),
200            DefPathItem::Impl => {
201                let full_def = self.hax_def_for_item(item)?;
202                // Two cases, depending on whether the impl block is
203                // a "regular" impl block (`impl Foo { ... }`) or a trait
204                // implementation (`impl Bar for Foo { ... }`).
205                let impl_elem = match full_def.kind() {
206                    // Inherent impl ("regular" impl)
207                    hax::FullDefKind::InherentImpl { ty, .. } => {
208                        // We need to convert the type, which may contain quantified
209                        // substs and bounds. In order to properly do so, we introduce
210                        // a body translation context.
211                        let item_src =
212                            TransItemSource::new(item.clone(), TransItemSourceKind::InherentImpl);
213                        let mut bt_ctx = ItemTransCtx::new(item_src, None, self);
214                        bt_ctx.translate_item_generics(
215                            span,
216                            &full_def,
217                            &TransItemSourceKind::InherentImpl,
218                        )?;
219                        let ty = bt_ctx.translate_ty(span, &ty)?;
220                        ImplElem::Ty(Binder {
221                            kind: BinderKind::InherentImplBlock,
222                            params: bt_ctx.into_generics(),
223                            skip_binder: ty,
224                        })
225                    }
226                    // Trait implementation
227                    hax::FullDefKind::TraitImpl { .. } => {
228                        let impl_id = {
229                            let item_src = TransItemSource::new(
230                                item.clone(),
231                                TransItemSourceKind::TraitImpl(TraitImplSource::Normal),
232                            );
233                            self.register_and_enqueue(&None, item_src).unwrap()
234                        };
235                        ImplElem::Trait(impl_id)
236                    }
237                    _ => unreachable!(),
238                };
239
240                Some(PathElem::Impl(impl_elem))
241            }
242            // TODO: do nothing for now
243            DefPathItem::OpaqueTy => None,
244            // TODO: this is not very satisfactory, but on the other hand
245            // we should be able to extract closures in local let-bindings
246            // (i.e., we shouldn't have to introduce top-level let-bindings).
247            DefPathItem::Closure => Some(PathElem::Ident("closure".to_string(), disambiguator)),
248            // Do nothing, functions in `extern` blocks are in the same namespace as the
249            // block.
250            DefPathItem::ForeignMod => None,
251            // Do nothing, the constructor of a struct/variant has the same name as the
252            // struct/variant.
253            DefPathItem::Ctor => None,
254            DefPathItem::Use => Some(PathElem::Ident("{use}".to_string(), disambiguator)),
255            DefPathItem::AnonConst => Some(PathElem::Ident("{const}".to_string(), disambiguator)),
256            DefPathItem::PromotedConst => Some(PathElem::Ident(
257                "{promoted_const}".to_string(),
258                disambiguator,
259            )),
260            _ => {
261                raise_error!(
262                    self,
263                    span,
264                    "Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}"
265                );
266            }
267        };
268        Ok(path_elem)
269    }
270
271    /// Retrieve the name for this [`hax::DefId`]. Because a given `DefId` may give rise to several
272    /// charon items, prefer to use `translate_name` when possible.
273    ///
274    /// We lookup the path associated to an id, and convert it to a name.
275    /// Paths very precisely identify where an item is. There are important
276    /// subcases, like the items in an `Impl` block:
277    /// ```ignore
278    /// impl<T> List<T> {
279    ///   fn new() ...
280    /// }
281    /// ```
282    ///
283    /// One issue here is that "List" *doesn't appear* in the path, which would
284    /// look like the following:
285    ///
286    ///   `TypeNS("Crate") :: Impl :: ValueNs("new")`
287    ///                       ^^^
288    ///           This is where "List" should be
289    ///
290    /// For this reason, whenever we find an `Impl` path element, we actually
291    /// lookup the type of the sub-path, from which we can derive a name.
292    ///
293    /// Besides, as there may be several "impl" blocks for one type, each impl
294    /// block is identified by a unique number (rustc calls this a
295    /// "disambiguator"), which we grab.
296    ///
297    /// Example:
298    /// ========
299    /// For instance, if we write the following code in crate `test` and module
300    /// `bla`:
301    /// ```ignore
302    /// impl<T> Foo<T> {
303    ///   fn foo() { ... }
304    /// }
305    ///
306    /// impl<T> Foo<T> {
307    ///   fn bar() { ... }
308    /// }
309    /// ```
310    ///
311    /// The names we will generate for `foo` and `bar` are:
312    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(0)), Ident("foo")]`
313    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(1)), Ident("bar")]`
314    fn name_for_item(&mut self, item: &RustcItem) -> Result<Name, Error> {
315        if let Some(name) = self.cached_names.get(item) {
316            return Ok(name.clone());
317        }
318        let def_id = item.def_id();
319        trace!("Computing name for `{def_id:?}`");
320
321        let parent_name = if let Some(parent_id) = &def_id.parent {
322            let def = self.hax_def_for_item(item)?;
323            if matches!(item, RustcItem::Mono(..))
324                && let Some(parent_item) = def.typing_parent(&self.hax_state)
325            {
326                self.name_for_item(&RustcItem::Mono(parent_item.clone()))?
327            } else {
328                self.name_for_item(&RustcItem::Poly(parent_id.clone()))?
329            }
330        } else {
331            Name { name: Vec::new() }
332        };
333        let span = self.def_span(def_id);
334        let mut name = parent_name;
335        if let Some(path_elem) = self.path_elem_for_def(span, item)? {
336            name.name.push(path_elem);
337        }
338
339        trace!("Computed name for `{def_id:?}`: `{name:?}`");
340        self.cached_names.insert(item.clone(), name.clone());
341        Ok(name)
342    }
343
344    /// Compute the name for an item.
345    /// Internal function, use `translate_name`.
346    pub fn name_for_src(&mut self, src: &TransItemSource) -> Result<Name, Error> {
347        let mut name = if let Some(parent) = src.parent() {
348            self.name_for_src(&parent)?
349        } else {
350            self.name_for_item(&src.item)?
351        };
352        match &src.kind {
353            // Nothing to do for the real items.
354            TransItemSourceKind::Type
355            | TransItemSourceKind::Fun
356            | TransItemSourceKind::Global
357            | TransItemSourceKind::TraitImpl(TraitImplSource::Normal)
358            | TransItemSourceKind::TraitDecl
359            | TransItemSourceKind::InherentImpl
360            | TransItemSourceKind::Module => {}
361
362            TransItemSourceKind::TraitImpl(
363                kind @ (TraitImplSource::Closure(..)
364                | TraitImplSource::ImplicitDestruct
365                | TraitImplSource::TraitAlias),
366            ) => {
367                if let TraitImplSource::Closure(..) = kind {
368                    let _ = name.name.pop(); // Pop the `{closure}`
369                }
370                let impl_id = self.register_and_enqueue(&None, src.clone()).unwrap();
371                name.name.push(PathElem::Impl(ImplElem::Trait(impl_id)));
372            }
373            TransItemSourceKind::DefaultedMethod(_, method_name) => {
374                name.name.push(PathElem::Ident(
375                    method_name.to_string(),
376                    Disambiguator::ZERO,
377                ));
378            }
379            TransItemSourceKind::ClosureMethod(kind) => {
380                let fn_name = kind.method_name().to_string();
381                name.name
382                    .push(PathElem::Ident(fn_name, Disambiguator::ZERO));
383            }
384            TransItemSourceKind::DropInPlaceMethod(..) => {
385                name.name.push(PathElem::Ident(
386                    "drop_in_place".to_string(),
387                    Disambiguator::ZERO,
388                ));
389            }
390            TransItemSourceKind::ClosureAsFnCast => {
391                name.name
392                    .push(PathElem::Ident("as_fn".into(), Disambiguator::ZERO));
393            }
394            TransItemSourceKind::VTable
395            | TransItemSourceKind::VTableInstance(..)
396            | TransItemSourceKind::VTableInstanceInitializer(..) => {
397                name.name
398                    .push(PathElem::Ident("{vtable}".into(), Disambiguator::ZERO));
399            }
400            TransItemSourceKind::VTableMethod => {
401                name.name.push(PathElem::Ident(
402                    "{vtable_method}".into(),
403                    Disambiguator::ZERO,
404                ));
405            }
406            TransItemSourceKind::VTableDropShim => {
407                name.name.push(PathElem::Ident(
408                    "{vtable_drop_shim}".into(),
409                    Disambiguator::ZERO,
410                ));
411            }
412        }
413        Ok(name)
414    }
415
416    /// Retrieve the name for an item.
417    pub fn translate_name(&mut self, src: &TransItemSource) -> Result<Name, Error> {
418        let mut name = self.name_for_src(src)?;
419        // Push the generics used for monomorphization, if any.
420        if let RustcItem::Mono(item_ref) = &src.item
421            && !item_ref.generic_args.is_empty()
422        {
423            let trans_id = self.register_no_enqueue(&None, src).unwrap();
424            let span = self.def_span(&item_ref.def_id);
425            let mut bt_ctx = ItemTransCtx::new(src.clone(), trans_id, self);
426            bt_ctx.binding_levels.push(BindingLevel::new(true));
427            let args = bt_ctx.translate_generic_args(
428                span,
429                &item_ref.generic_args,
430                &item_ref.impl_exprs,
431            )?;
432            name.name.push(PathElem::Instantiated(Box::new(Binder {
433                params: GenericParams::empty(),
434                skip_binder: args,
435                kind: BinderKind::Other,
436            })));
437        }
438        Ok(name)
439    }
440
441    /// Remark: this **doesn't** register the def id (on purpose)
442    pub(crate) fn translate_trait_item_name(
443        &mut self,
444        def_id: &hax::DefId,
445    ) -> Result<TraitItemName, Error> {
446        let def = self.poly_hax_def(def_id)?;
447        let assoc = match def.kind() {
448            hax::FullDefKind::AssocTy {
449                associated_item, ..
450            }
451            | hax::FullDefKind::AssocConst {
452                associated_item, ..
453            }
454            | hax::FullDefKind::AssocFn {
455                associated_item, ..
456            } => associated_item,
457            _ => panic!("Unexpected def for associated item: {def:?}"),
458        };
459        Ok(TraitItemName(
460            assoc.name.as_ref().map(|n| n.into()).unwrap_or_default(),
461        ))
462    }
463
464    pub(crate) fn opacity_for_name(&self, name: &Name) -> ItemOpacity {
465        self.options.opacity_for_name(&self.translated, name)
466    }
467}
468
469// Attributes
470impl<'tcx, 'ctx> TranslateCtx<'tcx> {
471    /// Translates a rust attribute. Returns `None` if the attribute is a doc comment (rustc
472    /// encodes them as attributes). For now we use `String`s for `Attributes`.
473    pub(crate) fn translate_attribute(&mut self, attr: &hax::Attribute) -> Option<Attribute> {
474        use hax::Attribute as Haxttribute;
475        use hax::AttributeKind as HaxttributeKind;
476        match attr {
477            Haxttribute::Parsed(HaxttributeKind::DocComment { comment, .. }) => {
478                Some(Attribute::DocComment(comment.to_string()))
479            }
480            Haxttribute::Parsed(_) => None,
481            Haxttribute::Unparsed(attr) => {
482                let raw_attr = RawAttribute {
483                    path: attr.path.clone(),
484                    args: match &attr.args {
485                        hax::AttrArgs::Empty => None,
486                        hax::AttrArgs::Delimited(args) => Some(args.tokens.clone()),
487                        hax::AttrArgs::Eq { expr, .. } => self
488                            .tcx
489                            .sess
490                            .source_map()
491                            .span_to_snippet(expr.span.rust_span_data.unwrap().span())
492                            .ok(),
493                    },
494                };
495                match Attribute::parse_from_raw(raw_attr) {
496                    Ok(a) => Some(a),
497                    Err(msg) => {
498                        let span = self.translate_span_from_hax(&attr.span);
499                        register_error!(self, span, "Error parsing attribute: {msg}");
500                        None
501                    }
502                }
503            }
504        }
505    }
506
507    pub(crate) fn translate_inline(&self, def: &hax::FullDef) -> Option<InlineAttr> {
508        match def.kind() {
509            hax::FullDefKind::Fn { inline, .. }
510            | hax::FullDefKind::AssocFn { inline, .. }
511            | hax::FullDefKind::Closure { inline, .. } => match inline {
512                hax::InlineAttr::None => None,
513                hax::InlineAttr::Hint => Some(InlineAttr::Hint),
514                hax::InlineAttr::Never => Some(InlineAttr::Never),
515                hax::InlineAttr::Always => Some(InlineAttr::Always),
516                hax::InlineAttr::Force { .. } => Some(InlineAttr::Always),
517            },
518            _ => None,
519        }
520    }
521
522    pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef) -> AttrInfo {
523        // Default to `false` for impl blocks and closures.
524        let public = def.visibility.unwrap_or(false);
525        let inline = self.translate_inline(def);
526        let attributes = def
527            .attributes
528            .iter()
529            .filter_map(|attr| self.translate_attribute(&attr))
530            .collect_vec();
531
532        let rename = {
533            let mut renames = attributes.iter().filter_map(|a| a.as_rename()).cloned();
534            let rename = renames.next();
535            if renames.next().is_some() {
536                let span = self.translate_span_from_hax(&def.span);
537                register_error!(
538                    self,
539                    span,
540                    "There should be at most one `charon::rename(\"...\")` \
541                    or `aeneas::rename(\"...\")` attribute per declaration",
542                );
543            }
544            rename
545        };
546
547        AttrInfo {
548            attributes,
549            inline,
550            public,
551            rename,
552        }
553    }
554}
555
556// `ItemMeta`
557impl<'tcx, 'ctx> TranslateCtx<'tcx> {
558    /// Whether this item is in an `extern { .. }` block, in which case it has no body.
559    pub(crate) fn is_extern_item(&mut self, def: &hax::FullDef) -> bool {
560        def.def_id()
561            .parent
562            .as_ref()
563            .is_some_and(|parent| matches!(parent.kind, hax::DefKind::ForeignMod { .. }))
564    }
565
566    /// Compute the meta information for a Rust item.
567    pub(crate) fn translate_item_meta(
568        &mut self,
569        def: &hax::FullDef,
570        item_src: &TransItemSource,
571        name: Name,
572        name_opacity: ItemOpacity,
573    ) -> ItemMeta {
574        if let Some(item_meta) = self.cached_item_metas.get(&item_src) {
575            return item_meta.clone();
576        }
577        let span = def.source_span.as_ref().unwrap_or(&def.span);
578        let span = self.translate_span_from_hax(span);
579        let is_local = def.def_id().is_local;
580        let (attr_info, lang_item) = if !item_src.is_derived_item()
581            || matches!(item_src.kind, TransItemSourceKind::ClosureMethod(..))
582        {
583            let attr_info = self.translate_attr_info(def);
584            let lang_item = def
585                .lang_item
586                .clone()
587                .or_else(|| def.diagnostic_item.clone());
588            (attr_info, lang_item)
589        } else {
590            (AttrInfo::default(), None)
591        };
592
593        let opacity = if self.is_extern_item(def)
594            || attr_info.attributes.iter().any(|attr| attr.is_opaque())
595        {
596            // Force opaque in these cases.
597            ItemOpacity::Opaque.max(name_opacity)
598        } else {
599            name_opacity
600        };
601
602        let item_meta = ItemMeta {
603            name,
604            span,
605            source_text: def.source_text.clone(),
606            attr_info,
607            is_local,
608            opacity,
609            lang_item,
610        };
611        self.cached_item_metas
612            .insert(item_src.clone(), item_meta.clone());
613        item_meta
614    }
615}
616
617impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
618    pub(crate) fn translate_span_from_hax(&mut self, rspan: &hax::Span) -> Span {
619        self.t_ctx.translate_span_from_hax(rspan)
620    }
621
622    pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
623        self.t_ctx.def_span(def_id)
624    }
625}
charon_driver/translate/translate_meta.rs

charon_driver/translate/
translate_meta.rs
