Add Mbool memory chunk to improve compilation of computations at type _Bool

[xavierleroy]

This PR introduces a new kind of memory chunk, Mbool, to be used when compiling loads and stores of values of C type _Bool.

The semantics of a memory load with chunk Mbool is as follows:

• Read 8 bits as an integer n (all known ABIs mandates that _Bool has size 1 byte)
• Return 0 if n = 0, 1 if n = 1, and Vundef otherwise.

With this semantics, the result of the load is guaranteed to be a correct value of type _Bool, i.e. 0, 1 or Vundef. This is not the case in the current CompCert, where _Bool values are read using the Mint8unsigned chunk, resulting in any integer in the 0..255 range, or Vundef.

Consequently, the value analysis of Boolean computations is more precise, enabling nice optimizations, as in the following examples.

_Bool f(_Bool * p) { return *p; }

void g(_Bool * p) { *p ^= 1; }

_Bool h(_Bool * p, _Bool * q) { return *p & *q; }

With this PR, all three examples are compiled without any normalization to _Bool.

The semantics of Mbool loads is carefully engineered so that it can be implemented in the final assembly code as a 8-bit unsigned load Mint8unsigned, producing a "more defined than" result.

What's in this PR?

• The Mbool memory chunk is added, with the semantics outlined above.
• Value analysis and other back-end passes are adapted to deal with Mbool.
• The Stacking pass transforms Mbool loads and stores into Mint8unsigned loads and stores, after all optimizations have been done.
• The C front-end generates Mbool loads and stores to access l-values of _Bool type.
• The type soundness result in Ctyping is strengthened; now, it shows that the only values of type _Bool are 0, 1 and Vundef.

In passing, the PR refactors some code from the various Asmgen/Asmgenproof files into the shared Stacking/Stackingproof files. This was not absolutely necessary, just a good opportunity to do so.

[xavierleroy]

For the record: this change renders undefined some CompCert C programs that currently have defined behavior according to the CompCert C semantics, but are undefined behavior in ISO C. Consider:

_Bool char2bool (unsigned char c) { return *((_Bool *) &c); }
int main() { return char2bool(42); }

Currently, this is defined to return 1. (The function char2bool is equivalent to a c != 0 test.)

With the change in this PR, the load of the _Bool is undefined, since the byte read from memory is neither 0 nor 1.

char2bool(0) and char2bool(1) have well-defined semantics, though.