-
Notifications
You must be signed in to change notification settings - Fork 414
Support retagging of wildcard references in tree borrows #4707
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?
Support retagging of wildcard references in tree borrows #4707
Conversation
|
Thank you for contributing to Miri! A reviewer will take a look at your PR, typically within a week or two. |
| // then check if we can skip the entire subtree because the access might not | ||
| // change any permissions here anyway. |
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.
I'm confused by the "might not" here. (Isn't that something you already had before and we removed it in the previous PR?)
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.
Yes, your right. This got lost in a rebase.
This comment has been minimized.
This comment has been minimized.
99dacc6 to
52f2087
Compare
This comment has been minimized.
This comment has been minimized.
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.
Overall approach looks good. Here's a bunch of comments. :)
Please also add the 3 SB tests in this area: illegal_read/write_despite_exposed*.
|
|
||
| let state = perm.or_insert(node.default_location_state()); | ||
| #[cfg(feature = "expensive-consistency-checks")] | ||
| self.verify_wildcard_consistency(global); |
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.
We should only need this if a wildcard is involved in the access, right? I.e. if the tag is wildcard, or if there are multiple roots.
|
|
||
| /// Print extra text if the tag is exposed. | ||
| fn print_exposed(&self, exposed: bool) -> S { | ||
| if exposed { " Exposed" } else { "" } |
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.
| if exposed { " Exposed" } else { "" } | |
| if exposed { " (exposed)" } else { "" } |
| // We can still access both ref1, ref2. | ||
| assert_eq!(*ref2, 13); |
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.
Comment and code don't quite match... we can access both, after all.
You can just explain that this is technically UB we don't catch.
| // We should be able to access any of the references. | ||
| assert_eq!(*ref2, 13); |
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.
Again this doesn't quite test what the comment says.
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.
Please explain in the comment that this tests the max_local_tag logic.
|
Reminder, once the PR becomes ready for a review, use |
| }; | ||
| // Afterwards we check all tags in arbitrary order, so that we also catch | ||
| // protectors on different subtrees. | ||
| // (This unnecessarily checks the tags of `start_idx`s subtree again) |
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 comment seems outdated now.
| TreeVisitor { nodes: &mut self.nodes, loc }.traverse_this_parents_children_other( | ||
| *root, | ||
| // Visit all children, skipping none. | ||
| |_| ContinueTraversal::Recurse, | ||
| check_strong_protector, | ||
| )?; |
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 part is still duplicated between the two branches... maybe it makes more sense to share the entire visitor invocation, not just the check_strong_protector closure?
This comment has been minimized.
This comment has been minimized.
8c7ac81 to
4097b0a
Compare
|
This PR was rebased onto a different master commit. Here's a range-diff highlighting what actually changed. Rebasing is a normal part of keeping PRs up to date, so no action is needed—this note is just to help reviewers. |
|
@rustbot ready |
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.
Thanks! Looks good overall but I have plenty of minor comments.
| /// If we reborrow a reference which has wildcard provenance, then we do not know where in | ||
| /// the tree to attach them. Instead we create a new additional tree for this allocation | ||
| /// with this new reference as a root. We call this additional tree a wildcard subtree. | ||
| /// | ||
| /// Sorted according to `BorTag` from low to high. This also means the main root is `root[0]`. | ||
| /// | ||
| /// The actual structure should be a single tree but with wildcard provenance we approximate | ||
| /// this with this ordered set of trees. Each wildcard subtree could be the direct child of | ||
| /// any exposed tag (that is smaller than the root). This also means that it can only be the | ||
| /// child of a tree that comes before it in the vec ensuring we don't have any cycles in our | ||
| /// approximated tree. | ||
| /// |
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.
| /// If we reborrow a reference which has wildcard provenance, then we do not know where in | |
| /// the tree to attach them. Instead we create a new additional tree for this allocation | |
| /// with this new reference as a root. We call this additional tree a wildcard subtree. | |
| /// | |
| /// Sorted according to `BorTag` from low to high. This also means the main root is `root[0]`. | |
| /// | |
| /// The actual structure should be a single tree but with wildcard provenance we approximate | |
| /// this with this ordered set of trees. Each wildcard subtree could be the direct child of | |
| /// any exposed tag (that is smaller than the root). This also means that it can only be the | |
| /// child of a tree that comes before it in the vec ensuring we don't have any cycles in our | |
| /// approximated tree. | |
| /// | |
| /// If we reborrow a reference which has wildcard provenance, then we do not know where in | |
| /// the tree to attach them. Instead we create a new additional tree for this allocation | |
| /// with this new reference as a root. We call this additional tree a wildcard subtree. | |
| /// | |
| /// The actual structure should be a single tree but with wildcard provenance we approximate | |
| /// this with this ordered set of trees. Each wildcard subtree is the direct child of *some* exposed | |
| /// tag (that is smaller than the root), but we do not know which. This also means that it can only be the | |
| /// child of a tree that comes before it in the vec ensuring we don't have any cycles in our | |
| /// approximated tree. | |
| /// | |
| /// Sorted according to `BorTag` from low to high. This also means the main root is `root[0]`. |
| accessed_node: UniIndex, | ||
| visit_children: ChildrenVisitMode, | ||
| ) -> Result<(), Err> { | ||
| ) -> Result<UniIndex, Err> { |
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.
Please explain the return value in a doc comment for this function.
| ) -> InterpResult<'tcx> { | ||
| let idx = self.tag_mapping.insert(new_tag); | ||
| let parent_idx = self.tag_mapping.get(&parent_tag).unwrap(); | ||
|
|
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 root in self.roots.iter().rev() { | ||
| if Some(*root) == accessed_root { | ||
| continue; | ||
| } | ||
| check_tree(*root)?; |
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 root in self.roots.iter().rev() { | |
| if Some(*root) == accessed_root { | |
| continue; | |
| } | |
| check_tree(*root)?; | |
| for &root in self.roots.iter().rev() { | |
| if Some(root) == accessed_root { | |
| continue; | |
| } | |
| check_tree(root)?; |
| // Performs a foreign read on ref3 and either read on reb1. | ||
| // This temporarily treats ref3 as only foreign. | ||
| let _x = *reb2; | ||
| // Performs an either write on ref3 and reb1. |
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 is an "either write"?
| // This temporarily treats ref3 as only foreign. | ||
| let _x = *reb2; | ||
| // Performs an either write on ref3 and reb1. | ||
| // This should stop treating ref3 as only foreign. |
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.
Why?
| // This access doesn't freeze reb1 even though no access could have come from its | ||
| // child ref3 (since ref3>reb2). | ||
| // | ||
| // ref3 doesn't get frozen, because It's still reserved. |
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.
| // ref3 doesn't get frozen, because It's still reserved. | |
| // ref3 doesn't get frozen because it's still reserved. |
| // └────────────┘ | ||
|
|
||
| // This access doesn't freeze reb1 even though no access could have come from its | ||
| // child ref3 (since ref3>reb2). |
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.
Why does the max_local_access logic not detect this?
|
@rustbot ready |
| access_kind: AccessKind, | ||
| access_cause: AccessCause, | ||
| access_range: Option<AllocRange>, | ||
| access_cause: AccessCause, //diagnostics | ||
| access_range: Option<AllocRange>, //diagnostics | ||
| relatedness: AccessRelatedness, | ||
| span: Span, | ||
| location_range: Range<u64>, | ||
| span: Span, //diagnostics | ||
| location_range: Range<u64>, //diagnostics | ||
| protected: bool, |
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.
It might make sense to move all the diagnostics arguments into a single struct. Since these just get passed through unchanged all the way from Tree::perform_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.
That seems like a good idea for a future PR. :)
Adds proper suport for reborrowing wildcard pointers to tree borrows.