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::{EnumIsA, EnumToGetters};
8use serde::{Deserialize, Serialize};
9
10/// A variable
11#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
12pub struct Local {
13    /// Unique index identifying the variable
14    pub index: LocalId,
15    /// Variable name - may be `None` if the variable was introduced by Rust
16    /// through desugaring.
17    #[drive(skip)]
18    pub name: Option<String>,
19    /// The variable type
20    #[charon::rename("var_ty")]
21    pub ty: Ty,
22}
23#[deprecated(note = "use `Local` intead")]
24pub type Var = Local;
25#[deprecated(note = "use `LocalId` intead")]
26pub type VarId = LocalId;
27
28/// Marker to indicate that a declaration is opaque (i.e. we don't inspect its body).
29#[derive(Debug, Copy, Clone, Serialize, Deserialize, Drive, DriveMut)]
30pub struct Opaque;
31
32/// The local variables of a body.
33#[derive(Debug, Default, Clone, Serialize, Deserialize, Drive, DriveMut)]
34pub struct Locals {
35    /// The number of local variables used for the input arguments.
36    #[drive(skip)]
37    pub arg_count: usize,
38    /// The local variables.
39    /// We always have, in the following order:
40    /// - the local used for the return value (index 0)
41    /// - the `arg_count` input arguments
42    /// - the remaining locals, used for the intermediate computations
43    pub locals: Vector<LocalId, Local>,
44}
45
46/// An expression body.
47/// TODO: arg_count should be stored in GFunDecl below. But then,
48///       the print is obfuscated and Aeneas may need some refactoring.
49#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
50#[charon::rename("GexprBody")]
51pub struct GExprBody<T> {
52    pub span: Span,
53    /// The local variables.
54    pub locals: Locals,
55    /// For each line inside the body, we record any whole-line `//` comments found before it. They
56    /// are added to statements in the late `recover_body_comments` pass.
57    #[charon::opaque]
58    #[drive(skip)]
59    pub comments: Vec<(usize, Vec<String>)>,
60    pub body: T,
61}
62
63/// The body of a function or a constant.
64#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut, EnumIsA, EnumToGetters)]
65pub enum Body {
66    /// Body represented as a CFG. This is what ullbc is made of, and what we get after translating MIR.
67    Unstructured(ullbc_ast::ExprBody),
68    /// Body represented with structured control flow. This is what llbc is made of. We restructure
69    /// the control flow in `ullbc_to_llbc`.
70    Structured(llbc_ast::ExprBody),
71}
72
73/// Item kind: whether this function/const is part of a trait declaration, trait implementation, or
74/// neither.
75///
76/// Example:
77/// ```text
78/// trait Foo {
79///     fn bar(x : u32) -> u32; // trait item decl without default
80///
81///     fn baz(x : bool) -> bool { x } // trait item decl with default
82/// }
83///
84/// impl Foo for ... {
85///     fn bar(x : u32) -> u32 { x } // trait item implementation
86/// }
87///
88/// fn test(...) { ... } // regular
89///
90/// impl Type {
91///     fn test(...) { ... } // regular
92/// }
93/// ```
94#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut, PartialEq, Eq)]
95#[charon::variants_suffix("Item")]
96pub enum ItemKind {
97    /// This item stands on its own.
98    TopLevel,
99    /// This is a closure in a function body.
100    Closure { info: ClosureInfo },
101    /// This is an associated item in a trait declaration. It has a body if and only if the trait
102    /// provided a default implementation.
103    TraitDecl {
104        /// The trait declaration this item belongs to.
105        trait_ref: TraitDeclRef,
106        /// The name of the item.
107        // TODO: also include method generics so we can recover a full `FnPtr::TraitMethod`
108        #[drive(skip)]
109        item_name: TraitItemName,
110        /// Whether the trait declaration provides a default implementation.
111        #[drive(skip)]
112        has_default: bool,
113    },
114    /// This is an associated item in a trait implementation.
115    TraitImpl {
116        /// The trait implementation the method belongs to.
117        impl_ref: TraitImplRef,
118        /// The trait declaration that the impl block implements.
119        trait_ref: TraitDeclRef,
120        /// The name of the item
121        // TODO: also include method generics so we can recover a full `FnPtr::TraitMethod`
122        #[drive(skip)]
123        item_name: TraitItemName,
124        /// True if the trait decl had a default implementation for this function/const and this
125        /// item is a copy of the default item.
126        #[drive(skip)]
127        reuses_default: bool,
128    },
129    /// This is a vtable struct for a trait.
130    VTableTy {
131        /// The `dyn Trait` predicate implemented by this vtable.
132        dyn_predicate: DynPredicate,
133    },
134    /// This is a vtable value for an impl.
135    VTableInstance { impl_ref: TraitImplRef },
136}
137
138/// A function definition
139#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
140pub struct FunDecl {
141    #[drive(skip)]
142    pub def_id: FunDeclId,
143    /// The meta data associated with the declaration.
144    pub item_meta: ItemMeta,
145    /// The signature contains the inputs/output types *with* non-erased regions.
146    /// It also contains the list of region and type parameters.
147    pub signature: FunSig,
148    /// The function kind: "regular" function, trait method declaration, etc.
149    pub kind: ItemKind,
150    /// Whether this function is in fact the body of a constant/static that we turned into an
151    /// initializer function.
152    pub is_global_initializer: Option<GlobalDeclId>,
153    /// The function body, unless the function is opaque.
154    /// Opaque functions are: external functions, or local functions tagged
155    /// as opaque.
156    pub body: Result<Body, Opaque>,
157}
158
159/// Reference to a function declaration.
160#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
161pub struct FunDeclRef {
162    pub id: FunDeclId,
163    /// Generic arguments passed to the function.
164    pub generics: BoxedArgs,
165}
166
167#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
168pub enum GlobalKind {
169    /// A static.
170    Static,
171    /// A const with a name (either top-level or an associated const in a trait).
172    NamedConst,
173    /// A const without a name:
174    /// - An inline const expression (`const { 1 + 1 }`);
175    /// - A const expression in a type (`[u8; sizeof::<T>()]`);
176    /// - A promoted constant, automatically lifted from a body (`&0`).
177    AnonConst,
178}
179
180/// A global variable definition (constant or static).
181#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
182pub struct GlobalDecl {
183    #[drive(skip)]
184    pub def_id: GlobalDeclId,
185    /// The meta data associated with the declaration.
186    pub item_meta: ItemMeta,
187    pub generics: GenericParams,
188    pub ty: Ty,
189    /// The context of the global: distinguishes top-level items from trait-associated items.
190    pub kind: ItemKind,
191    /// The kind of global (static or const).
192    #[drive(skip)]
193    pub global_kind: GlobalKind,
194    /// The initializer function used to compute the initial value for this constant/static. It
195    /// uses the same generic parameters as the global.
196    #[charon::rename("body")]
197    pub init: FunDeclId,
198}
199
200/// Reference to a global declaration.
201#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
202pub struct GlobalDeclRef {
203    pub id: GlobalDeclId,
204    pub generics: BoxedArgs,
205}
206
207#[derive(
208    Debug, Clone, Serialize, Deserialize, Drive, DriveMut, PartialEq, Eq, Hash, PartialOrd, Ord,
209)]
210#[drive(skip)]
211pub struct TraitItemName(pub String);
212
213/// A trait **declaration**.
214///
215/// For instance:
216/// ```text
217/// trait Foo {
218///   type Bar;
219///
220///   fn baz(...); // required method (see below)
221///
222///   fn test() -> bool { true } // provided method (see below)
223/// }
224/// ```
225///
226/// In case of a trait declaration, we don't include the provided methods (the methods
227/// with a default implementation): they will be translated on a per-need basis. This is
228/// important for two reasons:
229/// - this makes the trait definitions a lot smaller (the Iterator trait
230///   has *one* declared function and more than 70 provided functions)
231/// - this is important for the external traits, whose provided methods
232///   often use features we don't support yet
233///
234/// Remark:
235/// In Aeneas, we still translate the provided methods on an individual basis,
236/// and in such a way thay they take as input a trait instance. This means that
237/// we can use default methods *but*:
238/// - implementations of required methods shoudln't call default methods
239/// - trait implementations shouldn't redefine required methods
240/// The use case we have in mind is [std::iter::Iterator]: it declares one required
241/// method (`next`) that should be implemented for every iterator, and defines many
242/// helpers like `all`, `map`, etc. that shouldn't be re-implemented.
243/// Of course, this forbids other useful use cases such as visitors implemented
244/// by means of traits.
245#[allow(clippy::type_complexity)]
246#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
247pub struct TraitDecl {
248    #[drive(skip)]
249    pub def_id: TraitDeclId,
250    pub item_meta: ItemMeta,
251    pub generics: GenericParams,
252    /// The "parent" clauses: the supertraits.
253    ///
254    /// Supertraits are actually regular where clauses, but we decided to have
255    /// a custom treatment.
256    /// ```text
257    /// trait Foo : Bar {
258    ///             ^^^
259    ///         supertrait, that we treat as a parent predicate
260    /// }
261    /// ```
262    /// TODO: actually, as of today, we consider that all trait clauses of
263    /// trait declarations are parent clauses.
264    pub parent_clauses: Vector<TraitClauseId, TraitClause>,
265    /// The associated constants declared in the trait.
266    pub consts: Vec<TraitAssocConst>,
267    /// The associated types declared in the trait. The binder binds the generic parameters of the
268    /// type if it is a GAT (Generic Associated Type). For a plain associated type the binder binds
269    /// nothing.
270    pub types: Vec<Binder<TraitAssocTy>>,
271    /// The methods declared by the trait. The binder binds the generic parameters of the method.
272    ///
273    /// ```rust
274    /// trait Trait<T> {
275    ///   // The `Binder` for this method binds `'a` and `U`.
276    ///   fn method<'a, U>(x: &'a U);
277    /// }
278    /// ```
279    pub methods: Vec<Binder<TraitMethod>>,
280    /// The virtual table struct for this trait, if it has one.
281    /// It is guaranteed that the trait has a vtable iff it is dyn-compatible.
282    pub vtable: Option<TypeDeclRef>,
283}
284
285/// An associated constant in a trait.
286#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
287pub struct TraitAssocConst {
288    pub name: TraitItemName,
289    pub ty: Ty,
290    pub default: Option<GlobalDeclRef>,
291}
292
293/// An associated type in a trait.
294#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
295pub struct TraitAssocTy {
296    pub name: TraitItemName,
297    pub default: Option<Ty>,
298    /// List of trait clauses that apply to this type.
299    pub implied_clauses: Vector<TraitClauseId, TraitClause>,
300}
301
302/// A trait method.
303#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
304pub struct TraitMethod {
305    pub name: TraitItemName,
306    /// Each method declaration is represented by a function item. That function contains the
307    /// signature of the method as well as information like attributes. It has a body iff the
308    /// method declaration has a default implementation; otherwise it has an `Opaque` body.
309    pub item: FunDeclRef,
310}
311
312/// A trait **implementation**.
313///
314/// For instance:
315/// ```text
316/// impl Foo for List {
317///   type Bar = ...
318///
319///   fn baz(...) { ... }
320/// }
321/// ```
322#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
323pub struct TraitImpl {
324    #[drive(skip)]
325    pub def_id: TraitImplId,
326    pub item_meta: ItemMeta,
327    /// The information about the implemented trait.
328    /// Note that this contains the instantiation of the "parent"
329    /// clauses.
330    pub impl_trait: TraitDeclRef,
331    pub generics: GenericParams,
332    /// The trait references for the parent clauses (see [TraitDecl]).
333    pub parent_trait_refs: Vector<TraitClauseId, TraitRef>,
334    /// The implemented associated constants.
335    pub consts: Vec<(TraitItemName, GlobalDeclRef)>,
336    /// The implemented associated types.
337    pub types: Vec<(TraitItemName, Binder<TraitAssocTyImpl>)>,
338    /// The implemented methods
339    pub methods: Vec<(TraitItemName, Binder<FunDeclRef>)>,
340    /// The virtual table instance for this trait implementation. This is `Some` iff the trait is
341    /// dyn-compatible.
342    pub vtable: Option<GlobalDeclRef>,
343}
344
345/// The value of a trait associated type.
346#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
347pub struct TraitAssocTyImpl {
348    pub value: Ty,
349    /// The `Vec` corresponds to the same `Vector` in `TraitAssocTy`. In the same way, this is
350    /// empty after the `lift_associated_item_clauses` pass.
351    #[charon::opaque]
352    pub implied_trait_refs: Vector<TraitClauseId, TraitRef>,
353}
354
355/// A function operand is used in function calls.
356/// It either designates a top-level function, or a place in case
357/// we are using function pointers stored in local variables.
358#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
359#[charon::variants_prefix("FnOp")]
360pub enum FnOperand {
361    /// Regular case: call to a top-level function, trait method, etc.
362    Regular(FnPtr),
363    /// Use of a function pointer stored in a local variable
364    Move(Place),
365}
366
367#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
368pub struct Call {
369    pub func: FnOperand,
370    pub args: Vec<Operand>,
371    pub dest: Place,
372}
373
374#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
375pub struct CopyNonOverlapping {
376    pub src: Operand,
377    pub dst: Operand,
378    pub count: Operand,
379}
380
381/// (U)LLBC is a language with side-effects: a statement may abort in a way that isn't tracked by
382/// control-flow. The two kinds of abort are:
383/// - Panic (may unwind or not depending on compilation setting);
384/// - Undefined behavior:
385#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
386pub enum AbortKind {
387    /// A built-in panicking function.
388    Panic(Option<Name>),
389    /// Undefined behavior in the rust abstract machine.
390    UndefinedBehavior,
391    /// Unwind had to stop for Abi reasons or because cleanup code panicked again.
392    UnwindTerminate,
393}
394
395/// Check the value of an operand and abort if the value is not expected. This is introduced to
396/// avoid a lot of small branches.
397///
398/// We translate MIR asserts (introduced for out-of-bounds accesses or divisions by zero for
399/// instance) to this. We then eliminate them in [crate::transform::remove_dynamic_checks],
400/// because they're implicit in the semantics of our array accesses etc. Finally we introduce new asserts in
401/// [crate::transform::reconstruct_asserts].
402#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
403#[charon::rename("Assertion")]
404pub struct Assert {
405    pub cond: Operand,
406    /// The value that the operand should evaluate to for the assert to succeed.
407    #[drive(skip)]
408    pub expected: bool,
409    /// What kind of abort happens on assert failure.
410    pub on_failure: AbortKind,
411}