Skip to content

Commit 7842335

Browse files
authored
Merge pull request #718 from RalfJung/stacked-borrows-2
SharedReadOnly reborrows are never weak
2 parents 048ce3c + 17643af commit 7842335

File tree

1 file changed

+4
-1
lines changed

1 file changed

+4
-1
lines changed

src/stacked_borrows.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -400,6 +400,9 @@ impl<'tcx> Stack {
400400
// Either way, we ensure that we insert the new item in a way that between
401401
// `derived_from` and the new one, there are only items *compatible with* `derived_from`.
402402
let new_idx = if weak {
403+
// A weak SharedReadOnly reborrow might be added below other items, violating the
404+
// invariant that only SharedReadOnly can sit on top of SharedReadOnly.
405+
assert!(new.perm != Permission::SharedReadOnly, "Weak SharedReadOnly reborrows don't work");
403406
// A very liberal reborrow because the new pointer does not expect any kind of aliasing guarantee.
404407
// Just insert new permission as child of old permission, and maintain everything else.
405408
// This inserts "as far down as possible", which is good because it makes this pointer as
@@ -581,8 +584,8 @@ trait EvalContextPrivExt<'a, 'mir, 'tcx: 'a+'mir>: crate::MiriEvalContextExt<'a,
581584
// We need a frozen-sensitive reborrow.
582585
return this.visit_freeze_sensitive(place, size, |cur_ptr, size, frozen| {
583586
// We are only ever `SharedReadOnly` inside the frozen bits.
584-
let weak = !frozen || kind != RefKind::Shared; // `RefKind::Raw` is always weak, as is `SharedReadWrite`.
585587
let perm = if frozen { Permission::SharedReadOnly } else { Permission::SharedReadWrite };
588+
let weak = perm == Permission::SharedReadWrite;
586589
let item = Item { perm, tag: new_tag, protector };
587590
alloc.extra.for_each(cur_ptr, size, |stack, global| {
588591
stack.reborrow(cur_ptr.tag, force_weak || weak, item, global)

0 commit comments

Comments
 (0)