show an error on some invalid flag combinations: TB + permissive provenance; strict provenance + native calls
This commit is contained in:
parent
cb73bb6538
commit
2de456151a
4 changed files with 21 additions and 17 deletions
|
@ -347,8 +347,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 +437,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
|
||||
|
|
|
@ -539,6 +539,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" {
|
||||
|
@ -728,13 +729,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() {
|
||||
|
|
|
@ -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 {
|
||||
|
|
|
@ -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;
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue