charon_lib/ast/
expressions.rs

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
//! Implements expressions: paths, operands, rvalues, lvalues

use crate::ast::*;
use derive_visitor::{Drive, DriveMut};
use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName};
use serde::{Deserialize, Serialize};
use std::vec::Vec;

#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct Place {
    pub kind: PlaceKind,
    pub ty: Ty,
}

#[derive(
    Debug,
    PartialEq,
    Eq,
    Clone,
    EnumIsA,
    EnumAsGetters,
    EnumToGetters,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
)]
#[charon::variants_prefix("Place")]
pub enum PlaceKind {
    Base(VarId),
    Projection(Box<Place>, ProjectionElem),
}

/// Note that we don't have the equivalent of "downcasts".
/// Downcasts are actually necessary, for instance when initializing enumeration
/// values: the value is initially `Bottom`, and we need a way of knowing the
/// variant.
/// For example:
/// `((_0 as Right).0: T2) = move _1;`
/// In MIR, downcasts always happen before field projections: in our internal
/// language, we thus merge downcasts and field projections.
#[derive(
    Debug,
    PartialEq,
    Eq,
    Clone,
    EnumIsA,
    EnumAsGetters,
    EnumToGetters,
    VariantName,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
)]
pub enum ProjectionElem {
    /// Dereference a shared/mutable reference, a box, or a raw pointer.
    Deref,
    /// Projection from ADTs (variants, structures).
    /// We allow projections to be used as left-values and right-values.
    /// We should never have projections to fields of symbolic variants (they
    /// should have been expanded before through a match).
    Field(FieldProjKind, FieldId),
    /// MIR imposes that the argument to an index projection be a local variable, meaning
    /// that even constant indices into arrays are let-bound as separate variables.
    /// We **eliminate** this variant in a micro-pass.
    #[charon::opaque]
    Index {
        offset: Box<Operand>,
        from_end: bool,
    },
    /// Take a subslice of a slice or array. If `from_end` is `true` this is
    /// `slice[from..slice.len() - to]`, otherwise this is `slice[from..to]`.
    /// We **eliminate** this variant in a micro-pass.
    #[charon::opaque]
    Subslice {
        from: Box<Operand>,
        to: Box<Operand>,
        from_end: bool,
    },
}

#[derive(
    Debug,
    PartialEq,
    Eq,
    Copy,
    Clone,
    EnumIsA,
    EnumAsGetters,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
)]
#[charon::variants_prefix("Proj")]
pub enum FieldProjKind {
    Adt(TypeDeclId, Option<VariantId>),
    /// If we project from a tuple, the projection kind gives the arity of the tuple.
    Tuple(usize),
    /// Access to a field in a closure state.
    /// We eliminate this in a micro-pass ([crate::update_closure_signatures]).
    #[charon::opaque]
    ClosureState,
}

#[derive(
    Debug,
    PartialEq,
    Eq,
    Copy,
    Clone,
    EnumIsA,
    EnumAsGetters,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
)]
#[charon::variants_prefix("B")]
pub enum BorrowKind {
    Shared,
    Mut,
    /// See <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.MutBorrowKind.html#variant.TwoPhaseBorrow>
    /// and <https://rustc-dev-guide.rust-lang.org/borrow_check/two_phase_borrows.html>
    TwoPhaseMut,
    /// Those are typically introduced when using guards in matches, to make sure guards don't
    /// change the variant of an enum value while me match over it.
    ///
    /// See <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.FakeBorrowKind.html#variant.Shallow>.
    Shallow,
    /// Data must be immutable but not aliasable. In other words you can't mutate the data but you
    /// can mutate *through it*, e.g. if it points to a `&mut T`. This is only used in closure
    /// captures, e.g.
    /// ```rust,ignore
    /// let mut z = 3;
    /// let x: &mut isize = &mut z;
    /// let y = || *x += 5;
    /// ```
    /// Here the captured variable can't be `&mut &mut x` since the `x` binding is not mutable, yet
    /// we must be able to mutate what it points to.
    ///
    /// See <https://doc.rust-lang.org/beta/nightly-rustc/rustc_middle/mir/enum.MutBorrowKind.html#variant.ClosureCapture>.
    UniqueImmutable,
}

/// Unary operation
#[derive(
    Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
)]
#[charon::rename("Unop")]
pub enum UnOp {
    Not,
    /// This can overflow. In practice, rust introduces an assert before
    /// (in debug mode) to check that it is not equal to the minimum integer
    /// value (for the proper type).
    Neg,
    /// Casts are rvalues in MIR, but we treat them as unops.
    Cast(CastKind),
    /// Coercion from array (i.e., [T; N]) to slice.
    ///
    /// **Remark:** We introduce this unop when translating from MIR, **then transform**
    /// it to a function call in a micro pass. The type and the scalar value are not
    /// *necessary* as we can retrieve them from the context, but storing them here is
    /// very useful. The [RefKind] argument states whethere we operate on a mutable
    /// or a shared borrow to an array.
    #[charon::opaque]
    ArrayToSlice(RefKind, Ty, ConstGeneric),
}

/// Nullary operation
#[derive(
    Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
)]
#[charon::rename("Nullop")]
pub enum NullOp {
    SizeOf,
    AlignOf,
    OffsetOf(Vec<(usize, FieldId)>),
    UbChecks,
}

/// For all the variants: the first type gives the source type, the second one gives
/// the destination type.
#[derive(
    Debug, PartialEq, Eq, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
)]
#[charon::variants_prefix("Cast")]
pub enum CastKind {
    /// Conversion between types in {Integer, Bool}
    /// Remark: for now we don't support conversions with Char.
    Scalar(LiteralTy, LiteralTy),
    RawPtr(Ty, Ty),
    FnPtr(Ty, Ty),
    /// [Unsize coercion](https://doc.rust-lang.org/std/ops/trait.CoerceUnsized.html). This is
    /// either `[T; N]` -> `[T]` or `T: Trait` -> `dyn Trait` coercions, behind a pointer
    /// (reference, `Box`, or other type that implements `CoerceUnsized`).
    ///
    /// The special case of `&[T; N]` -> `&[T]` coercion is caught by `UnOp::ArrayToSlice`.
    Unsize(Ty, Ty),
    /// Reinterprets the bits of a value of one type as another type, i.e. exactly what
    /// [`std::mem::transmute`] does.
    Transmute(Ty, Ty),
}

/// Binary operations.
#[derive(
    Debug, PartialEq, Eq, Copy, Clone, EnumIsA, VariantName, Serialize, Deserialize, Drive, DriveMut,
)]
#[charon::rename("Binop")]
pub enum BinOp {
    BitXor,
    BitAnd,
    BitOr,
    Eq,
    Lt,
    Le,
    Ne,
    Ge,
    Gt,
    /// Fails if the divisor is 0, or if the operation is `int::MIN / -1`.
    Div,
    /// Fails if the divisor is 0, or if the operation is `int::MIN % -1`.
    Rem,
    /// Fails on overflow.
    Add,
    /// Fails on overflow.
    Sub,
    /// Fails on overflow.
    Mul,
    /// Returns `(result, did_overflow)`, where `result` is the result of the operation with
    /// wrapping semantics, and `did_overflow` is a boolean that indicates whether the operation
    /// overflowed. This operation does not fail.
    CheckedAdd,
    /// Like `CheckedAdd`.
    CheckedSub,
    /// Like `CheckedAdd`.
    CheckedMul,
    /// Fails if the shift is bigger than the bit-size of the type.
    Shl,
    /// Fails if the shift is bigger than the bit-size of the type.
    Shr,
    // No Offset binary operation: this is an operation on raw pointers
}

#[derive(
    Debug,
    PartialEq,
    Eq,
    Clone,
    EnumIsA,
    EnumToGetters,
    EnumAsGetters,
    VariantName,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
)]
pub enum Operand {
    Copy(Place),
    Move(Place),
    /// Constant value (including constant and static variables)
    #[charon::rename("Constant")]
    Const(ConstantExpr),
}

/// A function identifier. See [crate::ullbc_ast::Terminator]
#[derive(
    Debug,
    Clone,
    PartialEq,
    Eq,
    EnumIsA,
    EnumAsGetters,
    VariantName,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
)]
#[charon::variants_prefix("F")]
pub enum FunId {
    /// A "regular" function (function local to the crate, external function
    /// not treated as a primitive one).
    Regular(FunDeclId),
    /// A primitive function, coming from a standard library (for instance:
    /// `alloc::boxed::Box::new`).
    /// TODO: rename to "Primitive"
    #[charon::rename("FBuiltin")]
    Builtin(BuiltinFunId),
}

/// An built-in function identifier, identifying a function coming from a
/// standard library.
#[derive(
    Debug,
    Clone,
    Copy,
    PartialEq,
    Eq,
    EnumIsA,
    EnumAsGetters,
    VariantName,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
)]
pub enum BuiltinFunId {
    /// `alloc::boxed::Box::new`
    BoxNew,
    /// Cast an array as a slice.
    ///
    /// Converted from [UnOp::ArrayToSlice]
    ArrayToSliceShared,
    /// Cast an array as a slice.
    ///
    /// Converted from [UnOp::ArrayToSlice]
    ArrayToSliceMut,
    /// `repeat(n, x)` returns an array where `x` has been replicated `n` times.
    ///
    /// We introduce this when desugaring the [ArrayRepeat] rvalue.
    ArrayRepeat,
    /// Converted from indexing `ProjectionElem`s. The signature depends on the parameters. It
    /// could look like:
    /// - `fn ArrayIndexShared<T,N>(&[T;N], usize) -> &T`
    /// - `fn SliceIndexShared<T>(&[T], usize) -> &T`
    /// - `fn ArraySubSliceShared<T,N>(&[T;N], usize, usize) -> &[T]`
    /// - `fn SliceSubSliceMut<T>(&mut [T], usize, usize) -> &mut [T]`
    /// - etc
    Index(BuiltinIndexOp),
}

/// One of 8 built-in indexing operations.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize, Drive, DriveMut)]
pub struct BuiltinIndexOp {
    /// Whether this is a slice or array.
    pub is_array: bool,
    /// Whether we're indexing mutably or not. Determines the type ofreference of the input and
    /// output.
    pub mutability: RefKind,
    /// Whether we're indexing a single element or a subrange. If `true`, the function takes
    /// two indices and the output is a slice; otherwise, the function take one index and the
    /// output is a reference to a single element.
    pub is_range: bool,
}

#[derive(Debug, Clone, PartialEq, Eq, EnumAsGetters, Serialize, Deserialize, Drive, DriveMut)]
pub enum FunIdOrTraitMethodRef {
    #[charon::rename("FunId")]
    Fun(FunId),
    /// If a trait: the reference to the trait and the id of the trait method.
    /// The fun decl id is not really necessary - we put it here for convenience
    /// purposes.
    #[charon::rename("TraitMethod")]
    Trait(TraitRef, TraitItemName, FunDeclId),
}

#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct FnPtr {
    pub func: FunIdOrTraitMethodRef,
    pub generics: GenericArgs,
}

/// A constant expression.
///
/// Only the [Literal] and [Var] cases are left in the final LLBC.
///
/// The other cases come from a straight translation from the MIR:
///
/// [Adt] case:
/// It is a bit annoying, but rustc treats some ADT and tuple instances as
/// constants when generating MIR:
/// - an enumeration with one variant and no fields is a constant.
/// - a structure with no field is a constant.
/// - sometimes, Rust stores the initialization of an ADT as a constant
///   (if all the fields are constant) rather than as an aggregated value
/// We later desugar those to regular ADTs, see [regularize_constant_adts.rs].
///
/// [Global] case: access to a global variable. We later desugar it to
/// a separate statement.
///
/// [Ref] case: reference to a constant value. We later desugar it to a separate
/// statement.
///
/// [FnPtr] case: a function pointer (to a top-level function).
///
/// Remark:
/// MIR seems to forbid more complex expressions like paths. For instance,
/// reading the constant `a.b` is translated to `{ _1 = const a; _2 = (_1.0) }`.
#[derive(
    Debug,
    PartialEq,
    Eq,
    Clone,
    VariantName,
    EnumIsA,
    EnumAsGetters,
    Serialize,
    Deserialize,
    Drive,
    DriveMut,
)]
#[charon::variants_prefix("C")]
pub enum RawConstantExpr {
    Literal(Literal),
    ///
    /// In most situations:
    /// Enumeration with one variant with no fields, structure with
    /// no fields, unit (encoded as a 0-tuple).
    ///
    /// Less frequently: arbitrary ADT values.
    ///
    /// We eliminate this case in a micro-pass.
    #[charon::opaque]
    Adt(Option<VariantId>, Vec<ConstantExpr>),
    /// The value is a top-level constant/static.
    ///
    /// We eliminate this case in a micro-pass.
    ///
    /// Remark: constants can actually have generic parameters.
    /// ```text
    /// struct V<const N: usize, T> {
    ///   x: [T; N],
    /// }
    ///
    /// impl<const N: usize, T> V<N, T> {
    ///   const LEN: usize = N; // This has generics <N, T>
    /// }
    ///
    /// fn use_v<const N: usize, T>(v: V<N, T>) {
    ///   let l = V::<N, T>::LEN; // We need to provided a substitution here
    /// }
    /// ```
    #[charon::opaque]
    Global(GlobalDeclRef),
    ///
    /// A trait constant.
    ///
    /// Ex.:
    /// ```text
    /// impl Foo for Bar {
    ///   const C : usize = 32; // <-
    /// }
    /// ```
    ///
    /// Remark: trait constants can not be used in types, they are necessarily
    /// values.
    TraitConst(TraitRef, TraitItemName),
    /// A shared reference to a constant value.
    ///
    /// We eliminate this case in a micro-pass.
    #[charon::opaque]
    Ref(Box<ConstantExpr>),
    /// A mutable pointer to a mutable static.
    ///
    /// We eliminate this case in a micro-pass.
    #[charon::opaque]
    MutPtr(Box<ConstantExpr>),
    /// A const generic var
    Var(ConstGenericVarId),
    /// Function pointer
    FnPtr(FnPtr),
}

#[derive(Debug, PartialEq, Eq, Clone, Serialize, Deserialize, Drive, DriveMut)]
pub struct ConstantExpr {
    pub value: RawConstantExpr,
    pub ty: Ty,
}

/// TODO: we could factor out [Rvalue] and function calls (for LLBC, not ULLBC).
/// We can also factor out the unops, binops with the function calls.
/// TODO: move the aggregate kind to operands
/// TODO: we should prefix the type variants with "R" or "Rv", this would avoid collisions
#[derive(
    Debug, Clone, EnumToGetters, EnumAsGetters, EnumIsA, Serialize, Deserialize, Drive, DriveMut,
)]
pub enum Rvalue {
    /// Lifts an operand as an rvalue.
    Use(Operand),
    /// Takes a reference to the given place.
    #[charon::rename("RvRef")]
    Ref(Place, BorrowKind),
    /// Takes a raw pointer with the given mutability to the given place. This is generated by
    /// pointer casts like `&v as *const _` or raw borrow expressions like `&raw const v.`
    RawPtr(Place, RefKind),
    /// Binary operations (note that we merge "checked" and "unchecked" binops)
    BinaryOp(BinOp, Operand, Operand),
    /// Unary operation (e.g. not, neg)
    UnaryOp(UnOp, Operand),
    /// Nullary operation (e.g. `size_of`)
    NullaryOp(NullOp, Ty),
    /// Discriminant (for enumerations).
    /// Note that discriminant values have type isize. We also store the identifier
    /// of the type from which we read the discriminant.
    ///
    /// This case is filtered in [crate::remove_read_discriminant]
    Discriminant(Place, TypeDeclId),
    /// Creates an aggregate value, like a tuple, a struct or an enum:
    /// ```text
    /// l = List::Cons { value:x, tail:tl };
    /// ```
    /// Note that in some MIR passes (like optimized MIR), aggregate values are
    /// decomposed, like below:
    /// ```text
    /// (l as List::Cons).value = x;
    /// (l as List::Cons).tail = tl;
    /// ```
    /// Because we may want to plug our translation mechanism at various
    /// places, we need to take both into accounts in the translation and in
    /// our semantics. Aggregate value initialization is easy, you might want
    /// to have a look at expansion of `Bottom` values for explanations about the
    /// other case.
    ///
    /// Remark: in case of closures, the aggregated value groups the closure id
    /// together with its state.
    Aggregate(AggregateKind, Vec<Operand>),
    /// Copy the value of the referenced global.
    /// Not present in MIR; introduced in [simplify_constants.rs].
    Global(GlobalDeclRef),
    /// Reference the value of the global. This has type `&T` or `*mut T` depending on desired
    /// mutability.
    /// Not present in MIR; introduced in [simplify_constants.rs].
    GlobalRef(GlobalDeclRef, RefKind),
    /// Length of a memory location. The run-time length of e.g. a vector or a slice is
    /// represented differently (but pretty-prints the same, FIXME).
    /// Should be seen as a function of signature:
    /// - `fn<T;N>(&[T;N]) -> usize`
    /// - `fn<T>(&[T]) -> usize`
    ///
    /// We store the type argument and the const generic (the latter only for arrays).
    ///
    /// [Len] is automatically introduced by rustc, notably for the bound checks:
    /// we eliminate it together with the bounds checks whenever possible.
    /// There are however occurrences that we don't eliminate (yet).
    /// For instance, for the following Rust code:
    /// ```text
    /// fn slice_pattern_4(x: &[()]) {
    ///     match x {
    ///         [_named] => (),
    ///         _ => (),
    ///     }
    /// }
    /// ```
    /// rustc introduces a check that the length of the slice is exactly equal
    /// to 1 and that we preserve.
    Len(Place, Ty, Option<ConstGeneric>),
    /// [Repeat(x, n)] creates an array where [x] is copied [n] times.
    ///
    /// We translate this to a function call.
    #[charon::opaque]
    Repeat(Operand, Ty, ConstGeneric),
    /// Transmutes a `*mut u8` (obtained from `malloc`) into shallow-initialized `Box<T>`. This
    /// only appears as part of lowering `Box::new()` in some cases. We reconstruct the original
    /// `Box::new()` call.
    #[charon::opaque]
    ShallowInitBox(Operand, Ty),
}

/// An aggregated ADT.
///
/// Note that ADTs are desaggregated at some point in MIR. For instance, if
/// we have in Rust:
/// ```ignore
///   let ls = Cons(hd, tl);
/// ```
///
/// In MIR we have (yes, the discriminant update happens *at the end* for some
/// reason):
/// ```text
///   (ls as Cons).0 = move hd;
///   (ls as Cons).1 = move tl;
///   discriminant(ls) = 0; // assuming `Cons` is the variant of index 0
/// ```
///
/// Rem.: in the Aeneas semantics, both cases are handled (in case of desaggregated
/// initialization, `ls` is initialized to `⊥`, then this `⊥` is expanded to
/// `Cons (⊥, ⊥)` upon the first assignment, at which point we can initialize
/// the field 0, etc.).
#[derive(Debug, Clone, VariantIndexArity, Serialize, Deserialize, Drive, DriveMut)]
#[charon::variants_prefix("Aggregated")]
pub enum AggregateKind {
    /// A struct, enum or union aggregate. The `VariantId`, if present, indicates this is an enum
    /// and the aggregate uses that variant. The `FieldId`, if present, indicates this is a union
    /// and the aggregate writes into that field. Otherwise this is a struct.
    Adt(TypeId, Option<VariantId>, Option<FieldId>, GenericArgs),
    /// We don't put this with the ADT cas because this is the only built-in type
    /// with aggregates, and it is a primitive type. In particular, it makes
    /// sense to treat it differently because it has a variable number of fields.
    Array(Ty, ConstGeneric),
    /// Aggregated values for closures group the function id together with its
    /// state.
    Closure(FunDeclId, GenericArgs),
}