Skip to content

Commit

Permalink
Auto merge of rust-lang#2195 - RalfJung:vtable-validation, r=RalfJung
Browse files Browse the repository at this point in the history
test for Stacked Borrows error during vtable validation

Fixes rust-lang/miri#2123
Needs rust-lang#97761
  • Loading branch information
bors committed Jun 12, 2022
2 parents 96ee9a0 + 6ed05d9 commit 03a05ae
Show file tree
Hide file tree
Showing 56 changed files with 104 additions and 67 deletions.
2 changes: 1 addition & 1 deletion rust-version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
09d52bc5d4260bac8b9a2ea8ac7a07c5c72906f1
99930ac7f8cbb5d9b319b2e2e92794fd6f24f556
14 changes: 7 additions & 7 deletions src/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -16,10 +16,9 @@ pub enum TerminationInfo {
Exit(i64),
Abort(String),
UnsupportedInIsolation(String),
ExperimentalUb {
StackedBorrowsUb {
msg: String,
help: Option<String>,
url: String,
history: Option<TagHistory>,
},
Deadlock,
Expand All @@ -43,7 +42,7 @@ impl fmt::Display for TerminationInfo {
Exit(code) => write!(f, "the evaluated program completed with exit code {}", code),
Abort(msg) => write!(f, "{}", msg),
UnsupportedInIsolation(msg) => write!(f, "{}", msg),
ExperimentalUb { msg, .. } => write!(f, "{}", msg),
StackedBorrowsUb { msg, .. } => write!(f, "{}", msg),
Deadlock => write!(f, "the evaluated program deadlocked"),
MultipleSymbolDefinitions { link_name, .. } =>
write!(f, "multiple definitions of symbol `{}`", link_name),
Expand Down Expand Up @@ -146,7 +145,7 @@ pub fn report_error<'tcx, 'mir>(
Exit(code) => return Some(*code),
Abort(_) => Some("abnormal termination"),
UnsupportedInIsolation(_) => Some("unsupported operation"),
ExperimentalUb { .. } => Some("Undefined Behavior"),
StackedBorrowsUb { .. } => Some("Undefined Behavior"),
Deadlock => Some("deadlock"),
MultipleSymbolDefinitions { .. } | SymbolShimClashing { .. } => None,
};
Expand All @@ -157,11 +156,12 @@ pub fn report_error<'tcx, 'mir>(
(None, format!("pass the flag `-Zmiri-disable-isolation` to disable isolation;")),
(None, format!("or pass `-Zmiri-isolation-error=warn` to configure Miri to return an error code from isolated operations (if supported for that operation) and continue with a warning")),
],
ExperimentalUb { url, help, history, .. } => {
StackedBorrowsUb { help, history, .. } => {
let url = "https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md";
msg.extend(help.clone());
let mut helps = vec![
(None, format!("this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental")),
(None, format!("see {} for further information", url)),
(None, format!("this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental")),
(None, format!("see {url} for further information")),
];
match history {
Some(TagHistory::Tagged {tag, created: (created_range, created_span), invalidated, protected }) => {
Expand Down
9 changes: 1 addition & 8 deletions src/stacked_borrows.rs
Original file line number Diff line number Diff line change
Expand Up @@ -250,14 +250,7 @@ pub fn err_sb_ub<'tcx>(
help: Option<String>,
history: Option<TagHistory>,
) -> InterpError<'tcx> {
err_machine_stop!(TerminationInfo::ExperimentalUb {
msg,
help,
url: format!(
"https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md"
),
history
})
err_machine_stop!(TerminationInfo::StackedBorrowsUb { msg, help, history })
}

// # Stacked Borrows Core Begin
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/box-cell-alias.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | unsafe { (*ptr).set(20); }
| trying to reborrow <TAG> for SharedReadWrite permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of a reborrow at ALLOC[0x0..0x1]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x1]
--> $DIR/box-cell-alias.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/alias_through_mutation.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | let _val = *target_alias;
| attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of an access at ALLOC[0x0..0x4]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/alias_through_mutation.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/aliasing_mut1.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ error: Undefined Behavior: not granting access to tag <TAG> because incompatible
LL | pub fn safe(_x: &mut i32, _y: &mut i32) {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ not granting access to tag <TAG> because incompatible item is protected: [Unique for <TAG> (call ID)]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/aliasing_mut1.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/aliasing_mut2.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ error: Undefined Behavior: not granting access to tag <TAG> because incompatible
LL | pub fn safe(_x: &i32, _y: &mut i32) {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ not granting access to tag <TAG> because incompatible item is protected: [SharedReadOnly for <TAG> (call ID)]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/aliasing_mut2.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/aliasing_mut3.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | pub fn safe(_x: &mut i32, _y: &i32) {}
| trying to reborrow <untagged> for SharedReadOnly permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of a reborrow at ALLOC[0x0..0x4]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: tag was most recently created at offsets [0x0..0x4]
--> $DIR/aliasing_mut3.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/aliasing_mut4.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ error: Undefined Behavior: not granting access to tag <TAG> because incompatible
LL | pub fn safe(_x: &i32, _y: &mut Cell<i32>) {}
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ not granting access to tag <TAG> because incompatible item is protected: [SharedReadOnly for <TAG> (call ID)]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/aliasing_mut4.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/box_exclusive_violation1.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | *our
| attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of an access at ALLOC[0x0..0x4]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/box_exclusive_violation1.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/buggy_as_mut_slice.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | v1[1] = 5;
| attempting a write access using <TAG> at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
| this error occurs as part of an access at ALLOC[0x4..0x8]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0xc]
--> $DIR/buggy_as_mut_slice.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/buggy_split_at_mut.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | let (a, b) = safe::split_at_mut(&mut array, 0);
| trying to reborrow <TAG> for Unique permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of a reborrow at ALLOC[0x0..0x10]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x10]
--> $DIR/buggy_split_at_mut.rs:LL:CC
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ error: Undefined Behavior: deallocating while item is protected: [Unique for <TA
LL | unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ deallocating while item is protected: [Unique for <TAG> (call ID)]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information

= note: inside `std::alloc::dealloc` at RUSTLIB/alloc/src/alloc.rs:LL:CC
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ error: Undefined Behavior: deallocating while item is protected: [SharedReadWrit
LL | unsafe { __rust_dealloc(ptr, layout.size(), layout.align()) }
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ deallocating while item is protected: [SharedReadWrite for <TAG> (call ID)]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information

= note: inside `std::alloc::dealloc` at RUSTLIB/alloc/src/alloc.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/illegal_read1.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | let _val = *xref; // ...but any use of raw will invalidate our ref.
| attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of an access at ALLOC[0x0..0x4]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/illegal_read1.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/illegal_read2.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | let _val = *xref; // ...but any use of raw will invalidate our ref.
| attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of an access at ALLOC[0x0..0x4]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/illegal_read2.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/illegal_read3.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | let _val = *xref2;
| attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of an access at ALLOC[0x0..0x4]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/illegal_read3.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/illegal_read4.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | let _illegal = *xref2;
| attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of an access at ALLOC[0x0..0x4]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/illegal_read4.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/illegal_read5.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | let _val = *xref; // the mutable one is dead and gone
| attempting a read access using <TAG> at ALLOC[$HEX], but that tag does not exist in the borrow stack for this location
| this error occurs as part of an access at ALLOC[$HEX..$HEX]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [$HEX..$HEX]
--> $DIR/illegal_read5.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/illegal_read6.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | let _val = *raw;
| attempting a read access using <untagged> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of an access at ALLOC[0x0..0x4]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: tag was most recently created at offsets [0x0..0x4]
--> $DIR/illegal_read6.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/illegal_read7.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | let _val = *x.get_mut();
| trying to reborrow <TAG> for SharedReadWrite permission at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of a reborrow at ALLOC[0x0..0x4]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/illegal_read7.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/illegal_read8.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | let _fail = *y1;
| attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of an access at ALLOC[0x0..0x4]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/illegal_read8.rs:LL:CC
Expand Down
2 changes: 1 addition & 1 deletion tests/fail/stacked_borrows/illegal_write1.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LL | let _x = *xref;
| attempting a read access using <TAG> at ALLOC[0x0], but that tag does not exist in the borrow stack for this location
| this error occurs as part of an access at ALLOC[0x0..0x4]
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the rules it violated are still experimental
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
= help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <TAG> was created by a retag at offsets [0x0..0x4]
--> $DIR/illegal_write1.rs:LL:CC
Expand Down
Loading

0 comments on commit 03a05ae

Please sign in to comment.