Merge pull request #4109 from RalfJung/flags

Error on some invalid flag combinations

README.md

@@ -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

src/bin/miri.rs

@@ -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() {

tests/pass/ptr_int_casts.rs

@@ -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 {

tests/pass/ptr_int_from_exposed.rs

@@ -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;