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

charon_driver/translate/
translate_meta.rs
