mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

readme: move some things around

Browse Source
This commit is contained in:
Ralf Jung 2022-06-26 22:07:02 -04:00
parent 5c16713056
commit 4120425108
1 changed files with 15 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
README.md
View File

@ -289,6 +289,11 @@ environment variable. We first document the most relevant and most commonly used
`-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.
@ -307,6 +312,16 @@ environment variable. We first document the most relevant and most commonly used
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
@ -354,23 +369,6 @@ to Miri failing to detect cases of undefined behavior in a program.
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-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-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-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