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

[Phoebe Wang via llvm-commits]

phoebewang 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?

We had discussions regarding eliminating `movz` in https://github.com/llvm/llvm-project/pull/126448#discussion_r1953735330
I was worrying the correctness, but don't know how to prove it. Do you have any idea how to prove the problem of #128309 with alive2?

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