add -Zmiri-no-extra-rounding-error to specifically disable just that part of float-nondet
This commit is contained in:
parent
eef454f89b
commit
4aa4376008
5 changed files with 18 additions and 6 deletions
|
|
@ -286,11 +286,6 @@ environment variable. We first document the most relevant and most commonly used
|
|||
specific circumstances, but Miri's behavior will also be more stable across versions and targets.
|
||||
This is equivalent to `-Zmiri-fixed-schedule -Zmiri-compare-exchange-weak-failure-rate=0.0
|
||||
-Zmiri-address-reuse-cross-thread-rate=0.0 -Zmiri-disable-weak-memory-emulation`.
|
||||
* `-Zmiri-deterministic-floats` makes Miri's floating-point behavior fully deterministic. This means
|
||||
that operations will always return the preferred NaN, imprecise operations will not have any
|
||||
random error applied to them, and `min`/`max` as "maybe fused" multiply-add all behave
|
||||
deterministically. Note that Miri still uses host floats for some operations, so behavior can
|
||||
still differ depending on the host target and setup.
|
||||
* `-Zmiri-disable-isolation` disables host isolation. As a consequence,
|
||||
the program has access to host resources such as environment variables, file
|
||||
systems, and randomness.
|
||||
|
|
@ -324,6 +319,8 @@ environment variable. We first document the most relevant and most commonly used
|
|||
Can be used without a value; in that case the range defaults to `0..64`.
|
||||
* `-Zmiri-many-seeds-keep-going` tells Miri to really try all the seeds in the given range, even if
|
||||
a failing seed has already been found. This is useful to determine which fraction of seeds fails.
|
||||
* `-Zmiri-no-extra-rounding-error` stops Miri from adding extra rounding errors to float operations
|
||||
that do not have a guaranteed precision.
|
||||
* `-Zmiri-num-cpus` states the number of available CPUs to be reported by miri. By default, the
|
||||
number of available CPUs is `1`. Note that this flag does not affect how miri handles threads in
|
||||
any way.
|
||||
|
|
@ -376,6 +373,12 @@ to Miri failing to detect cases of undefined behavior in a program.
|
|||
will always fail and `0.0` means it will never fail. Note that setting it to
|
||||
`1.0` will likely cause hangs, since it means programs using
|
||||
`compare_exchange_weak` cannot make progress.
|
||||
* `-Zmiri-deterministic-floats` makes Miri's floating-point behavior fully deterministic. This means
|
||||
that operations will always return the preferred NaN, imprecise operations will not have any
|
||||
random error applied to them, and `min`/`max` and "maybe fused" multiply-add all behave
|
||||
deterministically. Note that Miri still uses host floats for some operations, so behavior can
|
||||
still differ depending on the host target and setup. See `-Zmiri-no-extra-rounding-error` for
|
||||
a flag that specifically only disables the random error.
|
||||
* `-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**.
|
||||
|
|
|
|||
|
|
@ -562,6 +562,8 @@ fn main() {
|
|||
miri_config.force_intrinsic_fallback = true;
|
||||
} else if arg == "-Zmiri-deterministic-floats" {
|
||||
miri_config.float_nondet = false;
|
||||
} else if arg == "-Zmiri-no-extra-rounding-error" {
|
||||
miri_config.float_rounding_error = false;
|
||||
} else if arg == "-Zmiri-strict-provenance" {
|
||||
miri_config.provenance_mode = ProvenanceMode::Strict;
|
||||
} else if arg == "-Zmiri-permissive-provenance" {
|
||||
|
|
|
|||
|
|
@ -170,6 +170,8 @@ pub struct MiriConfig {
|
|||
pub force_intrinsic_fallback: bool,
|
||||
/// Whether floating-point operations can behave non-deterministically.
|
||||
pub float_nondet: bool,
|
||||
/// Whether floating-point operations can have a non-deterministic rounding error.
|
||||
pub float_rounding_error: bool,
|
||||
}
|
||||
|
||||
impl Default for MiriConfig {
|
||||
|
|
@ -211,6 +213,7 @@ impl Default for MiriConfig {
|
|||
fixed_scheduling: false,
|
||||
force_intrinsic_fallback: false,
|
||||
float_nondet: true,
|
||||
float_rounding_error: true,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -617,6 +617,8 @@ pub struct MiriMachine<'tcx> {
|
|||
|
||||
/// Whether floating-point operations can behave non-deterministically.
|
||||
pub float_nondet: bool,
|
||||
/// Whether floating-point operations can have a non-deterministic rounding error.
|
||||
pub float_rounding_error: bool,
|
||||
}
|
||||
|
||||
impl<'tcx> MiriMachine<'tcx> {
|
||||
|
|
@ -775,6 +777,7 @@ impl<'tcx> MiriMachine<'tcx> {
|
|||
mangle_internal_symbol_cache: Default::default(),
|
||||
force_intrinsic_fallback: config.force_intrinsic_fallback,
|
||||
float_nondet: config.float_nondet,
|
||||
float_rounding_error: config.float_rounding_error,
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -951,6 +954,7 @@ impl VisitProvenance for MiriMachine<'_> {
|
|||
mangle_internal_symbol_cache: _,
|
||||
force_intrinsic_fallback: _,
|
||||
float_nondet: _,
|
||||
float_rounding_error: _,
|
||||
} = self;
|
||||
|
||||
threads.visit_provenance(visit);
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ pub(crate) fn apply_random_float_error<F: rustc_apfloat::Float>(
|
|||
val: F,
|
||||
err_scale: i32,
|
||||
) -> F {
|
||||
if !ecx.machine.float_nondet {
|
||||
if !ecx.machine.float_nondet || !ecx.machine.float_rounding_error {
|
||||
return val;
|
||||
}
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue