> Is the critical difference here that the array access happens outside of the "for" expression?

Precisely: this means that `d[k]` is guaranteed to execute before the check that `k < 16`. In general, if you have some access like `d[k]` where `k` is some integer and `d` is some array of size `N`, you can assume that `k < N` on all paths which are dominated by the statement containing `d[k]`. In simpler terms, the optimizer will assume that `k < N` is true on every path after the access to `d[k]` occurs.

To make this clearer, consider an equivalent, slightly-transformed version of the original code:

    int d[16];
    int SATD (void)
    {
      int satd = 0, dd, k;
      dd = d[k=0];
      do {
        satd += (dd < 0 ? -dd : dd);
        k = k + 1;
        dd=d[k]; // At this point, k must be < 16.
      } while (k < 16); // The value of `k` has not changed, thus our previous
                        // assumption that `k < 16` must still hold. Thus `k < 16`
                        // can be simplified to `true`.
      return satd;
    }

    int d[16];
    int SATD (void)
    {
    int satd = 0, k = 0;
    k = 0;
    do
    {
      satd += d[k] < 0 ? -d[k] : d[k]; // At this point, k must be < 16
      k = k + 1;
    } while (k < 16); // The value of `k` has changed -- at best, we can assert
                      // that `k < 17` since its value increased by 1 since we
                      // last assumed it was less than 16. But the assumption
                      // that `k < 16` doesn't hold, and this check cannot be
                      // simplified.
    return satd;
    }

The problem is checking for k<16 and incrementing k and then using k to access array d[16] afterwards. That's how it goes out if bounds. The condition is inadequate for ensuring that k stays in the bounds of array d[16].

It seems like k is "obviously" an array index for array d[16] here, but whatever. Not in a position to have that discussion right now.

As for Java, (too lazy to look that up right now): That at least sounds like they enforce twos-complement representation for signed int values. C89 has UB here because ancient hardware also used ones-complement. And C89 wanted to be portable as a portable assembler. Well, if UB really makes anything portable. They didn't even go with platform-dependent a.k.a. implementation defined. Instead they specifically chose undefined behavior. The argument brought forward, at least today, is that C isn't supposed to be a portable assembler. Now which one is it supposed to be? Cannot have both at the same time.

Regarding the wrong code, I already wrote (and you can confirm in my unrolled analysis):

> every instance of testing `k < 16` is true before we hit UB. Therefore it can be simplified to true without loss of functionality, because after we hit UB, we are allowed to do absolutely anything.

Regarding the correct code, the key insight is that when k is 16, the test `k < 16` is false, so we break out of the loop and avoid reading out of bounds. Always check bounds before indexing the array, not after!

This article is a helpful introduction: https://blog.regehr.org/archives/213

> is the compiler doing a loop unroll and study that parallels your analysis?

Yes, compilers do all sorts of crazy stuff from bounds analyses to loop induction transformations. Personally, I've seen GCC eliminate my second loop variable in an implementation of the TEA cipher because it figured out that the first variable can be derived from the second, and it adjusted the bounds.

> it also seems a bit nuts that these c guys remediated that behavior by allowing an out of bounds index access with their change

You are right, it's insane that they decided to make a special case for one piece of wrong code (SPEC), probably because it's too popular to fail. That's a social/political problem, not a technical one.