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

charon_lib/ast/
expressions.rs
