charon_lib/ast/
expressions.rs

1//! Implements expressions: paths, operands, rvalues, lvalues
2
3use crate::ast::*;
4use derive_generic_visitor::{Drive, DriveMut};
5use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName};
6use serde::{Deserialize, Serialize};
7use std::vec::Vec;
8
9#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
10pub struct Place {
11    pub kind: PlaceKind,
12    pub ty: Ty,
13}
14
15#[derive(
16    Debug,
17    PartialEq,
18    Eq,
19    Clone,
20    EnumIsA,
21    EnumAsGetters,
22    EnumToGetters,
23    Serialize,
24    Deserialize,
25    Drive,
26    DriveMut,
27)]
28#[charon::variants_prefix("Place")]
29pub enum PlaceKind {
30    Local(LocalId),
31    Projection(Box<Place>, ProjectionElem),
32}
33
34/// Note that we don't have the equivalent of "downcasts".
35/// Downcasts are actually necessary, for instance when initializing enumeration
36/// values: the value is initially `Bottom`, and we need a way of knowing the
37/// variant.
38/// For example:
39/// `((_0 as Right).0: T2) = move _1;`
40/// In MIR, downcasts always happen before field projections: in our internal
41/// language, we thus merge downcasts and field projections.
42#[derive(
43    Debug,
44    PartialEq,
45    Eq,
46    Clone,
47    EnumIsA,
48    EnumAsGetters,
49    EnumToGetters,
50    VariantName,
51    Serialize,
52    Deserialize,
53    Drive,
54    DriveMut,
55)]
56pub enum ProjectionElem {
57    /// Dereference a shared/mutable reference, a box, or a raw pointer.
58    Deref,
59    /// Projection from ADTs (variants, structures).
60    /// We allow projections to be used as left-values and right-values.
61    /// We should never have projections to fields of symbolic variants (they
62    /// should have been expanded before through a match).
63    Field(FieldProjKind, FieldId),
64    /// MIR imposes that the argument to an index projection be a local variable, meaning
65    /// that even constant indices into arrays are let-bound as separate variables.
66    /// We **eliminate** this variant in a micro-pass for LLBC.
67    #[charon::rename("ProjIndex")]
68    Index {
69        offset: Box<Operand>,
70        #[drive(skip)]
71        from_end: bool,
72    },
73    /// Take a subslice of a slice or array. If `from_end` is `true` this is
74    /// `slice[from..slice.len() - to]`, otherwise this is `slice[from..to]`.
75    /// We **eliminate** this variant in a micro-pass for LLBC.
76    Subslice {
77        from: Box<Operand>,
78        to: Box<Operand>,
79        #[drive(skip)]
80        from_end: bool,
81    },
82}
83
84#[derive(
85    Debug,
86    PartialEq,
87    Eq,
88    Copy,
89    Clone,
90    EnumIsA,
91    EnumAsGetters,
92    Serialize,
93    Deserialize,
94    Drive,
95    DriveMut,
96)]
97#[charon::variants_prefix("Proj")]
98pub enum FieldProjKind {
99    Adt(TypeDeclId, Option<VariantId>),
100    /// If we project from a tuple, the projection kind gives the arity of the tuple.
101    #[drive(skip)]
102    Tuple(usize),
103}
104
105#[derive(
106    Debug,
107    PartialEq,
108    Eq,
109    Copy,
110    Clone,
111    EnumIsA,
112    EnumAsGetters,
113    Serialize,
114    Deserialize,
115    Drive,
116    DriveMut,
117)]
118#[charon::variants_prefix("B")]
119pub enum BorrowKind {
120    Shared,
121    Mut,
122    /// See <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.MutBorrowKind.html#variant.TwoPhaseBorrow>
123    /// and <https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html>
124    TwoPhaseMut,
125    /// Those are typically introduced when using guards in matches, to make sure guards don't
126    /// change the variant of an enum value while me match over it.
127    ///
128    /// See <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.FakeBorrowKind.html#variant.Shallow>.
129    Shallow,
130    /// Data must be immutable but not aliasable. In other words you can't mutate the data but you
131    /// can mutate *through it*, e.g. if it points to a `&mut T`. This is only used in closure
132    /// captures, e.g.
133    /// ```rust,ignore
134    /// let mut z = 3;
135    /// let x: &mut isize = &mut z;
136    /// let y = || *x += 5;
137    /// ```
138    /// Here the captured variable can't be `&mut &mut x` since the `x` binding is not mutable, yet
139    /// we must be able to mutate what it points to.
140    ///
141    /// See <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.MutBorrowKind.html#variant.ClosureCapture>.
142    UniqueImmutable,
143}
144
145/// Unary operation
146#[derive(
147    Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
148)]
149#[charon::rename("Unop")]
150pub enum UnOp {
151    Not,
152    /// This can overflow, for `-i::MIN`.
153    #[drive(skip)]
154    Neg(OverflowMode),
155    /// Retreive the metadata part of a fat pointer. For slices, this retreives their length.
156    PtrMetadata,
157    /// Casts are rvalues in MIR, but we treat them as unops.
158    Cast(CastKind),
159    /// Coercion from array (i.e., [T; N]) to slice.
160    ///
161    /// **Remark:** We introduce this unop when translating from MIR, **then transform**
162    /// it to a function call in a micro pass. The type and the scalar value are not
163    /// *necessary* as we can retrieve them from the context, but storing them here is
164    /// very useful. The [RefKind] argument states whethere we operate on a mutable
165    /// or a shared borrow to an array.
166    ArrayToSlice(RefKind, Ty, ConstGeneric),
167}
168
169/// Nullary operation
170#[derive(
171    Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
172)]
173#[charon::rename("Nullop")]
174pub enum NullOp {
175    SizeOf,
176    AlignOf,
177    #[drive(skip)]
178    OffsetOf(Vec<(usize, FieldId)>),
179    UbChecks,
180}
181
182/// For all the variants: the first type gives the source type, the second one gives
183/// the destination type.
184#[derive(
185    Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
186)]
187#[charon::variants_prefix("Cast")]
188pub enum CastKind {
189    /// Conversion between types in `{Integer, Bool}`
190    /// Remark: for now we don't support conversions with Char.
191    Scalar(LiteralTy, LiteralTy),
192    RawPtr(Ty, Ty),
193    FnPtr(Ty, Ty),
194    /// [Unsize coercion](https://doc.rust-lang.org/std/ops/trait.CoerceUnsized.html). This is
195    /// either `[T; N]` -> `[T]` or `T: Trait` -> `dyn Trait` coercions, behind a pointer
196    /// (reference, `Box`, or other type that implements `CoerceUnsized`).
197    ///
198    /// The special case of `&[T; N]` -> `&[T]` coercion is caught by `UnOp::ArrayToSlice`.
199    Unsize(Ty, Ty),
200    /// Reinterprets the bits of a value of one type as another type, i.e. exactly what
201    /// [`std::mem::transmute`] does.
202    Transmute(Ty, Ty),
203}
204
205#[derive(Debug, PartialEq, Eq, Copy, Clone, Serialize, Deserialize)]
206#[charon::variants_prefix("O")]
207pub enum OverflowMode {
208    /// If this operation overflows, it panics. Only exists in debug mode, for instance in
209    /// `a + b`, and is introduced by the `remove_dynamic_checks` pass.
210    Panic,
211    /// If this operation overflows, it UBs, for instance in `core::num::unchecked_add`.
212    UB,
213    /// If this operation overflows, it wraps around, for instance in `core::num::wrapping_add`,
214    /// or `a + b` in release mode.
215    Wrap,
216}
217
218/// Binary operations.
219#[derive(
220    Debug, PartialEq, Eq, Copy, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
221)]
222#[charon::rename("Binop")]
223pub enum BinOp {
224    BitXor,
225    BitAnd,
226    BitOr,
227    Eq,
228    Lt,
229    Le,
230    Ne,
231    Ge,
232    Gt,
233    #[drive(skip)]
234    Add(OverflowMode),
235    #[drive(skip)]
236    Sub(OverflowMode),
237    #[drive(skip)]
238    Mul(OverflowMode),
239    #[drive(skip)]
240    Div(OverflowMode),
241    #[drive(skip)]
242    Rem(OverflowMode),
243    /// Returns `(result, did_overflow)`, where `result` is the result of the operation with
244    /// wrapping semantics, and `did_overflow` is a boolean that indicates whether the operation
245    /// overflowed. This operation does not fail.
246    AddChecked,
247    /// Like `AddChecked`.
248    SubChecked,
249    /// Like `AddChecked`.
250    MulChecked,
251    /// Fails if the shift is bigger than the bit-size of the type.
252    #[drive(skip)]
253    Shl(OverflowMode),
254    /// Fails if the shift is bigger than the bit-size of the type.
255    #[drive(skip)]
256    Shr(OverflowMode),
257    /// `BinOp(Offset, ptr, n)` for `ptr` a pointer to type `T` offsets `ptr` by `n * size_of::<T>()`.
258    Offset,
259    /// `BinOp(Cmp, a, b)` returns `-1u8` if `a < b`, `0u8` if `a == b`, and `1u8` if `a > b`.
260    Cmp,
261}
262
263#[derive(
264    Debug,
265    PartialEq,
266    Eq,
267    Clone,
268    EnumIsA,
269    EnumToGetters,
270    EnumAsGetters,
271    VariantName,
272    Serialize,
273    Deserialize,
274    Drive,
275    DriveMut,
276)]
277pub enum Operand {
278    Copy(Place),
279    Move(Place),
280    /// Constant value (including constant and static variables)
281    #[charon::rename("Constant")]
282    Const(Box<ConstantExpr>),
283}
284
285/// A function identifier. See [crate::ullbc_ast::Terminator]
286#[derive(
287    Debug,
288    Clone,
289    PartialEq,
290    Eq,
291    Hash,
292    EnumIsA,
293    EnumAsGetters,
294    VariantName,
295    Serialize,
296    Deserialize,
297    Drive,
298    DriveMut,
299)]
300#[charon::variants_prefix("F")]
301pub enum FunId {
302    /// A "regular" function (function local to the crate, external function
303    /// not treated as a primitive one).
304    Regular(FunDeclId),
305    /// A primitive function, coming from a standard library (for instance:
306    /// `alloc::boxed::Box::new`).
307    /// TODO: rename to "Primitive"
308    #[charon::rename("FBuiltin")]
309    Builtin(BuiltinFunId),
310}
311
312impl From<FunDeclId> for FunId {
313    fn from(id: FunDeclId) -> Self {
314        Self::Regular(id)
315    }
316}
317impl From<BuiltinFunId> for FunId {
318    fn from(id: BuiltinFunId) -> Self {
319        Self::Builtin(id)
320    }
321}
322
323/// An built-in function identifier, identifying a function coming from a
324/// standard library.
325#[derive(
326    Debug,
327    Clone,
328    Copy,
329    PartialEq,
330    Eq,
331    Hash,
332    EnumIsA,
333    EnumAsGetters,
334    VariantName,
335    Serialize,
336    Deserialize,
337    Drive,
338    DriveMut,
339)]
340pub enum BuiltinFunId {
341    /// `alloc::boxed::Box::new`
342    BoxNew,
343    /// Cast an array as a slice.
344    ///
345    /// Converted from [UnOp::ArrayToSlice]
346    ArrayToSliceShared,
347    /// Cast an array as a slice.
348    ///
349    /// Converted from [UnOp::ArrayToSlice]
350    ArrayToSliceMut,
351    /// `repeat(n, x)` returns an array where `x` has been replicated `n` times.
352    ///
353    /// We introduce this when desugaring the `ArrayRepeat` rvalue.
354    ArrayRepeat,
355    /// Converted from indexing `ProjectionElem`s. The signature depends on the parameters. It
356    /// could look like:
357    /// - `fn ArrayIndexShared<T,N>(&[T;N], usize) -> &T`
358    /// - `fn SliceIndexShared<T>(&[T], usize) -> &T`
359    /// - `fn ArraySubSliceShared<T,N>(&[T;N], usize, usize) -> &[T]`
360    /// - `fn SliceSubSliceMut<T>(&mut [T], usize, usize) -> &mut [T]`
361    /// - etc
362    Index(BuiltinIndexOp),
363    /// Build a raw pointer, from a data pointer and metadata. The metadata can be unit, if
364    /// building a thin pointer.
365    ///
366    /// Converted from [AggregateKind::RawPtr]
367    PtrFromParts(RefKind),
368}
369
370/// One of 8 built-in indexing operations.
371#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize, Drive, DriveMut)]
372pub struct BuiltinIndexOp {
373    /// Whether this is a slice or array.
374    #[drive(skip)]
375    pub is_array: bool,
376    /// Whether we're indexing mutably or not. Determines the type ofreference of the input and
377    /// output.
378    pub mutability: RefKind,
379    /// Whether we're indexing a single element or a subrange. If `true`, the function takes
380    /// two indices and the output is a slice; otherwise, the function take one index and the
381    /// output is a reference to a single element.
382    #[drive(skip)]
383    pub is_range: bool,
384}
385
386/// Reference to a function declaration or builtin function.
387#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
388pub struct MaybeBuiltinFunDeclRef {
389    #[charon::rename("fun_decl_id")]
390    pub id: FunId,
391    #[charon::rename("fun_decl_generics")]
392    pub generics: BoxedArgs,
393}
394
395/// Reference to a trait method.
396#[derive(Debug, Clone, Serialize, Deserialize, PartialEq, Eq, Hash, Drive, DriveMut)]
397pub struct TraitMethodRef {
398    pub trait_ref: TraitRef,
399    pub name: TraitItemName,
400    pub generics: BoxedArgs,
401    /// Reference to the method declaration; can be derived from the trait_ref, provided here for
402    /// convenience. The generic args are for the method, not for this function.
403    pub method_decl_id: FunDeclId,
404}
405
406#[derive(
407    Debug, Clone, PartialEq, Eq, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut, Hash,
408)]
409pub enum FunIdOrTraitMethodRef {
410    #[charon::rename("FunId")]
411    Fun(FunId),
412    /// If a trait: the reference to the trait and the id of the trait method.
413    /// The fun decl id is not really necessary - we put it here for convenience
414    /// purposes.
415    #[charon::rename("TraitMethod")]
416    Trait(TraitRef, TraitItemName, FunDeclId),
417}
418
419impl From<FunId> for FunIdOrTraitMethodRef {
420    fn from(id: FunId) -> Self {
421        Self::Fun(id)
422    }
423}
424impl From<FunDeclId> for FunIdOrTraitMethodRef {
425    fn from(id: FunDeclId) -> Self {
426        Self::Fun(id.into())
427    }
428}
429
430#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut, Hash)]
431pub struct FnPtr {
432    pub func: Box<FunIdOrTraitMethodRef>,
433    pub generics: BoxedArgs,
434}
435
436impl From<FunDeclRef> for FnPtr {
437    fn from(fn_ref: FunDeclRef) -> Self {
438        FnPtr {
439            func: Box::new(fn_ref.id.into()),
440            generics: fn_ref.generics,
441        }
442    }
443}
444
445/// A constant expression.
446///
447/// Only the [`RawConstantExpr::Literal`] and [`RawConstantExpr::Var`]
448/// cases are left in the final LLBC.
449///
450/// The other cases come from a straight translation from the MIR:
451///
452/// [`RawConstantExpr::Adt`] case:
453/// It is a bit annoying, but rustc treats some ADT and tuple instances as
454/// constants when generating MIR:
455/// - an enumeration with one variant and no fields is a constant.
456/// - a structure with no field is a constant.
457/// - sometimes, Rust stores the initialization of an ADT as a constant
458///   (if all the fields are constant) rather than as an aggregated value
459/// We later desugar those to regular ADTs, see [regularize_constant_adts.rs].
460///
461/// [`RawConstantExpr::Global`] case: access to a global variable. We later desugar it to
462/// a separate statement.
463///
464/// [`RawConstantExpr::Ref`] case: reference to a constant value. We later desugar it to a separate
465/// statement.
466///
467/// [`RawConstantExpr::FnPtr`] case: a function pointer (to a top-level function).
468///
469/// Remark:
470/// MIR seems to forbid more complex expressions like paths. For instance,
471/// reading the constant `a.b` is translated to `{ _1 = const a; _2 = (_1.0) }`.
472#[derive(
473    Debug,
474    PartialEq,
475    Eq,
476    Clone,
477    VariantName,
478    EnumIsA,
479    EnumAsGetters,
480    Serialize,
481    Deserialize,
482    Drive,
483    DriveMut,
484)]
485#[charon::variants_prefix("C")]
486pub enum RawConstantExpr {
487    Literal(Literal),
488    ///
489    /// In most situations:
490    /// Enumeration with one variant with no fields, structure with
491    /// no fields, unit (encoded as a 0-tuple).
492    ///
493    /// Less frequently: arbitrary ADT values.
494    ///
495    /// We eliminate this case in a micro-pass.
496    #[charon::opaque]
497    Adt(Option<VariantId>, Vec<ConstantExpr>),
498    #[charon::opaque]
499    Array(Vec<ConstantExpr>),
500    /// The value is a top-level constant/static.
501    ///
502    /// We eliminate this case in a micro-pass.
503    ///
504    /// Remark: constants can actually have generic parameters.
505    /// ```text
506    /// struct V<const N: usize, T> {
507    ///   x: [T; N],
508    /// }
509    ///
510    /// impl<const N: usize, T> V<N, T> {
511    ///   const LEN: usize = N; // This has generics <N, T>
512    /// }
513    ///
514    /// fn use_v<const N: usize, T>(v: V<N, T>) {
515    ///   let l = V::<N, T>::LEN; // We need to provided a substitution here
516    /// }
517    /// ```
518    #[charon::opaque]
519    Global(GlobalDeclRef),
520    ///
521    /// A trait constant.
522    ///
523    /// Ex.:
524    /// ```text
525    /// impl Foo for Bar {
526    ///   const C : usize = 32; // <-
527    /// }
528    /// ```
529    ///
530    /// Remark: trait constants can not be used in types, they are necessarily
531    /// values.
532    TraitConst(TraitRef, TraitItemName),
533    /// A shared reference to a constant value.
534    ///
535    /// We eliminate this case in a micro-pass.
536    #[charon::opaque]
537    Ref(Box<ConstantExpr>),
538    /// A pointer to a mutable static.
539    ///
540    /// We eliminate this case in a micro-pass.
541    #[charon::opaque]
542    Ptr(RefKind, Box<ConstantExpr>),
543    /// A const generic var
544    Var(ConstGenericDbVar),
545    /// Function pointer
546    FnPtr(FnPtr),
547    /// Raw memory value obtained from constant evaluation. Used when a more structured
548    /// representation isn't possible (e.g. for unions) or just isn't implemented yet.
549    #[drive(skip)]
550    RawMemory(Vec<u8>),
551    /// A constant expression that Charon still doesn't handle, along with the reason why.
552    #[drive(skip)]
553    Opaque(String),
554}
555
556#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
557pub struct ConstantExpr {
558    pub value: RawConstantExpr,
559    pub ty: Ty,
560}
561
562/// TODO: we could factor out [Rvalue] and function calls (for LLBC, not ULLBC).
563/// We can also factor out the unops, binops with the function calls.
564/// TODO: move the aggregate kind to operands
565/// TODO: we should prefix the type variants with "R" or "Rv", this would avoid collisions
566#[derive(
567    Debug, Clone, EnumToGetters, EnumAsGetters, EnumIsA, Serialize, Deserialize, Drive, DriveMut,
568)]
569pub enum Rvalue {
570    /// Lifts an operand as an rvalue.
571    Use(Operand),
572    /// Takes a reference to the given place.
573    #[charon::rename("RvRef")]
574    Ref(Place, BorrowKind),
575    /// Takes a raw pointer with the given mutability to the given place. This is generated by
576    /// pointer casts like `&v as *const _` or raw borrow expressions like `&raw const v.`
577    RawPtr(Place, RefKind),
578    /// Binary operations (note that we merge "checked" and "unchecked" binops)
579    BinaryOp(BinOp, Operand, Operand),
580    /// Unary operation (e.g. not, neg)
581    UnaryOp(UnOp, Operand),
582    /// Nullary operation (e.g. `size_of`)
583    NullaryOp(NullOp, Ty),
584    /// Discriminant (for enumerations).
585    /// Note that discriminant values have type isize. We also store the identifier
586    /// of the type from which we read the discriminant.
587    ///
588    /// This case is filtered in [crate::transform::remove_read_discriminant]
589    Discriminant(Place, TypeDeclId),
590    /// Creates an aggregate value, like a tuple, a struct or an enum:
591    /// ```text
592    /// l = List::Cons { value:x, tail:tl };
593    /// ```
594    /// Note that in some MIR passes (like optimized MIR), aggregate values are
595    /// decomposed, like below:
596    /// ```text
597    /// (l as List::Cons).value = x;
598    /// (l as List::Cons).tail = tl;
599    /// ```
600    /// Because we may want to plug our translation mechanism at various
601    /// places, we need to take both into accounts in the translation and in
602    /// our semantics. Aggregate value initialization is easy, you might want
603    /// to have a look at expansion of `Bottom` values for explanations about the
604    /// other case.
605    ///
606    /// Remark: in case of closures, the aggregated value groups the closure id
607    /// together with its state.
608    Aggregate(AggregateKind, Vec<Operand>),
609    /// Copy the value of the referenced global.
610    /// Not present in MIR; introduced in [simplify_constants.rs].
611    Global(GlobalDeclRef),
612    /// Reference the value of the global. This has type `&T` or `*mut T` depending on desired
613    /// mutability.
614    /// Not present in MIR; introduced in [simplify_constants.rs].
615    GlobalRef(GlobalDeclRef, RefKind),
616    /// Length of a memory location. The run-time length of e.g. a vector or a slice is
617    /// represented differently (but pretty-prints the same, FIXME).
618    /// Should be seen as a function of signature:
619    /// - `fn<T;N>(&[T;N]) -> usize`
620    /// - `fn<T>(&[T]) -> usize`
621    ///
622    /// We store the type argument and the const generic (the latter only for arrays).
623    ///
624    /// `Len` is automatically introduced by rustc, notably for the bound checks:
625    /// we eliminate it together with the bounds checks whenever possible.
626    /// There are however occurrences that we don't eliminate (yet).
627    /// For instance, for the following Rust code:
628    /// ```text
629    /// fn slice_pattern_4(x: &[()]) {
630    ///     match x {
631    ///         [_named] => (),
632    ///         _ => (),
633    ///     }
634    /// }
635    /// ```
636    /// rustc introduces a check that the length of the slice is exactly equal
637    /// to 1 and that we preserve.
638    Len(Place, Ty, Option<ConstGeneric>),
639    /// `Repeat(x, n)` creates an array where `x` is copied `n` times.
640    ///
641    /// We translate this to a function call for LLBC.
642    Repeat(Operand, Ty, ConstGeneric),
643    /// Transmutes a `*mut u8` (obtained from `malloc`) into shallow-initialized `Box<T>`. This
644    /// only appears as part of lowering `Box::new()` in some cases. We reconstruct the original
645    /// `Box::new()` call, but sometimes may fail to do so, leaking the expression.
646    ShallowInitBox(Operand, Ty),
647}
648
649/// An aggregated ADT.
650///
651/// Note that ADTs are desaggregated at some point in MIR. For instance, if
652/// we have in Rust:
653/// ```ignore
654///   let ls = Cons(hd, tl);
655/// ```
656///
657/// In MIR we have (yes, the discriminant update happens *at the end* for some
658/// reason):
659/// ```text
660///   (ls as Cons).0 = move hd;
661///   (ls as Cons).1 = move tl;
662///   discriminant(ls) = 0; // assuming `Cons` is the variant of index 0
663/// ```
664///
665/// Rem.: in the Aeneas semantics, both cases are handled (in case of desaggregated
666/// initialization, `ls` is initialized to `⊥`, then this `⊥` is expanded to
667/// `Cons (⊥, ⊥)` upon the first assignment, at which point we can initialize
668/// the field 0, etc.).
669#[derive(Debug, Clone, VariantIndexArity, Serialize, Deserialize, Drive, DriveMut)]
670#[charon::variants_prefix("Aggregated")]
671pub enum AggregateKind {
672    /// A struct, enum or union aggregate. The `VariantId`, if present, indicates this is an enum
673    /// and the aggregate uses that variant. The `FieldId`, if present, indicates this is a union
674    /// and the aggregate writes into that field. Otherwise this is a struct.
675    Adt(TypeDeclRef, Option<VariantId>, Option<FieldId>),
676    /// We don't put this with the ADT cas because this is the only built-in type
677    /// with aggregates, and it is a primitive type. In particular, it makes
678    /// sense to treat it differently because it has a variable number of fields.
679    Array(Ty, ConstGeneric),
680    /// Construct a raw pointer from a pointer value, and its metadata (can be unit, if building
681    /// a thin pointer). The type is the type of the pointee.
682    /// We lower this to a builtin function call for LLBC in [crate::transform::ops_to_function_calls].
683    RawPtr(Ty, RefKind),
684}
charon_lib/ast/expressions.rs

charon_lib/ast/
expressions.rs
