Skip to content

Commit bf4d4c0

Browse files
committed
Auto merge of #3766 - RalfJung:tree-borrows-int2ptr, r=RalfJung
better diagnostics for Tree Borrows + int2ptr casts - Entirely reject `-Zmiri-permissive-provenance -Zmiri-tree-borrows` since that combination just doesn't work - In the int2ptr cast warning, when Tree Borrows is enabled, do not recommend `-Zmiri-permissive-provenance`, instead note that Tree Borrows does not support int2ptr casts Fixes rust-lang/miri#3764
2 parents f98fdfc + 5e1f8e2 commit bf4d4c0

16 files changed

+201
-138
lines changed

src/tools/miri/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/tools/miri/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/tools/miri/src/diagnostics.rs

Lines changed: 69 additions & 73 deletions
Large diffs are not rendered by default.

src/tools/miri/tests/pass/adjacent-allocs.rs

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,3 @@
1-
//@revisions: stack tree
2-
//@[tree]compile-flags: -Zmiri-tree-borrows
31
//@compile-flags: -Zmiri-permissive-provenance
42

53
fn ensure_allocs_can_be_adjacent() {

src/tools/miri/tests/pass/box.rs

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
1-
//@revisions: stack tree
2-
//@[tree]compile-flags: -Zmiri-tree-borrows -Zmiri-permissive-provenance
1+
//@compile-flags: -Zmiri-permissive-provenance
32
#![feature(ptr_internals)]
43

54
fn main() {

src/tools/miri/tests/pass/box.stack.stderr

Lines changed: 0 additions & 33 deletions
This file was deleted.

src/tools/miri/tests/pass/box.tree.stdout

Lines changed: 0 additions & 3 deletions
This file was deleted.
Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,14 @@
11
//@revisions: stack tree
2-
//@[tree]compile-flags: -Zmiri-tree-borrows -Zmiri-permissive-provenance
3-
#![feature(extern_types)]
2+
//@[tree]compile-flags: -Zmiri-tree-borrows
3+
#![feature(extern_types, strict_provenance)]
4+
5+
use std::ptr;
46

57
extern "C" {
68
type Foo;
79
}
810

911
fn main() {
10-
let x: &Foo = unsafe { &*(16 as *const Foo) };
12+
let x: &Foo = unsafe { &*(ptr::without_provenance::<()>(16) as *const Foo) };
1113
let _y: &Foo = &*x;
1214
}

src/tools/miri/tests/pass/extern_types.stack.stderr

Lines changed: 2 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,8 @@
1-
warning: integer-to-pointer cast
2-
--> $DIR/extern_types.rs:LL:CC
3-
|
4-
LL | let x: &Foo = unsafe { &*(16 as *const Foo) };
5-
| ^^^^^^^^^^^^^^^^^^ integer-to-pointer cast
6-
|
7-
= help: this program is using integer-to-pointer casts or (equivalently) `ptr::with_exposed_provenance`, which means that Miri might miss pointer bugs in this program
8-
= help: see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation
9-
= help: to ensure that Miri does not miss bugs in your program, use Strict Provenance APIs (https://doc.rust-lang.org/nightly/std/ptr/index.html#strict-provenance, https://crates.io/crates/sptr) instead
10-
= help: you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics
11-
= help: alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning
12-
= note: BACKTRACE:
13-
= note: inside `main` at $DIR/extern_types.rs:LL:CC
14-
151
warning: reborrow of reference to `extern type`
162
--> $DIR/extern_types.rs:LL:CC
173
|
18-
LL | let x: &Foo = unsafe { &*(16 as *const Foo) };
19-
| ^^^^^^^^^^^^^^^^^^^^ reborrow of a reference to `extern type` is not properly supported
4+
LL | let x: &Foo = unsafe { &*(ptr::without_provenance::<()>(16) as *const Foo) };
5+
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ reborrow of a reference to `extern type` is not properly supported
206
|
217
= help: `extern type` are not compatible with the Stacked Borrows aliasing model implemented by Miri; Miri may miss bugs in this code
228
= help: try running with `MIRIFLAGS=-Zmiri-tree-borrows` to use the more permissive but also even more experimental Tree Borrows aliasing checks instead

0 commit comments

Comments
 (0)