diff options
| -rw-r--r-- | src/tools/miri/README.md | 2 | ||||
| -rw-r--r-- | src/tools/miri/src/bin/miri.rs | 4 | ||||
| -rw-r--r-- | src/tools/miri/src/eval.rs | 63 | ||||
| -rw-r--r-- | src/tools/miri/src/lib.rs | 11 | ||||
| -rw-r--r-- | src/tools/miri/src/machine.rs | 71 | ||||
| -rw-r--r-- | src/tools/miri/src/math.rs | 11 | ||||
| -rw-r--r-- | src/tools/miri/tests/pass/concurrency/sync.rs | 3 | ||||
| -rw-r--r-- | src/tools/miri/tests/pass/float_extra_rounding_error.rs | 23 |
8 files changed, 116 insertions, 72 deletions
diff --git a/src/tools/miri/README.md b/src/tools/miri/README.md index 7ccd27d7b83..cb4a56b58ac 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 ae1b25f8857..8fd8d332978 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 4c531a8d1f5..f174a448a81 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 { @@ -171,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 { @@ -213,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 5ed6d6b346c..0856411b8e8 100644 --- a/src/tools/miri/src/lib.rs +++ b/src/tools/miri/src/lib.rs @@ -138,15 +138,14 @@ 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, 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 0136de55216..7802a58f112 100644 --- a/src/tools/miri/src/machine.rs +++ b/src/tools/miri/src/machine.rs @@ -49,6 +49,75 @@ 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, +} + +#[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. @@ -599,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 e9e5a1070c9..dd994b03f5d 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<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())); diff --git a/src/tools/miri/tests/pass/concurrency/sync.rs b/src/tools/miri/tests/pass/concurrency/sync.rs index a92359758da..142ac9cc8ca 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. 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 00000000000..73512399f82 --- /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); +} |