Skip to content

Commit 97261f7

Browse files
committed
better diagnostics for Tree Borrows + int2ptr casts
1 parent dee7e9d commit 97261f7

File tree

3 files changed

+30
-5
lines changed

3 files changed

+30
-5
lines changed

src/bin/miri.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -620,6 +620,14 @@ fn main() {
620620
"-Zmiri-unique-is-unique only has an effect when -Zmiri-tree-borrows is also used"
621621
);
622622
}
623+
// Tree Borrows + permissive provenance does not work.
624+
if miri_config.provenance_mode == ProvenanceMode::Permissive
625+
&& matches!(miri_config.borrow_tracker, Some(BorrowTrackerMethod::TreeBorrows))
626+
{
627+
show_error!(
628+
"Tree Borrows does not support integer-to-pointer casts, and is hence not compatible with permissive provenance"
629+
);
630+
}
623631

624632
debug!("rustc arguments: {:?}", rustc_args);
625633
debug!("crate arguments: {:?}", miri_config.args);

src/borrow_tracker/mod.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -232,6 +232,10 @@ impl GlobalStateInner {
232232
pub fn remove_unreachable_allocs(&mut self, allocs: &LiveAllocs<'_, '_>) {
233233
self.root_ptr_tags.retain(|id, _| allocs.is_live(*id));
234234
}
235+
236+
pub fn borrow_tracker_method(&self) -> BorrowTrackerMethod {
237+
self.borrow_tracker_method
238+
}
235239
}
236240

237241
/// Which borrow tracking method to use

src/diagnostics.rs

Lines changed: 18 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -647,8 +647,8 @@ impl<'tcx> MiriMachine<'tcx> {
647647
};
648648

649649
let helps = match &e {
650-
Int2Ptr { details: true } =>
651-
vec![
650+
Int2Ptr { details: true } => {
651+
let mut v = vec![
652652
(
653653
None,
654654
format!(
@@ -673,13 +673,26 @@ impl<'tcx> MiriMachine<'tcx> {
673673
"you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics"
674674
),
675675
),
676-
(
676+
];
677+
if self.borrow_tracker.as_ref().is_some_and(|b| {
678+
matches!(b.borrow().borrow_tracker_method(), BorrowTrackerMethod::TreeBorrows)
679+
}) {
680+
v.push((
681+
None,
682+
format!(
683+
"Tree Borrows does not support integer-to-pointer casts, so the program is likely to go wrong when this pointer gets used"
684+
),
685+
));
686+
} else {
687+
v.push((
677688
None,
678689
format!(
679690
"alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning"
680691
),
681-
),
682-
],
692+
));
693+
}
694+
v
695+
}
683696
ExternTypeReborrow => {
684697
vec![
685698
(

0 commit comments

Comments
 (0)