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+
143#![ deny( rustc:: untranslatable_diagnostic) ]
244#![ deny( rustc:: diagnostic_outside_of_impl) ]
345use crate :: ArtificialField ;
@@ -46,7 +88,7 @@ pub(crate) fn places_conflict<'tcx>(
4688/// access depth. The `bias` parameter is used to determine how the unknowable (comparing runtime
4789/// array indices, for example) should be interpreted - this depends on what the caller wants in
4890/// order to make the conservative choice and preserve soundness.
49- #[ instrument ( level = "debug" , skip ( tcx , body ) ) ]
91+ #[ inline ]
5092pub ( super ) fn borrow_conflicts_with_place < ' tcx > (
5193 tcx : TyCtxt < ' tcx > ,
5294 body : & Body < ' tcx > ,
@@ -56,15 +98,24 @@ pub(super) fn borrow_conflicts_with_place<'tcx>(
5698 access : AccessDepth ,
5799 bias : PlaceConflictBias ,
58100) -> 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+
59109 // This Local/Local case is handled by the more general code below, but
60110 // 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 ;
63113 }
64114
65115 place_components_conflict ( tcx, body, borrow_place, borrow_kind, access_place, access, bias)
66116}
67117
118+ #[ instrument( level = "debug" , skip( tcx, body) ) ]
68119fn place_components_conflict < ' tcx > (
69120 tcx : TyCtxt < ' tcx > ,
70121 body : & Body < ' tcx > ,
@@ -74,65 +125,10 @@ fn place_components_conflict<'tcx>(
74125 access : AccessDepth ,
75126 bias : PlaceConflictBias ,
76127) -> 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-
119128 let borrow_local = borrow_place. local ;
120129 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) ;
136132
137133 // loop invariant: borrow_c is always either equal to access_c or disjoint from it.
138134 for ( i, ( borrow_c, & access_c) ) in
@@ -287,21 +283,6 @@ fn place_components_conflict<'tcx>(
287283 }
288284}
289285
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-
305286// Given that the bases of `elem1` and `elem2` are always either equal
306287// or disjoint (and have the same type!), return the overlap situation
307288// between `elem1` and `elem2`.
0 commit comments