Skip to content

Commit 2bac80d

Browse files
implement powf(1, SNaN) non-det
1 parent eba5d08 commit 2bac80d

File tree

2 files changed

+29
-15
lines changed

2 files changed

+29
-15
lines changed

src/tools/miri/src/intrinsics/mod.rs

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -506,6 +506,13 @@ fn random_nan<S: Semantics>(rng: &mut StdRng) -> IeeeFloat<S> {
506506
/// - logf32, logf64, log2f32, log2f64, log10f32, log10f64
507507
/// - powf32, powf64
508508
///
509+
/// # Return
510+
///
511+
/// Returns `Some(output)` if the `intrinsic` results in a defined fixed `output` specified in the C standard
512+
/// (specifically, C23 annex F.10) when given `args` as arguments. Outputs that are unaffected by a relative error
513+
/// (such as INF and zero) are not handled here, they are assumed to be handled by the underlying
514+
/// implementation. Returns `None` if no specific value is guaranteed.
515+
///
509516
/// # Note
510517
///
511518
/// For `powf*` operations of the form:
@@ -520,12 +527,7 @@ fn random_nan<S: Semantics>(rng: &mut StdRng) -> IeeeFloat<S> {
520527
/// This discrepancy exists because SNaN handling is not consistently defined across platforms,
521528
/// and the C standard leaves behavior for SNaNs unspecified.
522529
///
523-
/// # Return
524-
///
525-
/// Returns `Some(output)` if the `intrinsic` results in a defined fixed `output` specified in the C standard
526-
/// (specifically, C23 annex F.10) when given `args` as arguments. Outputs that are unaffected by a relative error
527-
/// (such as INF and zero) are not handled here, they are assumed to be handled by the underlying
528-
/// implementation. Returns `None` if no specific value is guaranteed.
530+
/// Miri chooses to adhere to both implementations and returns either one of them non-deterministically.
529531
fn fixed_float_value<'tcx, S: Semantics>(
530532
ecx: &mut MiriInterpCx<'tcx>,
531533
intrinsic_name: &str,
@@ -539,12 +541,15 @@ fn fixed_float_value<'tcx, S: Semantics>(
539541
// e^0 = 1
540542
("expf32" | "expf64" | "exp2f32" | "exp2f64", [input]) if input.is_zero() => one,
541543

542-
// 1^y = 1 for any y, even a NaN
543-
("powf32" | "powf64", [base, _]) if *base == one => one,
544-
545544
// (-1)^(±INF) = 1
546545
("powf32" | "powf64", [base, exp]) if *base == -one && exp.is_infinite() => one,
547546

547+
// 1^y = 1 for any y, even a NaN, *but* not a SNaN
548+
("powf32" | "powf64", [base, exp]) if *base == one => {
549+
let rng = ecx.machine.rng.get_mut();
550+
// Handle both the musl and glibc cases non-deterministically.
551+
if !exp.is_signaling() || rng.random() { one } else { random_nan(rng) }
552+
}
548553
// x^(±0) = 1 for any x, even a NaN, *but* not a SNaN
549554
("powf32" | "powf64", [base, exp]) if exp.is_zero() => {
550555
// Handle both the musl and glibc cases non-deterministically.

src/tools/miri/tests/pass/float.rs

Lines changed: 15 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1066,25 +1066,34 @@ pub fn libm() {
10661066
assert_eq!((-1f32).powf(f32::NEG_INFINITY), 1.0);
10671067
assert_eq!((-1f64).powf(f64::NEG_INFINITY), 1.0);
10681068

1069-
macro_rules! test_snan_pow {
1070-
($snan:expr, $pow_op:path) => {{
1069+
// Makes sure an operations returns both `1` and a `NaN` randomly.
1070+
macro_rules! test_snan_nondet {
1071+
($pow_op:expr) => {{
10711072
let mut nan_seen = false;
10721073
let mut one_seen = false;
10731074

10741075
for _ in 0..64 {
1075-
let res = $pow_op($snan, 0 as _);
1076+
let res = $pow_op;
10761077
nan_seen |= res.is_nan();
10771078
one_seen |= res == 1.0;
1079+
1080+
// speedup test
1081+
if nan_seen && one_seen { break; };
10781082
}
10791083

10801084
let op_as_str = stringify!($pow_op);
10811085

1082-
assert!(nan_seen && one_seen, "{}(SNaN, 0) should return both `NaN` or `1.0` randomly", op_as_str);
1086+
assert!(nan_seen && one_seen, "{} should return both `NaN` or `1.0` randomly", op_as_str);
10831087
}};
10841088
}
10851089

1086-
test_snan_pow!(SNAN_F32, f32::powf);
1087-
test_snan_pow!(SNAN_F64, f64::powf);
1090+
// x^(SNaN) = (1 | NaN)
1091+
test_snan_nondet!(f32::powf(SNAN_F32, 0.0));
1092+
test_snan_nondet!(f64::powf(SNAN_F64, 0.0));
1093+
1094+
// 1^(SNaN) = (1 | NaN)
1095+
test_snan_nondet!(f32::powf(1.0, SNAN_F32));
1096+
test_snan_nondet!(f64::powf(1.0, SNAN_F64));
10881097

10891098

10901099
// For pown (powi in rust) the C standard says:

0 commit comments

Comments
 (0)