false positive: `a - b > b` is not really an underflow check

[cuviper]

In the original PR for overflow_check_conditional, I found this comment suggesting checks for subtraction: #741 (comment)

I agree with linting a - b > a -- there's no way for this to be true without underflow. You can also look at this algebraically, where this simplifies to 0 > b, which is nonsense for an unsigned type.

I disagree with linting a - b > b -- if you already know that a - b won't underflow (from a separate test or precondition), then this is a legitimate way of testing a > 2 * b, with the benefit of avoiding potential overflow in 2 * b.

One could alternately write this as a > b.saturating_mul(2) or a > b.saturating_add(b), but I tried this in one of my Project Euler solutions, and it was measurably slower. Even a raw a > 2 * b was slower than a - b > b!

Thoughts?

[cuviper]

The performance difference is a tangent, but FWIW I explored this in godbolt. I think the key is that my code wants to return b in a filter_map, and the sub version maintains this value while using one less register (no ecx). I guess this could make a difference to register pressure in the larger inlined context? Not sure...

[bootandy]

Your thoughts seems reasonable to me.

I also have a case where clippy marks:

if a + b < a {
    let new = a + b;
    // do something with `new`
}

But if I replace this with the following, as Clippy suggests:

let (new, overflow) = a.overflowing_add(b);
if !overflow {
    // do something with `new`
}

It actually changes the logic.

So yeah. I think something's wrong here.

I also have a case where clippy marks:

if a + b < a {
    let new = a + b;
    // do something with `new`
}

But if I replace this with the following, as Clippy suggests:

let (new, overflow) = a.overflowing_add(b);
if !overflow {
    // do something with `new`
}

It actually changes the logic.

So yeah. I think something's wrong here.

[Bubbler-4]

I also got this lint today by typing if r < n - r and was puzzled as to how it could be an overflow check at all. r < n - r is more expressive than other equivalents in my situation because r represents one choice and n - r represents another.