-
Notifications
You must be signed in to change notification settings - Fork 332
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Auto merge of #3732 - JoJoDeveloping:tree-borrows-protector-end-write…
…, r=RalfJung TB: Refine protector end semantics Tree Borrows has protector end tag semantics, namely that protectors ending cause a [special implicit read](https://perso.crans.org/vanille/treebor/diff.0.html) on all locations protected by that protector that have actually been accessed. See also #3067. While this is enough for ensuring protectors allow adding/reordering reads, it does not prove that one can reorder writes. For this, we need to make this stronger, by making this implicit read be a write in cases when there was a write to the location protected by that protector, i.e. if the permission is `Active`. There is a test that shows why this behavior is necessary, see `tests/fail/tree_borrows/protector-write-lazy.rs`.
- Loading branch information
Showing
6 changed files
with
100 additions
and
36 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,35 @@ | ||
| //@compile-flags: -Zmiri-tree-borrows | ||
| // This test tests that TB's protector end semantics correctly ensure | ||
| // that protected activated writes can be reordered. | ||
| fn the_other_function(ref_to_fst_elem: &mut i32, ptr_to_vec: *mut i32) -> *mut i32 { | ||
| // Activate the reference. Afterwards, we should be able to reorder arbitrary writes. | ||
| *ref_to_fst_elem = 0; | ||
| // Here is such an arbitrary write. | ||
| // It could be moved down after the retag, in which case the `funky_ref` would be invalidated. | ||
| // We need to ensure that the `funky_ptr` is unusable even if the write to `ref_to_fst_elem` | ||
| // happens before the retag. | ||
| *ref_to_fst_elem = 42; | ||
| // this creates a reference that is Reserved Lazy on the first element (offset 0). | ||
| // It does so by doing a proper retag on the second element (offset 1), which is fine | ||
| // since nothing else happens at that offset, but the lazy init mechanism means it's | ||
| // also reserved at offset 0, but not initialized. | ||
| let funky_ptr_lazy_on_fst_elem = | ||
| unsafe { (&mut *(ptr_to_vec.wrapping_add(1))) as *mut i32 }.wrapping_sub(1); | ||
| // If we write to `ref_to_fst_elem` here, then any further access to `funky_ptr_lazy_on_fst_elem` would | ||
| // definitely be UB. Since the compiler ought to be able to reorder the write of `42` above down to | ||
| // here, that means we want this program to also be UB. | ||
| return funky_ptr_lazy_on_fst_elem; | ||
| } | ||
|
|
||
| fn main() { | ||
| let mut v = vec![0, 1]; | ||
| // get a pointer to the root of the allocation | ||
| // note that it's not important it's the actual root, what matters is that it's a parent | ||
| // of both references that will be created | ||
| let ptr_to_vec = v.as_mut_ptr(); | ||
| let ref_to_fst_elem = unsafe { &mut *ptr_to_vec }; | ||
| let funky_ptr_lazy_on_fst_elem = the_other_function(ref_to_fst_elem, ptr_to_vec); | ||
| // now we try to use the funky lazy pointer. | ||
| // It should be UB, since the write-on-protector-end should disable it. | ||
| unsafe { println!("Value of funky: {}", *funky_ptr_lazy_on_fst_elem) } //~ ERROR: /reborrow through .* is forbidden/ | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,27 @@ | ||
| error: Undefined Behavior: reborrow through <TAG> at ALLOC[0x0] is forbidden | ||
| --> $DIR/protector-write-lazy.rs:LL:CC | ||
| | | ||
| LL | unsafe { println!("Value of funky: {}", *funky_ptr_lazy_on_fst_elem) } | ||
| | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ reborrow 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 reborrow (acting as a child read access) | ||
| help: the accessed tag <TAG> was created here, in the initial state Reserved | ||
| --> $DIR/protector-write-lazy.rs:LL:CC | ||
| | | ||
| LL | unsafe { (&mut *(ptr_to_vec.wrapping_add(1))) as *mut i32 }.wrapping_sub(1); | ||
| | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | ||
| 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/protector-write-lazy.rs:LL:CC | ||
| | | ||
| LL | } | ||
| | ^ | ||
| = help: this transition corresponds to a loss of read and write permissions | ||
| = note: BACKTRACE (of the first span): | ||
| = note: inside `main` at $DIR/protector-write-lazy.rs:LL:CC | ||
| = note: this error originates in the macro `$crate::format_args_nl` which comes from the expansion of the macro `println` (in Nightly builds, run with -Z macro-backtrace for more info) | ||
|
|
||
| note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
|
||
| error: aborting due to 1 previous error | ||
|
|