charon_lib/ast/
expressions.rs

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

charon_lib/ast/
expressions.rs
