llvm dev - Jan 2020 - Correctness of nsw/nuw and sext/zext in SCEV

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20200124/0de88e01/attachment.html>