1
+ //! The borrowck rules for proving disjointness are applied from the "root" of the
2
+ //! borrow forwards, iterating over "similar" projections in lockstep until
3
+ //! we can prove overlap one way or another. Essentially, we treat `Overlap` as
4
+ //! a monoid and report a conflict if the product ends up not being `Disjoint`.
5
+ //!
6
+ //! At each step, if we didn't run out of borrow or place, we know that our elements
7
+ //! have the same type, and that they only overlap if they are the identical.
8
+ //!
9
+ //! For example, if we are comparing these:
10
+ //! ```text
11
+ //! BORROW: (*x1[2].y).z.a
12
+ //! ACCESS: (*x1[i].y).w.b
13
+ //! ```
14
+ //!
15
+ //! Then our steps are:
16
+ //! ```text
17
+ //! x1 | x1 -- places are the same
18
+ //! x1[2] | x1[i] -- equal or disjoint (disjoint if indexes differ)
19
+ //! x1[2].y | x1[i].y -- equal or disjoint
20
+ //! *x1[2].y | *x1[i].y -- equal or disjoint
21
+ //! (*x1[2].y).z | (*x1[i].y).w -- we are disjoint and don't need to check more!
22
+ //! ```
23
+ //!
24
+ //! Because `zip` does potentially bad things to the iterator inside, this loop
25
+ //! also handles the case where the access might be a *prefix* of the borrow, e.g.
26
+ //!
27
+ //! ```text
28
+ //! BORROW: (*x1[2].y).z.a
29
+ //! ACCESS: x1[i].y
30
+ //! ```
31
+ //!
32
+ //! Then our steps are:
33
+ //! ```text
34
+ //! x1 | x1 -- places are the same
35
+ //! x1[2] | x1[i] -- equal or disjoint (disjoint if indexes differ)
36
+ //! x1[2].y | x1[i].y -- equal or disjoint
37
+ //! ```
38
+ //!
39
+ //! -- here we run out of access - the borrow can access a part of it. If this
40
+ //! is a full deep access, then we *know* the borrow conflicts with it. However,
41
+ //! if the access is shallow, then we can proceed:
42
+ //!
43
+ //! ```text
44
+ //! x1[2].y | (*x1[i].y) -- a deref! the access can't get past this, so we
45
+ //! are disjoint
46
+ //! ```
47
+ //!
48
+ //! Our invariant is, that at each step of the iteration:
49
+ //! - If we didn't run out of access to match, our borrow and access are comparable
50
+ //! and either equal or disjoint.
51
+ //! - If we did run out of access, the borrow can access a part of it.
52
+
1
53
#![ deny( rustc:: untranslatable_diagnostic) ]
2
54
#![ deny( rustc:: diagnostic_outside_of_impl) ]
3
55
use crate :: ArtificialField ;
4
56
use crate :: Overlap ;
5
57
use crate :: { AccessDepth , Deep , Shallow } ;
6
58
use rustc_hir as hir;
7
59
use rustc_middle:: mir:: {
8
- Body , BorrowKind , Local , MutBorrowKind , Place , PlaceElem , PlaceRef , ProjectionElem ,
60
+ Body , BorrowKind , MutBorrowKind , Place , PlaceElem , PlaceRef , ProjectionElem ,
9
61
} ;
10
62
use rustc_middle:: ty:: { self , TyCtxt } ;
11
63
use std:: cmp:: max;
@@ -48,7 +100,7 @@ pub fn places_conflict<'tcx>(
48
100
/// access depth. The `bias` parameter is used to determine how the unknowable (comparing runtime
49
101
/// array indices, for example) should be interpreted - this depends on what the caller wants in
50
102
/// order to make the conservative choice and preserve soundness.
51
- #[ instrument ( level = "debug" , skip ( tcx , body ) ) ]
103
+ #[ inline ]
52
104
pub ( super ) fn borrow_conflicts_with_place < ' tcx > (
53
105
tcx : TyCtxt < ' tcx > ,
54
106
body : & Body < ' tcx > ,
@@ -58,15 +110,24 @@ pub(super) fn borrow_conflicts_with_place<'tcx>(
58
110
access : AccessDepth ,
59
111
bias : PlaceConflictBias ,
60
112
) -> bool {
113
+ let borrow_local = borrow_place. local ;
114
+ let access_local = access_place. local ;
115
+
116
+ if borrow_local != access_local {
117
+ // We have proven the borrow disjoint - further projections will remain disjoint.
118
+ return false ;
119
+ }
120
+
61
121
// This Local/Local case is handled by the more general code below, but
62
122
// it's so common that it's a speed win to check for it first.
63
- if let Some ( l1 ) = borrow_place. as_local ( ) && let Some ( l2 ) = access_place. as_local ( ) {
64
- return l1 == l2 ;
123
+ if borrow_place. projection . is_empty ( ) && access_place. projection . is_empty ( ) {
124
+ return true ;
65
125
}
66
126
67
127
place_components_conflict ( tcx, body, borrow_place, borrow_kind, access_place, access, bias)
68
128
}
69
129
130
+ #[ instrument( level = "debug" , skip( tcx, body) ) ]
70
131
fn place_components_conflict < ' tcx > (
71
132
tcx : TyCtxt < ' tcx > ,
72
133
body : & Body < ' tcx > ,
@@ -76,65 +137,10 @@ fn place_components_conflict<'tcx>(
76
137
access : AccessDepth ,
77
138
bias : PlaceConflictBias ,
78
139
) -> bool {
79
- // The borrowck rules for proving disjointness are applied from the "root" of the
80
- // borrow forwards, iterating over "similar" projections in lockstep until
81
- // we can prove overlap one way or another. Essentially, we treat `Overlap` as
82
- // a monoid and report a conflict if the product ends up not being `Disjoint`.
83
- //
84
- // At each step, if we didn't run out of borrow or place, we know that our elements
85
- // have the same type, and that they only overlap if they are the identical.
86
- //
87
- // For example, if we are comparing these:
88
- // BORROW: (*x1[2].y).z.a
89
- // ACCESS: (*x1[i].y).w.b
90
- //
91
- // Then our steps are:
92
- // x1 | x1 -- places are the same
93
- // x1[2] | x1[i] -- equal or disjoint (disjoint if indexes differ)
94
- // x1[2].y | x1[i].y -- equal or disjoint
95
- // *x1[2].y | *x1[i].y -- equal or disjoint
96
- // (*x1[2].y).z | (*x1[i].y).w -- we are disjoint and don't need to check more!
97
- //
98
- // Because `zip` does potentially bad things to the iterator inside, this loop
99
- // also handles the case where the access might be a *prefix* of the borrow, e.g.
100
- //
101
- // BORROW: (*x1[2].y).z.a
102
- // ACCESS: x1[i].y
103
- //
104
- // Then our steps are:
105
- // x1 | x1 -- places are the same
106
- // x1[2] | x1[i] -- equal or disjoint (disjoint if indexes differ)
107
- // x1[2].y | x1[i].y -- equal or disjoint
108
- //
109
- // -- here we run out of access - the borrow can access a part of it. If this
110
- // is a full deep access, then we *know* the borrow conflicts with it. However,
111
- // if the access is shallow, then we can proceed:
112
- //
113
- // x1[2].y | (*x1[i].y) -- a deref! the access can't get past this, so we
114
- // are disjoint
115
- //
116
- // Our invariant is, that at each step of the iteration:
117
- // - If we didn't run out of access to match, our borrow and access are comparable
118
- // and either equal or disjoint.
119
- // - If we did run out of access, the borrow can access a part of it.
120
-
121
140
let borrow_local = borrow_place. local ;
122
141
let access_local = access_place. local ;
123
-
124
- match place_base_conflict ( borrow_local, access_local) {
125
- Overlap :: Arbitrary => {
126
- bug ! ( "Two base can't return Arbitrary" ) ;
127
- }
128
- Overlap :: EqualOrDisjoint => {
129
- // This is the recursive case - proceed to the next element.
130
- }
131
- Overlap :: Disjoint => {
132
- // We have proven the borrow disjoint - further
133
- // projections will remain disjoint.
134
- debug ! ( "borrow_conflicts_with_place: disjoint" ) ;
135
- return false ;
136
- }
137
- }
142
+ // borrow_conflicts_with_place should have checked that.
143
+ assert_eq ! ( borrow_local, access_local) ;
138
144
139
145
// loop invariant: borrow_c is always either equal to access_c or disjoint from it.
140
146
for ( ( borrow_place, borrow_c) , & access_c) in
@@ -277,21 +283,6 @@ fn place_components_conflict<'tcx>(
277
283
}
278
284
}
279
285
280
- // Given that the bases of `elem1` and `elem2` are always either equal
281
- // or disjoint (and have the same type!), return the overlap situation
282
- // between `elem1` and `elem2`.
283
- fn place_base_conflict ( l1 : Local , l2 : Local ) -> Overlap {
284
- if l1 == l2 {
285
- // the same local - base case, equal
286
- debug ! ( "place_element_conflict: DISJOINT-OR-EQ-LOCAL" ) ;
287
- Overlap :: EqualOrDisjoint
288
- } else {
289
- // different locals - base case, disjoint
290
- debug ! ( "place_element_conflict: DISJOINT-LOCAL" ) ;
291
- Overlap :: Disjoint
292
- }
293
- }
294
-
295
286
// Given that the bases of `elem1` and `elem2` are always either equal
296
287
// or disjoint (and have the same type!), return the overlap situation
297
288
// between `elem1` and `elem2`.
0 commit comments