From 821a44d3efb677e65b392e627f2d6647841db77e Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 1 Sep 2025 09:02:43 +0200 Subject: [PATCH 1/3] move some configuration enums to a more logical place --- src/tools/miri/src/eval.rs | 59 ----------------------------------- src/tools/miri/src/lib.rs | 10 +++--- src/tools/miri/src/machine.rs | 59 +++++++++++++++++++++++++++++++++++ 3 files changed, 63 insertions(+), 65 deletions(-) diff --git a/src/tools/miri/src/eval.rs b/src/tools/miri/src/eval.rs index 4c531a8d1f52..43d251b157ba 100644 --- a/src/tools/miri/src/eval.rs +++ b/src/tools/miri/src/eval.rs @@ -32,65 +32,6 @@ pub enum MiriEntryFnType { /// will hang the program. const MAIN_THREAD_YIELDS_AT_SHUTDOWN: u32 = 256; -#[derive(Copy, Clone, Debug, PartialEq)] -pub enum AlignmentCheck { - /// Do not check alignment. - None, - /// Check alignment "symbolically", i.e., using only the requested alignment for an allocation and not its real base address. - Symbolic, - /// Check alignment on the actual physical integer address. - Int, -} - -#[derive(Copy, Clone, Debug, PartialEq)] -pub enum RejectOpWith { - /// Isolated op is rejected with an abort of the machine. - Abort, - - /// If not Abort, miri returns an error for an isolated op. - /// Following options determine if user should be warned about such error. - /// Do not print warning about rejected isolated op. - NoWarning, - - /// Print a warning about rejected isolated op, with backtrace. - Warning, - - /// Print a warning about rejected isolated op, without backtrace. - WarningWithoutBacktrace, -} - -#[derive(Copy, Clone, Debug, PartialEq)] -pub enum IsolatedOp { - /// Reject an op requiring communication with the host. By - /// default, miri rejects the op with an abort. If not, it returns - /// an error code, and prints a warning about it. Warning levels - /// are controlled by `RejectOpWith` enum. - Reject(RejectOpWith), - - /// Execute op requiring communication with the host, i.e. disable isolation. - Allow, -} - -#[derive(Debug, Copy, Clone, PartialEq, Eq)] -pub enum BacktraceStyle { - /// Prints a terser backtrace which ideally only contains relevant information. - Short, - /// Prints a backtrace with all possible information. - Full, - /// Prints only the frame that the error occurs in. - Off, -} - -#[derive(Debug, Copy, Clone, PartialEq, Eq)] -pub enum ValidationMode { - /// Do not perform any kind of validation. - No, - /// Validate the interior of the value, but not things behind references. - Shallow, - /// Fully recursively validate references. - Deep, -} - /// Configuration needed to spawn a Miri instance. #[derive(Clone)] pub struct MiriConfig { diff --git a/src/tools/miri/src/lib.rs b/src/tools/miri/src/lib.rs index 5ed6d6b346c7..090f10f48133 100644 --- a/src/tools/miri/src/lib.rs +++ b/src/tools/miri/src/lib.rs @@ -138,15 +138,13 @@ pub use crate::data_structures::mono_hash_map::MonoHashMap; pub use crate::diagnostics::{ EvalContextExt as _, NonHaltingDiagnostic, TerminationInfo, report_error, }; -pub use crate::eval::{ - AlignmentCheck, BacktraceStyle, IsolatedOp, MiriConfig, MiriEntryFnType, RejectOpWith, - ValidationMode, create_ecx, eval_entry, -}; +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::{ - AllocExtra, DynMachineCallback, FrameExtra, MachineCallback, MemoryKind, MiriInterpCx, - MiriInterpCxExt, MiriMachine, MiriMemoryKind, PrimitiveLayouts, Provenance, ProvenanceExtra, + AlignmentCheck, AllocExtra, BacktraceStyle, DynMachineCallback, 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 0136de552163..e27b2e89b48a 100644 --- a/src/tools/miri/src/machine.rs +++ b/src/tools/miri/src/machine.rs @@ -49,6 +49,65 @@ pub const SIGRTMAX: i32 = 42; /// base address for each evaluation would produce unbounded memory usage. const ADDRS_PER_ANON_GLOBAL: usize = 32; +#[derive(Copy, Clone, Debug, PartialEq)] +pub enum AlignmentCheck { + /// Do not check alignment. + None, + /// Check alignment "symbolically", i.e., using only the requested alignment for an allocation and not its real base address. + Symbolic, + /// Check alignment on the actual physical integer address. + Int, +} + +#[derive(Copy, Clone, Debug, PartialEq)] +pub enum RejectOpWith { + /// Isolated op is rejected with an abort of the machine. + Abort, + + /// If not Abort, miri returns an error for an isolated op. + /// Following options determine if user should be warned about such error. + /// Do not print warning about rejected isolated op. + NoWarning, + + /// Print a warning about rejected isolated op, with backtrace. + Warning, + + /// Print a warning about rejected isolated op, without backtrace. + WarningWithoutBacktrace, +} + +#[derive(Copy, Clone, Debug, PartialEq)] +pub enum IsolatedOp { + /// Reject an op requiring communication with the host. By + /// default, miri rejects the op with an abort. If not, it returns + /// an error code, and prints a warning about it. Warning levels + /// are controlled by `RejectOpWith` enum. + Reject(RejectOpWith), + + /// Execute op requiring communication with the host, i.e. disable isolation. + Allow, +} + +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum BacktraceStyle { + /// Prints a terser backtrace which ideally only contains relevant information. + Short, + /// Prints a backtrace with all possible information. + Full, + /// Prints only the frame that the error occurs in. + Off, +} + +#[derive(Debug, Copy, Clone, PartialEq, Eq)] +pub enum ValidationMode { + /// Do not perform any kind of validation. + No, + /// Validate the interior of the value, but not things behind references. + Shallow, + /// Fully recursively validate references. + Deep, +} + /// Extra data stored with each stack frame pub struct FrameExtra<'tcx> { /// Extra data for the Borrow Tracker. From a3546491021831e17c030c7f8ec82f4715b321de Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 2 Sep 2025 15:02:35 +0200 Subject: [PATCH 2/3] add a flag to always apply the maximum float error --- src/tools/miri/README.md | 2 ++ src/tools/miri/src/bin/miri.rs | 4 +++- src/tools/miri/src/eval.rs | 4 ++-- src/tools/miri/src/lib.rs | 7 +++--- src/tools/miri/src/machine.rs | 12 +++++++++- src/tools/miri/src/math.rs | 11 +++++++-- .../tests/pass/float_extra_rounding_error.rs | 23 +++++++++++++++++++ 7 files changed, 54 insertions(+), 9 deletions(-) create mode 100644 src/tools/miri/tests/pass/float_extra_rounding_error.rs 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); +} From d4f861ecb6319e1db20d20e3cc5ddab84b4aaade Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 2 Sep 2025 16:33:10 +0200 Subject: [PATCH 3/3] account for aarch64 windows oversleeping --- src/tools/miri/tests/pass/concurrency/sync.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tools/miri/tests/pass/concurrency/sync.rs b/src/tools/miri/tests/pass/concurrency/sync.rs index a92359758dad..142ac9cc8ca4 100644 --- a/src/tools/miri/tests/pass/concurrency/sync.rs +++ b/src/tools/miri/tests/pass/concurrency/sync.rs @@ -9,7 +9,8 @@ use std::time::{Duration, Instant}; // We are expecting to sleep for 10ms. How long of a sleep we are accepting? // Even with 1000ms we still see this test fail on macOS runners. -const MAX_SLEEP_TIME_MS: u64 = 2000; +// On a aarch64-pc-windows-msvc runner, we saw 2.7s! +const MAX_SLEEP_TIME_MS: u64 = 4000; // Check if Rust barriers are working.