Skip to content

Commit

Permalink
add -Zmiri-strict-provenance
Browse files Browse the repository at this point in the history
  • Loading branch information
RalfJung committed Apr 1, 2022
1 parent 6e1ed17 commit 9af03bf
Show file tree
Hide file tree
Showing 18 changed files with 48 additions and 20 deletions.
4 changes: 4 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -294,6 +294,10 @@ environment variable:
entropy. The default seed is 0. **NOTE**: This entropy is not good enough
for cryptographic use! Do not generate secret keys in Miri or perform other
kinds of cryptographic operations that rely on proper random numbers.
* `-Zmiri-strict-provenance` enables [strict
provenance](https://github.com/rust-lang/rust/issues/95228) checking in Miri. This means that
casting an integer to a pointer yields a result with 'invalid' provenance, i.e., with provenance
that cannot be used for any memory access. Also implies `-Zmiri-tag-raw-pointers`.
* `-Zmiri-symbolic-alignment-check` makes the alignment check more strict. By
default, alignment is checked by casting the pointer to an integer, and making
sure that is a multiple of the alignment. This can lead to cases where a
Expand Down
4 changes: 4 additions & 0 deletions src/bin/miri.rs
Original file line number Diff line number Diff line change
Expand Up @@ -363,6 +363,10 @@ fn main() {
"-Zmiri-tag-raw-pointers" => {
miri_config.tag_raw = true;
}
"-Zmiri-strict-provenance" => {
miri_config.strict_provenance = true;
miri_config.tag_raw = true;
}
"-Zmiri-track-raw-pointers" => {
eprintln!(
"WARNING: -Zmiri-track-raw-pointers has been renamed to -Zmiri-tag-raw-pointers, the old name is deprecated."
Expand Down
7 changes: 6 additions & 1 deletion src/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -108,9 +108,13 @@ pub struct MiriConfig {
/// If `Some`, enable the `measureme` profiler, writing results to a file
/// with the specified prefix.
pub measureme_out: Option<String>,
/// Panic when unsupported functionality is encountered
/// Panic when unsupported functionality is encountered.
pub panic_on_unsupported: bool,
/// Which style to use for printing backtraces.
pub backtrace_style: BacktraceStyle,
/// Whether to enforce "strict provenance" rules. Enabling this means int2ptr casts return
/// pointers with an invalid provenance, i.e., not valid for any memory access.
pub strict_provenance: bool,
}

impl Default for MiriConfig {
Expand All @@ -136,6 +140,7 @@ impl Default for MiriConfig {
measureme_out: None,
panic_on_unsupported: false,
backtrace_style: BacktraceStyle::Short,
strict_provenance: false,
}
}
}
Expand Down
20 changes: 14 additions & 6 deletions src/intptrcast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,23 +15,27 @@ pub type MemoryExtra = RefCell<GlobalState>;
pub struct GlobalState {
/// This is used as a map between the address of each allocation and its `AllocId`.
/// It is always sorted
pub int_to_ptr_map: Vec<(u64, AllocId)>,
int_to_ptr_map: Vec<(u64, AllocId)>,
/// The base address for each allocation. We cannot put that into
/// `AllocExtra` because function pointers also have a base address, and
/// they do not have an `AllocExtra`.
/// This is the inverse of `int_to_ptr_map`.
pub base_addr: FxHashMap<AllocId, u64>,
base_addr: FxHashMap<AllocId, u64>,
/// This is used as a memory address when a new pointer is casted to an integer. It
/// is always larger than any address that was previously made part of a block.
pub next_base_addr: u64,
next_base_addr: u64,
/// Whether to enforce "strict provenance" rules. Enabling this means int2ptr casts return
/// pointers with an invalid provenance, i.e., not valid for any memory access.
strict_provenance: bool,
}

impl Default for GlobalState {
fn default() -> Self {
impl GlobalState {
pub fn new(config: &MiriConfig) -> Self {
GlobalState {
int_to_ptr_map: Vec::default(),
base_addr: FxHashMap::default(),
next_base_addr: STACK_ADDR,
strict_provenance: config.strict_provenance,
}
}
}
Expand All @@ -43,8 +47,12 @@ impl<'mir, 'tcx> GlobalState {
) -> Pointer<Option<Tag>> {
trace!("Casting 0x{:x} to a pointer", addr);
let global_state = memory.extra.intptrcast.borrow();
let pos = global_state.int_to_ptr_map.binary_search_by_key(&addr, |(addr, _)| *addr);

if global_state.strict_provenance {
return Pointer::new(None, Size::from_bytes(addr));
}

let pos = global_state.int_to_ptr_map.binary_search_by_key(&addr, |(addr, _)| *addr);
let alloc_id = match pos {
Ok(pos) => Some(global_state.int_to_ptr_map[pos].1),
Err(0) => None,
Expand Down
2 changes: 1 addition & 1 deletion src/machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -205,7 +205,7 @@ impl MemoryExtra {
MemoryExtra {
stacked_borrows,
data_race,
intptrcast: Default::default(),
intptrcast: RefCell::new(intptrcast::GlobalState::new(config)),
extern_statics: FxHashMap::default(),
rng: RefCell::new(rng),
tracked_alloc_id: config.tracked_alloc_id,
Expand Down
2 changes: 1 addition & 1 deletion tests/compile-fail/box-cell-alias.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// compile-flags: -Zmiri-tag-raw-pointers
// compile-flags: -Zmiri-strict-provenance

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

Expand Down
2 changes: 1 addition & 1 deletion tests/compile-fail/stacked_borrows/zst_slice.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// compile-flags: -Zmiri-tag-raw-pointers
// compile-flags: -Zmiri-strict-provenance
// error-pattern: does not exist in the borrow stack

fn main() {
Expand Down
9 changes: 9 additions & 0 deletions tests/compile-fail/strict-provenance-offset.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
// compile-flags: -Zmiri-strict-provenance
// error-pattern: not a valid pointer

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) };
}
2 changes: 1 addition & 1 deletion tests/run-pass/btreemap.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// compile-flags: -Zmiri-tag-raw-pointers
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity
#![feature(btree_drain_filter)]
use std::collections::{BTreeMap, BTreeSet};
use std::mem;
Expand Down
1 change: 0 additions & 1 deletion tests/run-pass/concurrency/channels.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
// ignore-windows: Concurrency on Windows is not supported yet.
// compile-flags: -Zmiri-disable-isolation

use std::sync::mpsc::{channel, sync_channel};
use std::thread;
Expand Down
2 changes: 1 addition & 1 deletion tests/run-pass/concurrency/sync.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// ignore-windows: Concurrency on Windows is not supported yet.
// compile-flags: -Zmiri-disable-isolation -Zmiri-check-number-validity
// compile-flags: -Zmiri-disable-isolation -Zmiri-strict-provenance -Zmiri-check-number-validity

use std::sync::{Arc, Barrier, Condvar, Mutex, Once, RwLock};
use std::thread;
Expand Down
2 changes: 1 addition & 1 deletion tests/run-pass/concurrency/thread_locals.rs
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
// ignore-windows: Concurrency on Windows is not supported yet.
// compile-flags: -Zmiri-check-number-validity
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity

//! The main purpose of this test is to check that if we take a pointer to
//! thread's `t1` thread-local `A` and send it to another thread `t2`,
Expand Down
1 change: 0 additions & 1 deletion tests/run-pass/concurrency/tls_lib_drop_single_thread.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
// compile-flags: -Zmiri-tag-raw-pointers
//! Check that destructors of the thread locals are executed on all OSes.
use std::cell::RefCell;
Expand Down
2 changes: 1 addition & 1 deletion tests/run-pass/rc.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// compile-flags: -Zmiri-tag-raw-pointers
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity
#![feature(new_uninit)]
#![feature(get_mut_unchecked)]

Expand Down
2 changes: 1 addition & 1 deletion tests/run-pass/slices.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// compile-flags: -Zmiri-tag-raw-pointers
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity
#![feature(new_uninit)]
#![feature(slice_as_chunks)]
#![feature(slice_partition_dedup)]
Expand Down
2 changes: 1 addition & 1 deletion tests/run-pass/strings.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// compile-flags: -Zmiri-tag-raw-pointers
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity

fn empty() -> &'static str {
""
Expand Down
2 changes: 1 addition & 1 deletion tests/run-pass/vec.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// compile-flags: -Zmiri-tag-raw-pointers -Zmiri-check-number-validity
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity
// Gather all references from a mutable iterator and make sure Miri notices if
// using them is dangerous.
fn test_all_refs<'a, T: 'a>(dummy: &mut T, iter: impl Iterator<Item = &'a mut T>) {
Expand Down
2 changes: 1 addition & 1 deletion tests/run-pass/vecdeque.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// compile-flags: -Zmiri-tag-raw-pointers
// compile-flags: -Zmiri-strict-provenance -Zmiri-check-number-validity
use std::collections::VecDeque;

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

0 comments on commit 9af03bf

Please sign in to comment.