Infinite loop language lawyering

Compilers are at least operating in a relatively constrained domain, with well defined rules . . . except that strolling through the copious arguments that always crop up in any discussion that touches on language specification and compiler behaviour makes it pretty clear that "well defined rules" are something you need to be focusing on right from the start of your language design, rather than retrofitting to an already established language.

Even if you do focus on well-defined rules from day 1, the whole field of programming language semantics is relatively young, and it's not completely clear which formal semantic model gets you the best outcomes; we know that axiomatic semantics are hard for non-specialists to interpret correctly, but that's about it for things we can use to choose between formalisms. At the moment, it looks like operational semantics are the front-runner, since they lend themselves nicely to optimizations on the basis of the "as-if" rule, but it's not clear whether operational or denotational semantics are easier to transform to a form that's clear to non-specialists. And there's no point having "correct" formal semantics if they're only referenced by specialists in formal semantics (since that's a subset of compiler developers); we need the formal semantics to at least be transformable into something that's clear to a skilled programmer.

Unfortunately, it becomes impossible for the compiler to even determine what the programmer wrote at the point where it's interesting to know if a condition is constant, especially since defensive programming means that a condition might be known to be constant, even though it's variable at source level. Consider the following C function:

static int fetch_update_package_epoch(epochs *epoch_area) {
    if (epoch_area == NULL) {
         return 0;
    }
    epoch_area->package += 1;
    return epoch_area->package;
}

At source level, this is clearly not attempting to invoke UB, and there's no constant comparisons involved. As a result, by the time the optimizer is relying on assuming no UB, what it will be looking at (after optimizing the function's IR over many passes) is something like:

define dso_local i32 @fetch_update_package_epoch(ptr noundef %epoch_area) local_unnamed_addr {
entry:
  %cmp = icmp eq ptr %epoch_area, null
  br i1 %cmp, label %return, label %if.end

if.end:
  %0 = load i32, ptr %epoch_area, align 4
  %add = add nsw i32 %0, 1
  store i32 %add, ptr %epoch_area, align 4
  br label %return

return:
  %retval.0 = phi i32 [ %add, %if.end ], [ 0, %entry ]
  ret i32 %retval.0
}

This is short enough to inline; when it's inlined, the optimizer will replace a %call = call noundef i32 @fetch_update_package_epoch(epochs*)(ptr noundef nonnull %epochs) with the function body, making the right substitution for epoch_area. Now, because the call tells us that epoch_area is nonnull, the comparison becomes a constant, the branch can be made unconditional, and then dead code elimination removes the NULL check.

But the problem is that what's triggered the comparison becoming a constant is the compiler identifying that epoch_area in the call at IR level is nonnull. The optimizer can't warn you that it's eliding the NULL check based on this, because it cannot distinguish "this is nonnull because otherwise there is UB in the program" from "this is nonnull because the source lines are epoch_area epochs = { package = 1 }; pkg = fetch_update_package_epoch(&epochs);. Both of those are the same IR at this point - a call with a non-NULL annotation on the pointer - how should the optimizer know that one of those annotations is fine to ignore, but the other matters? And note that you also don't want to warn just because a pointer is marked as non-NULL because it'd be UB to be NULL, since that would cause you to warn on:

static int fetch_update_package_epoch(epochs *epoch_area) {
    epoch_area->package += 1;
    return epoch_area->package;
}

But it might be perfectly clear from the rest of the source code context that, in this case, epoch_area will never be NULL, because no function calls this with a possibly-NULL pointer.

That only works because the output language is still JavaScript, with JavaScript semantics; the issue in this case is that the compiler has read in C (or Rust, or whatever) source code, translated it to an IR like GIMPLE or LLVM IR (with different semantics to the source language) on the basis that the translation only has UB in the IR if the source code had UB, optimized the IR on the assumption of no UB in the IR output, and then ended up with IR that it translates to machine code that has different semantics to the one the programmer intended, because the programmer did not intend to write code with UB.

Note, for example, that C++'s "forward progress" assumption also allows for endless loops, as long as they're "trivial", change state visible to another thread, or they contain I/O. It's only pure computational loops that can be elided if they do not terminate, and only if they're non-trivial in the original source - so for(;;) {} is trivial, and therefore cannot be elided, while for(;;) do_the_thing() is non-trivial, and can be elided if do_the_thing() has no effects visible outside the current thread. This is useful for compilers, since once it's able to show that do_the_thing() is a no-op, it can elide the whole loop - even if do_the_thing is actually a macro containing a break; statement.

There is no real equivalent of this stack of languages in the JavaScript ecosystem, because the "machine code" you execute is also JavaScript.