-
Notifications
You must be signed in to change notification settings - Fork 421
Tree Borrows: multiple invalid exposed nodes on main subtree #4757
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
5
commits into
rust-lang:master
Choose a base branch
from
royAmmerschuber:feature/multi_exposed_main
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.
+111
−11
Open
Changes from all commits
Commits
Show all changes
5 commits
Select commit
Hold shift + click to select a range
4352e93
detect properly if there are valid exposed nodes
royAmmerschuber 55e4fb5
add comments
royAmmerschuber dc8d21f
fix rebase issues
royAmmerschuber 07f7e6c
various changes
royAmmerschuber 2081d1a
fix code behind flag
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 | ||||||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
|
|
@@ -111,7 +111,7 @@ impl LocationState { | |||||||||||||||||||||||||||||
| // We need to update the wildcard state, if the permission | ||||||||||||||||||||||||||||||
| // of an exposed pointer changes. | ||||||||||||||||||||||||||||||
| if node.is_exposed { | ||||||||||||||||||||||||||||||
| let access_type = self.permission.strongest_allowed_child_access(protected); | ||||||||||||||||||||||||||||||
| let access_type = self.permission.strongest_allowed_local_access(protected); | ||||||||||||||||||||||||||||||
| WildcardState::update_exposure(idx, access_type, nodes, wildcard_accesses); | ||||||||||||||||||||||||||||||
| } | ||||||||||||||||||||||||||||||
| } | ||||||||||||||||||||||||||||||
|
|
@@ -1034,6 +1034,8 @@ impl<'tcx> LocationTree { | |||||||||||||||||||||||||||||
| wildcard_state.access_relatedness(access_kind, only_foreign) | ||||||||||||||||||||||||||||||
| }; | ||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||
| let mut has_exposed = false; | ||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||
| // This does a traversal across the tree updating children before their parents. The | ||||||||||||||||||||||||||||||
| // difference to `perform_normal_access` is that we take the access relatedness from | ||||||||||||||||||||||||||||||
| // the wildcard tracking state of the node instead of from the visitor itself. | ||||||||||||||||||||||||||||||
|
|
@@ -1082,6 +1084,17 @@ impl<'tcx> LocationTree { | |||||||||||||||||||||||||||||
| return Err(no_valid_exposed_references_error(diagnostics)); | ||||||||||||||||||||||||||||||
| }; | ||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||
| let mut entry = args.data.perms.entry(args.idx); | ||||||||||||||||||||||||||||||
| let perm = entry.or_insert(node.default_location_state()); | ||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||
| // We only count exposed nodes through which an access could happen. | ||||||||||||||||||||||||||||||
| if node.is_exposed | ||||||||||||||||||||||||||||||
| && perm.permission.strongest_allowed_local_access(protected).allows(access_kind) | ||||||||||||||||||||||||||||||
| && max_local_tag.is_none_or(|max_local_tag| max_local_tag >= node.tag) | ||||||||||||||||||||||||||||||
| { | ||||||||||||||||||||||||||||||
| has_exposed = true; | ||||||||||||||||||||||||||||||
| } | ||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||
| let Some(relatedness) = wildcard_relatedness.to_relatedness() else { | ||||||||||||||||||||||||||||||
| // If the access type is Either, then we do not apply any transition | ||||||||||||||||||||||||||||||
| // to this node, but we still update each of its children. | ||||||||||||||||||||||||||||||
|
|
@@ -1090,8 +1103,6 @@ impl<'tcx> LocationTree { | |||||||||||||||||||||||||||||
| return Ok(()); | ||||||||||||||||||||||||||||||
| }; | ||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||
| let mut entry = args.data.perms.entry(args.idx); | ||||||||||||||||||||||||||||||
| let perm = entry.or_insert(node.default_location_state()); | ||||||||||||||||||||||||||||||
| // We know the exact relatedness, so we can actually do precise checks. | ||||||||||||||||||||||||||||||
| perm.perform_transition( | ||||||||||||||||||||||||||||||
| args.idx, | ||||||||||||||||||||||||||||||
|
|
@@ -1115,6 +1126,23 @@ impl<'tcx> LocationTree { | |||||||||||||||||||||||||||||
| }) | ||||||||||||||||||||||||||||||
| }, | ||||||||||||||||||||||||||||||
| )?; | ||||||||||||||||||||||||||||||
| // For a wildcard access to be valid each subtree needs to either contain an exposed tag | ||||||||||||||||||||||||||||||
| // through which the access could have happened or a foreign access to the subtree must | ||||||||||||||||||||||||||||||
| // be possible. If neither of these is the case than the access is UB. | ||||||||||||||||||||||||||||||
| // In reality this is only ever UB on the main subtree as all other trees always allow | ||||||||||||||||||||||||||||||
| // foreign accesses. | ||||||||||||||||||||||||||||||
| if !has_exposed | ||||||||||||||||||||||||||||||
| // Check that no access that is foreign to this subtree is possible. | ||||||||||||||||||||||||||||||
| // (Its only impossible for the main subtree). | ||||||||||||||||||||||||||||||
|
Comment on lines
+1129
to
+1136
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||||||||||||||||||||||||||
| && self | ||||||||||||||||||||||||||||||
| .wildcard_accesses | ||||||||||||||||||||||||||||||
| .get(root) | ||||||||||||||||||||||||||||||
| .unwrap() | ||||||||||||||||||||||||||||||
| .access_relatedness(access_kind, /* only_foreign */ true) | ||||||||||||||||||||||||||||||
| .is_none() | ||||||||||||||||||||||||||||||
| { | ||||||||||||||||||||||||||||||
| return Err(no_valid_exposed_references_error(diagnostics)).into(); | ||||||||||||||||||||||||||||||
| } | ||||||||||||||||||||||||||||||
| interp_ok(()) | ||||||||||||||||||||||||||||||
| } | ||||||||||||||||||||||||||||||
| } | ||||||||||||||||||||||||||||||
|
|
||||||||||||||||||||||||||||||
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
48 changes: 48 additions & 0 deletions
48
tests/fail/tree_borrows/wildcard/cross_tree_update_main_invalid_exposed2.rs
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,48 @@ | ||
| //@compile-flags: -Zmiri-tree-borrows -Zmiri-permissive-provenance | ||
| use std::cell::Cell; | ||
|
|
||
| /// Checks how accesses from one subtree affect other subtrees. | ||
| /// This test checks that an access from a subtree performs a | ||
| /// wildcard access on all earlier trees, and that local | ||
| /// accesses are treated as access errors for tags that are | ||
| /// larger than the root of the accessed subtree. | ||
| /// This tests the case were we have multiple exposed nodes on | ||
| /// the main tree that are invalid because their tag is too large. | ||
| pub fn main() { | ||
| let mut x: u32 = 42; | ||
|
|
||
| let ptr_base = &mut x as *mut u32; | ||
| let ref1 = unsafe { &mut *ptr_base }; | ||
| let int1 = ref1 as *mut u32 as usize; | ||
| let wild = int1 as *mut u32; | ||
|
|
||
| // Activates ref1. | ||
| *ref1 = 4; | ||
|
|
||
| let ref2 = unsafe { &mut *wild }; | ||
|
|
||
| // Freezes ref1. | ||
| let ref3 = unsafe { &mut *(ptr_base as *mut Cell<u32>) }; | ||
| let _int3 = ref3 as *mut Cell<u32> as usize; | ||
| let ref4 = unsafe { &mut *(ptr_base as *mut Cell<u32>) }; | ||
| let _int4 = ref4 as *mut Cell<u32> as usize; | ||
|
|
||
| // ┌──────────────┐ | ||
| // │ │ | ||
| // │ptr_base(Act) ├───────────┬──────────────────┐ * | ||
| // │ │ │ │ │ | ||
| // └──────┬───────┘ │ │ │ | ||
| // │ │ │ │ | ||
| // │ │ │ │ | ||
| // ▼ ▼ ▼ ▼ | ||
| // ┌─────────────┐ ┌────────────┐ ┌────────────┐ ┌───────────┐ | ||
| // │ │ │ │ │ │ │ │ | ||
| // │ ref1(Frz)* │ │ ref3(ReIM)*│ │ ref4(ReIM)*│ │ ref2(Res) │ | ||
| // │ │ │ │ │ │ │ │ | ||
| // └─────────────┘ └────────────┘ └────────────┘ └───────────┘ | ||
|
|
||
| // Performs a wildcard access on the main root. However, as there are | ||
| // no exposed tags with write permissions and a tag smaller than ref2 | ||
| // this access fails. | ||
| *ref2 = 13; //~ ERROR: /write access through .* is forbidden/ | ||
| } |
14 changes: 14 additions & 0 deletions
14
tests/fail/tree_borrows/wildcard/cross_tree_update_main_invalid_exposed2.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,14 @@ | ||
| error: Undefined Behavior: write access through <wildcard> at ALLOC[0x0] is forbidden | ||
| --> tests/fail/tree_borrows/wildcard/cross_tree_update_main_invalid_exposed2.rs:LL:CC | ||
| | | ||
| LL | *ref2 = 13; | ||
| | ^^^^^^^^^^ 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: there are no exposed tags which may perform this access here | ||
|
|
||
| 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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This isn't just about whether there is an exposed node, it's about whether there's an exposed node that allows this access. The name should at least indicate that, and there should be a comment here explaining that.