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

charon_lib/ast/
gast.rs
