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 math.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]

Now that I think of it, did you mean without --keep-base?

[RalfJung]

No, --keep-base is fine. GH CI still checks your branch merged with latest master so I think the bot is a bit overeager here.

Thanks!
@bors r+

[bors]

📌 Commit 71add2f has been approved by RalfJung

It is now in the queue for this repository.

[Kobzol]

This (probably) caused non-deterministic failures on CI: #144787 (comment). I'll post a revert.

[LorrensP-2158466]

Weird how that one wasn't caught with many-seeds.

I'll run a much larger seed ranges this weekend to fetch them out. Or I can add the Miri constant to every approx_eq test.