[LLVMdev] RFC: Proposal for Poison Semantics

[Matthias Braun]

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

> On Jan 29, 2015, at 9:43 PM, Sanjoy Das <sanjoy at playingwithpointers.com> wrote:
> 
> 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
> 
>> On Thu, Jan 29, 2015 at 8:05 PM, Matthias Braun <matze at braunis.de> wrote:
>> 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
>> 
>>>> On Jan 29, 2015, at 11:29 AM, Sanjoy Das <sanjoy at playingwithpointers.com> wrote:
>>>> 
>>>> 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
>>> _______________________________________________
>>> LLVM Developers mailing list
>>> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
>>> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
> 
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu         http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev