[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

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