Skip to content

Commit 2ab7620

Browse files
authored
Unrolled build for #142514
Rollup merge of #142514 - LorrensP-2158466:miri-float-nondet-pow, r=RalfJung Miri: handling of SNaN inputs in `f*::pow` operations 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`
2 parents ad3b725 + 67ab61e commit 2ab7620

File tree

3 files changed

+109
-44
lines changed

3 files changed

+109
-44
lines changed

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

Lines changed: 69 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -191,7 +191,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
191191
let [f] = check_intrinsic_arg_count(args)?;
192192
let f = this.read_scalar(f)?.to_f32()?;
193193

194-
let res = fixed_float_value(intrinsic_name, &[f]).unwrap_or_else(||{
194+
let res = fixed_float_value(this, intrinsic_name, &[f]).unwrap_or_else(|| {
195195
// Using host floats (but it's fine, these operations do not have
196196
// guaranteed precision).
197197
let host = f.to_host();
@@ -235,7 +235,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
235235
let [f] = check_intrinsic_arg_count(args)?;
236236
let f = this.read_scalar(f)?.to_f64()?;
237237

238-
let res = fixed_float_value(intrinsic_name, &[f]).unwrap_or_else(||{
238+
let res = fixed_float_value(this, intrinsic_name, &[f]).unwrap_or_else(|| {
239239
// Using host floats (but it's fine, these operations do not have
240240
// guaranteed precision).
241241
let host = f.to_host();
@@ -312,7 +312,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
312312
let f1 = this.read_scalar(f1)?.to_f32()?;
313313
let f2 = this.read_scalar(f2)?.to_f32()?;
314314

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

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

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

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

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

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

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

@@ -496,52 +496,88 @@ fn apply_random_float_error_to_imm<'tcx>(
496496
/// - logf32, logf64, log2f32, log2f64, log10f32, log10f64
497497
/// - powf32, powf64
498498
///
499+
/// # Return
500+
///
499501
/// Returns `Some(output)` if the `intrinsic` results in a defined fixed `output` specified in the C standard
500502
/// (specifically, C23 annex F.10) when given `args` as arguments. Outputs that are unaffected by a relative error
501503
/// (such as INF and zero) are not handled here, they are assumed to be handled by the underlying
502504
/// implementation. Returns `None` if no specific value is guaranteed.
505+
///
506+
/// # Note
507+
///
508+
/// For `powf*` operations of the form:
509+
///
510+
/// - `(SNaN)^(±0)`
511+
/// - `1^(SNaN)`
512+
///
513+
/// The result is implementation-defined:
514+
/// - musl returns for both `1.0`
515+
/// - glibc returns for both `NaN`
516+
///
517+
/// This discrepancy exists because SNaN handling is not consistently defined across platforms,
518+
/// and the C standard leaves behavior for SNaNs unspecified.
519+
///
520+
/// Miri chooses to adhere to both implementations and returns either one of them non-deterministically.
503521
fn fixed_float_value<S: Semantics>(
522+
ecx: &mut MiriInterpCx<'_>,
504523
intrinsic_name: &str,
505524
args: &[IeeeFloat<S>],
506525
) -> Option<IeeeFloat<S>> {
507526
let one = IeeeFloat::<S>::one();
508-
match (intrinsic_name, args) {
527+
Some(match (intrinsic_name, args) {
509528
// cos(+- 0) = 1
510-
("cosf32" | "cosf64", [input]) if input.is_zero() => Some(one),
529+
("cosf32" | "cosf64", [input]) if input.is_zero() => one,
511530

512531
// 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),
532+
("expf32" | "expf64" | "exp2f32" | "exp2f64", [input]) if input.is_zero() => one,
517533

518534
// (-1)^(±INF) = 1
519-
("powf32" | "powf64", [base, exp]) if *base == -one && exp.is_infinite() => Some(one),
535+
("powf32" | "powf64", [base, exp]) if *base == -one && exp.is_infinite() => one,
536+
537+
// 1^y = 1 for any y, even a NaN
538+
("powf32" | "powf64", [base, exp]) if *base == one => {
539+
let rng = ecx.machine.rng.get_mut();
540+
// SNaN exponents get special treatment: they might return 1, or a NaN.
541+
let return_nan = exp.is_signaling() && ecx.machine.float_nondet && rng.random();
542+
// Handle both the musl and glibc cases non-deterministically.
543+
if return_nan { ecx.generate_nan(args) } else { one }
544+
}
520545

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.
524546
// x^(±0) = 1 for any x, even a NaN
525-
("powf32" | "powf64", [_, exp]) if exp.is_zero() => Some(one),
547+
("powf32" | "powf64", [base, exp]) if exp.is_zero() => {
548+
let rng = ecx.machine.rng.get_mut();
549+
// SNaN bases get special treatment: they might return 1, or a NaN.
550+
let return_nan = base.is_signaling() && ecx.machine.float_nondet && rng.random();
551+
// Handle both the musl and glibc cases non-deterministically.
552+
if return_nan { ecx.generate_nan(args) } else { one }
553+
}
526554

527-
// There are a lot of cases for fixed outputs according to the C Standard, but these are mainly INF or zero
528-
// which are not affected by the applied error.
529-
_ => None,
530-
}
555+
// There are a lot of cases for fixed outputs according to the C Standard, but these are
556+
// mainly INF or zero which are not affected by the applied error.
557+
_ => return None,
558+
})
531559
}
532560

533-
/// Returns `Some(output)` if `powi` (called `pown` in C) results in a fixed value specified in the C standard
534-
/// (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()),
542-
543-
_ => None,
544-
}
561+
/// Returns `Some(output)` if `powi` (called `pown` in C) results in a fixed value specified in the
562+
/// C standard (specifically, C23 annex F.10.4.6) when doing `base^exp`. Otherwise, returns `None`.
563+
fn fixed_powi_float_value<S: Semantics>(
564+
ecx: &mut MiriInterpCx<'_>,
565+
base: IeeeFloat<S>,
566+
exp: i32,
567+
) -> Option<IeeeFloat<S>> {
568+
Some(match exp {
569+
0 => {
570+
let one = IeeeFloat::<S>::one();
571+
let rng = ecx.machine.rng.get_mut();
572+
let return_nan = ecx.machine.float_nondet && rng.random() && base.is_signaling();
573+
// For SNaN treatment, we are consistent with `powf`above.
574+
// (We wouldn't have two, unlike powf all implementations seem to agree for powi,
575+
// but for now we are maximally conservative.)
576+
if return_nan { ecx.generate_nan(&[base]) } else { one }
577+
}
578+
579+
_ => return None,
580+
})
545581
}
546582

547583
/// Given an floating-point operation and a floating-point value, clamps the result to the output

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

Lines changed: 14 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1066,17 +1066,6 @@ 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);
10801069

10811070
assert_eq!(0f32.powi(10), 0.0);
10821071
assert_eq!(0f64.powi(100), 0.0);
@@ -1500,4 +1489,18 @@ fn test_non_determinism() {
15001489
test_operations_f32(12., 5.);
15011490
test_operations_f64(19., 11.);
15021491
test_operations_f128(25., 18.);
1492+
1493+
1494+
// SNaN^0 = (1 | NaN)
1495+
ensure_nondet(|| f32::powf(SNAN_F32, 0.0).is_nan());
1496+
ensure_nondet(|| f64::powf(SNAN_F64, 0.0).is_nan());
1497+
1498+
// 1^SNaN = (1 | NaN)
1499+
ensure_nondet(|| f32::powf(1.0, SNAN_F32).is_nan());
1500+
ensure_nondet(|| f64::powf(1.0, SNAN_F64).is_nan());
1501+
1502+
// same as powf (keep it consistent):
1503+
// x^SNaN = (1 | NaN)
1504+
ensure_nondet(|| f32::powi(SNAN_F32, 0).is_nan());
1505+
ensure_nondet(|| f64::powi(SNAN_F64, 0).is_nan());
15031506
}

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

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -260,6 +260,7 @@ fn test_f32() {
260260

261261
// Intrinsics
262262
let nan = F32::nan(Neg, Quiet, 0).as_f32();
263+
let snan = F32::nan(Neg, Signaling, 1).as_f32();
263264
check_all_outcomes(
264265
HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
265266
|| F32::from(f32::min(nan, nan)),
@@ -313,6 +314,18 @@ fn test_f32() {
313314
HashSet::from_iter([F32::nan(Pos, Quiet, 0), F32::nan(Neg, Quiet, 0)]),
314315
|| F32::from(nan.ln_gamma().0),
315316
);
317+
check_all_outcomes(
318+
HashSet::from_iter([
319+
F32::from(1.0),
320+
F32::nan(Pos, Quiet, 0),
321+
F32::nan(Neg, Quiet, 0),
322+
F32::nan(Pos, Quiet, 1),
323+
F32::nan(Neg, Quiet, 1),
324+
F32::nan(Pos, Signaling, 1),
325+
F32::nan(Neg, Signaling, 1),
326+
]),
327+
|| F32::from(snan.powf(0.0)),
328+
);
316329
}
317330

318331
fn test_f64() {
@@ -376,6 +389,7 @@ fn test_f64() {
376389

377390
// Intrinsics
378391
let nan = F64::nan(Neg, Quiet, 0).as_f64();
392+
let snan = F64::nan(Neg, Signaling, 1).as_f64();
379393
check_all_outcomes(
380394
HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
381395
|| F64::from(f64::min(nan, nan)),
@@ -433,6 +447,18 @@ fn test_f64() {
433447
HashSet::from_iter([F64::nan(Pos, Quiet, 0), F64::nan(Neg, Quiet, 0)]),
434448
|| F64::from(nan.ln_gamma().0),
435449
);
450+
check_all_outcomes(
451+
HashSet::from_iter([
452+
F64::from(1.0),
453+
F64::nan(Pos, Quiet, 0),
454+
F64::nan(Neg, Quiet, 0),
455+
F64::nan(Pos, Quiet, 1),
456+
F64::nan(Neg, Quiet, 1),
457+
F64::nan(Pos, Signaling, 1),
458+
F64::nan(Neg, Signaling, 1),
459+
]),
460+
|| F64::from(snan.powf(0.0)),
461+
);
436462
}
437463

438464
fn test_casts() {

0 commit comments

Comments
 (0)