Signed integer overflow specification

[Lysxia]

The documentation of Verifiable C is misleading about the semantics of signed integer overflow with respect to C standards.

Page 16 of VC.pdf says

The C language specification says that a C compiler \emph{may} treat signed integer overflow by wrapping around mod $2^n$, where n is the word size (e.g., 32).

What specification is this referring to? According to C standards, signed integer overflow is undefined behavior; in this document, that is in fact the first example given under the definition of undefined behavior (3.4.3, p22 of this PDF).

One could say that wraparound is allowed as a consequence of the fact that standard-compliant compilers are free to implement undefined behaviors in any way they like. However, if all behaviors are allowed, then the standard does not further need to explicitly allow one in particular, but the excerpt above suggests it does. Perhaps that excerpt is referring to Annex H (H.2.2, p564 of the PDF), but that is not quite a specification. Hence, this formulation is not quite incorrect, but it is confusing for one who knows a bit about C standards.

In any case, CompCert's documentation correctly acknowledges this fact:

We see that the expression 65536 * 65536 + 2 caused an overflow in signed arithmetic. This is an undefined behavior according to the C standards, but the CompCert C semantics fully defines this behavior as computing the result modulo 232.

I also disagree with the claim that this treatment of undefined behavior is conventional. VC.pdf continues:

In practice, almost all C compilers (including CompCert) do this wraparound, and it is part of the CompCert C light operational semantics.

On the contrary, compilers typically assume that undefined behavior never happens to allow for more optimizations, thus there are no semantics for signed integer overflow. A typical example is that given x > 0 and y > 0, since overflow is undefined, then one can assume that x+y > 0, which may lead to simplifications, but that assumption is not compatible with wraparound semantics.

[andrew-appel]

You are right. It would be a good idea to make signed integer overflow undefined in Verifiable C, even though it is defined in CompCert Clight. This could be accomplished by a small modification to Verifiable C's type-checker. Likely we will do this soon.

[andrew-appel]

This is now fixed in commit aa981cf.