Skip to content

Commit

Permalink
Auto merge of #2636 - RalfJung:scalar-field-retag, r=oli-obk
Browse files Browse the repository at this point in the history
Stacked Borrows: make scalar field retagging the default

I think it is time to finally close this soundness gap. Any objections? :)

Unfortunately the latest released versions of hashbrown and scopeguard can fail under full field retagging. The fixes have landed in the git repos but have not been released yet. I don't know if scalar field retagging as enabled by this PR is sufficient to cause problems with these crates, but it seems likely that this would be the case -- e.g. if both `value` and `dropfn` are scalars, the entire scopeguard struct will be a `ScalarPair` and thus get field retagging.

However, given that we actually generate LLVM `noalias` for these cases, it seems prudent to inform users of this risk. They can easily set `-Zmiri-field-retag=none` to opt-out of this change.

Cc #2528
  • Loading branch information
bors committed Oct 29, 2022
2 parents 8927d82 + 14c247c commit 7138140
Show file tree
Hide file tree
Showing 14 changed files with 76 additions and 42 deletions.
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>) ]

0 comments on commit 7138140

Please sign in to comment.