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 std::vec::Vec;
8
9#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
10pub struct Place {
11    pub kind: PlaceKind,
12    pub ty: Ty,
13}
14
15#[derive(
16    Debug,
17    PartialEq,
18    Eq,
19    Clone,
20    EnumIsA,
21    EnumAsGetters,
22    EnumToGetters,
23    Serialize,
24    Deserialize,
25    Drive,
26    DriveMut,
27)]
28#[charon::variants_prefix("Place")]
29pub enum PlaceKind {
30    Local(LocalId),
31    Projection(Box<Place>, ProjectionElem),
32}
33
34/// Note that we don't have the equivalent of "downcasts".
35/// Downcasts are actually necessary, for instance when initializing enumeration
36/// values: the value is initially `Bottom`, and we need a way of knowing the
37/// variant.
38/// For example:
39/// `((_0 as Right).0: T2) = move _1;`
40/// In MIR, downcasts always happen before field projections: in our internal
41/// language, we thus merge downcasts and field projections.
42#[derive(
43    Debug,
44    PartialEq,
45    Eq,
46    Clone,
47    EnumIsA,
48    EnumAsGetters,
49    EnumToGetters,
50    VariantName,
51    Serialize,
52    Deserialize,
53    Drive,
54    DriveMut,
55)]
56pub enum ProjectionElem {
57    /// Dereference a shared/mutable reference, a box, or a raw pointer.
58    Deref,
59    /// Projection from ADTs (variants, structures).
60    /// We allow projections to be used as left-values and right-values.
61    /// We should never have projections to fields of symbolic variants (they
62    /// should have been expanded before through a match).
63    Field(FieldProjKind, FieldId),
64    /// MIR imposes that the argument to an index projection be a local variable, meaning
65    /// that even constant indices into arrays are let-bound as separate variables.
66    /// We **eliminate** this variant in a micro-pass.
67    #[charon::opaque]
68    Index {
69        offset: Box<Operand>,
70        #[drive(skip)]
71        from_end: bool,
72    },
73    /// Take a subslice of a slice or array. If `from_end` is `true` this is
74    /// `slice[from..slice.len() - to]`, otherwise this is `slice[from..to]`.
75    /// We **eliminate** this variant in a micro-pass.
76    #[charon::opaque]
77    Subslice {
78        from: Box<Operand>,
79        to: Box<Operand>,
80        #[drive(skip)]
81        from_end: bool,
82    },
83}
84
85#[derive(
86    Debug,
87    PartialEq,
88    Eq,
89    Copy,
90    Clone,
91    EnumIsA,
92    EnumAsGetters,
93    Serialize,
94    Deserialize,
95    Drive,
96    DriveMut,
97)]
98#[charon::variants_prefix("Proj")]
99pub enum FieldProjKind {
100    Adt(TypeDeclId, Option<VariantId>),
101    /// If we project from a tuple, the projection kind gives the arity of the tuple.
102    #[drive(skip)]
103    Tuple(usize),
104    /// Access to a field in a closure state.
105    /// We eliminate this in a micro-pass ([crate::update_closure_signatures]).
106    #[charon::opaque]
107    ClosureState,
108}
109
110#[derive(
111    Debug,
112    PartialEq,
113    Eq,
114    Copy,
115    Clone,
116    EnumIsA,
117    EnumAsGetters,
118    Serialize,
119    Deserialize,
120    Drive,
121    DriveMut,
122)]
123#[charon::variants_prefix("B")]
124pub enum BorrowKind {
125    Shared,
126    Mut,
127    /// See <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.MutBorrowKind.html#variant.TwoPhaseBorrow>
128    /// and <https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html>
129    TwoPhaseMut,
130    /// Those are typically introduced when using guards in matches, to make sure guards don't
131    /// change the variant of an enum value while me match over it.
132    ///
133    /// See <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.FakeBorrowKind.html#variant.Shallow>.
134    Shallow,
135    /// Data must be immutable but not aliasable. In other words you can't mutate the data but you
136    /// can mutate *through it*, e.g. if it points to a `&mut T`. This is only used in closure
137    /// captures, e.g.
138    /// ```rust,ignore
139    /// let mut z = 3;
140    /// let x: &mut isize = &mut z;
141    /// let y = || *x += 5;
142    /// ```
143    /// Here the captured variable can't be `&mut &mut x` since the `x` binding is not mutable, yet
144    /// we must be able to mutate what it points to.
145    ///
146    /// See <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.MutBorrowKind.html#variant.ClosureCapture>.
147    UniqueImmutable,
148}
149
150/// Unary operation
151#[derive(
152    Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
153)]
154#[charon::rename("Unop")]
155pub enum UnOp {
156    Not,
157    /// This can overflow. In practice, rust introduces an assert before
158    /// (in debug mode) to check that it is not equal to the minimum integer
159    /// value (for the proper type).
160    Neg,
161    /// Retreive the metadata part of a fat pointer. For slices, this retreives their length.
162    PtrMetadata,
163    /// Casts are rvalues in MIR, but we treat them as unops.
164    Cast(CastKind),
165    /// Coercion from array (i.e., [T; N]) to slice.
166    ///
167    /// **Remark:** We introduce this unop when translating from MIR, **then transform**
168    /// it to a function call in a micro pass. The type and the scalar value are not
169    /// *necessary* as we can retrieve them from the context, but storing them here is
170    /// very useful. The [RefKind] argument states whethere we operate on a mutable
171    /// or a shared borrow to an array.
172    #[charon::opaque]
173    ArrayToSlice(RefKind, Ty, ConstGeneric),
174}
175
176/// Nullary operation
177#[derive(
178    Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
179)]
180#[charon::rename("Nullop")]
181pub enum NullOp {
182    SizeOf,
183    AlignOf,
184    #[drive(skip)]
185    OffsetOf(Vec<(usize, FieldId)>),
186    UbChecks,
187}
188
189/// For all the variants: the first type gives the source type, the second one gives
190/// the destination type.
191#[derive(
192    Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
193)]
194#[charon::variants_prefix("Cast")]
195pub enum CastKind {
196    /// Conversion between types in {Integer, Bool}
197    /// Remark: for now we don't support conversions with Char.
198    Scalar(LiteralTy, LiteralTy),
199    RawPtr(Ty, Ty),
200    FnPtr(Ty, Ty),
201    /// [Unsize coercion](https://doc.rust-lang.org/std/ops/trait.CoerceUnsized.html). This is
202    /// either `[T; N]` -> `[T]` or `T: Trait` -> `dyn Trait` coercions, behind a pointer
203    /// (reference, `Box`, or other type that implements `CoerceUnsized`).
204    ///
205    /// The special case of `&[T; N]` -> `&[T]` coercion is caught by `UnOp::ArrayToSlice`.
206    Unsize(Ty, Ty),
207    /// Reinterprets the bits of a value of one type as another type, i.e. exactly what
208    /// [`std::mem::transmute`] does.
209    Transmute(Ty, Ty),
210}
211
212/// Binary operations.
213#[derive(
214    Debug, PartialEq, Eq, Copy, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
215)]
216#[charon::rename("Binop")]
217pub enum BinOp {
218    BitXor,
219    BitAnd,
220    BitOr,
221    Eq,
222    Lt,
223    Le,
224    Ne,
225    Ge,
226    Gt,
227    /// Fails if the divisor is 0, or if the operation is `int::MIN / -1`.
228    Div,
229    /// Fails if the divisor is 0, or if the operation is `int::MIN % -1`.
230    Rem,
231    /// Fails on overflow.
232    /// Not present in MIR: this is introduced by the `remove_dynamic_checks` pass.
233    Add,
234    /// Fails on overflow.
235    /// Not present in MIR: this is introduced by the `remove_dynamic_checks` pass.
236    Sub,
237    /// Fails on overflow.
238    /// Not present in MIR: this is introduced by the `remove_dynamic_checks` pass.
239    Mul,
240    /// Wraps on overflow.
241    WrappingAdd,
242    /// Wraps on overflow.
243    WrappingSub,
244    /// Wraps on overflow.
245    WrappingMul,
246    /// Returns `(result, did_overflow)`, where `result` is the result of the operation with
247    /// wrapping semantics, and `did_overflow` is a boolean that indicates whether the operation
248    /// overflowed. This operation does not fail.
249    CheckedAdd,
250    /// Like `CheckedAdd`.
251    CheckedSub,
252    /// Like `CheckedAdd`.
253    CheckedMul,
254    /// Fails if the shift is bigger than the bit-size of the type.
255    Shl,
256    /// Fails if the shift is bigger than the bit-size of the type.
257    Shr,
258    /// `BinOp(Offset, ptr, n)` for `ptr` a pointer to type `T` offsets `ptr` by `n * size_of::<T>()`.
259    Offset,
260    /// `BinOp(Cmp, a, b)` returns `-1u8` if `a < b`, `0u8` if `a == b`, and `1u8` if `a > b`.
261    Cmp,
262}
263
264#[derive(
265    Debug,
266    PartialEq,
267    Eq,
268    Clone,
269    EnumIsA,
270    EnumToGetters,
271    EnumAsGetters,
272    VariantName,
273    Serialize,
274    Deserialize,
275    Drive,
276    DriveMut,
277)]
278pub enum Operand {
279    Copy(Place),
280    Move(Place),
281    /// Constant value (including constant and static variables)
282    #[charon::rename("Constant")]
283    Const(Box<ConstantExpr>),
284}
285
286/// A function identifier. See [crate::ullbc_ast::Terminator]
287#[derive(
288    Debug,
289    Clone,
290    PartialEq,
291    Eq,
292    EnumIsA,
293    EnumAsGetters,
294    VariantName,
295    Serialize,
296    Deserialize,
297    Drive,
298    DriveMut,
299)]
300#[charon::variants_prefix("F")]
301pub enum FunId {
302    /// A "regular" function (function local to the crate, external function
303    /// not treated as a primitive one).
304    Regular(FunDeclId),
305    /// A primitive function, coming from a standard library (for instance:
306    /// `alloc::boxed::Box::new`).
307    /// TODO: rename to "Primitive"
308    #[charon::rename("FBuiltin")]
309    Builtin(BuiltinFunId),
310}
311
312/// An built-in function identifier, identifying a function coming from a
313/// standard library.
314#[derive(
315    Debug,
316    Clone,
317    Copy,
318    PartialEq,
319    Eq,
320    EnumIsA,
321    EnumAsGetters,
322    VariantName,
323    Serialize,
324    Deserialize,
325    Drive,
326    DriveMut,
327)]
328pub enum BuiltinFunId {
329    /// `alloc::boxed::Box::new`
330    BoxNew,
331    /// Cast an array as a slice.
332    ///
333    /// Converted from [UnOp::ArrayToSlice]
334    ArrayToSliceShared,
335    /// Cast an array as a slice.
336    ///
337    /// Converted from [UnOp::ArrayToSlice]
338    ArrayToSliceMut,
339    /// `repeat(n, x)` returns an array where `x` has been replicated `n` times.
340    ///
341    /// We introduce this when desugaring the [ArrayRepeat] rvalue.
342    ArrayRepeat,
343    /// Converted from indexing `ProjectionElem`s. The signature depends on the parameters. It
344    /// could look like:
345    /// - `fn ArrayIndexShared<T,N>(&[T;N], usize) -> &T`
346    /// - `fn SliceIndexShared<T>(&[T], usize) -> &T`
347    /// - `fn ArraySubSliceShared<T,N>(&[T;N], usize, usize) -> &[T]`
348    /// - `fn SliceSubSliceMut<T>(&mut [T], usize, usize) -> &mut [T]`
349    /// - etc
350    Index(BuiltinIndexOp),
351    /// Build a raw pointer, from a data pointer and metadata. The metadata can be unit, if
352    /// building a thin pointer.
353    ///
354    /// Converted from [AggregateKind::RawPtr]
355    PtrFromParts(RefKind),
356}
357
358/// One of 8 built-in indexing operations.
359#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
360pub struct BuiltinIndexOp {
361    /// Whether this is a slice or array.
362    #[drive(skip)]
363    pub is_array: bool,
364    /// Whether we're indexing mutably or not. Determines the type ofreference of the input and
365    /// output.
366    pub mutability: RefKind,
367    /// Whether we're indexing a single element or a subrange. If `true`, the function takes
368    /// two indices and the output is a slice; otherwise, the function take one index and the
369    /// output is a reference to a single element.
370    #[drive(skip)]
371    pub is_range: bool,
372}
373
374#[derive(Debug, Clone, PartialEq, Eq, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut)]
375pub enum FunIdOrTraitMethodRef {
376    #[charon::rename("FunId")]
377    Fun(FunId),
378    /// If a trait: the reference to the trait and the id of the trait method.
379    /// The fun decl id is not really necessary - we put it here for convenience
380    /// purposes.
381    #[charon::rename("TraitMethod")]
382    Trait(TraitRef, TraitItemName, FunDeclId),
383}
384
385#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
386pub struct FnPtr {
387    pub func: Box<FunIdOrTraitMethodRef>,
388    pub generics: BoxedArgs,
389}
390
391/// A constant expression.
392///
393/// Only the [Literal] and [Var] cases are left in the final LLBC.
394///
395/// The other cases come from a straight translation from the MIR:
396///
397/// [Adt] case:
398/// It is a bit annoying, but rustc treats some ADT and tuple instances as
399/// constants when generating MIR:
400/// - an enumeration with one variant and no fields is a constant.
401/// - a structure with no field is a constant.
402/// - sometimes, Rust stores the initialization of an ADT as a constant
403///   (if all the fields are constant) rather than as an aggregated value
404/// We later desugar those to regular ADTs, see [regularize_constant_adts.rs].
405///
406/// [Global] case: access to a global variable. We later desugar it to
407/// a separate statement.
408///
409/// [Ref] case: reference to a constant value. We later desugar it to a separate
410/// statement.
411///
412/// [FnPtr] case: a function pointer (to a top-level function).
413///
414/// Remark:
415/// MIR seems to forbid more complex expressions like paths. For instance,
416/// reading the constant `a.b` is translated to `{ _1 = const a; _2 = (_1.0) }`.
417#[derive(
418    Debug,
419    PartialEq,
420    Eq,
421    Clone,
422    VariantName,
423    EnumIsA,
424    EnumAsGetters,
425    Serialize,
426    Deserialize,
427    Drive,
428    DriveMut,
429)]
430#[charon::variants_prefix("C")]
431pub enum RawConstantExpr {
432    Literal(Literal),
433    ///
434    /// In most situations:
435    /// Enumeration with one variant with no fields, structure with
436    /// no fields, unit (encoded as a 0-tuple).
437    ///
438    /// Less frequently: arbitrary ADT values.
439    ///
440    /// We eliminate this case in a micro-pass.
441    #[charon::opaque]
442    Adt(Option<VariantId>, Vec<ConstantExpr>),
443    #[charon::opaque]
444    Array(Vec<ConstantExpr>),
445    /// The value is a top-level constant/static.
446    ///
447    /// We eliminate this case in a micro-pass.
448    ///
449    /// Remark: constants can actually have generic parameters.
450    /// ```text
451    /// struct V<const N: usize, T> {
452    ///   x: [T; N],
453    /// }
454    ///
455    /// impl<const N: usize, T> V<N, T> {
456    ///   const LEN: usize = N; // This has generics <N, T>
457    /// }
458    ///
459    /// fn use_v<const N: usize, T>(v: V<N, T>) {
460    ///   let l = V::<N, T>::LEN; // We need to provided a substitution here
461    /// }
462    /// ```
463    #[charon::opaque]
464    Global(GlobalDeclRef),
465    ///
466    /// A trait constant.
467    ///
468    /// Ex.:
469    /// ```text
470    /// impl Foo for Bar {
471    ///   const C : usize = 32; // <-
472    /// }
473    /// ```
474    ///
475    /// Remark: trait constants can not be used in types, they are necessarily
476    /// values.
477    TraitConst(TraitRef, TraitItemName),
478    /// A shared reference to a constant value.
479    ///
480    /// We eliminate this case in a micro-pass.
481    #[charon::opaque]
482    Ref(Box<ConstantExpr>),
483    /// A mutable pointer to a mutable static.
484    ///
485    /// We eliminate this case in a micro-pass.
486    #[charon::opaque]
487    MutPtr(Box<ConstantExpr>),
488    /// A const generic var
489    Var(ConstGenericDbVar),
490    /// Function pointer
491    FnPtr(FnPtr),
492    /// Raw memory value obtained from constant evaluation. Used when a more structured
493    /// representation isn't possible (e.g. for unions) or just isn't implemented yet.
494    #[drive(skip)]
495    RawMemory(Vec<u8>),
496    /// A constant expression that Charon still doesn't handle, along with the reason why.
497    #[drive(skip)]
498    Opaque(String),
499}
500
501#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
502pub struct ConstantExpr {
503    pub value: RawConstantExpr,
504    pub ty: Ty,
505}
506
507/// TODO: we could factor out [Rvalue] and function calls (for LLBC, not ULLBC).
508/// We can also factor out the unops, binops with the function calls.
509/// TODO: move the aggregate kind to operands
510/// TODO: we should prefix the type variants with "R" or "Rv", this would avoid collisions
511#[derive(
512    Debug, Clone, EnumToGetters, EnumAsGetters, EnumIsA, Serialize, Deserialize, Drive, DriveMut,
513)]
514pub enum Rvalue {
515    /// Lifts an operand as an rvalue.
516    Use(Operand),
517    /// Takes a reference to the given place.
518    #[charon::rename("RvRef")]
519    Ref(Place, BorrowKind),
520    /// Takes a raw pointer with the given mutability to the given place. This is generated by
521    /// pointer casts like `&v as *const _` or raw borrow expressions like `&raw const v.`
522    RawPtr(Place, RefKind),
523    /// Binary operations (note that we merge "checked" and "unchecked" binops)
524    BinaryOp(BinOp, Operand, Operand),
525    /// Unary operation (e.g. not, neg)
526    UnaryOp(UnOp, Operand),
527    /// Nullary operation (e.g. `size_of`)
528    NullaryOp(NullOp, Ty),
529    /// Discriminant (for enumerations).
530    /// Note that discriminant values have type isize. We also store the identifier
531    /// of the type from which we read the discriminant.
532    ///
533    /// This case is filtered in [crate::remove_read_discriminant]
534    Discriminant(Place, TypeDeclId),
535    /// Creates an aggregate value, like a tuple, a struct or an enum:
536    /// ```text
537    /// l = List::Cons { value:x, tail:tl };
538    /// ```
539    /// Note that in some MIR passes (like optimized MIR), aggregate values are
540    /// decomposed, like below:
541    /// ```text
542    /// (l as List::Cons).value = x;
543    /// (l as List::Cons).tail = tl;
544    /// ```
545    /// Because we may want to plug our translation mechanism at various
546    /// places, we need to take both into accounts in the translation and in
547    /// our semantics. Aggregate value initialization is easy, you might want
548    /// to have a look at expansion of `Bottom` values for explanations about the
549    /// other case.
550    ///
551    /// Remark: in case of closures, the aggregated value groups the closure id
552    /// together with its state.
553    Aggregate(AggregateKind, Vec<Operand>),
554    /// Copy the value of the referenced global.
555    /// Not present in MIR; introduced in [simplify_constants.rs].
556    Global(GlobalDeclRef),
557    /// Reference the value of the global. This has type `&T` or `*mut T` depending on desired
558    /// mutability.
559    /// Not present in MIR; introduced in [simplify_constants.rs].
560    GlobalRef(GlobalDeclRef, RefKind),
561    /// Length of a memory location. The run-time length of e.g. a vector or a slice is
562    /// represented differently (but pretty-prints the same, FIXME).
563    /// Should be seen as a function of signature:
564    /// - `fn<T;N>(&[T;N]) -> usize`
565    /// - `fn<T>(&[T]) -> usize`
566    ///
567    /// We store the type argument and the const generic (the latter only for arrays).
568    ///
569    /// [Len] is automatically introduced by rustc, notably for the bound checks:
570    /// we eliminate it together with the bounds checks whenever possible.
571    /// There are however occurrences that we don't eliminate (yet).
572    /// For instance, for the following Rust code:
573    /// ```text
574    /// fn slice_pattern_4(x: &[()]) {
575    ///     match x {
576    ///         [_named] => (),
577    ///         _ => (),
578    ///     }
579    /// }
580    /// ```
581    /// rustc introduces a check that the length of the slice is exactly equal
582    /// to 1 and that we preserve.
583    Len(Place, Ty, Option<ConstGeneric>),
584    /// [Repeat(x, n)] creates an array where [x] is copied [n] times.
585    ///
586    /// We translate this to a function call.
587    #[charon::opaque]
588    Repeat(Operand, Ty, ConstGeneric),
589    /// Transmutes a `*mut u8` (obtained from `malloc`) into shallow-initialized `Box<T>`. This
590    /// only appears as part of lowering `Box::new()` in some cases. We reconstruct the original
591    /// `Box::new()` call.
592    #[charon::opaque]
593    ShallowInitBox(Operand, Ty),
594}
595
596/// An aggregated ADT.
597///
598/// Note that ADTs are desaggregated at some point in MIR. For instance, if
599/// we have in Rust:
600/// ```ignore
601///   let ls = Cons(hd, tl);
602/// ```
603///
604/// In MIR we have (yes, the discriminant update happens *at the end* for some
605/// reason):
606/// ```text
607///   (ls as Cons).0 = move hd;
608///   (ls as Cons).1 = move tl;
609///   discriminant(ls) = 0; // assuming `Cons` is the variant of index 0
610/// ```
611///
612/// Rem.: in the Aeneas semantics, both cases are handled (in case of desaggregated
613/// initialization, `ls` is initialized to `⊥`, then this `⊥` is expanded to
614/// `Cons (⊥, ⊥)` upon the first assignment, at which point we can initialize
615/// the field 0, etc.).
616#[derive(Debug, Clone, VariantIndexArity, Serialize, Deserialize, Drive, DriveMut)]
617#[charon::variants_prefix("Aggregated")]
618pub enum AggregateKind {
619    /// A struct, enum or union aggregate. The `VariantId`, if present, indicates this is an enum
620    /// and the aggregate uses that variant. The `FieldId`, if present, indicates this is a union
621    /// and the aggregate writes into that field. Otherwise this is a struct.
622    Adt(TypeId, Option<VariantId>, Option<FieldId>, BoxedArgs),
623    /// We don't put this with the ADT cas because this is the only built-in type
624    /// with aggregates, and it is a primitive type. In particular, it makes
625    /// sense to treat it differently because it has a variable number of fields.
626    Array(Ty, ConstGeneric),
627    /// Aggregated values for closures group the function id together with its
628    /// state.
629    Closure(FunDeclId, BoxedArgs),
630    /// Construct a raw pointer from a pointer value, and its metadata (can be unit, if building
631    /// a thin pointer). The type is the type of the pointee.
632    /// We lower this to a builtin function call in [crate::ops_to_function_calls].
633    #[charon::opaque]
634    RawPtr(Ty, RefKind),
635}
charon_lib/ast/expressions.rs

charon_lib/ast/
expressions.rs
