Skip to content

Miri: handling of SNaN inputs in f*::pow operations #142514

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.

Sign up for GitHub

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 2 commits into from
Jun 30, 2025
+109 −44
Merged

Miri: handling of SNaN inputs in f*::pow operations #142514

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
60a4828
make some powf and powi cases involving SNaN non-deterministic
LorrensP-2158466 Jun 14, 2025
67ab61e
add float_nan test for powf
RalfJung Jun 29, 2025
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
102 changes: 69 additions & 33 deletions src/tools/miri/src/intrinsics/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
let [f] = check_intrinsic_arg_count(args)?;
let f = this.read_scalar(f)?.to_f32()?;

let res = fixed_float_value(intrinsic_name, &[f]).unwrap_or_else(||{
let res = fixed_float_value(this, intrinsic_name, &[f]).unwrap_or_else(|| {
// Using host floats (but it's fine, these operations do not have
// guaranteed precision).
let host = f.to_host();
Expand Down Expand Up @@ -235,7 +235,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
let [f] = check_intrinsic_arg_count(args)?;
let f = this.read_scalar(f)?.to_f64()?;

let res = fixed_float_value(intrinsic_name, &[f]).unwrap_or_else(||{
let res = fixed_float_value(this, intrinsic_name, &[f]).unwrap_or_else(|| {
// Using host floats (but it's fine, these operations do not have
// guaranteed precision).
let host = f.to_host();
Expand Down Expand Up @@ -312,7 +312,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
let f1 = this.read_scalar(f1)?.to_f32()?;
let f2 = this.read_scalar(f2)?.to_f32()?;

let res = fixed_float_value(intrinsic_name, &[f1, f2]).unwrap_or_else(|| {
let res = fixed_float_value(this, intrinsic_name, &[f1, f2]).unwrap_or_else(|| {
// Using host floats (but it's fine, this operation does not have guaranteed precision).
let res = f1.to_host().powf(f2.to_host()).to_soft();

Expand All @@ -330,7 +330,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
let f1 = this.read_scalar(f1)?.to_f64()?;
let f2 = this.read_scalar(f2)?.to_f64()?;

let res = fixed_float_value(intrinsic_name, &[f1, f2]).unwrap_or_else(|| {
let res = fixed_float_value(this, intrinsic_name, &[f1, f2]).unwrap_or_else(|| {
// Using host floats (but it's fine, this operation does not have guaranteed precision).
let res = f1.to_host().powf(f2.to_host()).to_soft();

Expand All @@ -349,7 +349,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
let f = this.read_scalar(f)?.to_f32()?;
let i = this.read_scalar(i)?.to_i32()?;

let res = fixed_powi_float_value(f, i).unwrap_or_else(|| {
let res = fixed_powi_float_value(this, f, i).unwrap_or_else(|| {
// Using host floats (but it's fine, this operation does not have guaranteed precision).
let res = f.to_host().powi(i).to_soft();

Expand All @@ -367,7 +367,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
let f = this.read_scalar(f)?.to_f64()?;
let i = this.read_scalar(i)?.to_i32()?;

let res = fixed_powi_float_value(f, i).unwrap_or_else(|| {
let res = fixed_powi_float_value(this, f, i).unwrap_or_else(|| {
// Using host floats (but it's fine, this operation does not have guaranteed precision).
let res = f.to_host().powi(i).to_soft();

Expand Down Expand Up @@ -496,52 +496,88 @@ fn apply_random_float_error_to_imm<'tcx>(
/// - logf32, logf64, log2f32, log2f64, log10f32, log10f64
/// - powf32, powf64
///
/// # Return
///
/// Returns `Some(output)` if the `intrinsic` results in a defined fixed `output` specified in the C standard
/// (specifically, C23 annex F.10) when given `args` as arguments. Outputs that are unaffected by a relative error
/// (such as INF and zero) are not handled here, they are assumed to be handled by the underlying
/// implementation. Returns `None` if no specific value is guaranteed.
///
/// # Note
///
/// For `powf*` operations of the form:
///
/// - `(SNaN)^(±0)`
/// - `1^(SNaN)`
///
/// The result is implementation-defined:
/// - musl returns for both `1.0`
/// - glibc returns for both `NaN`
///
/// This discrepancy exists because SNaN handling is not consistently defined across platforms,
/// and the C standard leaves behavior for SNaNs unspecified.
///
/// Miri chooses to adhere to both implementations and returns either one of them non-deterministically.
fn fixed_float_value<S: Semantics>(
ecx: &mut MiriInterpCx<'_>,
intrinsic_name: &str,
args: &[IeeeFloat<S>],
) -> Option<IeeeFloat<S>> {
let one = IeeeFloat::<S>::one();
match (intrinsic_name, args) {
Some(match (intrinsic_name, args) {
// cos(+- 0) = 1
("cosf32" | "cosf64", [input]) if input.is_zero() => Some(one),
("cosf32" | "cosf64", [input]) if input.is_zero() => one,

// e^0 = 1
("expf32" | "expf64" | "exp2f32" | "exp2f64", [input]) if input.is_zero() => Some(one),

// 1^y = 1 for any y, even a NaN.
("powf32" | "powf64", [base, _]) if *base == one => Some(one),
("expf32" | "expf64" | "exp2f32" | "exp2f64", [input]) if input.is_zero() => one,

// (-1)^(±INF) = 1
("powf32" | "powf64", [base, exp]) if *base == -one && exp.is_infinite() => Some(one),
("powf32" | "powf64", [base, exp]) if *base == -one && exp.is_infinite() => one,

// 1^y = 1 for any y, even a NaN
("powf32" | "powf64", [base, exp]) if *base == one => {
let rng = ecx.machine.rng.get_mut();
// SNaN exponents get special treatment: they might return 1, or a NaN.
let return_nan = exp.is_signaling() && ecx.machine.float_nondet && rng.random();
// Handle both the musl and glibc cases non-deterministically.
if return_nan { ecx.generate_nan(args) } else { one }
}

// FIXME(#4286): The C ecosystem is inconsistent with handling sNaN's, some return 1 others propogate
// the NaN. We should return either 1 or the NaN non-deterministically here.
// But for now, just handle them all the same.
// x^(±0) = 1 for any x, even a NaN
("powf32" | "powf64", [_, exp]) if exp.is_zero() => Some(one),
("powf32" | "powf64", [base, exp]) if exp.is_zero() => {
let rng = ecx.machine.rng.get_mut();
// SNaN bases get special treatment: they might return 1, or a NaN.
let return_nan = base.is_signaling() && ecx.machine.float_nondet && rng.random();
// Handle both the musl and glibc cases non-deterministically.
if return_nan { ecx.generate_nan(args) } else { one }
}

// There are a lot of cases for fixed outputs according to the C Standard, but these are mainly INF or zero
// which are not affected by the applied error.
_ => None,
}
// There are a lot of cases for fixed outputs according to the C Standard, but these are
// mainly INF or zero which are not affected by the applied error.
_ => return None,
})
}

/// Returns `Some(output)` if `powi` (called `pown` in C) results in a fixed value specified in the C standard
/// (specifically, C23 annex F.10.4.6) when doing `base^exp`. Otherwise, returns `None`.
fn fixed_powi_float_value<S: Semantics>(base: IeeeFloat<S>, exp: i32) -> Option<IeeeFloat<S>> {
match (base.category(), exp) {
// x^0 = 1, if x is not a Signaling NaN
// FIXME(#4286): The C ecosystem is inconsistent with handling sNaN's, some return 1 others propogate
// the NaN. We should return either 1 or the NaN non-deterministically here.
// But for now, just handle them all the same.
(_, 0) => Some(IeeeFloat::<S>::one()),

_ => None,
}
/// Returns `Some(output)` if `powi` (called `pown` in C) results in a fixed value specified in the
/// C standard (specifically, C23 annex F.10.4.6) when doing `base^exp`. Otherwise, returns `None`.
fn fixed_powi_float_value<S: Semantics>(
ecx: &mut MiriInterpCx<'_>,
base: IeeeFloat<S>,
exp: i32,
) -> Option<IeeeFloat<S>> {
Some(match exp {
0 => {
let one = IeeeFloat::<S>::one();
let rng = ecx.machine.rng.get_mut();
let return_nan = ecx.machine.float_nondet && rng.random() && base.is_signaling();
// For SNaN treatment, we are consistent with `powf`above.
// (We wouldn't have two, unlike powf all implementations seem to agree for powi,
// but for now we are maximally conservative.)
if return_nan { ecx.generate_nan(&[base]) } else { one }
}

_ => return None,
})
}

/// Given an floating-point operation and a floating-point value, clamps the result to the output
Expand Down
25 changes: 14 additions & 11 deletions src/tools/miri/tests/pass/float.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1066,17 +1066,6 @@ pub fn libm() {
assert_eq!((-1f32).powf(f32::NEG_INFINITY), 1.0);
assert_eq!((-1f64).powf(f64::NEG_INFINITY), 1.0);

// For pow (powf in rust) the C standard says:
// x^0 = 1 for all x even a sNaN
// FIXME(#4286): this does not match the behavior of all implementations.
assert_eq!(SNAN_F32.powf(0.0), 1.0);
assert_eq!(SNAN_F64.powf(0.0), 1.0);

// For pown (powi in rust) the C standard says:
// x^0 = 1 for all x even a sNaN
// FIXME(#4286): this does not match the behavior of all implementations.
assert_eq!(SNAN_F32.powi(0), 1.0);
assert_eq!(SNAN_F64.powi(0), 1.0);

assert_eq!(0f32.powi(10), 0.0);
assert_eq!(0f64.powi(100), 0.0);
Expand Down Expand Up @@ -1500,4 +1489,18 @@ fn test_non_determinism() {
test_operations_f32(12., 5.);
test_operations_f64(19., 11.);
test_operations_f128(25., 18.);


// SNaN^0 = (1 | NaN)
ensure_nondet(|| f32::powf(SNAN_F32, 0.0).is_nan());
ensure_nondet(|| f64::powf(SNAN_F64, 0.0).is_nan());

// 1^SNaN = (1 | NaN)
ensure_nondet(|| f32::powf(1.0, SNAN_F32).is_nan());
ensure_nondet(|| f64::powf(1.0, SNAN_F64).is_nan());

// same as powf (keep it consistent):
// x^SNaN = (1 | NaN)
ensure_nondet(|| f32::powi(SNAN_F32, 0).is_nan());
ensure_nondet(|| f64::powi(SNAN_F64, 0).is_nan());
}
26 changes: 26 additions & 0 deletions src/tools/miri/tests/pass/float_nan.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -260,6 +260,7 @@ fn test_f32() {

// Intrinsics
let nan = F32::nan(Neg, Quiet, 0).as_f32();
let snan = F32::nan(Neg, Signaling, 1).as_f32();
check_all_outcomes(
HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
|| F32::from(f32::min(nan, nan)),
Expand Down Expand Up @@ -313,6 +314,18 @@ fn test_f32() {
HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
|| F32::from(nan.ln_gamma().0),
);
check_all_outcomes(
HashSet::from_iter([
F32::from(1.0),
F32::nan(Pos, Quiet, 0),
F32::nan(Neg, Quiet, 0),
F32::nan(Pos, Quiet, 1),
F32::nan(Neg, Quiet, 1),
F32::nan(Pos, Signaling, 1),
F32::nan(Neg, Signaling, 1),
]),
|| F32::from(snan.powf(0.0)),
);
}

fn test_f64() {
Expand Down Expand Up @@ -376,6 +389,7 @@ fn test_f64() {

// Intrinsics
let nan = F64::nan(Neg, Quiet, 0).as_f64();
let snan = F64::nan(Neg, Signaling, 1).as_f64();
check_all_outcomes(
HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
|| F64::from(f64::min(nan, nan)),
Expand Down Expand Up @@ -433,6 +447,18 @@ fn test_f64() {
HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
|| F64::from(nan.ln_gamma().0),
);
check_all_outcomes(
HashSet::from_iter([
F64::from(1.0),
F64::nan(Pos, Quiet, 0),
F64::nan(Neg, Quiet, 0),
F64::nan(Pos, Quiet, 1),
F64::nan(Neg, Quiet, 1),
F64::nan(Pos, Signaling, 1),
F64::nan(Neg, Signaling, 1),
]),
|| F64::from(snan.powf(0.0)),
);
}

fn test_casts() {
Expand Down
Loading