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

charon_lib/ast/meta/
attrs.rs
