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
-
53
1
#![ deny( rustc:: untranslatable_diagnostic) ]
54
2
#![ deny( rustc:: diagnostic_outside_of_impl) ]
55
3
use crate :: ArtificialField ;
56
4
use crate :: Overlap ;
57
5
use crate :: { AccessDepth , Deep , Shallow } ;
58
6
use rustc_hir as hir;
59
7
use rustc_middle:: mir:: {
60
- Body , BorrowKind , MutBorrowKind , Place , PlaceElem , PlaceRef , ProjectionElem ,
8
+ Body , BorrowKind , Local , MutBorrowKind , Place , PlaceElem , PlaceRef , ProjectionElem ,
61
9
} ;
62
10
use rustc_middle:: ty:: { self , TyCtxt } ;
63
11
use std:: cmp:: max;
@@ -100,7 +48,7 @@ pub fn places_conflict<'tcx>(
100
48
/// access depth. The `bias` parameter is used to determine how the unknowable (comparing runtime
101
49
/// array indices, for example) should be interpreted - this depends on what the caller wants in
102
50
/// order to make the conservative choice and preserve soundness.
103
- #[ inline ]
51
+ #[ instrument ( level = "debug" , skip ( tcx , body ) ) ]
104
52
pub ( super ) fn borrow_conflicts_with_place < ' tcx > (
105
53
tcx : TyCtxt < ' tcx > ,
106
54
body : & Body < ' tcx > ,
@@ -110,24 +58,15 @@ pub(super) fn borrow_conflicts_with_place<'tcx>(
110
58
access : AccessDepth ,
111
59
bias : PlaceConflictBias ,
112
60
) -> 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
-
121
61
// This Local/Local case is handled by the more general code below, but
122
62
// it's so common that it's a speed win to check for it first.
123
- if borrow_place. projection . is_empty ( ) && access_place. projection . is_empty ( ) {
124
- return true ;
63
+ if let Some ( l1 ) = borrow_place. as_local ( ) && let Some ( l2 ) = access_place. as_local ( ) {
64
+ return l1 == l2 ;
125
65
}
126
66
127
67
place_components_conflict ( tcx, body, borrow_place, borrow_kind, access_place, access, bias)
128
68
}
129
69
130
- #[ instrument( level = "debug" , skip( tcx, body) ) ]
131
70
fn place_components_conflict < ' tcx > (
132
71
tcx : TyCtxt < ' tcx > ,
133
72
body : & Body < ' tcx > ,
@@ -137,10 +76,65 @@ fn place_components_conflict<'tcx>(
137
76
access : AccessDepth ,
138
77
bias : PlaceConflictBias ,
139
78
) -> 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
+
140
121
let borrow_local = borrow_place. local ;
141
122
let access_local = access_place. local ;
142
- // borrow_conflicts_with_place should have checked that.
143
- assert_eq ! ( borrow_local, access_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
+ }
144
138
145
139
// loop invariant: borrow_c is always either equal to access_c or disjoint from it.
146
140
for ( ( borrow_place, borrow_c) , & access_c) in
@@ -283,6 +277,21 @@ fn place_components_conflict<'tcx>(
283
277
}
284
278
}
285
279
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
+
286
295
// Given that the bases of `elem1` and `elem2` are always either equal
287
296
// or disjoint (and have the same type!), return the overlap situation
288
297
// between `elem1` and `elem2`.
0 commit comments