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
