public inbox for gcc@gcc.gnu.org
 help / color / mirror / Atom feed
From: Krister Walfridsson <krister.walfridsson@gmail.com>
To: gcc@gcc.gnu.org
Subject: GIMPLE undefined behavior
Date: Wed, 31 Aug 2022 23:55:42 +0000 (UTC)	[thread overview]
Message-ID: <Pine.NEB.4.64.2208312350480.7751@gateway.kwa> (raw)

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

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?

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?

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...).

    /Krister

             reply	other threads:[~2022-08-31 23:56 UTC|newest]

Thread overview: 4+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2022-08-31 23:55 Krister Walfridsson [this message]
2022-09-01  6:54 ` Richard Biener
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=Pine.NEB.4.64.2208312350480.7751@gateway.kwa \
    --to=krister.walfridsson@gmail.com \
    --cc=gcc@gcc.gnu.org \
    /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).