-
Notifications
You must be signed in to change notification settings - Fork 12.8k
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 #2887 - Vanille-N:tb-mut-transmute, r=RalfJung
TB: more fail tests (mostly shared with SB) Although it was not in the tests, `mem::transmute` works for `UnsafeCell -> &` as well. Draft: will also introduce more test cases for cases that fail. Draft: depends on the new error messages from #2888
- Loading branch information
Showing
135 changed files
with
1,641 additions
and
118 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
File renamed without changes.
32 changes: 32 additions & 0 deletions
32
src/tools/miri/tests/fail/both_borrows/alias_through_mutation.tree.stderr
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,32 @@ | ||
error: Undefined Behavior: read access through <TAG> is forbidden | ||
--> $DIR/alias_through_mutation.rs:LL:CC | ||
| | ||
LL | let _val = *target_alias; | ||
| ^^^^^^^^^^^^^ read 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 child read accesses | ||
help: the accessed tag <TAG> was created here | ||
--> $DIR/alias_through_mutation.rs:LL:CC | ||
| | ||
LL | *x = &mut *(target as *mut _); | ||
| ^^^^^^^^^^^^^^^^^^^^^^^^ | ||
help: the conflicting tag <TAG> was created here, in the initial state Reserved | ||
--> $DIR/alias_through_mutation.rs:LL:CC | ||
| | ||
LL | retarget(&mut target_alias, target); | ||
| ^^^^^^ | ||
help: the conflicting tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x4] | ||
--> $DIR/alias_through_mutation.rs:LL:CC | ||
| | ||
LL | *target = 13; | ||
| ^^^^^^^^^^^^ | ||
= help: this corresponds to a loss of read and write permissions | ||
= note: BACKTRACE (of the first span): | ||
= note: inside `main` at $DIR/alias_through_mutation.rs:LL:CC | ||
|
||
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
||
error: aborting due to previous error | ||
|
8 changes: 7 additions & 1 deletion
8
...sts/fail/stacked_borrows/aliasing_mut1.rs → .../tests/fail/both_borrows/aliasing_mut1.rs
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
31 changes: 31 additions & 0 deletions
31
src/tools/miri/tests/fail/both_borrows/aliasing_mut1.tree.stderr
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,31 @@ | ||
error: Undefined Behavior: write access through <TAG> is forbidden | ||
--> $DIR/aliasing_mut1.rs:LL:CC | ||
| | ||
LL | *x = 1; | ||
| ^^^^^^ 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> has state Frozen which forbids child write accesses | ||
help: the accessed tag <TAG> was created here, in the initial state Reserved | ||
--> $DIR/aliasing_mut1.rs:LL:CC | ||
| | ||
LL | pub fn safe(x: &mut i32, y: &mut i32) { | ||
| ^ | ||
help: the accessed tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x4] | ||
--> $DIR/aliasing_mut1.rs:LL:CC | ||
| | ||
LL | pub fn safe(x: &mut i32, y: &mut i32) { | ||
| ^ | ||
= help: this corresponds to a loss of write permissions | ||
= note: BACKTRACE (of the first span): | ||
= note: inside `safe` at $DIR/aliasing_mut1.rs:LL:CC | ||
note: inside `main` | ||
--> $DIR/aliasing_mut1.rs:LL:CC | ||
| | ||
LL | safe_raw(xraw, xraw); | ||
| ^^^^^^^^^^^^^^^^^^^^ | ||
|
||
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
||
error: aborting due to previous error | ||
|
8 changes: 7 additions & 1 deletion
8
...sts/fail/stacked_borrows/aliasing_mut2.rs → .../tests/fail/both_borrows/aliasing_mut2.rs
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
31 changes: 31 additions & 0 deletions
31
src/tools/miri/tests/fail/both_borrows/aliasing_mut2.tree.stderr
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,31 @@ | ||
error: Undefined Behavior: write access through <TAG> is forbidden | ||
--> $DIR/aliasing_mut2.rs:LL:CC | ||
| | ||
LL | *y = 2; | ||
| ^^^^^^ 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> has state Frozen which forbids child write accesses | ||
help: the accessed tag <TAG> was created here, in the initial state Reserved | ||
--> $DIR/aliasing_mut2.rs:LL:CC | ||
| | ||
LL | pub fn safe(x: &i32, y: &mut i32) { | ||
| ^ | ||
help: the accessed tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x4] | ||
--> $DIR/aliasing_mut2.rs:LL:CC | ||
| | ||
LL | let _v = *x; | ||
| ^^ | ||
= help: this corresponds to a loss of write permissions | ||
= note: BACKTRACE (of the first span): | ||
= note: inside `safe` at $DIR/aliasing_mut2.rs:LL:CC | ||
note: inside `main` | ||
--> $DIR/aliasing_mut2.rs:LL:CC | ||
| | ||
LL | safe_raw(xshr, xraw); | ||
| ^^^^^^^^^^^^^^^^^^^^ | ||
|
||
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
||
error: aborting due to previous error | ||
|
8 changes: 7 additions & 1 deletion
8
...sts/fail/stacked_borrows/aliasing_mut3.rs → .../tests/fail/both_borrows/aliasing_mut3.rs
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
10 changes: 5 additions & 5 deletions
10
...fail/stacked_borrows/aliasing_mut3.stderr → ...l/both_borrows/aliasing_mut3.stack.stderr
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
31 changes: 31 additions & 0 deletions
31
src/tools/miri/tests/fail/both_borrows/aliasing_mut3.tree.stderr
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,31 @@ | ||
error: Undefined Behavior: write access through <TAG> is forbidden | ||
--> $DIR/aliasing_mut3.rs:LL:CC | ||
| | ||
LL | *x = 1; | ||
| ^^^^^^ 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> has state Frozen which forbids child write accesses | ||
help: the accessed tag <TAG> was created here, in the initial state Reserved | ||
--> $DIR/aliasing_mut3.rs:LL:CC | ||
| | ||
LL | pub fn safe(x: &mut i32, y: &i32) { | ||
| ^ | ||
help: the accessed tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x4] | ||
--> $DIR/aliasing_mut3.rs:LL:CC | ||
| | ||
LL | pub fn safe(x: &mut i32, y: &i32) { | ||
| ^ | ||
= help: this corresponds to a loss of write permissions | ||
= note: BACKTRACE (of the first span): | ||
= note: inside `safe` at $DIR/aliasing_mut3.rs:LL:CC | ||
note: inside `main` | ||
--> $DIR/aliasing_mut3.rs:LL:CC | ||
| | ||
LL | safe_raw(xraw, xshr); | ||
| ^^^^^^^^^^^^^^^^^^^^ | ||
|
||
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
||
error: aborting due to previous error | ||
|
9 changes: 8 additions & 1 deletion
9
...sts/fail/stacked_borrows/aliasing_mut4.rs → .../tests/fail/both_borrows/aliasing_mut4.rs
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
39 changes: 39 additions & 0 deletions
39
src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr
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,39 @@ | ||
error: Undefined Behavior: write access through <TAG> is forbidden | ||
--> RUSTLIB/core/src/mem/mod.rs:LL:CC | ||
| | ||
LL | ptr::write(dest, src); | ||
| ^^^^^^^^^^^^^^^^^^^^^ 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 foreign to the protected tag <TAG> (i.e., it is not a child) | ||
= help: the access would cause the protected tag <TAG> to transition from Frozen to Disabled | ||
= help: this is a loss of read permissions, which is not allowed for protected tags | ||
help: the accessed tag <TAG> was created here | ||
--> $DIR/aliasing_mut4.rs:LL:CC | ||
| | ||
LL | y.set(1); | ||
| ^^^^^^^^ | ||
help: the protected tag <TAG> was created here, in the initial state Frozen | ||
--> $DIR/aliasing_mut4.rs:LL:CC | ||
| | ||
LL | pub fn safe(x: &i32, y: &mut Cell<i32>) { | ||
| ^ | ||
= note: BACKTRACE (of the first span): | ||
= note: inside `std::mem::replace::<i32>` at RUSTLIB/core/src/mem/mod.rs:LL:CC | ||
= note: inside `std::cell::Cell::<i32>::replace` at RUSTLIB/core/src/cell.rs:LL:CC | ||
= note: inside `std::cell::Cell::<i32>::set` at RUSTLIB/core/src/cell.rs:LL:CC | ||
note: inside `safe` | ||
--> $DIR/aliasing_mut4.rs:LL:CC | ||
| | ||
LL | y.set(1); | ||
| ^^^^^^^^ | ||
note: inside `main` | ||
--> $DIR/aliasing_mut4.rs:LL:CC | ||
| | ||
LL | safe_raw(xshr, xraw as *mut _); | ||
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | ||
|
||
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
||
error: aborting due to previous error | ||
|
7 changes: 6 additions & 1 deletion
7
.../stacked_borrows/box_noalias_violation.rs → ...ail/both_borrows/box_noalias_violation.rs
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
File renamed without changes.
38 changes: 38 additions & 0 deletions
38
src/tools/miri/tests/fail/both_borrows/box_noalias_violation.tree.stderr
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,38 @@ | ||
error: Undefined Behavior: read access through <TAG> is forbidden | ||
--> $DIR/box_noalias_violation.rs:LL:CC | ||
| | ||
LL | *y | ||
| ^^ read 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 foreign to the protected tag <TAG> (i.e., it is not a child) | ||
= help: the access would cause the protected tag <TAG> to transition from Active to Frozen | ||
= help: this is a loss of write permissions, which is not allowed for protected tags | ||
help: the accessed tag <TAG> was created here | ||
--> $DIR/box_noalias_violation.rs:LL:CC | ||
| | ||
LL | let ptr = &mut v as *mut i32; | ||
| ^^^^^^ | ||
help: the protected tag <TAG> was created here, in the initial state Reserved | ||
--> $DIR/box_noalias_violation.rs:LL:CC | ||
| | ||
LL | unsafe fn test(mut x: Box<i32>, y: *const i32) -> i32 { | ||
| ^^^^^ | ||
help: the protected tag <TAG> later transitioned to Active due to a child write access at offsets [0x0..0x4] | ||
--> $DIR/box_noalias_violation.rs:LL:CC | ||
| | ||
LL | *x = 5; | ||
| ^^^^^^ | ||
= help: this corresponds to the first write to a 2-phase borrowed mutable reference | ||
= note: BACKTRACE (of the first span): | ||
= note: inside `test` at $DIR/box_noalias_violation.rs:LL:CC | ||
note: inside `main` | ||
--> $DIR/box_noalias_violation.rs:LL:CC | ||
| | ||
LL | test(Box::from_raw(ptr), ptr); | ||
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | ||
|
||
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
||
error: aborting due to previous error | ||
|
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
File renamed without changes.
Oops, something went wrong.