f64::atan2 documentation error

[gantha-shiva]

Location

library/std/src/f64.rs:793

Summary

The f64::atan2 function documentation specifies that the output could be in the range (-PI, PI]. However its not true. It could return -PI as well.
Following is from the function documentation:

/// * `x = 0`, `y = 0`: `0`
/// * `x >= 0`: `arctan(y/x)` -> `[-pi/2, pi/2]`
/// * `y >= 0`: `arctan(y/x) + pi` -> `(pi/2, pi]`
/// * `y < 0`: `arctan(y/x) - pi` -> `(-pi, -pi/2)`

Example case:
f64::atan2(-0.0, -1.0) returns -f64::PI

[GrigorenkoPV]

From my testing, f32::atan2(y, x).is_sign_positive() == y.is_sign_positive(). I was even able to make kani prove that for the libm implementation.

use kani::*;

#[kani::proof]
fn nan() {
    let x: f32 = any();
    let y: f32 = any();
    assume(x.is_nan() || y.is_nan());
    let res = libm::atan2f(y, x);
    assert!(res.is_nan());
}

#[kani::proof]
fn atan2() {
    let x: f32 = any();
    assume(!x.is_nan());
    let y: f32 = any();
    assume(!y.is_nan());
    let res = libm::atan2f(y, x);
    assert!(res.is_finite());
    assert_eq!(res.is_sign_positive(), y.is_sign_positive());
    assert!(res <= core::f32::consts::PI);
    assert!(res >= -core::f32::consts::PI);
}

@rustbot claim

I think I'll put up a PR adjusting documentation.

[lolbinarycat]

triage: @GrigorenkoPV still planning on working on this?

also note that this should be updated for other float types too (f16, f32, and f128)

[GrigorenkoPV]

triage: @GrigorenkoPV still planning on working on this?

I do, but not sure when I will have time, so I should probably unclaim this for now.

@rustbot release-assignment

Also, I think the fix here is pretty easy: as I see it, one just needs to mention that the sign of the result is the same as the sign of the first argument, and that -0 & +0 both exist with floats and are two slightly different things.

So probably just specify the output ranges for four of the cases:
x >= +0, y >= +0
x <= -0, y >= +0
x >= +0, y <= -0
x <= -0, y <= -0

@rustbot label +E-easy

[whirlwindaster]

@rustbot claim