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

charon_lib/ast/items/
global_decl.rs
