miri: algebraic intrinsics: bring back float non-determinism

This commit is contained in:
Ralf Jung
2025-04-29 11:03:30 +02:00
parent 1b8ab72680
commit 2393e447eb
6 changed files with 107 additions and 86 deletions

View File

@@ -178,8 +178,7 @@ impl<'tcx, M: Machine<'tcx>> InterpCx<'tcx, M> {
let res = self.binary_op(op, &a, &b)?;
// `binary_op` already called `generate_nan` if needed.
// FIXME: Miri should add some non-determinism to the result here to catch any dependences on exact computations. This has previously been done, but the behaviour was removed as part of constification.
let res = M::apply_float_nondet(self, res)?;
self.write_immediate(*res, dest)?;
}

View File

@@ -276,6 +276,14 @@ pub trait Machine<'tcx>: Sized {
F2::NAN
}
/// Apply non-determinism to float operations that do not return a precise result.
fn apply_float_nondet(
_ecx: &mut InterpCx<'tcx, Self>,
val: ImmTy<'tcx, Self::Provenance>,
) -> InterpResult<'tcx, ImmTy<'tcx, Self::Provenance>> {
interp_ok(val)
}
/// Determines the result of `min`/`max` on floats when the arguments are equal.
fn equal_float_min_max<F: Float>(_ecx: &InterpCx<'tcx, Self>, a: F, _b: F) -> F {
// By default, we pick the left argument.