charon_lib/ast/items/
fun_decl.rs

1use crate::ast::*;
2use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
3use macros::EnumIsA;
4use macros::VariantName;
5use serde_state::DeserializeState;
6use serde_state::SerializeState;
7
8/// A function definition
9#[derive(Debug, Clone)]
10#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
11pub struct FunDecl {
12    pub def_id: FunDeclId,
13    /// The meta data associated with the declaration.
14    pub item_meta: ItemMeta,
15    pub generics: GenericParams,
16    /// The signature contains the inputs/output types and ABI details.
17    pub signature: Box<FunSig>,
18    /// The function kind: "regular" function, trait method declaration, etc.
19    pub src: FunSource,
20    /// The function body.
21    pub body: Body,
22}
23
24/// A function signature.
25#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
26#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
27pub struct FunSig {
28    /// Is the function unsafe or not
29    pub is_unsafe: bool,
30    /// The calling convention of this function.
31    pub abi: Abi,
32    /// Whether this is a C-variadic function (its last parameter is `...`).
33    pub is_variadic: bool,
34    pub inputs: Vec<Ty>,
35    pub output: Ty,
36}
37
38#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
39#[derive(VariantName, EnumIsA)]
40#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
41#[serde_state(stateless)]
42#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Abi"))]
43pub enum Abi {
44    Rust,
45    C,
46    /// Rust's spelling for the ABI, e.g. "C-unwind" or "system".
47    Other(ustr::Ustr),
48}
49
50/// Where a given function came from.
51#[derive(Debug, Clone)]
52#[derive(SerializeState, DeserializeState, Drive, DriveMut, DriveTwo)]
53#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Fun"))]
54pub enum FunSource {
55    /// A normal function.
56    Normal,
57    /// A synthetic function representing an ADT constructor.
58    AdtConstructor,
59    /// A default method in a trait declaration.
60    TraitDefault {
61        /// The trait declaration this item belongs to.
62        trait_ref: TraitDeclRef,
63        /// The method this corresponds to.
64        // TODO: also include method generics so we can recover a full `FnPtr::TraitMethod`
65        item_id: TraitMethodId,
66    },
67    /// A method in a trait implementation.
68    TraitImpl {
69        /// The trait implementation the method belongs to.
70        impl_ref: TraitImplRef,
71        /// The trait declaration that the impl block implements.
72        trait_ref: TraitDeclRef,
73        /// The method this corresponds to.
74        // TODO: also include method generics so we can recover a full `FnPtr::TraitMethod`
75        item_id: TraitMethodId,
76        /// True if the trait decl had a default implementation for this method and this item is a
77        /// copy of the default item.
78        reuses_default: bool,
79    },
80    /// Wraps a concrete implementation of a method into a function that takes `dyn Trait` as its
81    /// `Self` type. This shim casts the receiver to the known concrete type and calls the real
82    /// method.
83    VTableShim,
84    /// The initializer for a global.
85    GlobalInitializer(GlobalDeclRef),
86    /// A target-specific variant behind a `TargetDispatch` façade. The dispatcher is the function
87    /// with the `Body::TargetDispatch` body that dispatches to this function.
88    TargetDependent { dispatcher: FunDeclRef },
89}
90
91impl FunDecl {
92    /// Replace the generic parameters of this function with the ones given by the binder.
93    pub fn substitute_params(self, subst: Binder<GenericArgs>) -> Self {
94        let FunDecl {
95            def_id,
96            item_meta,
97            generics: _,
98            signature,
99            src,
100            body,
101        } = self;
102        let signature = signature.substitute(&subst.skip_binder);
103        let src = src.substitute(&subst.skip_binder);
104        let body = body.substitute(&subst.skip_binder);
105        FunDecl {
106            def_id,
107            item_meta,
108            generics: subst.params,
109            signature,
110            src,
111            body,
112        }
113    }
114
115    /// Whether this function is unsafe to call, because it is declared `unsafe` (safety.unsafe-call),
116    /// or because it is a safe `#[target_feature]` function (safety.unsafe-target-feature-call). This
117    /// may be overriden at the call site, if we can statically discharge the unsafety (see [`CallSafety`]).
118    pub fn is_unsafe_to_call(&self, _krate: &TranslatedCrate) -> bool {
119        self.signature.is_unsafe
120    }
121
122    /// Whether this function is unsafe to declare.
123    pub fn is_unsafe_to_declare(&self, _krate: &TranslatedCrate) -> bool {
124        // The initializer of a global is part of the global's declaration.
125        !matches!(self.src, FunSource::GlobalInitializer(_))
126            && self.item_meta.is_unsafe_to_declare()
127    }
128}
129
130impl Abi {
131    pub fn rust() -> Self {
132        Self::Rust
133    }
134
135    pub fn rust_name(&self) -> &str {
136        match self {
137            Self::Rust => "Rust",
138            Self::C => "C",
139            Self::Other(name) => name.as_str(),
140        }
141    }
142}
charon_lib/ast/items/fun_decl.rs

charon_lib/ast/items/
fun_decl.rs
