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

charon_lib/ast/
gast.rs
