Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add -Zmiri-strict-provenance #2045

Merged
merged 1 commit into from
Apr 1, 2022
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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