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

charon_driver/translate/
translate_meta.rs
