[llvm-dev] Correctness of nsw/nuw and sext/zext in SCEV

[Jimmy Zhongduo Lin via llvm-dev]

Hi,

 

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 (https://www.playingwithpointers.com/blog/scev-integer-overflow.html). 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 http://llvm.1065342.n5.nabble.com/llvm-dev-SCEV-Why-is-backedge-taken-count-lt-nsw-gt-instead-of-lt-nuw-gt-td121335.html#a121345.

 

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.

 

Thanks,

Jimmy