@@ -23,6 +23,9 @@ use crate::*;
23
23
pub mod diagnostics;
24
24
use diagnostics:: { AllocHistory , TagHistory } ;
25
25
26
+ pub mod stack;
27
+ use stack:: Stack ;
28
+
26
29
pub type CallId = NonZeroU64 ;
27
30
28
31
// Even reading memory can have effects on the stack, so we need a `RefCell` here.
@@ -111,23 +114,6 @@ impl fmt::Debug for Item {
111
114
}
112
115
}
113
116
114
- /// Extra per-location state.
115
- #[ derive( Clone , Debug , PartialEq , Eq ) ]
116
- pub struct Stack {
117
- /// Used *mostly* as a stack; never empty.
118
- /// Invariants:
119
- /// * Above a `SharedReadOnly` there can only be more `SharedReadOnly`.
120
- /// * No tag occurs in the stack more than once.
121
- borrows : Vec < Item > ,
122
- /// If this is `Some(id)`, then the actual current stack is unknown. This can happen when
123
- /// wildcard pointers are used to access this location. What we do know is that `borrows` are at
124
- /// the top of the stack, and below it are arbitrarily many items whose `tag` is strictly less
125
- /// than `id`.
126
- /// When the bottom is unknown, `borrows` always has a `SharedReadOnly` or `Unique` at the bottom;
127
- /// we never have the unknown-to-known boundary in an SRW group.
128
- unknown_bottom : Option < SbTag > ,
129
- }
130
-
131
117
/// Extra per-allocation state.
132
118
#[ derive( Clone , Debug ) ]
133
119
pub struct Stacks {
@@ -298,65 +284,10 @@ impl Permission {
298
284
299
285
/// Core per-location operations: access, dealloc, reborrow.
300
286
impl < ' tcx > Stack {
301
- /// Find the item granting the given kind of access to the given tag, and return where
302
- /// it is on the stack. For wildcard tags, the given index is approximate, but if *no*
303
- /// index is given it means the match was *not* in the known part of the stack.
304
- /// `Ok(None)` indicates it matched the "unknown" part of the stack.
305
- /// `Err` indicates it was not found.
306
- fn find_granting (
307
- & self ,
308
- access : AccessKind ,
309
- tag : SbTagExtra ,
310
- exposed_tags : & FxHashSet < SbTag > ,
311
- ) -> Result < Option < usize > , ( ) > {
312
- let SbTagExtra :: Concrete ( tag) = tag else {
313
- // Handle the wildcard case.
314
- // Go search the stack for an exposed tag.
315
- if let Some ( idx) =
316
- self . borrows
317
- . iter ( )
318
- . enumerate ( ) // we also need to know *where* in the stack
319
- . rev ( ) // search top-to-bottom
320
- . find_map ( |( idx, item) | {
321
- // If the item fits and *might* be this wildcard, use it.
322
- if item. perm . grants ( access) && exposed_tags. contains ( & item. tag ) {
323
- Some ( idx)
324
- } else {
325
- None
326
- }
327
- } )
328
- {
329
- return Ok ( Some ( idx) ) ;
330
- }
331
- // If we couldn't find it in the stack, check the unknown bottom.
332
- return if self . unknown_bottom . is_some ( ) { Ok ( None ) } else { Err ( ( ) ) } ;
333
- } ;
334
-
335
- if let Some ( idx) =
336
- self . borrows
337
- . iter ( )
338
- . enumerate ( ) // we also need to know *where* in the stack
339
- . rev ( ) // search top-to-bottom
340
- // Return permission of first item that grants access.
341
- // We require a permission with the right tag, ensuring U3 and F3.
342
- . find_map ( |( idx, item) | {
343
- if tag == item. tag && item. perm . grants ( access) { Some ( idx) } else { None }
344
- } )
345
- {
346
- return Ok ( Some ( idx) ) ;
347
- }
348
-
349
- // Couldn't find it in the stack; but if there is an unknown bottom it might be there.
350
- let found = self . unknown_bottom . is_some_and ( |& unknown_limit| {
351
- tag. 0 < unknown_limit. 0 // unknown_limit is an upper bound for what can be in the unknown bottom.
352
- } ) ;
353
- if found { Ok ( None ) } else { Err ( ( ) ) }
354
- }
355
-
356
287
/// Find the first write-incompatible item above the given one --
357
288
/// i.e, find the height to which the stack will be truncated when writing to `granting`.
358
289
fn find_first_write_incompatible ( & self , granting : usize ) -> usize {
359
- let perm = self . borrows [ granting] . perm ;
290
+ let perm = self . get ( granting) . unwrap ( ) . perm ;
360
291
match perm {
361
292
Permission :: SharedReadOnly => bug ! ( "Cannot use SharedReadOnly for writing" ) ,
362
293
Permission :: Disabled => bug ! ( "Cannot use Disabled for anything" ) ,
@@ -367,7 +298,7 @@ impl<'tcx> Stack {
367
298
Permission :: SharedReadWrite => {
368
299
// The SharedReadWrite *just* above us are compatible, to skip those.
369
300
let mut idx = granting + 1 ;
370
- while let Some ( item) = self . borrows . get ( idx) {
301
+ while let Some ( item) = self . get ( idx) {
371
302
if item. perm == Permission :: SharedReadWrite {
372
303
// Go on.
373
304
idx += 1 ;
@@ -462,16 +393,16 @@ impl<'tcx> Stack {
462
393
// There is a SRW group boundary between the unknown and the known, so everything is incompatible.
463
394
0
464
395
} ;
465
- for item in self . borrows . drain ( first_incompatible_idx..) . rev ( ) {
466
- trace ! ( "access: popping item {:?}" , item) ;
396
+ self . pop_items_after ( first_incompatible_idx, |item| {
467
397
Stack :: item_popped (
468
398
& item,
469
399
Some ( ( tag, alloc_range, offset, access) ) ,
470
400
global,
471
401
alloc_history,
472
402
) ?;
473
403
alloc_history. log_invalidation ( item. tag , alloc_range, current_span) ;
474
- }
404
+ Ok ( ( ) )
405
+ } ) ?;
475
406
} else {
476
407
// On a read, *disable* all `Unique` above the granting item. This ensures U2 for read accesses.
477
408
// The reason this is not following the stack discipline (by removing the first Unique and
@@ -488,44 +419,39 @@ impl<'tcx> Stack {
488
419
// We are reading from something in the unknown part. That means *all* `Unique` we know about are dead now.
489
420
0
490
421
} ;
491
- for idx in ( first_incompatible_idx..self . borrows . len ( ) ) . rev ( ) {
492
- let item = & mut self . borrows [ idx] ;
493
-
494
- if item. perm == Permission :: Unique {
495
- trace ! ( "access: disabling item {:?}" , item) ;
496
- Stack :: item_popped (
497
- item,
498
- Some ( ( tag, alloc_range, offset, access) ) ,
499
- global,
500
- alloc_history,
501
- ) ?;
502
- item. perm = Permission :: Disabled ;
503
- alloc_history. log_invalidation ( item. tag , alloc_range, current_span) ;
504
- }
505
- }
422
+ self . disable_uniques_starting_at ( first_incompatible_idx, |item| {
423
+ Stack :: item_popped (
424
+ & item,
425
+ Some ( ( tag, alloc_range, offset, access) ) ,
426
+ global,
427
+ alloc_history,
428
+ ) ?;
429
+ alloc_history. log_invalidation ( item. tag , alloc_range, current_span) ;
430
+ Ok ( ( ) )
431
+ } ) ?;
506
432
}
507
433
508
434
// If this was an approximate action, we now collapse everything into an unknown.
509
435
if granting_idx. is_none ( ) || matches ! ( tag, SbTagExtra :: Wildcard ) {
510
436
// Compute the upper bound of the items that remain.
511
437
// (This is why we did all the work above: to reduce the items we have to consider here.)
512
438
let mut max = NonZeroU64 :: new ( 1 ) . unwrap ( ) ;
513
- for item in & self . borrows {
439
+ for i in 0 ..self . len ( ) {
440
+ let item = self . get ( i) . unwrap ( ) ;
514
441
// Skip disabled items, they cannot be matched anyway.
515
442
if !matches ! ( item. perm, Permission :: Disabled ) {
516
443
// We are looking for a strict upper bound, so add 1 to this tag.
517
444
max = cmp:: max ( item. tag . 0 . checked_add ( 1 ) . unwrap ( ) , max) ;
518
445
}
519
446
}
520
- if let Some ( unk) = self . unknown_bottom {
447
+ if let Some ( unk) = self . unknown_bottom ( ) {
521
448
max = cmp:: max ( unk. 0 , max) ;
522
449
}
523
450
// Use `max` as new strict upper bound for everything.
524
451
trace ! (
525
452
"access: forgetting stack to upper bound {max} due to wildcard or unknown access"
526
453
) ;
527
- self . borrows . clear ( ) ;
528
- self . unknown_bottom = Some ( SbTag ( max) ) ;
454
+ self . set_unknown_bottom ( SbTag ( max) ) ;
529
455
}
530
456
531
457
// Done.
@@ -553,8 +479,9 @@ impl<'tcx> Stack {
553
479
)
554
480
} ) ?;
555
481
556
- // Step 2: Remove all items. Also checks for protectors.
557
- for item in self . borrows . drain ( ..) . rev ( ) {
482
+ // Step 2: Consider all items removed. This checks for protectors.
483
+ for idx in ( 0 ..self . len ( ) ) . rev ( ) {
484
+ let item = self . get ( idx) . unwrap ( ) ;
558
485
Stack :: item_popped ( & item, None , global, alloc_history) ?;
559
486
}
560
487
Ok ( ( ) )
@@ -602,8 +529,7 @@ impl<'tcx> Stack {
602
529
// The new thing is SRW anyway, so we cannot push it "on top of the unkown part"
603
530
// (for all we know, it might join an SRW group inside the unknown).
604
531
trace ! ( "reborrow: forgetting stack entirely due to SharedReadWrite reborrow from wildcard or unknown" ) ;
605
- self . borrows . clear ( ) ;
606
- self . unknown_bottom = Some ( global. next_ptr_tag ) ;
532
+ self . set_unknown_bottom ( global. next_ptr_tag ) ;
607
533
return Ok ( ( ) ) ;
608
534
} ;
609
535
@@ -630,19 +556,18 @@ impl<'tcx> Stack {
630
556
// on top of `derived_from`, and we want the new item at the top so that we
631
557
// get the strongest possible guarantees.
632
558
// This ensures U1 and F1.
633
- self . borrows . len ( )
559
+ self . len ( )
634
560
} ;
635
561
636
562
// Put the new item there. As an optimization, deduplicate if it is equal to one of its new neighbors.
637
563
// `new_idx` might be 0 if we just cleared the entire stack.
638
- if self . borrows . get ( new_idx) == Some ( & new)
639
- || ( new_idx > 0 && self . borrows [ new_idx - 1 ] == new)
564
+ if self . get ( new_idx) == Some ( new) || ( new_idx > 0 && self . get ( new_idx - 1 ) . unwrap ( ) == new)
640
565
{
641
566
// Optimization applies, done.
642
567
trace ! ( "reborrow: avoiding adding redundant item {:?}" , new) ;
643
568
} else {
644
569
trace ! ( "reborrow: adding item {:?}" , new) ;
645
- self . borrows . insert ( new_idx, new) ;
570
+ self . insert ( new_idx, new) ;
646
571
}
647
572
Ok ( ( ) )
648
573
}
@@ -654,7 +579,7 @@ impl<'tcx> Stacks {
654
579
/// Creates new stack with initial tag.
655
580
fn new ( size : Size , perm : Permission , tag : SbTag ) -> Self {
656
581
let item = Item { perm, tag, protector : None } ;
657
- let stack = Stack { borrows : vec ! [ item ] , unknown_bottom : None } ;
582
+ let stack = Stack :: new ( item ) ;
658
583
659
584
Stacks {
660
585
stacks : RangeMap :: new ( size, stack) ,
0 commit comments