charon_lib/ast/
meta.rs

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

charon_lib/ast/
meta.rs
