[llvm-dev] Does poison add implicit "definedness" under the hood ?

[Juneyoung Lee via llvm-dev]

I think it is slightly different, let me explain the reason.

Lowering `z = add nsw x, y` into the following assembly is valid, but `z =
add x, y` into this isn't.

if (x + y overflows)
  z = 0;
else
  z = ADD x y

Lowering `z = add x, y` should be more 'precise'.
Instead of storing zero, 2's complement of x + y should be stored. This can
be more expensive.

Juneyoung

On Fri, Oct 30, 2020 at 5:13 AM Stefanos Baziotis <
stefanos.baziotis at gmail.com> wrote:

> Hi Juneyoung,
>
> > Okay, previously I was assuming that P has two kinds of additions
> (trapping add & silent add).
> > Maybe this isn't true, and P always traps when overflow happens? I hope
> my understanding is correct now.
>
> Exactly, P has only one add that explodes on overflow. (btw just to be
> clear, the point is
> not P - P was just introduced as an example to showcase the implicit
> semantics that poison adds).
>
> I think I understood most of what you said above. My point was not so much
> nsw vs dropping nsw but in
> any case, IIUC, dropping nsw is only bad since it only disables using
> arithmetic properties and their
> codegen is the same.
>
> > If we keep `add nsw` poison, lowering `add nsw` needs check, but the
> generated code is slightly different from `add`:
> > ...
> I'd think that this is the codegen of both `add nsw` and simply `add`.
> They both have to check whether there is overflow.
>
> > In case of `add x, y` without nsw, z should be 2's complement otherwise.
> I'm not sure I got that, but if P only supports 2's complement arithmetic
> anyway, that means that the codegen of the two (`add` and `add nsw`)
> is identical right ?
>
> Thanks again,
> Stefanos
>
> Στις Πέμ, 29 Οκτ 2020 στις 7:49 μ.μ., ο/η Juneyoung Lee <
> juneyoung.lee at sf.snu.ac.kr> έγραψε:
>
>> Okay, previously I was assuming that P has two kinds of additions
>> (trapping add & silent add).
>> Maybe this isn't true, and P always traps when overflow happens? I hope
>> my understanding is correct now.
>>
>>
>> There is `add` without nsw in IR, and the backend should still put
>> overflow check when lowering it.
>> If `add nsw` raises UB, dropping `nsw` from `add` will make the
>> instruction more costly, so optimizations that drop nsw should be done more
>> carefully.
>>
>>
>> If we keep `add nsw` poison, lowering `add nsw` needs check, but the
>> generated code is slightly different from `add`:
>>
>> // Assume that we're lowering `z = add nsw x, y` in IR into P's assembly
>> if (x + y overflows)
>>   z = garbage value; // the backend can choose which value to put here
>> else
>>   z = x + y; // never traps
>>
>> In case of `add x, y` without nsw, z should be 2's complement otherwise.
>>
>> In perspective of optimizations, `add nsw` is still different from `add`
>> because it allows simplifying more expressions using arithmetic properties.
>> But, dropping nsw will make the instruction expensive (as the UB case),
>> so it should be carefully done as well.
>>
>>
>> If clang explicitly inserts the overflow check in IR (either in if or
>> llvm.assume), I think that can be a good hint for code generation.
>> Code motion of adds should be more carefully done though, because the
>> hint might be missed.
>>
>> Juneyoung
>>
>> On Thu, Oct 29, 2020 at 7:21 PM Stefanos Baziotis <
>> stefanos.baziotis at gmail.com> wrote:
>>
>>> Hi Juneyoung,
>>>
>>> I think I lost you in your last example. First, I'm not sure if this
>>> last C code corresponds to LLVM IR code or after-LLVM-IR code. Assuming
>>> that we're talking about LLVM IR and for my imaginary platform P:
>>> The checking for overflow is not something that we have to do in LLVM
>>> IR, since as outlined in my previous email, LLVM IR has added the semantics
>>> that
>>> signed overflow does not explode / trap (because if it didn't add these
>>> semantics, additions that exploded and which did not happen in the original
>>> program will happen now etc.). It is the lowering of LLVM IR that has to
>>> add it.
>>>
>>> So, AFAIU, the "timeline" looks like this:
>>>
>>> -- Before (LLVM IR):
>>> for(i < n) {
>>>   y = add nsw x + 1  <-- notice: no check, we don't need to do it,
>>> semantics say it doesn't trap
>>>   use(y)
>>> }
>>> -- After (LLVM IR):
>>> int tmp = add nsw x + 1;  <-- still no check..
>>> for(i < n) {
>>>   y =  tmp;
>>>   use(y)
>>> }
>>>
>>> Now, we get that after and go ahead to lower it (i.e. after-LLVM-IR,
>>> back-end work). I'll actually try to do a better job than
>>> my original email:
>>>
>>> int tmp;
>>> if (x != INT_MAX)  <-- notice the !=. This check is to _guarantee_ that
>>> the addition won't explode / trap since if that happened, it would violate
>>> the semantics, that we implicitly added, of LLVM IR.
>>>   tmp = add nsw x + 1;
>>> for(i < n) {
>>>   y =  tmp;
>>>   use(y)
>>> }
>>>
>>> So this (your example):
>>> for(i < n) {
>>> if (x == INT_MAX)
>>>   trap
>>> y = add nsw x + 1
>>> use(y)
>>> }
>>> =>
>>> y = add nsw x + 1 // hoisted
>>> for(i < n) {
>>> if (x == INT_MAX)
>>>   trap
>>> use(y)
>>> }
>>>
>>> does not make sense to me either in the LLVM IR level or in the
>>> after-LLVM-IR level. For the former, it doesn't make sense since I don't
>>> see why we have to do the check inside the loop;
>>> the semantics mandate that it doesn't happen so we're ok, the burden is
>>> on the back-end. For the latter (i.e. we're in LLVM IR lowering, ISel or
>>> smth), we simply can't hoist this add outside without a check
>>> since if x == INT_MAX, the platform P will explode _immediately_, no
>>> matter what the value of `n` (and of course, if `n == 0`, the original code
>>> wouldn't explode).
>>>
>>> Do I miss something ?
>>> Guess: I think that what I miss is this: The semantics we added is not
>>> that signed wrapping won't explode. Rather: It does not explode _if it is
>>> not used in one of the X ways_. That would justify
>>> your example transformation in the LLVM IR level.
>>>
>>> I hope this was not confusing, thanks for your time!
>>>
>>> - Stefanos
>>>
>>>
>>> Στις Πέμ, 29 Οκτ 2020 στις 4:29 π.μ., ο/η Juneyoung Lee <
>>> juneyoung.lee at sf.snu.ac.kr> έγραψε:
>>>
>>>> Hi Stefanos,
>>>>
>>>> So, to justify this transformation as correct, implicitly, poison has
>>>>> _added definedness_ to signed wrapping: specifically, that the
>>>>> computer won't explode if SW happens. AFAIU, that is ok as far as C++
>>>>> semantics
>>>>> are concerned:
>>>>> Since signed wrapping was UB, making it more defined is ok.
>>>>
>>>>
>>>> Your understanding is correct. Since signed overflow is UB in C/C++,
>>>> lowering from C to IR can make such programs more defined.
>>>>
>>>> Instead, they have to lower it as something like:
>>>>> if (x == INT_MAX)
>>>>>   skip or whatever
>>>>
>>>>
>>>> Yes.
>>>> This means that the overflow check and the actual add operation can be
>>>> separated. This requires instruction selection to carefully combine the
>>>> check and add, but for optimization this is beneficial because add can
>>>> still be freely moved.
>>>>
>>>> for(i < n) {
>>>> if (x == INT_MAX)
>>>>   trap
>>>> y = add nsw x + 1
>>>> use(y)
>>>> }
>>>> =>
>>>> y = add nsw x + 1 // hoisted
>>>> for(i < n) {
>>>> if (x == INT_MAX)
>>>>   trap
>>>> use(y)
>>>> }
>>>>
>>>> Juneyoung
>>>>
>>>> On Thu, Oct 29, 2020 at 5:56 AM Stefanos Baziotis <
>>>> stefanos.baziotis at gmail.com> wrote:
>>>>
>>>>> Hi Juneyoung,
>>>>>
>>>>> First of all, great job on your talk!
>>>>>
>>>>> This is a question I guess you'd be the best person to answer but the
>>>>> rest of the LLVM community might want to participate.
>>>>>
>>>>> I was thinking about a UB-related example that has been discussed by
>>>>> multiple people
>>>>> (including you), all of them basically authors of this paper (
>>>>> https://www.cs.utah.edu/~regehr/papers/undef-pldi17.pdf):
>>>>>
>>>>> -- Before opt:
>>>>> for (int i = 0; i < n; ++i) {
>>>>>   a[i] = x + 1;
>>>>> }
>>>>>
>>>>> -- After opt (LICM):
>>>>> int tmp = x + 1;
>>>>> for (int i = 0; i < n; ++i) {
>>>>>   a[i] = tmp;
>>>>> }
>>>>> // Assume `tmp` is never used again.
>>>>>
>>>>> The reasoning here, is let's make signed wrapping _deferred_ UB that
>>>>> will only
>>>>> occur if the value is used in one of X ways (e.g. as a denominator).
>>>>> To that end, if
>>>>> n == 0 and x == INT_MAX, UB will never occur because the value is
>>>>> never used.
>>>>>
>>>>> But, by doing that, the first point is:
>>>>> If we translate this into machine code, the signed wrapping _will_
>>>>> happen, no matter
>>>>> the value won't be used.
>>>>>
>>>>> Now, imagine that on some platform P, signed wrapping explodes the
>>>>> computer.
>>>>> The computer _will_ explode (should explode ? more on that later)
>>>>> even if `n == 0`, something that would not happen in the original code.
>>>>>
>>>>> So, to justify this transformation as correct, implicitly, poison has
>>>>> _added definedness_ to signed wrapping: specifically, that the
>>>>> computer won't explode if SW happens. AFAIU, that is ok as far as C++
>>>>> semantics
>>>>> are concerned:
>>>>> Since signed wrapping was UB, making it more defined is ok.
>>>>>
>>>>> But that definedness now has created a burden to whoever is writing a
>>>>> back-end
>>>>> from LLVM IR to P (the SW exploding platform).
>>>>> That is, now, if they see a `add <nsw>`, they can't lower it to a
>>>>> trivial signed add,
>>>>> since if they do that and x == INT_MAX, the computer will explode and
>>>>> that violates
>>>>> the semantics of _LLVM IR_ (since we mandated that SW doesn't explode
>>>>> the machine).
>>>>>
>>>>> Instead, they have to lower it as something like:
>>>>> if (x == INT_MAX)
>>>>>   skip or whatever
>>>>>
>>>>> Is this whole thinking correct ? UB, undef and poison all are very
>>>>> subtle so I'm trying
>>>>> to wrap my head around.
>>>>>
>>>>> Thanks,
>>>>> Stefanos Baziotis
>>>>>
>>>>
>>>>
>>>> --
>>>>
>>>> Juneyoung Lee
>>>> Software Foundation Lab, Seoul National University
>>>>
>>>
>>
>> --
>>
>> Juneyoung Lee
>> Software Foundation Lab, Seoul National University
>>
>

-- 

Juneyoung Lee
Software Foundation Lab, Seoul National University
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20201030/edf8c014/attachment.html>