Skip to content

Commit

Permalink
make full field retagging the default
Browse files Browse the repository at this point in the history
  • Loading branch information
RalfJung committed Jul 17, 2023
1 parent d44deca commit 67e780e
Show file tree
Hide file tree
Showing 7 changed files with 35 additions and 27 deletions.
14 changes: 5 additions & 9 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -400,15 +400,11 @@ to Miri failing to detect cases of undefined behavior in a program.
application instead of raising an error within the context of Miri (and halting
execution). Note that code might not expect these operations to ever panic, so
this flag can lead to strange (mis)behavior.
* `-Zmiri-retag-fields` changes Stacked Borrows retagging to recurse into *all* fields.
This means that references in fields of structs/enums/tuples/arrays/... are retagged,
and in particular, they are protected when passed as function arguments.
(The default is to recurse only in cases where rustc would actually emit a `noalias` attribute.)
* `-Zmiri-retag-fields=<all|none|scalar>` controls when Stacked Borrows retagging recurses into
fields. `all` means it always recurses (like `-Zmiri-retag-fields`), `none` means it never
recurses, `scalar` (the default) means it only recurses for types where we would also emit
`noalias` annotations in the generated LLVM IR (types passed as individual scalars or pairs of
scalars). Setting this to `none` is **unsound**.
* `-Zmiri-retag-fields[=<all|none|scalar>]` controls when Stacked Borrows retagging recurses into
fields. `all` means it always recurses (the default, and equivalent to `-Zmiri-retag-fields`
without an explicit value), `none` means it never recurses, `scalar` means it only recurses for
types where we would also emit `noalias` annotations in the generated LLVM IR (types passed as
individual scalars or pairs of scalars). Setting this to `none` is **unsound**.
* `-Zmiri-tag-gc=<blocks>` configures how often the pointer tag garbage collector runs. The default
is to search for and remove unreachable tags once every `10000` basic blocks. Setting this to
`0` disables the garbage collector, which causes some programs to have explosive memory usage
Expand Down
2 changes: 1 addition & 1 deletion src/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,7 @@ impl Default for MiriConfig {
mute_stdout_stderr: false,
preemption_rate: 0.01, // 1%
report_progress: None,
retag_fields: RetagFields::OnlyScalar,
retag_fields: RetagFields::Yes,
external_so_file: None,
gc_interval: 10_000,
num_cpus: 1,
Expand Down
5 changes: 3 additions & 2 deletions tests/fail/generator-pinned-moved.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
//@compile-flags: -Zmiri-disable-validation
//@compile-flags: -Zmiri-disable-validation -Zmiri-disable-stacked-borrows
#![feature(generators, generator_trait)]

use std::{
Expand All @@ -10,9 +10,10 @@ fn firstn() -> impl Generator<Yield = u64, Return = ()> {
static move || {
let mut num = 0;
let num = &mut num;
*num += 0;

yield *num;
*num += 1; //~ ERROR: dereferenced after this allocation got freed
*num += 1; //~ERROR: dereferenced after this allocation got freed
}
}

Expand Down
38 changes: 26 additions & 12 deletions tests/pass/generator.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ use std::ptr;
use std::sync::atomic::{AtomicUsize, Ordering};

fn basic() {
fn finish<T>(mut amt: usize, mut t: T) -> T::Return
fn finish<T>(mut amt: usize, self_referential: bool, mut t: T) -> T::Return
where
T: Generator<Yield = usize>,
{
Expand All @@ -22,7 +22,10 @@ fn basic() {
loop {
let state = t.as_mut().resume(());
// Test if the generator is valid (according to type invariants).
let _ = unsafe { ManuallyDrop::new(ptr::read(t.as_mut().get_unchecked_mut())) };
// For self-referential generators however this is UB!
if !self_referential {
let _ = unsafe { ManuallyDrop::new(ptr::read(t.as_mut().get_unchecked_mut())) };
}
match state {
GeneratorState::Yielded(y) => {
amt -= y;
Expand All @@ -40,9 +43,9 @@ fn basic() {
panic!()
}

finish(1, || yield 1);
finish(1, false, || yield 1);

finish(3, || {
finish(3, false, || {
let mut x = 0;
yield 1;
x += 1;
Expand All @@ -52,27 +55,27 @@ fn basic() {
assert_eq!(x, 2);
});

finish(7 * 8 / 2, || {
finish(7 * 8 / 2, false, || {
for i in 0..8 {
yield i;
}
});

finish(1, || {
finish(1, false, || {
if true {
yield 1;
} else {
}
});

finish(1, || {
finish(1, false, || {
if false {
} else {
yield 1;
}
});

finish(2, || {
finish(2, false, || {
if {
yield 1;
false
Expand All @@ -83,9 +86,20 @@ fn basic() {
yield 1;
});

// also test a self-referential generator
// also test self-referential generators
assert_eq!(
finish(5, true, static || {
let mut x = 5;
let y = &mut x;
*y = 5;
yield *y;
*y = 10;
x
}),
10
);
assert_eq!(
finish(5, || {
finish(5, true, || {
let mut x = Box::new(5);
let y = &mut *x;
*y = 5;
Expand All @@ -97,7 +111,7 @@ fn basic() {
);

let b = true;
finish(1, || {
finish(1, false, || {
yield 1;
if b {
return;
Expand All @@ -109,7 +123,7 @@ fn basic() {
drop(x);
});

finish(3, || {
finish(3, false, || {
yield 1;
#[allow(unreachable_code)]
let _x: (String, !) = (String::new(), {
Expand Down
1 change: 0 additions & 1 deletion tests/pass/stacked-borrows/interior_mutability.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
//@compile-flags: -Zmiri-retag-fields
use std::cell::{Cell, Ref, RefCell, RefMut, UnsafeCell};
use std::mem::{self, MaybeUninit};

Expand Down
1 change: 0 additions & 1 deletion tests/pass/stacked-borrows/stacked-borrows.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
//@compile-flags: -Zmiri-retag-fields
#![feature(allocator_api)]
use std::ptr;

Expand Down
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@
//@compile-flags: -Zmiri-retag-fields
// Checks that the test does not run forever (which relies on a fast path).

#![allow(dropping_copy_types)]
Expand Down

0 comments on commit 67e780e

Please sign in to comment.