[llvm] [VPlan] Use DIV nuw when optimizing latch exit user (PR #212292)
Florian Hahn via llvm-commits
llvm-commits at lists.llvm.org
Thu Jul 30 04:41:23 PDT 2026
https://github.com/fhahn commented:
> > I think it is still not quite right and it looks like there may be an Alive2 bug somewhere. If I delete the sceond set of functions, the first set of functions fails to verify: https://alive2.llvm.org/ce/z/Rra7Wu
> > The target function adds `nuw` to the increment, but the phi starts at -1, so will warp in the first iteration.
> > Also I think the proof would need to be the other way around: src should have increment with `nuw` + instruction sequence to compute the end value from the exit count as DerivedIV will be expanded, without NUW.
> > `tgt` should have `nuw` added to the sequence computing the final value as the new code would generate.
>
> Um, the first set of functions are supposed to fail, and fail in the original link as well. Yes, the difference is nuw on the exit value: totally missed that. Hopefully clearer, more general, and correct? https://alive2.llvm.org/ce/z/zDzViR
Ah right, not sure if the failing variant up front adds much. From the latest version, it is not clear how the preconditions (assumes) translate to the checks in the code which just require the AddRec to have NUW? Shouldn't the proof just have `nuw` on the IV increment on the source side? With that, I think the example which uses `iv + 2` does not verify, as iv + 1 is guaranteed to not wrap, but `iv + 2` may wrap?
https://github.com/llvm/llvm-project/pull/212292
More information about the llvm-commits
mailing list