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

charon_lib/ast/
expressions.rs
