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

[Valeriy Savchenko via llvm-commits]

SavchenkoValeriy wrote:

> > > > Alive2 struggles (times out) with 32 bit vectors for this particular proof: https://alive2.llvm.org/ce/z/S-78k- In my z3 proof, even 16 bit took quite some times.
> > > 
> > > 
> > > Please confirm if I shrunk the inputs correctly: https://alive2.llvm.org/ce/z/AABL4v (I guess you missed poison-generating flags in the source, as otherwise your target function is defined for a less pairs of inputs than the source.)
> > 
> > 
> > In your example, we can always infer that the result is < 65535 just because we are extending i8 to i32. The correct shrinking would include extending N / 4 to size N, but actually we can infer that the result is < 2^(N/2). Like this: https://alive2.llvm.org/ce/z/5A5mCg
> 
> Oh, you're right, missed that the sum fits N/2; so inferring nsw/nuw should make sense as the result will never overflow: https://alive2.llvm.org/ce/z/_rAdQg.

Exactly!

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