[llvm] [ValueTracking] Refine known bits for linear interpolation patterns (PR #166378)

[Valeriy Savchenko via llvm-commits]

SavchenkoValeriy wrote:

> > Since that is true for arbitrary a, b, c and d within our constraints, we can
> > conclude that:
> > max(a * (b - c) + c * d) <= max(max(a), max(d)) * max(b) = U
> 
> Would it be possible to add an Alive2 proof for the conclusion?

That's a great point and I believe that such statements should be proven. However, I'd disagree that Alive2 is the best tool for this particular change.

Alive2 proves individual transformations and I will provide Alive2 proofs for the tests that I added. Since I added a more general known bits calculation that in theory can work well with one transformation but not the other, I wrote a z3 proof to show that inferred known bits are correct: https://gist.github.com/SavchenkoValeriy/a7d3e40868b9d512a70260ae63d8413b

https://github.com/llvm/llvm-project/pull/166378