Auto merge of #2922 - Vanille-N:tb-tests, r=RalfJung

TB: `box_exclusive_violation1` moved to `both_borrows` `box_noalias_violation` was already shared, it makes sense to test `box_exclusive_violation` with TB too.
rust-lang · Jun 11, 2023 · 85533a3 · 85533a3
2 parents 634c21f + be5f6b2
commit 85533a3
Show file tree

Hide file tree

Showing 3 changed files with 48 additions and 1 deletion.
diff --git a/...acked_borrows/box_exclusive_violation1.rs → .../both_borrows/box_exclusive_violation1.rs b/...acked_borrows/box_exclusive_violation1.rs → .../both_borrows/box_exclusive_violation1.rs
@@ -1,3 +1,6 @@
+//@revisions: stack tree
+//@[tree]compile-flags: -Zmiri-tree-borrows
+
 fn demo_box_advanced_unique(mut our: Box<i32>) -> i32 {
     unknown_code_1(&*our);
 
@@ -24,7 +27,9 @@ fn unknown_code_1(x: &i32) {
 
 fn unknown_code_2() {
     unsafe {
-        *LEAK = 7; //~ ERROR: /write access .* tag does not exist in the borrow stack/
+        *LEAK = 7;
+        //~[stack]^ ERROR: /write access .* tag does not exist in the borrow stack/
+        //~[tree]| ERROR: /write access through .* is forbidden/
     }
 }
 

diff --git a/...d_borrows/box_exclusive_violation1.stderr → ...ows/box_exclusive_violation1.stack.stderr b/...d_borrows/box_exclusive_violation1.stderr → ...ows/box_exclusive_violation1.stack.stderr
diff --git a/src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.tree.stderr b/src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.tree.stderr
@@ -0,0 +1,42 @@
+error: Undefined Behavior: write access through <TAG> is forbidden
+  --> $DIR/box_exclusive_violation1.rs:LL:CC
+   |
+LL |         *LEAK = 7;
+   |         ^^^^^^^^^ write access through <TAG> 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> is a child of the conflicting tag <TAG>
+   = help: the conflicting tag <TAG> has state Disabled which forbids this child write access
+help: the accessed tag <TAG> was created here
+  --> $DIR/box_exclusive_violation1.rs:LL:CC
+   |
+LL | fn unknown_code_1(x: &i32) {
+   |                   ^
+help: the conflicting tag <TAG> was created here, in the initial state Frozen
+  --> $DIR/box_exclusive_violation1.rs:LL:CC
+   |
+LL |     unknown_code_1(&*our);
+   |                    ^^^^^
+help: the conflicting tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x4]
+  --> $DIR/box_exclusive_violation1.rs:LL:CC
+   |
+LL |     *our = 5;
+   |     ^^^^^^^^
+   = help: this transition corresponds to a loss of read permissions
+   = note: BACKTRACE (of the first span):
+   = note: inside `unknown_code_2` at $DIR/box_exclusive_violation1.rs:LL:CC
+note: inside `demo_box_advanced_unique`
+  --> $DIR/box_exclusive_violation1.rs:LL:CC
+   |
+LL |     unknown_code_2();
+   |     ^^^^^^^^^^^^^^^^
+note: inside `main`
+  --> $DIR/box_exclusive_violation1.rs:LL:CC
+   |
+LL |     demo_box_advanced_unique(Box::new(0));
+   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+