Skip to content

miri: algebraic intrinsics: bring back float non-determinism #140439

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
Apr 30, 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
3 changes: 1 addition & 2 deletions compiler/rustc_const_eval/src/interpret/intrinsics.rs
Original file line number Diff line number Diff line change
Expand Up @@ -178,8 +178,7 @@ impl<'tcx, M: Machine<'tcx>> InterpCx<'tcx, M> {

let res = self.binary_op(op, &a, &b)?;
// `binary_op` already called `generate_nan` if needed.

// FIXME: Miri should add some non-determinism to the result here to catch any dependences on exact computations. This has previously been done, but the behaviour was removed as part of constification.
let res = M::apply_float_nondet(self, res)?;
self.write_immediate(*res, dest)?;
}

Expand Down
8 changes: 8 additions & 0 deletions compiler/rustc_const_eval/src/interpret/machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -276,6 +276,14 @@ pub trait Machine<'tcx>: Sized {
F2::NAN
}

/// Apply non-determinism to float operations that do not return a precise result.
fn apply_float_nondet(
_ecx: &mut InterpCx<'tcx, Self>,
val: ImmTy<'tcx, Self::Provenance>,
) -> InterpResult<'tcx, ImmTy<'tcx, Self::Provenance>> {
interp_ok(val)
}

/// Determines the result of `min`/`max` on floats when the arguments are equal.
fn equal_float_min_max<F: Float>(_ecx: &InterpCx<'tcx, Self>, a: F, _b: F) -> F {
// By default, we pick the left argument.
Expand Down
27 changes: 2 additions & 25 deletions src/tools/miri/src/intrinsics/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,13 @@ use rand::Rng;
use rustc_abi::Size;
use rustc_apfloat::{Float, Round};
use rustc_middle::mir;
use rustc_middle::ty::{self, FloatTy, ScalarInt};
use rustc_middle::ty::{self, FloatTy};
use rustc_span::{Symbol, sym};

use self::atomic::EvalContextExt as _;
use self::helpers::{ToHost, ToSoft, check_intrinsic_arg_count};
use self::simd::EvalContextExt as _;
use crate::math::apply_random_float_error_ulp;
use crate::math::apply_random_float_error_to_imm;
use crate::*;

impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
Expand Down Expand Up @@ -473,26 +473,3 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
interp_ok(EmulateItemResult::NeedsReturn)
}
}

/// Applies a random 16ULP floating point error to `val` and returns the new value.
/// Will fail if `val` is not a floating point number.
fn apply_random_float_error_to_imm<'tcx>(
ecx: &mut MiriInterpCx<'tcx>,
val: ImmTy<'tcx>,
ulp_exponent: u32,
) -> InterpResult<'tcx, ImmTy<'tcx>> {
let scalar = val.to_scalar_int()?;
let res: ScalarInt = match val.layout.ty.kind() {
ty::Float(FloatTy::F16) =>
apply_random_float_error_ulp(ecx, scalar.to_f16(), ulp_exponent).into(),
ty::Float(FloatTy::F32) =>
apply_random_float_error_ulp(ecx, scalar.to_f32(), ulp_exponent).into(),
ty::Float(FloatTy::F64) =>
apply_random_float_error_ulp(ecx, scalar.to_f64(), ulp_exponent).into(),
ty::Float(FloatTy::F128) =>
apply_random_float_error_ulp(ecx, scalar.to_f128(), ulp_exponent).into(),
_ => bug!("intrinsic called with non-float input type"),
};

interp_ok(ImmTy::from_scalar_int(res, val.layout))
}
10 changes: 10 additions & 0 deletions src/tools/miri/src/machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1199,6 +1199,16 @@ impl<'tcx> Machine<'tcx> for MiriMachine<'tcx> {
ecx.generate_nan(inputs)
}

#[inline(always)]
fn apply_float_nondet(
ecx: &mut InterpCx<'tcx, Self>,
val: ImmTy<'tcx>,
) -> InterpResult<'tcx, ImmTy<'tcx>> {
crate::math::apply_random_float_error_to_imm(
ecx, val, 2 /* log2(4) */
)
}

#[inline(always)]
fn equal_float_min_max<F: Float>(ecx: &MiriInterpCx<'tcx>, a: F, b: F) -> F {
ecx.equal_float_min_max(a, b)
Expand Down
26 changes: 26 additions & 0 deletions src/tools/miri/src/math.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
use rand::Rng as _;
use rustc_apfloat::Float as _;
use rustc_apfloat::ieee::IeeeFloat;
use rustc_middle::ty::{self, FloatTy, ScalarInt};

use crate::*;

/// Disturbes a floating-point result by a relative error in the range (-2^scale, 2^scale).
///
Expand Down Expand Up @@ -43,6 +46,29 @@ pub(crate) fn apply_random_float_error_ulp<F: rustc_apfloat::Float>(
apply_random_float_error(ecx, val, err_scale)
}

/// Applies a random 16ULP floating point error to `val` and returns the new value.
/// Will fail if `val` is not a floating point number.
pub(crate) fn apply_random_float_error_to_imm<'tcx>(
ecx: &mut MiriInterpCx<'tcx>,
val: ImmTy<'tcx>,
ulp_exponent: u32,
) -> InterpResult<'tcx, ImmTy<'tcx>> {
let scalar = val.to_scalar_int()?;
let res: ScalarInt = match val.layout.ty.kind() {
ty::Float(FloatTy::F16) =>
apply_random_float_error_ulp(ecx, scalar.to_f16(), ulp_exponent).into(),
ty::Float(FloatTy::F32) =>
apply_random_float_error_ulp(ecx, scalar.to_f32(), ulp_exponent).into(),
ty::Float(FloatTy::F64) =>
apply_random_float_error_ulp(ecx, scalar.to_f64(), ulp_exponent).into(),
ty::Float(FloatTy::F128) =>
apply_random_float_error_ulp(ecx, scalar.to_f128(), ulp_exponent).into(),
_ => bug!("intrinsic called with non-float input type"),
};

interp_ok(ImmTy::from_scalar_int(res, val.layout))
}

pub(crate) fn sqrt<S: rustc_apfloat::ieee::Semantics>(x: IeeeFloat<S>) -> IeeeFloat<S> {
match x.category() {
// preserve zero sign
Expand Down
119 changes: 60 additions & 59 deletions src/tools/miri/tests/pass/float.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1292,8 +1292,7 @@ fn test_non_determinism() {
}
}
// We saw the same thing N times.
// FIXME: temporarily disabled as it breaks std tests.
//panic!("expected non-determinism, got {rounds} times the same result: {first:?}");
panic!("expected non-determinism, got {rounds} times the same result: {first:?}");
}

macro_rules! test_operations_f {
Expand All @@ -1319,66 +1318,68 @@ fn test_non_determinism() {
}
pub fn test_operations_f32(a: f32, b: f32) {
test_operations_f!(a, b);
ensure_nondet(|| a.log(b));
ensure_nondet(|| a.exp());
ensure_nondet(|| 10f32.exp2());
ensure_nondet(|| f32::consts::E.ln());
ensure_nondet(|| 1f32.ln_1p());
ensure_nondet(|| 10f32.log10());
ensure_nondet(|| 8f32.log2());
ensure_nondet(|| 27.0f32.cbrt());
ensure_nondet(|| 3.0f32.hypot(4.0f32));
ensure_nondet(|| 1f32.sin());
ensure_nondet(|| 0f32.cos());
// On i686-pc-windows-msvc , these functions are implemented by calling the `f64` version,
// which means the little rounding errors Miri introduces are discard by the cast down to `f32`.
// Just skip the test for them.
if !cfg!(all(target_os = "windows", target_env = "msvc", target_arch = "x86")) {
ensure_nondet(|| 1.0f32.tan());
ensure_nondet(|| 1.0f32.asin());
ensure_nondet(|| 5.0f32.acos());
ensure_nondet(|| 1.0f32.atan());
ensure_nondet(|| 1.0f32.atan2(2.0f32));
ensure_nondet(|| 1.0f32.sinh());
ensure_nondet(|| 1.0f32.cosh());
ensure_nondet(|| 1.0f32.tanh());
}
ensure_nondet(|| 1.0f32.asinh());
ensure_nondet(|| 2.0f32.acosh());
ensure_nondet(|| 0.5f32.atanh());
ensure_nondet(|| 5.0f32.gamma());
ensure_nondet(|| 5.0f32.ln_gamma());
ensure_nondet(|| 5.0f32.erf());
ensure_nondet(|| 5.0f32.erfc());
// FIXME: temporarily disabled as it breaks std tests.
// ensure_nondet(|| a.log(b));
// ensure_nondet(|| a.exp());
// ensure_nondet(|| 10f32.exp2());
// ensure_nondet(|| f32::consts::E.ln());
// ensure_nondet(|| 1f32.ln_1p());
// ensure_nondet(|| 10f32.log10());
// ensure_nondet(|| 8f32.log2());
// ensure_nondet(|| 27.0f32.cbrt());
// ensure_nondet(|| 3.0f32.hypot(4.0f32));
// ensure_nondet(|| 1f32.sin());
// ensure_nondet(|| 0f32.cos());
// // On i686-pc-windows-msvc , these functions are implemented by calling the `f64` version,
// // which means the little rounding errors Miri introduces are discard by the cast down to `f32`.
// // Just skip the test for them.
// if !cfg!(all(target_os = "windows", target_env = "msvc", target_arch = "x86")) {
// ensure_nondet(|| 1.0f32.tan());
// ensure_nondet(|| 1.0f32.asin());
// ensure_nondet(|| 5.0f32.acos());
// ensure_nondet(|| 1.0f32.atan());
// ensure_nondet(|| 1.0f32.atan2(2.0f32));
// ensure_nondet(|| 1.0f32.sinh());
// ensure_nondet(|| 1.0f32.cosh());
// ensure_nondet(|| 1.0f32.tanh());
// }
// ensure_nondet(|| 1.0f32.asinh());
// ensure_nondet(|| 2.0f32.acosh());
// ensure_nondet(|| 0.5f32.atanh());
// ensure_nondet(|| 5.0f32.gamma());
// ensure_nondet(|| 5.0f32.ln_gamma());
// ensure_nondet(|| 5.0f32.erf());
// ensure_nondet(|| 5.0f32.erfc());
}
pub fn test_operations_f64(a: f64, b: f64) {
test_operations_f!(a, b);
ensure_nondet(|| a.log(b));
ensure_nondet(|| a.exp());
ensure_nondet(|| 50f64.exp2());
ensure_nondet(|| 3f64.ln());
ensure_nondet(|| 1f64.ln_1p());
ensure_nondet(|| f64::consts::E.log10());
ensure_nondet(|| f64::consts::E.log2());
ensure_nondet(|| 27.0f64.cbrt());
ensure_nondet(|| 3.0f64.hypot(4.0f64));
ensure_nondet(|| 1f64.sin());
ensure_nondet(|| 0f64.cos());
ensure_nondet(|| 1.0f64.tan());
ensure_nondet(|| 1.0f64.asin());
ensure_nondet(|| 5.0f64.acos());
ensure_nondet(|| 1.0f64.atan());
ensure_nondet(|| 1.0f64.atan2(2.0f64));
ensure_nondet(|| 1.0f64.sinh());
ensure_nondet(|| 1.0f64.cosh());
ensure_nondet(|| 1.0f64.tanh());
ensure_nondet(|| 1.0f64.asinh());
ensure_nondet(|| 3.0f64.acosh());
ensure_nondet(|| 0.5f64.atanh());
ensure_nondet(|| 5.0f64.gamma());
ensure_nondet(|| 5.0f64.ln_gamma());
ensure_nondet(|| 5.0f64.erf());
ensure_nondet(|| 5.0f64.erfc());
// FIXME: temporarily disabled as it breaks std tests.
// ensure_nondet(|| a.log(b));
// ensure_nondet(|| a.exp());
// ensure_nondet(|| 50f64.exp2());
// ensure_nondet(|| 3f64.ln());
// ensure_nondet(|| 1f64.ln_1p());
// ensure_nondet(|| f64::consts::E.log10());
// ensure_nondet(|| f64::consts::E.log2());
// ensure_nondet(|| 27.0f64.cbrt());
// ensure_nondet(|| 3.0f64.hypot(4.0f64));
// ensure_nondet(|| 1f64.sin());
// ensure_nondet(|| 0f64.cos());
// ensure_nondet(|| 1.0f64.tan());
// ensure_nondet(|| 1.0f64.asin());
// ensure_nondet(|| 5.0f64.acos());
// ensure_nondet(|| 1.0f64.atan());
// ensure_nondet(|| 1.0f64.atan2(2.0f64));
// ensure_nondet(|| 1.0f64.sinh());
// ensure_nondet(|| 1.0f64.cosh());
// ensure_nondet(|| 1.0f64.tanh());
// ensure_nondet(|| 1.0f64.asinh());
// ensure_nondet(|| 3.0f64.acosh());
// ensure_nondet(|| 0.5f64.atanh());
// ensure_nondet(|| 5.0f64.gamma());
// ensure_nondet(|| 5.0f64.ln_gamma());
// ensure_nondet(|| 5.0f64.erf());
// ensure_nondet(|| 5.0f64.erfc());
}
pub fn test_operations_f128(a: f128, b: f128) {
test_operations_f!(a, b);
Expand Down
Loading