@@ -17,6 +17,7 @@ use self::atomic::EvalContextExt as _;
17
17
use self::helpers::{ToHost, ToSoft, check_intrinsic_arg_count};
18
18
use self::simd::EvalContextExt as _;
19
19
use crate::math::{IeeeExt, apply_random_float_error_ulp};
20
+ use crate::operator::EvalContextExt as _;
20
21
use crate::*;
21
22
22
23
impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
@@ -191,7 +192,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
191
192
let [f] = check_intrinsic_arg_count(args)?;
192
193
let f = this.read_scalar(f)?.to_f32()?;
193
194
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(||{
195
196
// Using host floats (but it's fine, these operations do not have
196
197
// guaranteed precision).
197
198
let host = f.to_host();
@@ -235,7 +236,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
235
236
let [f] = check_intrinsic_arg_count(args)?;
236
237
let f = this.read_scalar(f)?.to_f64()?;
237
238
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(||{
239
240
// Using host floats (but it's fine, these operations do not have
240
241
// guaranteed precision).
241
242
let host = f.to_host();
@@ -312,7 +313,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
312
313
let f1 = this.read_scalar(f1)?.to_f32()?;
313
314
let f2 = this.read_scalar(f2)?.to_f32()?;
314
315
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(|| {
316
317
// Using host floats (but it's fine, this operation does not have guaranteed precision).
317
318
let res = f1.to_host().powf(f2.to_host()).to_soft();
318
319
@@ -330,7 +331,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
330
331
let f1 = this.read_scalar(f1)?.to_f64()?;
331
332
let f2 = this.read_scalar(f2)?.to_f64()?;
332
333
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(|| {
334
335
// Using host floats (but it's fine, this operation does not have guaranteed precision).
335
336
let res = f1.to_host().powf(f2.to_host()).to_soft();
336
337
@@ -349,7 +350,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
349
350
let f = this.read_scalar(f)?.to_f32()?;
350
351
let i = this.read_scalar(i)?.to_i32()?;
351
352
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(|| {
353
354
// Using host floats (but it's fine, this operation does not have guaranteed precision).
354
355
let res = f.to_host().powi(i).to_soft();
355
356
@@ -367,7 +368,7 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
367
368
let f = this.read_scalar(f)?.to_f64()?;
368
369
let i = this.read_scalar(i)?.to_i32()?;
369
370
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(|| {
371
372
// Using host floats (but it's fine, this operation does not have guaranteed precision).
372
373
let res = f.to_host().powi(i).to_soft();
373
374
@@ -496,49 +497,84 @@ fn apply_random_float_error_to_imm<'tcx>(
496
497
/// - logf32, logf64, log2f32, log2f64, log10f32, log10f64
497
498
/// - powf32, powf64
498
499
///
500
+ /// # Return
501
+ ///
499
502
/// Returns `Some(output)` if the `intrinsic` results in a defined fixed `output` specified in the C standard
500
503
/// (specifically, C23 annex F.10) when given `args` as arguments. Outputs that are unaffected by a relative error
501
504
/// (such as INF and zero) are not handled here, they are assumed to be handled by the underlying
502
505
/// implementation. Returns `None` if no specific value is guaranteed.
506
+ ///
507
+ /// # Note
508
+ ///
509
+ /// For `powf*` operations of the form:
510
+ ///
511
+ /// - `(SNaN)^(±0)`
512
+ /// - `1^(SNaN)`
513
+ ///
514
+ /// The result is implementation-defined:
515
+ /// - musl returns for both `1.0`
516
+ /// - glibc returns for both `NaN`
517
+ ///
518
+ /// This discrepancy exists because SNaN handling is not consistently defined across platforms,
519
+ /// and the C standard leaves behavior for SNaNs unspecified.
520
+ ///
521
+ /// Miri chooses to adhere to both implementations and returns either one of them non-deterministically.
503
522
fn fixed_float_value<S: Semantics>(
523
+ ecx: &mut MiriInterpCx<'_>,
504
524
intrinsic_name: &str,
505
525
args: &[IeeeFloat<S>],
506
526
) -> Option<IeeeFloat<S>> {
507
527
let one = IeeeFloat::<S>::one();
508
- match (intrinsic_name, args) {
528
+ Some( match (intrinsic_name, args) {
509
529
// cos(+- 0) = 1
510
- ("cosf32" | "cosf64", [input]) if input.is_zero() => Some( one) ,
530
+ ("cosf32" | "cosf64", [input]) if input.is_zero() => one,
511
531
512
532
// 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),
533
+ ("expf32" | "expf64" | "exp2f32" | "exp2f64", [input]) if input.is_zero() => one,
517
534
518
535
// (-1)^(±INF) = 1
519
- ("powf32" | "powf64", [base, exp]) if *base == -one && exp.is_infinite() => Some(one),
536
+ ("powf32" | "powf64", [base, exp]) if *base == -one && exp.is_infinite() => one,
537
+
538
+ // 1^y = 1 for any y, even a NaN, *but* not a SNaN
539
+ ("powf32" | "powf64", [base, exp]) if *base == one => {
540
+ let rng = ecx.machine.rng.get_mut();
541
+ let return_nan = ecx.machine.float_nondet && rng.random() && exp.is_signaling();
542
+ // Handle both the musl and glibc cases non-deterministically.
543
+ if return_nan { ecx.generate_nan(args) } else { one }
544
+ }
520
545
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),
546
+ // x^(±0) = 1 for any x, even a NaN, *but* not a SNaN
547
+ ("powf32" | "powf64", [base, exp]) if exp.is_zero() => {
548
+ let rng = ecx.machine.rng.get_mut();
549
+ let return_nan = ecx.machine.float_nondet && rng.random() && base.is_signaling();
550
+ // Handle both the musl and glibc cases non-deterministically.
551
+ if return_nan { ecx.generate_nan(args) } else { one }
552
+ }
526
553
527
554
// There are a lot of cases for fixed outputs according to the C Standard, but these are mainly INF or zero
528
555
// which are not affected by the applied error.
529
- _ => None,
530
- }
556
+ _ => return None,
557
+ })
531
558
}
532
559
533
560
/// Returns `Some(output)` if `powi` (called `pown` in C) results in a fixed value specified in the C standard
534
561
/// (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()),
562
+ // 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.
563
+ fn fixed_powi_float_value<S: Semantics>(
564
+ ecx: &mut MiriInterpCx<'_>,
565
+ base: IeeeFloat<S>,
566
+ exp: i32,
567
+ ) -> Option<IeeeFloat<S>> {
568
+ 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
+ Some(
574
+ // Handle both the musl and glibc powf cases non-deterministically.
575
+ if return_nan { ecx.generate_nan(&[base]) } else { one },
576
+ )
577
+ }
542
578
543
579
_ => None,
544
580
}
0 commit comments