Miri: non-deterministic floating point operations in foreign_items

[LorrensP-2158466]

Part of rust-lang/miri/#3555, this pr does the foreign_items work.

Some things have changed since #138062 and #142514. I moved the "helpers" used for creating fixed outputs and clamping operations to their defined ranges to helpers.rs. These are now also extended to handle the floating-point operations in foreign_items. Tests in miri/tests/float.rs were changed/added.

Failing tests in std were extracted, run under miri with -Zmiri-many-seeds=0..1000 and changed accordingly. Double checked with -Zmiri-many-seeds.

I noticed that the C standard doesn't specify the output ranges for all of its mathematical operations; it just specifies them as:

Returns
The sinh functions return sinh x.

So I used Wolfram|Alpha.

[rustbot]

r? @tgross35

rustbot has assigned @tgross35.
They will have a look at your PR within the next two weeks and either review your PR or reassign to another reviewer.

Use r? to explicitly pick a reviewer

[rustbot]

The Miri subtree was changed

cc @rust-lang/miri

[LorrensP-2158466]

There are some holes in the behaviour of some operations, because I did not know how I could efficiently handle them, I'll mark them and add some explanation.

Also,
r? @RalfJung

[oli-obk]

Please create a PR for the libstd changes on their own so a libs reviewer can review it. Once that is done and synced, you can open a PR against the miri repo with the miri changes.

[RalfJung]

In a previous PR we had both in one PR with two reviewers since we needed to go back and forth a bit. We could do that again? I think it worked well.

[LorrensP-2158466]

It's the same for me, I kept the commits for Miri and stdlib separate, so if I have to split it up, it's pretty straightforward.

[RalfJung]

🤷 I'm also fine either way, it'll just be a bunch of work to port the commits to the Miri repo.

I noticed that the C standard doesn't specify the output ranges for all of its mathematical operations; it just specifies them as:

Functions where C does not give an output range shouldn't get their value clamped, I would say.

[RalfJung]

I moved the "helpers" used for creating fixed outputs and clamping operations to their defined ranges to helpers.rs. These are now also extended to handle the floating-point operations in foreign_items. Tests in miri/tests/float.rs were changed/added.

Please don't, that file is already too big.^^

If the helpers are only needed in one file, keep them there.
Otherwise, add them in src/tools/miri/src/math.rs.

[LorrensP-2158466]

Reopening.

[LorrensP-2158466]

Functions where C does not give an output range shouldn't get their value clamped, I would say.

You're right, but this has some consequences. For example, the sin operation doesn't have an explicitly defined fixed output range, yet we guarantee and test this in Miri: rust-lang/miri#4207.

The C standard for the return values of sin is:

Returns
The sin functions return sin x.

The range of sine x is [-1, 1], but is not explicitly defined.

But asin has the following description:

Returns
The asin functions return arcsin x in the interval [−π/2, +π/2] radians.

I think we have 2 approaches:

• We say this is implementation-defined and revert all the clamps that are not explicitly defined
• We implicitly read the mathematically defined output ranges of those operations.

[tgross35]

If we run into libm implementations that can't even guarantee to return a value within the math function's output domain, tbh I would consider that downright broken and worthy of a bug report, or strong reason to just always use our libm on that platform. I'd be a bit hesitant to encourage users to think about this via Miri unless we think there is a chance this is actually a problem in practice (do we know of any platforms where this has been a problem?).

If it's mostly a concern about following the specification to the letter, I think it might be worth a defect report to see if the C committee is willing to codeify the output domain.

[RalfJung]

I think we have 2 approaches:

I would suggest a third:

• We do this kind of clamping wherever C mandates it, plus wherever it is easy and/or useful. So, fine to do it for sin and cos, but not for the gamma function ;)

[RalfJung]

But asin has the following description:

The arcsin function likely states this not as a means of guaranteeing precision, but because the inverse sine of x is under-defined -- infinitely many different inputs map to x (for x in [-1, 1]). By giving the interval, the answer becomes uniquely defined.

[LorrensP-2158466]

We do this kind of clamping wherever C mandates it, plus wherever it is easy and/or useful. So, fine to do it for sin and cos, but not for the gamma function ;)

Yeah, that sounds even better. I find them easy and useful atm.

[LorrensP-2158466]

If we run into libm implementations that can't even guarantee to return a value within the math function's output domain, tbh I would consider that downright broken and worthy of a bug report, or strong reason to just always use our libm on that platform. I'd be a bit hesitant to encourage users to think about this via Miri unless we think there is a chance this is actually a problem in practice (do we know of any platforms where this has been a problem?)

I don't think this happens in modern implementations and on modern systems. I mean, that would be really problematic as you said.

Also, during the development of this nondet behaviour, I always tested it without miri on my machine (Macbook m1) and I never encountered any weird things regarding the math functions. But there are a lot of platforms, so who knows...

If it's mostly a concern about following the specification to the letter, I think it might be worth a defect report to see if the C committee is willing to codeify the output domain.

Regardless of whether it happens or not (in these implementations/on these hardwares), I really don't like how the spec defines the output ranges of these operations. If an implementation only does what the spec explicitly defines, it can (in theory) implement sin to go beyond its mathematical range of [-1, +1] and still be conformant to the spec. Now, I am a noob in this field, but that's just my 2 cents 😄 .

[LorrensP-2158466]

@rustbot ready