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
|
(** The following module defines micro-passes which operate on the pure AST *)
open Errors
open Pure
(** This function computes pretty names for the variables in the pure AST. It
relies on the "meta"-place information in the AST to generate naming
constraints.
The way it works is as follows:
- we only modify the names of the unnamed variables
- whenever we see an rvalue/lvalue which is exactly an unnamed variable,
and this value is linked to some meta-place information which contains
a name and an empty path, we consider we should use this name
For instance, the following situations happen:
- let's say we evaluate:
```
match (ls : List<T>) {
List::Cons(x, hd) => {
...
}
}
```
Actually, in MIR, we get:
```
tmp := discriminant(ls);
switch tmp {
0 => {
x := (ls as Cons).0;
hd := (ls as Cons).1;
...
}
}
```
If `ls` maps to a symbolic value `s0` upon evaluating the match in symbolic
mode, we expand this value upon evaluating `tmp = discriminant(ls)`.
However, at this point, we don't know which should be the names of
the symbolic values we introduce for the fields of `Cons`!
Let's imagine we have (for the `Cons` branch): `s0 ~~> Cons s1 s2`.
The assigments lead to the following binding in the evaluation context:
```
x -> s1
hd -> s2
```
When generating the symbolic AST, we save as meta-information that we
assign `s1` to the place `x` and `s2` to the place `hd`. This way,
we learn we can use the names `x` and `hd` for the variables which are
introduced by the match:
```
match ls with
| Cons x hd -> ...
| ...
```
- If we write the following in Rust:
```
let x = y + z;
```
We get the following MIR:
```
let tmp = y + z;
```
TODO: finish...
- If we write the following in Rust:
```
let px = &mut x;
f(px);
```
Rustc generates the following MIR:
```
px := &mut x;
tmp := &mut ( *px ); // "tmp" is actually an anonymous variable
f(move tmp);
```
As borrows and dereferencements are ignored in the pure paths we generate
(because they are extracted to the identity), we save as meta-data that
at some point we assign the value of `px` to `tmp`.
TODO: actually useless, because `tmp` later gets inlined.
- TODO: inputs and end abstraction...
*)
let compute_pretty_names () = ()
(** Remove the meta-information *)
let remove_meta (e : expression) : expression =
let obj =
object
inherit [_] map_expression as super
method! visit_Meta env meta e = super#visit_expression env e
end
in
obj#visit_expression () e
|
