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

charon_lib/ast/items/
fun_decl.rs
