[llvm] [SCEV] Add non-poison/non-zero checks on denominators (PR #117152)

[Yingwei Zheng via llvm-commits]

dtcxzyw wrote:

> If I understand correctly, you're basically trying to add the invariant that simplification of SCEV expressions must preserve undefined behavior.

Yeah. For this case, `ScalarEvolution::createAddRecFromPHI` only checks `initval == refine(f(0))`. It doesn't imply `initval == f(0)`.

> I think the problem here is rather in that particular addrec construction code. We basically have a derefinement issue here, similar to what we see in select simplification.

Do we need an `AllowRefinement` argument for SCEV constructors and disallow refinement in these rewriters?


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