-
Notifications
You must be signed in to change notification settings - Fork 445
Simplify wildcard datastructure. #4851
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?
Simplify wildcard datastructure. #4851
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.
That's a very nice overall code reduction :)
| /// | ||
| /// NOTE: same guarantees on entry initialization as for `perms`. | ||
| pub wildcard_accesses: UniValMap<WildcardState>, | ||
| /// Stores how nodes are related to exposed nodes, |
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.
| /// Stores how nodes are related to exposed nodes, | |
| /// Stores how nodes are related to exposed nodes. |
| @@ -1180,14 +1186,7 @@ impl<'tcx> LocationTree { | |||
| // as a foreign access, and if not, then we can error. | |||
| // In practice, all wildcard trees accept foreign accesses, but the main tree does | |||
| // not, so this catches UB when none of the nodes in the main tree allows this 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.
This comment is outdated now. Why did you change this to instead pass around a boolean?
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.
Previously we checked the max_foreign_access field which would be set to Write on wildcard roots. This PR removes max_foreign_access from WildcardState so we can't use that anymore.
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, makes sense. Please update the comment then.
| } | ||
| } else { | ||
| relatedness | ||
| } |
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 seems to move some of the logic of determining the relatedness here into tree.rs. Seems better to have that in a helper in wildcard.rs like before.
| /// that is foreign to this node. | ||
| /// Only gets allocated if we add an exposed node. | ||
| #[derive(Clone, Debug, Default, PartialEq, Eq)] | ||
| pub struct WildcardData(UniValMap<WildcardState>); |
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 generally define types before using them. WildcardState as at the end of the file so currently one has to jump around a lot to understand this code.
| /// How many local nodes are exposed with read permissions. | ||
| local_reads: u16, | ||
| } | ||
| impl 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.
| impl Tree { | |
| impl Tree { |
| // When the first tag gets exposed then we initialize the | ||
| // wildcard state for every node and location in the 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.
This doesn't seem to be correct? We're only initializing it from the exposed node upwards.
| let old_access_type = perm.strongest_allowed_local_access(true); | ||
| let access_type = perm.strongest_allowed_local_access(false); |
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 those boolean arguments.
| .map(|id| wildcard_accesses.0.get(id).cloned().unwrap_or_default()) | ||
| .fold((0, 0), |acc, wc| (acc.0 + wc.local_reads, acc.1 + wc.local_writes)); | ||
| let expected_reads = | ||
| child_reads + Into::<u16>::into(exposed_as >= WildcardAccessLevel::Read); |
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.
| child_reads + Into::<u16>::into(exposed_as >= WildcardAccessLevel::Read); | |
| child_reads + u16::from(exposed_as >= WildcardAccessLevel::Read); |
Same below
| @@ -451,19 +445,6 @@ impl<'tcx> 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.
| // We don't have to update `wildcard_accesses` as the new node is not exposed and | |
| // has no children so the default counts of 0 are correct. | |
| /// NOTE: same guarantees on entry initialization as for `perms`. | ||
| pub wildcard_accesses: UniValMap<WildcardState>, | ||
| /// Stores how nodes are related to exposed nodes, | ||
| pub wildcard_accesses: WildcardData, |
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 name of the field and the type are inconsistent.
And generally this is more about exposed nodes than about wildcard pointers, so maybe the name should reflect that? Something like exposed_cache: ExposedNodeCache or so? It's a cache in the sense that it just caches information that could also be recomputed.
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 think it makes sense to change it to wildcard_cache as a name. I feel like exposed is a too general term considering this specifically tracks the relatedness for a wildcard access.
This also means the doc-comment is wrong as we only care about exposed nodes through which an access is possible.
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 specifically tracks how many accessible exposed children every node has. So having "exposed" in the name seems quite apt to me?
Makes it so that each node only needs to count all local exposed nodes instead of also keeping track of foreign nodes. This makes the update logic significantly simpler.