-
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.
Unique gets special treatment when -Zmiri-unique-is-unique
- Loading branch information
Showing
25 changed files
with
486 additions
and
13 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
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
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
15 changes: 15 additions & 0 deletions
15
src/tools/miri/tests/fail/tree_borrows/children-can-alias.default.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,15 @@ | ||
error: Undefined Behavior: entering unreachable code | ||
--> $DIR/children-can-alias.rs:LL:CC | ||
| | ||
LL | std::hint::unreachable_unchecked(); | ||
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ entering unreachable code | ||
| | ||
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior | ||
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information | ||
= note: BACKTRACE: | ||
= note: inside `main` at $DIR/children-can-alias.rs:LL:CC | ||
|
||
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
||
error: aborting due to previous error | ||
|
59 changes: 59 additions & 0 deletions
59
src/tools/miri/tests/fail/tree_borrows/children-can-alias.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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,59 @@ | ||
//@revisions: default uniq | ||
//@compile-flags: -Zmiri-tree-borrows | ||
//@[uniq]compile-flags: -Zmiri-unique-is-unique | ||
|
||
//! This is NOT intended behavior. | ||
//! We should eventually find a solution so that the version with `Unique` passes too, | ||
//! otherwise `Unique` is more strict than `&mut`! | ||
|
||
#![feature(ptr_internals)] | ||
|
||
use core::ptr::addr_of_mut; | ||
use core::ptr::Unique; | ||
|
||
fn main() { | ||
let mut data = 0u8; | ||
let raw = addr_of_mut!(data); | ||
unsafe { | ||
raw_children_of_refmut_can_alias(&mut *raw); | ||
raw_children_of_unique_can_alias(Unique::new_unchecked(raw)); | ||
|
||
// Ultimately the intended behavior is that both above tests would | ||
// succeed. | ||
std::hint::unreachable_unchecked(); | ||
//~[default]^ ERROR: entering unreachable code | ||
} | ||
} | ||
|
||
unsafe fn raw_children_of_refmut_can_alias(x: &mut u8) { | ||
let child1 = addr_of_mut!(*x); | ||
let child2 = addr_of_mut!(*x); | ||
// We create two raw aliases of `x`: they have the exact same | ||
// tag and can be used interchangeably. | ||
child1.write(1); | ||
child2.write(2); | ||
child1.write(1); | ||
child2.write(2); | ||
} | ||
|
||
unsafe fn raw_children_of_unique_can_alias(x: Unique<u8>) { | ||
let child1 = x.as_ptr(); | ||
let child2 = x.as_ptr(); | ||
// Under `-Zmiri-unique-is-unique`, `Unique` accidentally offers more guarantees | ||
// than `&mut`. Not because it responds differently to accesses but because | ||
// there is no easy way to obtain a copy with the same tag. | ||
// | ||
// The closest (non-hack) attempt is two calls to `as_ptr`. | ||
// - Without `-Zmiri-unique-is-unique`, independent `as_ptr` calls return pointers | ||
// with the same tag that can thus be used interchangeably. | ||
// - With the current implementation of `-Zmiri-unique-is-unique`, they return cousin | ||
// tags with permissions that do not tolerate aliasing. | ||
// Eventually we should make such aliasing allowed in some situations | ||
// (e.g. when there is no protector), which will probably involve | ||
// introducing a new kind of permission. | ||
child1.write(1); | ||
child2.write(2); | ||
//~[uniq]^ ERROR: /write access through .* is forbidden/ | ||
child1.write(1); | ||
child2.write(2); | ||
} |
37 changes: 37 additions & 0 deletions
37
src/tools/miri/tests/fail/tree_borrows/children-can-alias.uniq.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,37 @@ | ||
error: Undefined Behavior: write access through <TAG> is forbidden | ||
--> $DIR/children-can-alias.rs:LL:CC | ||
| | ||
LL | child2.write(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> 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/children-can-alias.rs:LL:CC | ||
| | ||
LL | let child2 = x.as_ptr(); | ||
| ^^^^^^^^^^ | ||
help: the conflicting tag <TAG> was created here, in the initial state Reserved | ||
--> $DIR/children-can-alias.rs:LL:CC | ||
| | ||
LL | let child2 = x.as_ptr(); | ||
| ^ | ||
help: the conflicting tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x1] | ||
--> $DIR/children-can-alias.rs:LL:CC | ||
| | ||
LL | child1.write(1); | ||
| ^^^^^^^^^^^^^^^ | ||
= help: this transition corresponds to a loss of read and write permissions | ||
= note: BACKTRACE (of the first span): | ||
= note: inside `raw_children_of_unique_can_alias` at $DIR/children-can-alias.rs:LL:CC | ||
note: inside `main` | ||
--> $DIR/children-can-alias.rs:LL:CC | ||
| | ||
LL | raw_children_of_unique_can_alias(Unique::new_unchecked(raw)); | ||
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | ||
|
||
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
||
error: aborting due to previous error | ||
|
32 changes: 32 additions & 0 deletions
32
src/tools/miri/tests/fail/tree_borrows/unique.default.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: write access through <TAG> is forbidden | ||
--> $DIR/unique.rs:LL:CC | ||
| | ||
LL | *uniq.as_ptr() = 3; | ||
| ^^^^^^^^^^^^^^^^^^ 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 this child write access | ||
help: the accessed tag <TAG> was created here, in the initial state Reserved | ||
--> $DIR/unique.rs:LL:CC | ||
| | ||
LL | let refmut = &mut data; | ||
| ^^^^^^^^^ | ||
help: the accessed tag <TAG> later transitioned to Active due to a child write access at offsets [0x0..0x1] | ||
--> $DIR/unique.rs:LL:CC | ||
| | ||
LL | *uniq.as_ptr() = 1; // activation | ||
| ^^^^^^^^^^^^^^^^^^ | ||
= help: this transition corresponds to the first write to a 2-phase borrowed mutable reference | ||
help: the accessed tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x1] | ||
--> $DIR/unique.rs:LL:CC | ||
| | ||
LL | let _definitely_parent = data; // definitely Frozen by now | ||
| ^^^^ | ||
= help: this transition corresponds to a loss of write permissions | ||
= note: BACKTRACE (of the first span): | ||
= note: inside `main` at $DIR/unique.rs:LL:CC | ||
|
||
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
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,27 @@ | ||
//@revisions: default uniq | ||
//@compile-flags: -Zmiri-tree-borrows | ||
//@[uniq]compile-flags: -Zmiri-unique-is-unique | ||
|
||
// A pattern that detects if `Unique` is treated as exclusive or not: | ||
// activate the pointer behind a `Unique` then do a read that is parent | ||
// iff `Unique` was specially reborrowed. | ||
|
||
#![feature(ptr_internals)] | ||
use core::ptr::Unique; | ||
|
||
fn main() { | ||
let mut data = 0u8; | ||
let refmut = &mut data; | ||
let rawptr = refmut as *mut u8; | ||
|
||
unsafe { | ||
let uniq = Unique::new_unchecked(rawptr); | ||
*uniq.as_ptr() = 1; // activation | ||
let _maybe_parent = *rawptr; // maybe becomes Frozen | ||
*uniq.as_ptr() = 2; | ||
//~[uniq]^ ERROR: /write access through .* is forbidden/ | ||
let _definitely_parent = data; // definitely Frozen by now | ||
*uniq.as_ptr() = 3; | ||
//~[default]^ ERROR: /write access through .* is forbidden/ | ||
} | ||
} |
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: write access through <TAG> is forbidden | ||
--> $DIR/unique.rs:LL:CC | ||
| | ||
LL | *uniq.as_ptr() = 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> is a child of the conflicting tag <TAG> | ||
= help: the conflicting tag <TAG> has state Frozen which forbids this child write access | ||
help: the accessed tag <TAG> was created here | ||
--> $DIR/unique.rs:LL:CC | ||
| | ||
LL | *uniq.as_ptr() = 2; | ||
| ^^^^^^^^^^^^^ | ||
help: the conflicting tag <TAG> was created here, in the initial state Reserved | ||
--> $DIR/unique.rs:LL:CC | ||
| | ||
LL | let uniq = Unique::new_unchecked(rawptr); | ||
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | ||
help: the conflicting tag <TAG> later transitioned to Active due to a child write access at offsets [0x0..0x1] | ||
--> $DIR/unique.rs:LL:CC | ||
| | ||
LL | *uniq.as_ptr() = 1; // activation | ||
| ^^^^^^^^^^^^^^^^^^ | ||
= help: this transition corresponds to the first write to a 2-phase borrowed mutable reference | ||
help: the conflicting tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x1] | ||
--> $DIR/unique.rs:LL:CC | ||
| | ||
LL | let _maybe_parent = *rawptr; // maybe becomes Frozen | ||
| ^^^^^^^ | ||
= help: this transition corresponds to a loss of write permissions | ||
= note: BACKTRACE (of the first span): | ||
= note: inside `main` at $DIR/unique.rs:LL:CC | ||
|
||
note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
||
error: aborting due to previous error | ||
|
Oops, something went wrong.