-
Notifications
You must be signed in to change notification settings - Fork 421
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
base: master
Are you sure you want to change the base?
Tree Borrows: improve protector end access child skipping #4766
Conversation
|
Thank you for contributing to Miri! A reviewer will take a look at your PR, typically within a week or two. |
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.
Mostly comments about comments, as usual. :)
| global, | ||
| ChildrenVisitMode::VisitChildrenOfAccessed, | ||
| &diagnostics, | ||
| None, // min_exposed_child only matters for protector end access, |
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.
| None, // min_exposed_child only matters for protector end access, | |
| /* min_exposed_child */ None, // only matters for protector end access, |
| let min_exposed_child = if self.roots.len() > 1 { | ||
| LocationTree::get_min_exposed_child(source_idx, &self.nodes) | ||
| } else { | ||
| None |
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.
Is this correct?
| None | |
| // There's no point in computing this when there is just one tree. | |
| None |
| while let Some(idx) = stack.pop() { | ||
| let node = nodes.get(idx).unwrap(); | ||
| if min_tag.is_some_and(|min| min < node.tag) { | ||
| continue; |
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.
| continue; | |
| // The minimum we found before is bigger than this tag, and therefore | |
| // also bigger than all its children, so we can skip this subtree. | |
| continue; |
| if let Some(min_exposed_child) = min_exposed_child | ||
| && tag > min_exposed_child |
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.
Shouldn't this condition check visit_children?
| // On a protector release access we skip the children of the accessed tag so that | ||
| // we can correctly return references from functions. However, if the tag has |
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.
| // On a protector release access we skip the children of the accessed tag so that | |
| // we can correctly return references from functions. However, if the tag has | |
| // On a protector release access we have to skip the children of the accessed tag. | |
| // However, if the tag has |
|
|
||
| /// This is a variant of the test in `../protector-write-lazy.rs`, but with | ||
| /// wildcard references. | ||
| /// Checks that a protector release transitions a foreign reference on a reference, |
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.
What does "transitions a foreign reference on a reference" mean?
| /// wildcard references. | ||
| /// Checks that a protector release transitions a foreign reference on a reference, | ||
| /// if we can determine that it's not a child of the released tag. | ||
| /// For this version we know the tag is not a child, because its wildcard root has |
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.
| /// For this version we know the tag is not a child, because its wildcard root has | |
| /// For this version we know the tag is not a child because its wildcard root has |
| // │ │ | ||
| // ▼ ▼ | ||
| // ┌───────────┐ ┌───────────┐ | ||
| // │ arg4 │ │ ref6│ |
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.
Does the horizontal alignment of ref6 mean anything?
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 test seems very similar to the previous one, why did you add it as a separate test? Is there some plausible bug in the code that could make a difference between these tests?
| /// * `min_exposed_child`: any subtree that could be a child of `access_source` must | ||
| /// have a root with a larger tag than this. If None then no other subtree can be | ||
| /// a child of `access_source`. | ||
| /// This only gets read if `visit_children==SkipChildrenOfAccessed`. |
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.
The comment doesn't match the name. What about something like this?
| /// * `min_exposed_child`: any subtree that could be a child of `access_source` must | |
| /// have a root with a larger tag than this. If None then no other subtree can be | |
| /// a child of `access_source`. | |
| /// This only gets read if `visit_children==SkipChildrenOfAccessed`. | |
| /// * `min_exposed_child`: The tag of the smallest exposed (transitive) child of the accessed node. | |
| /// This is useful with `visit_children == SkipChildrenOfAccessed`, where we need to skip children | |
| /// of the accessed. |
|
Reminder, once the PR becomes ready for a review, use |
Currently, if we do a protector release access we assume that any other subtree (including the main subtree) could be a child of the accessed node, meaning we conservatively don't update them based on the access.
This PR determines as accurately as possible (under the current model), which other subtrees could be children of the accessed tag.
This means we now accurately reflect: