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