miri: add flag to suppress float non-determinism

This commit is contained in:
Ralf Jung 2025-06-11 08:40:46 +02:00
parent 1c047506f9
commit 2a10f12112
8 changed files with 31 additions and 4 deletions

View file

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

View file

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

View file

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

View file

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

View file

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

View file

@ -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> {
@ -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,
}
}
@ -956,6 +960,7 @@ impl VisitProvenance for MiriMachine<'_> {
int2ptr_warned: _,
mangle_internal_symbol_cache: _,
force_intrinsic_fallback: _,
float_nondet: _,
} = self;
threads.visit_provenance(visit);

View file

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

View file

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