add float_nan test for powf

plus various minor tweaks

Author: RalfJung

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

@@ -17,7 +17,6 @@ use self::atomic::EvalContextExt as _;
 use self::helpers::{ToHost, ToSoft, check_intrinsic_arg_count};
 use self::simd::EvalContextExt as _;
 use crate::math::{IeeeExt, apply_random_float_error_ulp};
-use crate::operator::EvalContextExt as _;
 use crate::*;
 
 impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
@@ -535,18 +534,20 @@ fn fixed_float_value<S: Semantics>(
         // (-1)^(±INF) = 1
         ("powf32" | "powf64", [base, exp]) if *base == -one && exp.is_infinite() => one,
 
-        // 1^y = 1 for any y, even a NaN, *but* not a SNaN
+        // 1^y = 1 for any y, even a NaN
         ("powf32" | "powf64", [base, exp]) if *base == one => {
             let rng = ecx.machine.rng.get_mut();
-            let return_nan = ecx.machine.float_nondet && rng.random() && exp.is_signaling();
+            // 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 }
         }
 
-        // x^(±0) = 1 for any x, even a NaN, *but* not a SNaN
+        // x^(±0) = 1 for any x, even a NaN
         ("powf32" | "powf64", [base, exp]) if exp.is_zero() => {
             let rng = ecx.machine.rng.get_mut();
-            let return_nan = ecx.machine.float_nondet && rng.random() && base.is_signaling();
+            // 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 }
         }
@@ -559,7 +560,9 @@ fn fixed_float_value<S: Semantics>(
 
 /// 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`.
-// TODO: I'm not sure what I should document here about pown(1, SNaN) since musl and glibc do the same and the C standard is explicit here.
+/// 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.)
 fn fixed_powi_float_value<S: Semantics>(
     ecx: &mut MiriInterpCx<'_>,
     base: IeeeFloat<S>,

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

@@ -1491,16 +1491,16 @@ fn test_non_determinism() {
     test_operations_f128(25., 18.);
 
 
-    // x^(SNaN) = (1 | NaN)
-    ensure_nondet(|| f32::powf(SNAN_F32, 0.0));
-    ensure_nondet(|| f64::powf(SNAN_F64, 0.0));
+    // 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));
-    ensure_nondet(|| f64::powf(1.0, SNAN_F64));
+    // 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));
-    ensure_nondet(|| f64::powi(SNAN_F64, 0));
+    // x^SNaN = (1 | NaN)
+    ensure_nondet(|| f32::powi(SNAN_F32, 0).is_nan());
+    ensure_nondet(|| f64::powi(SNAN_F64, 0).is_nan());
 }

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

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