@@ -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.
503521fn 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
0 commit comments