Auto merge of #2489 - RalfJung:srw-merging, r=saethlin

add test that we do not merge neighboring SRW

Turns out that interior_mut2 also already tests this, but that also involves `UnsafeCell` so the new test still seems more clear. Basically the new test is the same as the old except that it uses raw pointers rather than `&UnsafeCell`. (When the old test was written, raw pointers were still untagged, so no such test would have been possible.)

I verified that both of these fail when we remove mutable references rather than disabling them.
Here is the patch I used for that:

<details>

```diff
diff --git a/Cargo.toml b/Cargo.toml
index 208b3a76..f9d1b0ac 100644
--- a/Cargo.toml
+++ b/Cargo.toml
`@@` -53,7 +53,7 `@@` name = "compiletest"
 harness = false

 [features]
-default = ["stack-cache"]
+default = []
 stack-cache = []

 # Be aware that this file is inside a workspace when used via the
diff --git a/src/lib.rs b/src/lib.rs
index ba337f28..2a3066f4 100644
--- a/src/lib.rs
+++ b/src/lib.rs
`@@` -9,6 +9,7 `@@`
 #![feature(is_some_with)]
 #![feature(nonzero_ops)]
 #![feature(local_key_cell_methods)]
+#![feature(drain_filter)]
 // Configure clippy and other lints
 #![allow(
     clippy::collapsible_else_if,
diff --git a/src/stacked_borrows/stack.rs b/src/stacked_borrows/stack.rs
index 4a9a13d3..37246df7 100644
--- a/src/stacked_borrows/stack.rs
+++ b/src/stacked_borrows/stack.rs
`@@` -351,6 +351,9 `@@` impl<'tcx> Stack {
         #[cfg(all(feature = "stack-cache", debug_assertions))]
         self.verify_cache_consistency();

+        // HACK -- now just delete all disabled things.
+        self.borrows.drain_filter(|b| matches!(b.perm(), Permission::Disabled));
+
         Ok(())
     }
```

</details>

r? `@saethlin`
This commit is contained in:
bors 2022-08-16 11:54:55 +00:00
commit 793f198b9d
4 changed files with 58 additions and 6 deletions

3
ci.sh
View File

@ -5,11 +5,12 @@ set -x
# Determine configuration
export RUSTFLAGS="-D warnings"
export CARGO_INCREMENTAL=0
export CARGO_EXTRA_FLAGS="--all-features"
# Prepare
echo "Build and install miri"
./miri install # implicitly locked
./miri check --no-default-features # make sure this can be built
./miri check --all-features # and this, too
./miri build --all-targets --locked # the build that all the `./miri test` below will use
echo

View File

@ -81,7 +81,7 @@ impl<'tcx> Stack {
/// Panics if any of the caching mechanisms have broken,
/// - The StackCache indices don't refer to the parallel items,
/// - There are no Unique items outside of first_unique..last_unique
#[cfg(debug_assertions)]
#[cfg(all(feature = "stack-cache", debug_assertions))]
fn verify_cache_consistency(&self) {
// Only a full cache needs to be valid. Also see the comments in find_granting_cache
// and set_unknown_bottom.
@ -128,7 +128,7 @@ pub(super) fn find_granting(
tag: ProvenanceExtra,
exposed_tags: &FxHashSet<SbTag>,
) -> Result<Option<usize>, ()> {
#[cfg(debug_assertions)]
#[cfg(all(feature = "stack-cache", debug_assertions))]
self.verify_cache_consistency();
let ProvenanceExtra::Concrete(tag) = tag else {
@ -320,13 +320,14 @@ pub fn disable_uniques_starting_at<V: FnMut(Item) -> crate::InterpResult<'tcx>>(
if disable_start <= unique_range.end {
let lower = unique_range.start.max(disable_start);
let upper = self.unique_range.end;
let upper = unique_range.end;
for item in &mut self.borrows[lower..upper] {
if item.perm() == Permission::Unique {
log::trace!("access: disabling item {:?}", item);
visitor(*item)?;
item.set_permission(Permission::Disabled);
// Also update all copies of this item in the cache.
#[cfg(feature = "stack-cache")]
for it in &mut self.cache.items {
if it.tag() == item.tag() {
it.set_permission(Permission::Disabled);
@ -347,7 +348,7 @@ pub fn disable_uniques_starting_at<V: FnMut(Item) -> crate::InterpResult<'tcx>>(
self.unique_range.end = self.unique_range.end.min(disable_start);
}
#[cfg(debug_assertions)]
#[cfg(all(feature = "stack-cache", debug_assertions))]
self.verify_cache_consistency();
Ok(())
@ -402,7 +403,7 @@ pub fn pop_items_after<V: FnMut(Item) -> crate::InterpResult<'tcx>>(
self.unique_range = 0..0;
}
#[cfg(debug_assertions)]
#[cfg(all(feature = "stack-cache", debug_assertions))]
self.verify_cache_consistency();
Ok(())
}

View File

@ -0,0 +1,22 @@
// This tests demonstrates the effect of 'Disabling' mutable references on reads, rather than
// removing them from the stack -- the latter would 'merge' neighboring SRW groups which we would
// like to avoid.
fn main() {
unsafe {
let mut mem = 0;
let base = &mut mem as *mut i32; // the base pointer we build the rest of the stack on
let raw = {
let mutref = &mut *base;
mutref as *mut i32
};
// In the stack, we now have [base, mutref, raw].
// We do this in a weird way where `mutref` is out of scope here, just in case
// Miri decides to get smart and argue that items for tags that are no longer
// used by any pointer stored anywhere in the machine can be removed.
let _val = *base;
// now mutref is disabled
*base = 1;
// this should pop raw from the stack, since it is in a different SRW group
let _val = *raw; //~ERROR: that tag does not exist in the borrow stack
}
}

View File

@ -0,0 +1,28 @@
error: Undefined Behavior: attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
--> $DIR/disable_mut_does_not_merge_srw.rs:LL:CC
|
LL | let _val = *raw;
| ^^^^
| |
| attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of an access at ALLOC[0x0..0x4]
|
= 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: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/disable_mut_does_not_merge_srw.rs:LL:CC
|
LL | mutref as *mut i32
| ^^^^^^
help: <TAG> was later invalidated at offsets [0x0..0x4]
--> $DIR/disable_mut_does_not_merge_srw.rs:LL:CC
|
LL | *base = 1;
| ^^^^^^^^^
= note: backtrace:
= note: inside `main` at $DIR/disable_mut_does_not_merge_srw.rs:LL:CC
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
error: aborting due to previous error