charon_lib/ast/meta/
attrs.rs

1use crate::ast::*;
2use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
3use macros::{EnumAsGetters, EnumIsA, EnumToGetters};
4use serde::{Deserialize, Serialize};
5
6/// `#[inline]` built-in attribute.
7#[derive(Debug, Copy, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
8pub enum InlineAttr {
9    /// `#[inline]`
10    Hint,
11    /// `#[inline(never)]`
12    Never,
13    /// `#[inline(always)]`
14    Always,
15}
16
17/// Attributes (`#[...]`).
18#[derive(
19    Debug,
20    Clone,
21    PartialEq,
22    Eq,
23    EnumIsA,
24    EnumAsGetters,
25    EnumToGetters,
26    Serialize,
27    Deserialize,
28    Drive,
29    DriveMut,
30    DriveTwo,
31)]
32#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Attr"))]
33pub enum Attribute {
34    /// Do not translate the body of this item.
35    /// Written `#[charon::opaque]`
36    Opaque,
37    /// Do not translate this item at all.
38    /// Written `#[charon::exclude]`
39    Exclude,
40    /// Provide a new name that consumers of the llbc can use.
41    /// Written `#[charon::rename("new_name")]`
42    Rename(String),
43    /// For enums only: rename the variants by pre-pending their names with the given prefix.
44    /// Written `#[charon::variants_prefix("prefix_")]`.
45    VariantsPrefix(String),
46    /// Same as `VariantsPrefix`, but appends to the name instead of pre-pending.
47    VariantsSuffix(String),
48    /// The structure is treated as a transparent wrapper around its sole field.
49    /// Written `#[charon::transparent]`.
50    Transparent,
51    /// An item annotated with `#[charon::contract(kind = "...", parent)]` or
52    /// `#[charon::contract(kind = "...", for = "...")]`. This makes it a contract for the target
53    /// item.
54    IsContract {
55        kind: String,
56        target: MaybeAssocItemId,
57    },
58    /// An item that has a contract that applies to it. The referenced item is the function that
59    /// specifies the contract.
60    HasContract { kind: String, contract: FunDeclId },
61    /// A doc-comment such as `/// ...`.
62    DocComment(String),
63    /// A built-in attribute.
64    Builtin(#[drive(skip)] from_rustc::AttributeKind),
65    /// None of the above.
66    Unknown(RawAttribute),
67}
68
69/// A general attribute.
70#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
71pub struct RawAttribute {
72    pub path: String,
73    /// The arguments passed to the attribute, if any. We don't distinguish different delimiters or
74    /// the `path = lit` case.
75    pub args: Option<String>,
76}
77
78/// Information about the attributes and visibility of an item, field or variant..
79#[derive(
80    Debug, PartialEq, Eq, Default, Clone, Serialize, Deserialize, Drive, DriveMut, DriveTwo,
81)]
82pub struct AttrInfo {
83    /// Attributes (`#[...]`).
84    pub attributes: Vec<Attribute>,
85    /// Inline hints (on functions only).
86    pub inline: Option<InlineAttr>,
87    /// The name computed from `charon::rename` and `charon::variants_prefix` attributes, if any.
88    /// This provides a custom name that can be used by consumers of llbc. E.g. Aeneas uses this to
89    /// rename definitions in the extracted code.
90    pub rename: Option<String>,
91    /// Whether this item is declared public. Impl blocks and closures don't have visibility
92    /// modifiers; we arbitrarily set this to `false` for them.
93    ///
94    /// Note that this is different from being part of the crate's public API: to be part of the
95    /// public API, an item has to also be reachable from public items in the crate root. For
96    /// example:
97    /// ```rust,ignore
98    /// mod foo {
99    ///     pub struct X;
100    /// }
101    /// mod bar {
102    ///     pub fn something(_x: super::foo::X) {}
103    /// }
104    /// pub use bar::something; // exposes `X`
105    /// ```
106    /// Without the `pub use ...`, neither `X` nor `something` would be part of the crate's public
107    /// API (this is called "pub-in-priv" items). With or without the `pub use`, we set `public =
108    /// true`; computing item reachability is harder.
109    pub public: bool,
110}
111
112impl AttrInfo {
113    pub fn dummy_private() -> Self {
114        AttrInfo {
115            public: false,
116            ..Default::default()
117        }
118    }
119
120    pub fn dummy_public() -> Self {
121        AttrInfo {
122            public: true,
123            ..Default::default()
124        }
125    }
126}
charon_lib/ast/meta/attrs.rs

charon_lib/ast/meta/
attrs.rs
