charon_driver/translate/
translate_meta.rs

1//! Translate information about items: name, attributes, etc.
2use itertools::Itertools;
3use rustc_middle::mir;
4use rustc_span::RemapPathScopeComponents;
5use std::cmp::Ord;
6use std::path::{Component, PathBuf};
7
8use super::translate_crate::RustcItem;
9use super::translate_ctx::*;
10use crate::hax;
11use crate::hax::{DefPathItem, SInto};
12use charon_lib::ast::*;
13
14// Spans
15impl<'tcx> TranslateCtx<'tcx> {
16    /// Register a file if it is a "real" file and was not already registered
17    /// `span` must be a span from which we obtained that filename.
18    fn register_file(&mut self, filename: FileName, span: rustc_span::Span) -> FileId {
19        // Lookup the file if it was already registered
20        match self.file_to_id.get(&filename) {
21            Some(id) => *id,
22            None => {
23                let source_file = self.tcx.sess.source_map().lookup_source_file(span.lo());
24                let crate_name = self.tcx.crate_name(source_file.cnum).to_string();
25                let id = self.translated.files.push_with(|id| File {
26                    id,
27                    name: filename.clone(),
28                    crate_name,
29                    contents: source_file.src.as_deref().cloned(),
30                });
31                self.file_to_id.insert(filename, id);
32                id
33            }
34        }
35    }
36
37    pub fn translate_filename(&mut self, name: rustc_span::FileName) -> meta::FileName {
38        match name {
39            rustc_span::FileName::Real(name) => {
40                match name.local_path() {
41                    Some(path) => {
42                        // Normalize path separators: cross-compiling to Windows uses `\` as path
43                        // separators.
44                        let path: PathBuf = {
45                            let mut normalized = PathBuf::new();
46                            for comp in path.components() {
47                                for segment in comp.as_os_str().to_string_lossy().split("\\") {
48                                    normalized.push(segment);
49                                }
50                            }
51                            normalized
52                        };
53                        let path = if let Ok(path) = path.strip_prefix(&self.sysroot) {
54                            // The path to files in the standard library may be full paths to somewhere
55                            // in the sysroot. This may depend on how the toolchain is installed
56                            // (rustup vs nix), so we normalize the paths here to avoid
57                            // inconsistencies in the translation.
58                            if let Ok(path) = path.strip_prefix("lib/rustlib/src/rust") {
59                                let mut rewritten_path: PathBuf = "/rustc".into();
60                                rewritten_path.extend(path);
61                                rewritten_path
62                            } else {
63                                // Unclear if this can happen, but just in case.
64                                let mut rewritten_path: PathBuf = "/toolchain".into();
65                                rewritten_path.extend(path);
66                                rewritten_path
67                            }
68                        } else {
69                            // Find the cargo home directory: according to cargo docs and having a
70                            // look at the cargo source, it's either the `$CARGO_HOME` var or
71                            // `$HOME/.cargo`
72                            let cargo_home = std::env::var("CARGO_HOME")
73                                .map(PathBuf::from)
74                                .ok()
75                                .or_else(|| std::env::home_dir().map(|p| p.join(".cargo")));
76                            if let Some(cargo_home) = cargo_home
77                                && let Ok(path) = path.strip_prefix(cargo_home)
78                            {
79                                // Avoid some more machine-dependent paths in the llbc output.
80                                let mut rewritten_path: PathBuf = "/cargo".into();
81                                rewritten_path.extend(path);
82                                rewritten_path
83                            } else {
84                                path
85                            }
86                        };
87                        FileName::Local(path)
88                    }
89                    None => {
90                        // We use the virtual name because it is always available.
91                        // That name normally starts with `/rustc/<hash>/`. For our purposes we hide
92                        // the hash.
93                        let virtual_name = name.path(RemapPathScopeComponents::MACRO);
94                        let mut components_iter = virtual_name.components();
95                        if let Some(
96                            [
97                                Component::RootDir,
98                                Component::Normal(rustc),
99                                Component::Normal(hash),
100                            ],
101                        ) = components_iter.by_ref().array_chunks().next()
102                            && rustc.to_str() == Some("rustc")
103                            && hash.len() == 40
104                        {
105                            let path_without_hash = [Component::RootDir, Component::Normal(rustc)]
106                                .into_iter()
107                                .chain(components_iter)
108                                .collect();
109                            FileName::Virtual(path_without_hash)
110                        } else {
111                            FileName::Virtual(virtual_name.into())
112                        }
113                    }
114                }
115            }
116            // We use the debug formatter to generate a filename.
117            // This is not ideal, but filenames are for debugging anyway.
118            _ => FileName::NotReal(format!("{name:?}")),
119        }
120    }
121
122    pub fn translate_span_data(&mut self, span: rustc_span::Span) -> meta::SpanData {
123        let smap: &rustc_span::source_map::SourceMap = self.tcx.sess.psess.source_map();
124        let filename = smap.span_to_filename(span);
125        let filename = self.translate_filename(filename);
126        let file_id = match &filename {
127            FileName::NotReal(_) => {
128                // For now we forbid not real filenames
129                unimplemented!();
130            }
131            FileName::Virtual(_) | FileName::Local(_) => self.register_file(filename, span),
132        };
133
134        let convert_loc = |pos: rustc_span::BytePos| -> Loc {
135            let loc = smap.lookup_char_pos(pos);
136            Loc {
137                line: loc.line,
138                col: loc.col_display,
139            }
140        };
141        let beg = convert_loc(span.lo());
142        let end = convert_loc(span.hi());
143
144        // Put together
145        meta::SpanData { file_id, beg, end }
146    }
147
148    /// Compute span data from a Rust source scope
149    pub fn translate_span_from_source_info(
150        &mut self,
151        source_scopes: &rustc_index::IndexVec<mir::SourceScope, mir::SourceScopeData>,
152        source_info: &mir::SourceInfo,
153    ) -> Span {
154        // Translate the span
155        let data = self.translate_span_data(source_info.span);
156
157        // Lookup the top-most inlined parent scope.
158        let mut parent_span = None;
159        let mut scope_data = &source_scopes[source_info.scope];
160        while let Some(parent_scope) = scope_data.inlined_parent_scope {
161            scope_data = &source_scopes[parent_scope];
162            parent_span = Some(scope_data.span);
163        }
164
165        if let Some(parent_span) = parent_span {
166            let parent_span = self.translate_span_data(parent_span);
167            Span {
168                data: parent_span,
169                generated_from_span: Some(data),
170            }
171        } else {
172            Span {
173                data,
174                generated_from_span: None,
175            }
176        }
177    }
178
179    pub(crate) fn translate_span(&mut self, span: &rustc_span::Span) -> Span {
180        Span {
181            data: self.translate_span_data(*span),
182            generated_from_span: None,
183        }
184    }
185
186    pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
187        let span = def_id.def_span(&self.hax_state);
188        self.translate_span(&span)
189    }
190}
191
192// Names
193impl<'tcx> TranslateCtx<'tcx> {
194    fn path_elem_for_def(
195        &mut self,
196        span: Span,
197        item: &RustcItem,
198    ) -> Result<Option<PathElem>, Error> {
199        let def_id = item.def_id();
200        let path_elem = def_id.path_item(&self.hax_state);
201        // Disambiguator disambiguates identically-named (but distinct) identifiers. This happens
202        // notably with macros and inherent impl blocks.
203        let disambiguator = Disambiguator::new(path_elem.disambiguator as usize);
204        // Match over the key data
205        let path_elem = match path_elem.data {
206            DefPathItem::CrateRoot { name, .. } => {
207                // Sanity check
208                error_assert!(self, span, path_elem.disambiguator == 0);
209                Some(PathElem::Ident(name.to_string(), disambiguator))
210            }
211            // We map the three namespaces onto a single one. We can always disambiguate by looking
212            // at the definition.
213            DefPathItem::TypeNs(symbol)
214            | DefPathItem::ValueNs(symbol)
215            | DefPathItem::MacroNs(symbol) => {
216                Some(PathElem::Ident(symbol.to_string(), disambiguator))
217            }
218            DefPathItem::Impl => {
219                let full_def = self.hax_def_for_item(item)?;
220                // Two cases, depending on whether the impl block is
221                // a "regular" impl block (`impl Foo { ... }`) or a trait
222                // implementation (`impl Bar for Foo { ... }`).
223                let impl_elem = match full_def.kind() {
224                    // Inherent impl ("regular" impl)
225                    hax::FullDefKind::InherentImpl { ty, .. } => {
226                        // We need to convert the type, which may contain quantified
227                        // substs and bounds. In order to properly do so, we introduce
228                        // a body translation context.
229                        let item_src =
230                            TransItemSource::new(item.clone(), TransItemSourceKind::InherentImpl);
231                        let mut bt_ctx = ItemTransCtx::new(item_src, None, self);
232                        bt_ctx.translate_item_generics(
233                            span,
234                            &full_def,
235                            &TransItemSourceKind::InherentImpl,
236                        )?;
237                        let ty = bt_ctx.translate_ty(span, ty)?;
238                        ImplElem::Ty(Box::new(Binder {
239                            kind: BinderKind::InherentImplBlock,
240                            params: bt_ctx.into_generics(),
241                            skip_binder: ty,
242                        }))
243                    }
244                    // Trait implementation
245                    hax::FullDefKind::TraitImpl { .. } => {
246                        let impl_id = {
247                            let item_src = TransItemSource::new(
248                                item.clone(),
249                                TransItemSourceKind::TraitImpl(TraitImplSource::Normal),
250                            );
251                            self.register_and_enqueue(&None, item_src).unwrap()
252                        };
253                        ImplElem::Trait(impl_id)
254                    }
255                    _ => unreachable!(),
256                };
257
258                Some(PathElem::Impl(impl_elem))
259            }
260            // TODO: do nothing for now
261            DefPathItem::OpaqueTy => None,
262            // TODO: this is not very satisfactory, but on the other hand
263            // we should be able to extract closures in local let-bindings
264            // (i.e., we shouldn't have to introduce top-level let-bindings).
265            DefPathItem::Closure => Some(PathElem::Ident("closure".to_string(), disambiguator)),
266            // Do nothing, functions in `extern` blocks are in the same namespace as the
267            // block.
268            DefPathItem::ForeignMod => None,
269            // Do nothing, the constructor of a struct/variant has the same name as the
270            // struct/variant.
271            DefPathItem::Ctor => None,
272            DefPathItem::Use => Some(PathElem::Ident("{use}".to_string(), disambiguator)),
273            DefPathItem::AnonConst => Some(PathElem::Ident("{const}".to_string(), disambiguator)),
274            DefPathItem::PromotedConst => Some(PathElem::Ident(
275                "{promoted_const}".to_string(),
276                disambiguator,
277            )),
278            _ => {
279                raise_error!(
280                    self,
281                    span,
282                    "Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}"
283                );
284            }
285        };
286        Ok(path_elem)
287    }
288
289    /// Retrieve the name for this [`hax::DefId`]. Because a given `DefId` may give rise to several
290    /// charon items, prefer to use `translate_name` when possible.
291    ///
292    /// We lookup the path associated to an id, and convert it to a name.
293    /// Paths very precisely identify where an item is. There are important
294    /// subcases, like the items in an `Impl` block:
295    /// ```ignore
296    /// impl<T> List<T> {
297    ///   fn new() ...
298    /// }
299    /// ```
300    ///
301    /// One issue here is that "List" *doesn't appear* in the path, which would
302    /// look like the following:
303    ///
304    ///   `TypeNS("Crate") :: Impl :: ValueNs("new")`
305    ///                       ^^^
306    ///           This is where "List" should be
307    ///
308    /// For this reason, whenever we find an `Impl` path element, we actually
309    /// lookup the type of the sub-path, from which we can derive a name.
310    ///
311    /// Besides, as there may be several "impl" blocks for one type, each impl
312    /// block is identified by a unique number (rustc calls this a
313    /// "disambiguator"), which we grab.
314    ///
315    /// Example:
316    /// ========
317    /// For instance, if we write the following code in crate `test` and module
318    /// `bla`:
319    /// ```ignore
320    /// impl<T> Foo<T> {
321    ///   fn foo() { ... }
322    /// }
323    ///
324    /// impl<T> Foo<T> {
325    ///   fn bar() { ... }
326    /// }
327    /// ```
328    ///
329    /// The names we will generate for `foo` and `bar` are:
330    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(0)), Ident("foo")]`
331    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(1)), Ident("bar")]`
332    fn name_for_item(&mut self, item: &RustcItem) -> Result<Name, Error> {
333        if let Some(name) = self.cached_names.get(item) {
334            return Ok(name.clone());
335        }
336        let def_id = item.def_id();
337        trace!("Computing name for `{def_id:?}`");
338
339        let parent_name = if let Some(parent_id) = def_id.parent(&self.hax_state) {
340            let def = self.hax_def_for_item(item)?;
341            if matches!(item, RustcItem::Mono(..))
342                && let Some(parent_item) = def.typing_parent(&self.hax_state)
343            {
344                self.name_for_item(&RustcItem::Mono(parent_item.clone()))?
345            } else {
346                self.name_for_item(&RustcItem::Poly(parent_id.clone()))?
347            }
348        } else {
349            Name { name: Vec::new() }
350        };
351        let span = self.def_span(def_id);
352        let mut name = parent_name;
353        if let Some(path_elem) = self.path_elem_for_def(span, item)? {
354            name.name.push(path_elem);
355        }
356
357        trace!("Computed name for `{def_id:?}`: `{name:?}`");
358        self.cached_names.insert(item.clone(), name.clone());
359        Ok(name)
360    }
361
362    /// Compute the name for an item.
363    /// Internal function, use `translate_name`.
364    pub fn name_for_src(&mut self, src: &TransItemSource) -> Result<Name, Error> {
365        let mut name = if let Some(parent) = src.parent() {
366            self.name_for_src(&parent)?
367        } else {
368            self.name_for_item(&src.item)?
369        };
370        match &src.kind {
371            // Nothing to do for the real items.
372            TransItemSourceKind::Type
373            | TransItemSourceKind::Fun
374            | TransItemSourceKind::Global
375            | TransItemSourceKind::TraitImpl(TraitImplSource::Normal)
376            | TransItemSourceKind::TraitDecl
377            | TransItemSourceKind::InherentImpl
378            | TransItemSourceKind::Module => {}
379
380            TransItemSourceKind::TraitImpl(
381                kind @ (TraitImplSource::Closure(..)
382                | TraitImplSource::ImplicitDestruct
383                | TraitImplSource::TraitAlias),
384            ) => {
385                if let TraitImplSource::Closure(..) = kind {
386                    let _ = name.name.pop(); // Pop the `{closure}`
387                }
388                let impl_id = self.register_and_enqueue(&None, src.clone()).unwrap();
389                name.name.push(PathElem::Impl(ImplElem::Trait(impl_id)));
390            }
391            TransItemSourceKind::DefaultedMethod(_, trait_id, method_id) => {
392                let method_name = self.translated.assoc_item_name(*trait_id, *method_id);
393                name.name.push(PathElem::Ident(
394                    method_name.to_string(),
395                    Disambiguator::ZERO,
396                ));
397            }
398            TransItemSourceKind::ClosureMethod(kind) => {
399                let fn_name = kind.method_name().to_string();
400                name.name
401                    .push(PathElem::Ident(fn_name, Disambiguator::ZERO));
402            }
403            TransItemSourceKind::DropInPlaceMethod(..) => {
404                name.name.push(PathElem::Ident(
405                    "drop_in_place".to_string(),
406                    Disambiguator::ZERO,
407                ));
408            }
409            TransItemSourceKind::ClosureAsFnCast => {
410                name.name
411                    .push(PathElem::Ident("as_fn".into(), Disambiguator::ZERO));
412            }
413            TransItemSourceKind::VTable
414            | TransItemSourceKind::VTableInstance(..)
415            | TransItemSourceKind::VTableInstanceInitializer(..) => {
416                name.name
417                    .push(PathElem::Ident("{vtable}".into(), Disambiguator::ZERO));
418            }
419            TransItemSourceKind::VTableMethod => {
420                name.name.push(PathElem::Ident(
421                    "{vtable_method}".into(),
422                    Disambiguator::ZERO,
423                ));
424            }
425            TransItemSourceKind::VTableDropShim => {
426                name.name.push(PathElem::Ident(
427                    "{vtable_drop_shim}".into(),
428                    Disambiguator::ZERO,
429                ));
430            }
431        }
432        Ok(name)
433    }
434
435    /// Retrieve the name for an item.
436    pub fn translate_name(&mut self, src: &TransItemSource) -> Result<Name, Error> {
437        let mut name = self.name_for_src(src)?;
438        // Push the generics used for monomorphization, if any. We skip mono trait impls as the
439        // generics are already included in the `PathElem::Impl` reference.
440        if let RustcItem::Mono(item_ref) = &src.item
441            && !item_ref.generic_args.is_empty()
442            && !matches!(src.kind, TransItemSourceKind::TraitImpl(..))
443        {
444            let trans_id = self.register_no_enqueue(&None, src).unwrap();
445            let span = self.def_span(&item_ref.def_id);
446            let mut bt_ctx = ItemTransCtx::new(src.clone(), trans_id, self);
447            let binder = bt_ctx.inside_binder(BinderKind::Other, |bt_ctx| {
448                bt_ctx.translate_generic_args(span, &item_ref.generic_args, &item_ref.impl_exprs)
449            })?;
450            if !binder.skip_binder.is_empty() {
451                name.name.push(PathElem::Instantiated(Box::new(binder)));
452            }
453        }
454        Ok(name)
455    }
456
457    pub(crate) fn opacity_for_name(&self, name: &Name) -> ItemOpacity {
458        self.options.opacity_for_name(&self.translated, name)
459    }
460}
461
462// Attributes
463impl<'tcx> TranslateCtx<'tcx> {
464    /// Parse a raw attribute to recognize our special `charon::*`, `aeneas::*` and `verify::*` attributes.
465    fn parse_attr_from_raw(
466        &mut self,
467        def_id: &hax::DefId,
468        raw_attr: RawAttribute,
469    ) -> Result<Attribute, String> {
470        // If the attribute path has two components, the first of which is `charon` or `aeneas`, we
471        // try to parse it. Otherwise we return `Unknown`.
472        let path = raw_attr.path.split("::").collect_vec();
473        let attr_name = if let &[path_start, attr_name] = path.as_slice()
474            && (path_start == "charon" || path_start == "aeneas" || path_start == "verify")
475        {
476            attr_name
477        } else {
478            return Ok(Attribute::Unknown(raw_attr));
479        };
480
481        match self.parse_special_attr(def_id, attr_name, &raw_attr)? {
482            Some(parsed) => Ok(parsed),
483            None => Err(format!("Unrecognized attribute: `{}`", raw_attr)),
484        }
485    }
486
487    /// Parse a `charon::*`, `aeneas::*` or `verify::*` attribute.
488    fn parse_special_attr(
489        &mut self,
490        def_id: &hax::DefId,
491        attr_name: &str,
492        raw_attr: &RawAttribute,
493    ) -> Result<Option<Attribute>, String> {
494        let args = raw_attr.args.as_deref();
495        let parsed = match attr_name {
496            // `#[charon::opaque]`
497            "opaque" if args.is_none() => Attribute::Opaque,
498            // `#[charon::opaque]`
499            "exclude" if args.is_none() => Attribute::Exclude,
500            // `#[charon::rename("new_name")]`
501            "rename" if let Some(attr) = args => {
502                let Some(attr) = attr
503                    .strip_prefix("\"")
504                    .and_then(|attr| attr.strip_suffix("\""))
505                else {
506                    return Err(format!(
507                        "the new name should be between quotes: `rename(\"{attr}\")`."
508                    ));
509                };
510
511                if attr.is_empty() {
512                    return Err(format!("attribute `rename` should not be empty"));
513                }
514
515                let first_char = attr.chars().nth(0).unwrap();
516                let is_identifier = (first_char.is_alphabetic() || first_char == '_')
517                    && attr.chars().all(|c| c.is_alphanumeric() || c == '_');
518                if !is_identifier {
519                    return Err(format!(
520                        "attribute `rename` should contain a valid identifier"
521                    ));
522                }
523
524                Attribute::Rename(attr.to_string())
525            }
526            // `#[charon::variants_prefix("T")]`
527            "variants_prefix" if let Some(attr) = args => {
528                let Some(attr) = attr
529                    .strip_prefix("\"")
530                    .and_then(|attr| attr.strip_suffix("\""))
531                else {
532                    return Err(format!(
533                        "the name should be between quotes: `variants_prefix(\"{attr}\")`."
534                    ));
535                };
536
537                Attribute::VariantsPrefix(attr.to_string())
538            }
539            // `#[charon::variants_suffix("T")]`
540            "variants_suffix" if let Some(attr) = args => {
541                let Some(attr) = attr
542                    .strip_prefix("\"")
543                    .and_then(|attr| attr.strip_suffix("\""))
544                else {
545                    return Err(format!(
546                        "the name should be between quotes: `variants_suffix(\"{attr}\")`."
547                    ));
548                };
549
550                Attribute::VariantsSuffix(attr.to_string())
551            }
552            // `#[verify::start_from]`
553            "start_from" => {
554                if matches!(def_id.kind, hax::DefKind::Mod) {
555                    return Err("`start_from` on modules has no effect".to_string());
556                }
557                Attribute::Unknown(raw_attr.clone())
558            }
559            // `#[verify::test]`: mark a function for test extraction
560            "test" if args.is_none() => Attribute::Unknown(raw_attr.clone()),
561            _ => return Ok(None),
562        };
563        Ok(Some(parsed))
564    }
565
566    /// Translates a rust attribute. Returns `None` if the attribute is a doc comment (rustc
567    /// encodes them as attributes). For now we use `String`s for `Attributes`.
568    pub(crate) fn translate_attribute(
569        &mut self,
570        def_id: &hax::DefId,
571        attr: &rustc_hir::Attribute,
572    ) -> Option<Attribute> {
573        use rustc_hir as hir;
574        use rustc_hir::attrs as hir_attrs;
575        match attr {
576            hir::Attribute::Parsed(hir_attrs::AttributeKind::DocComment { comment, .. }) => {
577                Some(Attribute::DocComment(comment.to_string()))
578            }
579            hir::Attribute::Parsed(_) => None,
580            hir::Attribute::Unparsed(attr) => {
581                let raw_attr = RawAttribute {
582                    path: attr.path.to_string(),
583                    args: match &attr.args {
584                        hir::AttrArgs::Empty => None,
585                        hir::AttrArgs::Delimited(args) => {
586                            Some(rustc_ast_pretty::pprust::tts_to_string(&args.tokens))
587                        }
588                        hir::AttrArgs::Eq { expr, .. } => {
589                            self.tcx.sess.source_map().span_to_snippet(expr.span).ok()
590                        }
591                    },
592                };
593                match self.parse_attr_from_raw(def_id, raw_attr) {
594                    Ok(a) => Some(a),
595                    Err(msg) => {
596                        let span = self.translate_span(&attr.span.sinto(&self.hax_state));
597                        register_error!(self, span, "Error parsing attribute: {msg}");
598                        None
599                    }
600                }
601            }
602        }
603    }
604
605    pub(crate) fn translate_inline(&self, def: &hax::FullDef<'tcx>) -> Option<InlineAttr> {
606        match def.kind() {
607            hax::FullDefKind::Fn { inline, .. }
608            | hax::FullDefKind::AssocFn { inline, .. }
609            | hax::FullDefKind::Closure { inline, .. } => match inline {
610                hax::InlineAttr::None => None,
611                hax::InlineAttr::Hint => Some(InlineAttr::Hint),
612                hax::InlineAttr::Never => Some(InlineAttr::Never),
613                hax::InlineAttr::Always => Some(InlineAttr::Always),
614                hax::InlineAttr::Force { .. } => Some(InlineAttr::Always),
615            },
616            _ => None,
617        }
618    }
619
620    pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef<'tcx>) -> AttrInfo {
621        // Default to `false` for impl blocks and closures.
622        let public = def.visibility.unwrap_or(false);
623        let inline = self.translate_inline(def);
624        let attributes = def
625            .attributes
626            .iter()
627            .filter_map(|attr| self.translate_attribute(def.def_id(), attr))
628            .collect_vec();
629
630        let rename = {
631            let mut renames = attributes.iter().filter_map(|a| a.as_rename()).cloned();
632            let rename = renames.next();
633            if renames.next().is_some() {
634                let span = self.translate_span(&def.span);
635                register_error!(
636                    self,
637                    span,
638                    "There should be at most one `charon::rename(\"...\")` \
639                    or `aeneas::rename(\"...\")` attribute per declaration",
640                );
641            }
642            rename
643        };
644
645        AttrInfo {
646            attributes,
647            inline,
648            public,
649            rename,
650        }
651    }
652}
653
654// `ItemMeta`
655impl<'tcx> TranslateCtx<'tcx> {
656    /// Whether this item is in an `extern { .. }` block, in which case it has no body.
657    pub(crate) fn is_extern_item(&mut self, def: &hax::FullDef<'tcx>) -> bool {
658        def.def_id()
659            .parent(&self.hax_state)
660            .is_some_and(|parent| matches!(parent.kind, hax::DefKind::ForeignMod))
661    }
662
663    /// If this is an item declared in an `extern { .. }` block, return its symbol name.
664    pub(crate) fn extern_item_symbol_name(&mut self, def: &hax::FullDef<'tcx>) -> Option<String> {
665        if !self.is_extern_item(def) {
666            return None;
667        }
668        let path_item = def.def_id().path_item(&self.hax_state);
669        match path_item.data {
670            hax::DefPathItem::ValueNs(name) | hax::DefPathItem::TypeNs(name) => {
671                Some(name.to_string())
672            }
673            _ => None,
674        }
675    }
676
677    /// Compute the meta information for a Rust item.
678    pub(crate) fn translate_item_meta(
679        &mut self,
680        def: &hax::FullDef<'tcx>,
681        item_src: &TransItemSource,
682        name: Name,
683        name_opacity: ItemOpacity,
684    ) -> ItemMeta {
685        if let Some(item_meta) = self.cached_item_metas.get(item_src) {
686            return item_meta.clone();
687        }
688        let span = def.source_span.as_ref().unwrap_or(&def.span);
689        let span = self.translate_span(span);
690        let is_local = def.def_id().is_local();
691        let (attr_info, lang_item) = if !item_src.is_derived_item()
692            || matches!(item_src.kind, TransItemSourceKind::ClosureMethod(..))
693        {
694            let attr_info = self.translate_attr_info(def);
695            let lang_item = def.lang_item.or(def.diagnostic_item).map(|s| s.to_string());
696            (attr_info, lang_item)
697        } else {
698            (AttrInfo::default(), None)
699        };
700
701        let opacity = if attr_info.attributes.iter().any(|attr| attr.is_exclude()) {
702            ItemOpacity::Invisible.max(name_opacity)
703        } else if self.is_extern_item(def)
704            || attr_info.attributes.iter().any(|attr| attr.is_opaque())
705        {
706            // Force opaque in these cases.
707            ItemOpacity::Opaque.max(name_opacity)
708        } else {
709            name_opacity
710        };
711
712        let item_meta = ItemMeta {
713            name,
714            span,
715            source_text: def.source_text.clone(),
716            attr_info,
717            is_local,
718            opacity,
719            lang_item,
720        };
721        self.cached_item_metas
722            .insert(item_src.clone(), item_meta.clone());
723        item_meta
724    }
725}
charon_driver/translate/translate_meta.rs

charon_driver/translate/
translate_meta.rs
