add a flag to always apply the maximum float error

This commit is contained in:
Ralf Jung 2025-09-02 15:02:35 +02:00
parent 821a44d3ef
commit a354649102
7 changed files with 54 additions and 9 deletions

View file

@ -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

View file

@ -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" {

View file

@ -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,
}
}
}

View file

@ -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};

View file

@ -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> {

View file

@ -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()));

View file

@ -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);
}