Skip to content

Commit 18662da

Browse files
committed
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
2 parents 4762301 + 05640c4 commit 18662da

File tree

135 files changed

+1641
-118
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

135 files changed

+1641
-118
lines changed

tests/fail/stacked_borrows/alias_through_mutation.rs renamed to tests/fail/both_borrows/alias_through_mutation.rs

+6-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
//@revisions: stack tree
2+
//@[tree]compile-flags: -Zmiri-tree-borrows
3+
14
// This makes a ref that was passed to us via &mut alias with things it should not alias with
25
fn retarget(x: &mut &u32, target: &mut u32) {
36
unsafe {
@@ -11,5 +14,7 @@ fn main() {
1114
retarget(&mut target_alias, target);
1215
// now `target_alias` points to the same thing as `target`
1316
*target = 13;
14-
let _val = *target_alias; //~ ERROR: /read access .* tag does not exist in the borrow stack/
17+
let _val = *target_alias;
18+
//~[stack]^ ERROR: /read access .* tag does not exist in the borrow stack/
19+
//~[tree]| ERROR: /read access through .* is forbidden/
1520
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
error: Undefined Behavior: read access through <TAG> is forbidden
2+
--> $DIR/alias_through_mutation.rs:LL:CC
3+
|
4+
LL | let _val = *target_alias;
5+
| ^^^^^^^^^^^^^ read access through <TAG> 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> is a child of the conflicting tag <TAG>
9+
= help: the conflicting tag <TAG> has state Disabled which forbids child read accesses
10+
help: the accessed tag <TAG> was created here
11+
--> $DIR/alias_through_mutation.rs:LL:CC
12+
|
13+
LL | *x = &mut *(target as *mut _);
14+
| ^^^^^^^^^^^^^^^^^^^^^^^^
15+
help: the conflicting tag <TAG> was created here, in the initial state Reserved
16+
--> $DIR/alias_through_mutation.rs:LL:CC
17+
|
18+
LL | retarget(&mut target_alias, target);
19+
| ^^^^^^
20+
help: the conflicting tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x4]
21+
--> $DIR/alias_through_mutation.rs:LL:CC
22+
|
23+
LL | *target = 13;
24+
| ^^^^^^^^^^^^
25+
= help: this corresponds to a loss of read and write permissions
26+
= note: BACKTRACE (of the first span):
27+
= note: inside `main` at $DIR/alias_through_mutation.rs:LL:CC
28+
29+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
30+
31+
error: aborting due to previous error
32+

tests/fail/stacked_borrows/aliasing_mut1.rs renamed to tests/fail/both_borrows/aliasing_mut1.rs

+7-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,12 @@
1+
//@revisions: stack tree
2+
//@[tree]compile-flags: -Zmiri-tree-borrows
13
use std::mem;
24

3-
pub fn safe(_x: &mut i32, _y: &mut i32) {} //~ ERROR: protect
5+
pub fn safe(x: &mut i32, y: &mut i32) {
6+
//~[stack]^ ERROR: protect
7+
*x = 1; //~[tree] ERROR: /write access through .* is forbidden/
8+
*y = 2;
9+
}
410

511
fn main() {
612
let mut x = 0;

tests/fail/stacked_borrows/aliasing_mut1.stderr renamed to tests/fail/both_borrows/aliasing_mut1.stack.stderr

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
error: Undefined Behavior: not granting access to tag <TAG> because that would remove [Unique for <TAG>] which is strongly protected because it is an argument of call ID
22
--> $DIR/aliasing_mut1.rs:LL:CC
33
|
4-
LL | pub fn safe(_x: &mut i32, _y: &mut i32) {}
5-
| ^^ not granting access to tag <TAG> because that would remove [Unique for <TAG>] which is strongly protected because it is an argument of call ID
4+
LL | pub fn safe(x: &mut i32, y: &mut i32) {
5+
| ^ not granting access to tag <TAG> because that would remove [Unique for <TAG>] which is strongly protected because it is an argument of call ID
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
88
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
@@ -14,8 +14,8 @@ LL | let xraw: *mut i32 = unsafe { mem::transmute(&mut x) };
1414
help: <TAG> is this argument
1515
--> $DIR/aliasing_mut1.rs:LL:CC
1616
|
17-
LL | pub fn safe(_x: &mut i32, _y: &mut i32) {}
18-
| ^^
17+
LL | pub fn safe(x: &mut i32, y: &mut i32) {
18+
| ^
1919
= note: BACKTRACE (of the first span):
2020
= note: inside `safe` at $DIR/aliasing_mut1.rs:LL:CC
2121
note: inside `main`
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
error: Undefined Behavior: write access through <TAG> is forbidden
2+
--> $DIR/aliasing_mut1.rs:LL:CC
3+
|
4+
LL | *x = 1;
5+
| ^^^^^^ write access through <TAG> 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 Frozen which forbids child write accesses
9+
help: the accessed tag <TAG> was created here, in the initial state Reserved
10+
--> $DIR/aliasing_mut1.rs:LL:CC
11+
|
12+
LL | pub fn safe(x: &mut i32, y: &mut i32) {
13+
| ^
14+
help: the accessed tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x4]
15+
--> $DIR/aliasing_mut1.rs:LL:CC
16+
|
17+
LL | pub fn safe(x: &mut i32, y: &mut i32) {
18+
| ^
19+
= help: this corresponds to a loss of write permissions
20+
= note: BACKTRACE (of the first span):
21+
= note: inside `safe` at $DIR/aliasing_mut1.rs:LL:CC
22+
note: inside `main`
23+
--> $DIR/aliasing_mut1.rs:LL:CC
24+
|
25+
LL | safe_raw(xraw, xraw);
26+
| ^^^^^^^^^^^^^^^^^^^^
27+
28+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
29+
30+
error: aborting due to previous error
31+

tests/fail/stacked_borrows/aliasing_mut2.rs renamed to tests/fail/both_borrows/aliasing_mut2.rs

+7-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,12 @@
1+
//@revisions: stack tree
2+
//@[tree]compile-flags: -Zmiri-tree-borrows
13
use std::mem;
24

3-
pub fn safe(_x: &i32, _y: &mut i32) {} //~ ERROR: protect
5+
pub fn safe(x: &i32, y: &mut i32) {
6+
//~[stack]^ ERROR: protect
7+
let _v = *x;
8+
*y = 2; //~[tree] ERROR: /write access through .* is forbidden/
9+
}
410

511
fn main() {
612
let mut x = 0;

tests/fail/stacked_borrows/aliasing_mut2.stderr renamed to tests/fail/both_borrows/aliasing_mut2.stack.stderr

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
error: Undefined Behavior: not granting access to tag <TAG> because that would remove [SharedReadOnly for <TAG>] which is strongly protected because it is an argument of call ID
22
--> $DIR/aliasing_mut2.rs:LL:CC
33
|
4-
LL | pub fn safe(_x: &i32, _y: &mut i32) {}
5-
| ^^ not granting access to tag <TAG> because that would remove [SharedReadOnly for <TAG>] which is strongly protected because it is an argument of call ID
4+
LL | pub fn safe(x: &i32, y: &mut i32) {
5+
| ^ not granting access to tag <TAG> because that would remove [SharedReadOnly for <TAG>] which is strongly protected because it is an argument of call ID
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
88
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
@@ -14,8 +14,8 @@ LL | let xref = &mut x;
1414
help: <TAG> is this argument
1515
--> $DIR/aliasing_mut2.rs:LL:CC
1616
|
17-
LL | pub fn safe(_x: &i32, _y: &mut i32) {}
18-
| ^^
17+
LL | pub fn safe(x: &i32, y: &mut i32) {
18+
| ^
1919
= note: BACKTRACE (of the first span):
2020
= note: inside `safe` at $DIR/aliasing_mut2.rs:LL:CC
2121
note: inside `main`
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
error: Undefined Behavior: write access through <TAG> is forbidden
2+
--> $DIR/aliasing_mut2.rs:LL:CC
3+
|
4+
LL | *y = 2;
5+
| ^^^^^^ write access through <TAG> 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 Frozen which forbids child write accesses
9+
help: the accessed tag <TAG> was created here, in the initial state Reserved
10+
--> $DIR/aliasing_mut2.rs:LL:CC
11+
|
12+
LL | pub fn safe(x: &i32, y: &mut i32) {
13+
| ^
14+
help: the accessed tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x4]
15+
--> $DIR/aliasing_mut2.rs:LL:CC
16+
|
17+
LL | let _v = *x;
18+
| ^^
19+
= help: this corresponds to a loss of write permissions
20+
= note: BACKTRACE (of the first span):
21+
= note: inside `safe` at $DIR/aliasing_mut2.rs:LL:CC
22+
note: inside `main`
23+
--> $DIR/aliasing_mut2.rs:LL:CC
24+
|
25+
LL | safe_raw(xshr, xraw);
26+
| ^^^^^^^^^^^^^^^^^^^^
27+
28+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
29+
30+
error: aborting due to previous error
31+

tests/fail/stacked_borrows/aliasing_mut3.rs renamed to tests/fail/both_borrows/aliasing_mut3.rs

+7-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,12 @@
1+
//@revisions: stack tree
2+
//@[tree]compile-flags: -Zmiri-tree-borrows
13
use std::mem;
24

3-
pub fn safe(_x: &mut i32, _y: &i32) {} //~ ERROR: borrow stack
5+
pub fn safe(x: &mut i32, y: &i32) {
6+
//~[stack]^ ERROR: borrow stack
7+
*x = 1; //~[tree] ERROR: /write access through .* is forbidden/
8+
let _v = *y;
9+
}
410

511
fn main() {
612
let mut x = 0;

tests/fail/stacked_borrows/aliasing_mut3.stderr renamed to tests/fail/both_borrows/aliasing_mut3.stack.stderr

+5-5
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
11
error: Undefined Behavior: trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
22
--> $DIR/aliasing_mut3.rs:LL:CC
33
|
4-
LL | pub fn safe(_x: &mut i32, _y: &i32) {}
5-
| ^^
6-
| |
7-
| trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
8-
| this error occurs as part of function-entry retag at ALLOC[0x0..0x4]
4+
LL | pub fn safe(x: &mut i32, y: &i32) {
5+
| ^
6+
| |
7+
| trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
8+
| this error occurs as part of function-entry retag at ALLOC[0x0..0x4]
99
|
1010
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
1111
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
error: Undefined Behavior: write access through <TAG> is forbidden
2+
--> $DIR/aliasing_mut3.rs:LL:CC
3+
|
4+
LL | *x = 1;
5+
| ^^^^^^ write access through <TAG> 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 Frozen which forbids child write accesses
9+
help: the accessed tag <TAG> was created here, in the initial state Reserved
10+
--> $DIR/aliasing_mut3.rs:LL:CC
11+
|
12+
LL | pub fn safe(x: &mut i32, y: &i32) {
13+
| ^
14+
help: the accessed tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x4]
15+
--> $DIR/aliasing_mut3.rs:LL:CC
16+
|
17+
LL | pub fn safe(x: &mut i32, y: &i32) {
18+
| ^
19+
= help: this corresponds to a loss of write permissions
20+
= note: BACKTRACE (of the first span):
21+
= note: inside `safe` at $DIR/aliasing_mut3.rs:LL:CC
22+
note: inside `main`
23+
--> $DIR/aliasing_mut3.rs:LL:CC
24+
|
25+
LL | safe_raw(xraw, xshr);
26+
| ^^^^^^^^^^^^^^^^^^^^
27+
28+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
29+
30+
error: aborting due to previous error
31+

tests/fail/stacked_borrows/aliasing_mut4.rs renamed to tests/fail/both_borrows/aliasing_mut4.rs

+8-1
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,15 @@
1+
//@revisions: stack tree
2+
//@[tree]compile-flags: -Zmiri-tree-borrows
3+
//@[tree]error-in-other-file: /write access through .* is forbidden/
14
use std::cell::Cell;
25
use std::mem;
36

47
// Make sure &mut UnsafeCell also is exclusive
5-
pub fn safe(_x: &i32, _y: &mut Cell<i32>) {} //~ ERROR: protect
8+
pub fn safe(x: &i32, y: &mut Cell<i32>) {
9+
//~[stack]^ ERROR: protect
10+
y.set(1);
11+
let _ = *x;
12+
}
613

714
fn main() {
815
let mut x = 0;

tests/fail/stacked_borrows/aliasing_mut4.stderr renamed to tests/fail/both_borrows/aliasing_mut4.stack.stderr

+4-4
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
error: Undefined Behavior: not granting access to tag <TAG> because that would remove [SharedReadOnly for <TAG>] which is strongly protected because it is an argument of call ID
22
--> $DIR/aliasing_mut4.rs:LL:CC
33
|
4-
LL | pub fn safe(_x: &i32, _y: &mut Cell<i32>) {}
5-
| ^^ not granting access to tag <TAG> because that would remove [SharedReadOnly for <TAG>] which is strongly protected because it is an argument of call ID
4+
LL | pub fn safe(x: &i32, y: &mut Cell<i32>) {
5+
| ^ not granting access to tag <TAG> because that would remove [SharedReadOnly for <TAG>] which is strongly protected because it is an argument of call ID
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
88
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
@@ -14,8 +14,8 @@ LL | let xref = &mut x;
1414
help: <TAG> is this argument
1515
--> $DIR/aliasing_mut4.rs:LL:CC
1616
|
17-
LL | pub fn safe(_x: &i32, _y: &mut Cell<i32>) {}
18-
| ^^
17+
LL | pub fn safe(x: &i32, y: &mut Cell<i32>) {
18+
| ^
1919
= note: BACKTRACE (of the first span):
2020
= note: inside `safe` at $DIR/aliasing_mut4.rs:LL:CC
2121
note: inside `main`
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,39 @@
1+
error: Undefined Behavior: write access through <TAG> is forbidden
2+
--> RUSTLIB/core/src/mem/mod.rs:LL:CC
3+
|
4+
LL | ptr::write(dest, src);
5+
| ^^^^^^^^^^^^^^^^^^^^^ write access through <TAG> 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> is foreign to the protected tag <TAG> (i.e., it is not a child)
9+
= help: the access would cause the protected tag <TAG> to transition from Frozen to Disabled
10+
= help: this is a loss of read permissions, which is not allowed for protected tags
11+
help: the accessed tag <TAG> was created here
12+
--> $DIR/aliasing_mut4.rs:LL:CC
13+
|
14+
LL | y.set(1);
15+
| ^^^^^^^^
16+
help: the protected tag <TAG> was created here, in the initial state Frozen
17+
--> $DIR/aliasing_mut4.rs:LL:CC
18+
|
19+
LL | pub fn safe(x: &i32, y: &mut Cell<i32>) {
20+
| ^
21+
= note: BACKTRACE (of the first span):
22+
= note: inside `std::mem::replace::<i32>` at RUSTLIB/core/src/mem/mod.rs:LL:CC
23+
= note: inside `std::cell::Cell::<i32>::replace` at RUSTLIB/core/src/cell.rs:LL:CC
24+
= note: inside `std::cell::Cell::<i32>::set` at RUSTLIB/core/src/cell.rs:LL:CC
25+
note: inside `safe`
26+
--> $DIR/aliasing_mut4.rs:LL:CC
27+
|
28+
LL | y.set(1);
29+
| ^^^^^^^^
30+
note: inside `main`
31+
--> $DIR/aliasing_mut4.rs:LL:CC
32+
|
33+
LL | safe_raw(xshr, xraw as *mut _);
34+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
35+
36+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
37+
38+
error: aborting due to previous error
39+

tests/fail/stacked_borrows/box_noalias_violation.rs renamed to tests/fail/both_borrows/box_noalias_violation.rs

+6-1
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,13 @@
1+
//@revisions: stack tree
2+
//@[tree]compile-flags: -Zmiri-tree-borrows
3+
14
unsafe fn test(mut x: Box<i32>, y: *const i32) -> i32 {
25
// We will call this in a way that x and y alias.
36
*x = 5;
47
std::mem::forget(x);
5-
*y //~ERROR: weakly protected
8+
*y
9+
//~[stack]^ ERROR: weakly protected
10+
//~[tree]| ERROR: /read access through .* is forbidden/
611
}
712

813
fn main() {
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,38 @@
1+
error: Undefined Behavior: read access through <TAG> is forbidden
2+
--> $DIR/box_noalias_violation.rs:LL:CC
3+
|
4+
LL | *y
5+
| ^^ read access through <TAG> 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> is foreign to the protected tag <TAG> (i.e., it is not a child)
9+
= help: the access would cause the protected tag <TAG> to transition from Active to Frozen
10+
= help: this is a loss of write permissions, which is not allowed for protected tags
11+
help: the accessed tag <TAG> was created here
12+
--> $DIR/box_noalias_violation.rs:LL:CC
13+
|
14+
LL | let ptr = &mut v as *mut i32;
15+
| ^^^^^^
16+
help: the protected tag <TAG> was created here, in the initial state Reserved
17+
--> $DIR/box_noalias_violation.rs:LL:CC
18+
|
19+
LL | unsafe fn test(mut x: Box<i32>, y: *const i32) -> i32 {
20+
| ^^^^^
21+
help: the protected tag <TAG> later transitioned to Active due to a child write access at offsets [0x0..0x4]
22+
--> $DIR/box_noalias_violation.rs:LL:CC
23+
|
24+
LL | *x = 5;
25+
| ^^^^^^
26+
= help: this corresponds to the first write to a 2-phase borrowed mutable reference
27+
= note: BACKTRACE (of the first span):
28+
= note: inside `test` at $DIR/box_noalias_violation.rs:LL:CC
29+
note: inside `main`
30+
--> $DIR/box_noalias_violation.rs:LL:CC
31+
|
32+
LL | test(Box::from_raw(ptr), ptr);
33+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
34+
35+
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
36+
37+
error: aborting due to previous error
38+

tests/fail/stacked_borrows/buggy_as_mut_slice.rs renamed to tests/fail/both_borrows/buggy_as_mut_slice.rs

+6-2
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
//@revisions: stack tree
2+
//@[tree]compile-flags: -Zmiri-tree-borrows
13
mod safe {
24
use std::slice::from_raw_parts_mut;
35

@@ -9,7 +11,9 @@ mod safe {
911
fn main() {
1012
let v = vec![0, 1, 2];
1113
let v1 = safe::as_mut_slice(&v);
12-
let _v2 = safe::as_mut_slice(&v);
14+
let v2 = safe::as_mut_slice(&v);
1315
v1[1] = 5;
14-
//~^ ERROR: /write access .* tag does not exist in the borrow stack/
16+
//~[stack]^ ERROR: /write access .* tag does not exist in the borrow stack/
17+
v2[1] = 7;
18+
//~[tree]^ ERROR: /write access through .* is forbidden/
1519
}

0 commit comments

Comments
 (0)