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(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord)]
19#[derive(EnumIsA)]
20#[derive(Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
21pub enum ItemOpacity {
22    /// Translate the item fully.
23    Transparent,
24    /// Translate the item depending on the normal rust visibility of its contents: for types, we
25    /// translate fully if it is a struct with public fields or an enum; for other items this is
26    /// equivalent to `Opaque`.
27    Foreign,
28    /// Translate the item name and signature, but not its contents. For function and globals, this
29    /// means we don't translate the body (the code); for ADTs, this means we don't translate the
30    /// fields/variants. For traits and trait impls, this doesn't change anything. For modules,
31    /// this means we don't explore its contents (we still translate any of its items mentioned
32    /// from somewhere else).
33    ///
34    /// This can happen either if the item was annotated with `#[charon::opaque]` or if it was
35    /// declared opaque via a command-line argument.
36    #[cfg_attr(feature = "charon_on_charon", charon::rename("ItemOpaque"))]
37    Opaque,
38    /// Translate nothing of this item. The corresponding map will not have an entry for the
39    /// `ItemId`. Useful when even the signature of the item causes errors.
40    Invisible,
41}
42
43/// Meta information about an item (function, trait decl, trait impl, type decl, global).
44#[derive(Debug, Clone)]
45#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
46#[serde_state(stateless)]
47pub struct ItemMeta {
48    #[serde_state(stateful)]
49    pub name: Name,
50    pub span: Span,
51    /// The source code that corresponds to this item.
52    pub source_text: Option<String>,
53    /// Attributes and visibility.
54    pub attr_info: AttrInfo,
55    /// `true` if the type decl is a local type decl, `false` if it comes from an external crate.
56    pub is_local: bool,
57    /// Whether this item was selected as a starting point for translation (using `--start-from`,
58    /// or by default all the top-level items in the main crate).
59    pub started_from: bool,
60    /// Whether this item is declared in an `extern { .. }` block.
61    pub is_extern: bool,
62    /// Whether this item is considered opaque. For function and globals, this means we don't
63    /// translate the body (the code); for ADTs, this means we don't translate the fields/variants.
64    /// For traits and trait impls, this doesn't change anything. For modules, this means we don't
65    /// explore its contents (we still translate any of its items mentioned from somewhere else).
66    ///
67    /// This can happen either if the item was annotated with `#[charon::opaque]` or if it was
68    /// declared opaque via a command-line argument.
69    pub opacity: ItemOpacity,
70    /// If the item is a rustc lang item, record which one it is.
71    pub lang_item: Option<LangItem>,
72    /// If the item is a rustc diagnostic item, record its internal identifier.
73    pub diagnostic_item: Option<String>,
74    /// Whether an error occurred while translating this item.
75    pub has_errors: bool,
76}
77
78impl ItemOpacity {
79    pub fn with_content_visibility(self, contents_are_public: bool) -> Self {
80        use ItemOpacity::*;
81        match self {
82            Invisible => Invisible,
83            Transparent => Transparent,
84            Foreign if contents_are_public => Transparent,
85            Foreign => Opaque,
86            Opaque => Opaque,
87        }
88    }
89
90    pub fn with_private_contents(self) -> Self {
91        self.with_content_visibility(false)
92    }
93}
94
95impl ItemMeta {
96    pub fn renamed_name(&self) -> Name {
97        let mut name = self.name.clone();
98        if let Some(rename) = self.attr_info.rename.clone() {
99            *name.name.last_mut().unwrap() = PathElem::Ident(rename, Disambiguator::new(0));
100        }
101        name
102    }
103
104    pub fn dummy_public(span: Span, name: Name, is_local: bool, opacity: ItemOpacity) -> Self {
105        ItemMeta {
106            name,
107            span,
108            source_text: None,
109            attr_info: AttrInfo::dummy_public(),
110            is_local,
111            started_from: false,
112            is_extern: false,
113            opacity,
114            lang_item: None,
115            diagnostic_item: None,
116            has_errors: false,
117        }
118    }
119
120    /// Whether the item is unsafe to declare: if it is declared in an `extern` block (safety.unsafe-extern),
121    /// or it has an unsafe attribute (safety.unsafe-attribute).
122    pub fn is_unsafe_to_declare(&self) -> bool {
123        self.is_extern
124            || self
125                .attr_info
126                .attributes
127                .iter()
128                .any(|attr| attr.is_unsafe_to_apply())
129    }
130}
charon_lib/ast/meta.rs

charon_lib/ast/
meta.rs
