X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/9131d1a0288847311e6d15fb8c0cda54d6815d7f..a448e297bd91c98e949afcef1cd63855be7a2375:/personal/_posts/2018-07-24-pointers-and-bytes.md

diff --git a/personal/_posts/2018-07-24-pointers-and-bytes.md b/personal/_posts/2018-07-24-pointers-and-bytes.md
index dfd6bd1..0496a5d 100644
--- a/personal/_posts/2018-07-24-pointers-and-bytes.md
+++ b/personal/_posts/2018-07-24-pointers-and-bytes.md
@@ -19,7 +19,7 @@ I hope that by the end of this post, you will agree with me on both of these sta
 ## Pointers Are Complicated
 
 What is the problem with "pointers are just integers"?  Let us consider the following example:<br>
-(I am using C++ code here mostly because writing unsafe code is easier in C++, and unsafe code is where these problems really show up. C has all the same issues, as does unsafe Rust.)
+(I am using C++ code here mostly because writing unsafe code is easier in C++ than in Rust, and unsafe code is where these problems really show up. C has all the same issues, as does unsafe Rust.)
 {% highlight c++ %}
 int test() {
     auto x = new int[8];
@@ -56,7 +56,7 @@ int test() {
     auto x = new int[8];
     auto y = new int[8];
     y[0] = 42;
-    auto x_ptr = &x[8]; // one past the end
+    auto x_ptr = x+8; // one past the end
     if (x_ptr == &y[0])
       *x_ptr = 23;
     return y[0];
@@ -119,8 +119,15 @@ C++ and Rust employ a more "high-level" view of memory and pointers, restricting
 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]({% 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]({% post_url 2017-07-08-rustbelt %}), and it is also how [miri](https://github.com/solson/miri/) implements pointers):
+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]({% post_url 2017-07-08-rustbelt %}), and it is also how [miri](https://github.com/solson/miri/) implements [pointers](https://github.com/rust-lang/rust/blob/fefe81605d6111faa8dbb3635ab2c51d59de740a/src/librustc/mir/interpret/mod.rs#L121-L124)):
 A pointer is a pair of some kind of ID uniquely identifying the *allocation*, and an *offset* into the allocation.
+If we defined this in Rust, we might write
+{% highlight rust %}
+struct Pointer {
+    alloc_id: usize,
+    offset: isize,
+}
+{% endhighlight %}
 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]
 
@@ -137,8 +144,10 @@ However, this simple model starts to fall apart once you consider pointer-intege
 In miri, casting a pointer to an integer does not actually do anything, we now just have an integer variable (i.e., its *type* says it is an integer) whose *value* is a pointer (i.e., an allocation-offset pair).
 However, multiplying that "integer" by 2 leads to an error, because it is entirely unclear what it means to multiply such an abstract pointer by 2.
 
-This is the most lazy thing to do, and we do it because it is not clear what else to do (other than not supporting these casts at all -- but this way, miri can run more programs).
-In our abstract machine, there is no single coherent "address space" that all allocations live in, that we could use to map every pointer to a distinct integer.
+I should clarify that this is *not* a good solution when defining language semantics.
+It works fine for an interpreter though.
+It is the most lazy thing to do, and we do it because it is not clear what else to do (other than not supporting these casts at all -- but this way, miri can run more programs):
+In our abstract machine, there just is no single coherent "address space" that all allocations live in, that we could use to map every pointer to a distinct integer.
 Every allocation is just identified by an (unobservable) ID.
 We could now start to enrich this model with extra data like a base address for each allocation, and somehow use that when casting an integer back to a pointer... but that's where it gets really complicated, and anyway discussing such a model is not the point of this post.
 The point it to discuss the *need* for such a model.
@@ -150,6 +159,8 @@ We mostly just ignore the problem in miri and opportunistically do as much as we
 A full definition of a language like C++ or Rust of course cannot take this shortcut, it has to explain what really happens here.
 To my knowledge, no satisfying solution exists, but academic research is [getting closer](http://sf.snu.ac.kr/publications/llvmtwin.pdf).
 
+**Update:** This was by no means meant to be an exhaustive list of academic research on C in general. I do not know of other work that focuses directly on the interplay of integer-pointer casts and optimizations, but other noteworthy work on formalizing C includes [KCC](https://github.com/kframework/c-semantics), [Robbert Krebber's PhD thesis](https://robbertkrebbers.nl/thesis.html) and [Cerberus](https://www.cl.cam.ac.uk/~pes20/cerberus/). **/Update**
+
 This is why pointers are not simple, either.
 
 ## From Pointers to Bytes
@@ -162,7 +173,8 @@ We have to say what the value of `v` is, so we have to find some way to answer t
 (And this is an entirely separate issue from the problem with multiplication that came up in the last section. We just assume some abstract type `Pointer`.)
 
 We cannot represent a byte of a pointer as an element of `0..256`.
-Instead, we will remember both the pointer, and which byte of the pointer we got.
+Essentially, if we use a naive model of memory, the extra "hidden" part of a pointer (the one that makes it more than just an integer) would be lost when a pointer is stored to memory and loaded again.
+We have to fix this, so we have to extend our notion of a "byte" to accomodate that extra state.
 So, a byte is now *either* an element of `0..256` ("raw bits"), *or* the n-th byte of some abstract pointer.
 If we were to implement our memory model in Rust, this might look as follows:
 {% highlight rust %}