1- use std:: collections:: { BTreeMap , BTreeSet } ;
2-
31use 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 ;
93use rustc_mir_dataflow:: points:: PointIndex ;
104
115use super :: { LiveLoans , LocalizedOutlivesConstraintSet } ;
6+ use crate :: BorrowSet ;
127use crate :: constraints:: OutlivesConstraint ;
13- use crate :: dataflow:: BorrowIndex ;
148use crate :: region_infer:: values:: LivenessValues ;
159use crate :: type_check:: Locations ;
16- use crate :: { BorrowSet , PlaceConflictBias , places_conflict} ;
1710
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
1912/// traversing the full graph of constraints that combines:
2013/// - the localized constraints (the physical edges),
2114/// - with the constraints that hold at all points (the logical edges).
2215pub ( super ) fn compute_loan_liveness < ' tcx > (
23- tcx : TyCtxt < ' tcx > ,
24- body : & Body < ' tcx > ,
2516 liveness : & LivenessValues ,
2617 outlives_constraints : impl Iterator < Item = OutlivesConstraint < ' tcx > > ,
2718 borrow_set : & BorrowSet < ' tcx > ,
2819 localized_outlives_constraints : & LocalizedOutlivesConstraintSet ,
2920) -> LiveLoans {
3021 let mut live_loans = LiveLoans :: new ( borrow_set. len ( ) ) ;
3122
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-
3723 // Create the full graph with the physical edges we've localized earlier, and the logical edges
3824 // of constraints that hold at all points.
3925 let logical_constraints =
@@ -59,15 +45,15 @@ pub(super) fn compute_loan_liveness<'tcx>(
5945 continue ;
6046 }
6147
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.
7157 //
7258 // Kills should prevent a loan from reaching its successor points in the CFG, but not
7359 // 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>(
9278 // two-step traversal described above: only kills encountered on exit via a backward
9379 // edge are ignored.
9480 //
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.
10986 //
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.
11389
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+ }
11993
12094 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- }
12995 stack. push ( succ) ;
13096 }
13197 }
@@ -192,116 +158,3 @@ impl LocalizedConstraintGraph {
192158 physical_edges. chain ( materialized_edges)
193159 }
194160}
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