From be5f6b24d26a61845dfeedda2f49da15f99d6a56 Mon Sep 17 00:00:00 2001
From: Neven Villani <vanille@crans.org>
Date: Sat, 10 Jun 2023 14:50:59 +0200
Subject: [PATCH] box_exclusive_violation

---
 .../box_exclusive_violation1.rs               |  7 +++-
 .../box_exclusive_violation1.stack.stderr}    |  0
 .../box_exclusive_violation1.tree.stderr      | 42 +++++++++++++++++++
 3 files changed, 48 insertions(+), 1 deletion(-)
 rename src/tools/miri/tests/fail/{stacked_borrows => both_borrows}/box_exclusive_violation1.rs (70%)
 rename src/tools/miri/tests/fail/{stacked_borrows/box_exclusive_violation1.stderr => both_borrows/box_exclusive_violation1.stack.stderr} (100%)
 create mode 100644 src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.tree.stderr

diff --git a/src/tools/miri/tests/fail/stacked_borrows/box_exclusive_violation1.rs b/src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.rs
similarity index 70%
rename from src/tools/miri/tests/fail/stacked_borrows/box_exclusive_violation1.rs
rename to src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.rs
index 87a6b7bbd67ec..4936c1a901821 100644
--- a/src/tools/miri/tests/fail/stacked_borrows/box_exclusive_violation1.rs
+++ b/src/tools/miri/tests/fail/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/src/tools/miri/tests/fail/stacked_borrows/box_exclusive_violation1.stderr b/src/tools/miri/tests/fail/both_borrows/box_exclusive_violation1.stack.stderr
similarity index 100%
rename from src/tools/miri/tests/fail/stacked_borrows/box_exclusive_violation1.stderr
rename to src/tools/miri/tests/fail/both_borrows/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
new file mode 100644
index 0000000000000..97f82db6fe732
--- /dev/null
+++ 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
+