charon_lib/ast/
gast.rs

1//! Definitions common to [crate::ullbc_ast] and [crate::llbc_ast]
2use crate::ast::*;
3use crate::common::serialize_map_to_array::SeqHashMapToArray;
4use crate::ids::IndexVec;
5use crate::llbc_ast;
6use crate::ullbc_ast;
7use derive_generic_visitor::{Drive, DriveMut};
8use macros::EnumAsGetters;
9use macros::{EnumIsA, EnumToGetters};
10use serde_state::DeserializeState;
11use serde_state::SerializeState;
12
13/// A variable
14#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
15pub struct Local {
16    /// Unique index identifying the variable
17    pub index: LocalId,
18    /// Variable name - may be `None` if the variable was introduced by Rust
19    /// through desugaring.
20    #[drive(skip)]
21    pub name: Option<String>,
22    /// Span of the variable declaration.
23    pub span: Span,
24    /// The variable type
25    #[charon::rename("local_ty")]
26    pub ty: Ty,
27}
28#[deprecated(note = "use `Local` intead")]
29pub type Var = Local;
30#[deprecated(note = "use `LocalId` intead")]
31pub type VarId = LocalId;
32
33/// The local variables of a body.
34#[derive(
35    Debug, PartialEq, Eq, Default, Clone, SerializeState, DeserializeState, Drive, DriveMut,
36)]
37pub struct Locals {
38    /// The number of local variables used for the input arguments.
39    #[drive(skip)]
40    pub arg_count: usize,
41    /// The local variables.
42    /// We always have, in the following order:
43    /// - the local used for the return value (index 0)
44    /// - the `arg_count` input arguments
45    /// - the remaining locals, used for the intermediate computations
46    pub locals: IndexVec<LocalId, Local>,
47}
48
49/// An expression body.
50/// TODO: arg_count should be stored in GFunDecl below. But then,
51///       the print is obfuscated and Aeneas may need some refactoring.
52#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
53#[charon::rename("GexprBody")]
54pub struct GExprBody<T> {
55    pub span: Span,
56    /// The number of regions existentially bound in this body. We introduce fresh such regions
57    /// during translation instead of the erased regions that rustc gives us.
58    #[drive(skip)]
59    pub bound_body_regions: usize,
60    /// The local variables.
61    pub locals: Locals,
62    /// The statements and blocks that compose this body.
63    pub body: T,
64    /// For each line inside the body, we record any whole-line `//` comments found before it. They
65    /// are added to statements in the late `recover_body_comments` pass.
66    #[charon::opaque]
67    #[drive(skip)]
68    pub comments: Vec<(usize, Vec<String>)>,
69}
70
71/// The body of a function.
72#[derive(
73    Debug,
74    PartialEq,
75    Eq,
76    Clone,
77    SerializeState,
78    DeserializeState,
79    Drive,
80    DriveMut,
81    EnumIsA,
82    EnumAsGetters,
83    EnumToGetters,
84)]
85#[serde_state(state_implements = HashConsSerializerState)]
86#[charon::variants_suffix("Body")]
87pub enum Body {
88    /// Body represented as a CFG. This is what ullbc is made of, and what we get after translating MIR.
89    Unstructured(ullbc_ast::ExprBody),
90    /// Body represented with structured control flow. This is what llbc is made of. We restructure
91    /// the control flow in the `ullbc_to_llbc` pass.
92    Structured(llbc_ast::ExprBody),
93    /// A façade body that dispatches to one of several per-target function bodies. Created during
94    /// multi-target merging for functions with the same signature but different bodies across
95    /// targets.
96    TargetDispatch(
97        #[serde(with = "SeqHashMapToArray::<TargetTriple, FunDeclRef>")]
98        SeqHashMap<TargetTriple, FunDeclRef>,
99    ),
100    /// The body of the function item we add for each trait method declaration, if the trait
101    /// doesn't provide a default for that method.
102    TraitMethodWithoutDefault,
103    /// Function declared in an `extern { ... }` block. The string is the foreign symbol name.
104    Extern(#[drive(skip)] String),
105    /// Rust intrinsic function.
106    Intrinsic {
107        /// The intrinsic name.
108        #[drive(skip)]
109        name: String,
110        /// The argument names, None if not available.
111        #[drive(skip)]
112        arg_names: Vec<Option<String>>,
113    },
114    /// A body that the user chose not to translate, based on opacity settings like
115    /// `--include`/`--opaque`.
116    Opaque,
117    /// A body that was not available. Typically that's function bodies for non-generic and
118    /// non-inlineable std functions, as these are not present in the compiled standard library
119    /// `.rmeta` file shipped with a rust toolchain.
120    Missing,
121    /// We encountered an error while translating this body.
122    #[drive(skip)]
123    #[serde_state(stateless)]
124    Error(Error),
125}
126
127/// Item kind: whether this function/const is part of a trait declaration, trait implementation, or
128/// neither.
129///
130/// Example:
131/// ```text
132/// trait Foo {
133///     fn bar(x : u32) -> u32; // trait item decl without default
134///
135///     fn baz(x : bool) -> bool { x } // trait item decl with default
136/// }
137///
138/// impl Foo for ... {
139///     fn bar(x : u32) -> u32 { x } // trait item implementation
140/// }
141///
142/// fn test(...) { ... } // regular
143///
144/// impl Type {
145///     fn test(...) { ... } // regular
146/// }
147/// ```
148#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, PartialEq, Eq)]
149#[charon::variants_suffix("Item")]
150pub enum ItemSource {
151    /// This item stands on its own.
152    TopLevel,
153    /// This is a closure in a function body.
154    Closure {
155        info: ClosureInfo,
156    },
157    /// This is an associated item in a trait declaration. It has a body if and only if the trait
158    /// provided a default implementation.
159    TraitDecl {
160        /// The trait declaration this item belongs to.
161        trait_ref: TraitDeclRef,
162        /// The associated item this corresponds to.
163        // TODO: also include method generics so we can recover a full `FnPtr::TraitMethod`
164        item_id: AssocItemId,
165        /// Whether the trait declaration provides a default implementation.
166        #[drive(skip)]
167        has_default: bool,
168    },
169    /// This is an associated item in a trait implementation.
170    TraitImpl {
171        /// The trait implementation the method belongs to.
172        impl_ref: TraitImplRef,
173        /// The trait declaration that the impl block implements.
174        trait_ref: TraitDeclRef,
175        /// The associated item this corresponds to.
176        // TODO: also include method generics so we can recover a full `FnPtr::TraitMethod`
177        item_id: AssocItemId,
178        /// True if the trait decl had a default implementation for this function/const and this
179        /// item is a copy of the default item.
180        #[drive(skip)]
181        reuses_default: bool,
182    },
183    /// This function is a target-specific variant behind a `TargetDispatch` façade. The dispatcher
184    /// is the function with the `Body::TargetDispatch` body that dispatches to this function.
185    TargetDependent {
186        dispatcher: FunDeclRef,
187    },
188    /// This is a vtable struct for a trait.
189    VTableTy {
190        /// The `dyn Trait` predicate implemented by this vtable.
191        dyn_predicate: DynPredicate,
192        /// Record what each vtable field means.
193        field_map: IndexVec<FieldId, VTableField>,
194        /// For each implied clause that is also a supertrait clause, reords which field id
195        /// corresponds to it.
196        supertrait_map: IndexVec<TraitClauseId, Option<FieldId>>,
197    },
198    /// This is a vtable value for an impl.
199    VTableInstance {
200        impl_ref: TraitImplRef,
201    },
202    /// The method shim wraps a concrete implementation of a method into a function that takes `dyn
203    /// Trait` as its `Self` type. This shim casts the receiver to the known concrete type and
204    /// calls the real method.
205    VTableMethodShim,
206    VTableInstanceMono,
207}
208
209#[derive(Debug, Clone, SerializeState, DeserializeState, Drive, DriveMut, PartialEq, Eq)]
210#[charon::variants_prefix("VTable")]
211pub enum VTableField {
212    Size,
213    Align,
214    Drop,
215    Method(TraitMethodId),
216    SuperTrait(TraitClauseId),
217}
218
219/// A function definition
220#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
221pub struct FunDecl {
222    pub def_id: FunDeclId,
223    /// The meta data associated with the declaration.
224    pub item_meta: ItemMeta,
225    pub generics: GenericParams,
226    /// The signature contains the inputs/output types *with* non-erased regions.
227    /// It also contains the list of region and type parameters.
228    pub signature: FunSig,
229    /// The function kind: "regular" function, trait method declaration, etc.
230    pub src: ItemSource,
231    /// Whether this function is in fact the body of a constant/static that we turned into an
232    /// initializer function.
233    pub is_global_initializer: Option<GlobalDeclId>,
234    /// The function body.
235    pub body: Body,
236}
237
238/// Reference to a function declaration.
239#[derive(Debug, Clone, SerializeState, DeserializeState, PartialEq, Eq, Hash, Drive, DriveMut)]
240pub struct FunDeclRef {
241    pub id: FunDeclId,
242    /// Generic arguments passed to the function.
243    pub generics: BoxedArgs,
244}
245
246#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
247pub enum GlobalKind {
248    /// A static.
249    Static,
250    /// A const with a name (either top-level or an associated const in a trait).
251    NamedConst,
252    /// A const without a name:
253    /// - An inline const expression (`const { 1 + 1 }`);
254    /// - A const expression in a type (`[u8; sizeof::<T>()]`);
255    /// - A promoted constant, automatically lifted from a body (`&0`).
256    AnonConst,
257}
258
259/// A global variable definition (constant or static).
260#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
261pub struct GlobalDecl {
262    pub def_id: GlobalDeclId,
263    /// The meta data associated with the declaration.
264    pub item_meta: ItemMeta,
265    pub generics: GenericParams,
266    pub ty: Ty,
267    /// The context of the global: distinguishes top-level items from trait-associated items.
268    pub src: ItemSource,
269    /// The kind of global (static or const).
270    #[drive(skip)]
271    pub global_kind: GlobalKind,
272    /// The initializer function used to compute the initial value for this constant/static. It
273    /// uses the same generic parameters as the global.
274    pub init: FunDeclId,
275}
276
277/// Reference to a global declaration.
278#[derive(Debug, Clone, SerializeState, DeserializeState, PartialEq, Eq, Hash, Drive, DriveMut)]
279pub struct GlobalDeclRef {
280    pub id: GlobalDeclId,
281    pub generics: BoxedArgs,
282}
283
284#[derive(
285    Debug,
286    Clone,
287    Copy,
288    SerializeState,
289    DeserializeState,
290    Drive,
291    DriveMut,
292    PartialEq,
293    Eq,
294    Hash,
295    PartialOrd,
296    Ord,
297)]
298#[drive(skip)]
299#[serde_state(stateless)]
300pub struct TraitItemName(pub ustr::Ustr);
301
302generate_index_type!(TraitMethodId, "TraitMethod");
303generate_index_type!(AssocTypeId, "AssocType");
304generate_index_type!(AssocConstId, "AssocConst");
305
306/// A trait **declaration**.
307///
308/// For instance:
309/// ```text
310/// trait Foo {
311///   type Bar;
312///
313///   fn baz(...); // required method (see below)
314///
315///   fn test() -> bool { true } // provided method (see below)
316/// }
317/// ```
318///
319/// In case of a trait declaration, we don't include the provided methods (the methods
320/// with a default implementation): they will be translated on a per-need basis. This is
321/// important for two reasons:
322/// - this makes the trait definitions a lot smaller (the Iterator trait
323///   has *one* declared function and more than 70 provided functions)
324/// - this is important for the external traits, whose provided methods
325///   often use features we don't support yet
326///
327/// Remark:
328/// In Aeneas, we still translate the provided methods on an individual basis,
329/// and in such a way thay they take as input a trait instance. This means that
330/// we can use default methods *but*:
331/// - implementations of required methods shoudln't call default methods
332/// - trait implementations shouldn't redefine required methods
333///
334/// The use case we have in mind is [std::iter::Iterator]: it declares one required
335/// method (`next`) that should be implemented for every iterator, and defines many
336/// helpers like `all`, `map`, etc. that shouldn't be re-implemented.
337/// Of course, this forbids other useful use cases such as visitors implemented
338/// by means of traits.
339#[allow(clippy::type_complexity)]
340#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
341pub struct TraitDecl {
342    pub def_id: TraitDeclId,
343    pub item_meta: ItemMeta,
344    pub generics: GenericParams,
345    /// The "parent" clauses: the supertraits.
346    ///
347    /// Supertraits are actually regular where clauses, but we decided to have
348    /// a custom treatment.
349    /// ```text
350    /// trait Foo : Bar {
351    ///             ^^^
352    ///         supertrait, that we treat as a parent predicate
353    /// }
354    /// ```
355    /// TODO: actually, as of today, we consider that all trait clauses of
356    /// trait declarations are parent clauses.
357    pub implied_clauses: IndexVec<TraitClauseId, TraitParam>,
358    /// The associated constants declared in the trait.
359    pub consts: IndexMap<AssocConstId, TraitAssocConst>,
360    /// The associated types declared in the trait. The binder binds the generic parameters of the
361    /// type if it is a GAT (Generic Associated Type). For a plain associated type the binder binds
362    /// nothing.
363    pub types: IndexMap<AssocTypeId, Binder<TraitAssocTy>>,
364    /// The methods declared by the trait. The binder binds the generic parameters of the method.
365    ///
366    /// ```rust
367    /// trait Trait<T> {
368    ///   // The `Binder` for this method binds `'a` and `U`.
369    ///   fn method<'a, U>(x: &'a U);
370    /// }
371    /// ```
372    pub methods: IndexMap<TraitMethodId, Binder<TraitMethod>>,
373    /// The virtual table struct for this trait, if it has one.
374    /// It is guaranteed that the trait has a vtable iff it is dyn-compatible.
375    pub vtable: Option<TypeDeclRef>,
376}
377
378/// An associated constant in a trait.
379#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
380pub struct TraitAssocConst {
381    pub name: TraitItemName,
382    #[drive(skip)]
383    #[serde_state(stateless)]
384    pub attr_info: AttrInfo,
385    pub ty: Ty,
386    pub default: Option<GlobalDeclRef>,
387}
388
389/// An associated type in a trait.
390#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
391pub struct TraitAssocTy {
392    pub name: TraitItemName,
393    #[drive(skip)]
394    #[serde_state(stateless)]
395    pub attr_info: AttrInfo,
396    pub default: Option<TraitAssocTyImpl>,
397    /// List of trait clauses that apply to this type.
398    pub implied_clauses: IndexVec<TraitClauseId, TraitParam>,
399}
400
401/// A trait method.
402#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
403pub struct TraitMethod {
404    pub name: TraitItemName,
405    #[drive(skip)]
406    #[serde_state(stateless)]
407    pub attr_info: AttrInfo,
408    pub signature: FunSig,
409    /// Each method declaration is represented by a function item. That function contains the
410    /// signature of the method as well as information like attributes. It has a body iff the
411    /// method declaration has a default implementation; otherwise it has an `Opaque` body.
412    pub item: FunDeclRef,
413}
414
415/// A trait **implementation**.
416///
417/// For instance:
418/// ```text
419/// impl Foo for List {
420///   type Bar = ...
421///
422///   fn baz(...) { ... }
423/// }
424/// ```
425#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
426pub struct TraitImpl {
427    pub def_id: TraitImplId,
428    pub item_meta: ItemMeta,
429    /// The information about the implemented trait.
430    /// Note that this contains the instantiation of the "parent"
431    /// clauses.
432    pub impl_trait: TraitDeclRef,
433    pub generics: GenericParams,
434    /// The trait references for the parent clauses (see [TraitDecl]).
435    pub implied_trait_refs: IndexVec<TraitClauseId, TraitRef>,
436    /// The implemented associated constants.
437    pub consts: IndexMap<AssocConstId, GlobalDeclRef>,
438    /// The implemented associated types.
439    pub types: IndexMap<AssocTypeId, Binder<TraitAssocTyImpl>>,
440    /// The implemented methods
441    pub methods: IndexMap<TraitMethodId, Binder<FunDeclRef>>,
442    /// The virtual table instance for this trait implementation. This is `Some` iff the trait is
443    /// dyn-compatible.
444    pub vtable: Option<GlobalDeclRef>,
445}
446
447/// The value of a trait associated type.
448#[derive(Debug, Clone, PartialEq, Eq, Hash, SerializeState, DeserializeState, Drive, DriveMut)]
449pub struct TraitAssocTyImpl {
450    pub value: Ty,
451    /// This matches the corresponding vector in `TraitAssocTy`. In the same way, this is empty
452    /// after the `lift_associated_item_clauses` pass.
453    #[charon::opaque]
454    pub implied_trait_refs: IndexVec<TraitClauseId, TraitRef>,
455}
456
457/// A function operand is used in function calls.
458/// It either designates a top-level function, or a place in case
459/// we are using function pointers stored in local variables.
460#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
461#[charon::variants_prefix("FnOp")]
462pub enum FnOperand {
463    /// Regular case: call to a top-level function, trait method, etc.
464    Regular(FnPtr),
465    /// Use of a function pointer.
466    Dynamic(Operand),
467}
468
469#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
470pub struct Call {
471    pub func: FnOperand,
472    pub args: Vec<Operand>,
473    pub dest: Place,
474}
475
476#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
477pub struct CopyNonOverlapping {
478    pub src: Operand,
479    pub dst: Operand,
480    pub count: Operand,
481}
482
483/// The kind of a built-in assertion, which may panic and unwind. These are removed
484/// by `reconstruct_fallible_operations` because they're implicit in the semantics of (U)LLBC.
485/// This kind should only be used for error-reporting purposes, as the check itself
486/// is performed in the instructions preceding the assert.
487#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
488pub enum BuiltinAssertKind {
489    BoundsCheck { len: Operand, index: Operand },
490    Overflow(BinOp, Operand, Operand),
491    OverflowNeg(Operand),
492    DivisionByZero(Operand),
493    RemainderByZero(Operand),
494    MisalignedPointerDereference { required: Operand, found: Operand },
495    NullPointerDereference,
496    InvalidEnumConstruction(Operand),
497}
498
499/// (U)LLBC is a language with side-effects: a statement may abort in a way that isn't tracked by
500/// control-flow. The three kinds of abort are:
501/// - Panic
502/// - Undefined behavior (caused by an "assume")
503/// - Unwind termination
504#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
505pub enum AbortKind {
506    /// A built-in panicking function, or a panic due to a failed built-in check (e.g. for out-of-bounds accesses).
507    Panic(Option<Name>),
508    /// Undefined behavior in the rust abstract machine.
509    UndefinedBehavior,
510    /// Unwind had to stop for ABI reasons or because cleanup code panicked again.
511    UnwindTerminate,
512}
513
514/// A `Drop` statement/terminator can mean two things, depending on what MIR phase we retrieved
515/// from rustc: it could be a real drop, or it could be a "conditional drop", which is where drop
516/// may happen depending on whether the borrow-checker determines a drop is needed.
517#[derive(Debug, PartialEq, Eq, Clone, Copy, SerializeState, DeserializeState, Drive, DriveMut)]
518pub enum DropKind {
519    /// A real drop. This calls `<T as Destruct>::drop_in_place(&raw mut place)` and marks the
520    /// place as moved-out-of. Use `--desugar-drops` to transform all such drops to an actual
521    /// function call.
522    ///
523    /// The `drop_in_place` method is added by Charon to the `Destruct` trait to make it possible
524    /// to track drop code in polymorphic code. It contains the same code as the
525    /// `core::ptr::drop_in_place<T>` builtin would.
526    ///
527    /// Drop are precise in MIR `elaborated` and `optimized`.
528    Precise,
529    /// A conditional drop, which may or may not end up running drop code depending on the code
530    /// path that led to it. A conditional drop may also become a partial drop (dropping only the
531    /// subplaces that haven't been moved out of), may be conditional on the code path that led to
532    /// it, or become an async drop. The exact semantics are left intentionally unspecified by
533    /// rustc developers. To elaborate such drops into precise drops, pass `--precise-drops` to
534    /// Charon.
535    ///
536    /// A conditional drop may also be passed an unaligned place when dropping fields of packed
537    /// structs. Such a thing is UB for a precise drop.
538    ///
539    /// Drop are conditional in MIR `built` and `promoted`.
540    Conditional,
541}
542
543/// Check the value of an operand and abort if the value is not expected. This is introduced to
544/// avoid a lot of small branches.
545///
546/// We translate MIR asserts (introduced for out-of-bounds accesses or divisions by zero for
547/// instance) to this. We then eliminate them in [crate::transform::resugar::reconstruct_fallible_operations],
548/// because they're implicit in the semantics of our array accesses etc. Finally we introduce new asserts in
549/// [crate::transform::resugar::reconstruct_asserts].
550#[derive(Debug, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut)]
551#[charon::rename("Assertion")]
552pub struct Assert {
553    pub cond: Operand,
554    /// The value that the operand should evaluate to for the assert to succeed.
555    #[drive(skip)]
556    pub expected: bool,
557    /// The kind of check performed by this assert. This is only used for error reporting, as the check
558    /// is actually performed by the instructions preceding the assert.
559    pub check_kind: Option<BuiltinAssertKind>,
560}
561
562/// A generic `*DeclRef`-shaped struct, used when we're generic over the type of item.
563#[derive(Debug, PartialEq, Eq, Clone, Drive, DriveMut)]
564pub struct DeclRef<Id> {
565    pub id: Id,
566    pub generics: BoxedArgs,
567    /// If the item is a trait associated item, `generics` are only those of the item, and this
568    /// contains a reference to the trait.
569    pub trait_ref: Option<TraitRef>,
570}
571
572impl DeclRef<ItemId> {
573    pub fn try_convert_id<Id>(self) -> Result<DeclRef<Id>, <ItemId as TryInto<Id>>::Error>
574    where
575        ItemId: TryInto<Id>,
576    {
577        Ok(DeclRef {
578            id: self.id.try_into()?,
579            generics: self.generics,
580            trait_ref: self.trait_ref,
581        })
582    }
583}
584
585// Implement `DeclRef<_>` -> `FooDeclRef` conversions.
586macro_rules! convert_item_ref {
587    ($item_ref_ty:ident($id:ident)) => {
588        impl TryFrom<DeclRef<ItemId>> for $item_ref_ty {
589            type Error = ();
590            fn try_from(item: DeclRef<ItemId>) -> Result<Self, ()> {
591                assert!(item.trait_ref.is_none());
592                Ok($item_ref_ty {
593                    id: item.id.try_into()?,
594                    generics: item.generics,
595                })
596            }
597        }
598        impl From<DeclRef<$id>> for $item_ref_ty {
599            fn from(item: DeclRef<$id>) -> Self {
600                assert!(item.trait_ref.is_none());
601                $item_ref_ty {
602                    id: item.id,
603                    generics: item.generics,
604                }
605            }
606        }
607    };
608}
609convert_item_ref!(TypeDeclRef(TypeId));
610convert_item_ref!(FunDeclRef(FunDeclId));
611convert_item_ref!(GlobalDeclRef(GlobalDeclId));
612convert_item_ref!(TraitDeclRef(TraitDeclId));
613convert_item_ref!(TraitImplRef(TraitImplId));
614impl TryFrom<DeclRef<ItemId>> for FnPtr {
615    type Error = ();
616    fn try_from(item: DeclRef<ItemId>) -> Result<Self, ()> {
617        let id: FunId = item.id.try_into()?;
618        Ok(FnPtr::new(id.into(), item.generics))
619    }
620}
621
622impl TryFrom<DeclRef<ItemId>> for MaybeBuiltinFunDeclRef {
623    type Error = ();
624    fn try_from(item: DeclRef<ItemId>) -> Result<Self, ()> {
625        Ok(item.try_convert_id::<FunId>()?.into())
626    }
627}
628impl From<DeclRef<FunId>> for MaybeBuiltinFunDeclRef {
629    fn from(item: DeclRef<FunId>) -> Self {
630        MaybeBuiltinFunDeclRef {
631            id: item.id,
632            generics: item.generics,
633            trait_ref: item.trait_ref,
634        }
635    }
636}
charon_lib/ast/gast.rs

charon_lib/ast/
gast.rs
