1
- use std:: collections:: { BTreeMap , BTreeSet } ;
2
-
3
1
use rustc_data_structures:: fx:: { FxHashMap , FxHashSet , FxIndexSet } ;
4
- use rustc_middle:: mir:: visit:: Visitor ;
5
- use rustc_middle:: mir:: {
6
- Body , Local , Location , Place , Rvalue , Statement , StatementKind , Terminator , TerminatorKind ,
7
- } ;
8
- use rustc_middle:: ty:: { RegionVid , TyCtxt } ;
2
+ use rustc_middle:: ty:: RegionVid ;
9
3
use rustc_mir_dataflow:: points:: PointIndex ;
10
4
11
5
use super :: { LiveLoans , LocalizedOutlivesConstraintSet } ;
6
+ use crate :: BorrowSet ;
12
7
use crate :: constraints:: OutlivesConstraint ;
13
- use crate :: dataflow:: BorrowIndex ;
14
8
use crate :: region_infer:: values:: LivenessValues ;
15
9
use crate :: type_check:: Locations ;
16
- use crate :: { BorrowSet , PlaceConflictBias , places_conflict} ;
17
10
18
- /// Compute loan reachability, stop at kills, and trace loan liveness throughout the CFG, by
11
+ /// Compute loan reachability to approximately trace loan liveness throughout the CFG, by
19
12
/// traversing the full graph of constraints that combines:
20
13
/// - the localized constraints (the physical edges),
21
14
/// - with the constraints that hold at all points (the logical edges).
22
15
pub ( super ) fn compute_loan_liveness < ' tcx > (
23
- tcx : TyCtxt < ' tcx > ,
24
- body : & Body < ' tcx > ,
25
16
liveness : & LivenessValues ,
26
17
outlives_constraints : impl Iterator < Item = OutlivesConstraint < ' tcx > > ,
27
18
borrow_set : & BorrowSet < ' tcx > ,
28
19
localized_outlives_constraints : & LocalizedOutlivesConstraintSet ,
29
20
) -> LiveLoans {
30
21
let mut live_loans = LiveLoans :: new ( borrow_set. len ( ) ) ;
31
22
32
- // FIXME: it may be preferable for kills to be encoded in the edges themselves, to simplify and
33
- // likely make traversal (and constraint generation) more efficient. We also display kills on
34
- // edges when visualizing the constraint graph anyways.
35
- let kills = collect_kills ( body, tcx, borrow_set) ;
36
-
37
23
// Create the full graph with the physical edges we've localized earlier, and the logical edges
38
24
// of constraints that hold at all points.
39
25
let logical_constraints =
@@ -59,15 +45,15 @@ pub(super) fn compute_loan_liveness<'tcx>(
59
45
continue ;
60
46
}
61
47
62
- // Record the loan as being live on entry to this point.
63
- live_loans . insert ( node . point , loan_idx ) ;
64
-
65
- // Here, we have a conundrum. There's currently a weakness in our theory , in that
66
- // we're using a single notion of reachability to represent what used to be _two_
67
- // different transitive closures. It didn't seem impactful when coming up with the
68
- // single-graph and reachability through space (regions) + time (CFG) concepts, but in
69
- // practice the combination of time-traveling with kills is more impactful than
70
- // initially anticipated.
48
+ // Record the loan as being live on entry to this point if it reaches a live region
49
+ // there.
50
+ //
51
+ // This is an approximation of liveness (which is the thing we want) , in that we're
52
+ // using a single notion of reachability to represent what used to be _two_ different
53
+ // transitive closures. It didn't seem impactful when coming up with the single-graph
54
+ // and reachability through space (regions) + time (CFG) concepts, but in practice the
55
+ // combination of time-traveling with kills is more impactful than initially
56
+ // anticipated.
71
57
//
72
58
// Kills should prevent a loan from reaching its successor points in the CFG, but not
73
59
// while time-traveling: we're not actually at that CFG point, but looking for
@@ -92,40 +78,20 @@ pub(super) fn compute_loan_liveness<'tcx>(
92
78
// two-step traversal described above: only kills encountered on exit via a backward
93
79
// edge are ignored.
94
80
//
95
- // In our test suite, there are a couple of cases where kills are encountered while
96
- // time-traveling, however as far as we can tell, always in cases where they would be
97
- // unreachable. We have reason to believe that this is a property of the single-graph
98
- // approach (but haven't proved it yet):
99
- // - reachable kills while time-traveling would also be encountered via regular
100
- // traversal
101
- // - it makes _some_ sense to ignore unreachable kills, but subtleties around dead code
102
- // in general need to be better thought through (like they were for NLLs).
103
- // - ignoring kills is a conservative approximation: the loan is still live and could
104
- // cause false positive errors at another place access. Soundness issues in this
105
- // domain should look more like the absence of reachability instead.
106
- //
107
- // This is enough in practice to pass tests, and therefore is what we have implemented
108
- // for now.
81
+ // This version of the analysis, however, is enough in practice to pass the tests that
82
+ // we care about and NLLs reject, without regressions on crater, and is an actionable
83
+ // subset of the full analysis. It also naturally points to areas of improvement that we
84
+ // wish to explore later, namely handling kills appropriately during traversal, instead
85
+ // of continuing traversal to all the reachable nodes.
109
86
//
110
- // FIXME: all of the above. Analyze potential unsoundness, possibly in concert with a
111
- // borrowck implementation in a-mir-formality, fuzzing, or manually crafting
112
- // counter-examples.
87
+ // FIXME: analyze potential unsoundness, possibly in concert with a borrowck
88
+ // implementation in a-mir-formality, fuzzing, or manually crafting counter-examples.
113
89
114
- // Continuing traversal will depend on whether the loan is killed at this point, and
115
- // whether we're time-traveling.
116
- let current_location = liveness. location_from_point ( node. point ) ;
117
- let is_loan_killed =
118
- kills. get ( & current_location) . is_some_and ( |kills| kills. contains ( & loan_idx) ) ;
90
+ if liveness. is_live_at ( node. region , liveness. location_from_point ( node. point ) ) {
91
+ live_loans. insert ( node. point , loan_idx) ;
92
+ }
119
93
120
94
for succ in graph. outgoing_edges ( node) {
121
- // If the loan is killed at this point, it is killed _on exit_. But only during
122
- // forward traversal.
123
- if is_loan_killed {
124
- let destination = liveness. location_from_point ( succ. point ) ;
125
- if current_location. is_predecessor_of ( destination, body) {
126
- continue ;
127
- }
128
- }
129
95
stack. push ( succ) ;
130
96
}
131
97
}
@@ -192,116 +158,3 @@ impl LocalizedConstraintGraph {
192
158
physical_edges. chain ( materialized_edges)
193
159
}
194
160
}
195
-
196
- /// Traverses the MIR and collects kills.
197
- fn collect_kills < ' tcx > (
198
- body : & Body < ' tcx > ,
199
- tcx : TyCtxt < ' tcx > ,
200
- borrow_set : & BorrowSet < ' tcx > ,
201
- ) -> BTreeMap < Location , BTreeSet < BorrowIndex > > {
202
- let mut collector = KillsCollector { borrow_set, tcx, body, kills : BTreeMap :: default ( ) } ;
203
- for ( block, data) in body. basic_blocks . iter_enumerated ( ) {
204
- collector. visit_basic_block_data ( block, data) ;
205
- }
206
- collector. kills
207
- }
208
-
209
- struct KillsCollector < ' a , ' tcx > {
210
- body : & ' a Body < ' tcx > ,
211
- tcx : TyCtxt < ' tcx > ,
212
- borrow_set : & ' a BorrowSet < ' tcx > ,
213
-
214
- /// The set of loans killed at each location.
215
- kills : BTreeMap < Location , BTreeSet < BorrowIndex > > ,
216
- }
217
-
218
- // This visitor has a similar structure to the `Borrows` dataflow computation with respect to kills,
219
- // and the datalog polonius fact generation for the `loan_killed_at` relation.
220
- impl < ' tcx > KillsCollector < ' _ , ' tcx > {
221
- /// Records the borrows on the specified place as `killed`. For example, when assigning to a
222
- /// local, or on a call's return destination.
223
- fn record_killed_borrows_for_place ( & mut self , place : Place < ' tcx > , location : Location ) {
224
- // For the reasons described in graph traversal, we also filter out kills
225
- // unreachable from the loan's introduction point, as they would stop traversal when
226
- // e.g. checking for reachability in the subset graph through invariance constraints
227
- // higher up.
228
- let filter_unreachable_kills = |loan| {
229
- let introduction = self . borrow_set [ loan] . reserve_location ;
230
- let reachable = introduction. is_predecessor_of ( location, self . body ) ;
231
- reachable
232
- } ;
233
-
234
- let other_borrows_of_local = self
235
- . borrow_set
236
- . local_map
237
- . get ( & place. local )
238
- . into_iter ( )
239
- . flat_map ( |bs| bs. iter ( ) )
240
- . copied ( ) ;
241
-
242
- // If the borrowed place is a local with no projections, all other borrows of this
243
- // local must conflict. This is purely an optimization so we don't have to call
244
- // `places_conflict` for every borrow.
245
- if place. projection . is_empty ( ) {
246
- if !self . body . local_decls [ place. local ] . is_ref_to_static ( ) {
247
- self . kills
248
- . entry ( location)
249
- . or_default ( )
250
- . extend ( other_borrows_of_local. filter ( |& loan| filter_unreachable_kills ( loan) ) ) ;
251
- }
252
- return ;
253
- }
254
-
255
- // By passing `PlaceConflictBias::NoOverlap`, we conservatively assume that any given
256
- // pair of array indices are not equal, so that when `places_conflict` returns true, we
257
- // will be assured that two places being compared definitely denotes the same sets of
258
- // locations.
259
- let definitely_conflicting_borrows = other_borrows_of_local
260
- . filter ( |& i| {
261
- places_conflict (
262
- self . tcx ,
263
- self . body ,
264
- self . borrow_set [ i] . borrowed_place ,
265
- place,
266
- PlaceConflictBias :: NoOverlap ,
267
- )
268
- } )
269
- . filter ( |& loan| filter_unreachable_kills ( loan) ) ;
270
-
271
- self . kills . entry ( location) . or_default ( ) . extend ( definitely_conflicting_borrows) ;
272
- }
273
-
274
- /// Records the borrows on the specified local as `killed`.
275
- fn record_killed_borrows_for_local ( & mut self , local : Local , location : Location ) {
276
- if let Some ( borrow_indices) = self . borrow_set . local_map . get ( & local) {
277
- self . kills . entry ( location) . or_default ( ) . extend ( borrow_indices. iter ( ) ) ;
278
- }
279
- }
280
- }
281
-
282
- impl < ' tcx > Visitor < ' tcx > for KillsCollector < ' _ , ' tcx > {
283
- fn visit_statement ( & mut self , statement : & Statement < ' tcx > , location : Location ) {
284
- // Make sure there are no remaining borrows for locals that have gone out of scope.
285
- if let StatementKind :: StorageDead ( local) = statement. kind {
286
- self . record_killed_borrows_for_local ( local, location) ;
287
- }
288
-
289
- self . super_statement ( statement, location) ;
290
- }
291
-
292
- fn visit_assign ( & mut self , place : & Place < ' tcx > , rvalue : & Rvalue < ' tcx > , location : Location ) {
293
- // When we see `X = ...`, then kill borrows of `(*X).foo` and so forth.
294
- self . record_killed_borrows_for_place ( * place, location) ;
295
- self . super_assign ( place, rvalue, location) ;
296
- }
297
-
298
- fn visit_terminator ( & mut self , terminator : & Terminator < ' tcx > , location : Location ) {
299
- // A `Call` terminator's return value can be a local which has borrows, so we need to record
300
- // those as killed as well.
301
- if let TerminatorKind :: Call { destination, .. } = terminator. kind {
302
- self . record_killed_borrows_for_place ( destination, location) ;
303
- }
304
-
305
- self . super_terminator ( terminator, location) ;
306
- }
307
- }
0 commit comments