initial implementation of wildcard provenence for tree borrows #4630
Conversation
basic tests for wildcard provenance wildcard tracking data structure & expose_tag implementation basic wildcard accesses fix compilation errors & first working testcase comments & protector test update wildcard tracking when neccessary & fix ui tests remove either state move exposed_as to node & use own AccessLevel enum deallocation through wildcards wildcard reborrowing Location struct & comments test for correctly activating through wildcards & fix updating idempotent foreign access compelete verify function use check_nondet helper in a few more places
|
Thank you for contributing to Miri! |
There was a problem hiding this comment.
Here's a first round of comments. I didn't get to the wildcard.rs file yet. Also you did some really deep surgery in this code, much deeper than I expected, so we may have to discuss this in person because this is code I didn't write and therefore don't remember all that much about how it works.
Some general points that I didn't comment on everywhere, but that should be fixed everywhere:
- Please write complete, correctly capitalized and punctuated sentences.
- Please leave empty lines between functions and between types (except when you define a group of types that should be seen as a single unit).
| rustc_args.push(arg); | ||
| } | ||
| } | ||
| // Tree Borrows implies strict provenance, and is not compatible with native calls. |
There was a problem hiding this comment.
native functions are only incompatible with strict provenance? So this check can be removed completely?
There was a problem hiding this comment.
What do you mean?
"Tree Borrows implies strict provenance" is not true any more.
There was a problem hiding this comment.
I'm not familiar with the nativelib interface. So I'm unsure if there is any other reason (besides strict provenance) why tree borrows would be incompatible with nativelib.
I assume there isn't, and I will remove the comment along with the check directly after it.
There was a problem hiding this comment.
Indeed, we can now allow TB + native_lib. (I didn't even realize the check can be removed entirely, I just noted that the comment states an incorrect implication.)
| // The body of this loop needs `borrow_tracker` immutably | ||
| // so we can't move this code inside the following `end_call`. | ||
|
|
||
| // TODO support protected wildcard pointers |
There was a problem hiding this comment.
It's unclear what "support" means.
| /// Which tag the access that caused this error was made through, i.e. | ||
| /// which tag was used to read/write/deallocate. | ||
| pub accessed_info: &'node NodeDebugInfo, | ||
| pub accessed_info: Option<&'node NodeDebugInfo>, |
There was a problem hiding this comment.
This needs an explanation of what None means.
| machine: &MiriMachine<'tcx>, | ||
| ) -> InterpResult<'tcx> { | ||
| // TODO: for now we bail out on wildcard pointers. Eventually we should | ||
| // handle them as much as we can. |
There was a problem hiding this comment.
This comment seems outdated now?
| let orig_tag = match parent_prov { | ||
| ProvenanceExtra::Wildcard => return interp_ok(place.ptr().provenance), // TODO: handle wildcard pointers | ||
| ProvenanceExtra::Concrete(tag) => tag, | ||
| let (orig_tag, provenance) = match parent_prov { |
There was a problem hiding this comment.
So orig_tag is exactly the same as parent_prov except you converted it from ProvenanceExtra to Option...? What's the point of that?
Also, provenance is way to imprecise as a name. There's so many provenances floating around here, this isn't useful. I'd suggest new_prov.
| pub fn dealloc( | ||
| &mut self, | ||
| tag: BorTag, | ||
| tag: Option<BorTag>, |
There was a problem hiding this comment.
It's odd that dealloc changes its signature like this but perform_access does not.
| for (perms_range, Location { perms, .. }) in | ||
| self.rperms.iter_mut(access_range.start, access_range.size) | ||
| { | ||
| let tag = if let Some(tag) = tag { | ||
| tag | ||
| } else { | ||
| // the order in which we check if any nodes are invalidated doesnt matter, | ||
| // so we use the root as a default tag | ||
| self.nodes.get(self.root).unwrap().tag | ||
| }; | ||
| TreeVisitor { | ||
| nodes: &mut self.nodes, | ||
| tag_mapping: &self.tag_mapping, | ||
| perms, | ||
| wildcard_accesses: None, | ||
| } | ||
| .traverse_this_parents_children_other( | ||
| tag, | ||
| // visit all children, skipping none | ||
| |_| ContinueTraversal::Recurse, | ||
| |args: NodeAppArgs<'_>| -> Result<(), TransitionError> { | ||
| let NodeAppArgs { node, perm, .. } = args; | ||
| let perm = perm.get().copied().unwrap_or_else(|| node.default_location_state()); | ||
| if global.borrow().protected_tags.get(&node.tag) |
There was a problem hiding this comment.
This looks like you entirely changed the old logic here... what is happening?
There was a problem hiding this comment.
These changes are mostly whitespace.
Only the let tag = ... on line 787 and wildcard_accesses: None, on line 798 are actual changes.
| if node.is_exposed { | ||
| return None; | ||
| } |
There was a problem hiding this comment.
Why does this make sense? This is definitely non-trivial, therefore needs a comment.
| /// methods for wildcard borrows | ||
| impl<'tcx> Tree { | ||
| /// analogous to `perform_access`, but we do not know from which exposed reference the access happens. | ||
| pub fn perform_wildcard_access( |
There was a problem hiding this comment.
Shouldn't this be in wildcard.rs?
There was a problem hiding this comment.
This is in tree.rs mostly because it accesses private functions of LocationState (perform_access, skip_if_known_noop, record_new_access)
| /// We do not know the accessed pointer, but we know that it is a child of this pointer | ||
| WildcardChildAccess, | ||
| /// We do not know the accessed pointer, but we know that it is foreign to this pointer | ||
| WildcardForeignAccess, |
There was a problem hiding this comment.
Why does it make sense to have these as new variants in this type, rather than having a separate type for the wildcard traversal?
There was a problem hiding this comment.
This way I can reuse the code of perms.rs and LocationState::perform_access directly, which both take a AccessRelatedness as an argument. Also, no code seems to rely on the concrete value of AccessRelatedness. Only if its foreign or child access.
There was a problem hiding this comment.
So could this enum be simplified to just Local vs Foreign?
| // Keep original provenance. | ||
| return interp_ok(place.ptr().provenance); | ||
| } | ||
| }; |
There was a problem hiding this comment.
There is a ptr_try_get_alloc_id above (which github doesn't let me add a comment to -- thanks github) which is subtle and I think not entirely correct. For a wildcard pointer, this will resolve the pointer to an AllocId if it can. If ptr_size is 0, however, that might not be the only legal AllocId!
If the size is 0 on a wildcard pointer I think we have to bail early, there's not much we can do.
3 participants
initial support for wildcard writes in tree borrows.