Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
22364f8
This pattern using lazy protected Reserved IM prevents spurious writes
Vanille-N Jul 9, 2024
2de6e7f
Implement fix for reservedim_spurious_write: ignore IM on protected
Vanille-N Jul 9, 2024
22996ad
Apply suggestions
Vanille-N Jul 9, 2024
68aed4a
Second byte is not involved in the example; use a Cell<()> instead
Vanille-N Jul 10, 2024
78f6386
Clarify comment in tests/fail/tree_borrows/reservedim_spurious_write.rs
Vanille-N Jul 12, 2024
fd81880
Leave a trace of the current suboptimal status of foreign_write
Vanille-N Jul 12, 2024
e1e5b8a
Preparing for merge from rustc
Jul 16, 2024
547ade5
Merge from rustc
Jul 16, 2024
451035f
Auto merge of #3751 - rust-lang:rustup-2024-07-16, r=RalfJung
bors Jul 16, 2024
b3736d6
Auto merge of #3742 - Vanille-N:master, r=RalfJung
bors Jul 16, 2024
e5544dc
Preparing for merge from rustc
Jul 20, 2024
424d79c
Merge from rustc
Jul 20, 2024
0c1448d
Auto merge of #3755 - rust-lang:rustup-2024-07-20, r=RalfJung
bors Jul 20, 2024
69b9eab
Add `O_NOFOLLOW` flag support
newpavlov Jul 22, 2024
06a14f1
Fix test
newpavlov Jul 22, 2024
fc8af31
Auto merge of #3744 - newpavlov:nofollow, r=RalfJung
bors Jul 22, 2024
56d672e
Add `pread` and `pwrite` shims
newpavlov Jul 22, 2024
b7b2305
Auto merge of #3743 - newpavlov:pread_pwrite, r=RalfJung
bors Jul 22, 2024
c646256
Preparing for merge from rustc
Jul 24, 2024
675a5ba
Merge from rustc
Jul 24, 2024
0b22f0c
Auto merge of #3761 - rust-lang:rustup-2024-07-24, r=RalfJung
bors Jul 24, 2024
a0088d7
Allow getpid in isolation mode, add gettid support
Mandragorian Jul 20, 2024
12cb742
Auto merge of #3756 - Mandragorian:gettid_support, r=RalfJung
bors Jul 24, 2024
c45f464
show warning when Stacked Borrows skips a reborrow due to 'extern type'
RalfJung Jun 22, 2024
f1ae48c
Auto merge of #3701 - RalfJung:extern-type-reborrow, r=saethlin
bors Jul 24, 2024
6da04f9
Preparing for merge from rustc
Jul 25, 2024
4a26aa4
Merge from rustc
Jul 25, 2024
35e70f3
Auto merge of #3762 - rust-lang:rustup-2024-07-25, r=saethlin
bors Jul 25, 2024
b549035
Preparing for merge from rustc
Jul 26, 2024
4bd2757
Merge from rustc
Jul 26, 2024
f98fdfc
Auto merge of #3765 - rust-lang:rustup-2024-07-26, r=RalfJung
bors Jul 26, 2024
7bc7e67
better diagnostics for Tree Borrows + int2ptr casts
RalfJung Jul 26, 2024
5e1f8e2
diagnostics: add a macro to make things a bit easier to read
RalfJung Jul 26, 2024
bf4d4c0
Auto merge of #3766 - RalfJung:tree-borrows-int2ptr, r=RalfJung
bors Jul 26, 2024
a52b1d6
Let insert_fd takes in FileDescription instead of FileDescriptor
tiif Jul 26, 2024
adbb89e
Auto merge of #3763 - tiif:global-fd-id, r=oli-obk
bors Jul 26, 2024
80a32f8
Preparing for merge from rustc
Jul 27, 2024
00e89d3
Merge from rustc
Jul 27, 2024
822286f
fix clippy
RalfJung Jul 27, 2024
a6796c1
Auto merge of #3768 - rust-lang:rustup-2024-07-27, r=RalfJung
bors Jul 27, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Implement fix for reservedim_spurious_write: ignore IM on protected
  • Loading branch information
Vanille-N committed Jul 9, 2024
commit 2de6e7f3a680a8000f83f2b62252d18a1bb06966
10 changes: 8 additions & 2 deletions src/tools/miri/src/borrow_tracker/tree_borrows/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -141,8 +141,14 @@ impl<'tcx> NewPermission {
) -> Option<Self> {
let ty_is_freeze = pointee.is_freeze(*cx.tcx, cx.param_env());
let ty_is_unpin = pointee.is_unpin(*cx.tcx, cx.param_env());
let is_protected = kind == RetagKind::FnEntry;
// As demonstrated by `tests/fail/tree_borrows/reservedim_spurious_write.rs`,
// interior mutability and protectors interact poorly.
// To eliminate the case of Protected Reserved IM we override interior mutability
// in the case of a protected reference.
let initial_state = match mutability {
Mutability::Mut if ty_is_unpin => Permission::new_reserved(ty_is_freeze),
Mutability::Mut if ty_is_unpin =>
Permission::new_reserved(ty_is_freeze || is_protected),
Mutability::Not if ty_is_freeze => Permission::new_frozen(),
// Raw pointers never enter this function so they are not handled.
// However raw pointers are not the only pointers that take the parent
Expand All @@ -151,7 +157,7 @@ impl<'tcx> NewPermission {
_ => return None,
};

let protector = (kind == RetagKind::FnEntry).then_some(ProtectorKind::StrongProtector);
let protector = is_protected.then_some(ProtectorKind::StrongProtector);
Some(Self { zero_size: false, initial_state, protector })
}

Expand Down
5 changes: 5 additions & 0 deletions src/tools/miri/src/borrow_tracker/tree_borrows/perms.rs
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,11 @@ enum PermissionPriv {
/// - foreign-read then child-write is UB due to `conflicted`,
/// - child-write then foreign-read is UB since child-write will activate and then
/// foreign-read disables a protected `Active`, which is UB.
///
/// Note: since the discovery of `tests/fail/tree_borrows/reservedim_spurious_write.rs`,
/// `ty_is_freeze` does not strictly mean that the type has no interior mutability,
/// it could be an interior mutable type that lost its interior mutability privileges
/// when retagged with a protector.
Reserved { ty_is_freeze: bool, conflicted: bool },
/// represents: a unique pointer;
/// allows: child reads, child writes;
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Warning: this tree is indicative only. Some tags may have been hidden.
| RsM | └─┬──<TAG=base>
| RsM | ├─┬──<TAG=x>
| RsM | │ └─┬──<TAG=caller:x>
| RsM | │ └────<TAG=callee:x> Strongly protected
| Rs | │ └────<TAG=callee:x> Strongly protected
| RsM | └────<TAG=y, callee:y, caller:y>
──────────────────────────────────────────────────
error: Undefined Behavior: write access through <TAG> (y, callee:y, caller:y) at ALLOC[0x0] is forbidden
Expand All @@ -16,14 +16,14 @@ LL | *y = 1;
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
= help: the accessed tag <TAG> (y, callee:y, caller:y) is foreign to the protected tag <TAG> (callee:x) (i.e., it is not a child)
= help: this foreign write access would cause the protected tag <TAG> (callee:x) (currently Reserved (interior mutable)) to become Disabled
= help: this foreign write access would cause the protected tag <TAG> (callee:x) (currently Reserved) to become Disabled
= help: protected tags must never be Disabled
help: the accessed tag <TAG> was created here
--> $DIR/cell-protected-write.rs:LL:CC
|
LL | let y = (&mut *n).get();
| ^^^^^^^^^
help: the protected tag <TAG> was created here, in the initial state Reserved (interior mutable)
help: the protected tag <TAG> was created here, in the initial state Reserved
--> $DIR/cell-protected-write.rs:LL:CC
|
LL | unsafe fn write_second(x: &mut UnsafeCell<u8>, y: *mut u8) {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -100,7 +100,7 @@ fn example(spurious: bool) {
let y = inner(unsafe { &mut *(ptr.0 as *mut Cell<u8>).wrapping_add(1) }, b.clone());
synchronized!(b, "ret x");
synchronized!(b, "write y");
unsafe { *y.wrapping_sub(1) = 13 }
unsafe { *y.wrapping_sub(1) = 13 } //~ERROR: /write access through .* is forbidden/
synchronized!(b, "end");
});

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,41 @@
Without spurious write
Thread 1 executing: start
Thread 2 executing: start
Thread 2 executing: retag x (&mut, protect)
Thread 1 executing: retag x (&mut, protect)
Thread 1 executing: [lazy] retag y (&mut, protect, IM)
Thread 2 executing: [lazy] retag y (&mut, protect, IM)
Thread 2 executing: spurious write x
Thread 1 executing: spurious write x (skipped)
Thread 1 executing: ret y
Thread 2 executing: ret y
Thread 2 executing: ret x
Thread 1 executing: ret x
Thread 1 executing: write y
Thread 2 executing: write y
error: Undefined Behavior: write access through <TAG> at ALLOC[0x0] is forbidden
--> $DIR/reservedim_spurious_write.rs:LL:CC
|
LL | unsafe { *y.wrapping_sub(1) = 13 }
| ^^^^^^^^^^^^^^^^^^^^^^^ write access through <TAG> at ALLOC[0x0] is forbidden
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
= help: the accessed tag <TAG> has state Disabled which forbids this child write access
help: the accessed tag <TAG> was created here, in the initial state Reserved
--> $DIR/reservedim_spurious_write.rs:LL:CC
|
LL | fn inner(y: &mut Cell<u8>, b: IdxBarrier) -> *mut u8 {
| ^
help: the accessed tag <TAG> later transitioned to Disabled due to a protector release (acting as a foreign write access) on every location previously accessed by this tag
--> $DIR/reservedim_spurious_write.rs:LL:CC
|
LL | }
| ^
= help: this transition corresponds to a loss of read and write permissions
= note: BACKTRACE (of the first span) on thread `unnamed-ID`:
= note: inside closure at $DIR/reservedim_spurious_write.rs:LL:CC

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

error: aborting due to 1 previous error

2 changes: 1 addition & 1 deletion src/tools/miri/tests/pass/tree_borrows/reserved.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ Warning: this tree is indicative only. Some tags may have been hidden.
| RsM | └─┬──<TAG=base>
| RsM | ├─┬──<TAG=x>
| RsM | │ └─┬──<TAG=caller:x>
| RsCM| │ └────<TAG=callee:x>
| RsC | │ └────<TAG=callee:x>
| RsM | └────<TAG=y, caller:y, callee:y>
──────────────────────────────────────────────────
[interior mut] Foreign Read: Re* -> Re*
Expand Down