Skip to content

Commit

Permalink
Auto merge of rust-lang#3701 - RalfJung:extern-type-reborrow, r=saethlin
Browse files Browse the repository at this point in the history
show warning when Stacked Borrows skips a reborrow due to 'extern type'

When this happens, we can't actually be sure to catch all bugs -- LLVM will still get a `noalias` but Miri can't do reborrowing. That's not good.
  • Loading branch information
bors committed Jul 24, 2024
2 parents 12cb742 + c45f464 commit f1ae48c
Show file tree
Hide file tree
Showing 7 changed files with 83 additions and 27 deletions.
15 changes: 14 additions & 1 deletion src/tools/miri/src/borrow_tracker/stacked_borrows/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ pub mod diagnostics;
mod item;
mod stack;

use std::cell::RefCell;
use std::cmp;
use std::fmt::Write;
use std::mem;
Expand Down Expand Up @@ -820,7 +821,19 @@ trait EvalContextPrivExt<'tcx, 'ecx>: crate::MiriInterpCxExt<'tcx> {
// See https://github.com/rust-lang/unsafe-code-guidelines/issues/276.
let size = match size {
Some(size) => size,
None => return Ok(place.clone()),
None => {
// The first time this happens, show a warning.
thread_local! { static WARNING_SHOWN: RefCell<bool> = const { RefCell::new(false) }; }
WARNING_SHOWN.with_borrow_mut(|shown| {
if *shown {
return;
}
// Not yet shown. Show it!
*shown = true;
this.emit_diagnostic(NonHaltingDiagnostic::ExternTypeReborrow);
});
return Ok(place.clone());
}
};

// Compute new borrow.
Expand Down
31 changes: 26 additions & 5 deletions src/tools/miri/src/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -130,6 +130,7 @@ pub enum NonHaltingDiagnostic {
WeakMemoryOutdatedLoad {
ptr: Pointer,
},
ExternTypeReborrow,
}

/// Level of Miri specific diagnostics
Expand Down Expand Up @@ -593,6 +594,8 @@ impl<'tcx> MiriMachine<'tcx> {
RejectedIsolatedOp(_) =>
("operation rejected by isolation".to_string(), DiagLevel::Warning),
Int2Ptr { .. } => ("integer-to-pointer cast".to_string(), DiagLevel::Warning),
ExternTypeReborrow =>
("reborrow of reference to `extern type`".to_string(), DiagLevel::Warning),
CreatedPointerTag(..)
| PoppedPointerTag(..)
| CreatedCallId(..)
Expand Down Expand Up @@ -630,6 +633,8 @@ impl<'tcx> MiriMachine<'tcx> {
Int2Ptr { .. } => format!("integer-to-pointer cast"),
WeakMemoryOutdatedLoad { ptr } =>
format!("weak memory emulation: outdated value returned from load at {ptr}"),
ExternTypeReborrow =>
format!("reborrow of a reference to `extern type` is not properly supported"),
};

let notes = match &e {
Expand All @@ -647,34 +652,50 @@ impl<'tcx> MiriMachine<'tcx> {
(
None,
format!(
"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."
"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"
),
),
(
None,
format!(
"See https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation."
"see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation"
),
),
(
None,
format!(
"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."
"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"
),
),
(
None,
format!(
"You can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics."
"you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics"
),
),
(
None,
format!(
"Alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning."
"alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning"
),
),
],
ExternTypeReborrow => {
vec![
(
None,
format!(
"`extern type` are not compatible with the Stacked Borrows aliasing model implemented by Miri; Miri may miss bugs in this code"
),
),
(
None,
format!(
"try running with `MIRIFLAGS=-Zmiri-tree-borrows` to use the more permissive but also even more experimental Tree Borrows aliasing checks instead"
),
),
]
}
_ => vec![],
};

Expand Down
13 changes: 12 additions & 1 deletion src/tools/miri/tests/fail/extern-type-field-offset.stderr
Original file line number Diff line number Diff line change
@@ -1,3 +1,14 @@
warning: reborrow of reference to `extern type`
--> $DIR/extern-type-field-offset.rs:LL:CC
|
LL | let x: &Newtype = unsafe { &*(&buf as *const _ as *const Newtype) };
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ reborrow of a reference to `extern type` is not properly supported
|
= help: `extern type` are not compatible with the Stacked Borrows aliasing model implemented by Miri; Miri may miss bugs in this code
= help: try running with `MIRIFLAGS=-Zmiri-tree-borrows` to use the more permissive but also even more experimental Tree Borrows aliasing checks instead
= note: BACKTRACE:
= note: inside `main` at $DIR/extern-type-field-offset.rs:LL:CC

error: unsupported operation: `extern type` field does not have a known offset
--> $DIR/extern-type-field-offset.rs:LL:CC
|
Expand All @@ -10,5 +21,5 @@ LL | let _field = &x.a;

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

error: aborting due to 1 previous error
error: aborting due to 1 previous error; 1 warning emitted

Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,11 @@ warning: integer-to-pointer cast
LL | (*p.as_mut_ptr().cast::<[*const i32; 2]>())[0] = 4 as *const i32;
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ integer-to-pointer cast
|
= 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.
= help: See https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation.
= 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.
= help: You can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics.
= help: Alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning.
= 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
= help: see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation
= 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
= help: you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics
= help: alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning
= note: BACKTRACE:
= note: inside `main` at $DIR/ptr_metadata_uninit_slice_len.rs:LL:CC

Expand Down
10 changes: 5 additions & 5 deletions src/tools/miri/tests/pass/box.stack.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,11 @@ warning: integer-to-pointer cast
LL | let r2 = ((r as usize) + 0) as *mut i32;
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ integer-to-pointer cast
|
= 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.
= help: See https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation.
= 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.
= help: You can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics.
= help: Alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning.
= 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
= help: see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation
= 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
= help: you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics
= help: alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning
= note: BACKTRACE:
= note: inside `into_raw` at $DIR/box.rs:LL:CC
note: inside `main`
Expand Down
21 changes: 16 additions & 5 deletions src/tools/miri/tests/pass/extern_types.stack.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,22 @@ warning: integer-to-pointer cast
LL | let x: &Foo = unsafe { &*(16 as *const Foo) };
| ^^^^^^^^^^^^^^^^^^ integer-to-pointer cast
|
= 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.
= help: See https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation.
= 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.
= help: You can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics.
= help: Alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning.
= 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
= help: see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation
= 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
= help: you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics
= help: alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning
= note: BACKTRACE:
= note: inside `main` at $DIR/extern_types.rs:LL:CC

warning: reborrow of reference to `extern type`
--> $DIR/extern_types.rs:LL:CC
|
LL | let x: &Foo = unsafe { &*(16 as *const Foo) };
| ^^^^^^^^^^^^^^^^^^^^ reborrow of a reference to `extern type` is not properly supported
|
= help: `extern type` are not compatible with the Stacked Borrows aliasing model implemented by Miri; Miri may miss bugs in this code
= help: try running with `MIRIFLAGS=-Zmiri-tree-borrows` to use the more permissive but also even more experimental Tree Borrows aliasing checks instead
= note: BACKTRACE:
= note: inside `main` at $DIR/extern_types.rs:LL:CC

10 changes: 5 additions & 5 deletions src/tools/miri/tests/pass/stacked-borrows/issue-miri-2389.stderr
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,11 @@ warning: integer-to-pointer cast
LL | let wildcard = &root0 as *const Cell<i32> as usize as *const Cell<i32>;
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ integer-to-pointer cast
|
= 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.
= help: See https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation.
= 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.
= help: You can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics.
= help: Alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning.
= 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
= help: see https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html for more details on that operation
= 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
= help: you can then set `MIRIFLAGS=-Zmiri-strict-provenance` to ensure you are not relying on `with_exposed_provenance` semantics
= help: alternatively, `MIRIFLAGS=-Zmiri-permissive-provenance` disables this warning
= note: BACKTRACE:
= note: inside `main` at $DIR/issue-miri-2389.rs:LL:CC

0 comments on commit f1ae48c

Please sign in to comment.