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 Add,
233 /// Fails on overflow.
234 Sub,
235 /// Fails on overflow.
236 Mul,
237 /// Returns `(result, did_overflow)`, where `result` is the result of the operation with
238 /// wrapping semantics, and `did_overflow` is a boolean that indicates whether the operation
239 /// overflowed. This operation does not fail.
240 CheckedAdd,
241 /// Like `CheckedAdd`.
242 CheckedSub,
243 /// Like `CheckedAdd`.
244 CheckedMul,
245 /// Fails if the shift is bigger than the bit-size of the type.
246 Shl,
247 /// Fails if the shift is bigger than the bit-size of the type.
248 Shr,
249 /// `BinOp(Offset, ptr, n)` for `ptr` a pointer to type `T` offsets `ptr` by `n * size_of::<T>()`.
250 Offset,
251 /// `BinOp(Cmp, a, b)` returns `-1u8` if `a < b`, `0u8` if `a == b`, and `1u8` if `a > b`.
252 Cmp,
253}
254
255#[derive(
256 Debug,
257 PartialEq,
258 Eq,
259 Clone,
260 EnumIsA,
261 EnumToGetters,
262 EnumAsGetters,
263 VariantName,
264 Serialize,
265 Deserialize,
266 Drive,
267 DriveMut,
268)]
269pub enum Operand {
270 Copy(Place),
271 Move(Place),
272 /// Constant value (including constant and static variables)
273 #[charon::rename("Constant")]
274 Const(ConstantExpr),
275}
276
277/// A function identifier. See [crate::ullbc_ast::Terminator]
278#[derive(
279 Debug,
280 Clone,
281 PartialEq,
282 Eq,
283 EnumIsA,
284 EnumAsGetters,
285 VariantName,
286 Serialize,
287 Deserialize,
288 Drive,
289 DriveMut,
290)]
291#[charon::variants_prefix("F")]
292pub enum FunId {
293 /// A "regular" function (function local to the crate, external function
294 /// not treated as a primitive one).
295 Regular(FunDeclId),
296 /// A primitive function, coming from a standard library (for instance:
297 /// `alloc::boxed::Box::new`).
298 /// TODO: rename to "Primitive"
299 #[charon::rename("FBuiltin")]
300 Builtin(BuiltinFunId),
301}
302
303/// An built-in function identifier, identifying a function coming from a
304/// standard library.
305#[derive(
306 Debug,
307 Clone,
308 Copy,
309 PartialEq,
310 Eq,
311 EnumIsA,
312 EnumAsGetters,
313 VariantName,
314 Serialize,
315 Deserialize,
316 Drive,
317 DriveMut,
318)]
319pub enum BuiltinFunId {
320 /// `alloc::boxed::Box::new`
321 BoxNew,
322 /// Cast an array as a slice.
323 ///
324 /// Converted from [UnOp::ArrayToSlice]
325 ArrayToSliceShared,
326 /// Cast an array as a slice.
327 ///
328 /// Converted from [UnOp::ArrayToSlice]
329 ArrayToSliceMut,
330 /// `repeat(n, x)` returns an array where `x` has been replicated `n` times.
331 ///
332 /// We introduce this when desugaring the [ArrayRepeat] rvalue.
333 ArrayRepeat,
334 /// Converted from indexing `ProjectionElem`s. The signature depends on the parameters. It
335 /// could look like:
336 /// - `fn ArrayIndexShared<T,N>(&[T;N], usize) -> &T`
337 /// - `fn SliceIndexShared<T>(&[T], usize) -> &T`
338 /// - `fn ArraySubSliceShared<T,N>(&[T;N], usize, usize) -> &[T]`
339 /// - `fn SliceSubSliceMut<T>(&mut [T], usize, usize) -> &mut [T]`
340 /// - etc
341 Index(BuiltinIndexOp),
342 /// Build a raw pointer, from a data pointer and metadata. The metadata can be unit, if
343 /// building a thin pointer.
344 ///
345 /// Converted from [AggregateKind::RawPtr]
346 PtrFromParts(RefKind),
347}
348
349/// One of 8 built-in indexing operations.
350#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
351pub struct BuiltinIndexOp {
352 /// Whether this is a slice or array.
353 #[drive(skip)]
354 pub is_array: bool,
355 /// Whether we're indexing mutably or not. Determines the type ofreference of the input and
356 /// output.
357 pub mutability: RefKind,
358 /// Whether we're indexing a single element or a subrange. If `true`, the function takes
359 /// two indices and the output is a slice; otherwise, the function take one index and the
360 /// output is a reference to a single element.
361 #[drive(skip)]
362 pub is_range: bool,
363}
364
365#[derive(Debug, Clone, PartialEq, Eq, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut)]
366pub enum FunIdOrTraitMethodRef {
367 #[charon::rename("FunId")]
368 Fun(FunId),
369 /// If a trait: the reference to the trait and the id of the trait method.
370 /// The fun decl id is not really necessary - we put it here for convenience
371 /// purposes.
372 #[charon::rename("TraitMethod")]
373 Trait(TraitRef, TraitItemName, FunDeclId),
374}
375
376#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
377pub struct FnPtr {
378 pub func: FunIdOrTraitMethodRef,
379 pub generics: GenericArgs,
380}
381
382/// A constant expression.
383///
384/// Only the [Literal] and [Var] cases are left in the final LLBC.
385///
386/// The other cases come from a straight translation from the MIR:
387///
388/// [Adt] case:
389/// It is a bit annoying, but rustc treats some ADT and tuple instances as
390/// constants when generating MIR:
391/// - an enumeration with one variant and no fields is a constant.
392/// - a structure with no field is a constant.
393/// - sometimes, Rust stores the initialization of an ADT as a constant
394/// (if all the fields are constant) rather than as an aggregated value
395/// We later desugar those to regular ADTs, see [regularize_constant_adts.rs].
396///
397/// [Global] case: access to a global variable. We later desugar it to
398/// a separate statement.
399///
400/// [Ref] case: reference to a constant value. We later desugar it to a separate
401/// statement.
402///
403/// [FnPtr] case: a function pointer (to a top-level function).
404///
405/// Remark:
406/// MIR seems to forbid more complex expressions like paths. For instance,
407/// reading the constant `a.b` is translated to `{ _1 = const a; _2 = (_1.0) }`.
408#[derive(
409 Debug,
410 PartialEq,
411 Eq,
412 Clone,
413 VariantName,
414 EnumIsA,
415 EnumAsGetters,
416 Serialize,
417 Deserialize,
418 Drive,
419 DriveMut,
420)]
421#[charon::variants_prefix("C")]
422pub enum RawConstantExpr {
423 Literal(Literal),
424 ///
425 /// In most situations:
426 /// Enumeration with one variant with no fields, structure with
427 /// no fields, unit (encoded as a 0-tuple).
428 ///
429 /// Less frequently: arbitrary ADT values.
430 ///
431 /// We eliminate this case in a micro-pass.
432 #[charon::opaque]
433 Adt(Option<VariantId>, Vec<ConstantExpr>),
434 #[charon::opaque]
435 Array(Vec<ConstantExpr>),
436 /// The value is a top-level constant/static.
437 ///
438 /// We eliminate this case in a micro-pass.
439 ///
440 /// Remark: constants can actually have generic parameters.
441 /// ```text
442 /// struct V<const N: usize, T> {
443 /// x: [T; N],
444 /// }
445 ///
446 /// impl<const N: usize, T> V<N, T> {
447 /// const LEN: usize = N; // This has generics <N, T>
448 /// }
449 ///
450 /// fn use_v<const N: usize, T>(v: V<N, T>) {
451 /// let l = V::<N, T>::LEN; // We need to provided a substitution here
452 /// }
453 /// ```
454 #[charon::opaque]
455 Global(GlobalDeclRef),
456 ///
457 /// A trait constant.
458 ///
459 /// Ex.:
460 /// ```text
461 /// impl Foo for Bar {
462 /// const C : usize = 32; // <-
463 /// }
464 /// ```
465 ///
466 /// Remark: trait constants can not be used in types, they are necessarily
467 /// values.
468 TraitConst(TraitRef, TraitItemName),
469 /// A shared reference to a constant value.
470 ///
471 /// We eliminate this case in a micro-pass.
472 #[charon::opaque]
473 Ref(Box<ConstantExpr>),
474 /// A mutable pointer to a mutable static.
475 ///
476 /// We eliminate this case in a micro-pass.
477 #[charon::opaque]
478 MutPtr(Box<ConstantExpr>),
479 /// A const generic var
480 Var(ConstGenericDbVar),
481 /// Function pointer
482 FnPtr(FnPtr),
483 /// Raw memory value obtained from constant evaluation. Used when a more structured
484 /// representation isn't possible (e.g. for unions) or just isn't implemented yet.
485 #[drive(skip)]
486 RawMemory(Vec<u8>),
487 /// A constant expression that Charon still doesn't handle, along with the reason why.
488 #[drive(skip)]
489 Opaque(String),
490}
491
492#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
493pub struct ConstantExpr {
494 pub value: RawConstantExpr,
495 pub ty: Ty,
496}
497
498/// TODO: we could factor out [Rvalue] and function calls (for LLBC, not ULLBC).
499/// We can also factor out the unops, binops with the function calls.
500/// TODO: move the aggregate kind to operands
501/// TODO: we should prefix the type variants with "R" or "Rv", this would avoid collisions
502#[derive(
503 Debug, Clone, EnumToGetters, EnumAsGetters, EnumIsA, Serialize, Deserialize, Drive, DriveMut,
504)]
505pub enum Rvalue {
506 /// Lifts an operand as an rvalue.
507 Use(Operand),
508 /// Takes a reference to the given place.
509 #[charon::rename("RvRef")]
510 Ref(Place, BorrowKind),
511 /// Takes a raw pointer with the given mutability to the given place. This is generated by
512 /// pointer casts like `&v as *const _` or raw borrow expressions like `&raw const v.`
513 RawPtr(Place, RefKind),
514 /// Binary operations (note that we merge "checked" and "unchecked" binops)
515 BinaryOp(BinOp, Operand, Operand),
516 /// Unary operation (e.g. not, neg)
517 UnaryOp(UnOp, Operand),
518 /// Nullary operation (e.g. `size_of`)
519 NullaryOp(NullOp, Ty),
520 /// Discriminant (for enumerations).
521 /// Note that discriminant values have type isize. We also store the identifier
522 /// of the type from which we read the discriminant.
523 ///
524 /// This case is filtered in [crate::remove_read_discriminant]
525 Discriminant(Place, TypeDeclId),
526 /// Creates an aggregate value, like a tuple, a struct or an enum:
527 /// ```text
528 /// l = List::Cons { value:x, tail:tl };
529 /// ```
530 /// Note that in some MIR passes (like optimized MIR), aggregate values are
531 /// decomposed, like below:
532 /// ```text
533 /// (l as List::Cons).value = x;
534 /// (l as List::Cons).tail = tl;
535 /// ```
536 /// Because we may want to plug our translation mechanism at various
537 /// places, we need to take both into accounts in the translation and in
538 /// our semantics. Aggregate value initialization is easy, you might want
539 /// to have a look at expansion of `Bottom` values for explanations about the
540 /// other case.
541 ///
542 /// Remark: in case of closures, the aggregated value groups the closure id
543 /// together with its state.
544 Aggregate(AggregateKind, Vec<Operand>),
545 /// Copy the value of the referenced global.
546 /// Not present in MIR; introduced in [simplify_constants.rs].
547 Global(GlobalDeclRef),
548 /// Reference the value of the global. This has type `&T` or `*mut T` depending on desired
549 /// mutability.
550 /// Not present in MIR; introduced in [simplify_constants.rs].
551 GlobalRef(GlobalDeclRef, RefKind),
552 /// Length of a memory location. The run-time length of e.g. a vector or a slice is
553 /// represented differently (but pretty-prints the same, FIXME).
554 /// Should be seen as a function of signature:
555 /// - `fn<T;N>(&[T;N]) -> usize`
556 /// - `fn<T>(&[T]) -> usize`
557 ///
558 /// We store the type argument and the const generic (the latter only for arrays).
559 ///
560 /// [Len] is automatically introduced by rustc, notably for the bound checks:
561 /// we eliminate it together with the bounds checks whenever possible.
562 /// There are however occurrences that we don't eliminate (yet).
563 /// For instance, for the following Rust code:
564 /// ```text
565 /// fn slice_pattern_4(x: &[()]) {
566 /// match x {
567 /// [_named] => (),
568 /// _ => (),
569 /// }
570 /// }
571 /// ```
572 /// rustc introduces a check that the length of the slice is exactly equal
573 /// to 1 and that we preserve.
574 Len(Place, Ty, Option<ConstGeneric>),
575 /// [Repeat(x, n)] creates an array where [x] is copied [n] times.
576 ///
577 /// We translate this to a function call.
578 #[charon::opaque]
579 Repeat(Operand, Ty, ConstGeneric),
580 /// Transmutes a `*mut u8` (obtained from `malloc`) into shallow-initialized `Box<T>`. This
581 /// only appears as part of lowering `Box::new()` in some cases. We reconstruct the original
582 /// `Box::new()` call.
583 #[charon::opaque]
584 ShallowInitBox(Operand, Ty),
585}
586
587/// An aggregated ADT.
588///
589/// Note that ADTs are desaggregated at some point in MIR. For instance, if
590/// we have in Rust:
591/// ```ignore
592/// let ls = Cons(hd, tl);
593/// ```
594///
595/// In MIR we have (yes, the discriminant update happens *at the end* for some
596/// reason):
597/// ```text
598/// (ls as Cons).0 = move hd;
599/// (ls as Cons).1 = move tl;
600/// discriminant(ls) = 0; // assuming `Cons` is the variant of index 0
601/// ```
602///
603/// Rem.: in the Aeneas semantics, both cases are handled (in case of desaggregated
604/// initialization, `ls` is initialized to `⊥`, then this `⊥` is expanded to
605/// `Cons (⊥, ⊥)` upon the first assignment, at which point we can initialize
606/// the field 0, etc.).
607#[derive(Debug, Clone, VariantIndexArity, Serialize, Deserialize, Drive, DriveMut)]
608#[charon::variants_prefix("Aggregated")]
609pub enum AggregateKind {
610 /// A struct, enum or union aggregate. The `VariantId`, if present, indicates this is an enum
611 /// and the aggregate uses that variant. The `FieldId`, if present, indicates this is a union
612 /// and the aggregate writes into that field. Otherwise this is a struct.
613 Adt(TypeId, Option<VariantId>, Option<FieldId>, GenericArgs),
614 /// We don't put this with the ADT cas because this is the only built-in type
615 /// with aggregates, and it is a primitive type. In particular, it makes
616 /// sense to treat it differently because it has a variable number of fields.
617 Array(Ty, ConstGeneric),
618 /// Aggregated values for closures group the function id together with its
619 /// state.
620 Closure(FunDeclId, GenericArgs),
621 /// Construct a raw pointer from a pointer value, and its metadata (can be unit, if building
622 /// a thin pointer). The type is the type of the pointee.
623 /// We lower this to a builtin function call in [crate::ops_to_function_calls].
624 #[charon::opaque]
625 RawPtr(Ty, RefKind),
626}