add float_nan test for powf

plus various minor tweaks

3 files changed, 54 insertions, 28 deletions

diff --git a/src/tools/miri/src/intrinsics/mod.rs b/src/tools/miri/src/intrinsics/mod.rs
index 2dbcaefb94b..ed1851a19ae 100644
--- a/src/tools/miri/src/intrinsics/mod.rs
+++ b/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> {}
@@ -192,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(this, 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();
@@ -236,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(this, 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();
@@ -535,49 +534,50 @@ 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 }
         }
 
-        // 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.
+        // 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`.
-// 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.
+/// 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>> {
-    match exp {
+    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();
-            Some(
-                // Handle both the musl and glibc powf cases non-deterministically.
-                if return_nan { ecx.generate_nan(&[base]) } else { one },
-            )
+            // 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 }
         }
 
-        _ => None,
-    }
+        _ => return None,
+    })
 }
 
 /// Given an floating-point operation and a floating-point value, clamps the result to the output
diff --git a/src/tools/miri/tests/pass/float.rs b/src/tools/miri/tests/pass/float.rs
index 041e86fbe68..f21c6089a7b 100644
--- a/src/tools/miri/tests/pass/float.rs
+++ b/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());
 }
diff --git a/src/tools/miri/tests/pass/float_nan.rs b/src/tools/miri/tests/pass/float_nan.rs
index cadbbd58af5..3ffdb6868ac 100644
--- a/src/tools/miri/tests/pass/float_nan.rs
+++ b/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() {