clarify abstract nature of pointers
[web.git] / ralf / _posts / 2018-07-24-pointers-and-bytes.md
index 61ecc14c8f2f5ccb52ffc80f4c6f863fc4e1ec4d..b3a74c480016c1d2c85b501e34b36cd0857f4bb1 100644 (file)
@@ -1,6 +1,7 @@
 ---
 title: "Pointers Are Complicated, or: What's in a Byte?"
 categories: internship rust
+forum: https://internals.rust-lang.org/t/pointers-are-complicated-or-whats-in-a-byte/8045
 ---
 
 This summer, I am again [working on Rust full-time]({{ site.baseurl }}{% post_url 2018-07-11-research-assistant %}), and again I will work (amongst other things) on a "memory model" for Rust/MIR.
@@ -43,7 +44,7 @@ First of all, it is not allowed to perform pointer arithmetic (like `&x[i]` does
 Our program violates this rule: `x[i]` is outside of `x`, so this is undefined behavior.
 To be clear: Just the *computation* of `x_ptr` is already UB, we don't even get to the part where we want to *use* this pointer![^1]
 
-[^1]: It turns out that `y-x` is also undefined behavior because [one may only subtract pointers into the same allocation](https://timsong-cpp.github.io/cppwp/n4140/expr.add#6). However, we could use `i = ((size_t)y - (size_t)x)/sizeof(int)` to work around that.
+[^1]: It turns out that `i = y-x` is *also* undefined behavior because [one may only subtract pointers into the same allocation](https://timsong-cpp.github.io/cppwp/n4140/expr.add#6). However, we could use `i = ((size_t)y - (size_t)x)/sizeof(int)` to work around that.
 
 But we are not done yet: This rule has a special exception that we can exploit to our advantage.
 If the arithmetic ends up computing a pointer *just past* the end of an allocation, that computation is fine.
@@ -110,7 +111,15 @@ So, what *is* a pointer?
 I don't know the full answer to this.
 In fact, this is an open area of research.
 
-Here's a simple proposal (in fact, this is the model used in my [RustBelt work]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}), and it is also how [miri](https://github.com/solson/miri/) implements pointers):
+One important point to stress here is that we are just looking for an *abstract model* of the pointer.
+Of course, on the actual machine, pointers are integers.
+But the actual machine also does not do the kind of optimizations that modern C++ compilers do, so it can get away with that.
+If we wrote the above programs in assembly, there would be no UB, and no optimizations.
+C++ and Rust employ a more "high-level" view of memory and pointers, restricting the programmer for the benefit of optimizations.
+When formally describing what the programmer may and may not do in these languages, as we have seen, the model of pointers as integers falls apart, so we have to look for something else.
+This is another example of using a "virtual machine" that's different from the real machine for specification purposes, which is an idea [I have blogged about before]({{ site.baseurl }}{% post_url 2017-06-06-MIR-semantics %}).
+
+Here's a simple proposal (in fact, this is the model of pointers used in [CompCert](https://hal.inria.fr/hal-00703441/document) and my [RustBelt work]({{ site.baseurl }}{% post_url 2017-07-08-rustbelt %}), and it is also how [miri](https://github.com/solson/miri/) implements pointers):
 A pointer is a pair of some kind of ID uniquely identifying the *allocation*, and an *offset* into the allocation.
 Adding/subtracting an integer to/from a pointer just acts on the offset, and can thus never leave the allocation.
 Subtracting a pointer from another is only allowed when both point to the same allocation (matching [C++](https://timsong-cpp.github.io/cppwp/n4140/expr.add#6)).[^2]
@@ -199,8 +208,10 @@ Using `Uninit` instead of an arbitrary bit pattern means miri can, in a single e
 
 ## Conclusion
 
-We have seen that pointers can be different even when they point to the same address, and that a byte is more than just a number in `0..256`.
+We have seen that in languages like C++ and Rust (unlike on real hardware), pointers can be different even when they point to the same address, and that a byte is more than just a number in `0..256`.
 With this, I think we are ready to look at a first draft of my "2018 memory model" (working title ;) -- in the next post. :)
-<!-- If you have any questions, feel free to [ask in the forums]! -->
+
+Thanks to @rkruppe and @nagisa for help in finding arguments for why `Uninit` is needed.
+If you have any questions, feel free to [ask in the forums](https://internals.rust-lang.org/t/pointers-are-complicated-or-whats-in-a-byte/8045)!
 
 #### Footnotes