[llvm] [DAGCombiner][X86] Correctly clean up high bits in `combinei64TruncSrlAdd` (PR #128353)

[Yingwei Zheng via llvm-commits]

dtcxzyw wrote:

> > A counterexample for original implementation: https://alive2.llvm.org/ce/z/YowPZY
> > We should keep low `64 - shamt` bits instead of `shamt - 32`.
> > Proof: https://alive2.llvm.org/ce/z/z_jdHD
> 
> The alive2 just proves the problem in calculation of NewAddConstVal, but is the problem in #128309 actually caused by zext vs. anyext?

Yeah, the original issue can be fixed by using zext instead of anyext. But alive2 still complains about the correctness, so I have to fix the number of low bits that should be kept.

> I was worrying the correctness, but don't know how to prove it. Do you have any idea how to prove the problem of https://github.com/llvm/llvm-project/issues/128309 with alive2?

We can hardcode c2 into the type and divide anyext into sext+zext (2 pairs): https://alive2.llvm.org/ce/z/7ieYLg


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