On Tue, Feb 15, 2022 at 2:00 PM Julian Seward <seward...@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.
