[llvm] [DemandedBits] Support non-constant shift amounts (PR #148880)

Panagiotis Karouzakis via llvm-commits llvm-commits at lists.llvm.org
Mon Jul 21 04:54:11 PDT 2025


karouzakisp wrote:

> > > > my transformation contains a loop and the Alive syntax doesn't permit loops
> > > 
> > > 
> > > You can use a smaller integer bitwidth (e.g., i4/i8), then unroll the loop with `-src-unroll=8 -tgt-unroll=8`.
> > 
> > 
> > Thanks for the tip. Here is the updated proof --> https://alive2.llvm.org/ce/z/tCvUT6
> 
> In your proof, the range of shamt is not taken into account. Updated: https://alive2.llvm.org/ce/z/n4hgkX ~Can you please add proofs for shl nsw/shl nuw/lshr/lshr exact/ashr/ashr exact?~ Can you please add proofs for lshr/ashr? Then you should paste the links into the PR description.

Thanks for the help.

I just added the proofs for lshr and ashr. Also, I updated the cpp code.

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


More information about the llvm-commits mailing list