3 ms·

> Is the question "what is the first byte?" any more or less problematical for a {base, offset} pointer than it is for a multi-byte integer, where place value m

> Is the question "what is the first byte?" any more or less problematical for a {base, offset} pointer than it is for a multi-byte integer, where place value matters? Shifting and bit-masking integers are operations that make sense. Storing an int in memory and loading back only one of its bytes is equivalent to loading it all, then shifting and masking. It's meaningful, thus you do need to model the bits faithfully. In contrast, shifting and masking pointers is (with some exceptions) not meaningful. Neither is it meaningful to store one of these in memory and to load back only part of it. It makes sense to use a more abstract, symbolic model for bytes of such values. For whatever it's worth, the author's solution for bytes is the same as CompCert's: https://github.com/AbsInt/CompCert/blob/3939a1ccfdb86795e9fdf5953489ddfee238152c/common/Memdata.v#L155 https://github.com/AbsInt/CompCert/blob/3939a1ccfdb86795e9fd...

mannykannot 8y ago
That's a good point - if I am following correctly, a memcpy of a byte from an integer can be regarded as an arithmetical operation (in fact, a multiplicative one), while, in general, there is no equivalent interpretation for copying a byte of a pointer. I guess one could make a similar argument for the bytes of a unicode string. While writing this, it occurred to me that the difficulties with casting between pointers and integers is in going from integers to pointers, where there is no unique mapping (for pointer to integer, base + offset is meaningful, but it loses information.)