Skip to content
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

Stacked Borrows: make scalar field retagging the default #2636

Merged
merged 1 commit into from
Oct 29, 2022
Merged
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
7 changes: 4 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -374,14 +374,15 @@ to Miri failing to detect cases of undefined behavior in a program.
application instead of raising an error within the context of Miri (and halting
execution). Note that code might not expect these operations to ever panic, so
this flag can lead to strange (mis)behavior.
* `-Zmiri-retag-fields` changes Stacked Borrows retagging to recurse into fields.
* `-Zmiri-retag-fields` changes Stacked Borrows retagging to recurse into *all* fields.
This means that references in fields of structs/enums/tuples/arrays/... are retagged,
and in particular, they are protected when passed as function arguments.
(The default is to recurse only in cases where rustc would actually emit a `noalias` attribute.)
* `-Zmiri-retag-fields=<all|none|scalar>` controls when Stacked Borrows retagging recurses into
fields. `all` means it always recurses (like `-Zmiri-retag-fields`), `none` means it never
recurses (the default), `scalar` means it only recurses for types where we would also emit
recurses, `scalar` (the default) means it only recurses for types where we would also emit
`noalias` annotations in the generated LLVM IR (types passed as indivudal scalars or pairs of
scalars).
scalars). Setting this to `none` is **unsound**.
* `-Zmiri-tag-gc=<blocks>` configures how often the pointer tag garbage collector runs. The default
is to search for and remove unreachable tags once every `10000` basic blocks. Setting this to
`0` disables the garbage collector, which causes some programs to have explosive memory usage
Expand Down
2 changes: 1 addition & 1 deletion src/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -163,7 +163,7 @@ impl Default for MiriConfig {
mute_stdout_stderr: false,
preemption_rate: 0.01, // 1%
report_progress: None,
retag_fields: RetagFields::No,
retag_fields: RetagFields::OnlyScalar,
external_so_file: None,
gc_interval: 10_000,
num_cpus: 1,
Expand Down
1 change: 0 additions & 1 deletion tests/fail/stacked_borrows/newtype_pair_retagging.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
//@compile-flags: -Zmiri-retag-fields=scalar
//@error-pattern: which is protected
struct Newtype<'a>(&'a mut i32, i32);

Expand Down
1 change: 0 additions & 1 deletion tests/fail/stacked_borrows/newtype_retagging.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
//@compile-flags: -Zmiri-retag-fields=scalar
//@error-pattern: which is protected
struct Newtype<'a>(&'a mut i32);

Expand Down
5 changes: 2 additions & 3 deletions tests/fail/stacked_borrows/return_invalid_mut_option.rs
Original file line number Diff line number Diff line change
@@ -1,16 +1,15 @@
// Make sure that we cannot return a `&mut` that got already invalidated, not even in an `Option`.
// Due to shallow reborrowing, the error only surfaces when we look into the `Option`.
fn foo(x: &mut (i32, i32)) -> Option<&mut i32> {
let xraw = x as *mut (i32, i32);
let ret = unsafe { &mut (*xraw).1 }; // let-bind to avoid 2phase
let ret = Some(ret);
let _val = unsafe { *xraw }; // invalidate xref
ret
ret //~ ERROR: /retag .* tag does not exist in the borrow stack/
}

fn main() {
match foo(&mut (1, 2)) {
Some(_x) => {} //~ ERROR: /retag .* tag does not exist in the borrow stack/
Some(_x) => {}
None => {}
}
}
19 changes: 12 additions & 7 deletions tests/fail/stacked_borrows/return_invalid_mut_option.stderr
Original file line number Diff line number Diff line change
@@ -1,26 +1,31 @@
error: Undefined Behavior: trying to retag from <TAG> for Unique permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
--> $DIR/return_invalid_mut_option.rs:LL:CC
|
LL | Some(_x) => {}
| ^^
| |
| trying to retag from <TAG> for Unique permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag at ALLOC[0x4..0x8]
LL | ret
| ^^^
| |
| trying to retag from <TAG> for Unique permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag at ALLOC[0x4..0x8]
|
= 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 Unique retag at offsets [0x4..0x8]
--> $DIR/return_invalid_mut_option.rs:LL:CC
|
LL | let ret = Some(ret);
| ^^^
| ^^^^^^^^^
help: <TAG> was later invalidated at offsets [0x0..0x8] by a read access
--> $DIR/return_invalid_mut_option.rs:LL:CC
|
LL | let _val = unsafe { *xraw }; // invalidate xref
| ^^^^^
= note: BACKTRACE:
= note: inside `main` at $DIR/return_invalid_mut_option.rs:LL:CC
= note: inside `foo` at $DIR/return_invalid_mut_option.rs:LL:CC
note: inside `main` at $DIR/return_invalid_mut_option.rs:LL:CC
--> $DIR/return_invalid_mut_option.rs:LL:CC
|
LL | match foo(&mut (1, 2)) {
| ^^^^^^^^^^^^^^^^

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

Expand Down
5 changes: 2 additions & 3 deletions tests/fail/stacked_borrows/return_invalid_mut_tuple.rs
Original file line number Diff line number Diff line change
@@ -1,12 +1,11 @@
// Make sure that we cannot return a `&mut` that got already invalidated, not even in a tuple.
// Due to shallow reborrowing, the error only surfaces when we look into the tuple.
fn foo(x: &mut (i32, i32)) -> (&mut i32,) {
let xraw = x as *mut (i32, i32);
let ret = (unsafe { &mut (*xraw).1 },);
let _val = unsafe { *xraw }; // invalidate xref
ret
ret //~ ERROR: /retag .* tag does not exist in the borrow stack/
}

fn main() {
foo(&mut (1, 2)).0; //~ ERROR: /retag .* tag does not exist in the borrow stack/
foo(&mut (1, 2)).0;
}
13 changes: 9 additions & 4 deletions tests/fail/stacked_borrows/return_invalid_mut_tuple.stderr
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
error: Undefined Behavior: trying to retag from <TAG> for Unique permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
--> $DIR/return_invalid_mut_tuple.rs:LL:CC
|
LL | foo(&mut (1, 2)).0;
| ^^^^^^^^^^^^^^^^^^
LL | ret
| ^^^
| |
| trying to retag from <TAG> for Unique permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag at ALLOC[0x4..0x8]
Expand All @@ -13,14 +13,19 @@ help: <TAG> was created by a Unique retag at offsets [0x4..0x8]
--> $DIR/return_invalid_mut_tuple.rs:LL:CC
|
LL | let ret = (unsafe { &mut (*xraw).1 },);
| ^^^^^^^^^^^^^^
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^
help: <TAG> was later invalidated at offsets [0x0..0x8] by a read access
--> $DIR/return_invalid_mut_tuple.rs:LL:CC
|
LL | let _val = unsafe { *xraw }; // invalidate xref
| ^^^^^
= note: BACKTRACE:
= note: inside `main` at $DIR/return_invalid_mut_tuple.rs:LL:CC
= note: inside `foo` at $DIR/return_invalid_mut_tuple.rs:LL:CC
note: inside `main` at $DIR/return_invalid_mut_tuple.rs:LL:CC
--> $DIR/return_invalid_mut_tuple.rs:LL:CC
|
LL | foo(&mut (1, 2)).0;
| ^^^^^^^^^^^^^^^^

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

Expand Down
5 changes: 2 additions & 3 deletions tests/fail/stacked_borrows/return_invalid_shr_option.rs
Original file line number Diff line number Diff line change
@@ -1,15 +1,14 @@
// Make sure that we cannot return a `&` that got already invalidated, not even in an `Option`.
// Due to shallow reborrowing, the error only surfaces when we look into the `Option`.
fn foo(x: &mut (i32, i32)) -> Option<&i32> {
let xraw = x as *mut (i32, i32);
let ret = Some(unsafe { &(*xraw).1 });
unsafe { *xraw = (42, 23) }; // unfreeze
ret
ret //~ ERROR: /retag .* tag does not exist in the borrow stack/
}

fn main() {
match foo(&mut (1, 2)) {
Some(_x) => {} //~ ERROR: /retag .* tag does not exist in the borrow stack/
Some(_x) => {}
None => {}
}
}
19 changes: 12 additions & 7 deletions tests/fail/stacked_borrows/return_invalid_shr_option.stderr
Original file line number Diff line number Diff line change
@@ -1,26 +1,31 @@
error: Undefined Behavior: trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
--> $DIR/return_invalid_shr_option.rs:LL:CC
|
LL | Some(_x) => {}
| ^^
| |
| trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag at ALLOC[0x4..0x8]
LL | ret
| ^^^
| |
| trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag at ALLOC[0x4..0x8]
|
= 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 SharedReadOnly retag at offsets [0x4..0x8]
--> $DIR/return_invalid_shr_option.rs:LL:CC
|
LL | let ret = Some(unsafe { &(*xraw).1 });
| ^^^^^^^^^^
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^
help: <TAG> was later invalidated at offsets [0x0..0x8] by a write access
--> $DIR/return_invalid_shr_option.rs:LL:CC
|
LL | unsafe { *xraw = (42, 23) }; // unfreeze
| ^^^^^^^^^^^^^^^^
= note: BACKTRACE:
= note: inside `main` at $DIR/return_invalid_shr_option.rs:LL:CC
= note: inside `foo` at $DIR/return_invalid_shr_option.rs:LL:CC
note: inside `main` at $DIR/return_invalid_shr_option.rs:LL:CC
--> $DIR/return_invalid_shr_option.rs:LL:CC
|
LL | match foo(&mut (1, 2)) {
| ^^^^^^^^^^^^^^^^

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

Expand Down
5 changes: 2 additions & 3 deletions tests/fail/stacked_borrows/return_invalid_shr_tuple.rs
Original file line number Diff line number Diff line change
@@ -1,12 +1,11 @@
// Make sure that we cannot return a `&` that got already invalidated, not even in a tuple.
// Due to shallow reborrowing, the error only surfaces when we look into the tuple.
fn foo(x: &mut (i32, i32)) -> (&i32,) {
let xraw = x as *mut (i32, i32);
let ret = (unsafe { &(*xraw).1 },);
unsafe { *xraw = (42, 23) }; // unfreeze
ret
ret //~ ERROR: /retag .* tag does not exist in the borrow stack/
}

fn main() {
foo(&mut (1, 2)).0; //~ ERROR: /retag .* tag does not exist in the borrow stack/
foo(&mut (1, 2)).0;
}
13 changes: 9 additions & 4 deletions tests/fail/stacked_borrows/return_invalid_shr_tuple.stderr
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
error: Undefined Behavior: trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
--> $DIR/return_invalid_shr_tuple.rs:LL:CC
|
LL | foo(&mut (1, 2)).0;
| ^^^^^^^^^^^^^^^^^^
LL | ret
| ^^^
| |
| trying to retag from <TAG> for SharedReadOnly permission at ALLOC[0x4], but that tag does not exist in the borrow stack for this location
| this error occurs as part of retag at ALLOC[0x4..0x8]
Expand All @@ -13,14 +13,19 @@ help: <TAG> was created by a SharedReadOnly retag at offsets [0x4..0x8]
--> $DIR/return_invalid_shr_tuple.rs:LL:CC
|
LL | let ret = (unsafe { &(*xraw).1 },);
| ^^^^^^^^^^
| ^^^^^^^^^^^^^^^^^^^^^^^^
help: <TAG> was later invalidated at offsets [0x0..0x8] by a write access
--> $DIR/return_invalid_shr_tuple.rs:LL:CC
|
LL | unsafe { *xraw = (42, 23) }; // unfreeze
| ^^^^^^^^^^^^^^^^
= note: BACKTRACE:
= note: inside `main` at $DIR/return_invalid_shr_tuple.rs:LL:CC
= note: inside `foo` at $DIR/return_invalid_shr_tuple.rs:LL:CC
note: inside `main` at $DIR/return_invalid_shr_tuple.rs:LL:CC
--> $DIR/return_invalid_shr_tuple.rs:LL:CC
|
LL | foo(&mut (1, 2)).0;
| ^^^^^^^^^^^^^^^^

note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace

Expand Down
19 changes: 19 additions & 0 deletions tests/pass/stacked-borrows/no_field_retagging.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
//@compile-flags: -Zmiri-retag-fields=none

struct Newtype<'a>(&'a mut i32);

fn dealloc_while_running(_n: Newtype<'_>, dealloc: impl FnOnce()) {
dealloc();
}

// Make sure that we do *not* retag the fields of `Newtype`.
fn main() {
let ptr = Box::into_raw(Box::new(0i32));
#[rustfmt::skip] // I like my newlines
unsafe {
dealloc_while_running(
Newtype(&mut *ptr),
|| drop(Box::from_raw(ptr)),
)
};
}
4 changes: 2 additions & 2 deletions tests/pass/stacked-borrows/stack-printing.stdout
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
0..1: [ SharedReadWrite<TAG> ]
0..1: [ SharedReadWrite<TAG> ]
0..1: [ SharedReadWrite<TAG> ]
0..1: [ SharedReadWrite<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> ]
0..1: [ SharedReadWrite<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> SharedReadOnly<TAG> ]
0..1: [ SharedReadWrite<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> ]
0..1: [ SharedReadWrite<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> SharedReadOnly<TAG> ]
0..1: [ unknown-bottom(..<TAG>) ]