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)]
27pub struct Loc {
28    /// The (1-based) line number.
29    pub line: usize,
30    /// The (0-based) column offset.
31    pub col: usize,
32}
33
34/// Span information
35#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
36pub struct SpanData {
37    #[charon::rename("file")]
38    pub file_id: FileId,
39    #[charon::rename("beg_loc")]
40    pub beg: Loc,
41    #[charon::rename("end_loc")]
42    pub end: Loc,
43}
44
45/// Meta information about a piece of code (block, statement, etc.)
46#[derive(
47    Debug,
48    Copy,
49    Clone,
50    PartialEq,
51    Eq,
52    PartialOrd,
53    Ord,
54    Hash,
55    Serialize,
56    Deserialize,
57    SerializeState,
58    DeserializeState,
59    Drive,
60    DriveMut,
61)]
62#[drive(skip)]
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#[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    /// A doc-comment such as `/// ...`.
131    DocComment(String),
132    /// A non-charon-specific attribute.
133    Unknown(RawAttribute),
134}
135
136/// A general attribute.
137#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
138pub struct RawAttribute {
139    pub path: String,
140    /// The arguments passed to the attribute, if any. We don't distinguish different delimiters or
141    /// the `path = lit` case.
142    pub args: Option<String>,
143}
144
145/// Information about the attributes and visibility of an item, field or variant..
146#[derive(Debug, Default, Clone, Serialize, Deserialize, Drive, DriveMut)]
147pub struct AttrInfo {
148    /// Attributes (`#[...]`).
149    pub attributes: Vec<Attribute>,
150    /// Inline hints (on functions only).
151    pub inline: Option<InlineAttr>,
152    /// The name computed from `charon::rename` and `charon::variants_prefix` attributes, if any.
153    /// This provides a custom name that can be used by consumers of llbc. E.g. Aeneas uses this to
154    /// rename definitions in the extracted code.
155    pub rename: Option<String>,
156    /// Whether this item is declared public. Impl blocks and closures don't have visibility
157    /// modifiers; we arbitrarily set this to `false` for them.
158    ///
159    /// Note that this is different from being part of the crate's public API: to be part of the
160    /// public API, an item has to also be reachable from public items in the crate root. For
161    /// example:
162    /// ```rust,ignore
163    /// mod foo {
164    ///     pub struct X;
165    /// }
166    /// mod bar {
167    ///     pub fn something(_x: super::foo::X) {}
168    /// }
169    /// pub use bar::something; // exposes `X`
170    /// ```
171    /// Without the `pub use ...`, neither `X` nor `something` would be part of the crate's public
172    /// API (this is called "pub-in-priv" items). With or without the `pub use`, we set `public =
173    /// true`; computing item reachability is harder.
174    pub public: bool,
175}
176
177#[derive(
178    Debug,
179    Copy,
180    Clone,
181    PartialEq,
182    Eq,
183    PartialOrd,
184    Ord,
185    Serialize,
186    Deserialize,
187    Drive,
188    DriveMut,
189    EnumIsA,
190)]
191pub enum ItemOpacity {
192    /// Translate the item fully.
193    Transparent,
194    /// Translate the item depending on the normal rust visibility of its contents: for types, we
195    /// translate fully if it is a struct with public fields or an enum; for other items this is
196    /// equivalent to `Opaque`.
197    Foreign,
198    /// Translate the item name and signature, but not its contents. For function and globals, this
199    /// means we don't translate the body (the code); for ADTs, this means we don't translate the
200    /// fields/variants. For traits and trait impls, this doesn't change anything. For modules,
201    /// this means we don't explore its contents (we still translate any of its items mentioned
202    /// from somewhere else).
203    ///
204    /// This can happen either if the item was annotated with `#[charon::opaque]` or if it was
205    /// declared opaque via a command-line argument.
206    Opaque,
207    /// Translate nothing of this item. The corresponding map will not have an entry for the
208    /// `ItemId`. Useful when even the signature of the item causes errors.
209    Invisible,
210}
211
212/// Meta information about an item (function, trait decl, trait impl, type decl, global).
213#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
214#[serde_state(stateless)]
215pub struct ItemMeta {
216    #[serde_state(stateful)]
217    pub name: Name,
218    pub span: Span,
219    /// The source code that corresponds to this item.
220    #[drive(skip)]
221    pub source_text: Option<String>,
222    /// Attributes and visibility.
223    #[drive(skip)]
224    pub attr_info: AttrInfo,
225    /// `true` if the type decl is a local type decl, `false` if it comes from an external crate.
226    #[drive(skip)]
227    pub is_local: bool,
228    /// Whether this item is considered opaque. For function and globals, this means we don't
229    /// translate the body (the code); for ADTs, this means we don't translate the fields/variants.
230    /// For traits and trait impls, this doesn't change anything. For modules, this means we don't
231    /// explore its contents (we still translate any of its items mentioned from somewhere else).
232    ///
233    /// This can happen either if the item was annotated with `#[charon::opaque]` or if it was
234    /// declared opaque via a command-line argument.
235    #[charon::opaque]
236    #[drive(skip)]
237    pub opacity: ItemOpacity,
238    /// If the item is built-in, record its internal builtin identifier.
239    #[drive(skip)]
240    pub lang_item: Option<String>,
241}
242
243/// A filename.
244#[derive(
245    Debug, PartialEq, Eq, Clone, Hash, PartialOrd, Ord, Serialize, Deserialize, Drive, DriveMut,
246)]
247pub enum FileName {
248    /// A remapped path (namely paths into stdlib)
249    #[drive(skip)] // drive is not implemented for `PathBuf`
250    Virtual(PathBuf),
251    /// A local path (a file coming from the current crate for instance)
252    #[drive(skip)] // drive is not implemented for `PathBuf`
253    Local(PathBuf),
254    /// A "not real" file name (macro, query, etc.)
255    NotReal(String),
256}
257
258#[derive(
259    Debug, PartialEq, Eq, Clone, Hash, PartialOrd, Ord, Serialize, Deserialize, Drive, DriveMut,
260)]
261pub struct File {
262    /// The path to the file.
263    pub name: FileName,
264    /// Name of the crate this file comes from.
265    pub crate_name: String,
266    /// The contents of the source file, as seen by rustc at the time of translation.
267    /// Some files don't have contents.
268    pub contents: Option<String>,
269}
charon_lib/ast/meta.rs

charon_lib/ast/
meta.rs
