I will second this request for much the same reason.
I'm going to try to compare the proposed semantics of poison with undef. This may be completely wrong, but I'm hoping the corrections will help clarify the semantics.
Begin attempt:
poison is similar to undef in that the optimizer is free to assume any value for the poison bits in an *input* to an instruction. Where it differs is that bits in the *output* which are not "entirely controlled by a non-poison input bit" are *also* poison.
This is different from undef in that there may be bits in the output whose values would be known for *any* specific value chosen for the poison input. For undef, these bits would not be undef and would instead be known. For poison, these bits are unconditionally poison.
(I'm having a hard time finding an example for this part; this implies it probably isn't true.)
Similarly, the choice of domain of input choices may restrict the output of an instruction when supplied undef. Such restrictions do not apply when the input is poison.
The simplest example of this difference might be:
%2 = sext i1 %1 to i32
If %1 is undef, the %2 can take only two values: all zeros, or all ones.
If %1 is poison, all bits of %2 are poison. %2 can thus take *any* value representable by an i32.
Note however that given a zext on the same input, 31 of the output bits would be defined in either case. Only the last bit would be either undef or poison depending. Note that the distinction between the two is important here in that it may influence propagation in later instructions.
To phrase these two differently, undef must take a specific value (or set of values) on input to an instruction. The only legal outputs are those which can result from all such values. Poison does not need to take a specific value and propagates to any output bit which is influenced by the value of a poison input.
If we follow the RFC, the following program has UB if X is poison but is well defined if X is undef:
%loc = select i1 X, %global0, %global1
store 42 to %loc
(Assuming both global0 and global1 can be legally stored to and are different locations.)
– Sanjoy
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-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:
undef xor undef == 0 but poison xor poison == poison ?
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* %addrThis 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
undef isn't strong enough to perform the simplification "a + 1 > a -->
true" for an nsw add.
If we use undef instead of poison, "a + 1" will produce undef iff a is
MAX_INT, but we cannot choose a bit-pattern for the undef result that is
greater than MAX_INT. In other words, as David said, the comparison "icmp
gt i32 undef, MAX_INT" is always true, just as "and i32 undef, 0" always
produces 0.
I've been discussing a model with David that might steer poison back
towards something that simply supports algebraic simplification. If we have
a math operation that cannot wrap, then it notionally produces as many bits
of undef as the operation could possibly produce. For example, "add nsw i8"
can produce an i9 undef, and "mul nsw i8" can produce an undefined 16 bit
bitpattern. This is strong enough to do things like "a + 1 > a --> true",
because on overflow of "a + 1" we can choose an poison value of "MAX_INT +
1", even though that is not a valid i8 bit pattern.
So, a short version would be that poison is like undef, except you get to
include the overflow bits of the computation in your undef value.
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 II 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* %addrThis 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
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 II 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?
I mean if the specification of nsw (say) in LLVM is "add nsw X Y" is
undefined behavior if the addition overflows, then we cannot hoist
additions through control flow since we could be introducing undefined
behavior that wasn't present in the original program. Hence it is
undesirable to state "add nsw X Y has UB if the addition overflows".
The RFC does not formalize nsw this way, so this is not a problem with
the RFC.
Can you enumerate? Or give an example?
I've given (counter-)examples for all of these in previous emails:
[zext] http://lists.cs.uiuc.edu/pipermail/llvmdev/2015-January/081321.html
+ http://lists.cs.uiuc.edu/pipermail/llvmdev/2015-January/081322.html
[sext] http://lists.cs.uiuc.edu/pipermail/llvmdev/2015-January/081316.html
[icmp] http://lists.cs.uiuc.edu/pipermail/llvmdev/2015-January/081312.html
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.
Yes, this RFC does the right thing in this case.
-- Sanjoy
I've been discussing a model with David that might steer poison back towards
something that simply supports algebraic simplification. If we have a math
operation that cannot wrap, then it notionally produces as many bits of
undef as the operation could possibly produce. For example, "add nsw i8" can
produce an i9 undef, and "mul nsw i8" can produce an undefined 16 bit
bitpattern. This is strong enough to do things like "a + 1 > a --> true",
because on overflow of "a + 1" we can choose an poison value of "MAX_INT +
1", even though that is not a valid i8 bit pattern.So, a short version would be that poison is like undef, except you get to
include the overflow bits of the computation in your undef value.
I suspect it will be hard to justify reg2mem is meaning preserving in
this scheme. But if this can be made to work, then I agree that this
is the right thing to do -- an i32 poison effectively has the
semantics of a wider type, and it makes sense to be explicit in that.
-- Sanjoy
Having though about this some more I think optimizing
(x+1 > x) <=> true
and at the same time modeling undefined behavior as a posion value is impossible. This is because we also want the following rule:
(x > INT_MAX) <=> false
Now if poison is a value, then the second replacement tells us (poison > INT_MAX) == false which contradicts the first rule.
The only way out of this while still allowing (x+1>x)<=>true I can see at the moment is defining that add nsw does produce actual undefined behavior allowing us to “freely rewrite" the following > to true in the UB cases. Of course having add produce actual undefined behaviour greatly limits us in the way we can actually move the instruction around without changing program semantics.
The only way allowing moving instructions and having add produce real UB I can see is that as soon as we start moving instructions around (specifically moving the add to a place it does not dominate or moving any other instruction over the add) we change the add to an instruction that does not produce real UB anymore; something like add swu = “add signed wrap gives undef”...
- Matthias
One way around this is to say that there are some special
instructions, icmp, sext and zext which produce a value solely
composed of poison bits if any of their input bits is poison. So
`<poison> icmp X` is poison for any value of X, including INT_MAX.
This is one way poison could be fundamentally different from undef.
-- Sanjoy
But
(Poison > INT_MAX) <=> poison
contradicts
(X > INT_MAX) <=> false
and I don't think you want to abandon the second rule just because x might be poison.
- Matthias
But
(Poison > INT_MAX) <=> poison
contradicts
(X > INT_MAX) <=> falseand I don't think you want to abandon the second rule just because x might be poison.
Maybe we could define poison in such a way that it is safe to pretend
it "is" false, as per our convenience. In this sense, could be
defined to be very similar to undef.
-- Sanjoy
Here's an idea for a slightly unusual framework for poison semantics:
we do it in two steps --
1. for every bit in the program, we define a second "shadow bit",
is-poison. We define the semantics of LLVM IR using this is-poison
relation. So, for instance, we could say if there is a bit 'b'in
address 'a' such that if is-poison['b'], then "store X to 'a'" is
undefined behavior.
2. we prove that there is no need to track is-poison for a
well-defined program. IOW, any program whose evaluation will actually
require us to do the book-keeping for is-poison will eventually run
into undefined behavior.
I think such an approach will explicitly address the issue that we're
using an N bit value to track 2^N+1 possibilities. And this is also a
sanity check -- since the is-poison relation is clearly made up and
does not *really exist*, if we cannot prove (2) then we did something
wrong in specifying step (1).
-- Sanjoy
So far, this is the model I like the best, but I do still have some concern.
The primary concern I have is that with this model, zext is no longer 100%
equivalent to anyext + mask. Much like you say, you *could* implement zext
that way, but once you convert them, the poison is lost.
Maybe that's OK though. I'm curious what others think. I haven't really had
enough time to fully explore this in my head.
This is actually how i tend to think of poison – it is undef, plus a shadow bit indicating the bits are poison. I think the important this is defining how the various operations propagate poison, why, and why not.
> Ah, yes. You are right, we cannot always assume that %y would be zero in
> the second case.
> This wouldn't be the first time we've lost information that we could use
to
> optimize a program by transforming it.
>
> Do you think this result would be problematic? It seems consistent with
the
> RFC and LLVM's current behavior.
>The problem is not that we're losing information, the problem is that
we're changing the behavior of a well-defined program.I'll try to put the whole argument in one place:
We start with
%x = add nuw i32 %m, %n
%y = zext i32 %x to i64
%s = lshr i64 %y, 32
%addr = gep %some_global, %s
store i32 42, i32* %addrIn the above program, for all values of %x, %s is 0. This means the
program is well-defined when %x is poison (since you don't need to
look at %x to determine the value of %addr, in the same sense as you
don't need to look at X to determine the value of "and X, 0"); and it
stores 42 to &(%some_global)[0]. Specifically, the above program is
well defined for "%m = %n = 2^32-1".Now if we do the usual transform of "zext (add nuw X Y)" => "add nuw
(zext X) (zext Y)" then we get%m.wide = zext i32 %m to i64
%n.wide = zext i32 %n to i64
%z = add nuw i64 %m.wide, %n.wide
%s = lshr i64 %y, 32
%addr = gep %some_global, %s
store i32 42, i32* %addrThe new program does *not* have the same behavior as the old program
for "%m = %n = 2^32-1". We have changed the behavior of a
well-defined program by doing the "zext (add nuw X Y)" => "add nuw
(zext X) (zext Y)" transform.
After some pondering and combing through LLVM's implementation, I think we
must conclude that zexting a value with any poison bits creates poison in
every new bit.
Considering the following program:
%zext = zext i32 %x to i64
%icmp = icmp i64 %zext, i64 1
we'd like to transform this to:
%icmp = icmp i32 %x, i32 1
Is it reasonable to say that '%icmp' in the before case is not poison but
'%icmp' in the after case is poison? LLVM assumes it can remove casts with
impunity, I think this is a useful property to maintain.
FWIW, I agree with your statement.
Here is the line of reasoning that I find troubling.
If we accept the above, we have a surprising result (using small bit-width
integers to make it easier to read)
%zext = zext i1 %x to i2
%and = and i2 %zext, 1
We cannot replace %and with %zext because the %and might be removing poison.
Perhaps this restriction is OK though. I just find it somewhat troubling.
I don’t know how things work at the moment, but it seems to me that you can do lots of sensible things, and avoid lots of silly things, if you keep track of four possible values for each bit:
- undef (the default)
- poison
- known to be 0
- known to be 1
This makes both David’s and Chandler’s examples work nicely if you assume:
- ZEXT makes all the new bits known 0
- SEXT makes all the new bits the same as the high bit
- AND clears unknown and poison bits to known 0 if the other input is known 0
- OR sets unknown and poison bits to known 1 if the other input is known 1
Also things such as ZEXTing a poison i32 to i64 and then right shifting by 32 will result in all known 0 bits.