stedolan / counterexamples

Counterexamples in Type Systems
http://counterexamples.org
372 stars 23 forks source link

Eventually, nothing: factually inaccuracy about the C standard #20

Open nneonneo opened 1 year ago

nneonneo commented 1 year ago

The section “Eventually, nothing” states:

according to the C standard, compilers are allowed to assume that the program contains no infinite loops without side-effects.

This is inaccurate; the precise statement from the C standard (C11, 6.8.5) states:

An iteration statement whose controlling expression is not a constant expression, that performs no input/output operations, does not access volatile objects, and performs no synchronization or atomic operations in its body, controlling expression, or (in the case of a for statement) its expression-3, may be assumed by the implementation to terminate.

Loops with constant controlling expressions, as well as loops that access volatile variables cannot be optimized out in C; the fact that they were was a simple bug in LLVM. It is probably more accurate to say that the C standard permits certain infinite loops to be optimized out.

stedolan commented 1 year ago

Loops that access volatile variables do contain side effects, by both the informal idea of "side effect" and C11's definition of "side effect" in 5.1.2.3p2.

The case of constant controlling expressions is more interesting - I hadn't realised there was a caveat in C11 for this! Apparently it was somewhat controversial: drafts of C11 up to at least October 2010 specified infinite side-effect-free loops as undefined behaviour (the authors said this codified the implicit rules of C99 and before), but by the time it was actually published it became the language you quote. (See N1528 and N1509).

I'll update the entry to mention that the controlling expression must not be integer constant expressions to trigger this behaviour (in the standard at least, regardless of what compilers do). Thanks for pointing this out!