Skip to content

miri: add flag to suppress float non-determinism #142337

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Jun 13, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions src/tools/miri/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -286,6 +286,11 @@ environment variable. We first document the most relevant and most commonly used
specific circumstances, but Miri's behavior will also be more stable across versions and targets.
This is equivalent to `-Zmiri-fixed-schedule -Zmiri-compare-exchange-weak-failure-rate=0.0
-Zmiri-address-reuse-cross-thread-rate=0.0 -Zmiri-disable-weak-memory-emulation`.
* `-Zmiri-deterministic-floats` makes Miri's floating-point behavior fully deterministic. This means
that operations will always return the preferred NaN, imprecise operations will not have any
random error applied to them, and `min`/`max` as "maybe fused" multiply-add all behave
deterministically. Note that Miri still uses host floats for some operations, so behavior can
still differ depending on the host target and setup.
* `-Zmiri-disable-isolation` disables host isolation. As a consequence,
the program has access to host resources such as environment variables, file
systems, and randomness.
Expand Down
2 changes: 2 additions & 0 deletions src/tools/miri/src/bin/miri.rs
Original file line number Diff line number Diff line change
Expand Up @@ -601,6 +601,8 @@ fn main() {
miri_config.collect_leak_backtraces = false;
} else if arg == "-Zmiri-force-intrinsic-fallback" {
miri_config.force_intrinsic_fallback = true;
} else if arg == "-Zmiri-deterministic-floats" {
miri_config.float_nondet = false;
} else if arg == "-Zmiri-strict-provenance" {
miri_config.provenance_mode = ProvenanceMode::Strict;
} else if arg == "-Zmiri-permissive-provenance" {
Expand Down
3 changes: 3 additions & 0 deletions src/tools/miri/src/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -166,6 +166,8 @@ pub struct MiriConfig {
pub fixed_scheduling: bool,
/// Always prefer the intrinsic fallback body over the native Miri implementation.
pub force_intrinsic_fallback: bool,
/// Whether floating-point operations can behave non-deterministically.
pub float_nondet: bool,
}

impl Default for MiriConfig {
Expand Down Expand Up @@ -205,6 +207,7 @@ impl Default for MiriConfig {
address_reuse_cross_thread_rate: 0.1,
fixed_scheduling: false,
force_intrinsic_fallback: false,
float_nondet: true,
}
}
}
Expand Down
4 changes: 2 additions & 2 deletions src/tools/miri/src/intrinsics/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -293,7 +293,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
let a = this.read_scalar(a)?.to_f32()?;
let b = this.read_scalar(b)?.to_f32()?;
let c = this.read_scalar(c)?.to_f32()?;
let fuse: bool = this.machine.rng.get_mut().random();
let fuse: bool = this.machine.float_nondet && this.machine.rng.get_mut().random();
let res = if fuse {
// FIXME: Using host floats, to work around https://github.com/rust-lang/rustc_apfloat/issues/11
a.to_host().mul_add(b.to_host(), c.to_host()).to_soft()
Expand All @@ -308,7 +308,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
let a = this.read_scalar(a)?.to_f64()?;
let b = this.read_scalar(b)?.to_f64()?;
let c = this.read_scalar(c)?.to_f64()?;
let fuse: bool = this.machine.rng.get_mut().random();
let fuse: bool = this.machine.float_nondet && this.machine.rng.get_mut().random();
let res = if fuse {
// FIXME: Using host floats, to work around https://github.com/rust-lang/rustc_apfloat/issues/11
a.to_host().mul_add(b.to_host(), c.to_host()).to_soft()
Expand Down
3 changes: 2 additions & 1 deletion src/tools/miri/src/intrinsics/simd.rs
Original file line number Diff line number Diff line change
Expand Up @@ -306,7 +306,8 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
let c = this.read_scalar(&this.project_index(&c, i)?)?;
let dest = this.project_index(&dest, i)?;

let fuse: bool = intrinsic_name == "fma" || this.machine.rng.get_mut().random();
let fuse: bool = intrinsic_name == "fma"
|| (this.machine.float_nondet && this.machine.rng.get_mut().random());

// Works for f32 and f64.
// FIXME: using host floats to work around https://github.com/rust-lang/miri/issues/2468.
Expand Down
5 changes: 5 additions & 0 deletions src/tools/miri/src/machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -618,6 +618,9 @@ pub struct MiriMachine<'tcx> {

/// Always prefer the intrinsic fallback body over the native Miri implementation.
pub force_intrinsic_fallback: bool,

/// Whether floating-point operations can behave non-deterministically.
pub float_nondet: bool,
}

impl<'tcx> MiriMachine<'tcx> {
Expand Down Expand Up @@ -778,6 +781,7 @@ impl<'tcx> MiriMachine<'tcx> {
int2ptr_warned: Default::default(),
mangle_internal_symbol_cache: Default::default(),
force_intrinsic_fallback: config.force_intrinsic_fallback,
float_nondet: config.float_nondet,
}
}

Expand Down Expand Up @@ -956,6 +960,7 @@ impl VisitProvenance for MiriMachine<'_> {
int2ptr_warned: _,
mangle_internal_symbol_cache: _,
force_intrinsic_fallback: _,
float_nondet: _,
} = self;

threads.visit_provenance(visit);
Expand Down
4 changes: 4 additions & 0 deletions src/tools/miri/src/math.rs
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,10 @@ pub(crate) fn apply_random_float_error<F: rustc_apfloat::Float>(
val: F,
err_scale: i32,
) -> F {
if !ecx.machine.float_nondet {
return val;
}

let rng = ecx.machine.rng.get_mut();
// Generate a random integer in the range [0, 2^PREC).
// (When read as binary, the position of the first `1` determines the exponent,
Expand Down
9 changes: 8 additions & 1 deletion src/tools/miri/src/operator.rs
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,11 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
}

fn generate_nan<F1: Float + FloatConvert<F2>, F2: Float>(&self, inputs: &[F1]) -> F2 {
let this = self.eval_context_ref();
if !this.machine.float_nondet {
return F2::NAN;
}

/// Make the given NaN a signaling NaN.
/// Returns `None` if this would not result in a NaN.
fn make_signaling<F: Float>(f: F) -> Option<F> {
Expand All @@ -89,7 +94,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
if f.is_nan() { Some(f) } else { None }
}

let this = self.eval_context_ref();
let mut rand = this.machine.rng.borrow_mut();
// Assemble an iterator of possible NaNs: preferred, quieting propagation, unchanged propagation.
// On some targets there are more possibilities; for now we just generate those options that
Expand Down Expand Up @@ -118,6 +122,9 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {

fn equal_float_min_max<F: Float>(&self, a: F, b: F) -> F {
let this = self.eval_context_ref();
if !this.machine.float_nondet {
return a;
}
// Return one side non-deterministically.
let mut rand = this.machine.rng.borrow_mut();
if rand.random() { a } else { b }
Expand Down
Loading