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("local_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 ItemSource {
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 /// The method shim wraps a concrete implementation of a method into a function that takes `dyn
137 /// Trait` as its `Self` type. This shim casts the receiver to the known concrete type and
138 /// calls the real method.
139 VTableMethodShim,
140}
141
142/// A function definition
143#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
144pub struct FunDecl {
145 #[drive(skip)]
146 pub def_id: FunDeclId,
147 /// The meta data associated with the declaration.
148 pub item_meta: ItemMeta,
149 /// The signature contains the inputs/output types *with* non-erased regions.
150 /// It also contains the list of region and type parameters.
151 pub signature: FunSig,
152 /// The function kind: "regular" function, trait method declaration, etc.
153 pub src: ItemSource,
154 /// Whether this function is in fact the body of a constant/static that we turned into an
155 /// initializer function.
156 pub is_global_initializer: Option<GlobalDeclId>,
157 /// The function body, unless the function is opaque.
158 /// Opaque functions are: external functions, or local functions tagged
159 /// as opaque.
160 pub body: Result<Body, Opaque>,
161}
162
163/// Reference to a function declaration.
164#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
165pub struct FunDeclRef {
166 pub id: FunDeclId,
167 /// Generic arguments passed to the function.
168 pub generics: BoxedArgs,
169}
170
171#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
172pub enum GlobalKind {
173 /// A static.
174 Static,
175 /// A const with a name (either top-level or an associated const in a trait).
176 NamedConst,
177 /// A const without a name:
178 /// - An inline const expression (`const { 1 + 1 }`);
179 /// - A const expression in a type (`[u8; sizeof::<T>()]`);
180 /// - A promoted constant, automatically lifted from a body (`&0`).
181 AnonConst,
182}
183
184/// A global variable definition (constant or static).
185#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
186pub struct GlobalDecl {
187 #[drive(skip)]
188 pub def_id: GlobalDeclId,
189 /// The meta data associated with the declaration.
190 pub item_meta: ItemMeta,
191 pub generics: GenericParams,
192 pub ty: Ty,
193 /// The context of the global: distinguishes top-level items from trait-associated items.
194 pub src: ItemSource,
195 /// The kind of global (static or const).
196 #[drive(skip)]
197 pub global_kind: GlobalKind,
198 /// The initializer function used to compute the initial value for this constant/static. It
199 /// uses the same generic parameters as the global.
200 pub init: FunDeclId,
201}
202
203/// Reference to a global declaration.
204#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
205pub struct GlobalDeclRef {
206 pub id: GlobalDeclId,
207 pub generics: BoxedArgs,
208}
209
210#[derive(
211 Debug, Clone, Serialize, Deserialize, Drive, DriveMut, PartialEq, Eq, Hash, PartialOrd, Ord,
212)]
213#[drive(skip)]
214pub struct TraitItemName(pub String);
215
216/// A trait **declaration**.
217///
218/// For instance:
219/// ```text
220/// trait Foo {
221/// type Bar;
222///
223/// fn baz(...); // required method (see below)
224///
225/// fn test() -> bool { true } // provided method (see below)
226/// }
227/// ```
228///
229/// In case of a trait declaration, we don't include the provided methods (the methods
230/// with a default implementation): they will be translated on a per-need basis. This is
231/// important for two reasons:
232/// - this makes the trait definitions a lot smaller (the Iterator trait
233/// has *one* declared function and more than 70 provided functions)
234/// - this is important for the external traits, whose provided methods
235/// often use features we don't support yet
236///
237/// Remark:
238/// In Aeneas, we still translate the provided methods on an individual basis,
239/// and in such a way thay they take as input a trait instance. This means that
240/// we can use default methods *but*:
241/// - implementations of required methods shoudln't call default methods
242/// - trait implementations shouldn't redefine required methods
243/// The use case we have in mind is [std::iter::Iterator]: it declares one required
244/// method (`next`) that should be implemented for every iterator, and defines many
245/// helpers like `all`, `map`, etc. that shouldn't be re-implemented.
246/// Of course, this forbids other useful use cases such as visitors implemented
247/// by means of traits.
248#[allow(clippy::type_complexity)]
249#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
250pub struct TraitDecl {
251 #[drive(skip)]
252 pub def_id: TraitDeclId,
253 pub item_meta: ItemMeta,
254 pub generics: GenericParams,
255 /// The "parent" clauses: the supertraits.
256 ///
257 /// Supertraits are actually regular where clauses, but we decided to have
258 /// a custom treatment.
259 /// ```text
260 /// trait Foo : Bar {
261 /// ^^^
262 /// supertrait, that we treat as a parent predicate
263 /// }
264 /// ```
265 /// TODO: actually, as of today, we consider that all trait clauses of
266 /// trait declarations are parent clauses.
267 pub implied_clauses: Vector<TraitClauseId, TraitParam>,
268 /// The associated constants declared in the trait.
269 pub consts: Vec<TraitAssocConst>,
270 /// The associated types declared in the trait. The binder binds the generic parameters of the
271 /// type if it is a GAT (Generic Associated Type). For a plain associated type the binder binds
272 /// nothing.
273 pub types: Vec<Binder<TraitAssocTy>>,
274 /// The methods declared by the trait. The binder binds the generic parameters of the method.
275 ///
276 /// ```rust
277 /// trait Trait<T> {
278 /// // The `Binder` for this method binds `'a` and `U`.
279 /// fn method<'a, U>(x: &'a U);
280 /// }
281 /// ```
282 pub methods: Vec<Binder<TraitMethod>>,
283 /// The virtual table struct for this trait, if it has one.
284 /// It is guaranteed that the trait has a vtable iff it is dyn-compatible.
285 pub vtable: Option<TypeDeclRef>,
286}
287
288/// An associated constant in a trait.
289#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
290pub struct TraitAssocConst {
291 pub name: TraitItemName,
292 pub ty: Ty,
293 pub default: Option<GlobalDeclRef>,
294}
295
296/// An associated type in a trait.
297#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
298pub struct TraitAssocTy {
299 pub name: TraitItemName,
300 pub default: Option<Ty>,
301 /// List of trait clauses that apply to this type.
302 pub implied_clauses: Vector<TraitClauseId, TraitParam>,
303}
304
305/// A trait method.
306#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
307pub struct TraitMethod {
308 pub name: TraitItemName,
309 /// Each method declaration is represented by a function item. That function contains the
310 /// signature of the method as well as information like attributes. It has a body iff the
311 /// method declaration has a default implementation; otherwise it has an `Opaque` body.
312 pub item: FunDeclRef,
313}
314
315/// A trait **implementation**.
316///
317/// For instance:
318/// ```text
319/// impl Foo for List {
320/// type Bar = ...
321///
322/// fn baz(...) { ... }
323/// }
324/// ```
325#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
326pub struct TraitImpl {
327 #[drive(skip)]
328 pub def_id: TraitImplId,
329 pub item_meta: ItemMeta,
330 /// The information about the implemented trait.
331 /// Note that this contains the instantiation of the "parent"
332 /// clauses.
333 pub impl_trait: TraitDeclRef,
334 pub generics: GenericParams,
335 /// The trait references for the parent clauses (see [TraitDecl]).
336 pub implied_trait_refs: Vector<TraitClauseId, TraitRef>,
337 /// The implemented associated constants.
338 pub consts: Vec<(TraitItemName, GlobalDeclRef)>,
339 /// The implemented associated types.
340 pub types: Vec<(TraitItemName, Binder<TraitAssocTyImpl>)>,
341 /// The implemented methods
342 pub methods: Vec<(TraitItemName, Binder<FunDeclRef>)>,
343 /// The virtual table instance for this trait implementation. This is `Some` iff the trait is
344 /// dyn-compatible.
345 pub vtable: Option<GlobalDeclRef>,
346}
347
348/// The value of a trait associated type.
349#[derive(Debug, Clone, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
350pub struct TraitAssocTyImpl {
351 pub value: Ty,
352 /// The `Vec` corresponds to the same `Vector` in `TraitAssocTy`. In the same way, this is
353 /// empty after the `lift_associated_item_clauses` pass.
354 #[charon::opaque]
355 pub implied_trait_refs: Vector<TraitClauseId, TraitRef>,
356}
357
358/// A function operand is used in function calls.
359/// It either designates a top-level function, or a place in case
360/// we are using function pointers stored in local variables.
361#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
362#[charon::variants_prefix("FnOp")]
363pub enum FnOperand {
364 /// Regular case: call to a top-level function, trait method, etc.
365 Regular(FnPtr),
366 /// Use of a function pointer stored in a local variable
367 Move(Place),
368}
369
370#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
371pub struct Call {
372 pub func: FnOperand,
373 pub args: Vec<Operand>,
374 pub dest: Place,
375}
376
377#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
378pub struct CopyNonOverlapping {
379 pub src: Operand,
380 pub dst: Operand,
381 pub count: Operand,
382}
383
384/// (U)LLBC is a language with side-effects: a statement may abort in a way that isn't tracked by
385/// control-flow. The two kinds of abort are:
386/// - Panic (may unwind or not depending on compilation setting);
387/// - Undefined behavior:
388#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
389pub enum AbortKind {
390 /// A built-in panicking function.
391 Panic(Option<Name>),
392 /// Undefined behavior in the rust abstract machine.
393 UndefinedBehavior,
394 /// Unwind had to stop for Abi reasons or because cleanup code panicked again.
395 UnwindTerminate,
396}
397
398/// Check the value of an operand and abort if the value is not expected. This is introduced to
399/// avoid a lot of small branches.
400///
401/// We translate MIR asserts (introduced for out-of-bounds accesses or divisions by zero for
402/// instance) to this. We then eliminate them in [crate::transform::resugar::reconstruct_fallible_operations],
403/// because they're implicit in the semantics of our array accesses etc. Finally we introduce new asserts in
404/// [crate::transform::resugar::reconstruct_asserts].
405#[derive(Debug, Clone, Serialize, Deserialize, Drive, DriveMut)]
406#[charon::rename("Assertion")]
407pub struct Assert {
408 pub cond: Operand,
409 /// The value that the operand should evaluate to for the assert to succeed.
410 #[drive(skip)]
411 pub expected: bool,
412 /// What kind of abort happens on assert failure.
413 pub on_failure: AbortKind,
414}