charon_lib/ast/items/
global_decl.rs

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

charon_lib/ast/items/
global_decl.rs
