Change stack and register models to bytes instead of values

[gergo-]

This pull request changes CompCert's stack and register model from a value-based one to a more low-level one based on bytes. That is, from the LTL level onwards, data structures like Locmap and Pregmap are no longer mappings from location names to values, but memory-like blocks of bytes. Their get and set operations decode bytes to values and vice versa on-the-fly. (However, register-to-register copies actually copy raw bytes.) To abstract similarities between the mreg and preg representation levels, a new Regfile module (functor) is introduced.

As enoding and decoding of values is type-sensitive, lemmas about these operations enforce well-typedness. In particular, the gss lemma only guarantees that a value written to a location can be read back unchanged if the value actually fits into the location. In other words, 64-bit values can no longer be stored into 32-bit registers and read back.

Large parts of these patches enforce this well-typedness at all intermediate language levels on all supported architectures.

This work is meant as a basis for further extensions for modeling subregister aliasing correctly in the future.