charon_lib/ast/
meta.rs

1//! Meta-information about programs (spans, etc.).
2
3use super::from_rustc::{self, LangItem};
4pub use super::meta_utils::*;
5use crate::ast::{FunDeclId, ItemId};
6use crate::names::Name;
7use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
8use macros::{EnumAsGetters, EnumIsA, EnumToGetters};
9use serde::{Deserialize, Serialize};
10use serde_state::{DeserializeState, SerializeState};
11use std::path::PathBuf;
12
13generate_index_type!(FileId);
14
15#[derive(
16    Debug,
17    Copy,
18    Clone,
19    PartialEq,
20    Eq,
21    PartialOrd,
22    Ord,
23    Hash,
24    Serialize,
25    Deserialize,
26    Drive,
27    DriveMut,
28    DriveTwo,
29)]
30#[drive(skip)]
31pub struct Loc {
32    /// The (1-based) line number.
33    pub line: usize,
34    /// The (0-based) column offset.
35    pub col: usize,
36}
37
38/// Span information
39#[derive(
40    Debug, Copy, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut, DriveTwo,
41)]
42pub struct SpanData {
43    #[cfg_attr(feature = "charon_on_charon", charon::rename("file"))]
44    pub file_id: FileId,
45    #[cfg_attr(feature = "charon_on_charon", charon::rename("beg_loc"))]
46    pub beg: Loc,
47    #[cfg_attr(feature = "charon_on_charon", charon::rename("end_loc"))]
48    pub end: Loc,
49}
50
51/// Meta information about a piece of code (block, statement, etc.)
52#[derive(
53    Debug,
54    Copy,
55    Clone,
56    PartialEq,
57    Eq,
58    PartialOrd,
59    Ord,
60    Hash,
61    Serialize,
62    Deserialize,
63    SerializeState,
64    DeserializeState,
65    Drive,
66    DriveMut,
67    DriveTwo,
68)]
69#[serde_state(stateless)]
70pub struct Span {
71    /// The source code span.
72    ///
73    /// If this meta information is for a statement/terminator coming from a macro
74    /// expansion/inlining/etc., this span is (in case of macros) for the macro
75    /// before expansion (i.e., the location the code where the user wrote the call
76    /// to the macro).
77    ///
78    /// Ex:
79    /// ```text
80    /// // Below, we consider the spans for the statements inside `test`
81    ///
82    /// //   the statement we consider, which gets inlined in `test`
83    ///                          VV
84    /// macro_rules! macro { ... st ... } // `generated_from_span` refers to this location
85    ///
86    /// fn test() {
87    ///     macro!(); // <-- `span` refers to this location
88    /// }
89    /// ```
90    pub data: SpanData,
91    /// Where the code actually comes from, in case of macro expansion/inlining/etc.
92    pub generated_from_span: Option<SpanData>,
93}
94
95/// `#[inline]` built-in attribute.
96#[derive(Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
97pub enum InlineAttr {
98    /// `#[inline]`
99    Hint,
100    /// `#[inline(never)]`
101    Never,
102    /// `#[inline(always)]`
103    Always,
104}
105
106/// Attributes (`#[...]`).
107#[derive(
108    Debug,
109    Clone,
110    PartialEq,
111    Eq,
112    EnumIsA,
113    EnumAsGetters,
114    EnumToGetters,
115    Serialize,
116    Deserialize,
117    Drive,
118    DriveMut,
119    DriveTwo,
120)]
121#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Attr"))]
122pub enum Attribute {
123    /// Do not translate the body of this item.
124    /// Written `#[charon::opaque]`
125    Opaque,
126    /// Do not translate this item at all.
127    /// Written `#[charon::exclude]`
128    Exclude,
129    /// Provide a new name that consumers of the llbc can use.
130    /// Written `#[charon::rename("new_name")]`
131    Rename(String),
132    /// For enums only: rename the variants by pre-pending their names with the given prefix.
133    /// Written `#[charon::variants_prefix("prefix_")]`.
134    VariantsPrefix(String),
135    /// Same as `VariantsPrefix`, but appends to the name instead of pre-pending.
136    VariantsSuffix(String),
137    /// The structure is treated as a transparent wrapper around its sole field.
138    /// Written `#[charon::transparent]`.
139    Transparent,
140    /// An item annotated with `#[charon::precondition]`. This makes it a precondition for its
141    /// parent item.
142    IsPrecondition(ItemId),
143    /// An item annotated with `#[charon::postcondition]`. This makes it a postcondition for its
144    /// parent item.
145    IsPostcondition(ItemId),
146    /// An item that has a precondition that applies to it. The referenced item is a function the
147    /// specifies the condition.
148    HasPrecondition(FunDeclId),
149    /// An item that has a postcondition that applies to it. The referenced item is a function the
150    /// specifies the condition.
151    HasPostcondition(FunDeclId),
152    /// A doc-comment such as `/// ...`.
153    DocComment(String),
154    /// A built-in attribute.
155    Builtin(#[drive(skip)] from_rustc::AttributeKind),
156    /// None of the above.
157    Unknown(RawAttribute),
158}
159
160/// A general attribute.
161#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
162pub struct RawAttribute {
163    pub path: String,
164    /// The arguments passed to the attribute, if any. We don't distinguish different delimiters or
165    /// the `path = lit` case.
166    pub args: Option<String>,
167}
168
169/// Information about the attributes and visibility of an item, field or variant..
170#[derive(
171    Debug, PartialEq, Eq, Default, Clone, Serialize, Deserialize, Drive, DriveMut, DriveTwo,
172)]
173pub struct AttrInfo {
174    /// Attributes (`#[...]`).
175    pub attributes: Vec<Attribute>,
176    /// Inline hints (on functions only).
177    pub inline: Option<InlineAttr>,
178    /// The name computed from `charon::rename` and `charon::variants_prefix` attributes, if any.
179    /// This provides a custom name that can be used by consumers of llbc. E.g. Aeneas uses this to
180    /// rename definitions in the extracted code.
181    pub rename: Option<String>,
182    /// Whether this item is declared public. Impl blocks and closures don't have visibility
183    /// modifiers; we arbitrarily set this to `false` for them.
184    ///
185    /// Note that this is different from being part of the crate's public API: to be part of the
186    /// public API, an item has to also be reachable from public items in the crate root. For
187    /// example:
188    /// ```rust,ignore
189    /// mod foo {
190    ///     pub struct X;
191    /// }
192    /// mod bar {
193    ///     pub fn something(_x: super::foo::X) {}
194    /// }
195    /// pub use bar::something; // exposes `X`
196    /// ```
197    /// Without the `pub use ...`, neither `X` nor `something` would be part of the crate's public
198    /// API (this is called "pub-in-priv" items). With or without the `pub use`, we set `public =
199    /// true`; computing item reachability is harder.
200    pub public: bool,
201}
202
203#[derive(
204    Debug,
205    Copy,
206    Clone,
207    PartialEq,
208    Eq,
209    PartialOrd,
210    Ord,
211    Serialize,
212    Deserialize,
213    Drive,
214    DriveMut,
215    DriveTwo,
216    EnumIsA,
217)]
218pub enum ItemOpacity {
219    /// Translate the item fully.
220    Transparent,
221    /// Translate the item depending on the normal rust visibility of its contents: for types, we
222    /// translate fully if it is a struct with public fields or an enum; for other items this is
223    /// equivalent to `Opaque`.
224    Foreign,
225    /// Translate the item name and signature, but not its contents. For function and globals, this
226    /// means we don't translate the body (the code); for ADTs, this means we don't translate the
227    /// fields/variants. For traits and trait impls, this doesn't change anything. For modules,
228    /// this means we don't explore its contents (we still translate any of its items mentioned
229    /// from somewhere else).
230    ///
231    /// This can happen either if the item was annotated with `#[charon::opaque]` or if it was
232    /// declared opaque via a command-line argument.
233    #[cfg_attr(feature = "charon_on_charon", charon::rename("ItemOpaque"))]
234    Opaque,
235    /// Translate nothing of this item. The corresponding map will not have an entry for the
236    /// `ItemId`. Useful when even the signature of the item causes errors.
237    Invisible,
238}
239
240/// Meta information about an item (function, trait decl, trait impl, type decl, global).
241#[derive(
242    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
243)]
244#[serde_state(stateless)]
245pub struct ItemMeta {
246    #[serde_state(stateful)]
247    pub name: Name,
248    pub span: Span,
249    /// The source code that corresponds to this item.
250    #[drive(skip)]
251    pub source_text: Option<String>,
252    /// Attributes and visibility.
253    pub attr_info: AttrInfo,
254    /// `true` if the type decl is a local type decl, `false` if it comes from an external crate.
255    #[drive(skip)]
256    pub is_local: bool,
257    /// Whether this item is considered opaque. For function and globals, this means we don't
258    /// translate the body (the code); for ADTs, this means we don't translate the fields/variants.
259    /// For traits and trait impls, this doesn't change anything. For modules, this means we don't
260    /// explore its contents (we still translate any of its items mentioned from somewhere else).
261    ///
262    /// This can happen either if the item was annotated with `#[charon::opaque]` or if it was
263    /// declared opaque via a command-line argument.
264    #[drive(skip)]
265    pub opacity: ItemOpacity,
266    /// If the item is a rustc lang item, record which one it is.
267    #[drive(skip)]
268    pub lang_item: Option<LangItem>,
269    /// If the item is a rustc diagnostic item, record its internal identifier.
270    #[drive(skip)]
271    pub diagnostic_item: Option<String>,
272}
273
274/// A filename.
275#[derive(
276    Debug,
277    PartialEq,
278    Eq,
279    Clone,
280    Hash,
281    PartialOrd,
282    Ord,
283    Serialize,
284    Deserialize,
285    Drive,
286    DriveMut,
287    DriveTwo,
288)]
289pub enum FileName {
290    /// A remapped path (namely paths into stdlib)
291    #[drive(skip)] // drive is not implemented for `PathBuf`
292    Virtual(PathBuf),
293    /// A local path (a file coming from the current crate for instance)
294    #[drive(skip)] // drive is not implemented for `PathBuf`
295    Local(PathBuf),
296    /// A "not real" file name (macro, query, etc.)
297    NotReal(String),
298}
299
300#[derive(
301    Debug,
302    PartialEq,
303    Eq,
304    Clone,
305    Hash,
306    PartialOrd,
307    Ord,
308    Serialize,
309    Deserialize,
310    Drive,
311    DriveMut,
312    DriveTwo,
313)]
314pub struct File {
315    /// The file identifier.
316    #[cfg_attr(feature = "charon_on_charon", charon::opaque)]
317    pub id: FileId,
318    /// The path to the file.
319    #[drive(skip)]
320    pub name: FileName,
321    /// Name of the crate this file comes from.
322    pub crate_name: String,
323    /// The contents of the source file, as seen by rustc at the time of translation.
324    /// Some files don't have contents.
325    pub contents: Option<String>,
326}
charon_lib/ast/meta.rs

charon_lib/ast/
meta.rs
