[llvm-dev] RFC: Killing undef and spreading poison

[Sanjoy Das via llvm-dev]

Hi,

On Thu, Jun 8, 2017 at 12:29 PM, Peter Lawrence
<peterl95124 at sbcglobal.net> wrote:
>
> Sanjoy,
>             in your blog post
> https://www.playingwithpointers.com/problem-with-undef.html
> you describe a problem with LLVM “undef”,
> yet in your paper http://www.cs.utah.edu/~regehr/papers/undef-pldi17.pdf
> you do not suggest fixing this problem, even though in chpt. 9 you identify
> other
> compilers that do attempt to avoid it.

That problem is mentioned in section 3.2 (which quotes the same
example as in the blog post), and section 4 (the paragraph starting
with "Defining branching on poison to be UB further enables analyses
to assume that...") addresses how the new semantics plugs this gap.

> The reason I keep asking for additional examples is that this one where
> You have illegally transformed the ‘nsw’ isn’t convincing. So please,

Maybe we're talking past each other.  Let me first discuss the framing
of the problem as I see it:

 1. Whether a transform is illegal or not is decided by the semantics
    we've assigned to the IR.  In this case, whether hoisting the
    multiplication with the nsw intact is illegal or not is decided by
    the semantics we've assigned to nsw.

 2. We want certain transforms to be legal, which limits the kinds of
    semantics we can possibly have for the IR.  For instance, we
    certainly don't want a semantics for IR that disallows constant
    folding `add i32 1, 2`.

The example I gave was to demonstrate why the current (albeit not very
clearly specified) semantics is incorrect.

So when you ask for an example, are you asking why the set of
transforms we want to be correct in the new semantics (i.e. (2))
includes "hoist nsw-arithmetic out of control flow while still keeping
the flags"?  IOW, in the language used in the paper I linked to, are
you asking "why can't we have a overflowing nsw addition be immediate
UB"?  If so, that is covered in section 2.2 (but we can get into more
detail if you want).

-- Sanjoy