Skip to content

Commit

Permalink
Auto merge of #2147 - RalfJung:readme, r=RalfJung
Browse files Browse the repository at this point in the history
split flag section into common and advanced flags

As discussed with `@oli-obk` . However I was not always sure which flags to put where, so if you think some flags should be in the other category please let me know. :)
  • Loading branch information
bors committed May 23, 2022
2 parents 27b40f1 + 4d9eafe commit 24c16b9
Showing 1 changed file with 41 additions and 35 deletions.
76 changes: 41 additions & 35 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -258,33 +258,12 @@ up the sysroot. If you are using `miri` (the Miri driver) directly, see the
[miri-flags]: #miri--z-flags-and-environment-variables

Miri adds its own set of `-Z` flags, which are usually set via the `MIRIFLAGS`
environment variable. Some of these are **unsound**, which means they can lead
to Miri failing to detect cases of undefined behavior in a program.
environment variable. We first document the most relevant and most commonly used flags:

* `-Zmiri-check-number-validity` enables checking of integer and float validity
(e.g., they must be initialized and not carry pointer provenance) as part of
enforcing validity invariants. This has no effect when
`-Zmiri-disable-validation` is present.
* `-Zmiri-compare-exchange-weak-failure-rate=<rate>` changes the failure rate of
`compare_exchange_weak` operations. The default is `0.8` (so 4 out of 5 weak ops will fail).
You can change it to any value between `0.0` and `1.0`, where `1.0` means it
will always fail and `0.0` means it will never fail.
* `-Zmiri-disable-abi-check` disables checking [function ABI]. Using this flag
is **unsound**.
* `-Zmiri-disable-alignment-check` disables checking pointer alignment, so you
can focus on other failures, but it means Miri can miss bugs in your program.
Using this flag is **unsound**.
* `-Zmiri-disable-data-race-detector` disables checking for data races. Using
this flag is **unsound**.
* `-Zmiri-disable-stacked-borrows` disables checking the experimental
[Stacked Borrows] aliasing rules. This can make Miri run faster, but it also
means no aliasing violations will be detected. Using this flag is **unsound**
(but the affected soundness rules are experimental).
* `-Zmiri-disable-validation` disables enforcing validity invariants, which are
enforced by default. This is mostly useful to focus on other failures (such
as out-of-bounds accesses) first. Setting this flag means Miri can miss bugs
in your program. However, this can also help to make Miri run faster. Using
this flag is **unsound**.
* `-Zmiri-disable-isolation` disables host isolation. As a consequence,
the program has access to host resources such as environment variables, file
systems, and randomness.
Expand All @@ -299,12 +278,50 @@ to Miri failing to detect cases of undefined behavior in a program.
cannot be accessed by the program. Can be used multiple times to exclude several variables. The
`TERM` environment variable is excluded by default to [speed up the test
harness](https://github.com/rust-lang/miri/issues/1702). This has no effect unless
`-Zmiri-disable-validation` is also set.
`-Zmiri-disable-isolation` is also set.
* `-Zmiri-env-forward=<var>` forwards the `var` environment variable to the interpreted program. Can
be used multiple times to forward several variables. This has no effect if
`-Zmiri-disable-validation` is set.
`-Zmiri-disable-isolation` is set.
* `-Zmiri-ignore-leaks` disables the memory leak checker, and also allows some
remaining threads to exist when the main thread exits.
* `-Zmiri-seed=<hex>` configures the seed of the RNG that Miri uses to resolve
non-determinism. This RNG is used to pick base addresses for allocations. When
isolation is enabled (the default), this is also used to emulate system
entropy. The default seed is 0. You can increase test coverage by running Miri
multiple times with different seeds.
**NOTE**: This entropy is not good enough for cryptographic use! Do not
generate secret keys in Miri or perform other kinds of cryptographic
operations that rely on proper random numbers.
* `-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. Also implies `-Zmiri-tag-raw-pointers` and
`-Zmiri-check-number-validity`.

The remaining flags are for advanced use only, and more likely to change or be removed.
Some of these are **unsound**, which means they can lead
to Miri failing to detect cases of undefined behavior in a program.

* `-Zmiri-check-number-validity` enables checking of integer and float validity
(e.g., they must be initialized and not carry pointer provenance) as part of
enforcing validity invariants. This has no effect when
`-Zmiri-disable-validation` is present.
* `-Zmiri-disable-abi-check` disables checking [function ABI]. Using this flag
is **unsound**.
* `-Zmiri-disable-alignment-check` disables checking pointer alignment, so you
can focus on other failures, but it means Miri can miss bugs in your program.
Using this flag is **unsound**.
* `-Zmiri-disable-data-race-detector` disables checking for data races. Using
this flag is **unsound**.
* `-Zmiri-disable-stacked-borrows` disables checking the experimental
[Stacked Borrows] aliasing rules. This can make Miri run faster, but it also
means no aliasing violations will be detected. Using this flag is **unsound**
(but the affected soundness rules are experimental).
* `-Zmiri-disable-validation` disables enforcing validity invariants, which are
enforced by default. This is mostly useful to focus on other failures (such
as out-of-bounds accesses) first. Setting this flag means Miri can miss bugs
in your program. However, this can also help to make Miri run faster. Using
this flag is **unsound**.
* `-Zmiri-measureme=<name>` enables `measureme` profiling for the interpreted program.
This can be used to find which parts of your program are executing slowly under Miri.
The profile is written out to a file with the prefix `<name>`, and can be processed
Expand All @@ -329,17 +346,6 @@ to Miri failing to detect cases of undefined behavior in a program.
memory/pointers which is subject to these operations. Also note that this flag
is currently incompatible with Stacked Borrows, so you will have to also pass
`-Zmiri-disable-stacked-borrows` to use this.
* `-Zmiri-seed=<hex>` configures the seed of the RNG that Miri uses to resolve
non-determinism. This RNG is used to pick base addresses for allocations.
When isolation is enabled (the default), this is also used to emulate system
entropy. The default seed is 0. **NOTE**: This entropy is not good enough
for cryptographic use! Do not generate secret keys in Miri or perform other
kinds of cryptographic operations that rely on proper random numbers.
* `-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. Also implies `-Zmiri-tag-raw-pointers` and
`-Zmiri-check-number-validity`.
* `-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
Expand Down

0 comments on commit 24c16b9

Please sign in to comment.