Skip to content

Commit

Permalink
Unique gets special treatment when -Zmiri-unique-is-unique
Browse files Browse the repository at this point in the history
  • Loading branch information
Vanille-N committed Jun 28, 2023
1 parent df1a7c0 commit 71f0db4
Show file tree
Hide file tree
Showing 25 changed files with 486 additions and 13 deletions.
3 changes: 3 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -435,6 +435,9 @@ to Miri failing to detect cases of undefined behavior in a program.
so with this flag.
* `-Zmiri-force-page-size=<num>` overrides the default page size for an architecture, in multiples of 1k.
`4` is default for most targets. This value should always be a power of 2 and nonzero.
* `-Zmiri-unique-is-unique` performs additional aliasing checks for `core::ptr::Unique` to ensure
that it could theoretically be considered `noalias`. This flag is experimental and has
an effect only when used with `-Zmiri-tree-borrows`.

[function ABI]: https://doc.rust-lang.org/reference/items/functions.html#extern-function-qualifier

Expand Down
10 changes: 10 additions & 0 deletions src/bin/miri.rs
Original file line number Diff line number Diff line change
Expand Up @@ -340,6 +340,8 @@ fn main() {
miri_config.borrow_tracker = None;
} else if arg == "-Zmiri-tree-borrows" {
miri_config.borrow_tracker = Some(BorrowTrackerMethod::TreeBorrows);
} else if arg == "-Zmiri-unique-is-unique" {
miri_config.unique_is_unique = true;
} else if arg == "-Zmiri-disable-data-race-detector" {
miri_config.data_race_detector = false;
miri_config.weak_memory_emulation = false;
Expand Down Expand Up @@ -557,6 +559,14 @@ fn main() {
rustc_args.push(arg);
}
}
// `-Zmiri-unique-is-unique` should only be used with `-Zmiri-tree-borrows`
if miri_config.unique_is_unique
&& !matches!(miri_config.borrow_tracker, Some(BorrowTrackerMethod::TreeBorrows))
{
show_error!(
"-Zmiri-unique-is-unique only has an effect when -Zmiri-tree-borrows is also used"
);
}

debug!("rustc arguments: {:?}", rustc_args);
debug!("crate arguments: {:?}", miri_config.args);
Expand Down
5 changes: 5 additions & 0 deletions src/borrow_tracker/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -103,6 +103,8 @@ pub struct GlobalStateInner {
pub tracked_call_ids: FxHashSet<CallId>,
/// Whether to recurse into datatypes when searching for pointers to retag.
pub retag_fields: RetagFields,
/// Whether `core::ptr::Unique` gets special (`Box`-like) handling.
pub unique_is_unique: bool,
}

impl VisitTags for GlobalStateInner {
Expand Down Expand Up @@ -170,6 +172,7 @@ impl GlobalStateInner {
tracked_pointer_tags: FxHashSet<BorTag>,
tracked_call_ids: FxHashSet<CallId>,
retag_fields: RetagFields,
unique_is_unique: bool,
) -> Self {
GlobalStateInner {
borrow_tracker_method,
Expand All @@ -180,6 +183,7 @@ impl GlobalStateInner {
tracked_pointer_tags,
tracked_call_ids,
retag_fields,
unique_is_unique,
}
}

Expand Down Expand Up @@ -244,6 +248,7 @@ impl BorrowTrackerMethod {
config.tracked_pointer_tags.clone(),
config.tracked_call_ids.clone(),
config.retag_fields,
config.unique_is_unique,
))
}
}
Expand Down
47 changes: 44 additions & 3 deletions src/borrow_tracker/tree_borrows/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ use rustc_middle::{
Ty,
},
};
use rustc_span::def_id::DefId;

use crate::*;

Expand Down Expand Up @@ -381,15 +382,19 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
place: &PlaceTy<'tcx, Provenance>,
) -> InterpResult<'tcx> {
let this = self.eval_context_mut();
let retag_fields = this.machine.borrow_tracker.as_mut().unwrap().get_mut().retag_fields;
let mut visitor = RetagVisitor { ecx: this, kind, retag_fields };
let options = this.machine.borrow_tracker.as_mut().unwrap().get_mut();
let retag_fields = options.retag_fields;
let unique_did =
options.unique_is_unique.then(|| this.tcx.lang_items().ptr_unique()).flatten();
let mut visitor = RetagVisitor { ecx: this, kind, retag_fields, unique_did };
return visitor.visit_value(place);

// The actual visitor.
struct RetagVisitor<'ecx, 'mir, 'tcx> {
ecx: &'ecx mut MiriInterpCx<'mir, 'tcx>,
kind: RetagKind,
retag_fields: RetagFields,
unique_did: Option<DefId>,
}
impl<'ecx, 'mir, 'tcx> RetagVisitor<'ecx, 'mir, 'tcx> {
#[inline(always)] // yes this helps in our benchmarks
Expand All @@ -414,6 +419,9 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
self.ecx
}

/// Regardless of how `Unique` is handled, Boxes are always reborrowed.
/// When `Unique` is also reborrowed, then it behaves exactly like `Box`
/// except for the fact that `Box` has a non-zero-sized reborrow.
fn visit_box(&mut self, place: &PlaceTy<'tcx, Provenance>) -> InterpResult<'tcx> {
let new_perm = NewPermission::from_unique_ty(
place.layout.ty,
Expand Down Expand Up @@ -452,6 +460,16 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
// even if field retagging is not enabled. *shrug*)
self.walk_value(place)?;
}
ty::Adt(adt, _) if self.unique_did == Some(adt.did()) => {
let place = inner_ptr_of_unique(self.ecx, place)?;
let new_perm = NewPermission::from_unique_ty(
place.layout.ty,
self.kind,
self.ecx,
/* zero_size */ true,
);
self.retag_ptr_inplace(&place, new_perm)?;
}
_ => {
// Not a reference/pointer/box. Only recurse if configured appropriately.
let recurse = match self.retag_fields {
Expand All @@ -468,7 +486,6 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
}
}
}

Ok(())
}
}
Expand Down Expand Up @@ -564,3 +581,27 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
tree_borrows.give_pointer_debug_name(tag, nth_parent, name)
}
}

/// Takes a place for a `Unique` and turns it into a place with the inner raw pointer.
/// I.e. input is what you get from the visitor upon encountering an `adt` that is `Unique`,
/// and output can be used by `retag_ptr_inplace`.
fn inner_ptr_of_unique<'tcx>(
ecx: &mut MiriInterpCx<'_, 'tcx>,
place: &PlaceTy<'tcx, Provenance>,
) -> InterpResult<'tcx, PlaceTy<'tcx, Provenance>> {
// Follows the same layout as `interpret/visitor.rs:walk_value` for `Box` in
// `rustc_const_eval`, just with one fewer layer.
// Here we have a `Unique(NonNull(*mut), PhantomData)`
assert_eq!(place.layout.fields.count(), 2, "Unique must have exactly 2 fields");
let (nonnull, phantom) = (ecx.place_field(place, 0)?, ecx.place_field(place, 1)?);
assert!(
phantom.layout.ty.ty_adt_def().is_some_and(|adt| adt.is_phantom_data()),
"2nd field of `Unique` should be `PhantomData` but is `{:?}`",
phantom.layout.ty,
);
// Now down to `NonNull(*mut)`
assert_eq!(nonnull.layout.fields.count(), 1, "NonNull must have exactly 1 field");
let ptr = ecx.place_field(&nonnull, 0)?;
// Finally a plain `*mut`
Ok(ptr)
}
5 changes: 5 additions & 0 deletions src/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,10 @@ pub struct MiriConfig {
pub validate: bool,
/// Determines if Stacked Borrows or Tree Borrows is enabled.
pub borrow_tracker: Option<BorrowTrackerMethod>,
/// Whether `core::ptr::Unique` receives special treatment.
/// If `true` then `Unique` is reborrowed with its own new tag and permission,
/// otherwise `Unique` is just another raw pointer.
pub unique_is_unique: bool,
/// Controls alignment checking.
pub check_alignment: AlignmentCheck,
/// Controls function [ABI](Abi) checking.
Expand Down Expand Up @@ -156,6 +160,7 @@ impl Default for MiriConfig {
env: vec![],
validate: true,
borrow_tracker: Some(BorrowTrackerMethod::StackedBorrows),
unique_is_unique: false,
check_alignment: AlignmentCheck::Int,
check_abi: true,
isolated_op: IsolatedOp::Reject(RejectOpWith::Abort),
Expand Down
15 changes: 15 additions & 0 deletions tests/fail/tree_borrows/children-can-alias.default.stderr
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
error: Undefined Behavior: entering unreachable code
--> $DIR/children-can-alias.rs:LL:CC
|
LL | std::hint::unreachable_unchecked();
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ entering unreachable code
|
= 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/children-can-alias.rs:LL:CC

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

error: aborting due to previous error

59 changes: 59 additions & 0 deletions tests/fail/tree_borrows/children-can-alias.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
//@revisions: default uniq
//@compile-flags: -Zmiri-tree-borrows
//@[uniq]compile-flags: -Zmiri-unique-is-unique

//! This is NOT intended behavior.
//! We should eventually find a solution so that the version with `Unique` passes too,
//! otherwise `Unique` is more strict than `&mut`!

#![feature(ptr_internals)]

use core::ptr::addr_of_mut;
use core::ptr::Unique;

fn main() {
let mut data = 0u8;
let raw = addr_of_mut!(data);
unsafe {
raw_children_of_refmut_can_alias(&mut *raw);
raw_children_of_unique_can_alias(Unique::new_unchecked(raw));

// Ultimately the intended behavior is that both above tests would
// succeed.
std::hint::unreachable_unchecked();
//~[default]^ ERROR: entering unreachable code
}
}

unsafe fn raw_children_of_refmut_can_alias(x: &mut u8) {
let child1 = addr_of_mut!(*x);
let child2 = addr_of_mut!(*x);
// We create two raw aliases of `x`: they have the exact same
// tag and can be used interchangeably.
child1.write(1);
child2.write(2);
child1.write(1);
child2.write(2);
}

unsafe fn raw_children_of_unique_can_alias(x: Unique<u8>) {
let child1 = x.as_ptr();
let child2 = x.as_ptr();
// Under `-Zmiri-unique-is-unique`, `Unique` accidentally offers more guarantees
// than `&mut`. Not because it responds differently to accesses but because
// there is no easy way to obtain a copy with the same tag.
//
// The closest (non-hack) attempt is two calls to `as_ptr`.
// - Without `-Zmiri-unique-is-unique`, independent `as_ptr` calls return pointers
// with the same tag that can thus be used interchangeably.
// - With the current implementation of `-Zmiri-unique-is-unique`, they return cousin
// tags with permissions that do not tolerate aliasing.
// Eventually we should make such aliasing allowed in some situations
// (e.g. when there is no protector), which will probably involve
// introducing a new kind of permission.
child1.write(1);
child2.write(2);
//~[uniq]^ ERROR: /write access through .* is forbidden/
child1.write(1);
child2.write(2);
}
37 changes: 37 additions & 0 deletions tests/fail/tree_borrows/children-can-alias.uniq.stderr
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
error: Undefined Behavior: write access through <TAG> is forbidden
--> $DIR/children-can-alias.rs:LL:CC
|
LL | child2.write(2);
| ^^^^^^^^^^^^^^^ write access through <TAG> is forbidden
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
= help: the accessed tag <TAG> is a child of the conflicting tag <TAG>
= help: the conflicting tag <TAG> has state Disabled which forbids this child write access
help: the accessed tag <TAG> was created here
--> $DIR/children-can-alias.rs:LL:CC
|
LL | let child2 = x.as_ptr();
| ^^^^^^^^^^
help: the conflicting tag <TAG> was created here, in the initial state Reserved
--> $DIR/children-can-alias.rs:LL:CC
|
LL | let child2 = x.as_ptr();
| ^
help: the conflicting tag <TAG> later transitioned to Disabled due to a foreign write access at offsets [0x0..0x1]
--> $DIR/children-can-alias.rs:LL:CC
|
LL | child1.write(1);
| ^^^^^^^^^^^^^^^
= help: this transition corresponds to a loss of read and write permissions
= note: BACKTRACE (of the first span):
= note: inside `raw_children_of_unique_can_alias` at $DIR/children-can-alias.rs:LL:CC
note: inside `main`
--> $DIR/children-can-alias.rs:LL:CC
|
LL | raw_children_of_unique_can_alias(Unique::new_unchecked(raw));
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

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

error: aborting due to previous error

32 changes: 32 additions & 0 deletions tests/fail/tree_borrows/unique.default.stderr
Original file line number Diff line number Diff line change
@@ -0,0 +1,32 @@
error: Undefined Behavior: write access through <TAG> is forbidden
--> $DIR/unique.rs:LL:CC
|
LL | *uniq.as_ptr() = 3;
| ^^^^^^^^^^^^^^^^^^ write access through <TAG> is forbidden
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
= help: the accessed tag <TAG> has state Frozen which forbids this child write access
help: the accessed tag <TAG> was created here, in the initial state Reserved
--> $DIR/unique.rs:LL:CC
|
LL | let refmut = &mut data;
| ^^^^^^^^^
help: the accessed tag <TAG> later transitioned to Active due to a child write access at offsets [0x0..0x1]
--> $DIR/unique.rs:LL:CC
|
LL | *uniq.as_ptr() = 1; // activation
| ^^^^^^^^^^^^^^^^^^
= help: this transition corresponds to the first write to a 2-phase borrowed mutable reference
help: the accessed tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x1]
--> $DIR/unique.rs:LL:CC
|
LL | let _definitely_parent = data; // definitely Frozen by now
| ^^^^
= help: this transition corresponds to a loss of write permissions
= note: BACKTRACE (of the first span):
= note: inside `main` at $DIR/unique.rs:LL:CC

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

error: aborting due to previous error

27 changes: 27 additions & 0 deletions tests/fail/tree_borrows/unique.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
//@revisions: default uniq
//@compile-flags: -Zmiri-tree-borrows
//@[uniq]compile-flags: -Zmiri-unique-is-unique

// A pattern that detects if `Unique` is treated as exclusive or not:
// activate the pointer behind a `Unique` then do a read that is parent
// iff `Unique` was specially reborrowed.

#![feature(ptr_internals)]
use core::ptr::Unique;

fn main() {
let mut data = 0u8;
let refmut = &mut data;
let rawptr = refmut as *mut u8;

unsafe {
let uniq = Unique::new_unchecked(rawptr);
*uniq.as_ptr() = 1; // activation
let _maybe_parent = *rawptr; // maybe becomes Frozen
*uniq.as_ptr() = 2;
//~[uniq]^ ERROR: /write access through .* is forbidden/
let _definitely_parent = data; // definitely Frozen by now
*uniq.as_ptr() = 3;
//~[default]^ ERROR: /write access through .* is forbidden/
}
}
38 changes: 38 additions & 0 deletions tests/fail/tree_borrows/unique.uniq.stderr
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
error: Undefined Behavior: write access through <TAG> is forbidden
--> $DIR/unique.rs:LL:CC
|
LL | *uniq.as_ptr() = 2;
| ^^^^^^^^^^^^^^^^^^ write access through <TAG> is forbidden
|
= help: this indicates a potential bug in the program: it performed an invalid operation, but the Tree Borrows rules it violated are still experimental
= help: the accessed tag <TAG> is a child of the conflicting tag <TAG>
= help: the conflicting tag <TAG> has state Frozen which forbids this child write access
help: the accessed tag <TAG> was created here
--> $DIR/unique.rs:LL:CC
|
LL | *uniq.as_ptr() = 2;
| ^^^^^^^^^^^^^
help: the conflicting tag <TAG> was created here, in the initial state Reserved
--> $DIR/unique.rs:LL:CC
|
LL | let uniq = Unique::new_unchecked(rawptr);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
help: the conflicting tag <TAG> later transitioned to Active due to a child write access at offsets [0x0..0x1]
--> $DIR/unique.rs:LL:CC
|
LL | *uniq.as_ptr() = 1; // activation
| ^^^^^^^^^^^^^^^^^^
= help: this transition corresponds to the first write to a 2-phase borrowed mutable reference
help: the conflicting tag <TAG> later transitioned to Frozen due to a foreign read access at offsets [0x0..0x1]
--> $DIR/unique.rs:LL:CC
|
LL | let _maybe_parent = *rawptr; // maybe becomes Frozen
| ^^^^^^^
= help: this transition corresponds to a loss of write permissions
= note: BACKTRACE (of the first span):
= note: inside `main` at $DIR/unique.rs:LL:CC

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

error: aborting due to previous error

Loading

0 comments on commit 71f0db4

Please sign in to comment.