diff --git a/src/tools/miri/README.md b/src/tools/miri/README.md index 7ccd27d7b83e..cb4a56b58ac8 100644 --- a/src/tools/miri/README.md +++ b/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 diff --git a/src/tools/miri/src/bin/miri.rs b/src/tools/miri/src/bin/miri.rs index ae1b25f8857a..8fd8d332978d 100644 --- a/src/tools/miri/src/bin/miri.rs +++ b/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" { diff --git a/src/tools/miri/src/eval.rs b/src/tools/miri/src/eval.rs index 43d251b157ba..f174a448a810 100644 --- a/src/tools/miri/src/eval.rs +++ b/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, } } } diff --git a/src/tools/miri/src/lib.rs b/src/tools/miri/src/lib.rs index 090f10f48133..0856411b8e83 100644 --- a/src/tools/miri/src/lib.rs +++ b/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}; diff --git a/src/tools/miri/src/machine.rs b/src/tools/miri/src/machine.rs index e27b2e89b48a..7802a58f1123 100644 --- a/src/tools/miri/src/machine.rs +++ b/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> { diff --git a/src/tools/miri/src/math.rs b/src/tools/miri/src/math.rs index e9e5a1070c9e..dd994b03f5d1 100644 --- a/src/tools/miri/src/math.rs +++ b/src/tools/miri/src/math.rs @@ -15,7 +15,9 @@ pub(crate) fn apply_random_float_error( 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( // (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())); diff --git a/src/tools/miri/tests/pass/float_extra_rounding_error.rs b/src/tools/miri/tests/pass/float_extra_rounding_error.rs new file mode 100644 index 000000000000..73512399f82c --- /dev/null +++ b/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); +}