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
|
open Types
open Values
type field_proj_kind =
| ProjAdt of TypeDeclId.id * VariantId.id option
| ProjOption of VariantId.id
(** Option is an assumed type, coming from the standard library *)
| ProjTuple of int
[@@deriving show]
(* arity of the tuple *)
type projection_elem =
| Deref
| DerefBox
| Field of field_proj_kind * FieldId.id
[@@deriving show]
type projection = projection_elem list [@@deriving show]
type place = { var_id : VarId.id; projection : projection } [@@deriving show]
type borrow_kind = Shared | Mut | TwoPhaseMut [@@deriving show]
type unop =
| Not
| Neg
| Cast of integer_type * integer_type
(** Cast an integer from a source type to a target type *)
[@@deriving show, ord]
(** A binary operation
Note that we merge checked binops and unchecked binops: we perform a
micro-pass on the MIR AST to remove the assertions introduced by rustc,
and later extract the binops which can fail (addition, substraction, etc.)
or have preconditions (division, remainder...) to monadic functions.
*)
type binop =
| BitXor
| BitAnd
| BitOr
| Eq
| Lt
| Le
| Ne
| Ge
| Gt
| Div
| Rem
| Add
| Sub
| Mul
| Shl
| Shr
[@@deriving show, ord]
let all_binops =
[
BitXor;
BitAnd;
BitOr;
Eq;
Lt;
Le;
Ne;
Ge;
Gt;
Div;
Rem;
Add;
Sub;
Mul;
Shl;
Shr;
]
type operand =
| Copy of place
| Move of place
| Constant of ety * constant_value
[@@deriving show]
(** An aggregated ADT.
Note that ADTs are desaggregated at some point in MIR. For instance, if
we have in Rust:
```
let ls = Cons(hd, tl);
```
In MIR we have (yes, the discriminant update happens *at the end* for some
reason):
```
(ls as Cons).0 = move hd;
(ls as Cons).1 = move tl;
discriminant(ls) = 0; // assuming `Cons` is the variant of index 0
```
Note that in our semantics, we handle both cases (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.).
*)
type aggregate_kind =
| AggregatedTuple
| AggregatedOption of VariantId.id * ety
(* TODO: AggregatedOption should be merged with AggregatedAdt *)
| AggregatedAdt of
TypeDeclId.id * VariantId.id option * erased_region list * ety list
[@@deriving show]
(* TODO: move the aggregate kind to operands *)
type rvalue =
| Use of operand
| Ref of place * borrow_kind
| UnaryOp of unop * operand
| BinaryOp of binop * operand * operand
| Discriminant of place
| Aggregate of aggregate_kind * operand list
[@@deriving show]
|
