Re: Uninit warnings due to optimizing short-circuit conditionals

[Richard Biener <richard.guenther@gmail.com>]

On Tue, Feb 15, 2022 at 2:00 PM Julian Seward <sewardj42@gmail.com> wrote:
>
> Sorry for the delayed response.  I've been paging this all back in.
>
> I first saw this problem when memcheck-ing Firefox as compiled by Clang, some
> years back.  Not long after GCC was also at it.  The transformation in
> question is (at the C level):
>
> A && B  ==>  B && A   if it can be proved that A
>                       is always false whenever B is undefined
>                       and (I assume) that B is provably exception-free
>
> where && means the standard lazy left-first C logical-AND.  I believe this
> might have become more prevalent due to ever-more aggressive inlining (at
> least for Firefox), which presented the compilers with greater opportunities
> to make the required proofs.

Note GCC doesn't try to prove this, instead it reasons that when
B is undefined it takes an indeterminate value and if A is _not_ always
false then the program would have invoked undefined behavior, so we
can disregard this possibility and assume B is not undefined.  So
either B is not undefined and everything is OK, or B is undefined but
then A must be always false.

Note that when A is always false we may have transformed a valid
program (does not access B) into a program invoking undefined behavior
(in C language terms).  We don't treat undefined uses as "very" undefined
behavior but I do remember we've shot ourselves in the foot with this
transform - in this case we'd have to make the use of B determinate
somehow, something we cannot yet do.  So we'd want a transform
like

 A && B ==> OK(B) && A

where 'OK' sanitizes B in case it is undefined.  The error we can run into
is that two of the uninit Bs can be equated to two different values,
breaking the B == B invariant (technically also OK, but not if it was us
that introduced the undefinedness in the first place).

Richard.