add a flag to always apply the maximum float error

Author: RalfJung

src/tools/miri/README.md

@@ -319,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-max-extra-rounding-error` tells Miri to always apply the maximum error to float operations
+  that do not have a guaranteed precision. The sign of the error is still non-deterministic.
 * `-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

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

@@ -556,7 +556,9 @@ fn main() {
         } 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;
+            miri_config.float_rounding_error = miri::FloatRoundingErrorMode::None;
+        } else if arg == "-Zmiri-max-extra-rounding-error" {
+            miri_config.float_rounding_error = miri::FloatRoundingErrorMode::Max;
         } else if arg == "-Zmiri-strict-provenance" {
             miri_config.provenance_mode = ProvenanceMode::Strict;
         } else if arg == "-Zmiri-permissive-provenance" {

src/tools/miri/src/eval.rs

@@ -112,7 +112,7 @@ pub struct MiriConfig {
     /// 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,
+    pub float_rounding_error: FloatRoundingErrorMode,
 }
 
 impl Default for MiriConfig {
@@ -154,7 +154,7 @@ impl Default for MiriConfig {
             fixed_scheduling: false,
             force_intrinsic_fallback: false,
             float_nondet: true,
-            float_rounding_error: true,
+            float_rounding_error: FloatRoundingErrorMode::Random,
         }
     }
 }

src/tools/miri/src/lib.rs

@@ -142,9 +142,10 @@ pub use crate::eval::{MiriConfig, MiriEntryFnType, create_ecx, eval_entry};
 pub use crate::helpers::{AccessKind, EvalContextExt as _, ToU64 as _, ToUsize as _};
 pub use crate::intrinsics::EvalContextExt as _;
 pub use crate::machine::{
-    AlignmentCheck, AllocExtra, BacktraceStyle, DynMachineCallback, FrameExtra, IsolatedOp,
-    MachineCallback, MemoryKind, MiriInterpCx, MiriInterpCxExt, MiriMachine, MiriMemoryKind,
-    PrimitiveLayouts, Provenance, ProvenanceExtra, RejectOpWith, ValidationMode,
+    AlignmentCheck, AllocExtra, BacktraceStyle, DynMachineCallback, FloatRoundingErrorMode,
+    FrameExtra, IsolatedOp, MachineCallback, MemoryKind, MiriInterpCx, MiriInterpCxExt,
+    MiriMachine, MiriMemoryKind, PrimitiveLayouts, Provenance, ProvenanceExtra, RejectOpWith,
+    ValidationMode,
 };
 pub use crate::operator::EvalContextExt as _;
 pub use crate::provenance_gc::{EvalContextExt as _, LiveAllocs, VisitProvenance, VisitWith};

src/tools/miri/src/machine.rs

@@ -108,6 +108,16 @@ pub enum ValidationMode {
     Deep,
 }
 
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub enum FloatRoundingErrorMode {
+    /// Apply a random error (the default).
+    Random,
+    /// Don't apply any error.
+    None,
+    /// Always apply the maximum error (with a random sign).
+    Max,
+}
+
 /// Extra data stored with each stack frame
 pub struct FrameExtra<'tcx> {
     /// Extra data for the Borrow Tracker.
@@ -658,7 +668,7 @@ 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,
+    pub float_rounding_error: FloatRoundingErrorMode,
 }
 
 impl<'tcx> MiriMachine<'tcx> {

src/tools/miri/src/math.rs

@@ -15,7 +15,9 @@ pub(crate) fn apply_random_float_error<F: rustc_apfloat::Float>(
     val: F,
     err_scale: i32,
 ) -> F {
-    if !ecx.machine.float_nondet || !ecx.machine.float_rounding_error {
+    if !ecx.machine.float_nondet
+        || matches!(ecx.machine.float_rounding_error, FloatRoundingErrorMode::None)
+    {
         return val;
     }
 
@@ -24,7 +26,12 @@ pub(crate) fn apply_random_float_error<F: rustc_apfloat::Float>(
     // (When read as binary, the position of the first `1` determines the exponent,
     // and the remaining bits fill the mantissa. `PREC` is one plus the size of the mantissa,
     // so this all works out.)
-    let r = F::from_u128(rng.random_range(0..(1 << F::PRECISION))).value;
+    let r = F::from_u128(match ecx.machine.float_rounding_error {
+        FloatRoundingErrorMode::Random => rng.random_range(0..(1 << F::PRECISION)),
+        FloatRoundingErrorMode::Max => (1 << F::PRECISION) - 1, // force max error
+        FloatRoundingErrorMode::None => unreachable!(),
+    })
+    .value;
     // Multiply this with 2^(scale - PREC). The result is between 0 and
     // 2^PREC * 2^(scale - PREC) = 2^scale.
     let err = r.scalbn(err_scale.strict_sub(F::PRECISION.try_into().unwrap()));

src/tools/miri/tests/pass/float_extra_rounding_error.rs

@@ -0,0 +1,23 @@
+//! Check that the flags to control the extra rounding error work.
+//@revisions: random max none
+//@[max]compile-flags: -Zmiri-max-extra-rounding-error
+//@[none]compile-flags: -Zmiri-no-extra-rounding-error
+#![feature(cfg_select)]
+
+use std::collections::HashSet;
+use std::hint::black_box;
+
+fn main() {
+    let expected = cfg_select! {
+        random => 13, // FIXME: why is it 13?
+        max => 2,
+        none => 1,
+    };
+    // Call `sin(0.5)` a bunch of times and see how many different values we get.
+    let mut values = HashSet::new();
+    for _ in 0..(expected * 16) {
+        let val = black_box(0.5f64).sin();
+        values.insert(val.to_bits());
+    }
+    assert_eq!(values.len(), expected);
+}