split flag section into common and advanced flags
This commit is contained in:
parent
ab03d32622
commit
a3a2a474cb
1 changed files with 39 additions and 33 deletions
72
README.md
72
README.md
|
|
@ -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.
|
||||
|
|
@ -305,6 +284,44 @@ to Miri failing to detect cases of undefined behavior in a program.
|
|||
`-Zmiri-disable-validation` 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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue