Skip to content

Commit 732461b

Browse files
committed
Auto merge of #2045 - RalfJung:strict-provenance, r=RalfJung
add -Zmiri-strict-provenance This implements [strict provenance](rust-lang/rust#95228) in Miri. The only change is that casting an integer to a pointer does not even attempt to produce a good provenance for the given address; instead, it always uses the invalid provenance. This stricter than even `-Zmiri-tag-raw-pointers` in that it also rejects the following example (which does not even involve Stacked Borrows): ```rust fn main() { let x = 22; let ptr = &x as *const _ as *const u8; let roundtrip = ptr as usize as *const u8; let _ = unsafe { roundtrip.offset(1) }; } ``` The new flag also implies `-Zmiri-tag-raw-pointers` since the only reason one would *not* want to tag raw pointers is to support ptr-int-ptr roundtrips. Note that the flag does *not* check against ptr-to-int *transmutes*; that still requires `-Zmiri-check-number-validity`. You can also check for strict provenance *without* Stacked Borrows by adding `-Zmiri-disable-stacked-borrows`. The new "Miri hard mode" flags for maximal checking are `-Zmiri-strict-provenance -Zmiri-check-number-validity`. (Add `-Zmiri-symbolic-alignment-check` if you feel extra spicy today.)
2 parents 5d5d8b1 + 9af03bf commit 732461b

18 files changed

+48
-20
lines changed

README.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -294,6 +294,10 @@ environment variable:
294294
entropy. The default seed is 0. **NOTE**: This entropy is not good enough
295295
for cryptographic use! Do not generate secret keys in Miri or perform other
296296
kinds of cryptographic operations that rely on proper random numbers.
297+
* `-Zmiri-strict-provenance` enables [strict
298+
provenance](https://github.com/rust-lang/rust/issues/95228) checking in Miri. This means that
299+
casting an integer to a pointer yields a result with 'invalid' provenance, i.e., with provenance
300+
that cannot be used for any memory access. Also implies `-Zmiri-tag-raw-pointers`.
297301
* `-Zmiri-symbolic-alignment-check` makes the alignment check more strict. By
298302
default, alignment is checked by casting the pointer to an integer, and making
299303
sure that is a multiple of the alignment. This can lead to cases where a

src/bin/miri.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -363,6 +363,10 @@ fn main() {
363363
"-Zmiri-tag-raw-pointers" => {
364364
miri_config.tag_raw = true;
365365
}
366+
"-Zmiri-strict-provenance" => {
367+
miri_config.strict_provenance = true;
368+
miri_config.tag_raw = true;
369+
}
366370
"-Zmiri-track-raw-pointers" => {
367371
eprintln!(
368372
"WARNING: -Zmiri-track-raw-pointers has been renamed to -Zmiri-tag-raw-pointers, the old name is deprecated."

src/eval.rs

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -108,9 +108,13 @@ pub struct MiriConfig {
108108
/// If `Some`, enable the `measureme` profiler, writing results to a file
109109
/// with the specified prefix.
110110
pub measureme_out: Option<String>,
111-
/// Panic when unsupported functionality is encountered
111+
/// Panic when unsupported functionality is encountered.
112112
pub panic_on_unsupported: bool,
113+
/// Which style to use for printing backtraces.
113114
pub backtrace_style: BacktraceStyle,
115+
/// Whether to enforce "strict provenance" rules. Enabling this means int2ptr casts return
116+
/// pointers with an invalid provenance, i.e., not valid for any memory access.
117+
pub strict_provenance: bool,
114118
}
115119

116120
impl Default for MiriConfig {
@@ -136,6 +140,7 @@ impl Default for MiriConfig {
136140
measureme_out: None,
137141
panic_on_unsupported: false,
138142
backtrace_style: BacktraceStyle::Short,
143+
strict_provenance: false,
139144
}
140145
}
141146
}

src/intptrcast.rs

Lines changed: 14 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -15,23 +15,27 @@ pub type MemoryExtra = RefCell<GlobalState>;
1515
pub struct GlobalState {
1616
/// This is used as a map between the address of each allocation and its `AllocId`.
1717
/// It is always sorted
18-
pub int_to_ptr_map: Vec<(u64, AllocId)>,
18+
int_to_ptr_map: Vec<(u64, AllocId)>,
1919
/// The base address for each allocation. We cannot put that into
2020
/// `AllocExtra` because function pointers also have a base address, and
2121
/// they do not have an `AllocExtra`.
2222
/// This is the inverse of `int_to_ptr_map`.
23-
pub base_addr: FxHashMap<AllocId, u64>,
23+
base_addr: FxHashMap<AllocId, u64>,
2424
/// This is used as a memory address when a new pointer is casted to an integer. It
2525
/// is always larger than any address that was previously made part of a block.
26-
pub next_base_addr: u64,
26+
next_base_addr: u64,
27+
/// Whether to enforce "strict provenance" rules. Enabling this means int2ptr casts return
28+
/// pointers with an invalid provenance, i.e., not valid for any memory access.
29+
strict_provenance: bool,
2730
}
2831

29-
impl Default for GlobalState {
30-
fn default() -> Self {
32+
impl GlobalState {
33+
pub fn new(config: &MiriConfig) -> Self {
3134
GlobalState {
3235
int_to_ptr_map: Vec::default(),
3336
base_addr: FxHashMap::default(),
3437
next_base_addr: STACK_ADDR,
38+
strict_provenance: config.strict_provenance,
3539
}
3640
}
3741
}
@@ -43,8 +47,12 @@ impl<'mir, 'tcx> GlobalState {
4347
) -> Pointer<Option<Tag>> {
4448
trace!("Casting 0x{:x} to a pointer", addr);
4549
let global_state = memory.extra.intptrcast.borrow();
46-
let pos = global_state.int_to_ptr_map.binary_search_by_key(&addr, |(addr, _)| *addr);
4750

51+
if global_state.strict_provenance {
52+
return Pointer::new(None, Size::from_bytes(addr));
53+
}
54+
55+
let pos = global_state.int_to_ptr_map.binary_search_by_key(&addr, |(addr, _)| *addr);
4856
let alloc_id = match pos {
4957
Ok(pos) => Some(global_state.int_to_ptr_map[pos].1),
5058
Err(0) => None,

src/machine.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -205,7 +205,7 @@ impl MemoryExtra {
205205
MemoryExtra {
206206
stacked_borrows,
207207
data_race,
208-
intptrcast: Default::default(),
208+
intptrcast: RefCell::new(intptrcast::GlobalState::new(config)),
209209
extern_statics: FxHashMap::default(),
210210
rng: RefCell::new(rng),
211211
tracked_alloc_id: config.tracked_alloc_id,

tests/compile-fail/box-cell-alias.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// compile-flags: -Zmiri-tag-raw-pointers
1+
// compile-flags: -Zmiri-strict-provenance
22

33
// Taken from <https://github.com/rust-lang/unsafe-code-guidelines/issues/194#issuecomment-520934222>.
44

tests/compile-fail/stacked_borrows/zst_slice.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// compile-flags: -Zmiri-tag-raw-pointers
1+
// compile-flags: -Zmiri-strict-provenance
22
// error-pattern: does not exist in the borrow stack
33

44
fn main() {
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
// compile-flags: -Zmiri-strict-provenance
2+
// error-pattern: not a valid pointer
3+
4+
fn main() {
5+
let x = 22;
6+
let ptr = &x as *const _ as *const u8;
7+
let roundtrip = ptr as usize as *const u8;
8+
let _ = unsafe { roundtrip.offset(1) };
9+
}

tests/run-pass/btreemap.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// compile-flags: -Zmiri-tag-raw-pointers
1+
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity
22
#![feature(btree_drain_filter)]
33
use std::collections::{BTreeMap, BTreeSet};
44
use std::mem;

tests/run-pass/concurrency/channels.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
// ignore-windows: Concurrency on Windows is not supported yet.
2-
// compile-flags: -Zmiri-disable-isolation
32

43
use std::sync::mpsc::{channel, sync_channel};
54
use std::thread;

tests/run-pass/concurrency/sync.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
// ignore-windows: Concurrency on Windows is not supported yet.
2-
// compile-flags: -Zmiri-disable-isolation -Zmiri-check-number-validity
2+
// compile-flags: -Zmiri-disable-isolation -Zmiri-strict-provenance -Zmiri-check-number-validity
33

44
use std::sync::{Arc, Barrier, Condvar, Mutex, Once, RwLock};
55
use std::thread;

tests/run-pass/concurrency/thread_locals.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
// ignore-windows: Concurrency on Windows is not supported yet.
2-
// compile-flags: -Zmiri-check-number-validity
2+
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity
33

44
//! The main purpose of this test is to check that if we take a pointer to
55
//! thread's `t1` thread-local `A` and send it to another thread `t2`,

tests/run-pass/concurrency/tls_lib_drop_single_thread.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,3 @@
1-
// compile-flags: -Zmiri-tag-raw-pointers
21
//! Check that destructors of the thread locals are executed on all OSes.
32
43
use std::cell::RefCell;

tests/run-pass/rc.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// compile-flags: -Zmiri-tag-raw-pointers
1+
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity
22
#![feature(new_uninit)]
33
#![feature(get_mut_unchecked)]
44

tests/run-pass/slices.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// compile-flags: -Zmiri-tag-raw-pointers
1+
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity
22
#![feature(new_uninit)]
33
#![feature(slice_as_chunks)]
44
#![feature(slice_partition_dedup)]

tests/run-pass/strings.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// compile-flags: -Zmiri-tag-raw-pointers
1+
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity
22

33
fn empty() -> &'static str {
44
""

tests/run-pass/vec.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// compile-flags: -Zmiri-tag-raw-pointers -Zmiri-check-number-validity
1+
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity
22
// Gather all references from a mutable iterator and make sure Miri notices if
33
// using them is dangerous.
44
fn test_all_refs<'a, T: 'a>(dummy: &mut T, iter: impl Iterator<Item = &'a mut T>) {

tests/run-pass/vecdeque.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
// compile-flags: -Zmiri-tag-raw-pointers
1+
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity
22
use std::collections::VecDeque;
33

44
fn test_all_refs<'a, T: 'a>(dummy: &mut T, iter: impl Iterator<Item = &'a mut T>) {

0 commit comments

Comments
 (0)