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, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
8pub struct GlobalDecl {
9    pub def_id: GlobalDeclId,
10    /// The meta data associated with the declaration.
11    pub item_meta: ItemMeta,
12    /// Remark: constants can actually have generic parameters.
13    /// ```text
14    /// struct V<const N: usize, T> {
15    ///     x: [T; N],
16    /// }
17    ///
18    /// impl<const N: usize, T> V<N, T> {
19    ///     const LEN: usize = N; // This has generics <N, T>
20    /// }
21    ///
22    /// fn use_v<const N: usize, T>(v: V<N, T>) {
23    ///     let l = V::<N, T>::LEN; // We need to provided a substitution here
24    /// }
25    /// ```
26    pub generics: GenericParams,
27    pub ty: Ty,
28    /// The context of the global: distinguishes normal items from trait-associated items and
29    /// vtable instances.
30    pub src: GlobalSource,
31    /// The kind of global (static or const).
32    pub global_kind: GlobalKind,
33    /// The value of this constant/static. By default this is a [`ConstantExprKind::Call`] to the
34    /// initializer function that computes the value (the function uses the same generic parameters
35    /// as the global).
36    pub value: ConstantExpr,
37}
38
39#[derive(
40    Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
41)]
42pub enum GlobalKind {
43    /// A static.
44    Static,
45    /// A thread-local static.
46    ThreadLocal,
47    /// A const with a name (either top-level or an associated const in a trait).
48    NamedConst,
49    /// A const without a name:
50    /// - An inline const expression (`const { 1 + 1 }`);
51    /// - A const expression in a type (`[u8; sizeof::<T>()]`);
52    /// - A promoted constant, automatically lifted from a body (`&0`).
53    AnonConst,
54}
55
56/// Where a given global came from.
57#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
58#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Global"))]
59pub enum GlobalSource {
60    /// A normal global.
61    Normal,
62    /// A default assoc const in a trait declaration.
63    TraitDefault {
64        /// The trait declaration the const belongs to.
65        trait_ref: TraitDeclRef,
66        /// The associated const this corresponds to.
67        item_id: AssocConstId,
68    },
69    /// An associated const in a trait implementation.
70    TraitImpl {
71        /// The trait implementation the const belongs to.
72        impl_ref: TraitImplRef,
73        /// The trait declaration that the impl block implements.
74        trait_ref: TraitDeclRef,
75        /// The associated const this corresponds to.
76        item_id: AssocConstId,
77        /// True if the trait decl had a default value for this const and this item is a copy of
78        /// the default item.
79        reuses_default: bool,
80    },
81    /// Defines the vtable for a trait impl.
82    VTableInstance {
83        /// The originating impl. This is `None` in monomorphized mode: the vtable global itself
84        /// identifies the concrete instantiation, so we don't translate an impl reference solely
85        /// to record its provenance.
86        impl_ref: Option<TraitImplRef>,
87    },
88}
89
90impl GlobalDecl {
91    /// If this global's value is a call to its initializer function, returns the initializer's id.
92    pub fn init_fun_id(&self) -> Option<FunDeclId> {
93        match self.value.kind() {
94            ConstantExprKind::Call(fn_ptr, _) => match &*fn_ptr.kind {
95                FnPtrKind::Fun(id) => Some(*id),
96                _ => None,
97            },
98            _ => None,
99        }
100    }
101}
charon_lib/ast/items/global_decl.rs

charon_lib/ast/items/
global_decl.rs
