llvm dev - Jan 2015 - [LLVMdev] RFC: Proposal for Poison Semantics

On 01/27/2015 09:38 PM, Sanjoy Das wrote:
>> if the definition of NUW is that zext-ing the result is equivalent to
>> zext-ing the inputs and doing the operation at a higher bitwidth (my
>> understanding), then %m and %n cannot hold those values, that would
violate
>> the NUW flag.
> The problem to solve is adequately defining "cannot hold".  In
the
> strictest sense, you could say if %m = %n = 2^31 - 1 then the program
> has UB; in effect defining "cannot hold" in the same way a
location
> you're loading from "cannot be" non-deferenceable.  But, as
David points
> out, that would mean you cannot hoist arithmetic with the nuw/nsw tags
> intact:
>
>    if (foo)
>     %t = add nuw X Y
>
> since it could be that (X != 2^32-1 && Y != 2^32-1) only if foo
=> true.  Arithmetic with no-wrap flags effectively are side-effecting
> operations in this scheme.
>
> The RFC tries to formalize a weaker notion of "cannot hold" that
> justifies treating arithmetic like arithmetic.  I'm trying to show
> that the notion of poison value in this RFC is too weak; and allows
> for certain programs to be well-defined (like the example I just
> showed) which change meaning in the face of transforms we'd like to be
> able to do.
I don't think your example is actually problematic.  The original 
program before your transformation *executed* undefined behavior in the 
form of '%x = add nuw i32 %m, %n' with "%m = %n = 2^32-1 (a.k.a 
INT_MAX)".  If I understand the c++ spec correctly, that implies that 
the meaning of this program is lost, even if the value of that 
instruction doesn't contribute to the output of the program.  We can 
produce any output for this program (or none, or wipe your hard drive) 
and it would be "correct".

To show a problem, you'd need to show a *well defined* program which 
becomes undefined through a series of transformations.  In your example, 
you might try the input program:

  br i1 %cnd, label %skip, label %exec
exec:
  %x1 = add nuw i32 %m, %n
  br label %skip
skip:
  %x  = phi (x1, 0)
  %y = zext i32 %x to i64
  %s = lshr i64 %y, 32
  %addr = gep %some_global, %s
  store i32 42, i32* %addr

But when the add is speculated, this becomes:

  %x1 = add nuw i32 %m, %n
  %x  = select i1 %cnd x1, 0
  %y = zext i32 %x to i64
  %s = lshr i64 %y, 32
  %addr = gep %some_global, %s
  store i32 42, i32* %addr

This is well defined as per the spec David sent out.  %x is not poison.  %x1 is,
but that's fine.

Philip



-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20150128/85639b0f/attachment.html>

> I don't think your example is actually problematic.  The original
program
> before your transformation *executed* undefined behavior in the form of
'%x
> = add nuw i32 %m, %n' with "%m = %n = 2^32-1 (a.k.a
INT_MAX)".  If I
I was trying to show why the rule "signed overflow is undefined
behavior" is problematic w.r.t. hoisting arithmetic by repeating an
argument David made in the first email on this thread.  That
particular example is not a counterexample to the RFC.

The RFC has issues with icmps, sexts and zexts; but they're distinct
from the hoisting problem.
>  %x1 = add nuw i32 %m, %n
>  %x  = select i1 %cnd x1, 0
>  %y = zext i32 %x to i64
>  %s = lshr i64 %y, 32
>  %addr = gep %some_global, %s
>  store i32 42, i32* %addr
>
> This is well defined as per the spec David sent out.  %x is not poison. 
%x1
> is, but that's fine.
AFAICT, going by the RFC, %x is poison iff %x1 is poison and %cond is true.

-- Sanjoy

On 01/28/2015 11:29 PM, Sanjoy Das wrote:
>> I don't think your example is actually problematic.  The original
program
>> before your transformation *executed* undefined behavior in the form of
'%x
>> = add nuw i32 %m, %n' with "%m = %n = 2^32-1 (a.k.a
INT_MAX)".  If I
> I was trying to show why the rule "signed overflow is undefined
> behavior" is problematic w.r.t. hoisting arithmetic by repeating an
> argument David made in the first email on this thread.  That
> particular example is not a counterexample to the RFC.
Er, I really don't get your point here.  This is a direct mapping of 
what the C++ spec says onto LLVM IR.  Can you clarify what you
mean?
>
> The RFC has issues with icmps, sexts and zexts; but they're distinct
> from the hoisting problem.
Can you enumerate?  Or give an example?
>
>>   %x1 = add nuw i32 %m, %n
>>   %x  = select i1 %cnd x1, 0
>>   %y = zext i32 %x to i64
>>   %s = lshr i64 %y, 32
>>   %addr = gep %some_global, %s
>>   store i32 42, i32* %addr
>>
>> This is well defined as per the spec David sent out.  %x is not poison.
%x1
>> is, but that's fine.
> AFAICT, going by the RFC, %x is poison iff %x1 is poison and %cond is true.
You're correct; I was sloppy in my wording.  What I should have said was 
that %x is poison exactly when the original program would have executed 
undefined behaviour.  If the original program was well defined (and thus 
%cnd is false), %x is not poison.  That seems like exactly what we want.

Philip