@@ -43,22 +43,22 @@ it is safe with respect to the in-scope loans.
43
43
# Formal model
44
44
45
45
Throughout the docs we'll consider a simple subset of Rust in which
46
- you can only borrow from lvalues , defined like so:
46
+ you can only borrow from places , defined like so:
47
47
48
48
``` text
49
- LV = x | LV .f | *LV
49
+ P = x | P .f | *P
50
50
```
51
51
52
- Here ` x ` represents some variable, ` LV .f` is a field reference,
53
- and ` *LV ` is a pointer dereference. There is no auto-deref or other
52
+ Here ` x ` represents some variable, ` P .f` is a field reference,
53
+ and ` *P ` is a pointer dereference. There is no auto-deref or other
54
54
niceties. This means that if you have a type like:
55
55
56
56
``` rust
57
57
struct S { f : i32 }
58
58
```
59
59
60
60
and a variable ` a: Box<S> ` , then the rust expression ` a.f ` would correspond
61
- to an ` LV ` of ` (*a).f ` .
61
+ to an ` P ` of ` (*a).f ` .
62
62
63
63
Here is the formal grammar for the types we'll consider:
64
64
@@ -99,7 +99,7 @@ this sort of thing.
99
99
#### Loans and restrictions
100
100
101
101
The way the borrow checker works is that it analyzes each borrow
102
- expression (in our simple model, that's stuff like ` &LV ` , though in
102
+ expression (in our simple model, that's stuff like ` &P ` , though in
103
103
real life there are a few other cases to consider). For each borrow
104
104
expression, it computes a ` Loan ` , which is a data structure that
105
105
records (1) the value being borrowed, (2) the mutability and scope of
@@ -108,29 +108,29 @@ struct defined in `middle::borrowck`. Formally, we define `LOAN` as
108
108
follows:
109
109
110
110
``` text
111
- LOAN = (LV , LT, MQ, RESTRICTION*)
112
- RESTRICTION = (LV , ACTION*)
111
+ LOAN = (P , LT, MQ, RESTRICTION*)
112
+ RESTRICTION = (P , ACTION*)
113
113
ACTION = MUTATE | CLAIM | FREEZE
114
114
```
115
115
116
- Here the ` LOAN ` tuple defines the lvalue ` LV ` being borrowed; the
116
+ Here the ` LOAN ` tuple defines the place ` P ` being borrowed; the
117
117
lifetime ` LT ` of that borrow; the mutability ` MQ ` of the borrow; and a
118
118
list of restrictions. The restrictions indicate actions which, if
119
119
taken, could invalidate the loan and lead to type safety violations.
120
120
121
- Each ` RESTRICTION ` is a pair of a restrictive lvalue ` LV ` (which will
121
+ Each ` RESTRICTION ` is a pair of a restrictive place ` P ` (which will
122
122
either be the path that was borrowed or some prefix of the path that
123
123
was borrowed) and a set of restricted actions. There are three kinds
124
- of actions that may be restricted for the path ` LV ` :
124
+ of actions that may be restricted for the path ` P ` :
125
125
126
- - ` MUTATE ` means that ` LV ` cannot be assigned to;
127
- - ` CLAIM ` means that the ` LV ` cannot be borrowed mutably;
128
- - ` FREEZE ` means that the ` LV ` cannot be borrowed immutably;
126
+ - ` MUTATE ` means that ` P ` cannot be assigned to;
127
+ - ` CLAIM ` means that the ` P ` cannot be borrowed mutably;
128
+ - ` FREEZE ` means that the ` P ` cannot be borrowed immutably;
129
129
130
- Finally, it is never possible to move from an lvalue that appears in a
131
- restriction. This implies that the "empty restriction" ` (LV , []) ` ,
130
+ Finally, it is never possible to move from a place that appears in a
131
+ restriction. This implies that the "empty restriction" ` (P , []) ` ,
132
132
which contains an empty set of actions, still has a purpose---it
133
- prevents moves from ` LV ` . I chose not to make ` MOVE ` a fourth kind of
133
+ prevents moves from ` P ` . I chose not to make ` MOVE ` a fourth kind of
134
134
action because that would imply that sometimes moves are permitted
135
135
from restricted values, which is not the case.
136
136
@@ -239,22 +239,22 @@ live. (This is done via restrictions, read on.)
239
239
240
240
We start with the ` gather_loans ` pass, which walks the AST looking for
241
241
borrows. For each borrow, there are three bits of information: the
242
- lvalue ` LV ` being borrowed and the mutability ` MQ ` and lifetime ` LT `
242
+ place ` P ` being borrowed and the mutability ` MQ ` and lifetime ` LT `
243
243
of the resulting pointer. Given those, ` gather_loans ` applies four
244
244
validity tests:
245
245
246
- 1 . ` MUTABILITY(LV , MQ) ` : The mutability of the reference is
247
- compatible with the mutability of ` LV ` (i.e., not borrowing immutable
246
+ 1 . ` MUTABILITY(P , MQ) ` : The mutability of the reference is
247
+ compatible with the mutability of ` P ` (i.e., not borrowing immutable
248
248
data as mutable).
249
249
250
- 2 . ` ALIASABLE(LV , MQ) ` : The aliasability of the reference is
251
- compatible with the aliasability of ` LV ` . The goal is to prevent
250
+ 2 . ` ALIASABLE(P , MQ) ` : The aliasability of the reference is
251
+ compatible with the aliasability of ` P ` . The goal is to prevent
252
252
` &mut ` borrows of aliasability data.
253
253
254
- 3 . ` LIFETIME(LV , LT, MQ) ` : The lifetime of the borrow does not exceed
254
+ 3 . ` LIFETIME(P , LT, MQ) ` : The lifetime of the borrow does not exceed
255
255
the lifetime of the value being borrowed.
256
256
257
- 4 . ` RESTRICTIONS(LV , LT, ACTIONS) = RS ` : This pass checks and computes the
257
+ 4 . ` RESTRICTIONS(P , LT, ACTIONS) = RS ` : This pass checks and computes the
258
258
restrictions to maintain memory safety. These are the restrictions
259
259
that will go into the final loan. We'll discuss in more detail below.
260
260
@@ -263,7 +263,7 @@ that will go into the final loan. We'll discuss in more detail below.
263
263
Checking mutability is fairly straightforward. We just want to prevent
264
264
immutable data from being borrowed as mutable. Note that it is ok to borrow
265
265
mutable data as immutable, since that is simply a freeze. The judgement
266
- ` MUTABILITY(LV , MQ) ` means the mutability of ` LV ` is compatible with a borrow
266
+ ` MUTABILITY(P , MQ) ` means the mutability of ` P ` is compatible with a borrow
267
267
of mutability ` MQ ` . The Rust code corresponding to this predicate is the
268
268
function ` check_mutability ` in ` middle::borrowck::gather_loans ` .
269
269
@@ -288,15 +288,15 @@ MUTABILITY(X, imm) // M-Var-Imm
288
288
289
289
Fields and boxes inherit their mutability from
290
290
their base expressions, so both of their rules basically
291
- delegate the check to the base expression ` LV ` :
291
+ delegate the check to the base expression ` P ` :
292
292
293
293
``` text
294
- MUTABILITY(LV .f, MQ) // M-Field
295
- MUTABILITY(LV , MQ)
294
+ MUTABILITY(P .f, MQ) // M-Field
295
+ MUTABILITY(P , MQ)
296
296
297
- MUTABILITY(*LV , MQ) // M-Deref-Unique
298
- TYPE(LV ) = Box<Ty>
299
- MUTABILITY(LV , MQ)
297
+ MUTABILITY(*P , MQ) // M-Deref-Unique
298
+ TYPE(P ) = Box<Ty>
299
+ MUTABILITY(P , MQ)
300
300
```
301
301
302
302
### Checking mutability of immutable pointer types
@@ -305,24 +305,24 @@ Immutable pointer types like `&T` can only
305
305
be borrowed if MQ is immutable:
306
306
307
307
``` text
308
- MUTABILITY(*LV , imm) // M-Deref-Borrowed-Imm
309
- TYPE(LV ) = &Ty
308
+ MUTABILITY(*P , imm) // M-Deref-Borrowed-Imm
309
+ TYPE(P ) = &Ty
310
310
```
311
311
312
312
### Checking mutability of mutable pointer types
313
313
314
314
` &mut T ` can be frozen, so it is acceptable to borrow it as either imm or mut:
315
315
316
316
``` text
317
- MUTABILITY(*LV , MQ) // M-Deref-Borrowed-Mut
318
- TYPE(LV ) = &mut Ty
317
+ MUTABILITY(*P , MQ) // M-Deref-Borrowed-Mut
318
+ TYPE(P ) = &mut Ty
319
319
```
320
320
321
321
## Checking aliasability
322
322
323
323
The goal of the aliasability check is to ensure that we never permit ` &mut `
324
- borrows of aliasable data. The judgement ` ALIASABLE(LV , MQ) ` means the
325
- aliasability of ` LV ` is compatible with a borrow of mutability ` MQ ` . The Rust
324
+ borrows of aliasable data. The judgement ` ALIASABLE(P , MQ) ` means the
325
+ aliasability of ` P ` is compatible with a borrow of mutability ` MQ ` . The Rust
326
326
code corresponding to this predicate is the function ` check_aliasability() ` in
327
327
` middle::borrowck::gather_loans ` .
328
328
@@ -340,11 +340,11 @@ the stack frame.
340
340
Owned content is aliasable if it is found in an aliasable location:
341
341
342
342
``` text
343
- ALIASABLE(LV .f, MQ) // M-Field
344
- ALIASABLE(LV , MQ)
343
+ ALIASABLE(P .f, MQ) // M-Field
344
+ ALIASABLE(P , MQ)
345
345
346
- ALIASABLE(*LV , MQ) // M-Deref-Unique
347
- ALIASABLE(LV , MQ)
346
+ ALIASABLE(*P , MQ) // M-Deref-Unique
347
+ ALIASABLE(P , MQ)
348
348
```
349
349
350
350
### Checking aliasability of immutable pointer types
@@ -353,25 +353,25 @@ Immutable pointer types like `&T` are aliasable, and hence can only be
353
353
borrowed immutably:
354
354
355
355
``` text
356
- ALIASABLE(*LV , imm) // M-Deref-Borrowed-Imm
357
- TYPE(LV ) = &Ty
356
+ ALIASABLE(*P , imm) // M-Deref-Borrowed-Imm
357
+ TYPE(P ) = &Ty
358
358
```
359
359
360
360
### Checking aliasability of mutable pointer types
361
361
362
362
` &mut T ` can be frozen, so it is acceptable to borrow it as either imm or mut:
363
363
364
364
``` text
365
- ALIASABLE(*LV , MQ) // M-Deref-Borrowed-Mut
366
- TYPE(LV ) = &mut Ty
365
+ ALIASABLE(*P , MQ) // M-Deref-Borrowed-Mut
366
+ TYPE(P ) = &mut Ty
367
367
```
368
368
369
369
## Checking lifetime
370
370
371
371
These rules aim to ensure that no data is borrowed for a scope that exceeds
372
372
its lifetime. These two computations wind up being intimately related.
373
- Formally, we define a predicate ` LIFETIME(LV , LT, MQ) ` , which states that
374
- "the lvalue ` LV ` can be safely borrowed for the lifetime ` LT ` with mutability
373
+ Formally, we define a predicate ` LIFETIME(P , LT, MQ) ` , which states that
374
+ "the place ` P ` can be safely borrowed for the lifetime ` LT ` with mutability
375
375
` MQ ` ". The Rust code corresponding to this predicate is the module
376
376
` middle::borrowck::gather_loans::lifetime ` .
377
377
@@ -391,12 +391,12 @@ The lifetime of a field or box is the same as the lifetime
391
391
of its owner:
392
392
393
393
``` text
394
- LIFETIME(LV .f, LT, MQ) // L-Field
395
- LIFETIME(LV , LT, MQ)
394
+ LIFETIME(P .f, LT, MQ) // L-Field
395
+ LIFETIME(P , LT, MQ)
396
396
397
- LIFETIME(*LV , LT, MQ) // L-Deref-Send
398
- TYPE(LV ) = Box<Ty>
399
- LIFETIME(LV , LT, MQ)
397
+ LIFETIME(*P , LT, MQ) // L-Deref-Send
398
+ TYPE(P ) = Box<Ty>
399
+ LIFETIME(P , LT, MQ)
400
400
```
401
401
402
402
### Checking lifetime for derefs of references
@@ -408,26 +408,26 @@ of the borrow is shorter than the lifetime `LT'` of the pointer
408
408
itself:
409
409
410
410
``` text
411
- LIFETIME(*LV , LT, MQ) // L-Deref-Borrowed
412
- TYPE(LV ) = <' Ty OR <' mut Ty
411
+ LIFETIME(*P , LT, MQ) // L-Deref-Borrowed
412
+ TYPE(P ) = <' Ty OR <' mut Ty
413
413
LT <= LT'
414
414
```
415
415
416
416
## Computing the restrictions
417
417
418
418
The final rules govern the computation of * restrictions* , meaning that
419
419
we compute the set of actions that will be illegal for the life of the
420
- loan. The predicate is written `RESTRICTIONS(LV , LT, ACTIONS) =
420
+ loan. The predicate is written `RESTRICTIONS(P , LT, ACTIONS) =
421
421
RESTRICTION* ` , which can be read "in order to prevent ` ACTIONS` from
422
- occurring on ` LV ` , the restrictions ` RESTRICTION* ` must be respected
422
+ occurring on ` P ` , the restrictions ` RESTRICTION* ` must be respected
423
423
for the lifetime of the loan".
424
424
425
425
Note that there is an initial set of restrictions: these restrictions
426
426
are computed based on the kind of borrow:
427
427
428
428
``` text
429
- &mut LV => RESTRICTIONS(LV , LT, MUTATE|CLAIM|FREEZE)
430
- &LV => RESTRICTIONS(LV , LT, MUTATE|CLAIM)
429
+ &mut P => RESTRICTIONS(P , LT, MUTATE|CLAIM|FREEZE)
430
+ &P => RESTRICTIONS(P , LT, MUTATE|CLAIM)
431
431
```
432
432
433
433
The reasoning here is that a mutable borrow must be the only writer,
@@ -451,8 +451,8 @@ Restricting a field is the same as restricting the owner of that
451
451
field:
452
452
453
453
``` text
454
- RESTRICTIONS(LV .f, LT, ACTIONS) = RS, (LV .f, ACTIONS) // R-Field
455
- RESTRICTIONS(LV , LT, ACTIONS) = RS
454
+ RESTRICTIONS(P .f, LT, ACTIONS) = RS, (P .f, ACTIONS) // R-Field
455
+ RESTRICTIONS(P , LT, ACTIONS) = RS
456
456
```
457
457
458
458
The reasoning here is as follows. If the field must not be mutated,
@@ -467,32 +467,32 @@ origin of inherited mutability.
467
467
Because the mutability of owned referents is inherited, restricting an
468
468
owned referent is similar to restricting a field, in that it implies
469
469
restrictions on the pointer. However, boxes have an important
470
- twist: if the owner ` LV ` is mutated, that causes the owned referent
471
- ` *LV ` to be freed! So whenever an owned referent ` *LV ` is borrowed, we
472
- must prevent the box ` LV ` from being mutated, which means
470
+ twist: if the owner ` P ` is mutated, that causes the owned referent
471
+ ` *P ` to be freed! So whenever an owned referent ` *P ` is borrowed, we
472
+ must prevent the box ` P ` from being mutated, which means
473
473
that we always add ` MUTATE ` and ` CLAIM ` to the restriction set imposed
474
- on ` LV ` :
474
+ on ` P ` :
475
475
476
476
``` text
477
- RESTRICTIONS(*LV , LT, ACTIONS) = RS, (*LV , ACTIONS) // R-Deref-Send-Pointer
478
- TYPE(LV ) = Box<Ty>
479
- RESTRICTIONS(LV , LT, ACTIONS|MUTATE|CLAIM) = RS
477
+ RESTRICTIONS(*P , LT, ACTIONS) = RS, (*P , ACTIONS) // R-Deref-Send-Pointer
478
+ TYPE(P ) = Box<Ty>
479
+ RESTRICTIONS(P , LT, ACTIONS|MUTATE|CLAIM) = RS
480
480
```
481
481
482
482
### Restrictions for loans of immutable borrowed referents
483
483
484
484
Immutable borrowed referents are freely aliasable, meaning that
485
485
the compiler does not prevent you from copying the pointer. This
486
486
implies that issuing restrictions is useless. We might prevent the
487
- user from acting on ` *LV ` itself, but there could be another path
488
- ` *LV1 ` that refers to the exact same memory, and we would not be
487
+ user from acting on ` *P ` itself, but there could be another path
488
+ ` *P1 ` that refers to the exact same memory, and we would not be
489
489
restricting that path. Therefore, the rule for ` &Ty ` pointers
490
490
always returns an empty set of restrictions, and it only permits
491
491
restricting ` MUTATE ` and ` CLAIM ` actions:
492
492
493
493
``` text
494
- RESTRICTIONS(*LV , LT, ACTIONS) = [] // R-Deref-Imm-Borrowed
495
- TYPE(LV ) = <' Ty
494
+ RESTRICTIONS(*P , LT, ACTIONS) = [] // R-Deref-Imm-Borrowed
495
+ TYPE(P ) = <' Ty
496
496
LT <= LT' // (1)
497
497
ACTIONS subset of [MUTATE, CLAIM]
498
498
```
@@ -546,7 +546,7 @@ This function is legal. The reason for this is that the inner pointer
546
546
(` *point : &'b Point ` ) is enough to guarantee the memory is immutable
547
547
and valid for the lifetime ` 'b ` . This is reflected in
548
548
` RESTRICTIONS() ` by the fact that we do not recurse (i.e., we impose
549
- no restrictions on ` LV ` , which in this particular case is the pointer
549
+ no restrictions on ` P ` , which in this particular case is the pointer
550
550
` point : &'a &'b Point ` ).
551
551
552
552
#### Why both ` LIFETIME() ` and ` RESTRICTIONS() ` ?
@@ -612,10 +612,10 @@ while the new claimant is live.
612
612
The rule for mutable borrowed pointers is as follows:
613
613
614
614
``` text
615
- RESTRICTIONS(*LV , LT, ACTIONS) = RS, (*LV , ACTIONS) // R-Deref-Mut-Borrowed
616
- TYPE(LV ) = <' mut Ty
615
+ RESTRICTIONS(*P , LT, ACTIONS) = RS, (*P , ACTIONS) // R-Deref-Mut-Borrowed
616
+ TYPE(P ) = <' mut Ty
617
617
LT <= LT' // (1)
618
- RESTRICTIONS(LV , LT, ACTIONS) = RS // (2)
618
+ RESTRICTIONS(P , LT, ACTIONS) = RS // (2)
619
619
```
620
620
621
621
Let's examine the two numbered clauses:
@@ -670,7 +670,7 @@ fn foo(t0: &mut i32) {
670
670
671
671
Remember that ` &mut ` pointers are linear, and hence ` let t1 = t0 ` is a
672
672
move of ` t0 ` -- or would be, if it were legal. Instead, we get an
673
- error, because clause (2) imposes restrictions on ` LV ` (` t0 ` , here),
673
+ error, because clause (2) imposes restrictions on ` P ` (` t0 ` , here),
674
674
and any restrictions on a path make it impossible to move from that
675
675
path.
676
676
@@ -906,7 +906,7 @@ results of a dataflow computation.
906
906
907
907
The ` MovePath ` tree tracks every path that is moved or assigned to.
908
908
These paths have the same form as the ` LoanPath ` data structure, which
909
- in turn is the "real world version of the lvalues ` LV ` that we
909
+ in turn is the "real world version of the places ` P ` that we
910
910
introduced earlier. The difference between a ` MovePath ` and a ` LoanPath `
911
911
is that move paths are:
912
912
@@ -1132,7 +1132,7 @@ is implied by the relevant moves.
1132
1132
While writing up these docs, I encountered some rules I believe to be
1133
1133
stricter than necessary:
1134
1134
1135
- - I think restricting the ` &mut ` LV against moves and ` ALIAS ` is sufficient,
1135
+ - I think restricting the ` &mut ` P against moves and ` ALIAS ` is sufficient,
1136
1136
` MUTATE ` and ` CLAIM ` are overkill. ` MUTATE ` was necessary when swap was
1137
1137
a built-in operator, but as it is not, it is implied by ` CLAIM ` ,
1138
1138
and ` CLAIM ` is implied by ` ALIAS ` . The only net effect of this is an
0 commit comments