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

charon_lib/ast/
meta.rs
