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

charon_lib/ast/items/
fun_decl.rs
