3 ms·

This is an interesting discussion, but I get the impression that the author is trying to reconcile two fundamentally irreconcilable ways of looking at memory: o

This is an interesting discussion, but I get the impression that the author is trying to reconcile two fundamentally irreconcilable ways of looking at memory: on the one hand, the machine view of a single address space, and on the other, the program view of distinct variables. I am not at all convinced that there is a unifying viewpoint, at least if you want to cast pointers in both models to and from integers. One can, of course, map {base, offset} pointers to the natural numbers (though not necessarily Rust integer types? I don't know Rust) by considering the base to be the most significant bits of the number and the offset the least, but arithmetic on these numbers is not the same as pointer arithmetic in the address-space model. I do not follow the part, in the "what's in a byte" section, about a byte-by-byte memcpy. 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?

ralfjung 8y ago
> the author is trying to reconcile two fundamentally irreconcilable ways of looking at memory: on the one hand, the machine view of a single address space, and on the other, the program view of distinct variables That's not incorrect. However, the reason I am doing that is because this is what C is all about (nowadays, at least): Compilers doing high-level optimizations based on alias analysis and other sources, and programmers expecting to have a low-level picture of memory. Our choice is to either give up and declare C broken beyond repair, or try to find some way to reconcile these two worlds as best as possible.
tom_mellior 8y ago
> 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.)

ralfjung 8y ago

> the author is trying to reconcile two fundamentally irreconcilable ways of looking at memory: on the one hand, the machine view of a single address space, and on the other, the program view of distinct variables That's not incorrect. However, the reason I am doing that is because this is what C is all about (nowadays, at least): Compilers doing high-level optimizations based on alias analysis and other sources, and programmers expecting to have a low-level picture of memory. Our choice is to either give up and declare C broken beyond repair, or try to find some way to reconcile these two worlds as best as possible.

tom_mellior 8y ago

> 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.)