-
-
Notifications
You must be signed in to change notification settings - Fork 14.6k
miri/const eval: support MaybeDangling
#150446
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
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
WaffleLapkin marked this conversation as resolved.
Show resolved
Hide resolved
|
RalfJung marked this conversation as resolved.
Show resolved
Hide resolved
|
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,15 @@ | ||
| // Test that an unaligned `MaybeDangling<&u8>` is still detected as UB. | ||
| // | ||
| //@compile-flags: -Zmiri-disable-stacked-borrows | ||
| #![feature(maybe_dangling)] | ||
|
|
||
| use std::mem::{MaybeDangling, transmute}; | ||
|
|
||
| fn main() { | ||
| let a = [1u16, 0u16]; | ||
| unsafe { | ||
| let unaligned = MaybeDangling::new(a.as_ptr().byte_add(1)); | ||
| transmute::<MaybeDangling<*const u16>, MaybeDangling<&u16>>(unaligned) | ||
| //~^ ERROR: Undefined Behavior: constructing invalid value: encountered an unaligned reference | ||
| }; | ||
| } |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| error: Undefined Behavior: constructing invalid value: encountered an unaligned reference (required ALIGN byte alignment but found ALIGN) | ||
| --> tests/fail/unaligned_pointers/maybe_dangling_unalighed.rs:LL:CC | ||
| | | ||
| LL | transmute::<MaybeDangling<*const u16>, MaybeDangling<&u16>>(unaligned) | ||
| | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here | ||
| | | ||
| = 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: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
|
||
| error: aborting due to 1 previous error | ||
|
|
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This isn't even a borrow checking thing. Please move the test to |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| // Test that a null `MaybeDangling<&u8>` is still detected as UB. | ||
| // | ||
| //@compile-flags: -Zmiri-disable-stacked-borrows | ||
| #![feature(maybe_dangling)] | ||
|
|
||
| use std::mem::{MaybeDangling, transmute}; | ||
| use std::ptr::null; | ||
|
|
||
| fn main() { | ||
| let null = MaybeDangling::new(null()); | ||
| unsafe { transmute::<MaybeDangling<*const u8>, MaybeDangling<&u8>>(null) }; | ||
| //~^ ERROR: Undefined Behavior: constructing invalid value: encountered a null reference | ||
| } |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,13 @@ | ||
| error: Undefined Behavior: constructing invalid value: encountered a null reference | ||
| --> tests/fail/validity/maybe_dangling_null.rs:LL:CC | ||
| | | ||
| LL | unsafe { transmute::<MaybeDangling<*const u8>, MaybeDangling<&u8>>(null) }; | ||
| | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Undefined Behavior occurred here | ||
| | | ||
| = 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: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace | ||
|
|
||
| error: aborting due to 1 previous error | ||
|
|
|
Member
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Given that this case was contentious, please also add a test like // Under the current models, we do not forbid writing through
// `MaybeDangling<&i32>`. That's not yet finally decided, but meanwhile
// ensure we document this and notice when it changes.
fn write_through_shr(x: MaybeDangling<&i32>) {
let y: *mut i32 = transmute(x);
y.write(1);
}
let mutref = &mut 0i32;
write_through_shr(transmute(mutref)); |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,59 @@ | ||
| // Check that `MaybeDangling` actually prevents UB when it wraps dangling | ||
| // boxes and references | ||
| // | ||
| //@revisions: stack tree | ||
| //@[tree]compile-flags: -Zmiri-tree-borrows | ||
| #![feature(maybe_dangling)] | ||
|
|
||
| use std::mem::{self, MaybeDangling}; | ||
| use std::ptr::drop_in_place; | ||
|
|
||
| fn main() { | ||
| boxy(); | ||
| reference(); | ||
| write_through_shared_ref(); | ||
| } | ||
|
|
||
| fn boxy() { | ||
| let mut x = MaybeDangling::new(Box::new(1)); | ||
|
|
||
| // make the box dangle | ||
| unsafe { drop_in_place(x.as_mut()) }; | ||
|
|
||
| // move the dangling box (without `MaybeDangling` this causes UB) | ||
| let x: MaybeDangling<Box<u32>> = x; | ||
|
|
||
| mem::forget(x); | ||
| } | ||
|
|
||
| fn reference() { | ||
| let x = { | ||
| let local = 0; | ||
|
|
||
| // erase the lifetime to make a dangling reference | ||
| unsafe { | ||
| mem::transmute::<MaybeDangling<&u32>, MaybeDangling<&u32>>(MaybeDangling::new(&local)) | ||
| } | ||
| }; | ||
|
|
||
| // move the dangling reference (without `MaybeDangling` this causes UB) | ||
| let _x: MaybeDangling<&u32> = x; | ||
| } | ||
|
|
||
| fn write_through_shared_ref() { | ||
| // Under the current models, we do not forbid writing through | ||
| // `MaybeDangling<&i32>`. That's not yet finally decided, but meanwhile | ||
| // ensure we document this and notice when it changes. | ||
|
|
||
| unsafe { | ||
| let mutref = &mut 0; | ||
| write_through_shr(mem::transmute(mutref)); | ||
| } | ||
|
|
||
| fn write_through_shr(x: MaybeDangling<&i32>) { | ||
| unsafe { | ||
| let y: *mut i32 = mem::transmute(x); | ||
| y.write(1); | ||
| } | ||
| } | ||
| } |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,6 +1,6 @@ | ||
| 0..1: [ SharedReadWrite<TAG> ] | ||
| 0..1: [ SharedReadWrite<TAG> ] | ||
| 0..1: [ SharedReadWrite<TAG> ] | ||
| 0..1: [ SharedReadWrite<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> ] | ||
| 0..1: [ SharedReadWrite<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> SharedReadOnly<TAG> ] | ||
| 0..1: [ SharedReadWrite<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> Unique<TAG> ] | ||
| 0..1: [ SharedReadWrite<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> Disabled<TAG> SharedReadOnly<TAG> ] | ||
| 0..1: [ unknown-bottom(..<TAG>) ] |
Uh oh!
There was an error while loading. Please reload this page.