-
Notifications
You must be signed in to change notification settings - Fork 423
Tree Borrows: improve protector end access child skipping #4766
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Open
royAmmerschuber
wants to merge
7
commits into
rust-lang:master
Choose a base branch
from
royAmmerschuber:feature/protector-release-child-skipping
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
+262
−4
Open
Changes from all commits
Commits
Show all changes
7 commits
Select commit
Hold shift + click to select a range
203cb1d
Revert "remove skip child logic"
royAmmerschuber 817d46b
improve get_min_exposed
royAmmerschuber 41c6ce9
move min_exposed_child outside of location loop
royAmmerschuber 69336b4
add more comments
royAmmerschuber 3e17aa6
comments & skip min_exposed_child skip on normal accesses
royAmmerschuber 6a8dc50
update protector_release test diagrams
royAmmerschuber d35fd25
more comments
royAmmerschuber File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or 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 hidden or 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,79 @@ | ||
| //@compile-flags: -Zmiri-tree-borrows -Zmiri-permissive-provenance | ||
| use std::cell::UnsafeCell; | ||
|
|
||
| /// This is a variant of the test in `../protector-write-lazy.rs`, but with | ||
| /// wildcard references. | ||
| /// Checks that a protector release access correctly determines that certain tags | ||
| /// cannot be children of the protected tag and that it updates them accordingly. | ||
| /// | ||
| /// For this version we know the tag is not a child because its wildcard root has | ||
| /// a smaller tag then the released reference. | ||
| pub fn main() { | ||
| // We need two locations so that we can create a new reference | ||
| // that is foreign to an already active tag. | ||
| let mut x: UnsafeCell<[u32; 2]> = UnsafeCell::new([32, 33]); | ||
| let ref1 = &mut x; | ||
| let cell_ptr = ref1.get() as *mut u32; | ||
|
|
||
| let int = ref1 as *mut UnsafeCell<[u32; 2]> as usize; | ||
| let wild = int as *mut UnsafeCell<u32>; | ||
|
|
||
| let ref2 = unsafe { &mut *cell_ptr }; | ||
|
|
||
| // `ref3` gets created before the protected ref `arg4`. | ||
| let ref3 = unsafe { &mut *wild.wrapping_add(1) }; | ||
|
|
||
| let protect = |arg4: &mut u32| { | ||
| // Activates arg4. This would disable ref3 at [0] if it wasn't a cell. | ||
| *arg4 = 41; | ||
|
|
||
| // Creates an exposed child of arg4. | ||
| let ref5 = &mut *arg4; | ||
| let _int = ref5 as *mut u32 as usize; | ||
|
|
||
| // This creates ref6 from ref3 at [1], so that it doesn't disable arg4 at [0]. | ||
| let ref6 = unsafe { &mut *ref3.get() }; | ||
|
|
||
| // ┌───────────┐ | ||
| // │ ref1* │ | ||
| // │ Cel │ Cel │ * | ||
| // └─────┬─────┘ │ | ||
| // │ │ | ||
| // │ │ | ||
| // ▼ ▼ | ||
| // ┌───────────┐ ┌───────────┐ | ||
| // │ ref2│ │ │ │ ref3│ | ||
| // │ Act │ Res │ │ Cel │ Cel │ | ||
| // └─────┬─────┘ └─────┬─────┘ | ||
| // │ │ | ||
| // │ │ | ||
| // ▼ ▼ | ||
| // ┌───────────┐ ┌───────────┐ | ||
| // │ arg4│ │ │ │ ref6│ | ||
| // │ Act │ Res │ │ Res │ Res │ | ||
| // └─────┬─────┘ └───────────┘ | ||
| // │ | ||
| // │ | ||
| // ▼ | ||
| // ┌───────────┐ | ||
| // │ref5*| │ | ||
| // │ Res │ Res │ | ||
| // └───────────┘ | ||
|
|
||
| // Creates a pointer to [0] with the provenance of ref6. | ||
| return (ref6 as *mut u32).wrapping_sub(1); | ||
|
|
||
| // Protector release on arg4 happens here. | ||
| // This should cause a foreign write on all foreign nodes, | ||
| // unless they could be a child of arg4. | ||
| // arg4 has an exposed child, so some tags with a wildcard | ||
| // ancestor could be its children. | ||
| // However, the root of ref6 was created before arg4, so it | ||
| // cannot be a child of it. So it should get disabled | ||
| // (at location [0]). | ||
| }; | ||
| // ptr has provenance of ref6 | ||
| let ptr = protect(ref2); | ||
| // ref6 is disabled at [0]. | ||
| let _fail = unsafe { *ptr }; //~ ERROR: /read access through .* is forbidden/ | ||
| } |
This file contains hidden or 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,25 @@ | ||
| error: Undefined Behavior: read access through <TAG> at ALLOC[0x0] is forbidden | ||
| --> tests/fail/tree_borrows/wildcard/protector_release.rs:LL:CC | ||
| | | ||
| LL | let _fail = unsafe { *ptr }; | ||
| | ^^^^ Undefined Behavior occurred here | ||
| | | ||
| = 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: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/tree-borrows.md for further information | ||
| = help: the accessed tag <TAG> has state Disabled which forbids this child read access | ||
| help: the accessed tag <TAG> was created here, in the initial state Reserved | ||
| --> tests/fail/tree_borrows/wildcard/protector_release.rs:LL:CC | ||
| | | ||
| LL | let ref6 = unsafe { &mut *ref3.get() }; | ||
| | ^^^^^^^^^^^^^^^^ | ||
| help: the accessed tag <TAG> later transitioned to Disabled due to a protector release (acting as a foreign write access) on every location previously accessed by this tag | ||
| --> tests/fail/tree_borrows/wildcard/protector_release.rs:LL:CC | ||
| | | ||
| LL | }; | ||
| | ^ | ||
| = help: this transition corresponds to a loss of read and write permissions | ||
|
|
||
| note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
|
||
| error: aborting due to 1 previous error | ||
|
|
RalfJung marked this conversation as resolved.
Show resolved
Hide resolved
|
This file contains hidden or 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,81 @@ | ||
| //@compile-flags: -Zmiri-tree-borrows -Zmiri-permissive-provenance | ||
| use std::cell::UnsafeCell; | ||
|
|
||
| /// This is a variant of the test in `../protector-write-lazy.rs`, but with | ||
| /// wildcard references. | ||
| /// Checks that a protector release access correctly determines that certain tags | ||
| /// cannot be children of the protected tag and that it updates them accordingly. | ||
| /// | ||
| /// For this version we know the tag is not a child because its wildcard root has | ||
| /// a smaller tag then the exposed child of the protected tag. | ||
| /// So this test checks that we don't just compare with the accessed tag but instead | ||
| /// find the smallest exposed child. | ||
| pub fn main() { | ||
| // We need two locations so that we can create a new reference | ||
| // that is foreign to an already active tag. | ||
| let mut x: UnsafeCell<[u32; 2]> = UnsafeCell::new([32, 33]); | ||
| let ref1 = &mut x; | ||
| let cell_ptr = ref1.get() as *mut u32; | ||
|
|
||
| let int = ref1 as *mut UnsafeCell<[u32; 2]> as usize; | ||
| let wild = int as *mut UnsafeCell<u32>; | ||
|
|
||
| let ref2 = unsafe { &mut *cell_ptr }; | ||
|
|
||
| let protect = |arg3: &mut u32| { | ||
| // `ref4` gets created after the protected ref `arg3` but before the exposed `ref5`. | ||
| let ref4 = unsafe { &mut *wild.wrapping_add(1) }; | ||
|
|
||
| // Activates arg4. This would disable ref3 at [0] if it wasn't a cell. | ||
| *arg3 = 41; | ||
|
|
||
| // Creates an exposed child of arg3. | ||
| let ref5 = &mut *arg3; | ||
| let _int = ref5 as *mut u32 as usize; | ||
|
|
||
| // This creates ref6 from ref4 at [1], so that it doesn't disable arg3 at [0]. | ||
| let ref6 = unsafe { &mut *ref4.get() }; | ||
|
|
||
| // ┌───────────┐ | ||
| // │ ref1* │ | ||
| // │ Cel │ Cel │ * | ||
| // └─────┬─────┘ │ | ||
| // │ │ | ||
| // │ │ | ||
| // ▼ ▼ | ||
| // ┌───────────┐ ┌───────────┐ | ||
| // │ ref2| │ │ | ref4│ | ||
| // │ Act │ Res │ │ Cel │ Cel │ | ||
| // └─────┬─────┘ └─────┬─────┘ | ||
| // │ │ | ||
| // │ │ | ||
| // ▼ ▼ | ||
| // ┌───────────┐ ┌───────────┐ | ||
| // │ arg3| │ │ | ref6│ | ||
| // │ Act │ Res │ │ Res │ Res │ | ||
| // └─────┬─────┘ └───────────┘ | ||
| // │ | ||
| // │ | ||
| // ▼ | ||
| // ┌───────────┐ | ||
| // │ref5*| │ | ||
| // │ Res │ Res │ | ||
| // └───────────┘ | ||
|
|
||
| // Creates a pointer to [0] with the provenance of ref6. | ||
| return (ref6 as *mut u32).wrapping_sub(1); | ||
|
|
||
| // Protector release on arg3 happens here. | ||
| // This should cause a foreign write on all foreign nodes, | ||
| // unless they could be a child of arg3. | ||
| // arg3 has an exposed child, so some tags with a wildcard | ||
| // ancestor could be its children. | ||
| // However, the root of ref6 was created before the exposed | ||
| // child ref5, so it cannot be a child of it. So it should | ||
| // get disabled (at location [0]). | ||
| }; | ||
| // ptr has provenance of ref6 | ||
| let ptr = protect(ref2); | ||
RalfJung marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| // ref6 is disabled at [0]. | ||
| let _fail = unsafe { *ptr }; //~ ERROR: /read access through .* is forbidden/ | ||
| } | ||
25 changes: 25 additions & 0 deletions
25
tests/fail/tree_borrows/wildcard/protector_release2.stderr
This file contains hidden or 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,25 @@ | ||
| error: Undefined Behavior: read access through <TAG> at ALLOC[0x0] is forbidden | ||
| --> tests/fail/tree_borrows/wildcard/protector_release2.rs:LL:CC | ||
| | | ||
| LL | let _fail = unsafe { *ptr }; | ||
| | ^^^^ Undefined Behavior occurred here | ||
| | | ||
| = 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: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/tree-borrows.md for further information | ||
| = help: the accessed tag <TAG> has state Disabled which forbids this child read access | ||
| help: the accessed tag <TAG> was created here, in the initial state Reserved | ||
| --> tests/fail/tree_borrows/wildcard/protector_release2.rs:LL:CC | ||
| | | ||
| LL | let ref6 = unsafe { &mut *ref4.get() }; | ||
| | ^^^^^^^^^^^^^^^^ | ||
| help: the accessed tag <TAG> later transitioned to Disabled due to a protector release (acting as a foreign write access) on every location previously accessed by this tag | ||
| --> tests/fail/tree_borrows/wildcard/protector_release2.rs:LL:CC | ||
| | | ||
| LL | }; | ||
| | ^ | ||
| = help: this transition corresponds to a loss of read and write permissions | ||
|
|
||
| note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
|
||
| error: aborting due to 1 previous error | ||
|
|
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.