@@ -640,13 +640,18 @@ impl<'tcx> Tree {
640640 // Register new_tag as a child of parent_tag
641641 self . nodes . get_mut ( parent_idx) . unwrap ( ) . children . push ( idx) ;
642642
643- // We need to know the biggest SIFA for `update_last_accessed_after_retag` below .
644- let mut max_sifa = default_strongest_idempotent;
643+ // We need to know the weakest SIFA for `update_idempotent_foreign_access_after_retag` .
644+ let mut min_sifa = default_strongest_idempotent;
645645 for ( Range { start, end } , & perm) in
646646 inside_perms. iter ( Size :: from_bytes ( 0 ) , inside_perms. size ( ) )
647647 {
648648 assert ! ( perm. permission. is_initial( ) ) ;
649- max_sifa = cmp:: max ( max_sifa, perm. idempotent_foreign_access ) ;
649+ assert_eq ! (
650+ perm. idempotent_foreign_access,
651+ perm. permission. strongest_idempotent_foreign_access( protected)
652+ ) ;
653+
654+ min_sifa = cmp:: min ( min_sifa, perm. idempotent_foreign_access ) ;
650655 for ( _perms_range, perms) in self
651656 . rperms
652657 . iter_mut ( Size :: from_bytes ( start) + base_offset, Size :: from_bytes ( end - start) )
@@ -656,22 +661,28 @@ impl<'tcx> Tree {
656661 }
657662
658663 // Inserting the new perms might have broken the SIFA invariant (see
659- // `foreign_access_skipping.rs`). We now weaken the recorded SIFA for our parents, until the
660- // invariant is restored. We could weaken them all to `LocalAccess`, but it is more
661- // efficient to compute the SIFA for the new permission statically, and use that. For this
662- // we need the *maximum* SIFA (`Write` needs more fixup than `None`).
663- self . update_last_accessed_after_retag ( parent_idx, max_sifa) ;
664+ // `foreign_access_skipping.rs`) if the SIFA we inserted is weaker than that of some parent.
665+ // We now weaken the recorded SIFA for our parents, until the invariant is restored. We
666+ // could weaken them all to `None`, but it is more efficient to compute the SIFA for the new
667+ // permission statically, and use that. For this we need the *minimum* SIFA (`None` needs
668+ // more fixup than `Write`).
669+ self . update_idempotent_foreign_access_after_retag ( parent_idx, min_sifa) ;
664670
665671 interp_ok ( ( ) )
666672 }
667673
668- /// Restores the SIFA "children are stronger" invariant after a retag.
669- /// See `foreign_access_skipping` and `new_child`.
670- fn update_last_accessed_after_retag (
674+ /// Restores the SIFA "children are stronger"/"parents are weaker" invariant after a retag:
675+ /// reduce the SIFA of `current` and its parents to be no stronger than `strongest_allowed`.
676+ /// See `foreign_access_skipping.rs` and [`Tree::new_child`].
677+ fn update_idempotent_foreign_access_after_retag (
671678 & mut self ,
672679 mut current : UniIndex ,
673680 strongest_allowed : IdempotentForeignAccess ,
674681 ) {
682+ if strongest_allowed == IdempotentForeignAccess :: Write {
683+ // Nothing is stronger than `Write`.
684+ return ;
685+ }
675686 // We walk the tree upwards, until the invariant is restored
676687 loop {
677688 let current_node = self . nodes . get_mut ( current) . unwrap ( ) ;
0 commit comments