[PATCH] ScalarEvolution incorrectly assumes that the start of certain add recurrences don't overflow

hfinkel at anl.gov hfinkel at anl.gov
Fri Feb 6 23:12:23 PST 2015

In http://reviews.llvm.org/D7331#120174, @sanjoy wrote:

> > (where you also need to make sure that both are not nullptr). If the exit block is also the latch block, then there is no early-exit problem.
> It depends on how you interpret poison semantics -- if you pretend that an `add nsw` "cannot" overflow then the above is sufficient.  But if you interpret poison to cause UB when you *use* the poison, then the above condition is not enough:  you could exit from the latch block in the first iteration, ...
> All of this reasoning is shaky because currently LLVM does not have a consistent semantics for poison.  We may have to revisit this reasoning once it does :)

Here's what I'd like to do:

1. For now, let's stick with your strongest interpretation, and assume the local check is sufficient.
2. Add a loud WARNING comment explaining that the check is only correct if we assume the overflow cases of nsw are unreachable.
3. Bring up this example in the llvmdev thread discussing poison semantics

FWIW, I believe that the strong interpretation is consistent with a confirming implementation of C++, for example, which allows a program to trap upon encountering undefined behavior (1.3.24), and overflowing an integer operation is undefined behavior (5p4); there is no requirement that the result be used in order for undefined behavior to result.



More information about the llvm-commits mailing list