@@ -43,22 +43,22 @@ it is safe with respect to the in-scope loans.
4343# Formal model
4444
4545Throughout 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:
4747
4848``` text
49- LV = x | LV .f | *LV
49+ P = x | P .f | *P
5050```
5151
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
5454niceties. This means that if you have a type like:
5555
5656``` rust
5757struct S { f : i32 }
5858```
5959
6060and 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 ` .
6262
6363Here is the formal grammar for the types we'll consider:
6464
@@ -99,7 +99,7 @@ this sort of thing.
9999#### Loans and restrictions
100100
101101The 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
103103real life there are a few other cases to consider). For each borrow
104104expression, it computes a ` Loan ` , which is a data structure that
105105records (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
108108follows:
109109
110110``` text
111- LOAN = (LV , LT, MQ, RESTRICTION*)
112- RESTRICTION = (LV , ACTION*)
111+ LOAN = (P , LT, MQ, RESTRICTION*)
112+ RESTRICTION = (P , ACTION*)
113113ACTION = MUTATE | CLAIM | FREEZE
114114```
115115
116- Here the ` LOAN ` tuple defines the lvalue ` LV ` being borrowed; the
116+ Here the ` LOAN ` tuple defines the place ` P ` being borrowed; the
117117lifetime ` LT ` of that borrow; the mutability ` MQ ` of the borrow; and a
118118list of restrictions. The restrictions indicate actions which, if
119119taken, could invalidate the loan and lead to type safety violations.
120120
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
122122either be the path that was borrowed or some prefix of the path that
123123was 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 ` :
125125
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;
129129
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 , []) ` ,
132132which 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
134134action because that would imply that sometimes moves are permitted
135135from restricted values, which is not the case.
136136
@@ -239,22 +239,22 @@ live. (This is done via restrictions, read on.)
239239
240240We start with the ` gather_loans ` pass, which walks the AST looking for
241241borrows. 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 `
243243of the resulting pointer. Given those, ` gather_loans ` applies four
244244validity tests:
245245
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
248248data as mutable).
249249
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
252252` &mut ` borrows of aliasability data.
253253
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
255255the lifetime of the value being borrowed.
256256
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
258258restrictions to maintain memory safety. These are the restrictions
259259that will go into the final loan. We'll discuss in more detail below.
260260
@@ -263,7 +263,7 @@ that will go into the final loan. We'll discuss in more detail below.
263263Checking mutability is fairly straightforward. We just want to prevent
264264immutable data from being borrowed as mutable. Note that it is ok to borrow
265265mutable 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
267267of mutability ` MQ ` . The Rust code corresponding to this predicate is the
268268function ` check_mutability ` in ` middle::borrowck::gather_loans ` .
269269
@@ -288,15 +288,15 @@ MUTABILITY(X, imm) // M-Var-Imm
288288
289289Fields and boxes inherit their mutability from
290290their 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 ` :
292292
293293``` text
294- MUTABILITY(LV .f, MQ) // M-Field
295- MUTABILITY(LV , MQ)
294+ MUTABILITY(P .f, MQ) // M-Field
295+ MUTABILITY(P , MQ)
296296
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)
300300```
301301
302302### Checking mutability of immutable pointer types
@@ -305,24 +305,24 @@ Immutable pointer types like `&T` can only
305305be borrowed if MQ is immutable:
306306
307307``` 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
310310```
311311
312312### Checking mutability of mutable pointer types
313313
314314` &mut T ` can be frozen, so it is acceptable to borrow it as either imm or mut:
315315
316316``` 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
319319```
320320
321321## Checking aliasability
322322
323323The 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
326326code corresponding to this predicate is the function ` check_aliasability() ` in
327327` middle::borrowck::gather_loans ` .
328328
@@ -340,11 +340,11 @@ the stack frame.
340340Owned content is aliasable if it is found in an aliasable location:
341341
342342``` text
343- ALIASABLE(LV .f, MQ) // M-Field
344- ALIASABLE(LV , MQ)
343+ ALIASABLE(P .f, MQ) // M-Field
344+ ALIASABLE(P , MQ)
345345
346- ALIASABLE(*LV , MQ) // M-Deref-Unique
347- ALIASABLE(LV , MQ)
346+ ALIASABLE(*P , MQ) // M-Deref-Unique
347+ ALIASABLE(P , MQ)
348348```
349349
350350### Checking aliasability of immutable pointer types
@@ -353,25 +353,25 @@ Immutable pointer types like `&T` are aliasable, and hence can only be
353353borrowed immutably:
354354
355355``` 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
358358```
359359
360360### Checking aliasability of mutable pointer types
361361
362362` &mut T ` can be frozen, so it is acceptable to borrow it as either imm or mut:
363363
364364``` 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
367367```
368368
369369## Checking lifetime
370370
371371These rules aim to ensure that no data is borrowed for a scope that exceeds
372372its 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
375375` MQ ` ". The Rust code corresponding to this predicate is the module
376376` middle::borrowck::gather_loans::lifetime ` .
377377
@@ -391,12 +391,12 @@ The lifetime of a field or box is the same as the lifetime
391391of its owner:
392392
393393``` 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)
396396
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)
400400```
401401
402402### Checking lifetime for derefs of references
@@ -408,26 +408,26 @@ of the borrow is shorter than the lifetime `LT'` of the pointer
408408itself:
409409
410410``` 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
413413 LT <= LT'
414414```
415415
416416## Computing the restrictions
417417
418418The final rules govern the computation of * restrictions* , meaning that
419419we 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) =
421421RESTRICTION* ` , 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
423423for the lifetime of the loan".
424424
425425Note that there is an initial set of restrictions: these restrictions
426426are computed based on the kind of borrow:
427427
428428``` 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)
431431```
432432
433433The 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
451451field:
452452
453453``` 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
456456```
457457
458458The reasoning here is as follows. If the field must not be mutated,
@@ -467,32 +467,32 @@ origin of inherited mutability.
467467Because the mutability of owned referents is inherited, restricting an
468468owned referent is similar to restricting a field, in that it implies
469469restrictions 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
473473that we always add ` MUTATE ` and ` CLAIM ` to the restriction set imposed
474- on ` LV ` :
474+ on ` P ` :
475475
476476``` 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
480480```
481481
482482### Restrictions for loans of immutable borrowed referents
483483
484484Immutable borrowed referents are freely aliasable, meaning that
485485the compiler does not prevent you from copying the pointer. This
486486implies 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
489489restricting that path. Therefore, the rule for ` &Ty ` pointers
490490always returns an empty set of restrictions, and it only permits
491491restricting ` MUTATE ` and ` CLAIM ` actions:
492492
493493``` 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
496496 LT <= LT' // (1)
497497 ACTIONS subset of [MUTATE, CLAIM]
498498```
@@ -546,7 +546,7 @@ This function is legal. The reason for this is that the inner pointer
546546(` *point : &'b Point ` ) is enough to guarantee the memory is immutable
547547and valid for the lifetime ` 'b ` . This is reflected in
548548` 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
550550` point : &'a &'b Point ` ).
551551
552552#### Why both ` LIFETIME() ` and ` RESTRICTIONS() ` ?
@@ -612,10 +612,10 @@ while the new claimant is live.
612612The rule for mutable borrowed pointers is as follows:
613613
614614``` 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
617617 LT <= LT' // (1)
618- RESTRICTIONS(LV , LT, ACTIONS) = RS // (2)
618+ RESTRICTIONS(P , LT, ACTIONS) = RS // (2)
619619```
620620
621621Let's examine the two numbered clauses:
@@ -670,7 +670,7 @@ fn foo(t0: &mut i32) {
670670
671671Remember that ` &mut ` pointers are linear, and hence ` let t1 = t0 ` is a
672672move 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),
674674and any restrictions on a path make it impossible to move from that
675675path.
676676
@@ -906,7 +906,7 @@ results of a dataflow computation.
906906
907907The ` MovePath ` tree tracks every path that is moved or assigned to.
908908These 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
910910introduced earlier. The difference between a ` MovePath ` and a ` LoanPath `
911911is that move paths are:
912912
@@ -1132,7 +1132,7 @@ is implied by the relevant moves.
11321132While writing up these docs, I encountered some rules I believe to be
11331133stricter than necessary:
11341134
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,
11361136 ` MUTATE ` and ` CLAIM ` are overkill. ` MUTATE ` was necessary when swap was
11371137 a built-in operator, but as it is not, it is implied by ` CLAIM ` ,
11381138 and ` CLAIM ` is implied by ` ALIAS ` . The only net effect of this is an
0 commit comments