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