Merge pull request #4480 from RalfJung/no-extra-rounding-error

add -Zmiri-no-extra-rounding-error to specifically disable just that part of float-nondet

Author: oli-obk

README.md

@@ -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**.

src/bin/miri.rs

@@ -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" {

src/eval.rs

@@ -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,
         }
     }
 }

src/machine.rs

@@ -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);

src/math.rs

@@ -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;
     }