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)
+    // SNaN^0 = (1 | NaN)
     ensure_nondet(|| f32::powf(SNAN_F32, 0.0));
     ensure_nondet(|| f64::powf(SNAN_F64, 0.0));
 
-    // 1^(SNaN) = (1 | NaN)
+    // 1^SNaN = (1 | NaN)
     ensure_nondet(|| f32::powf(1.0, SNAN_F32));
     ensure_nondet(|| f64::powf(1.0, SNAN_F64));
 
     // same as powf (keep it consistent):
-    // x^(SNaN) = (1 | NaN)
+    // x^SNaN = (1 | NaN)
     ensure_nondet(|| f32::powi(SNAN_F32, 0));
     ensure_nondet(|| f64::powi(SNAN_F64, 0));
 }