Skip to content

Commit

Permalink
Auto merge of #2046 - RalfJung:very-strict, r=RalfJung
Browse files Browse the repository at this point in the history
make strict-provenance imply check-number-validity

I feel like Miri not catching [this example](rust-lang/unsafe-code-guidelines#286 (comment)) with strict provenance checking enabled is surprising.

OTOH, Miri suddenly complaining about uninit data in integers with `-Zmiri-strict-provenance` also might be surprising. Which one is more surprising? I don't know. We *could* go out of our way and have a mode where uninit integers are okay but provenance is not, but I am not sure if that is truly worth it. It'd be quite annoying to implement.
  • Loading branch information
bors committed Apr 4, 2022
2 parents fc2165d + 3dcba56 commit ec51594
Show file tree
Hide file tree
Showing 11 changed files with 38 additions and 9 deletions.
3 changes: 2 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -297,7 +297,8 @@ environment variable:
* `-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`.
that cannot be used for any memory access. Also implies `-Zmiri-tag-raw-pointers` and
`-Zmiri-check-number-validity`.
* `-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
1 change: 1 addition & 0 deletions src/bin/miri.rs
Original file line number Diff line number Diff line change
Expand Up @@ -366,6 +366,7 @@ fn main() {
"-Zmiri-strict-provenance" => {
miri_config.strict_provenance = true;
miri_config.tag_raw = true;
miri_config.check_number_validity = true;
}
"-Zmiri-track-raw-pointers" => {
eprintln!(
Expand Down
27 changes: 27 additions & 0 deletions tests/compile-fail/strict_provenance_transmute.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
// compile-flags: -Zmiri-strict-provenance
#![feature(strict_provenance)]

use std::mem;

// This is the example from
// <https://github.com/rust-lang/unsafe-code-guidelines/issues/286#issuecomment-1085144431>.

unsafe fn deref(left: *const u8, right: *const u8) {
let left_int: usize = mem::transmute(left); //~ERROR expected initialized plain (non-pointer) bytes
let right_int: usize = mem::transmute(right);
if left_int == right_int {
// The compiler is allowed to replace `left_int` by `right_int` here...
let left_ptr: *const u8 = mem::transmute(left_int);
// ...which however means here it could be dereferencing the wrong pointer.
let _val = *left_ptr;
}
}

fn main() {
let ptr1 = &0u8 as *const u8;
let ptr2 = &1u8 as *const u8;
unsafe {
// Two pointers with the same address but different provenance.
deref(ptr1, ptr2.with_addr(ptr1.addr()));
}
}
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-strict-provenance -Zmiri-check-number-validity
// compile-flags: -Zmiri-strict-provenance
#![feature(btree_drain_filter)]
use std::collections::{BTreeMap, BTreeSet};
use std::mem;
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-strict-provenance -Zmiri-check-number-validity
// compile-flags: -Zmiri-disable-isolation -Zmiri-strict-provenance

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-strict-provenance -Zmiri-check-number-validity
// compile-flags: -Zmiri-strict-provenance

//! 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
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-strict-provenance -Zmiri-check-number-validity
// compile-flags: -Zmiri-strict-provenance
#![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-strict-provenance -Zmiri-check-number-validity
// compile-flags: -Zmiri-strict-provenance
#![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-strict-provenance -Zmiri-check-number-validity
// compile-flags: -Zmiri-strict-provenance

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-strict-provenance -Zmiri-check-number-validity
// compile-flags: -Zmiri-strict-provenance
// 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-strict-provenance -Zmiri-check-number-validity
// compile-flags: -Zmiri-strict-provenance
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 ec51594

Please sign in to comment.