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 mut bt_ctx = ItemTransCtx::new(
212                            TransItemSource::new(item.clone(), TransItemSourceKind::InherentImpl),
213                            None,
214                            self,
215                        );
216                        bt_ctx.translate_def_generics(span, &full_def)?;
217                        let ty = bt_ctx.translate_ty(span, &ty)?;
218                        ImplElem::Ty(Binder {
219                            kind: BinderKind::InherentImplBlock,
220                            params: bt_ctx.into_generics(),
221                            skip_binder: ty,
222                        })
223                    }
224                    // Trait implementation
225                    hax::FullDefKind::TraitImpl { .. } => {
226                        let impl_id = {
227                            let item_src = TransItemSource::new(
228                                item.clone(),
229                                TransItemSourceKind::TraitImpl(TraitImplSource::Normal),
230                            );
231                            self.register_and_enqueue(&None, item_src).unwrap()
232                        };
233                        ImplElem::Trait(impl_id)
234                    }
235                    _ => unreachable!(),
236                };
237
238                Some(PathElem::Impl(impl_elem))
239            }
240            // TODO: do nothing for now
241            DefPathItem::OpaqueTy => None,
242            // TODO: this is not very satisfactory, but on the other hand
243            // we should be able to extract closures in local let-bindings
244            // (i.e., we shouldn't have to introduce top-level let-bindings).
245            DefPathItem::Closure => Some(PathElem::Ident("closure".to_string(), disambiguator)),
246            // Do nothing, functions in `extern` blocks are in the same namespace as the
247            // block.
248            DefPathItem::ForeignMod => None,
249            // Do nothing, the constructor of a struct/variant has the same name as the
250            // struct/variant.
251            DefPathItem::Ctor => None,
252            DefPathItem::Use => Some(PathElem::Ident("{use}".to_string(), disambiguator)),
253            DefPathItem::AnonConst => Some(PathElem::Ident("{const}".to_string(), disambiguator)),
254            DefPathItem::PromotedConst => Some(PathElem::Ident(
255                "{promoted_const}".to_string(),
256                disambiguator,
257            )),
258            _ => {
259                raise_error!(
260                    self,
261                    span,
262                    "Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}"
263                );
264            }
265        };
266        Ok(path_elem)
267    }
268
269    /// Retrieve the name for this [`hax::DefId`]. Because a given `DefId` may give rise to several
270    /// charon items, prefer to use `translate_name` when possible.
271    ///
272    /// We lookup the path associated to an id, and convert it to a name.
273    /// Paths very precisely identify where an item is. There are important
274    /// subcases, like the items in an `Impl` block:
275    /// ```ignore
276    /// impl<T> List<T> {
277    ///   fn new() ...
278    /// }
279    /// ```
280    ///
281    /// One issue here is that "List" *doesn't appear* in the path, which would
282    /// look like the following:
283    ///
284    ///   `TypeNS("Crate") :: Impl :: ValueNs("new")`
285    ///                       ^^^
286    ///           This is where "List" should be
287    ///
288    /// For this reason, whenever we find an `Impl` path element, we actually
289    /// lookup the type of the sub-path, from which we can derive a name.
290    ///
291    /// Besides, as there may be several "impl" blocks for one type, each impl
292    /// block is identified by a unique number (rustc calls this a
293    /// "disambiguator"), which we grab.
294    ///
295    /// Example:
296    /// ========
297    /// For instance, if we write the following code in crate `test` and module
298    /// `bla`:
299    /// ```ignore
300    /// impl<T> Foo<T> {
301    ///   fn foo() { ... }
302    /// }
303    ///
304    /// impl<T> Foo<T> {
305    ///   fn bar() { ... }
306    /// }
307    /// ```
308    ///
309    /// The names we will generate for `foo` and `bar` are:
310    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(0)), Ident("foo")]`
311    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(1)), Ident("bar")]`
312    fn name_for_item(&mut self, item: &RustcItem) -> Result<Name, Error> {
313        if let Some(name) = self.cached_names.get(item) {
314            return Ok(name.clone());
315        }
316        let def_id = item.def_id();
317        trace!("Computing name for `{def_id:?}`");
318
319        let parent_name = if let Some(parent_id) = &def_id.parent {
320            let def = self.hax_def_for_item(item)?;
321            if matches!(item, RustcItem::Mono(..))
322                && let Some(parent_item) = def.typing_parent(&self.hax_state)
323            {
324                self.name_for_item(&RustcItem::Mono(parent_item.clone()))?
325            } else {
326                self.name_for_item(&RustcItem::Poly(parent_id.clone()))?
327            }
328        } else {
329            Name { name: Vec::new() }
330        };
331        let span = self.def_span(def_id);
332        let mut name = parent_name;
333        if let Some(path_elem) = self.path_elem_for_def(span, item)? {
334            name.name.push(path_elem);
335        }
336
337        trace!("Computed name for `{def_id:?}`: `{name:?}`");
338        self.cached_names.insert(item.clone(), name.clone());
339        Ok(name)
340    }
341
342    /// Compute the name for an item.
343    /// Internal function, use `translate_name`.
344    pub fn name_for_src(&mut self, src: &TransItemSource) -> Result<Name, Error> {
345        let mut name = if let Some(parent) = src.parent() {
346            self.name_for_src(&parent)?
347        } else {
348            self.name_for_item(&src.item)?
349        };
350        match &src.kind {
351            // Nothing to do for the real items.
352            TransItemSourceKind::Type
353            | TransItemSourceKind::Fun
354            | TransItemSourceKind::Global
355            | TransItemSourceKind::TraitImpl(TraitImplSource::Normal)
356            | TransItemSourceKind::TraitDecl
357            | TransItemSourceKind::InherentImpl
358            | TransItemSourceKind::Module => {}
359
360            TransItemSourceKind::TraitImpl(
361                kind @ (TraitImplSource::Closure(..)
362                | TraitImplSource::ImplicitDestruct
363                | TraitImplSource::TraitAlias),
364            ) => {
365                if let TraitImplSource::Closure(..) = kind {
366                    let _ = name.name.pop(); // Pop the `{closure}`
367                }
368                let impl_id = self.register_and_enqueue(&None, src.clone()).unwrap();
369                name.name.push(PathElem::Impl(ImplElem::Trait(impl_id)));
370            }
371            TransItemSourceKind::DefaultedMethod(_, method_name) => {
372                name.name.push(PathElem::Ident(
373                    method_name.to_string(),
374                    Disambiguator::ZERO,
375                ));
376            }
377            TransItemSourceKind::ClosureMethod(kind) => {
378                let fn_name = kind.method_name().to_string();
379                name.name
380                    .push(PathElem::Ident(fn_name, Disambiguator::ZERO));
381            }
382            TransItemSourceKind::DropInPlaceMethod(..) => {
383                name.name.push(PathElem::Ident(
384                    "drop_in_place".to_string(),
385                    Disambiguator::ZERO,
386                ));
387            }
388            TransItemSourceKind::ClosureAsFnCast => {
389                name.name
390                    .push(PathElem::Ident("as_fn".into(), Disambiguator::ZERO));
391            }
392            TransItemSourceKind::VTable
393            | TransItemSourceKind::VTableInstance(..)
394            | TransItemSourceKind::VTableInstanceInitializer(..) => {
395                name.name
396                    .push(PathElem::Ident("{vtable}".into(), Disambiguator::ZERO));
397            }
398            TransItemSourceKind::VTableMethod => {
399                name.name.push(PathElem::Ident(
400                    "{vtable_method}".into(),
401                    Disambiguator::ZERO,
402                ));
403            }
404            TransItemSourceKind::VTableDropShim => {
405                name.name.push(PathElem::Ident(
406                    "{vtable_drop_shim}".into(),
407                    Disambiguator::ZERO,
408                ));
409            }
410        }
411        Ok(name)
412    }
413
414    /// Retrieve the name for an item.
415    pub fn translate_name(&mut self, src: &TransItemSource) -> Result<Name, Error> {
416        let mut name = self.name_for_src(src)?;
417        // Push the generics used for monomorphization, if any.
418        if let RustcItem::Mono(item_ref) = &src.item
419            && !item_ref.generic_args.is_empty()
420        {
421            let trans_id = self.register_no_enqueue(&None, src).unwrap();
422            let span = self.def_span(&item_ref.def_id);
423            let mut bt_ctx = ItemTransCtx::new(src.clone(), trans_id, self);
424            bt_ctx.binding_levels.push(BindingLevel::new(true));
425            let args = bt_ctx.translate_generic_args(
426                span,
427                &item_ref.generic_args,
428                &item_ref.impl_exprs,
429            )?;
430            name.name.push(PathElem::Instantiated(Box::new(Binder {
431                params: GenericParams::empty(),
432                skip_binder: args,
433                kind: BinderKind::Other,
434            })));
435        }
436        Ok(name)
437    }
438
439    /// Remark: this **doesn't** register the def id (on purpose)
440    pub(crate) fn translate_trait_item_name(
441        &mut self,
442        def_id: &hax::DefId,
443    ) -> Result<TraitItemName, Error> {
444        let def = self.poly_hax_def(def_id)?;
445        let assoc = match def.kind() {
446            hax::FullDefKind::AssocTy {
447                associated_item, ..
448            }
449            | hax::FullDefKind::AssocConst {
450                associated_item, ..
451            }
452            | hax::FullDefKind::AssocFn {
453                associated_item, ..
454            } => associated_item,
455            _ => panic!("Unexpected def for associated item: {def:?}"),
456        };
457        Ok(TraitItemName(
458            assoc.name.as_ref().map(|n| n.into()).unwrap_or_default(),
459        ))
460    }
461
462    pub(crate) fn opacity_for_name(&self, name: &Name) -> ItemOpacity {
463        self.options.opacity_for_name(&self.translated, name)
464    }
465}
466
467// Attributes
468impl<'tcx, 'ctx> TranslateCtx<'tcx> {
469    /// Translates a rust attribute. Returns `None` if the attribute is a doc comment (rustc
470    /// encodes them as attributes). For now we use `String`s for `Attributes`.
471    pub(crate) fn translate_attribute(&mut self, attr: &hax::Attribute) -> Option<Attribute> {
472        use hax::Attribute as Haxttribute;
473        use hax::AttributeKind as HaxttributeKind;
474        match attr {
475            Haxttribute::Parsed(HaxttributeKind::DocComment { comment, .. }) => {
476                Some(Attribute::DocComment(comment.to_string()))
477            }
478            Haxttribute::Parsed(_) => None,
479            Haxttribute::Unparsed(attr) => {
480                let raw_attr = RawAttribute {
481                    path: attr.path.clone(),
482                    args: match &attr.args {
483                        hax::AttrArgs::Empty => None,
484                        hax::AttrArgs::Delimited(args) => Some(args.tokens.clone()),
485                        hax::AttrArgs::Eq { expr, .. } => self
486                            .tcx
487                            .sess
488                            .source_map()
489                            .span_to_snippet(expr.span.rust_span_data.unwrap().span())
490                            .ok(),
491                    },
492                };
493                match Attribute::parse_from_raw(raw_attr) {
494                    Ok(a) => Some(a),
495                    Err(msg) => {
496                        let span = self.translate_span_from_hax(&attr.span);
497                        register_error!(self, span, "Error parsing attribute: {msg}");
498                        None
499                    }
500                }
501            }
502        }
503    }
504
505    pub(crate) fn translate_inline(&self, def: &hax::FullDef) -> Option<InlineAttr> {
506        match def.kind() {
507            hax::FullDefKind::Fn { inline, .. } | hax::FullDefKind::AssocFn { inline, .. } => {
508                match inline {
509                    hax::InlineAttr::None => None,
510                    hax::InlineAttr::Hint => Some(InlineAttr::Hint),
511                    hax::InlineAttr::Never => Some(InlineAttr::Never),
512                    hax::InlineAttr::Always => Some(InlineAttr::Always),
513                    hax::InlineAttr::Force { .. } => Some(InlineAttr::Always),
514                }
515            }
516            _ => None,
517        }
518    }
519
520    pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef) -> AttrInfo {
521        // Default to `false` for impl blocks and closures.
522        let public = def.visibility.unwrap_or(false);
523        let inline = self.translate_inline(def);
524        let attributes = def
525            .attributes
526            .iter()
527            .filter_map(|attr| self.translate_attribute(&attr))
528            .collect_vec();
529
530        let rename = {
531            let mut renames = attributes.iter().filter_map(|a| a.as_rename()).cloned();
532            let rename = renames.next();
533            if renames.next().is_some() {
534                let span = self.translate_span_from_hax(&def.span);
535                register_error!(
536                    self,
537                    span,
538                    "There should be at most one `charon::rename(\"...\")` \
539                    or `aeneas::rename(\"...\")` attribute per declaration",
540                );
541            }
542            rename
543        };
544
545        AttrInfo {
546            attributes,
547            inline,
548            public,
549            rename,
550        }
551    }
552}
553
554// `ItemMeta`
555impl<'tcx, 'ctx> TranslateCtx<'tcx> {
556    /// Whether this item is in an `extern { .. }` block, in which case it has no body.
557    pub(crate) fn is_extern_item(&mut self, def: &hax::FullDef) -> bool {
558        def.def_id()
559            .parent
560            .as_ref()
561            .is_some_and(|parent| matches!(parent.kind, hax::DefKind::ForeignMod { .. }))
562    }
563
564    /// Compute the meta information for a Rust item.
565    pub(crate) fn translate_item_meta(
566        &mut self,
567        def: &hax::FullDef,
568        item_src: &TransItemSource,
569        name: Name,
570        name_opacity: ItemOpacity,
571    ) -> ItemMeta {
572        if let Some(item_meta) = self.cached_item_metas.get(&item_src) {
573            return item_meta.clone();
574        }
575        let span = def.source_span.as_ref().unwrap_or(&def.span);
576        let span = self.translate_span_from_hax(span);
577        let is_local = def.def_id().is_local;
578        let (attr_info, lang_item) = if item_src.is_derived_item() {
579            (AttrInfo::default(), None)
580        } else {
581            let attr_info = self.translate_attr_info(def);
582            let lang_item = def
583                .lang_item
584                .clone()
585                .or_else(|| def.diagnostic_item.clone());
586            (attr_info, lang_item)
587        };
588
589        let opacity = if self.is_extern_item(def)
590            || attr_info.attributes.iter().any(|attr| attr.is_opaque())
591        {
592            // Force opaque in these cases.
593            ItemOpacity::Opaque.max(name_opacity)
594        } else {
595            name_opacity
596        };
597
598        let item_meta = ItemMeta {
599            name,
600            span,
601            source_text: def.source_text.clone(),
602            attr_info,
603            is_local,
604            opacity,
605            lang_item,
606        };
607        self.cached_item_metas
608            .insert(item_src.clone(), item_meta.clone());
609        item_meta
610    }
611}
612
613impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
614    pub(crate) fn translate_span_from_hax(&mut self, rspan: &hax::Span) -> Span {
615        self.t_ctx.translate_span_from_hax(rspan)
616    }
617
618    pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
619        self.t_ctx.def_span(def_id)
620    }
621}
charon_driver/translate/translate_meta.rs

charon_driver/translate/
translate_meta.rs
