Open
Description
As of Aug 7, 2023, the unsafe list implementation in sgx waitqueue has a violation against Stacked Borrows.
Here is the playground link; executing it with miri produces an error.
......
error: Undefined Behavior: trying to retag from <1601> for SharedReadOnly permission at alloc960[0x0], but that tag does not exist in the borrow stack for this location
--> /playground/.rustup/toolchains/nightly-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/non_null.rs:377:18
|
377 | unsafe { &*self.as_ptr().cast_const() }
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| trying to retag from <1601> for SharedReadOnly permission at alloc960[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag at alloc960[0x0..0x18]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
......
I basically copy-pasted library/std/src/sys/sgx/waitqueue/unsafe_list{.rs,/tests.rs}
into the playground link. I made a few minor modifications that should not affect the result:
- Changed
use crate::ptr::NonNull
touse std::ptr::NonNull
andrtassert!(...)
toassert!(...)
- Manually invokes the
push_pop()
test inmain()
(other test cases exhibit the same error)
It looks like an actual violation to me. Because
self.head_tail
is a mutable reborrow fromself.head_tail_entry
constructed ininit()
- Later in
pop()
, the compiler retags (which is a Stacked Borrows rule) fields ofself
, invalidating any old references to its fields includingself.head_tail
. - In the
is_empty()
called bypop()
, we try to use the invalidated pointer.
The last change to unsafe_list.rs was two years ago and it's a private module only used in sys/sgx/waitqueue
, so the problem might not be that severe.
Still, I wonder whether this is a false positive of miri, or can we confirm it's a Stacked Borrows/memory-safety violation.