Tree Borrows: multiple invalid exposed nodes on main subtree #4757

royAmmerschuber · 2025-12-10T16:10:59Z

If there is no exposed node on the main subtree that allows a child write, then a wildcard access to the tree is invalid.
This wasn't caught before if there were multiple exposed nodes in the main subtree whose tag was larger than the accessed tag.

rustbot · 2025-12-10T16:11:03Z

Thank you for contributing to Miri! A reviewer will take a look at your PR, typically within a week or two.
Please remember to not force-push to the PR branch except when you need to rebase due to a conflict or when the reviewer asks you for it.

RalfJung

Thanks! I can follow the logic. However, is there any way to generalize this so it doesn't just work for the main tree? Currently it looks like a pretty ad-hoc special case, and there are probably many of those that we could add.

I'm also confused by the PR title. This is about whether there's any eligible exposed node on the main tree, right? Why do you talk about "multiple"?

This wasn't caught before if there were multiple exposed nodes in the main subtree whose tag was larger than the accessed tag.

Are you saying this was caught if there was exactly one exposed node in the main subtree whose tag was larger than the accessed tag? How?

View changes since this review

RalfJung · 2025-12-13T08:59:34Z

src/borrow_tracker/tree_borrows/tree.rs

+                if node.is_exposed
+                    && perm.permission.strongest_allowed_child_access(protected)
+                        >= access_kind.into()
+                    && max_local_tag.is_none_or(|max_local_tag| max_local_tag > node.tag)


Suggested change

&& max_local_tag.is_none_or(|max_local_tag| max_local_tag > node.tag)

&& max_local_tag.is_none_or(|max_local_tag| max_local_tag >= node.tag)

The max-local-tag itself can be the souce of local accesses, right?

max_local_tag is actually never equal to node.tag as we only call perform_wildcard_access on the trees which don't contain max_local_tag. But >= is more fitting for the name of max_local_tag so ill change this.

RalfJung · 2025-12-13T09:00:21Z

src/borrow_tracker/tree_borrows/tree.rs

+            // Check that this is the main subtree.
+            && self
+                .wildcard_accesses
+                .get(root)
+                .unwrap()
+                .access_relatedness(access_kind, true)
+                .is_none()


How does this check that it is the main tree...?

This checks if no foreign access is possible on the root of the subtree. Only the main subtree doesn't allow foreign accesses, so if access_relatedness() is None then root is the main root.
I should add a comment to the bool flag (/* only_foreign */). Or I could make max_foreign_access public and read that directly.

This way it's implemented technically makes it generic to all subtrees, But the only one it actually effects is the main subtree.

The main problem here is that comment ant code don't match. Given that code, the comment should explain why this is correct for any tree that does not allow foreign accesses at the root.

RalfJung · 2025-12-13T09:01:29Z

src/borrow_tracker/tree_borrows/wildcard.rs

    Read,
    Write,
 }
+impl From<AccessKind> for WildcardAccessLevel {


If we have to start converting between them, there's not really any point any more in them being different types.

We could replace WildcardAccessLevel with Option<AccessKind>. We would have to implement Ord for AccessKind and rely on Option's Ord implementation, but I think that would still be the correct logic.

I do think it makes sense to keep the types separate since they represent different things. Access kind is the type of a concrete access, while access level represents the highest allowed access that is possible.

I only use this implementation to check if an access kind is allowed under a specific access level. Maybe I should replace this with a method access_level.allows(access_kind).

I only use this implementation to check if an access kind is allowed under a specific access level. Maybe I should replace this with a method access_level.allows(access_kind).

That would also be reasonable.

RalfJung · 2025-12-13T09:02:24Z

src/borrow_tracker/tree_borrows/tree.rs

+
+                // We only count exposed nodes through which an access could happen.
+                if node.is_exposed
+                    && perm.permission.strongest_allowed_child_access(protected)


We should probably rename that method to include wildcard; it's currently confusing when one reads this code and tries to understand it without knowing exactly by heart what each function does.

I forgot to rename this function to strongest_allowed_local_access which would be the correct term. I think the function name (at least with this change) already tells you exactly what the function does.

Hm, I see... but then it is somewhat confusing that it returns a WildcardAccess.

royAmmerschuber · 2025-12-14T14:35:31Z

However, is there any way to generalize this so it doesn't just work for the main tree? Currently it looks like a pretty ad-hoc special case, and there are probably many of those that we could add.

This PR is trying to better approximate the ideal version of the algorithm (where we recalculate the wildcard data structure before each access).
It should now return a no_valid_exposed_references_error() in the same cases as the ideal algorithm. It doesn't cover the cases where a TransitionError would get returned, but for these there is no easy way to check them, so we would probably have to implement the ideal algorithm directly.

As for this only being implemented for the main subtree. This error already never gets raised on the other subtrees. An access is UB if there exist no valid exposed nodes on the main subtree, even if there are valid exposed nodes on other subtrees. This is because those other subtrees would also have to be attached to one of the valid exposed nodes on the main subtree.

I'm also confused by the PR title. This is about whether there's any eligible exposed node on the main tree, right? Why do you talk about "multiple"?

Are you saying this was caught if there was exactly one exposed node in the main subtree whose tag was larger than the accessed tag? How?

Yes, it's already handled for the single invalid exposed case (see test case cross_tree_update_main_invalid_exposed.rs). In the single case when we try to calculate the relatedness for the invalid exposed node we know that neither a local (because it's invalid) nor a foreign (because it's the only exposed node on the main subtree) access could happen so its UB.
However, if this node has an invalid exposed cousin, then it thinks a foreign access could have happened from that cousin.

RalfJung · 2025-12-15T13:53:34Z

This PR is trying to better approximate the ideal version of the algorithm (where we recalculate the wildcard data structure before each access).
It should now return a no_valid_exposed_references_error() in the same cases as the ideal algorithm.

I like that way of framing it, thanks. However, I would say the ideal (or rather, idealized) algorithm would just not have the data structure at all and do nested tree traversals.

This should be reflected in the comments.

royAmmerschuber added 2 commits December 10, 2025 09:39

detect properly if there are valid exposed nodes

4352e93

add comments

55e4fb5

rustbot added the S-waiting-on-review Status: Waiting for a review to complete label Dec 10, 2025

fix rebase issues

dc8d21f

RalfJung reviewed Dec 13, 2025

View reviewed changes

RalfJung added S-waiting-on-author Status: Waiting for the PR author to address review comments and removed S-waiting-on-review Status: Waiting for a review to complete labels Dec 13, 2025

	&& max_local_tag.is_none_or(\|max_local_tag\| max_local_tag > node.tag)
	&& max_local_tag.is_none_or(\|max_local_tag\| max_local_tag >= node.tag)

Tree Borrows: multiple invalid exposed nodes on main subtree #4757

Are you sure you want to change the base?

Tree Borrows: multiple invalid exposed nodes on main subtree #4757

Conversation

royAmmerschuber commented Dec 10, 2025

Uh oh!

rustbot commented Dec 10, 2025

Uh oh!

RalfJung left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

royAmmerschuber commented Dec 14, 2025

Uh oh!

RalfJung commented Dec 15, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

RalfJung left a comment •

edited

Loading

RalfJung commented Dec 15, 2025 •

edited

Loading