<div dir="ltr">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.</div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Jan 29, 2015 at 10:14 PM, Sanjoy Das <span dir="ltr"><<a href="mailto:sanjoy@playingwithpointers.com" target="_blank">sanjoy@playingwithpointers.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Here's an idea for a slightly unusual framework for poison semantics:<br>
we do it in two steps --<br>
<br>
<br>
1. for every bit in the program, we define a second "shadow bit",<br>
is-poison.  We define the semantics of LLVM IR using this is-poison<br>
relation.  So, for instance, we could say if there is a bit 'b'in<br>
address 'a' such that if is-poison['b'], then "store X to 'a'" is<br>
undefined behavior.<br>
<br>
2. we prove that there is no need to track is-poison for a<br>
well-defined program.  IOW, any program whose evaluation will actually<br>
require us to do the book-keeping for is-poison will eventually run<br>
into undefined behavior.<br>
<br>
I think such an approach will explicitly address the issue that we're<br>
using an N bit value to track 2^N+1 possibilities.  And this is also a<br>
sanity check -- since the is-poison relation is clearly made up and<br>
does not *really exist*, if we cannot prove (2) then we did something<br>
wrong in specifying step (1).<br>
<br>
-- Sanjoy<br>
<br>
<br>
On Thu, Jan 29, 2015 at 10:05 PM, Sanjoy Das<br>
<div class="HOEnZb"><div class="h5"><<a href="mailto:sanjoy@playingwithpointers.com">sanjoy@playingwithpointers.com</a>> wrote:<br>
> On Thu, Jan 29, 2015 at 10:01 PM, Matthias Braun <<a href="mailto:matze@braunis.de">matze@braunis.de</a>> wrote:<br>
>> But<br>
>> (Poison > INT_MAX) <=> poison<br>
>> contradicts<br>
>> (X > INT_MAX) <=> false<br>
>><br>
>> and I don't think you want to abandon the second rule just because x might be poison.<br>
><br>
> Maybe we could define poison in such a way that it is safe to pretend<br>
> it "is" false, as per our convenience.  In this sense, could be<br>
> defined to be very similar to undef.<br>
><br>
> -- Sanjoy<br>
><br>
>><br>
>> - Matthias<br>
>><br>
>>> On Jan 29, 2015, at 9:43 PM, Sanjoy Das <<a href="mailto:sanjoy@playingwithpointers.com">sanjoy@playingwithpointers.com</a>> wrote:<br>
>>><br>
>>> One way around this is to say that there are some special<br>
>>> instructions, icmp, sext and zext which produce a value solely<br>
>>> composed of poison bits if any of their input bits is poison.  So<br>
>>> `<poison> icmp X` is poison for any value of X, including INT_MAX.<br>
>>> This is one way poison could be fundamentally different from undef.<br>
>>><br>
>>> -- Sanjoy<br>
>>><br>
>>>> On Thu, Jan 29, 2015 at 8:05 PM, Matthias Braun <<a href="mailto:matze@braunis.de">matze@braunis.de</a>> wrote:<br>
>>>> Having though about this some more I think optimizing<br>
>>>><br>
>>>> (x+1 > x) <=> true<br>
>>>><br>
>>>> and at the same time modeling undefined behavior as a posion value is impossible. This is because we also want the following rule:<br>
>>>><br>
>>>> (x > INT_MAX) <=> false<br>
>>>><br>
>>>> Now if poison is a value, then the second replacement tells us (poison > INT_MAX) == false which contradicts the first rule.<br>
>>>><br>
>>>><br>
>>>><br>
>>>> 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.<br>
>>>><br>
>>>> 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”...<br>
>>>><br>
>>>> - Matthias<br>
>>>><br>
>>>>>> On Jan 29, 2015, at 11:29 AM, Sanjoy Das <<a href="mailto:sanjoy@playingwithpointers.com">sanjoy@playingwithpointers.com</a>> wrote:<br>
>>>>>><br>
>>>>>> I've been discussing a model with David that might steer poison back towards<br>
>>>>>> something that simply supports algebraic simplification. If we have a math<br>
>>>>>> operation that cannot wrap, then it notionally produces as many bits of<br>
>>>>>> undef as the operation could possibly produce. For example, "add nsw i8" can<br>
>>>>>> produce an i9 undef, and "mul nsw i8" can produce an undefined 16 bit<br>
>>>>>> bitpattern. This is strong enough to do things like "a + 1 > a  -->  true",<br>
>>>>>> because on overflow of "a + 1" we can choose an poison value of "MAX_INT +<br>
>>>>>> 1", even though that is not a valid i8 bit pattern.<br>
>>>>>><br>
>>>>>> So, a short version would be that poison is like undef, except you get to<br>
>>>>>> include the overflow bits of the computation in your undef value.<br>
>>>>><br>
>>>>> I  suspect it will be hard to justify reg2mem is meaning preserving in<br>
>>>>> this scheme.  But if this can be made to work, then I agree that this<br>
>>>>> is the right thing to do -- an i32 poison effectively has the<br>
>>>>> semantics of a wider type, and it makes sense to be explicit in that.<br>
>>>>><br>
>>>>> -- Sanjoy<br>
>>>>> _______________________________________________<br>
>>>>> LLVM Developers mailing list<br>
>>>>> <a href="mailto:LLVMdev@cs.uiuc.edu">LLVMdev@cs.uiuc.edu</a>         <a href="http://llvm.cs.uiuc.edu" target="_blank">http://llvm.cs.uiuc.edu</a><br>
>>>>> <a href="http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev</a><br>
>>><br>
>>> _______________________________________________<br>
>>> LLVM Developers mailing list<br>
>>> <a href="mailto:LLVMdev@cs.uiuc.edu">LLVMdev@cs.uiuc.edu</a>         <a href="http://llvm.cs.uiuc.edu" target="_blank">http://llvm.cs.uiuc.edu</a><br>
>>> <a href="http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev</a><br>
<br>
_______________________________________________<br>
LLVM Developers mailing list<br>
<a href="mailto:LLVMdev@cs.uiuc.edu">LLVMdev@cs.uiuc.edu</a>         <a href="http://llvm.cs.uiuc.edu" target="_blank">http://llvm.cs.uiuc.edu</a><br>
<a href="http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev" target="_blank">http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev</a><br>
</div></div></blockquote></div><br></div>