charon_lib/ast/
meta.rs

1//! Meta information about programs (spans, etc.).
2use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
3use macros::EnumIsA;
4use serde::{Deserialize, Serialize};
5use serde_state::{DeserializeState, SerializeState};
6
7use super::from_rustc::LangItem;
8
9pub mod attrs;
10pub mod names;
11pub mod spans;
12
13pub use attrs::*;
14pub use names::*;
15pub use spans::*;
16
17/// How much to translate for a given item.
18#[derive(
19    Debug,
20    Copy,
21    Clone,
22    PartialEq,
23    Eq,
24    PartialOrd,
25    Ord,
26    Serialize,
27    Deserialize,
28    Drive,
29    DriveMut,
30    DriveTwo,
31    EnumIsA,
32)]
33pub enum ItemOpacity {
34    /// Translate the item fully.
35    Transparent,
36    /// Translate the item depending on the normal rust visibility of its contents: for types, we
37    /// translate fully if it is a struct with public fields or an enum; for other items this is
38    /// equivalent to `Opaque`.
39    Foreign,
40    /// Translate the item name and signature, but not its contents. For function and globals, this
41    /// means we don't translate the body (the code); for ADTs, this means we don't translate the
42    /// fields/variants. For traits and trait impls, this doesn't change anything. For modules,
43    /// this means we don't explore its contents (we still translate any of its items mentioned
44    /// from somewhere else).
45    ///
46    /// This can happen either if the item was annotated with `#[charon::opaque]` or if it was
47    /// declared opaque via a command-line argument.
48    #[cfg_attr(feature = "charon_on_charon", charon::rename("ItemOpaque"))]
49    Opaque,
50    /// Translate nothing of this item. The corresponding map will not have an entry for the
51    /// `ItemId`. Useful when even the signature of the item causes errors.
52    Invisible,
53}
54
55/// Meta information about an item (function, trait decl, trait impl, type decl, global).
56#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
57#[serde_state(stateless)]
58pub struct ItemMeta {
59    #[serde_state(stateful)]
60    pub name: Name,
61    pub span: Span,
62    /// The source code that corresponds to this item.
63    pub source_text: Option<String>,
64    /// Attributes and visibility.
65    pub attr_info: AttrInfo,
66    /// `true` if the type decl is a local type decl, `false` if it comes from an external crate.
67    pub is_local: bool,
68    /// Whether this item is considered opaque. For function and globals, this means we don't
69    /// translate the body (the code); for ADTs, this means we don't translate the fields/variants.
70    /// For traits and trait impls, this doesn't change anything. For modules, this means we don't
71    /// explore its contents (we still translate any of its items mentioned from somewhere else).
72    ///
73    /// This can happen either if the item was annotated with `#[charon::opaque]` or if it was
74    /// declared opaque via a command-line argument.
75    pub opacity: ItemOpacity,
76    /// If the item is a rustc lang item, record which one it is.
77    pub lang_item: Option<LangItem>,
78    /// If the item is a rustc diagnostic item, record its internal identifier.
79    pub diagnostic_item: Option<String>,
80}
81
82impl ItemOpacity {
83    pub fn with_content_visibility(self, contents_are_public: bool) -> Self {
84        use ItemOpacity::*;
85        match self {
86            Invisible => Invisible,
87            Transparent => Transparent,
88            Foreign if contents_are_public => Transparent,
89            Foreign => Opaque,
90            Opaque => Opaque,
91        }
92    }
93
94    pub fn with_private_contents(self) -> Self {
95        self.with_content_visibility(false)
96    }
97}
98
99impl ItemMeta {
100    pub fn renamed_name(&self) -> Name {
101        let mut name = self.name.clone();
102        if let Some(rename) = self.attr_info.rename.clone() {
103            *name.name.last_mut().unwrap() = PathElem::Ident(rename, Disambiguator::new(0));
104        }
105        name
106    }
107
108    pub fn dummy_public(span: Span, name: Name, is_local: bool, opacity: ItemOpacity) -> Self {
109        ItemMeta {
110            name,
111            span,
112            source_text: None,
113            attr_info: AttrInfo::dummy_public(),
114            is_local,
115            opacity,
116            lang_item: None,
117            diagnostic_item: None,
118        }
119    }
120}
charon_lib/ast/meta.rs

charon_lib/ast/
meta.rs
