charon_lib/ast/items/
global_decl.rs

1use crate::ast::*;
2use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
3use serde_state::DeserializeState;
4use serde_state::SerializeState;
5
6/// A global variable definition (constant or static).
7#[derive(Debug, Clone)]
8#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
9pub struct GlobalDecl {
10    pub def_id: GlobalDeclId,
11    /// The meta data associated with the declaration.
12    pub item_meta: ItemMeta,
13    /// Remark: constants can actually have generic parameters.
14    /// ```text
15    /// struct V<const N: usize, T> {
16    ///     x: [T; N],
17    /// }
18    ///
19    /// impl<const N: usize, T> V<N, T> {
20    ///     const LEN: usize = N; // This has generics <N, T>
21    /// }
22    ///
23    /// fn use_v<const N: usize, T>(v: V<N, T>) {
24    ///     let l = V::<N, T>::LEN; // We need to provided a substitution here
25    /// }
26    /// ```
27    pub generics: GenericParams,
28    pub ty: Ty,
29    /// The size in bytes of the global's allocation.
30    pub size: Size,
31    /// The alignment in bytes of the global's allocation.
32    pub align: Size,
33    /// The pointer metadata for references to this global (needed for unsized globals).
34    pub ptr_metadata: Operand,
35    /// The context of the global: distinguishes normal items from trait-associated items and
36    /// vtable instances.
37    pub src: GlobalSource,
38    /// The kind of global (static or const).
39    pub global_kind: GlobalKind,
40    /// The value of this constant/static. By default this is a [`ConstantExprKind::Call`] to the
41    /// initializer function that computes the value (the function uses the same generic parameters
42    /// as the global).
43    pub value: ConstantExpr,
44}
45
46#[derive(Debug, Clone, PartialEq, Eq)]
47#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
48pub enum GlobalKind {
49    /// A static or thread-local static.
50    Static {
51        is_mut: bool,
52        /// `false` for statics declared in an `extern` block without the `safe` qualifier.
53        is_safe: bool,
54        /// `true` for thread-local statics (through `thread_local!` or `#[thread_local]`).
55        is_thread_local: bool,
56    },
57    /// A const with a name (either top-level or an associated const in a trait).
58    NamedConst,
59    /// A const without a name:
60    /// - An inline const expression (`const { 1 + 1 }`);
61    /// - A const expression in a type (`[u8; sizeof::<T>()]`);
62    /// - A promoted constant, automatically lifted from a body (`&0`).
63    AnonConst,
64    /// The VTable of a trait implementation. Such globals can only be accessed by the generated
65    /// code -- it is UB to access them from user code.
66    #[cfg_attr(feature = "charon_on_charon", charon::rename("VTableGlobal"))]
67    VTable,
68}
69
70/// Where a given global came from.
71#[derive(Debug, Clone)]
72#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
73#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Global"))]
74pub enum GlobalSource {
75    /// A normal global.
76    Normal,
77    /// A default assoc const in a trait declaration.
78    TraitDefault {
79        /// The trait declaration the const belongs to.
80        trait_ref: TraitDeclRef,
81        /// The associated const this corresponds to.
82        item_id: AssocConstId,
83    },
84    /// An associated const in a trait implementation.
85    TraitImpl {
86        /// The trait implementation the const belongs to.
87        impl_ref: TraitImplRef,
88        /// The trait declaration that the impl block implements.
89        trait_ref: TraitDeclRef,
90        /// The associated const this corresponds to.
91        item_id: AssocConstId,
92        /// True if the trait decl had a default value for this const and this item is a copy of
93        /// the default item.
94        reuses_default: bool,
95    },
96    /// Defines the vtable for a trait impl.
97    VTableInstance {
98        /// The originating impl. This is `None` in monomorphized mode: the vtable global itself
99        /// identifies the concrete instantiation, so we don't translate an impl reference solely
100        /// to record its provenance.
101        impl_ref: Option<TraitImplRef>,
102    },
103}
104
105impl GlobalDecl {
106    /// If this global's value is a call to its initializer function, returns the initializer's id.
107    pub fn init_fun_id(&self) -> Option<FunDeclId> {
108        match self.value.kind() {
109            ConstantExprKind::Call(fn_ptr, _) => match &*fn_ptr.kind {
110                FnPtrKind::Fun(id) => Some(*id),
111                _ => None,
112            },
113            _ => None,
114        }
115    }
116
117    /// Whether this global is unsafe to access, because it is a mutable or unsafe external static (safety.unsafe-static).
118    pub fn is_unsafe_to_access(&self, _krate: &TranslatedCrate) -> bool {
119        match self.global_kind {
120            GlobalKind::Static {
121                is_mut,
122                is_safe,
123                is_thread_local: _,
124            } => is_mut || !is_safe,
125            GlobalKind::NamedConst | GlobalKind::AnonConst | GlobalKind::VTable => false,
126        }
127    }
128
129    /// Whether this global is unsafe to declare.
130    pub fn is_unsafe_to_declare(&self, _krate: &TranslatedCrate) -> bool {
131        self.item_meta.is_unsafe_to_declare()
132    }
133}
charon_lib/ast/items/global_decl.rs

charon_lib/ast/items/
global_decl.rs
