Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ harness = false
default = ["stack-cache", "native-lib"]
genmc = ["dep:genmc-sys"]
stack-cache = []
stack-cache-consistency-check = ["stack-cache"]
expensive-consistency-checks = ["stack-cache"]
tracing = ["serde_json"]
native-lib = ["dep:libffi", "dep:libloading", "dep:capstone", "dep:ipc-channel", "dep:nix", "dep:serde"]

Expand Down
12 changes: 0 additions & 12 deletions src/bin/miri.rs
Original file line number Diff line number Diff line change
Expand Up @@ -524,7 +524,6 @@ fn main() {
Some(BorrowTrackerMethod::TreeBorrows(TreeBorrowsParams {
precise_interior_mut: true,
}));
miri_config.provenance_mode = ProvenanceMode::Strict;
} else if arg == "-Zmiri-tree-borrows-no-precise-interior-mut" {
match &mut miri_config.borrow_tracker {
Some(BorrowTrackerMethod::TreeBorrows(params)) => {
Expand Down Expand Up @@ -720,17 +719,6 @@ fn main() {
rustc_args.push(arg);
}
}
// Tree Borrows implies strict provenance, and is not compatible with native calls.
if matches!(miri_config.borrow_tracker, Some(BorrowTrackerMethod::TreeBorrows { .. })) {
if miri_config.provenance_mode != ProvenanceMode::Strict {
fatal_error!(
"Tree Borrows does not support integer-to-pointer casts, and hence requires strict provenance"
);
}
if !miri_config.native_lib.is_empty() {
fatal_error!("Tree Borrows is not compatible with calling native functions");
}
}

// Native calls and strict provenance are not compatible.
if !miri_config.native_lib.is_empty() && miri_config.provenance_mode == ProvenanceMode::Strict {
Expand Down
1 change: 1 addition & 0 deletions src/borrow_tracker/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -365,6 +365,7 @@ 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`.

for (alloc_id, tag) in &frame
.extra
.borrow_tracker
Expand Down
10 changes: 5 additions & 5 deletions src/borrow_tracker/stacked_borrows/stack.rs
Original file line number Diff line number Diff line change
Expand Up @@ -153,7 +153,7 @@ impl<'tcx> Stack {
/// Panics if any of the caching mechanisms have broken,
/// - The StackCache indices don't refer to the parallel items,
/// - There are no Unique items outside of first_unique..last_unique
#[cfg(feature = "stack-cache-consistency-check")]
#[cfg(feature = "expensive-consistency-checks")]
fn verify_cache_consistency(&self) {
// Only a full cache needs to be valid. Also see the comments in find_granting_cache
// and set_unknown_bottom.
Expand Down Expand Up @@ -197,7 +197,7 @@ impl<'tcx> Stack {
tag: ProvenanceExtra,
exposed_tags: &FxHashSet<BorTag>,
) -> Result<Option<usize>, ()> {
#[cfg(feature = "stack-cache-consistency-check")]
#[cfg(feature = "expensive-consistency-checks")]
self.verify_cache_consistency();

let ProvenanceExtra::Concrete(tag) = tag else {
Expand Down Expand Up @@ -334,7 +334,7 @@ impl<'tcx> Stack {
// This primes the cache for the next access, which is almost always the just-added tag.
self.cache.add(new_idx, new);

#[cfg(feature = "stack-cache-consistency-check")]
#[cfg(feature = "expensive-consistency-checks")]
self.verify_cache_consistency();
}

Expand Down Expand Up @@ -417,7 +417,7 @@ impl<'tcx> Stack {
self.unique_range.end = self.unique_range.end.min(disable_start);
}

#[cfg(feature = "stack-cache-consistency-check")]
#[cfg(feature = "expensive-consistency-checks")]
self.verify_cache_consistency();

interp_ok(())
Expand Down Expand Up @@ -472,7 +472,7 @@ impl<'tcx> Stack {
self.unique_range = 0..0;
}

#[cfg(feature = "stack-cache-consistency-check")]
#[cfg(feature = "expensive-consistency-checks")]
self.verify_cache_consistency();
interp_ok(())
}
Expand Down
42 changes: 31 additions & 11 deletions src/borrow_tracker/tree_borrows/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -291,9 +291,10 @@ pub(super) struct TbError<'node> {
pub conflicting_info: &'node NodeDebugInfo,
// What kind of access caused this error (read, write, reborrow, deallocation)
pub access_cause: AccessCause,
/// Which tag the access that caused this error was made through, i.e.
/// Which tag if any the access that caused this error was made through, i.e.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should be something like (if any) or , if any,.

/// which tag was used to read/write/deallocate.
pub accessed_info: &'node NodeDebugInfo,
/// Not set on wildcard accesses.
pub accessed_info: Option<&'node NodeDebugInfo>,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This needs an explanation of what None means.

}

impl TbError<'_> {
Expand All @@ -302,10 +303,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
);
Expand All @@ -316,7 +319,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);
Expand All @@ -330,7 +333,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"
Expand All @@ -343,16 +346,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),
Expand All @@ -362,6 +367,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
Expand Down Expand Up @@ -625,8 +645,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<_>>();
Expand Down
Loading
Loading