Skip to content

Commit 958d5be

Browse files
implement powf(1, SNaN) non-det
1 parent 6ce85d8 commit 958d5be

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
@@ -518,6 +518,13 @@ fn random_nan<S: Semantics>(rng: &mut StdRng) -> IeeeFloat<S> {
518518
/// - logf32, logf64, log2f32, log2f64, log10f32, log10f64
519519
/// - powf32, powf64
520520
///
521+
/// # Return
522+
///
523+
/// Returns `Some(output)` if the `intrinsic` results in a defined fixed `output` specified in the C standard
524+
/// (specifically, C23 annex F.10) when given `args` as arguments. Outputs that are unaffected by a relative error
525+
/// (such as INF and zero) are not handled here, they are assumed to be handled by the underlying
526+
/// implementation. Returns `None` if no specific value is guaranteed.
527+
///
521528
/// # Note
522529
///
523530
/// For `powf*` operations of the form:
@@ -532,12 +539,7 @@ fn random_nan<S: Semantics>(rng: &mut StdRng) -> IeeeFloat<S> {
532539
/// This discrepancy exists because SNaN handling is not consistently defined across platforms,
533540
/// and the C standard leaves behavior for SNaNs unspecified.
534541
///
535-
/// # Return
536-
///
537-
/// Returns `Some(output)` if the `intrinsic` results in a defined fixed `output` specified in the C standard
538-
/// (specifically, C23 annex F.10) when given `args` as arguments. Outputs that are unaffected by a relative error
539-
/// (such as INF and zero) are not handled here, they are assumed to be handled by the underlying
540-
/// implementation. Returns `None` if no specific value is guaranteed.
542+
/// Miri chooses to adhere to both implementations and returns either one of them non-deterministically.
541543
fn fixed_float_value<'tcx, S: Semantics>(
542544
ecx: &mut MiriInterpCx<'tcx>,
543545
intrinsic_name: &str,
@@ -551,12 +553,15 @@ fn fixed_float_value<'tcx, S: Semantics>(
551553
// e^0 = 1
552554
("expf32" | "expf64" | "exp2f32" | "exp2f64", [input]) if input.is_zero() => one,
553555

554-
// 1^y = 1 for any y, even a NaN
555-
("powf32" | "powf64", [base, _]) if *base == one => one,
556-
557556
// (-1)^(±INF) = 1
558557
("powf32" | "powf64", [base, exp]) if *base == -one && exp.is_infinite() => one,
559558

559+
// 1^y = 1 for any y, even a NaN, *but* not a SNaN
560+
("powf32" | "powf64", [base, exp]) if *base == one => {
561+
let rng = ecx.machine.rng.get_mut();
562+
// Handle both the musl and glibc cases non-deterministically.
563+
if !exp.is_signaling() || rng.random() { one } else { random_nan(rng) }
564+
}
560565
// x^(±0) = 1 for any x, even a NaN, *but* not a SNaN
561566
("powf32" | "powf64", [base, exp]) if exp.is_zero() => {
562567
// 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
@@ -1067,25 +1067,34 @@ pub fn libm() {
10671067
assert_eq!((-1f32).powf(f32::NEG_INFINITY), 1.0);
10681068
assert_eq!((-1f64).powf(f64::NEG_INFINITY), 1.0);
10691069

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

10751076
for _ in 0..64 {
1076-
let res = $pow_op($snan, 0 as _);
1077+
let res = $pow_op;
10771078
nan_seen |= res.is_nan();
10781079
one_seen |= res == 1.0;
1080+
1081+
// speedup test
1082+
if nan_seen && one_seen { break; };
10791083
}
10801084

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

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

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

10901099

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

0 commit comments

Comments
 (0)