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

charon_lib/ast/bodies/
expressions.rs
