Closed wvwwvwwv closed 4 weeks ago
SDD 1.3.0 enabled SCC to enable a number of MIRI test cases. Still, a long way to go.
while the code is not as dangerous as
Miri
thinks it is
I'm worried you're underestimating how accurate Miri's UB detection is. The UB warned about in the following diagnostic is currently used for optimizations. We have a MIR optimization that explicitly reasons based on it, and rustc tells LLVM about the requirement here with the combination of noalias
and readonly
.
error: Undefined Behavior: attempting a write access using <3690> at alloc1139[0x8], but that tag only grants SharedReadOnly permission for this location
--> /build/src/bag.rs:428:33
|
428 | ... (self.storage[index].as_ptr().cast_mut()).write(val);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
| |
| attempting a write access using <3690> at alloc1139[0x8], but that tag only grants SharedReadOnly permission for this location
| this error occurs as part of an access at alloc1139[0x8..0x10]
|
= 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
help: <3690> was created by a SharedReadOnly retag at offsets [0x8..0x10]
--> /build/src/bag.rs:428:34
|
428 | ... (self.storage[index].as_ptr().cast_mut()).write(val);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= note: BACKTRACE (of the first span):
= note: inside `scc::bag::Storage::<usize, 32>::push` at /build/src/bag.rs:428:33: 428:85
note: inside `scc::Bag::<usize, 32>::push`
--> /build/src/bag.rs:102:28
|
102 | if let Some(val) = self.primary_storage.push(val, true) {
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
note: inside `main::_doctest_main_src_bag_rs_217_0`
--> src/bag.rs:224:1
|
10 | bag.push(7);
| ^^^^^^^^^^^
note: inside `main`
--> src/bag.rs:229:3
|
15 | } _doctest_main_src_bag_rs_217_0() }
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
In fact as far as I can tell, all of the UB diagnostics in this crate and in SDD are for scenarios where rustc explicitly permit LLVM to make optimizations that break this crate. Most of the rest of the diagnostics are about protectors, which is how Miri models the meaning of the LLVM attribute dereferenceable
.
I'll see if I can contribute some PRs to address some of the Miri diagnostics that I find most concerning.
@saethlin Super thanks! I agree that I may have underestimated MIRI's ability to detect UB. Really appreciate your comment, and I'll also look into those errors soon!
You may be interested in setting MIRIFLAGS=-Zmiri-tree-borrows
, which opts into a much more complicated but generally more permissive aliasing model. There's a manual for the model here: https://perso.crans.org/vanille/treebor/
Fixed most MIRI errors in bag.
Fixes all the Miri errors in bin/doc tests; had to deactivate async/multi-threaded tests due to the test run-time and tokio dependencies.
The current
EBR
code is not quite friendly toMiri
while the code is not as dangerous asMiri
thinks it is. Need to make the code more friendly toMiri
.