-
Notifications
You must be signed in to change notification settings - Fork 399
initial implementation of wildcard provenence for tree borrows #4630
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?
Changes from 3 commits
fdf62f8
165a18a
0d40e7b
e518de0
66aa932
fd2438b
fd1f4f7
adab680
3c3f264
a52fde6
121b535
90e30fd
c572e06
d52c0fc
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -365,6 +365,8 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> { | |
| let borrow_tracker = this.machine.borrow_tracker.as_ref().unwrap(); | ||
| // 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 | ||
|
||
| for (alloc_id, tag) in &frame | ||
| .extra | ||
| .borrow_tracker | ||
|
|
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -293,7 +293,7 @@ pub(super) struct TbError<'node> { | |
| pub access_cause: AccessCause, | ||
| /// 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. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This needs an explanation of what |
||
| } | ||
|
|
||
| impl TbError<'_> { | ||
|
|
@@ -302,10 +302,12 @@ impl TbError<'_> { | |
| use TransitionError::*; | ||
| let cause = self.access_cause; | ||
| let accessed = self.accessed_info; | ||
| let accessed_str = | ||
| self.accessed_info.map(|v| format!("{v}")).unwrap_or_else(|| "wildcard".into()); | ||
| let conflicting = self.conflicting_info; | ||
| let accessed_is_conflicting = accessed.tag == conflicting.tag; | ||
| let accessed_is_conflicting = accessed.map(|a| a.tag == conflicting.tag).unwrap_or(false); | ||
| let title = format!( | ||
| "{cause} through {accessed} at {alloc_id:?}[{offset:#x}] is forbidden", | ||
| "{cause} through {accessed_str} at {alloc_id:?}[{offset:#x}] is forbidden", | ||
| alloc_id = self.alloc_id, | ||
| offset = self.error_offset | ||
| ); | ||
|
|
@@ -316,7 +318,7 @@ impl TbError<'_> { | |
| let mut details = Vec::new(); | ||
| if !accessed_is_conflicting { | ||
| details.push(format!( | ||
| "the accessed tag {accessed} is a child of the conflicting tag {conflicting}" | ||
| "the accessed tag {accessed_str} is a child of the conflicting tag {conflicting}" | ||
| )); | ||
| } | ||
| let access = cause.print_as_access(/* is_foreign */ false); | ||
|
|
@@ -330,7 +332,7 @@ impl TbError<'_> { | |
| let access = cause.print_as_access(/* is_foreign */ true); | ||
| let details = vec![ | ||
| format!( | ||
| "the accessed tag {accessed} is foreign to the {conflicting_tag_name} tag {conflicting} (i.e., it is not a child)" | ||
| "the accessed tag {accessed_str} is foreign to the {conflicting_tag_name} tag {conflicting} (i.e., it is not a child)" | ||
| ), | ||
| format!( | ||
| "this {access} would cause the {conflicting_tag_name} tag {conflicting} (currently {before_disabled}) to become Disabled" | ||
|
|
@@ -343,16 +345,18 @@ impl TbError<'_> { | |
| let conflicting_tag_name = "strongly protected"; | ||
| let details = vec![ | ||
| format!( | ||
| "the allocation of the accessed tag {accessed} also contains the {conflicting_tag_name} tag {conflicting}" | ||
| "the allocation of the accessed tag {accessed_str} also contains the {conflicting_tag_name} tag {conflicting}" | ||
| ), | ||
| format!("the {conflicting_tag_name} tag {conflicting} disallows deallocations"), | ||
| ]; | ||
| (title, details, conflicting_tag_name) | ||
| } | ||
| }; | ||
| let mut history = HistoryData::default(); | ||
| if !accessed_is_conflicting { | ||
| history.extend(self.accessed_info.history.forget(), "accessed", false); | ||
| if let Some(accessed_info) = self.accessed_info | ||
| && !accessed_is_conflicting | ||
| { | ||
| history.extend(accessed_info.history.forget(), "accessed", false); | ||
| } | ||
| history.extend( | ||
| self.conflicting_info.history.extract_relevant(self.error_offset, self.error_kind), | ||
|
|
@@ -362,6 +366,21 @@ impl TbError<'_> { | |
| err_machine_stop!(TerminationInfo::TreeBorrowsUb { title, details, history }) | ||
| } | ||
| } | ||
| /// Cannot access this allocation with wildcard provenance, as there are no | ||
| /// Valid exposed references for this access kind. | ||
| pub fn no_valid_exposed_references_error<'tcx>( | ||
| alloc_id: AllocId, | ||
| offset: u64, | ||
| access_cause: AccessCause, | ||
| ) -> InterpErrorKind<'tcx> { | ||
| let title = | ||
| format!("{access_cause} through wildcard at {alloc_id:?}[{offset:#x}] is forbidden"); | ||
| let details = vec![format!( | ||
| "there are no exposed references who have {access_cause} permissions to this location" | ||
| )]; | ||
| let history = HistoryData::default(); | ||
| err_machine_stop!(TerminationInfo::TreeBorrowsUb { title, details, history }) | ||
| } | ||
|
|
||
| type S = &'static str; | ||
| /// Pretty-printing details | ||
|
|
@@ -625,8 +644,8 @@ impl DisplayRepr { | |
| let rperm = tree | ||
| .rperms | ||
| .iter_all() | ||
| .map(move |(_offset, perms)| { | ||
| let perm = perms.get(idx); | ||
| .map(move |(_offset, loc)| { | ||
| let perm = loc.perms.get(idx); | ||
| perm.cloned() | ||
| }) | ||
| .collect::<Vec<_>>(); | ||
|
|
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -14,6 +14,7 @@ mod foreign_access_skipping; | |
| mod perms; | ||
| mod tree; | ||
| mod unimap; | ||
| mod wildcard; | ||
|
|
||
| #[cfg(test)] | ||
| mod exhaustive; | ||
|
|
@@ -54,21 +55,25 @@ impl<'tcx> Tree { | |
| interpret::Pointer::new(alloc_id, range.start), | ||
| range.size.bytes(), | ||
| ); | ||
| // TODO: for now we bail out on wildcard pointers. Eventually we should | ||
| // handle them as much as we can. | ||
| let tag = match prov { | ||
| ProvenanceExtra::Concrete(tag) => tag, | ||
| ProvenanceExtra::Wildcard => return interp_ok(()), | ||
| }; | ||
| let global = machine.borrow_tracker.as_ref().unwrap(); | ||
| let span = machine.current_user_relevant_span(); | ||
| self.perform_access( | ||
| tag, | ||
| Some((range, access_kind, diagnostics::AccessCause::Explicit(access_kind))), | ||
| global, | ||
| alloc_id, | ||
| span, | ||
| ) | ||
| match prov { | ||
| ProvenanceExtra::Concrete(tag) => | ||
| self.perform_access( | ||
| tag, | ||
| Some((range, access_kind, diagnostics::AccessCause::Explicit(access_kind))), | ||
| global, | ||
| alloc_id, | ||
| span, | ||
| ), | ||
| ProvenanceExtra::Wildcard => | ||
| self.perform_wildcard_access( | ||
| Some((range, access_kind, diagnostics::AccessCause::Explicit(access_kind))), | ||
| global, | ||
| alloc_id, | ||
| span, | ||
| ), | ||
| } | ||
| } | ||
|
|
||
| /// Check that this pointer has permission to deallocate this range. | ||
|
|
@@ -82,18 +87,14 @@ impl<'tcx> Tree { | |
| // TODO: for now we bail out on wildcard pointers. Eventually we should | ||
| // handle them as much as we can. | ||
|
||
| let tag = match prov { | ||
| ProvenanceExtra::Concrete(tag) => tag, | ||
| ProvenanceExtra::Wildcard => return interp_ok(()), | ||
| ProvenanceExtra::Concrete(tag) => Some(tag), | ||
| ProvenanceExtra::Wildcard => None, | ||
| }; | ||
| let global = machine.borrow_tracker.as_ref().unwrap(); | ||
| let span = machine.current_user_relevant_span(); | ||
| self.dealloc(tag, alloc_range(Size::ZERO, size), global, alloc_id, span) | ||
| } | ||
|
|
||
| pub fn expose_tag(&mut self, _tag: BorTag) { | ||
| // TODO | ||
| } | ||
|
|
||
| /// A tag just lost its protector. | ||
| /// | ||
| /// This emits a special kind of access that is only applied | ||
|
|
@@ -252,10 +253,12 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> { | |
| }; | ||
|
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. There is a If the size is 0 on a wildcard pointer I think we have to bail early, there's not much we can do. |
||
| log_creation(this, Some((alloc_id, base_offset, parent_prov)))?; | ||
|
|
||
| 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 { | ||
|
||
| ProvenanceExtra::Wildcard => (None, Provenance::Wildcard), // TODO: handle wildcard pointers | ||
|
||
| ProvenanceExtra::Concrete(tag) => | ||
| (Some(tag), Provenance::Concrete { alloc_id, tag: new_tag }), | ||
| }; | ||
| let is_wildcard = orig_tag.is_none(); | ||
|
|
||
| trace!( | ||
| "reborrow: reference {:?} derived from {:?} (pointee {}): {:?}, size {}", | ||
|
|
@@ -266,7 +269,8 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> { | |
| ptr_size.bytes() | ||
| ); | ||
|
|
||
| if let Some(protect) = new_perm.protector { | ||
| // TODO support protecting wildcard pointers. | ||
| if !is_wildcard && let Some(protect) = new_perm.protector { | ||
| // We register the protection in two different places. | ||
| // This makes creating a protector slower, but checking whether a tag | ||
| // is protected faster. | ||
|
|
@@ -291,7 +295,7 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> { | |
| assert_eq!(ptr_size, Size::ZERO); // we did the deref check above, size has to be 0 here | ||
| // There's not actually any bytes here where accesses could even be tracked. | ||
| // Just produce the new provenance, nothing else to do. | ||
| return interp_ok(Some(Provenance::Concrete { alloc_id, tag: new_tag })); | ||
| return interp_ok(Some(provenance)); | ||
| } | ||
|
|
||
| let protected = new_perm.protector.is_some(); | ||
|
|
@@ -354,14 +358,30 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> { | |
| start: Size::from_bytes(perm_range.start) + base_offset, | ||
| size: Size::from_bytes(perm_range.end - perm_range.start), | ||
| }; | ||
|
|
||
| tree_borrows.perform_access( | ||
| orig_tag, | ||
| Some((range_in_alloc, AccessKind::Read, diagnostics::AccessCause::Reborrow)), | ||
| this.machine.borrow_tracker.as_ref().unwrap(), | ||
| alloc_id, | ||
| this.machine.current_user_relevant_span(), | ||
| )?; | ||
| if let Some(orig_tag) = orig_tag { | ||
| tree_borrows.perform_access( | ||
| orig_tag, | ||
| Some(( | ||
| range_in_alloc, | ||
| AccessKind::Read, | ||
| diagnostics::AccessCause::Reborrow, | ||
| )), | ||
| this.machine.borrow_tracker.as_ref().unwrap(), | ||
| alloc_id, | ||
| this.machine.current_user_relevant_span(), | ||
| )?; | ||
| } else { | ||
| tree_borrows.perform_wildcard_access( | ||
|
||
| Some(( | ||
| range_in_alloc, | ||
| AccessKind::Read, | ||
| diagnostics::AccessCause::Reborrow, | ||
| )), | ||
| this.machine.borrow_tracker.as_ref().unwrap(), | ||
| alloc_id, | ||
| this.machine.current_user_relevant_span(), | ||
| )?; | ||
| } | ||
|
|
||
| // Also inform the data race model (but only if any bytes are actually affected). | ||
| if range_in_alloc.size.bytes() > 0 { | ||
|
|
@@ -377,20 +397,20 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> { | |
| } | ||
| } | ||
| } | ||
|
|
||
| // Record the parent-child pair in the tree. | ||
| tree_borrows.new_child( | ||
| base_offset, | ||
| orig_tag, | ||
| new_tag, | ||
| inside_perms, | ||
| new_perm.outside_perm, | ||
| protected, | ||
| this.machine.current_user_relevant_span(), | ||
| )?; | ||
| if let Some(orig_tag) = orig_tag { | ||
| // Record the parent-child pair in the tree. | ||
| tree_borrows.new_child( | ||
| base_offset, | ||
| orig_tag, | ||
| new_tag, | ||
| inside_perms, | ||
| new_perm.outside_perm, | ||
| protected, | ||
| this.machine.current_user_relevant_span(), | ||
| )?; | ||
| } | ||
| drop(tree_borrows); | ||
|
|
||
|
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. That empty line was deliberate. Empty lines serve to separate logically distinct sections of code, similar to paragraphs in a text. Please only remove empty lines if they no longer serve that purpose. |
||
| interp_ok(Some(Provenance::Concrete { alloc_id, tag: new_tag })) | ||
| interp_ok(Some(provenance)) | ||
| } | ||
|
|
||
| fn tb_retag_place( | ||
|
|
||
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 now outdated.
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.
native functions are only incompatible with strict provenance? So this check can be removed completely?
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 do you mean?
"Tree Borrows implies strict provenance" is not true any more.
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 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.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.)