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

charon_lib/ast/
expressions.rs
