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