or an invalid enum discriminant)
* **Experimental**: Violations of the [Stacked Borrows] rules governing aliasing
for reference types
-* **Experimental**: Data races (but no weak memory effects)
+* **Experimental**: Data races
On top of that, Miri will also tell you about memory leaks: when there is memory
still allocated at the end of the execution, and that memory is not reachable
from a global `static`, Miri will raise an error.
+Miri supports almost all Rust language features; in particular, unwinding and
+concurrency are properly supported (including some experimental emulation of
+weak memory effects, i.e., reads can return outdated values).
+
You can use Miri to emulate programs on other targets, e.g. to ensure that
byte-level data manipulation works correctly both on little-endian and
big-endian systems. See
positives here, so if your program runs fine in Miri right now that is by no
means a guarantee that it is UB-free when these questions get answered.
- In particular, Miri does currently not check that integers/floats are
- initialized or that references point to valid data.
+ In particular, Miri does currently not check that references point to valid data.
* If the program relies on unspecified details of how data is laid out, it will
still run fine in Miri -- but might break (including causing UB) on different
compiler versions or different platforms.
not support networking. System API support varies between targets; if you run
on Windows it is a good idea to use `--target x86_64-unknown-linux-gnu` to get
better support.
-* Threading support is not finished yet. E.g., weak memory effects are not
- emulated and spin loops (without syscalls) just loop forever. There is no
- threading support on Windows.
+* Weak memory emulation may produce weak behaivours unobservable by compiled
+ programs running on real hardware when `SeqCst` fences are used, and it cannot
+ produce all behaviors possibly observable on real hardware.
[rust]: https://www.rust-lang.org/
[mir]: https://github.com/rust-lang/rfcs/blob/master/text/1211-mir.md
snippet calls Miri in a loop with different values for the seed:
```
-for seed in $({ echo obase=16; seq 255; } | bc); do
+for seed in $({ echo obase=16; seq 0 255; } | bc); do
MIRIFLAGS=-Zmiri-seed=$seed cargo miri test || { echo "Last seed: $seed"; break; };
done
```
[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**.
+ will always fail and `0.0` means it will never fail. Note than 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,
the program has access to host resources such as environment variables, file
systems, and randomness.
and `warn-nobacktrace` are the supported actions. The default is to `abort`,
which halts the machine. Some (but not all) operations also support continuing
execution with a "permission denied" error being returned to the program.
- `warn` prints a full backtrace when that happen; `warn-nobacktrace` is less
+ `warn` prints a full backtrace when that happens; `warn-nobacktrace` is less
verbose. `hide` hides the warning entirely.
* `-Zmiri-env-exclude=<var>` keeps the `var` environment variable isolated from the host so that it
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-permissive-provenance` disables the warning for integer-to-pointer casts and
+ [`ptr::from_exposed_addr`](https://doc.rust-lang.org/nightly/std/ptr/fn.from_exposed_addr.html).
+ This will necessarily miss some bugs as those operations are not efficiently and accurately
+ implementable in a sanitizer, but it will only miss bugs that concern memory/pointers which is
+ subject to these operations.
+* `-Zmiri-preemption-rate` configures the probability that at the end of a basic block, the active
+ thread will be preempted. The default is `0.01` (i.e., 1%). Setting this to `0` disables
+ preemption.
+* `-Zmiri-report-progress` makes Miri print the current stacktrace every now and then, so you can
+ tell what it is doing when a program just keeps running. You can customize how frequently the
+ report is printed via `-Zmiri-report-progress=<blocks>`, which prints the report every N basic
+ blocks.
+* `-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, to determine preemption and failure of
+ `compare_exchange_weak`, and to control store buffering for weak memory emulation. 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.
+* `-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
+ "happened to be" sufficiently aligned -- there is no UB in this execution but there would be UB in
+ others. To avoid such cases, the symbolic alignment check only takes into account the requested
+ alignment of the relevant allocation, and the offset into that allocation. This avoids missing
+ such bugs, but it also incurs some false positives when the code does manual integer arithmetic to
+ ensure alignment. (The standard library `align_to` method works fine in both modes; under
+ symbolic alignment it only fills the middle slice when the allocation guarantees sufficient
+ alignment.)
+
+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-allow-uninit-numbers` disables the check to ensure that number types (integer and float
+ types) always hold initialized data. (They must still be initialized when any actual operation,
+ such as arithmetic, is performed.) Using this flag is **unsound** and
+ [deprecated](https://github.com/rust-lang/miri/issues/2187). This has no effect when
+ `-Zmiri-disable-validation` is present.
+* `-Zmiri-allow-ptr-int-transmute` makes Miri more accepting of transmutation between pointers and
+ integers via `mem::transmute` or union/pointer type punning. This has two effects: it disables the
+ check against integers storing a pointer (i.e., data with provenance), thus allowing
+ pointer-to-integer transmutation, and it treats integer-to-pointer transmutation as equivalent to
+ a cast. Implies `-Zmiri-permissive-provenance`. Using this flag is **unsound** and
+ [deprecated](https://github.com/rust-lang/miri/issues/2188).
+* `-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**. This implies `-Zmiri-disable-weak-memory-emulation`.
+* `-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-weak-memory-emulation` disables the emulation of some C++11 weak
+ memory effects.
* `-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
using the tools in the repository https://github.com/rust-lang/measureme.
* `-Zmiri-mute-stdout-stderr` silently ignores all writes to stdout and stderr,
but reports to the program that it did actually write. This is useful when you
- are not interested in the actual program's output, but only want to see miri's
+ are not interested in the actual program's output, but only want to see Miri's
errors and warnings.
* `-Zmiri-panic-on-unsupported` will makes some forms of unsupported functionality,
such as FFI and unsupported syscalls, panic within the context of the emulated
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-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
- program passes the alignment check by pure chance, because things "happened to
- be" sufficiently aligned -- there is no UB in this execution but there would
- be UB in others. To avoid such cases, the symbolic alignment check only takes
- into account the requested alignment of the relevant allocation, and the
- offset into that allocation. This avoids missing such bugs, but it also
- incurs some false positives when the code does manual integer arithmetic to
- ensure alignment. (The standard library `align_to` method works fine in both
- modes; under symbolic alignment it only fills the middle slice when the
- allocation guarantees sufficient alignment.)
+* `-Zmiri-retag-fields` changes Stacked Borrows retagging to recurse into 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.
* `-Zmiri-track-alloc-id=<id1>,<id2>,...` shows a backtrace when the given allocations are
being allocated or freed. This helps in debugging memory leaks and
use after free bugs. Specifying this argument multiple times does not overwrite the previous
happening and where in your code would be a good place to look for it.
Specifying this argument multiple times does not overwrite the previous
values, instead it appends its values to the list. Listing a tag multiple times has no effect.
-* `-Zmiri-tag-raw-pointers` makes Stacked Borrows assign proper tags even for raw pointers. This can
- make valid code using int-to-ptr casts fail to pass the checks, but also can help identify latent
- aliasing issues in code that Miri accepts by default. You can recognize false positives by
- `<untagged>` occurring in the message -- this indicates a pointer that was cast from an integer,
- so Miri was unable to track this pointer. Note that it is not currently guaranteed that code that
- works with `-Zmiri-tag-raw-pointers` also works without `-Zmiri-tag-raw-pointers`, but for the
- vast majority of code, this will be the case.
[function ABI]: https://doc.rust-lang.org/reference/items/functions.html#extern-function-qualifier
* `MIRI_TEST_TARGET` (recognized by the test suite) indicates which target
architecture to test against. `miri` and `cargo miri` accept the `--target`
flag for the same purpose.
+* `MIRI_NO_STD` (recognized by `cargo miri` and the test suite) makes sure that the target's
+ sysroot is built without libstd. This allows testing and running no_std programs.
+* `MIRI_BLESS` (recognized by the test suite) overwrite all `stderr` and `stdout` files
+ instead of checking whether the output matches.
+* `MIRI_SKIP_UI_CHECKS` (recognized by the test suite) don't check whether the
+ `stderr` or `stdout` files match the actual output. Useful for the rustc test suite
+ which has subtle differences that we don't care about.
The following environment variables are *internal* and must not be used by
anyone but Miri itself. They are used to communicate between different Miri
This project began as part of an undergraduate research course in 2015 by
@solson at the [University of Saskatchewan][usask]. There are [slides] and a
-[report] available from that project. In 2016, @oli-obk joined to prepare miri
+[report] available from that project. In 2016, @oli-obk joined to prepare Miri
for eventually being used as const evaluator in the Rust compiler itself
(basically, for `const` and `static` stuff), replacing the old evaluator that
worked directly on the AST. In 2017, @RalfJung did an internship with Mozilla
-and began developing miri towards a tool for detecting undefined behavior, and
-also using miri as a way to explore the consequences of various possible
-definitions for undefined behavior in Rust. @oli-obk's move of the miri engine
+and began developing Miri towards a tool for detecting undefined behavior, and
+also using Miri as a way to explore the consequences of various possible
+definitions for undefined behavior in Rust. @oli-obk's move of the Miri engine
into the compiler finally came to completion in early 2018. Meanwhile, later
-that year, @RalfJung did a second internship, developing miri further with
+that year, @RalfJung did a second internship, developing Miri further with
support for checking basic type invariants and verifying that references are
used according to their aliasing restrictions.
* [`crossbeam-epoch` calling `assume_init` on a partly-initialized `MaybeUninit`](https://github.com/crossbeam-rs/crossbeam/pull/779)
* [`integer-encoding` dereferencing a misaligned pointer](https://github.com/dermesser/integer-encoding-rs/pull/23)
* [`rkyv` constructing a `Box<[u8]>` from an overaligned allocation](https://github.com/rkyv/rkyv/commit/a9417193a34757e12e24263178be8b2eebb72456)
+* [Data race in `thread::scope`](https://github.com/rust-lang/rust/issues/98498)
Violations of [Stacked Borrows] found that are likely bugs (but Stacked Borrows is currently just an experiment):
projects / rust.git / blobdiff