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(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(Debug, Default, Clone, Serialize, Deserialize, Drive, DriveMut, DriveTwo)]
80pub struct AttrInfo {
81    /// Attributes (`#[...]`).
82    pub attributes: Vec<Attribute>,
83    /// Inline hints (on functions only).
84    pub inline: Option<InlineAttr>,
85    /// The name computed from `charon::rename` and `charon::variants_prefix` attributes, if any.
86    /// This provides a custom name that can be used by consumers of llbc. E.g. Aeneas uses this to
87    /// rename definitions in the extracted code.
88    pub rename: Option<String>,
89    /// Whether this item is declared public. Impl blocks and closures don't have visibility
90    /// modifiers; we arbitrarily set this to `false` for them.
91    ///
92    /// Note that this is different from being part of the crate's public API: to be part of the
93    /// public API, an item has to also be reachable from public items in the crate root. For
94    /// example:
95    /// ```rust,ignore
96    /// mod foo {
97    ///     pub struct X;
98    /// }
99    /// mod bar {
100    ///     pub fn something(_x: super::foo::X) {}
101    /// }
102    /// pub use bar::something; // exposes `X`
103    /// ```
104    /// Without the `pub use ...`, neither `X` nor `something` would be part of the crate's public
105    /// API (this is called "pub-in-priv" items). With or without the `pub use`, we set `public =
106    /// true`; computing item reachability is harder.
107    pub public: bool,
108}
109
110impl AttrInfo {
111    pub fn dummy_private() -> Self {
112        AttrInfo {
113            public: false,
114            ..Default::default()
115        }
116    }
117
118    pub fn dummy_public() -> Self {
119        AttrInfo {
120            public: true,
121            ..Default::default()
122        }
123    }
124}
charon_lib/ast/meta/attrs.rs

charon_lib/ast/meta/
attrs.rs
