charon_lib/ast/
gast.rs

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

charon_lib/ast/
gast.rs
