Add non-determinism to algebraic intrinsics.

[bjoernager]

Tracking issue: rust-lang/rust#136469

Since rust-lang/rust#140172, the result of a call to any of the algebraic_add, algebraic_sub, algebraic_mul, algebraic_div, or algebraic_rem intrinsics has been deterministic in Miri.

Valid programmes do not depend on these computations being exact, thus Miri should add some non-determinism so that any such dependence is more likely to be caught.

[workingjubilee]

What kind of nondet are you thinking of?

I mean, we should probably try to reason a bit about the actual transformations that are allowed rather than just pulling floats out of a random number generator. Valid programs might still use mathematical reasoning (...with some appropriate error bars on either side, of course, to account for the differences between float-exact and real-exact computations).

One option I can think of is to flip a coin and then decide whether or not to compute the next few algebraic math operations to an absurd precision, without rounding inbetween?

[bjoernager]

Initially, these intrinsics used miri::intrinsics::apply_random_float_error_ulp_to_imm on the result before returning:

// Apply a relative error of 4ULP to simulate non-deterministic precision loss
// due to optimizations.
let res = apply_random_float_error_to_imm(this, res, 2 /* log2(4) */)?;

_{The final value of 4ULP was set in rust-lang/rust#136457.}

There had been some concerns about these computations being conditionally-exact. It seems to me that this is the optimal solution.

[RalfJung]

Formally, the algebraic operations return an arbitrary floating-point value. We do not make any guarantees on precision, and it is impossible for clients to do soundness-critical reasoning about what these functions return.

In practice, doing this in Miri would probably not help in finding real bugs, people would just disable Miri on the affected tests... so what Miri does is to just appliy a small imprecision, to at least catch code that incorrectly assumes an exact result.

[nnethercote]

Uh, github is claiming I closed this as completed. I've never seen this issue. I don't know what's going on.

[saethlin]

You have permission to close issues, and you just pushed a commit to the default branch of your fork that uses a closing keyword with this issue number.

I and many other contributors don't keep the master branch of our forks up to date anymore because of this problem.

Fortunately in this case, the issue should be closed.