Merge pull request #4109 from RalfJung/flags
Error on some invalid flag combinations
This commit is contained in:
commit
60e3bf4374
4 changed files with 24 additions and 44 deletions
|
@ -294,9 +294,10 @@ environment variable. We first document the most relevant and most commonly used
|
|||
will always fail and `0.0` means it will never fail. Note that setting it to
|
||||
`1.0` will likely cause hangs, since it means programs using
|
||||
`compare_exchange_weak` cannot make progress.
|
||||
* `-Zmiri-disable-isolation` disables host isolation. As a consequence,
|
||||
* `-Zmiri-disable-isolation` disables host isolation. As a consequence,
|
||||
the program has access to host resources such as environment variables, file
|
||||
systems, and randomness.
|
||||
This overwrites a previous `-Zmiri-isolation-error`.
|
||||
* `-Zmiri-disable-leak-backtraces` disables backtraces reports for memory leaks. By default, a
|
||||
backtrace is captured for every allocation when it is created, just in case it leaks. This incurs
|
||||
some memory overhead to store data that is almost never used. This flag is implied by
|
||||
|
@ -317,6 +318,7 @@ environment variable. We first document the most relevant and most commonly used
|
|||
execution with a "permission denied" error being returned to the program.
|
||||
`warn` prints a full backtrace each time that happens; `warn-nobacktrace` is less
|
||||
verbose and shown at most once per operation. `hide` hides the warning entirely.
|
||||
This overwrites a previous `-Zmiri-disable-isolation`.
|
||||
* `-Zmiri-many-seeds=[<from>]..<to>` runs the program multiple times with different seeds for Miri's
|
||||
RNG. With different seeds, Miri will make different choices to resolve non-determinism such as the
|
||||
order in which concurrent threads are scheduled, or the exact addresses assigned to allocations.
|
||||
|
@ -347,8 +349,8 @@ environment variable. We first document the most relevant and most commonly used
|
|||
can increase test coverage by running Miri multiple times with different seeds.
|
||||
* `-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.
|
||||
casting an integer to a pointer will stop execution because the provenance of the pointer
|
||||
cannot be determined.
|
||||
* `-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 program passes the alignment check by pure chance, because things
|
||||
|
@ -437,6 +439,8 @@ to Miri failing to detect cases of undefined behavior in a program.
|
|||
of Rust will be stricter than Tree Borrows. In other words, if you use Tree Borrows,
|
||||
even if your code is accepted today, it might be declared UB in the future.
|
||||
This is much less likely with Stacked Borrows.
|
||||
Using Tree Borrows currently implies `-Zmiri-strict-provenance` because integer-to-pointer
|
||||
casts are not supported in this mode, but that may change in the future.
|
||||
* `-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
|
||||
|
|
|
@ -514,8 +514,6 @@ fn main() {
|
|||
|
||||
let mut rustc_args = vec![];
|
||||
let mut after_dashdash = false;
|
||||
// If user has explicitly enabled/disabled isolation
|
||||
let mut isolation_enabled: Option<bool> = None;
|
||||
|
||||
// Note that we require values to be given with `=`, not with a space.
|
||||
// This matches how rustc parses `-Z`.
|
||||
|
@ -539,6 +537,7 @@ fn main() {
|
|||
miri_config.borrow_tracker = None;
|
||||
} else if arg == "-Zmiri-tree-borrows" {
|
||||
miri_config.borrow_tracker = Some(BorrowTrackerMethod::TreeBorrows);
|
||||
miri_config.provenance_mode = ProvenanceMode::Strict;
|
||||
} else if arg == "-Zmiri-unique-is-unique" {
|
||||
miri_config.unique_is_unique = true;
|
||||
} else if arg == "-Zmiri-disable-data-race-detector" {
|
||||
|
@ -548,19 +547,7 @@ fn main() {
|
|||
miri_config.check_alignment = miri::AlignmentCheck::None;
|
||||
} else if arg == "-Zmiri-symbolic-alignment-check" {
|
||||
miri_config.check_alignment = miri::AlignmentCheck::Symbolic;
|
||||
} else if arg == "-Zmiri-disable-abi-check" {
|
||||
eprintln!(
|
||||
"WARNING: the flag `-Zmiri-disable-abi-check` no longer has any effect; \
|
||||
ABI checks cannot be disabled any more"
|
||||
);
|
||||
} else if arg == "-Zmiri-disable-isolation" {
|
||||
if matches!(isolation_enabled, Some(true)) {
|
||||
show_error!(
|
||||
"-Zmiri-disable-isolation cannot be used along with -Zmiri-isolation-error"
|
||||
);
|
||||
} else {
|
||||
isolation_enabled = Some(false);
|
||||
}
|
||||
miri_config.isolated_op = miri::IsolatedOp::Allow;
|
||||
} else if arg == "-Zmiri-disable-leak-backtraces" {
|
||||
miri_config.collect_leak_backtraces = false;
|
||||
|
@ -569,14 +556,6 @@ fn main() {
|
|||
} else if arg == "-Zmiri-track-weak-memory-loads" {
|
||||
miri_config.track_outdated_loads = true;
|
||||
} else if let Some(param) = arg.strip_prefix("-Zmiri-isolation-error=") {
|
||||
if matches!(isolation_enabled, Some(false)) {
|
||||
show_error!(
|
||||
"-Zmiri-isolation-error cannot be used along with -Zmiri-disable-isolation"
|
||||
);
|
||||
} else {
|
||||
isolation_enabled = Some(true);
|
||||
}
|
||||
|
||||
miri_config.isolated_op = match param {
|
||||
"abort" => miri::IsolatedOp::Reject(miri::RejectOpWith::Abort),
|
||||
"hide" => miri::IsolatedOp::Reject(miri::RejectOpWith::NoWarning),
|
||||
|
@ -622,10 +601,6 @@ fn main() {
|
|||
many_seeds = Some(0..64);
|
||||
} else if arg == "-Zmiri-many-seeds-keep-going" {
|
||||
many_seeds_keep_going = true;
|
||||
} else if let Some(_param) = arg.strip_prefix("-Zmiri-env-exclude=") {
|
||||
show_error!(
|
||||
"`-Zmiri-env-exclude` has been removed; unset env vars before starting Miri instead"
|
||||
);
|
||||
} else if let Some(param) = arg.strip_prefix("-Zmiri-env-forward=") {
|
||||
miri_config.forwarded_env_vars.push(param.to_owned());
|
||||
} else if let Some(param) = arg.strip_prefix("-Zmiri-env-set=") {
|
||||
|
@ -728,13 +703,20 @@ fn main() {
|
|||
"-Zmiri-unique-is-unique only has an effect when -Zmiri-tree-borrows is also used"
|
||||
);
|
||||
}
|
||||
// Tree Borrows + permissive provenance does not work.
|
||||
if miri_config.provenance_mode == ProvenanceMode::Permissive
|
||||
&& matches!(miri_config.borrow_tracker, Some(BorrowTrackerMethod::TreeBorrows))
|
||||
{
|
||||
show_error!(
|
||||
"Tree Borrows does not support integer-to-pointer casts, and is hence not compatible with permissive provenance"
|
||||
);
|
||||
// Tree Borrows implies strict provenance, and is not compatible with native calls.
|
||||
if matches!(miri_config.borrow_tracker, Some(BorrowTrackerMethod::TreeBorrows)) {
|
||||
if miri_config.provenance_mode != ProvenanceMode::Strict {
|
||||
show_error!(
|
||||
"Tree Borrows does not support integer-to-pointer casts, and hence requires strict provenance"
|
||||
);
|
||||
}
|
||||
if miri_config.native_lib.is_some() {
|
||||
show_error!("Tree Borrows is not compatible with calling native functions");
|
||||
}
|
||||
}
|
||||
// Native calls and strict provenance are not compatible.
|
||||
if miri_config.native_lib.is_some() && miri_config.provenance_mode == ProvenanceMode::Strict {
|
||||
show_error!("strict provenance is not compatible with calling native functions");
|
||||
}
|
||||
// You can set either one seed or many.
|
||||
if many_seeds.is_some() && miri_config.seed.is_some() {
|
||||
|
|
|
@ -1,7 +1,4 @@
|
|||
//@revisions: stack tree
|
||||
// Tree Borrows doesn't support int2ptr casts, but let's make sure we don't immediately crash either.
|
||||
//@[tree]compile-flags: -Zmiri-tree-borrows
|
||||
//@[stack]compile-flags: -Zmiri-permissive-provenance
|
||||
//@compile-flags: -Zmiri-permissive-provenance
|
||||
use std::{mem, ptr};
|
||||
|
||||
fn eq_ref<T>(x: &T, y: &T) -> bool {
|
||||
|
|
|
@ -1,7 +1,4 @@
|
|||
//@revisions: stack tree
|
||||
// Tree Borrows doesn't support int2ptr casts, but let's make sure we don't immediately crash either.
|
||||
//@[tree]compile-flags: -Zmiri-tree-borrows
|
||||
//@[stack]compile-flags: -Zmiri-permissive-provenance
|
||||
//@compile-flags: -Zmiri-permissive-provenance
|
||||
|
||||
use std::ptr;
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue