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

charon_lib/ast/bodies/
expressions.rs
