[llvm-dev] 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 (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.
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.