charon_lib/ast/
meta.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
//! Meta-information about programs (spans, etc.).

pub use super::meta_utils::*;
use crate::names::Name;
use derive_visitor::{Drive, DriveMut};
use macros::{EnumAsGetters, EnumIsA, EnumToGetters};
use serde::{Deserialize, Serialize};
use std::path::PathBuf;

generate_index_type!(FileId);

#[derive(
    Debug,
    Copy,
    Clone,
    PartialEq,
    Eq,
    PartialOrd,
    Ord,
    Hash,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
)]
pub struct Loc {
    /// The (1-based) line number.
    pub line: usize,
    /// The (0-based) column offset.
    pub col: usize,
}

/// For use when deserializing.
#[cfg(feature = "rustc")]
fn dummy_span_data() -> rustc_span::SpanData {
    rustc_span::DUMMY_SP.data()
}

/// Span information
#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
pub struct RawSpan {
    pub file_id: FileId,
    pub beg: Loc,
    pub end: Loc,
    /// We keep the rust span so as to be able to leverage Rustc to print
    /// error messages (useful in the micro-passes for instance).
    /// We use `SpanData` instead of `Span` because `Span` is not `Send` when rustc runs
    /// single-threaded (default on older versions). We need this to be `Send` because we pass this
    /// data out of the rustc callbacks in charon-driver.
    #[cfg(feature = "rustc")]
    #[serde(skip)]
    #[drive(skip)]
    #[serde(default = "dummy_span_data")]
    #[charon::opaque]
    pub rust_span_data: rustc_span::SpanData,
}

#[cfg(feature = "rustc")]
impl From<RawSpan> for rustc_error_messages::MultiSpan {
    fn from(span: RawSpan) -> Self {
        span.rust_span_data.span().into()
    }
}

/// Meta information about a piece of code (block, statement, etc.)
#[derive(
    Debug,
    Copy,
    Clone,
    PartialEq,
    Eq,
    PartialOrd,
    Ord,
    Hash,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
)]
pub struct Span {
    /// The source code span.
    ///
    /// If this meta information is for a statement/terminator coming from a macro
    /// expansion/inlining/etc., this span is (in case of macros) for the macro
    /// before expansion (i.e., the location the code where the user wrote the call
    /// to the macro).
    ///
    /// Ex:
    /// ```text
    /// // Below, we consider the spans for the statements inside `test`
    ///
    /// //   the statement we consider, which gets inlined in `test`
    ///                          VV
    /// macro_rules! macro { ... st ... } // `generated_from_span` refers to this location
    ///
    /// fn test() {
    ///     macro!(); // <-- `span` refers to this location
    /// }
    /// ```
    pub span: RawSpan,
    /// Where the code actually comes from, in case of macro expansion/inlining/etc.
    pub generated_from_span: Option<RawSpan>,
}

#[cfg(feature = "rustc")]
impl From<Span> for rustc_span::Span {
    fn from(span: Span) -> Self {
        span.span.rust_span_data.span()
    }
}

#[cfg(feature = "rustc")]
impl From<Span> for rustc_error_messages::MultiSpan {
    fn from(span: Span) -> Self {
        span.span.into()
    }
}

impl Span {
    #[cfg(feature = "rustc")]
    pub fn rust_span(self) -> rustc_span::Span {
        self.span.rust_span_data.span()
    }
}

/// `#[inline]` built-in attribute.
#[derive(Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
pub enum InlineAttr {
    /// `#[inline]`
    Hint,
    /// `#[inline(never)]`
    Never,
    /// `#[inline(always)]`
    Always,
}

/// Attributes (`#[...]`).
#[derive(
    Debug,
    Clone,
    PartialEq,
    Eq,
    EnumIsA,
    EnumAsGetters,
    EnumToGetters,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
)]
#[charon::variants_prefix("Attr")]
pub enum Attribute {
    /// Do not translate the body of this item.
    /// Written `#[charon::opaque]`
    Opaque,
    /// Provide a new name that consumers of the llbc can use.
    /// Written `#[charon::rename("new_name")]`
    Rename(String),
    /// For enums only: rename the variants by pre-pending their names with the given prefix.
    /// Written `#[charon::variants_prefix("prefix_")]`.
    VariantsPrefix(String),
    /// Same as `VariantsPrefix`, but appends to the name instead of pre-pending.
    VariantsSuffix(String),
    /// A doc-comment such as `/// ...`.
    DocComment(String),
    /// A non-charon-specific attribute.
    Unknown(RawAttribute),
}

/// A general attribute.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
pub struct RawAttribute {
    pub path: String,
    /// The arguments passed to the attribute, if any. We don't distinguish different delimiters or
    /// the `path = lit` case.
    pub args: Option<String>,
}

/// Information about the attributes and visibility of an item, field or variant..
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct AttrInfo {
    /// Attributes (`#[...]`).
    pub attributes: Vec<Attribute>,
    /// Inline hints (on functions only).
    pub inline: Option<InlineAttr>,
    /// The name computed from `charon::rename` and `charon::variants_prefix` attributes, if any.
    /// This provides a custom name that can be used by consumers of llbc. E.g. Aeneas uses this to
    /// rename definitions in the extracted code.
    pub rename: Option<String>,
    /// Whether this item is declared public. Impl blocks and closures don't have visibility
    /// modifiers; we arbitrarily set this to `false` for them.
    ///
    /// Note that this is different from being part of the crate's public API: to be part of the
    /// public API, an item has to also be reachable from public items in the crate root. For
    /// example:
    /// ```rust,ignore
    /// mod foo {
    ///     pub struct X;
    /// }
    /// mod bar {
    ///     pub fn something(_x: super::foo::X) {}
    /// }
    /// pub use bar::something; // exposes `X`
    /// ```
    /// Without the `pub use ...`, neither `X` nor `something` would be part of the crate's public
    /// API (this is called "pub-in-priv" items). With or without the `pub use`, we set `public =
    /// true`; computing item reachability is harder.
    pub public: bool,
}

#[derive(
    Debug,
    Copy,
    Clone,
    PartialEq,
    Eq,
    PartialOrd,
    Ord,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
    EnumIsA,
)]
pub enum ItemOpacity {
    /// Translate the item fully.
    Transparent,
    /// Translate the item depending on the normal rust visibility of its contents: for types, we
    /// translate fully if it is a struct with public fields or an enum; for functions and globals
    /// this is equivalent to `Opaque`; for trait decls and impls this is equivalent to
    /// `Transparent`.
    Foreign,
    /// Translate the item name and signature, but not its contents. For function and globals, this
    /// means we don't translate the body (the code); for ADTs, this means we don't translate the
    /// fields/variants. For traits and trait impls, this doesn't change anything. For modules,
    /// this means we don't explore its contents (we still translate any of its items mentioned
    /// from somewhere else).
    ///
    /// This can happen either if the item was annotated with `#[charon::opaque]` or if it was
    /// declared opaque via a command-line argument.
    Opaque,
    /// Translate nothing of this item. The corresponding map will not have an entry for the
    /// `AnyTransId`. Useful when even the signature of the item causes errors.
    Invisible,
}

/// Meta information about an item (function, trait decl, trait impl, type decl, global).
#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct ItemMeta {
    pub name: Name,
    pub span: Span,
    /// The source code that corresponds to this item.
    pub source_text: Option<String>,
    /// Attributes and visibility.
    pub attr_info: AttrInfo,
    /// `true` if the type decl is a local type decl, `false` if it comes from an external crate.
    pub is_local: bool,
    /// Whether this item is considered opaque. For function and globals, this means we don't
    /// translate the body (the code); for ADTs, this means we don't translate the fields/variants.
    /// For traits and trait impls, this doesn't change anything. For modules, this means we don't
    /// explore its contents (we still translate any of its items mentioned from somewhere else).
    ///
    /// This can happen either if the item was annotated with `#[charon::opaque]` or if it was
    /// declared opaque via a command-line argument.
    #[charon::opaque]
    pub opacity: ItemOpacity,
}

#[derive(Debug, PartialEq, Eq, Clone, Copy, Serialize, Deserialize, Drive, DriveMut)]
pub struct FileInfo {}

/// A filename.
#[derive(
    Debug, PartialEq, Eq, Clone, Hash, PartialOrd, Ord, Serialize, Deserialize, Drive, DriveMut,
)]
pub enum FileName {
    /// A remapped path (namely paths into stdlib)
    #[drive(skip)] // drive is not implemented for `PathBuf`
    Virtual(PathBuf),
    /// A local path (a file coming from the current crate for instance)
    #[drive(skip)] // drive is not implemented for `PathBuf`
    Local(PathBuf),
    /// A "not real" file name (macro, query, etc.)
    #[charon::opaque]
    NotReal(String),
}