Skip to content

Commit

Permalink
Select more TB fail tests
Browse files Browse the repository at this point in the history
- reorganize tests/ structure: {stacked,tree,both}_borrows
- UnsafeCell transmutation (the one that should fail, i.e. transmute &
  -> UnsafeCell then try to write)
- select TB pass tests from existing SB fail tests (and a version that
  fails TB)
- many fail tests now shared
    * extra test for TB that parent write invalidates child reads
    * buggy_* tests now shared
    * tests for deep retagging (pass_invalid_shr_*) now shared
    * extra TB test that shared references are read-only
    * aliasing_mut{1,2,3,4} adapted to fail both
    * extra TB test that write to raw parent invalidates shared children
    * mut_exclusive_violation2 now shared
    * issue-miri-1050-2 revisions fix
- deduplications
  • Loading branch information
Vanille-N committed Jun 3, 2023
1 parent 507055b commit 580e2b3
Show file tree
Hide file tree
Showing 135 changed files with 1,641 additions and 118 deletions.
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
//@revisions: stack tree
//@[tree]compile-flags: -Zmiri-tree-borrows

// This makes a ref that was passed to us via &mut alias with things it should not alias with
fn retarget(x: &mut &u32, target: &mut u32) {
unsafe {
Expand All @@ -11,5 +14,7 @@ fn main() {
retarget(&mut target_alias, target);
// now `target_alias` points to the same thing as `target`
*target = 13;
let _val = *target_alias; //~ ERROR: /read access .* tag does not exist in the borrow stack/
let _val = *target_alias;
//~[stack]^ ERROR: /read access .* tag does not exist in the borrow stack/
//~[tree]| ERROR: /read access through .* is forbidden/
}
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

Original file line number Diff line number Diff line change
@@ -1,6 +1,12 @@
//@revisions: stack tree
//@[tree]compile-flags: -Zmiri-tree-borrows
use std::mem;

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

fn main() {
let mut x = 0;
Expand Down
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
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
--> $DIR/aliasing_mut1.rs:LL:CC
|
LL | pub fn safe(_x: &mut i32, _y: &mut i32) {}
| ^^ 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
LL | pub fn safe(x: &mut i32, y: &mut i32) {
| ^ 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
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
Expand All @@ -14,8 +14,8 @@ LL | let xraw: *mut i32 = unsafe { mem::transmute(&mut x) };
help: <TAG> is this argument
--> $DIR/aliasing_mut1.rs:LL:CC
|
LL | pub fn safe(_x: &mut i32, _y: &mut i32) {}
| ^^
LL | pub fn safe(x: &mut i32, y: &mut i32) {
| ^
= note: BACKTRACE (of the first span):
= note: inside `safe` at $DIR/aliasing_mut1.rs:LL:CC
note: inside `main`
Expand Down
31 changes: 31 additions & 0 deletions src/tools/miri/tests/fail/both_borrows/aliasing_mut1.tree.stderr
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

Original file line number Diff line number Diff line change
@@ -1,6 +1,12 @@
//@revisions: stack tree
//@[tree]compile-flags: -Zmiri-tree-borrows
use std::mem;

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

fn main() {
let mut x = 0;
Expand Down
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
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
--> $DIR/aliasing_mut2.rs:LL:CC
|
LL | pub fn safe(_x: &i32, _y: &mut i32) {}
| ^^ 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
LL | pub fn safe(x: &i32, y: &mut i32) {
| ^ 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
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
Expand All @@ -14,8 +14,8 @@ LL | let xref = &mut x;
help: <TAG> is this argument
--> $DIR/aliasing_mut2.rs:LL:CC
|
LL | pub fn safe(_x: &i32, _y: &mut i32) {}
| ^^
LL | pub fn safe(x: &i32, y: &mut i32) {
| ^
= note: BACKTRACE (of the first span):
= note: inside `safe` at $DIR/aliasing_mut2.rs:LL:CC
note: inside `main`
Expand Down
31 changes: 31 additions & 0 deletions src/tools/miri/tests/fail/both_borrows/aliasing_mut2.tree.stderr
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

Original file line number Diff line number Diff line change
@@ -1,6 +1,12 @@
//@revisions: stack tree
//@[tree]compile-flags: -Zmiri-tree-borrows
use std::mem;

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

fn main() {
let mut x = 0;
Expand Down
Original file line number Diff line number Diff line change
@@ -1,11 +1,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
--> $DIR/aliasing_mut3.rs:LL:CC
|
LL | pub fn safe(_x: &mut i32, _y: &i32) {}
| ^^
| |
| trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of function-entry retag at ALLOC[0x0..0x4]
LL | pub fn safe(x: &mut i32, y: &i32) {
| ^
| |
| trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of function-entry retag at ALLOC[0x0..0x4]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
Expand Down
31 changes: 31 additions & 0 deletions src/tools/miri/tests/fail/both_borrows/aliasing_mut3.tree.stderr
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

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

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

fn main() {
let mut x = 0;
Expand Down
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
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
--> $DIR/aliasing_mut4.rs:LL:CC
|
LL | pub fn safe(_x: &i32, _y: &mut Cell<i32>) {}
| ^^ 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
LL | pub fn safe(x: &i32, y: &mut Cell<i32>) {
| ^ 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
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
Expand All @@ -14,8 +14,8 @@ LL | let xref = &mut x;
help: <TAG> is this argument
--> $DIR/aliasing_mut4.rs:LL:CC
|
LL | pub fn safe(_x: &i32, _y: &mut Cell<i32>) {}
| ^^
LL | pub fn safe(x: &i32, y: &mut Cell<i32>) {
| ^
= note: BACKTRACE (of the first span):
= note: inside `safe` at $DIR/aliasing_mut4.rs:LL:CC
note: inside `main`
Expand Down
39 changes: 39 additions & 0 deletions src/tools/miri/tests/fail/both_borrows/aliasing_mut4.tree.stderr
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

Original file line number Diff line number Diff line change
@@ -1,8 +1,13 @@
//@revisions: stack tree
//@[tree]compile-flags: -Zmiri-tree-borrows

unsafe fn test(mut x: Box<i32>, y: *const i32) -> i32 {
// We will call this in a way that x and y alias.
*x = 5;
std::mem::forget(x);
*y //~ERROR: weakly protected
*y
//~[stack]^ ERROR: weakly protected
//~[tree]| ERROR: /read access through .* is forbidden/
}

fn main() {
Expand Down
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

Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
//@revisions: stack tree
//@[tree]compile-flags: -Zmiri-tree-borrows
mod safe {
use std::slice::from_raw_parts_mut;

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

0 comments on commit 580e2b3

Please sign in to comment.