Missed optimization in bounds analysis in unsigned arithmetic that cannot underflow

[davidben]

Clang doesn't seem to be able to optimize the following out:

bool f(size_t a, size_t b) {
    __builtin_assume(a <= b);
    __builtin_assume(b <= PTRDIFF_MAX);
    // This can be deleted, because:
    //   1. 0 <= a <= b implies that b - a <= b
    //   2. b - a <= b <= PTRDIFF_MAX
    return b - a <= PTRDIFF_MAX;
}

https://godbolt.org/z/vzE7qb7Gb

I ran into this while exploring what combination of __builtin_assumes would dispatch some unnecessary assertions in std::string_view. (A separate bug while I'll file after this.)

[XChy]

Alive2: https://alive2.llvm.org/ce/z/vecDSc

[fhahn]

ConstraintElimination can simplify this, if the assumes are reordered: https://godbolt.org/z/jx5K7M7xq

At the moment it supports transferring some facts between unsigned & signed systems; but this depends on the order we visit facts at the moment, perhaps we can delay transferral until the first use?