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    /// A function/const at the top level or in an inherent impl block.
99    Regular,
100    /// Function/const that is part of a trait declaration. It has a body if and only if the trait
101    /// provided a default implementation.
102    TraitDecl {
103        /// The trait declaration this item belongs to.
104        trait_ref: TraitDeclRef,
105        /// The name of the item.
106        // TODO: also include method generics so we can recover a full `FnPtr::TraitMethod`
107        #[drive(skip)]
108        item_name: TraitItemName,
109        /// Whether the trait declaration provides a default implementation.
110        #[drive(skip)]
111        has_default: bool,
112    },
113    /// Function/const that is part of a trait implementation.
114    TraitImpl {
115        /// The trait implementation the method belongs to.
116        impl_ref: TraitImplRef,
117        /// The trait declaration that the impl block implements.
118        trait_ref: TraitDeclRef,
119        /// The name of the item
120        // TODO: also include method generics so we can recover a full `FnPtr::TraitMethod`
121        #[drive(skip)]
122        item_name: TraitItemName,
123        /// True if the trait decl had a default implementation for this function/const and this
124        /// item is a copy of the default item.
125        #[drive(skip)]
126        reuses_default: bool,
127    },
128}
129
130/// A function definition
131#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
132pub struct FunDecl {
133    #[drive(skip)]
134    pub def_id: FunDeclId,
135    /// The meta data associated with the declaration.
136    pub item_meta: ItemMeta,
137    /// The signature contains the inputs/output types *with* non-erased regions.
138    /// It also contains the list of region and type parameters.
139    pub signature: FunSig,
140    /// The function kind: "regular" function, trait method declaration, etc.
141    pub kind: ItemKind,
142    /// Whether this function is in fact the body of a constant/static that we turned into an
143    /// initializer function.
144    pub is_global_initializer: Option<GlobalDeclId>,
145    /// The function body, unless the function is opaque.
146    /// Opaque functions are: external functions, or local functions tagged
147    /// as opaque.
148    pub body: Result<Body, Opaque>,
149}
150
151/// Reference to a function declaration.
152#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
153pub struct FunDeclRef {
154    #[charon::rename("fun_id")]
155    pub id: FunDeclId,
156    /// Generic arguments passed to the function.
157    #[charon::rename("fun_generics")]
158    pub generics: GenericArgs,
159}
160
161#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
162pub enum GlobalKind {
163    /// A static.
164    Static,
165    /// A const with a name (either top-level or an associated const in a trait).
166    NamedConst,
167    /// A const without a name:
168    /// - An inline const expression (`const { 1 + 1 }`);
169    /// - A const expression in a type (`[u8; sizeof::<T>()]`);
170    /// - A promoted constant, automatically lifted from a body (`&0`).
171    AnonConst,
172}
173
174/// A global variable definition (constant or static).
175#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
176pub struct GlobalDecl {
177    #[drive(skip)]
178    pub def_id: GlobalDeclId,
179    /// The meta data associated with the declaration.
180    pub item_meta: ItemMeta,
181    pub generics: GenericParams,
182    pub ty: Ty,
183    /// The context of the global: distinguishes top-level items from trait-associated items.
184    pub kind: ItemKind,
185    /// The kind of global (static or const).
186    #[drive(skip)]
187    pub global_kind: GlobalKind,
188    /// The initializer function used to compute the initial value for this constant/static. It
189    /// uses the same generic parameters as the global.
190    #[charon::rename("body")]
191    pub init: FunDeclId,
192}
193
194/// Reference to a global declaration.
195#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
196pub struct GlobalDeclRef {
197    #[charon::rename("global_id")]
198    pub id: GlobalDeclId,
199    #[charon::rename("global_generics")]
200    pub generics: GenericArgs,
201}
202
203#[derive(
204    Debug, Clone, Serialize, Deserialize, Drive, DriveMut, PartialEq, Eq, Hash, PartialOrd, Ord,
205)]
206#[drive(skip)]
207pub struct TraitItemName(pub String);
208
209/// A trait **declaration**.
210///
211/// For instance:
212/// ```text
213/// trait Foo {
214///   type Bar;
215///
216///   fn baz(...); // required method (see below)
217///
218///   fn test() -> bool { true } // provided method (see below)
219/// }
220/// ```
221///
222/// In case of a trait declaration, we don't include the provided methods (the methods
223/// with a default implementation): they will be translated on a per-need basis. This is
224/// important for two reasons:
225/// - this makes the trait definitions a lot smaller (the Iterator trait
226///   has *one* declared function and more than 70 provided functions)
227/// - this is important for the external traits, whose provided methods
228///   often use features we don't support yet
229///
230/// Remark:
231/// In Aeneas, we still translate the provided methods on an individual basis,
232/// and in such a way thay they take as input a trait instance. This means that
233/// we can use default methods *but*:
234/// - implementations of required methods shoudln't call default methods
235/// - trait implementations shouldn't redefine required methods
236/// The use case we have in mind is [std::iter::Iterator]: it declares one required
237/// method (`next`) that should be implemented for every iterator, and defines many
238/// helpers like `all`, `map`, etc. that shouldn't be re-implemented.
239/// Of course, this forbids other useful use cases such as visitors implemented
240/// by means of traits.
241#[allow(clippy::type_complexity)]
242#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
243pub struct TraitDecl {
244    #[drive(skip)]
245    pub def_id: TraitDeclId,
246    pub item_meta: ItemMeta,
247    pub generics: GenericParams,
248    /// The "parent" clauses: the supertraits.
249    ///
250    /// Supertraits are actually regular where clauses, but we decided to have
251    /// a custom treatment.
252    /// ```text
253    /// trait Foo : Bar {
254    ///             ^^^
255    ///         supertrait, that we treat as a parent predicate
256    /// }
257    /// ```
258    /// TODO: actually, as of today, we consider that all trait clauses of
259    /// trait declarations are parent clauses.
260    pub parent_clauses: Vector<TraitClauseId, TraitClause>,
261    /// The associated constants declared in the trait, along with their type.
262    pub consts: Vec<(TraitItemName, Ty)>,
263    /// Records associated constants that have a default value.
264    #[charon::opaque]
265    pub const_defaults: IndexMap<TraitItemName, GlobalDeclRef>,
266    /// The associated types declared in the trait.
267    pub types: Vec<TraitItemName>,
268    /// Records associated types that have a default value.
269    #[charon::opaque]
270    pub type_defaults: IndexMap<TraitItemName, Ty>,
271    /// List of trait clauses that apply to each associated type. This is used during translation,
272    /// but the `lift_associated_item_clauses` pass moves them to be parent clauses later. Hence
273    /// this is empty after that pass.
274    /// TODO: Do this as we translate to avoid the need to store this vector.
275    #[charon::opaque]
276    pub type_clauses: Vec<(TraitItemName, Vector<TraitClauseId, TraitClause>)>,
277    /// The methods declared by the trait. The signature of the methods can be found in each
278    /// corresponding `FunDecl`. These `FunDecl` may have a body if the trait provided a default
279    /// implementation for that method; otherwise it has an `Opaque` body.
280    ///
281    /// The binder contains the type parameters specific to the method. The `FunDeclRef` then
282    /// provides a full list of arguments to the pointed-to function.
283    pub methods: Vec<(TraitItemName, Binder<FunDeclRef>)>,
284}
285
286/// A trait **implementation**.
287///
288/// For instance:
289/// ```text
290/// impl Foo for List {
291///   type Bar = ...
292///
293///   fn baz(...) { ... }
294/// }
295/// ```
296#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
297pub struct TraitImpl {
298    #[drive(skip)]
299    pub def_id: TraitImplId,
300    pub item_meta: ItemMeta,
301    /// The information about the implemented trait.
302    /// Note that this contains the instantiation of the "parent"
303    /// clauses.
304    pub impl_trait: TraitDeclRef,
305    pub generics: GenericParams,
306    /// The trait references for the parent clauses (see [TraitDecl]).
307    pub parent_trait_refs: Vector<TraitClauseId, TraitRef>,
308    /// The associated constants declared in the trait.
309    pub consts: Vec<(TraitItemName, GlobalDeclRef)>,
310    /// The associated types declared in the trait.
311    pub types: Vec<(TraitItemName, Ty)>,
312    /// The `Vec` corresponds to the same `Vector` in `TraitDecl`. In the same way, this is
313    /// empty after the `lift_associated_item_clauses` pass.
314    #[charon::opaque]
315    pub type_clauses: Vec<(TraitItemName, Vector<TraitClauseId, TraitRef>)>,
316    /// The implemented methods
317    pub methods: Vec<(TraitItemName, Binder<FunDeclRef>)>,
318}
319
320/// A function operand is used in function calls.
321/// It either designates a top-level function, or a place in case
322/// we are using function pointers stored in local variables.
323#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
324#[charon::variants_prefix("FnOp")]
325pub enum FnOperand {
326    /// Regular case: call to a top-level function, trait method, etc.
327    Regular(FnPtr),
328    /// Use of a function pointer stored in a local variable
329    Move(Place),
330}
331
332#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
333pub struct Call {
334    pub func: FnOperand,
335    pub args: Vec<Operand>,
336    pub dest: Place,
337}
338
339/// (U)LLBC is a language with side-effects: a statement may abort in a way that isn't tracked by
340/// control-flow. The two kinds of abort are:
341/// - Panic (may unwind or not depending on compilation setting);
342/// - Undefined behavior:
343#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
344pub enum AbortKind {
345    /// A built-in panicking function.
346    Panic(Option<Name>),
347    /// Undefined behavior in the rust abstract machine.
348    UndefinedBehavior,
349}
350
351/// Check the value of an operand and abort if the value is not expected. This is introduced to
352/// avoid a lot of small branches.
353///
354/// We translate MIR asserts (introduced for out-of-bounds accesses or divisions by zero for
355/// instance) to this. We then eliminate them in [crate::remove_dynamic_checks], because they're
356/// implicit in the semantics of our array accesses etc. Finally we introduce new asserts in
357/// [crate::reconstruct_asserts].
358#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
359#[charon::rename("Assertion")]
360pub struct Assert {
361    pub cond: Operand,
362    /// The value that the operand should evaluate to for the assert to succeed.
363    #[drive(skip)]
364    pub expected: bool,
365    /// What kind of abort happens on assert failure.
366    pub on_failure: AbortKind,
367}