Skip to content

Commit ab579e4

Browse files
committed
Include the ID of the created tag in TB's Reborrow events
1 parent bbdeaef commit ab579e4

27 files changed

+52
-47
lines changed

src/borrow_tracker/tree_borrows/diagnostics.rs

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@ use crate::*;
1515
#[derive(Clone, Copy, Debug)]
1616
pub enum AccessCause {
1717
Explicit(AccessKind),
18-
Reborrow,
18+
Reborrow(BorTag),
1919
Dealloc,
2020
FnExit(AccessKind),
2121
}
@@ -24,7 +24,7 @@ impl fmt::Display for AccessCause {
2424
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
2525
match self {
2626
Self::Explicit(kind) => write!(f, "{kind}"),
27-
Self::Reborrow => write!(f, "reborrow"),
27+
Self::Reborrow(tag) => write!(f, "reborrow to create {tag:?}"),
2828
Self::Dealloc => write!(f, "deallocation"),
2929
// This is dead code, since the protector release access itself can never
3030
// cause UB (while the protector is active, if some other access invalidates
@@ -40,7 +40,8 @@ impl AccessCause {
4040
let rel = if is_foreign { "foreign" } else { "child" };
4141
match self {
4242
Self::Explicit(kind) => format!("{rel} {kind}"),
43-
Self::Reborrow => format!("reborrow (acting as a {rel} read access)"),
43+
Self::Reborrow(tag) =>
44+
format!("reborrow to create {tag:?} (acting as a {rel} read access)"),
4445
Self::Dealloc => format!("deallocation (acting as a {rel} write access)"),
4546
Self::FnExit(kind) => format!("protector release (acting as a {rel} {kind})"),
4647
}

src/borrow_tracker/tree_borrows/mod.rs

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -375,7 +375,11 @@ trait EvalContextPrivExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
375375

376376
tree_borrows.perform_access(
377377
orig_tag,
378-
Some((range_in_alloc, AccessKind::Read, diagnostics::AccessCause::Reborrow)),
378+
Some((
379+
range_in_alloc,
380+
AccessKind::Read,
381+
diagnostics::AccessCause::Reborrow(new_tag),
382+
)),
379383
this.machine.borrow_tracker.as_ref().unwrap(),
380384
alloc_id,
381385
this.machine.current_span(),

tests/fail/async-shared-mutable.tree.stderr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ help: the accessed tag <TAG> later transitioned to Active due to a child write a
2121
LL | *x = 1;
2222
| ^^^^^^
2323
= help: this transition corresponds to the first write to a 2-phase borrowed mutable reference
24-
help: the accessed tag <TAG> later transitioned to Frozen due to a reborrow (acting as a foreign read access) at offsets [OFFSET]
24+
help: the accessed tag <TAG> later transitioned to Frozen due to a reborrow to create <TAG> (acting as a foreign read access) at offsets [OFFSET]
2525
--> tests/fail/async-shared-mutable.rs:LL:CC
2626
|
2727
LL | let _: Pin<&_> = f.as_ref(); // Or: `f.as_mut().into_ref()`.

tests/fail/both_borrows/aliasing_mut1.tree.stderr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ help: the accessed tag <TAG> was created here, in the initial state Reserved
1111
|
1212
LL | pub fn safe(x: &mut i32, y: &mut i32) {
1313
| ^
14-
help: the accessed tag <TAG> later transitioned to Reserved (conflicted) due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
14+
help: the accessed tag <TAG> later transitioned to Reserved (conflicted) due to a reborrow to create <TAG> (acting as a foreign read access) at offsets [0x0..0x4]
1515
--> tests/fail/both_borrows/aliasing_mut1.rs:LL:CC
1616
|
1717
LL | pub fn safe(x: &mut i32, y: &mut i32) {

tests/fail/both_borrows/aliasing_mut3.tree.stderr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,7 @@ help: the accessed tag <TAG> was created here, in the initial state Reserved
1111
|
1212
LL | pub fn safe(x: &mut i32, y: &i32) {
1313
| ^
14-
help: the accessed tag <TAG> later transitioned to Reserved (conflicted) due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
14+
help: the accessed tag <TAG> later transitioned to Reserved (conflicted) due to a reborrow to create <TAG> (acting as a foreign read access) at offsets [0x0..0x4]
1515
--> tests/fail/both_borrows/aliasing_mut3.rs:LL:CC
1616
|
1717
LL | pub fn safe(x: &mut i32, y: &i32) {

tests/fail/both_borrows/load_invalid_shr.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,5 +12,5 @@ fn main() {
1212
unsafe { *xraw = 42 }; // unfreeze
1313
let _val = *xref_in_mem;
1414
//~[stack]^ ERROR: /retag .* tag does not exist in the borrow stack/
15-
//~[tree]| ERROR: /reborrow through .* is forbidden/
15+
//~[tree]| ERROR: /reborrow to create .* through .* is forbidden/
1616
}

tests/fail/both_borrows/load_invalid_shr.tree.stderr

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,11 @@
1-
error: Undefined Behavior: reborrow through <TAG> at ALLOC[0x0] is forbidden
1+
error: Undefined Behavior: reborrow to create <TAG> through <TAG> at ALLOC[0x0] is forbidden
22
--> tests/fail/both_borrows/load_invalid_shr.rs:LL:CC
33
|
44
LL | let _val = *xref_in_mem;
5-
| ^^^^^^^^^^^^ reborrow through <TAG> at ALLOC[0x0] is forbidden
5+
| ^^^^^^^^^^^^ reborrow to create <TAG> through <TAG> at ALLOC[0x0] is forbidden
66
|
77
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
8-
= help: the accessed tag <TAG> has state Disabled which forbids this reborrow (acting as a child read access)
8+
= help: the accessed tag <TAG> has state Disabled which forbids this reborrow to create <TAG> (acting as a child read access)
99
help: the accessed tag <TAG> was created here, in the initial state Frozen
1010
--> tests/fail/both_borrows/load_invalid_shr.rs:LL:CC
1111
|

tests/fail/both_borrows/newtype_pair_retagging.tree.stderr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ help: the protected tag <TAG> was created here, in the initial state Reserved
1818
|
1919
LL | fn dealloc_while_running(_n: Newtype<'_>, dealloc: impl FnOnce()) {
2020
| ^^
21-
help: the protected tag <TAG> later transitioned to Reserved (conflicted) due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
21+
help: the protected tag <TAG> later transitioned to Reserved (conflicted) due to a reborrow to create <TAG> (acting as a foreign read access) at offsets [0x0..0x4]
2222
--> tests/fail/both_borrows/newtype_pair_retagging.rs:LL:CC
2323
|
2424
LL | || drop(Box::from_raw(ptr)),

tests/fail/both_borrows/newtype_retagging.tree.stderr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ help: the protected tag <TAG> was created here, in the initial state Reserved
1818
|
1919
LL | fn dealloc_while_running(_n: Newtype<'_>, dealloc: impl FnOnce()) {
2020
| ^^
21-
help: the protected tag <TAG> later transitioned to Reserved (conflicted) due to a reborrow (acting as a foreign read access) at offsets [0x0..0x4]
21+
help: the protected tag <TAG> later transitioned to Reserved (conflicted) due to a reborrow to create <TAG> (acting as a foreign read access) at offsets [0x0..0x4]
2222
--> tests/fail/both_borrows/newtype_retagging.rs:LL:CC
2323
|
2424
LL | || drop(Box::from_raw(ptr)),

tests/fail/both_borrows/pass_invalid_shr.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,5 +11,5 @@ fn main() {
1111
unsafe { *xraw = 42 }; // unfreeze
1212
foo(xref);
1313
//~[stack]^ ERROR: /retag .* tag does not exist in the borrow stack/
14-
//~[tree]| ERROR: /reborrow through .* is forbidden/
14+
//~[tree]| ERROR: /reborrow to create .* through .* is forbidden/
1515
}

0 commit comments

Comments
 (0)