You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Auto merge of rust-lang#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 rust-lang#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`.
error: Undefined Behavior: reborrow through <TAG> at ALLOC[0x0] is forbidden
2
+
--> $DIR/protector-write-lazy.rs:LL:CC
3
+
|
4
+
LL | unsafe { println!("Value of funky: {}", *funky_ptr_lazy_on_fst_elem) }
5
+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^ reborrow through <TAG> at ALLOC[0x0] is forbidden
6
+
|
7
+
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
8
+
= help: the accessed tag <TAG> has state Disabled which forbids this reborrow (acting as a child read access)
9
+
help: the accessed tag <TAG> was created here, in the initial state Reserved
10
+
--> $DIR/protector-write-lazy.rs:LL:CC
11
+
|
12
+
LL | unsafe { (&mut *(ptr_to_vec.wrapping_add(1))) as *mut i32 }.wrapping_sub(1);
13
+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
14
+
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
15
+
--> $DIR/protector-write-lazy.rs:LL:CC
16
+
|
17
+
LL | }
18
+
| ^
19
+
= help: this transition corresponds to a loss of read and write permissions
20
+
= note: BACKTRACE (of the first span):
21
+
= note: inside `main` at $DIR/protector-write-lazy.rs:LL:CC
22
+
= 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)
23
+
24
+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
0 commit comments