miri: add flag to suppress float non-determinism

Author: RalfJung

src/tools/miri/README.md

@@ -286,6 +286,11 @@ 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.

src/tools/miri/src/bin/miri.rs

@@ -601,6 +601,8 @@ fn main() {
             miri_config.collect_leak_backtraces = false;
         } else if arg == "-Zmiri-force-intrinsic-fallback" {
             miri_config.force_intrinsic_fallback = true;
+        } else if arg == "-Zmiri-deterministic-floats" {
+            miri_config.float_nondet = false;
         } else if arg == "-Zmiri-strict-provenance" {
             miri_config.provenance_mode = ProvenanceMode::Strict;
         } else if arg == "-Zmiri-permissive-provenance" {

src/tools/miri/src/eval.rs

@@ -166,6 +166,8 @@ pub struct MiriConfig {
     pub fixed_scheduling: bool,
     /// Always prefer the intrinsic fallback body over the native Miri implementation.
     pub force_intrinsic_fallback: bool,
+    /// Whether floating-point operations can behave non-deterministically.
+    pub float_nondet: bool,
 }
 
 impl Default for MiriConfig {
@@ -205,6 +207,7 @@ impl Default for MiriConfig {
             address_reuse_cross_thread_rate: 0.1,
             fixed_scheduling: false,
             force_intrinsic_fallback: false,
+            float_nondet: true,
         }
     }
 }

src/tools/miri/src/intrinsics/mod.rs

@@ -293,7 +293,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
                 let a = this.read_scalar(a)?.to_f32()?;
                 let b = this.read_scalar(b)?.to_f32()?;
                 let c = this.read_scalar(c)?.to_f32()?;
-                let fuse: bool = this.machine.rng.get_mut().random();
+                let fuse: bool = this.machine.float_nondet && this.machine.rng.get_mut().random();
                 let res = if fuse {
                     // FIXME: Using host floats, to work around https://github.com/rust-lang/rustc_apfloat/issues/11
                     a.to_host().mul_add(b.to_host(), c.to_host()).to_soft()
@@ -308,7 +308,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
                 let a = this.read_scalar(a)?.to_f64()?;
                 let b = this.read_scalar(b)?.to_f64()?;
                 let c = this.read_scalar(c)?.to_f64()?;
-                let fuse: bool = this.machine.rng.get_mut().random();
+                let fuse: bool = this.machine.float_nondet && this.machine.rng.get_mut().random();
                 let res = if fuse {
                     // FIXME: Using host floats, to work around https://github.com/rust-lang/rustc_apfloat/issues/11
                     a.to_host().mul_add(b.to_host(), c.to_host()).to_soft()

src/tools/miri/src/intrinsics/simd.rs

@@ -306,7 +306,8 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
                     let c = this.read_scalar(&this.project_index(&c, i)?)?;
                     let dest = this.project_index(&dest, i)?;
 
-                    let fuse: bool = intrinsic_name == "fma" || this.machine.rng.get_mut().random();
+                    let fuse: bool = intrinsic_name == "fma"
+                        || (this.machine.float_nondet && this.machine.rng.get_mut().random());
 
                     // Works for f32 and f64.
                     // FIXME: using host floats to work around https://github.com/rust-lang/miri/issues/2468.

src/tools/miri/src/machine.rs

@@ -618,6 +618,9 @@ pub struct MiriMachine<'tcx> {
 
     /// Always prefer the intrinsic fallback body over the native Miri implementation.
     pub force_intrinsic_fallback: bool,
+
+    /// Whether floating-point operations can behave non-deterministically.
+    pub float_nondet: bool,
 }
 
 impl<'tcx> MiriMachine<'tcx> {
@@ -778,6 +781,7 @@ impl<'tcx> MiriMachine<'tcx> {
             int2ptr_warned: Default::default(),
             mangle_internal_symbol_cache: Default::default(),
             force_intrinsic_fallback: config.force_intrinsic_fallback,
+            float_nondet: config.float_nondet,
         }
     }
 
@@ -956,6 +960,7 @@ impl VisitProvenance for MiriMachine<'_> {
             int2ptr_warned: _,
             mangle_internal_symbol_cache: _,
             force_intrinsic_fallback: _,
+            float_nondet: _,
         } = self;
 
         threads.visit_provenance(visit);

src/tools/miri/src/math.rs

@@ -15,6 +15,10 @@ pub(crate) fn apply_random_float_error<F: rustc_apfloat::Float>(
     val: F,
     err_scale: i32,
 ) -> F {
+    if !ecx.machine.float_nondet {
+        return val;
+    }
+
     let rng = ecx.machine.rng.get_mut();
     // Generate a random integer in the range [0, 2^PREC).
     // (When read as binary, the position of the first `1` determines the exponent,

src/tools/miri/src/operator.rs

@@ -76,6 +76,11 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
     }
 
     fn generate_nan<F1: Float + FloatConvert<F2>, F2: Float>(&self, inputs: &[F1]) -> F2 {
+        let this = self.eval_context_ref();
+        if !this.machine.float_nondet {
+            return F2::NAN;
+        }
+
         /// Make the given NaN a signaling NaN.
         /// Returns `None` if this would not result in a NaN.
         fn make_signaling<F: Float>(f: F) -> Option<F> {
@@ -89,7 +94,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
             if f.is_nan() { Some(f) } else { None }
         }
 
-        let this = self.eval_context_ref();
         let mut rand = this.machine.rng.borrow_mut();
         // Assemble an iterator of possible NaNs: preferred, quieting propagation, unchanged propagation.
         // On some targets there are more possibilities; for now we just generate those options that
@@ -118,6 +122,9 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
 
     fn equal_float_min_max<F: Float>(&self, a: F, b: F) -> F {
         let this = self.eval_context_ref();
+        if !this.machine.float_nondet {
+            return a;
+        }
         // Return one side non-deterministically.
         let mut rand = this.machine.rng.borrow_mut();
         if rand.random() { a } else { b }