Skip to content

Commit 1dc8c00

Browse files
Auto merge of #142514 - LorrensP-2158466:miri-float-nondet-pow, r=<try>
Miri: handling of SNaN inputs in `f*::pow` operations <!-- homu-ignore:start --> <!-- If this PR is related to an unstable feature or an otherwise tracked effort, please link to the relevant tracking issue here. If you don't know of a related tracking issue or there are none, feel free to ignore this. This PR will get automatically assigned to a reviewer. In case you would like a specific user to review your work, you can assign it to them by using r? <reviewer name> --> <!-- homu-ignore:end --> fixes [miri/#4286](rust-lang/miri#4286) and related to #138062 and [miri/#4208](rust-lang/miri#4208 (comment)). For the following cases of the powf or powi operations, Miri returns either `1.0` or an arbitrary `NaN`: - `powf(SNaN, 0.0)` - `powf(1.0, SNaN)` - `powi(SNaN, 0)` Also added a macro in `miri/tests/pass/float.rs` which conveniently checks if both are indeed returned from such an operation. Made these changes in the rust repo so I could test against stdlib, since these were impacted some time ago and were fixed in #138062. Tested with: ```fish env MIRIFLAGS=-Zmiri-many-seeds ./x miri --no-fail-fast std core coretests -- f32 f64 ``` This was successful. This does take a while, so I recommend using `--no-doc` and separate use of `f32` or `f64` The pr is somewhat split up into 3 main commits, which implement the cases described above. The first commit also introduces the macro, and the last commit is just a global refactor of some things. r? `@RalfJung` try-job: x86_64-gnu-aux
2 parents fe5f3de + 550a13b commit 1dc8c00

File tree

2 files changed

+102
-38
lines changed

2 files changed

+102
-38
lines changed

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

Lines changed: 69 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ mod simd;
66
use std::ops::Neg;
77

88
use rand::Rng;
9+
use rand::rngs::StdRng;
910
use rustc_abi::Size;
1011
use rustc_apfloat::ieee::{IeeeFloat, Semantics};
1112
use rustc_apfloat::{self, Float, Round};
@@ -191,7 +192,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
191192
let [f] = check_intrinsic_arg_count(args)?;
192193
let f = this.read_scalar(f)?.to_f32()?;
193194

194-
let res = fixed_float_value(intrinsic_name, &[f]).unwrap_or_else(||{
195+
let res = fixed_float_value(this, intrinsic_name, &[f]).unwrap_or_else(||{
195196
// Using host floats (but it's fine, these operations do not have
196197
// guaranteed precision).
197198
let host = f.to_host();
@@ -235,7 +236,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
235236
let [f] = check_intrinsic_arg_count(args)?;
236237
let f = this.read_scalar(f)?.to_f64()?;
237238

238-
let res = fixed_float_value(intrinsic_name, &[f]).unwrap_or_else(||{
239+
let res = fixed_float_value(this, intrinsic_name, &[f]).unwrap_or_else(||{
239240
// Using host floats (but it's fine, these operations do not have
240241
// guaranteed precision).
241242
let host = f.to_host();
@@ -312,7 +313,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
312313
let f1 = this.read_scalar(f1)?.to_f32()?;
313314
let f2 = this.read_scalar(f2)?.to_f32()?;
314315

315-
let res = fixed_float_value(intrinsic_name, &[f1, f2]).unwrap_or_else(|| {
316+
let res = fixed_float_value(this, intrinsic_name, &[f1, f2]).unwrap_or_else(|| {
316317
// Using host floats (but it's fine, this operation does not have guaranteed precision).
317318
let res = f1.to_host().powf(f2.to_host()).to_soft();
318319

@@ -330,7 +331,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
330331
let f1 = this.read_scalar(f1)?.to_f64()?;
331332
let f2 = this.read_scalar(f2)?.to_f64()?;
332333

333-
let res = fixed_float_value(intrinsic_name, &[f1, f2]).unwrap_or_else(|| {
334+
let res = fixed_float_value(this, intrinsic_name, &[f1, f2]).unwrap_or_else(|| {
334335
// Using host floats (but it's fine, this operation does not have guaranteed precision).
335336
let res = f1.to_host().powf(f2.to_host()).to_soft();
336337

@@ -349,7 +350,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
349350
let f = this.read_scalar(f)?.to_f32()?;
350351
let i = this.read_scalar(i)?.to_i32()?;
351352

352-
let res = fixed_powi_float_value(f, i).unwrap_or_else(|| {
353+
let res = fixed_powi_float_value(this, f, i).unwrap_or_else(|| {
353354
// Using host floats (but it's fine, this operation does not have guaranteed precision).
354355
let res = f.to_host().powi(i).to_soft();
355356

@@ -367,7 +368,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
367368
let f = this.read_scalar(f)?.to_f64()?;
368369
let i = this.read_scalar(i)?.to_i32()?;
369370

370-
let res = fixed_powi_float_value(f, i).unwrap_or_else(|| {
371+
let res = fixed_powi_float_value(this, f, i).unwrap_or_else(|| {
371372
// Using host floats (but it's fine, this operation does not have guaranteed precision).
372373
let res = f.to_host().powi(i).to_soft();
373374

@@ -489,56 +490,97 @@ fn apply_random_float_error_to_imm<'tcx>(
489490
interp_ok(ImmTy::from_scalar_int(res, val.layout))
490491
}
491492

493+
/// Returns either a SNaN or a QNaN, with a randomly generated payload.
494+
fn random_nan<S: Semantics>(rng: &mut StdRng) -> IeeeFloat<S> {
495+
if rng.random() {
496+
IeeeFloat::<S>::snan(Some(rng.random()))
497+
} else {
498+
IeeeFloat::<S>::qnan(Some(rng.random()))
499+
}
500+
}
501+
492502
/// For the intrinsics:
493503
/// - sinf32, sinf64
494504
/// - cosf32, cosf64
495505
/// - expf32, expf64, exp2f32, exp2f64
496506
/// - logf32, logf64, log2f32, log2f64, log10f32, log10f64
497507
/// - powf32, powf64
498508
///
509+
/// # Return
510+
///
499511
/// Returns `Some(output)` if the `intrinsic` results in a defined fixed `output` specified in the C standard
500512
/// (specifically, C23 annex F.10) when given `args` as arguments. Outputs that are unaffected by a relative error
501513
/// (such as INF and zero) are not handled here, they are assumed to be handled by the underlying
502514
/// implementation. Returns `None` if no specific value is guaranteed.
515+
///
516+
/// # Note
517+
///
518+
/// For `powf*` operations of the form:
519+
///
520+
/// - `(SNaN)^(±0)`
521+
/// - `1^(SNaN)`
522+
///
523+
/// The result is implementation-defined:
524+
/// - musl returns for both `1.0`
525+
/// - glibc returns for both `NaN`
526+
///
527+
/// This discrepancy exists because SNaN handling is not consistently defined across platforms,
528+
/// and the C standard leaves behavior for SNaNs unspecified.
529+
///
530+
/// Miri chooses to adhere to both implementations and returns either one of them non-deterministically.
503531
fn fixed_float_value<S: Semantics>(
532+
ecx: &mut MiriInterpCx<'_>,
504533
intrinsic_name: &str,
505534
args: &[IeeeFloat<S>],
506535
) -> Option<IeeeFloat<S>> {
507536
let one = IeeeFloat::<S>::one();
508-
match (intrinsic_name, args) {
537+
Some(match (intrinsic_name, args) {
509538
// cos(+- 0) = 1
510-
("cosf32" | "cosf64", [input]) if input.is_zero() => Some(one),
539+
("cosf32" | "cosf64", [input]) if input.is_zero() => one,
511540

512541
// e^0 = 1
513-
("expf32" | "expf64" | "exp2f32" | "exp2f64", [input]) if input.is_zero() => Some(one),
514-
515-
// 1^y = 1 for any y, even a NaN.
516-
("powf32" | "powf64", [base, _]) if *base == one => Some(one),
542+
("expf32" | "expf64" | "exp2f32" | "exp2f64", [input]) if input.is_zero() => one,
517543

518544
// (-1)^(±INF) = 1
519-
("powf32" | "powf64", [base, exp]) if *base == -one && exp.is_infinite() => Some(one),
545+
("powf32" | "powf64", [base, exp]) if *base == -one && exp.is_infinite() => one,
520546

521-
// FIXME(#4286): The C ecosystem is inconsistent with handling sNaN's, some return 1 others propogate
522-
// the NaN. We should return either 1 or the NaN non-deterministically here.
523-
// But for now, just handle them all the same.
524-
// x^(±0) = 1 for any x, even a NaN
525-
("powf32" | "powf64", [_, exp]) if exp.is_zero() => Some(one),
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+
}
553+
554+
// x^(±0) = 1 for any x, even a NaN, *but* not a SNaN
555+
("powf32" | "powf64", [base, exp]) if exp.is_zero() => {
556+
let rng = ecx.machine.rng.get_mut();
557+
// Handle both the musl and glibc cases non-deterministically.
558+
if !base.is_signaling() || rng.random() { one } else { random_nan(rng) }
559+
}
526560

527561
// There are a lot of cases for fixed outputs according to the C Standard, but these are mainly INF or zero
528562
// which are not affected by the applied error.
529-
_ => None,
530-
}
563+
_ => return None,
564+
})
531565
}
532566

533567
/// Returns `Some(output)` if `powi` (called `pown` in C) results in a fixed value specified in the C standard
534568
/// (specifically, C23 annex F.10.4.6) when doing `base^exp`. Otherwise, returns `None`.
535-
fn fixed_powi_float_value<S: Semantics>(base: IeeeFloat<S>, exp: i32) -> Option<IeeeFloat<S>> {
536-
match (base.category(), exp) {
537-
// x^0 = 1, if x is not a Signaling NaN
538-
// FIXME(#4286): The C ecosystem is inconsistent with handling sNaN's, some return 1 others propogate
539-
// the NaN. We should return either 1 or the NaN non-deterministically here.
540-
// But for now, just handle them all the same.
541-
(_, 0) => Some(IeeeFloat::<S>::one()),
569+
// 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.
570+
fn fixed_powi_float_value<S: Semantics>(
571+
ecx: &mut MiriInterpCx<'_>,
572+
base: IeeeFloat<S>,
573+
exp: i32,
574+
) -> Option<IeeeFloat<S>> {
575+
match exp {
576+
0 => {
577+
let one = IeeeFloat::<S>::one();
578+
let rng = ecx.machine.rng.get_mut();
579+
Some(
580+
// Handle both the musl and glibc powf cases non-deterministically.
581+
if !base.is_signaling() || rng.random() { one } else { random_nan(rng) },
582+
)
583+
}
542584

543585
_ => None,
544586
}

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

Lines changed: 33 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1066,17 +1066,39 @@ 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-
// For pow (powf in rust) the C standard says:
1070-
// x^0 = 1 for all x even a sNaN
1071-
// FIXME(#4286): this does not match the behavior of all implementations.
1072-
assert_eq!(SNAN_F32.powf(0.0), 1.0);
1073-
assert_eq!(SNAN_F64.powf(0.0), 1.0);
1074-
1075-
// For pown (powi in rust) the C standard says:
1076-
// x^0 = 1 for all x even a sNaN
1077-
// FIXME(#4286): this does not match the behavior of all implementations.
1078-
assert_eq!(SNAN_F32.powi(0), 1.0);
1079-
assert_eq!(SNAN_F64.powi(0), 1.0);
1069+
// Makes sure an operations returns both `1` and a `NaN` randomly.
1070+
macro_rules! test_snan_nondet {
1071+
($pow_op:expr) => {{
1072+
let mut nan_seen = false;
1073+
let mut one_seen = false;
1074+
1075+
for _ in 0..64 {
1076+
let res = $pow_op;
1077+
nan_seen |= res.is_nan();
1078+
one_seen |= res == 1.0;
1079+
1080+
// little speedup
1081+
if nan_seen && one_seen { break; };
1082+
}
1083+
1084+
let op_as_str = stringify!($pow_op);
1085+
1086+
assert!(nan_seen && one_seen, "{} should return both `NaN` or `1.0` randomly", op_as_str);
1087+
}};
1088+
}
1089+
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));
1097+
1098+
// same as powf (keep it consistent):
1099+
// x^(SNaN) = (1 | NaN)
1100+
test_snan_nondet!(f32::powi(SNAN_F32, 0));
1101+
test_snan_nondet!(f64::powi(SNAN_F64, 0));
10801102

10811103
assert_eq!(0f32.powi(10), 0.0);
10821104
assert_eq!(0f64.powi(100), 0.0);

0 commit comments

Comments
 (0)