Skip to content

Commit

Permalink
make Miri build again with rustc provenance changes
Browse files Browse the repository at this point in the history
  • Loading branch information
RalfJung committed Aug 31, 2022
1 parent 95b315d commit d21b601
Show file tree
Hide file tree
Showing 31 changed files with 158 additions and 102 deletions.
7 changes: 4 additions & 3 deletions src/diagnostics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -226,13 +226,14 @@ pub fn report_error<'tcx, 'mir>(
let helps = match e.kind() {
Unsupported(
UnsupportedOpInfo::ThreadLocalStatic(_) |
UnsupportedOpInfo::ReadExternStatic(_)
UnsupportedOpInfo::ReadExternStatic(_) |
UnsupportedOpInfo::PartialPointerOverwrite(_) | // we make memory uninit instead
UnsupportedOpInfo::ReadPointerAsBytes
) =>
panic!("Error should never be raised by Miri: {kind:?}", kind = e.kind()),
Unsupported(
UnsupportedOpInfo::Unsupported(_) |
UnsupportedOpInfo::PartialPointerOverwrite(_) |
UnsupportedOpInfo::ReadPointerAsBytes
UnsupportedOpInfo::PartialPointerCopy(_)
) =>
vec![(None, format!("this is likely not a bug in the program; it indicates that the program performed an operation that the interpreter does not support"))],
UndefinedBehavior(UndefinedBehaviorInfo::AlignmentCheckFailed { .. })
Expand Down
2 changes: 1 addition & 1 deletion src/helpers.rs
Original file line number Diff line number Diff line change
Expand Up @@ -757,7 +757,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
}

// Step 2: get the bytes.
this.read_bytes_ptr(ptr, len)
this.read_bytes_ptr_strip_provenance(ptr, len)
}

fn read_wide_str(&self, mut ptr: Pointer<Option<Provenance>>) -> InterpResult<'tcx, Vec<u16>> {
Expand Down
15 changes: 15 additions & 0 deletions src/machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -205,6 +205,21 @@ impl interpret::Provenance for Provenance {
Provenance::Wildcard => None,
}
}

fn join(left: Option<Self>, right: Option<Self>) -> Option<Self> {
match (left, right) {
// If both are the *same* concrete tag, that is the result.
(
Some(Provenance::Concrete { alloc_id: left_alloc, sb: left_sb }),
Some(Provenance::Concrete { alloc_id: right_alloc, sb: right_sb }),
) if left_alloc == right_alloc && left_sb == right_sb => left,
// If one side is a wildcard, the best possible outcome is that it is equal to the other
// one, and we use that.
(Some(Provenance::Wildcard), o) | (o, Some(Provenance::Wildcard)) => o,
// Otherwise, fall back to `None`.
_ => None,
}
}
}

impl fmt::Debug for ProvenanceExtra {
Expand Down
8 changes: 4 additions & 4 deletions src/shims/foreign_items.rs
Original file line number Diff line number Diff line change
Expand Up @@ -560,8 +560,8 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
let n = Size::from_bytes(this.read_scalar(n)?.to_machine_usize(this)?);

let result = {
let left_bytes = this.read_bytes_ptr(left, n)?;
let right_bytes = this.read_bytes_ptr(right, n)?;
let left_bytes = this.read_bytes_ptr_strip_provenance(left, n)?;
let right_bytes = this.read_bytes_ptr_strip_provenance(right, n)?;

use std::cmp::Ordering::*;
match left_bytes.cmp(right_bytes) {
Expand All @@ -583,7 +583,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
let val = val as u8;

if let Some(idx) = this
.read_bytes_ptr(ptr, Size::from_bytes(num))?
.read_bytes_ptr_strip_provenance(ptr, Size::from_bytes(num))?
.iter()
.rev()
.position(|&c| c == val)
Expand All @@ -606,7 +606,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
let val = val as u8;

let idx = this
.read_bytes_ptr(ptr, Size::from_bytes(num))?
.read_bytes_ptr_strip_provenance(ptr, Size::from_bytes(num))?
.iter()
.position(|&c| c == val);
if let Some(idx) = idx {
Expand Down
2 changes: 1 addition & 1 deletion src/shims/unix/fs.rs
Original file line number Diff line number Diff line change
Expand Up @@ -761,7 +761,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
let communicate = this.machine.communicate();

if let Some(file_descriptor) = this.machine.file_handler.handles.get(&fd) {
let bytes = this.read_bytes_ptr(buf, Size::from_bytes(count))?;
let bytes = this.read_bytes_ptr_strip_provenance(buf, Size::from_bytes(count))?;
let result =
file_descriptor.write(communicate, bytes)?.map(|c| i64::try_from(c).unwrap());
this.try_unwrap_io_result(result)
Expand Down
3 changes: 2 additions & 1 deletion src/shims/windows/dlsym.rs
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,8 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
// stdout/stderr
use std::io::{self, Write};

let buf_cont = this.read_bytes_ptr(buf, Size::from_bytes(u64::from(n)))?;
let buf_cont =
this.read_bytes_ptr_strip_provenance(buf, Size::from_bytes(u64::from(n)))?;
let res = if this.machine.mute_stdout_stderr {
Ok(buf_cont.len())
} else if handle == -11 {
Expand Down
21 changes: 21 additions & 0 deletions tests/fail/copy_half_a_pointer.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
//@normalize-stderr-test: "\+0x[48]" -> "+HALF_PTR"
#![allow(dead_code)]

// We use packed structs to get around alignment restrictions
#[repr(packed)]
struct Data {
pad: u8,
ptr: &'static i32,
}

static G: i32 = 0;

fn main() {
let mut d = Data { pad: 0, ptr: &G };

// Get a pointer to the beginning of the Data struct (one u8 byte, then the pointer bytes).
let d_alias = &mut d as *mut _ as *mut *const u8;
unsafe {
let _x = d_alias.read_unaligned(); //~ERROR: unable to copy parts of a pointer
}
}
14 changes: 14 additions & 0 deletions tests/fail/copy_half_a_pointer.stderr
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
error: unsupported operation: unable to copy parts of a pointer from memory at ALLOC+HALF_PTR
--> $DIR/copy_half_a_pointer.rs:LL:CC
|
LL | let _x = d_alias.read_unaligned();
| ^^^^^^^^^^^^^^^^^^^^^^^^ unable to copy parts of a pointer from memory at ALLOC+HALF_PTR
|
= help: this is likely not a bug in the program; it indicates that the program performed an operation that the interpreter does not support
= note: BACKTRACE:
= note: inside `main` at $DIR/copy_half_a_pointer.rs:LL:CC

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

error: aborting due to previous error

3 changes: 1 addition & 2 deletions tests/fail/intrinsics/raw_eq_on_ptr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,5 @@ extern "rust-intrinsic" {

fn main() {
let x = &0;
// FIXME: the error message is not great (should be UB rather than 'unsupported')
unsafe { raw_eq(&x, &x) }; //~ERROR: unsupported operation
unsafe { raw_eq(&x, &x) }; //~ERROR: `raw_eq` on bytes with provenance
}
7 changes: 4 additions & 3 deletions tests/fail/intrinsics/raw_eq_on_ptr.stderr
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
error: unsupported operation: unable to turn pointer into raw bytes
error: Undefined Behavior: `raw_eq` on bytes with provenance
--> $DIR/raw_eq_on_ptr.rs:LL:CC
|
LL | unsafe { raw_eq(&x, &x) };
| ^^^^^^^^^^^^^^ unable to turn pointer into raw bytes
| ^^^^^^^^^^^^^^ `raw_eq` on bytes with provenance
|
= help: this is likely not a bug in the program; it indicates that the program performed an operation that the interpreter does not support
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE:
= note: inside `main` at $DIR/raw_eq_on_ptr.rs:LL:CC

Expand Down
1 change: 1 addition & 0 deletions tests/fail/invalid_int.rs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
#![allow(invalid_value)]
// Validation makes this fail in the wrong place
// Make sure we find these even with many checks disabled.
//@compile-flags: -Zmiri-disable-alignment-check -Zmiri-disable-stacked-borrows -Zmiri-disable-validation
Expand Down
3 changes: 2 additions & 1 deletion tests/fail/reading_half_a_pointer.rs
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ fn main() {
// starts 1 byte to the right, so using it would actually be wrong!
let d_alias = &mut w.data as *mut _ as *mut *const u8;
unsafe {
let _x = *d_alias; //~ ERROR: unable to turn pointer into raw bytes
let x = *d_alias;
let _val = *x; //~ERROR: is a dangling pointer (it has no provenance)
}
}
9 changes: 5 additions & 4 deletions tests/fail/reading_half_a_pointer.stderr
Original file line number Diff line number Diff line change
@@ -1,10 +1,11 @@
error: unsupported operation: unable to turn pointer into raw bytes
error: Undefined Behavior: dereferencing pointer failed: $HEX[noalloc] is a dangling pointer (it has no provenance)
--> $DIR/reading_half_a_pointer.rs:LL:CC
|
LL | let _x = *d_alias;
| ^^^^^^^^ unable to turn pointer into raw bytes
LL | let _val = *x;
| ^^ dereferencing pointer failed: $HEX[noalloc] is a dangling pointer (it has no provenance)
|
= help: this is likely not a bug in the program; it indicates that the program performed an operation that the interpreter does not support
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
= note: BACKTRACE:
= note: inside `main` at $DIR/reading_half_a_pointer.rs:LL:CC

Expand Down
13 changes: 0 additions & 13 deletions tests/fail/transmute_fat1.rs

This file was deleted.

15 changes: 0 additions & 15 deletions tests/fail/transmute_fat1.stderr

This file was deleted.

4 changes: 2 additions & 2 deletions tests/fail/validity/invalid_bool_uninit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@

union MyUninit {
init: (),
uninit: bool,
uninit: [bool; 1],
}

fn main() {
let _b = unsafe { MyUninit { init: () }.uninit }; //~ ERROR: uninitialized
let _b = unsafe { MyUninit { init: () }.uninit }; //~ ERROR: constructing invalid value
}
4 changes: 2 additions & 2 deletions tests/fail/validity/invalid_bool_uninit.stderr
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
error: Undefined Behavior: using uninitialized data, but this operation requires initialized memory
error: Undefined Behavior: constructing invalid value at [0]: encountered uninitialized memory, but expected a boolean
--> $DIR/invalid_bool_uninit.rs:LL:CC
|
LL | let _b = unsafe { MyUninit { init: () }.uninit };
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ using uninitialized data, but this operation requires initialized memory
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ constructing invalid value at [0]: encountered uninitialized memory, but expected a boolean
|
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
Expand Down
4 changes: 2 additions & 2 deletions tests/fail/validity/invalid_char_uninit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@

union MyUninit {
init: (),
uninit: char,
uninit: [char; 1],
}

fn main() {
let _b = unsafe { MyUninit { init: () }.uninit }; //~ ERROR: uninitialized
let _b = unsafe { MyUninit { init: () }.uninit }; //~ ERROR: constructing invalid value
}
4 changes: 2 additions & 2 deletions tests/fail/validity/invalid_char_uninit.stderr
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
error: Undefined Behavior: using uninitialized data, but this operation requires initialized memory
error: Undefined Behavior: constructing invalid value at [0]: encountered uninitialized memory, but expected a unicode scalar value
--> $DIR/invalid_char_uninit.rs:LL:CC
|
LL | let _b = unsafe { MyUninit { init: () }.uninit };
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ using uninitialized data, but this operation requires initialized memory
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ constructing invalid value at [0]: encountered uninitialized memory, but expected a unicode scalar value
|
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
Expand Down
4 changes: 2 additions & 2 deletions tests/fail/validity/invalid_fnptr_uninit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@

union MyUninit {
init: (),
uninit: fn(),
uninit: [fn(); 1],
}

fn main() {
let _b = unsafe { MyUninit { init: () }.uninit }; //~ ERROR: uninitialized
let _b = unsafe { MyUninit { init: () }.uninit }; //~ ERROR: constructing invalid value
}
4 changes: 2 additions & 2 deletions tests/fail/validity/invalid_fnptr_uninit.stderr
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
error: Undefined Behavior: using uninitialized data, but this operation requires initialized memory
error: Undefined Behavior: constructing invalid value at [0]: encountered uninitialized memory, but expected a function pointer
--> $DIR/invalid_fnptr_uninit.rs:LL:CC
|
LL | let _b = unsafe { MyUninit { init: () }.uninit };
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ using uninitialized data, but this operation requires initialized memory
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ constructing invalid value at [0]: encountered uninitialized memory, but expected a function pointer
|
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
Expand Down
4 changes: 0 additions & 4 deletions tests/fail/validity/ptr_integer_array_transmute.rs

This file was deleted.

15 changes: 0 additions & 15 deletions tests/fail/validity/ptr_integer_array_transmute.stderr

This file was deleted.

5 changes: 3 additions & 2 deletions tests/fail/validity/uninit_float.rs
Original file line number Diff line number Diff line change
@@ -1,8 +1,9 @@
#![allow(deprecated)]
#![allow(deprecated, invalid_value)]
// This test is adapted from https://github.com/rust-lang/miri/issues/1340#issue-600900312.

fn main() {
// Deliberately using `mem::uninitialized` to make sure that despite all the mitigations, we consider this UB.
let _val: f32 = unsafe { std::mem::uninitialized() };
// The array avoids a `Scalar` layout which detects uninit without even doing validation.
let _val: [f32; 1] = unsafe { std::mem::uninitialized() };
//~^ ERROR: uninitialized
}
6 changes: 3 additions & 3 deletions tests/fail/validity/uninit_float.stderr
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
error: Undefined Behavior: using uninitialized data, but this operation requires initialized memory
error: Undefined Behavior: constructing invalid value at .value[0]: encountered uninitialized bytes
--> $DIR/uninit_float.rs:LL:CC
|
LL | let _val: f32 = unsafe { std::mem::uninitialized() };
| ^^^^^^^^^^^^^^^^^^^^^^^^^ using uninitialized data, but this operation requires initialized memory
LL | let _val: [f32; 1] = unsafe { std::mem::uninitialized() };
| ^^^^^^^^^^^^^^^^^^^^^^^^^ constructing invalid value at .value[0]: encountered uninitialized bytes
|
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
Expand Down
4 changes: 3 additions & 1 deletion tests/fail/validity/uninit_integer.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
#![allow(invalid_value)]
// This test is from https://github.com/rust-lang/miri/issues/1340#issue-600900312.

fn main() {
let _val = unsafe { std::mem::MaybeUninit::<usize>::uninit().assume_init() };
// The array avoids a `Scalar` layout which detects uninit without even doing validation.
let _val = unsafe { std::mem::MaybeUninit::<[usize; 1]>::uninit().assume_init() };
//~^ ERROR: uninitialized
}
6 changes: 3 additions & 3 deletions tests/fail/validity/uninit_integer.stderr
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
error: Undefined Behavior: using uninitialized data, but this operation requires initialized memory
error: Undefined Behavior: constructing invalid value at .value[0]: encountered uninitialized bytes
--> $DIR/uninit_integer.rs:LL:CC
|
LL | let _val = unsafe { std::mem::MaybeUninit::<usize>::uninit().assume_init() };
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ using uninitialized data, but this operation requires initialized memory
LL | let _val = unsafe { std::mem::MaybeUninit::<[usize; 1]>::uninit().assume_init() };
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ constructing invalid value at .value[0]: encountered uninitialized bytes
|
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
Expand Down
5 changes: 4 additions & 1 deletion tests/fail/validity/uninit_raw_ptr.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,7 @@
#![allow(invalid_value)]

fn main() {
let _val = unsafe { std::mem::MaybeUninit::<*const u8>::uninit().assume_init() };
// The array avoids a `Scalar` layout which detects uninit without even doing validation.
let _val = unsafe { std::mem::MaybeUninit::<[*const u8; 1]>::uninit().assume_init() };
//~^ ERROR: uninitialized
}
6 changes: 3 additions & 3 deletions tests/fail/validity/uninit_raw_ptr.stderr
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
error: Undefined Behavior: using uninitialized data, but this operation requires initialized memory
error: Undefined Behavior: constructing invalid value at .value[0]: encountered uninitialized memory, but expected a raw pointer
--> $DIR/uninit_raw_ptr.rs:LL:CC
|
LL | let _val = unsafe { std::mem::MaybeUninit::<*const u8>::uninit().assume_init() };
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ using uninitialized data, but this operation requires initialized memory
LL | let _val = unsafe { std::mem::MaybeUninit::<[*const u8; 1]>::uninit().assume_init() };
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ constructing invalid value at .value[0]: encountered uninitialized memory, but expected a raw pointer
|
= help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
= help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
Expand Down
10 changes: 0 additions & 10 deletions tests/pass/transmute_fat.rs

This file was deleted.

Loading

0 comments on commit d21b601

Please sign in to comment.