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

[Valeriy Savchenko via llvm-commits]

SavchenkoValeriy wrote:

> > > Can you please provide a generalized alive2 proof? See https://llvm.org/docs/InstCombineContributorGuide.html#proofs.
> > 
> > 
> > I believe I answered it here: [#166378 (comment)](https://github.com/llvm/llvm-project/pull/166378#issuecomment-3487318866)
> > In short, I'm not improving any particular transformation but an analysis and analysis can't be proven via alive2. I provide a general z3 proof for the exact logic that I encoded. Please tell me if you have any questions about that proof.
> 
> z3 proof is ok. But you have to handle poison stuff yourself (e.g., `sub nuw`) to ensure your code matches the proof. It is also a burden for reviewers to check your proof. With Alive2 we can also check if additional poison-generating flags on adds/muls provide a better estimation of knownbits.

With the Alive2 proof it's also not fully true again because I need to prove the analysis and not the transformation.
In any case, something like this can be used for `sub nuw` https://alive2.llvm.org/ce/z/5egb4W and for `xor` https://alive2.llvm.org/ce/z/F45enJ proving the maximum property. Leading zeros property of unsigned maximum is, however, trivial enough. Please tell me if that works for you and is enough.

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