-
Notifications
You must be signed in to change notification settings - Fork 58
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Stacked Borrows does not support &UnsafeCell pointing to read-only data #303
Comments
Hm, yeah that seems like a fair point. Current Stacked Borrows cannot really handle this case -- it considers just the type of the pointer (roughly This is a fundamental problem with Stacked Borrows, not its implementation in Miri, so I moved the issue. Thanks for bringing this up! |
As mentioned in #314 , we have also run into this issue in Tock. Our original solution was basically casting One suggested alternative is to transmute the initialized memory we recieve to However, this does seem like at-best an abuse of |
This characterization in terms of not being "fixed" is not accurate. Your link mentioned this comes from the documentation for Read this: "What The Hardware Does" is not What Your Program Does: Uninitialized Memory Strictly speaking, it's not that the bytes can change values when you read them multiple times. On the contrary, from the abstract machine's perspective, reading a byte of uninitialized memory always gives you the same value. It's just that that byte value is not a number from 0 to 255, but instead a special value called "uninitialized". (From LLVM's perspective, this is represented by either The only effect of However, I don't know why Miri treats it differently. |
Thank you for the guidance; it is really helpful! Our miri issue that we are trying to fix is related to transmuting The question now though is if we are breaking aliasing rules by using The data that |
Yes, you are. I don't know why Miri no longer complains after that change; without a small example there are just too many variables here. But adding a |
Cell does not ensure that each read is a fresh read. For that you'd need some sort of volatile based abstraction. |
When fixing this we have to be careful not to accept this program -- it segfaults at runtime, so we better make sure it does have UB. |
Tree Borrows fixes this issue. |
Very exciting! |
Is there any practical use for these conversions? I'm not sure :) But they're spiritually similar to the Cell::from_mut conversion in the standard library. This makes it possible to write a function taking `&ReadOnlyCell<T>` if you only need to copy the `T` and you don't need the guarantee that it won't change from one read to the next (which it could, if other `&Cell<T>` references exist pointing to the same value). With these conversions in place, the relationships between the different reference types look like this: ``` &mut T / \ coerce Cell::from_mut / \ &T &Cell<T> \ / ReadOnlyCell::from_ref ReadOnlyCell::from_cell \ / &ReadOnlyCell<T> ``` This sort of thing wasn't supported by Miri until recently, but the new Tree Borrows model supports it: rust-lang/unsafe-code-guidelines#303. The new test currently fails Miri by default: ``` $ cargo +nightly miri test test_read_only_cell_conversions ... error: Undefined Behavior: trying to retag from <747397> for SharedReadWrite permission at alloc222352[0x0], but that tag only grants SharedReadOnly permission for this location ``` But it passes with `-Zmiri-tree-borrows`: ``` $ MIRIFLAGS="-Zmiri-tree-borrows" cargo +nightly miri test test_read_only_cell_conversions ... test buffer::tests::test_read_only_cell_conversions ... ok ```
Is there any practical use for these conversions? I'm not sure :) But they're spiritually similar to the `Cell::from_mut` conversion in the standard library. This makes it possible to write a function taking `&ReadOnlyCell<T>` if you only need to copy the `T` and you don't need the guarantee that it won't change from one read to the next (which it could, if other `&Cell<T>` references exist pointing to the same value). With these conversions in place, the relationships between the different reference types look like this: ``` &mut T / \ coerce Cell::from_mut / \ &T &Cell<T> \ / ReadOnlyCell::from_ref ReadOnlyCell::from_cell \ / &ReadOnlyCell<T> ``` This sort of thing wasn't supported by Miri until recently, but the new Tree Borrows model supports it: rust-lang/unsafe-code-guidelines#303. The new test currently fails Miri by default: ``` $ cargo +nightly miri test test_read_only_cell_conversions ... error: Undefined Behavior: trying to retag from <747397> for SharedReadWrite permission at alloc222352[0x0], but that tag only grants SharedReadOnly permission for this location ``` But it passes with `-Zmiri-tree-borrows`: ``` $ MIRIFLAGS="-Zmiri-tree-borrows" cargo +nightly miri test test_read_only_cell_conversions ... test buffer::tests::test_read_only_cell_conversions ... ok ```
I'm playing with the idea of a
ReadOnlyCell<T>
type, like aCell<T>
that only supports reading. The (kind of academic) goal of this type is to allow conversions from either&T
or&Cell<T>
into&ReadOnlyCell<T>
, similar to howCell::from_mut
converts from&mut T
to&Cell<T>
. Here's the example code (playground link):This fails Miri:
It seems like Miri is telling me that converting
&T
to&UnsafeCell<T>
is inherently UB. That's surprising to me. Obviously writing to thatUnsafeCell
would be UB. But here all I think I'm doing is telling the compiler not to treat the pointer asnoalias
, which is sort of like converting&T
to*const T
, which is legal. Am I thinking about this the right way?The text was updated successfully, but these errors were encountered: