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