charon_lib/ast/bodies/
expressions.rs

1//! Implements expressions: paths, operands, rvalues, lvalues
2use crate::ast::*;
3use derive_generic_visitor::{Drive, DriveMut, DriveTwo};
4use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName};
5use serde::{Deserialize, Serialize};
6use serde_state::{DeserializeState, SerializeState};
7use std::vec::Vec;
8
9/// An expression that evaluates to a value. This is the RHS of an assignment.
10#[derive(
11    Debug,
12    PartialEq,
13    Eq,
14    Clone,
15    EnumToGetters,
16    EnumAsGetters,
17    EnumIsA,
18    SerializeState,
19    DeserializeState,
20    Drive,
21    DriveMut,
22    DriveTwo,
23)]
24pub enum Rvalue {
25    /// Lifts an operand as an rvalue.
26    Use(Operand, #[drive(skip)] WithRetag),
27    /// Takes a reference to the given place.
28    /// The `Operand` refers to the init value of the metadata, it is `()` if no metadata
29    #[cfg_attr(feature = "charon_on_charon", charon::rename("RvRef"))]
30    Ref {
31        place: Place,
32        #[serde_state(stateless)]
33        kind: BorrowKind,
34        ptr_metadata: Operand,
35    },
36    /// Takes a raw pointer with the given mutability to the given place. This is generated by
37    /// pointer casts like `&v as *const _` or raw borrow expressions like `&raw const v.`
38    /// Like `Ref`, the `Operand` refers to the init value of the metadata, it is `()` if no metadata.
39    RawPtr {
40        place: Place,
41        kind: RefKind,
42        ptr_metadata: Operand,
43    },
44    /// Binary operations (note that we merge "checked" and "unchecked" binops)
45    BinaryOp(BinOp, Operand, Operand),
46    /// Unary operation (e.g. not, neg)
47    UnaryOp(UnOp, Operand),
48    /// Nullary operation (e.g. `size_of`)
49    NullaryOp(NullOp, Ty),
50    /// Discriminant read. Reads the discriminant value of an enum. The place must have the type of
51    /// an enum. The discriminant in question is the one in the `discriminant` field of the
52    /// corresponding `Variant`. This can be different than the value stored in memory (called
53    /// `tag`); that one is described by [`Discriminator`] and [`VariantLayout::tagger`].
54    Discriminant(Place),
55    /// Creates an aggregate value, like a tuple, a struct or an enum:
56    /// ```text
57    /// l = List::Cons { value:x, tail:tl };
58    /// ```
59    /// Note that in some MIR passes (like optimized MIR), aggregate values are
60    /// decomposed, like below:
61    /// ```text
62    /// (l as List::Cons).value = x;
63    /// (l as List::Cons).tail = tl;
64    /// ```
65    /// Because we may want to plug our translation mechanism at various
66    /// places, we need to take both into accounts in the translation and in
67    /// our semantics. Aggregate value initialization is easy, you might want
68    /// to have a look at expansion of `Bottom` values for explanations about the
69    /// other case.
70    ///
71    /// Remark: in case of closures, the aggregated value groups the closure id
72    /// together with its state.
73    Aggregate(AggregateKind, Vec<Operand>),
74    /// Length of a place of type `[T]` or `[T; N]`. This applies to the place itself, not to a
75    /// pointer value. This is inserted by rustc in a single case: slice patterns.
76    /// ```text
77    /// fn slice_pattern_4(x: &[()]) {
78    ///     match x {
79    ///         [_named] => (),
80    ///         _ => (),
81    ///     }
82    /// }
83    /// ```
84    Len(Place, Ty, Option<Box<ConstantExpr>>),
85    /// `Repeat(x, n)` creates an array where `x` is copied `n` times.
86    ///
87    /// We translate this to a function call for LLBC.
88    Repeat(Operand, Ty, Box<ConstantExpr>),
89}
90
91#[derive(
92    Debug,
93    PartialEq,
94    Eq,
95    Clone,
96    EnumIsA,
97    EnumToGetters,
98    EnumAsGetters,
99    VariantName,
100    SerializeState,
101    DeserializeState,
102    Drive,
103    DriveMut,
104    DriveTwo,
105)]
106#[serde_state(state_implements = HashConsSerializerState)] // Avoid corecursive impls due to perfect derive
107pub enum Operand {
108    Copy(Place),
109    Move(Place),
110    /// Constant value (including constant and static variables)
111    #[cfg_attr(feature = "charon_on_charon", charon::rename("Constant"))]
112    Const(Box<ConstantExpr>),
113}
114
115/// Used for [`Rvalue::Use`] to indicate whether the operand should be retagged (this is used
116/// for Rust's aliasing model).
117#[derive(
118    Debug, Hash, PartialEq, Eq, Clone, SerializeState, DeserializeState, Drive, DriveMut, DriveTwo,
119)]
120#[cfg_attr(feature = "charon_on_charon", charon::variants_suffix("Retag"))]
121pub enum WithRetag {
122    No,
123    Yes,
124}
125
126#[derive(Debug, PartialEq, Eq, Copy, Clone, Serialize, Deserialize)]
127#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("O"))]
128pub enum OverflowMode {
129    /// If this operation overflows, it panics. Only exists in debug mode, for instance in
130    /// `a + b`, and only if `--reconstruct-fallible-operations` is passed to Charon. Otherwise the
131    /// bound check will be explicit.
132    Panic,
133    /// If this operation overflows, it is UB; for instance in `core::num::unchecked_add`. This can
134    /// exists in safe code, but will always be preceded by a bounds check.
135    UB,
136    /// If this operation overflows, it wraps around for instance in `core::num::wrapping_add`,
137    /// or `a + b` in release mode.
138    Wrap,
139}
140
141/// Binary operations.
142#[derive(
143    Debug,
144    PartialEq,
145    Eq,
146    Copy,
147    Clone,
148    EnumIsA,
149    VariantName,
150    SerializeState,
151    DeserializeState,
152    Drive,
153    DriveMut,
154    DriveTwo,
155)]
156#[cfg_attr(feature = "charon_on_charon", charon::rename("Binop"))]
157#[serde_state(stateless)]
158pub enum BinOp {
159    BitXor,
160    BitAnd,
161    BitOr,
162    Eq,
163    Lt,
164    Le,
165    Ne,
166    Ge,
167    Gt,
168    #[drive(skip)]
169    Add(OverflowMode),
170    #[drive(skip)]
171    Sub(OverflowMode),
172    #[drive(skip)]
173    Mul(OverflowMode),
174    #[drive(skip)]
175    Div(OverflowMode),
176    #[drive(skip)]
177    Rem(OverflowMode),
178    /// Returns `(result, did_overflow)`, where `result` is the result of the operation with
179    /// wrapping semantics, and `did_overflow` is a boolean that indicates whether the operation
180    /// overflowed. This operation does not fail.
181    AddChecked,
182    /// Like `AddChecked`.
183    SubChecked,
184    /// Like `AddChecked`.
185    MulChecked,
186    /// Fails if the shift is bigger than the bit-size of the type.
187    #[drive(skip)]
188    Shl(OverflowMode),
189    /// Fails if the shift is bigger than the bit-size of the type.
190    #[drive(skip)]
191    Shr(OverflowMode),
192    /// `BinOp(Offset, ptr, n)` for `ptr` a pointer to type `T` offsets `ptr` by `n * size_of::<T>()`.
193    Offset,
194    /// `BinOp(Cmp, a, b)` returns `-1u8` if `a < b`, `0u8` if `a == b`, and `1u8` if `a > b`.
195    Cmp,
196}
197
198/// Unary operation
199#[derive(
200    Debug,
201    PartialEq,
202    Eq,
203    Clone,
204    EnumIsA,
205    VariantName,
206    SerializeState,
207    DeserializeState,
208    Drive,
209    DriveMut,
210    DriveTwo,
211)]
212#[cfg_attr(feature = "charon_on_charon", charon::rename("Unop"))]
213pub enum UnOp {
214    Not,
215    /// This can overflow, for `-i::MIN`.
216    #[drive(skip)]
217    #[serde_state(stateless)]
218    Neg(OverflowMode),
219    /// Casts are rvalues in MIR, but we treat them as unops.
220    Cast(CastKind),
221}
222
223/// For all the variants: the first type gives the source type, the second one gives
224/// the destination type.
225#[derive(
226    Debug,
227    PartialEq,
228    Eq,
229    Clone,
230    EnumIsA,
231    VariantName,
232    SerializeState,
233    DeserializeState,
234    Drive,
235    DriveMut,
236    DriveTwo,
237)]
238#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Cast"))]
239pub enum CastKind {
240    /// Conversion between types in `{Integer, Bool}`
241    /// Remark: for now we don't support conversions with Char.
242    Scalar(LiteralTy, LiteralTy),
243    RawPtr(Ty, Ty),
244    FnPtr(Ty, Ty),
245    /// [Unsize coercion](https://doc.rust-lang.org/std/ops/trait.CoerceUnsized.html). This is
246    /// either `[T; N]` -> `[T]` or `T: Trait` -> `dyn Trait` coercions, behind a pointer
247    /// (reference, `Box`, or other type that implements `CoerceUnsized`).
248    ///
249    /// The special case of `&[T; N]` -> `&[T]` coercion is caught by `UnOp::ArrayToSlice`.
250    Unsize(Ty, Ty, UnsizingMetadata),
251    /// Reinterprets the bits of a value of one type as another type, i.e. exactly what
252    /// [`std::mem::transmute`] does.
253    Transmute(Ty, Ty),
254    /// Converts a receiver type with `dyn Trait<...>` to a concrete type `T`, used in vtable method shims.
255    /// Valid conversions are references, raw pointers, and (optionally) boxes:
256    /// - `&[mut] dyn Trait<...>` -> `&[mut] T`
257    /// - `*[mut] dyn Trait<...>` -> `*[mut] T`
258    /// - `Box<dyn Trait<...>>` -> `Box<T>` when no `--raw-boxes`
259    ///
260    /// For possible receivers, see: <https://doc.rust-lang.org/reference/items/traits.html#dyn-compatibility>.
261    /// Other receivers, e.g., `Rc` should be unpacked before the cast and re-boxed after.
262    /// FIXME(ssyram): but this is not implemented yet, namely, there may still be
263    ///     something like `Rc<dyn Trait<...>> -> Rc<T>` in the types.
264    Concretize(Ty, Ty),
265}
266
267/// Nullary operation
268#[derive(
269    Debug,
270    PartialEq,
271    Eq,
272    Clone,
273    EnumIsA,
274    VariantName,
275    SerializeState,
276    DeserializeState,
277    Drive,
278    DriveMut,
279    DriveTwo,
280)]
281#[cfg_attr(feature = "charon_on_charon", charon::rename("Nullop"))]
282pub enum NullOp {
283    SizeOf,
284    AlignOf,
285    OffsetOf(TypeDeclRef, Option<VariantId>, FieldId),
286    UbChecks,
287    OverflowChecks,
288    ContractChecks,
289}
290
291#[derive(
292    Debug,
293    PartialEq,
294    Eq,
295    Copy,
296    Clone,
297    EnumIsA,
298    EnumAsGetters,
299    Serialize,
300    Deserialize,
301    Drive,
302    DriveMut,
303    DriveTwo,
304)]
305#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("B"))]
306pub enum BorrowKind {
307    Shared,
308    Mut,
309    /// See <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.MutBorrowKind.html#variant.TwoPhaseBorrow>
310    /// and <https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html>
311    TwoPhaseMut,
312    /// Those are typically introduced when using guards in matches, to make sure guards don't
313    /// change the variant of an enum value while me match over it.
314    ///
315    /// See <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.FakeBorrowKind.html#variant.Shallow>.
316    Shallow,
317    /// Data must be immutable but not aliasable. In other words you can't mutate the data but you
318    /// can mutate *through it*, e.g. if it points to a `&mut T`. This is only used in closure
319    /// captures, e.g.
320    /// ```rust,ignore
321    /// let mut z = 3;
322    /// let x: &mut isize = &mut z;
323    /// let y = || *x += 5;
324    /// ```
325    /// Here the captured variable can't be `&mut &mut x` since the `x` binding is not mutable, yet
326    /// we must be able to mutate what it points to.
327    ///
328    /// See <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.MutBorrowKind.html#variant.ClosureCapture>.
329    UniqueImmutable,
330}
331
332#[derive(
333    Debug,
334    PartialEq,
335    Eq,
336    PartialOrd,
337    Ord,
338    Clone,
339    EnumIsA,
340    VariantName,
341    SerializeState,
342    DeserializeState,
343    Drive,
344    DriveMut,
345    DriveTwo,
346    Hash,
347)]
348#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Meta"))]
349pub enum UnsizingMetadata {
350    /// Cast from `[T; N]` to `[T]`.
351    Length(Box<ConstantExpr>),
352    /// Cast from a sized value to a `dyn Trait` value. The `TraitRef` is the proof of the `dyn
353    /// Trait` predicate; the constant expression is a reference to the vtable `static` value.
354    VTable(TraitRef, Box<ConstantExpr>),
355    /// Cast from `dyn Trait` to `dyn OtherTrait`. The fields indicate how to retreive the vtable:
356    /// it's always either the same we already had, or the vtable for a (possibly nested) supertrait.
357    ///
358    /// Note that we cheat in one case: when upcasting to a marker trait (e.g. `dyn Trait -> dyn
359    /// Sized`), we keep the current vtable.
360    VTableUpcast(Vec<FieldId>),
361    Unknown,
362}
363
364/// An aggregated ADT.
365///
366/// Note that ADTs are desaggregated at some point in MIR. For instance, if
367/// we have in Rust:
368/// ```ignore
369///   let ls = Cons(hd, tl);
370/// ```
371///
372/// In MIR we have (yes, the discriminant update happens *at the end* for some
373/// reason):
374/// ```text
375///   (ls as Cons).0 = move hd;
376///   (ls as Cons).1 = move tl;
377///   discriminant(ls) = 0; // assuming `Cons` is the variant of index 0
378/// ```
379///
380/// Rem.: in the Aeneas semantics, both cases are handled (in case of desaggregated
381/// initialization, `ls` is initialized to `⊥`, then this `⊥` is expanded to
382/// `Cons (⊥, ⊥)` upon the first assignment, at which point we can initialize
383/// the field 0, etc.).
384#[derive(
385    Debug,
386    PartialEq,
387    Eq,
388    Clone,
389    VariantIndexArity,
390    SerializeState,
391    DeserializeState,
392    Drive,
393    DriveMut,
394    DriveTwo,
395)]
396#[cfg_attr(feature = "charon_on_charon", charon::variants_prefix("Aggregated"))]
397pub enum AggregateKind {
398    /// A struct, enum or union aggregate. The `VariantId`, if present, indicates this is an enum
399    /// and the aggregate uses that variant. The `FieldId`, if present, indicates this is a union
400    /// and the aggregate writes into that field. Otherwise this is a struct.
401    Adt(TypeDeclRef, Option<VariantId>, Option<FieldId>),
402    /// We don't put this with the ADT cas because this is the only built-in type
403    /// with aggregates, and it is a primitive type. In particular, it makes
404    /// sense to treat it differently because it has a variable number of fields.
405    Array(Ty, Box<ConstantExpr>),
406    /// Construct a raw pointer from a pointer value, and its metadata (can be unit, if building
407    /// a thin pointer). The type is the type of the pointee.
408    /// We lower this to a builtin function call for LLBC in [crate::transform::simplify_output::ops_to_function_calls].
409    RawPtr(Ty, RefKind),
410}
411
412impl Rvalue {
413    pub fn unit_value() -> Self {
414        Rvalue::Aggregate(
415            AggregateKind::Adt(
416                TypeDeclRef {
417                    id: TypeId::Builtin(BuiltinTy::Tuple),
418                    generics: Box::new(GenericArgs::empty()),
419                },
420                None,
421                None,
422            ),
423            Vec::new(),
424        )
425    }
426}
427
428impl Operand {
429    pub fn mk_const_unit() -> Self {
430        Operand::Const(Box::new(ConstantExpr::mk_unit()))
431    }
432
433    pub fn ty(&self) -> &Ty {
434        match self {
435            Operand::Copy(place) | Operand::Move(place) => place.ty(),
436            Operand::Const(constant_expr) => &constant_expr.ty,
437        }
438    }
439}
440
441impl BorrowKind {
442    pub fn mutable(x: bool) -> Self {
443        if x { Self::Mut } else { Self::Shared }
444    }
445}
446
447impl BinOp {
448    pub fn with_overflow(&self, overflow: OverflowMode) -> Self {
449        match self {
450            BinOp::Add(_) | BinOp::AddChecked => BinOp::Add(overflow),
451            BinOp::Sub(_) | BinOp::SubChecked => BinOp::Sub(overflow),
452            BinOp::Mul(_) | BinOp::MulChecked => BinOp::Mul(overflow),
453            BinOp::Div(_) => BinOp::Div(overflow),
454            BinOp::Rem(_) => BinOp::Rem(overflow),
455            BinOp::Shl(_) => BinOp::Shl(overflow),
456            BinOp::Shr(_) => BinOp::Shr(overflow),
457            _ => {
458                panic!(
459                    "Cannot set overflow mode for this binary operator: {:?}",
460                    self
461                );
462            }
463        }
464    }
465}
466
467impl UnOp {
468    pub fn with_overflow(&self, overflow: OverflowMode) -> Self {
469        match self {
470            UnOp::Neg(_) => UnOp::Neg(overflow),
471            _ => {
472                panic!(
473                    "Cannot set overflow mode for this unary operator: {:?}",
474                    self
475                );
476            }
477        }
478    }
479}
480
481impl From<BorrowKind> for RefKind {
482    fn from(value: BorrowKind) -> Self {
483        match value {
484            BorrowKind::Shared | BorrowKind::Shallow => RefKind::Shared,
485            BorrowKind::Mut | BorrowKind::TwoPhaseMut | BorrowKind::UniqueImmutable => RefKind::Mut,
486        }
487    }
488}
489
490impl From<RefKind> for BorrowKind {
491    fn from(value: RefKind) -> Self {
492        match value {
493            RefKind::Shared => BorrowKind::Shared,
494            RefKind::Mut => BorrowKind::Mut,
495        }
496    }
497}
charon_lib/ast/bodies/expressions.rs

charon_lib/ast/bodies/
expressions.rs
