Correctness of nsw/nuw and sext/zext in SCEV


I have been debugging and using SCEV for a while as it is so ubiquitous in loop analysis. However, what I am struggling with most is the proof of SCEV correctness when:

  1. There is nsw/nuw is in SCEV. I tried to find any reference about the correctness of sign wrap in SCEV, but did not find any paper that can explain it well. I understand that this is a known problem in llvm SCEV, but still hope to understand the original logic behind and find a way to verify it. So far what I learn most is from the source code and Sanjoy Das’s post ( The problem of source code is that I cannot verify if the code handles it correctly if I cannot test it with known good results, which makes any modification in SCEV scaring.

  2. SCEV of 32-bit induction variable needs to be extended to 64-bit. When a 64-bit range is needed, which I have encountered so often in 64-bit architecture, I think SCEV always uses zext, which I find it hard to digest since SCEV might not see how it is used later. For example, if the SCEV range is <%nb, +, 1>, wouldn’t %nb being negative cause problem with zext? This might be similar to

I am not really looking for a specific answer to a use case, but rather a way to verify the correctness of SCEV so that I can confidently say a certain behavior from existing code is expected or not. This is similar to using Alive in instruction combining. One closed solution I have found is Xilinx poster in eurollvm2019: “Scalar Evolution Canon: Click! Canonicalize SCEV and validate it by Z3 SMT solver!”, but not sure if it is ready to use.

Or if theoretical proof is not possible, at least certain consistency/assumptions can be maintained, like in a form of Wiki or llvm doc etc. To me, consistency is the most important as it is the only way to make problem reproducible.