public inbox for gcc@gcc.gnu.org
 help / color / mirror / Atom feed
From: Richard Biener <richard.guenther@gmail.com>
To: Krister Walfridsson <krister.walfridsson@gmail.com>,
	Andrew MacLeod <amacleod@redhat.com>
Cc: GCC Development <gcc@gcc.gnu.org>
Subject: Re: GIMPLE undefined behavior
Date: Thu, 1 Sep 2022 08:54:54 +0200	[thread overview]
Message-ID: <CAFiYyc0W5tjrbfQ7vx_NDN3L-zvPhomvb7KWqiyC6KGqoumWFA@mail.gmail.com> (raw)
In-Reply-To: <Pine.NEB.4.64.2208312350480.7751@gateway.kwa>

On Thu, Sep 1, 2022 at 1:57 AM Krister Walfridsson via Gcc
<gcc@gcc.gnu.org> wrote:
>
> I'm implementing a tool for translation validation (similar to Alive2 for
> LLVM). The tool uses an SMT solver to verify for each GIMPLE pass that the
> output IR is a refinement of the input IR:
>   * That each compiled function returns an identical result before/after
>     the pass (for input that does not invoke UB)
>   * That each function does not have additional UB after the pass
>   * That values in global memory are identical after the two versions of
>     the function are run

Nice.

> I have reported three bugs (106523, 106613, 106744) where the tool has
> found differences in the result, but it is a bit unclear to me what is
> considered undefined behavior in GIMPLE, so I have not reported any such
> cases yet...
>
> For example, ifcombine optimizes
>
> int foo (int x, int a, int b)
> {
>    int c;
>    int _1;
>    int _2;
>    int _3;
>    int _4;
>
>    <bb 2>:
>    c_6 = 1 << a_5(D);
>    _1 = c_6 & x_7(D);
>    if (_1 != 0)
>      goto <bb 3>;
>    else
>      goto <bb 5>;
>
>    <bb 3>:
>    _2 = x_7(D) >> b_8(D);
>    _3 = _2 & 1;
>    if (_3 != 0)
>      goto <bb 4>;
>    else
>      goto <bb 5>;
>
>    <bb 4>:
>
>    <bb 5>:
>    # _4 = PHI <2(4), 0(2), 0(3)>
>    return _4;
> }
>
> to
>
> int foo (int x, int a, int b)
> {
>    int c;
>    int _4;
>    int _10;
>    int _11;
>    int _12;
>    int _13;
>
>    <bb 2>:
>    _10 = 1 << b_8(D);
>    _11 = 1 << a_5(D);
>    _12 = _10 | _11;
>    _13 = x_7(D) & _12;
>    if (_12 == _13)
>      goto <bb 3>;
>    else
>      goto <bb 4>;
>
>    <bb 3>:
>
>    <bb 4>:
>    # _4 = PHI <2(3), 0(2)>
>    return _4;
> }
>
> Both return the same value for foo(8, 1, 34), but the optimized version
> shifts more than 31 bits when calculating _10. tree.def says for
> LSHIFT_EXPR that "the result is undefined" if the number of bits to shift
> by is larger than the type size, which I interpret as it just should be
> considered to return an arbitrary value. I.e., this does not invoke
> undefined behavior, so the optimization is allowed. Is my understanding
> correct?

It's generally poorly documented what is considered 'undefined behavior'.
We desparately need a section in the internals manual for this.
For the {L,R}SHIFT_EXPR case we assume the shift operand is
in range of [0, precision - 1], so in theory value-range propagation could
infer that b_8(D) < 32 after it "executed".  But it seems that
range-on-exit doesn't do that yet.

int x;
int foo (int i, int n)
{
  x = i << n;
  if (n > 32)
    return 7;
  return 0;
}

isn't optimized.

The problem with shifts is that there's not a "do it anway, but without
undefined behavior" operation to substitute.

As I said, we lack clear documentation here :/

> What about signed integer wrapping for PLUS_EXPR? This happens for
>
> int f (int c, int s)
> {
>    int y2;
>    int y1;
>    int x2;
>    int x1;
>    int _7;
>
>    <bb 2>:
>    y1_2 = c_1(D) + 2;
>    x1_4 = y1_2 * s_3(D);
>    y2_5 = c_1(D) + 4;
>    x2_6 = s_3(D) * y2_5;
>    _7 = x1_4 + x2_6;
>    return _7;
> }
>
> where slsr optimizes this to
>
> int f (int c, int s)
> {
>    int y1;
>    int x2;
>    int x1;
>    int _7;
>    int slsr_9;
>
>    <bb 2>:
>    y1_2 = c_1(D) + 2;
>    x1_4 = y1_2 * s_3(D);
>    slsr_9 = s_3(D) * 2;
>    x2_6 = x1_4 + slsr_9;
>    _7 = x1_4 + x2_6;
>    return _7;
>
> Calling f(-3, 0x75181005) makes slsr_9 overflow in the optimized code,
> even though the original did not overflow. My understanding is that signed
> overflow invokes undefined behavior in GIMPLE, so this is a bug in
> ifcombine. Is my understanding correct?

Yes, the above would be a bug - again value-range propagation might be
leveraged to produce a wrong-code testcase.

> I would appreciate some comments on which non-memory-related operations I
> should treat as invoking undefined behavior (memory operations are more
> complicated, and I'll be back with more concrete questions later...).

The more "interesting" cases are uninitialized values (registers or memory).

In general what we should worry about most is introducing undefined
behavior that, when a later pass can assume it doesn't happen, causes
wrong code to be generated.  Likewise when we have late instrumentation
that would flag such undefined behavior as a user error.  I think only
-ftrapv would cause "late" instrumentation (but please don't test -ftrapv,
it's known to be broken in ways).

Thanks,
Richard.

>     /Krister

  reply	other threads:[~2022-09-01  6:55 UTC|newest]

Thread overview: 4+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2022-08-31 23:55 Krister Walfridsson
2022-09-01  6:54 ` Richard Biener [this message]
2022-09-02  0:03   ` Krister Walfridsson
2022-09-02  6:19     ` Richard Biener

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=CAFiYyc0W5tjrbfQ7vx_NDN3L-zvPhomvb7KWqiyC6KGqoumWFA@mail.gmail.com \
    --to=richard.guenther@gmail.com \
    --cc=amacleod@redhat.com \
    --cc=gcc@gcc.gnu.org \
    --cc=krister.walfridsson@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).