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]
We always remember which allocation a pointer points to, so we can differentiate a pointer "one past the end" of one allocation from a pointer to the beginning of another allocation.
That's how miri can detect that our second example (with `&x[8]`) is UB.
+## The Model Falls Apart
+
In this model, pointers are not integers, but they are at least simple.
However, this simple model starts to fall apart once you consider pointer-integer casts.
-In miri, casting a pointer to an integer does not actually do anything, we now just have an integer variable whose value is a pointer (i.e., an allocation-offset pair).
-Multiplying that integer by 2 leads to an error, because it is entirely unclear what it means to multiply such a pair by 2.
+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).[^3]
+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.
+
+[^3]: This disconnect between the type and the value may seem somewhat strange, but we are actually not very concerned with *types* at this point. Types serve to classify values with the goal of establishing certain guarantees about a program, so we can only really start talking about types once we are done defining our set of values and program behaviors. Still, this means there are safe programs that miri cannot execute, such as `(Box::new(0).into_raw() as usize) * 2`. To avoid trouble with multiplication, I proposed to only allow "normal" integer values for integer types when doing [compile-time function evaluation]({{ site.baseurl }}{% post_url 2018-07-19-const %}). However, this makes pointer-integer casts an unsafe operation, because they do not actually produce a "fully operational" integer.
+
+This is the most lazy thing to do, and we do it because it is not clear what else to do -- 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.
+Every allocation is just identified by a (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 integer back to pointers... 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.
+If you are interested, I suggest you read [this paper](http://www.cis.upenn.edu/%7Estevez/papers/KHM+15.pdf) that explores the above idea of adding a base address.
+
+Long story short, pointer-integer casts are messy and hard to define formally when also considering optimizations like we discussed above.
+There is a conflict between the high-level view that is required to enable optimizations, and the low-level view that is required to explain casting a pointer to an integer and back.
+We mostly just ignore the problem in miri and opportunistically do as much as we can, given the simple model we are working with.
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 we are [getting](http://www.cis.upenn.edu/%7Estevez/papers/KHM+15.pdf) [closer](http://sf.snu.ac.kr/publications/llvmtwin.pdf).
+To my knowledge, no satisfying solution exists, but academic research is [getting closer](http://sf.snu.ac.kr/publications/llvmtwin.pdf).
+
This is why pointers are not simple, either.
## From Pointers to Bytes
}
{% endhighlight %}
With `Uninit`, we can easily argue that `x` is either `Uninit` or `1`, and since replacing `Uninit` by `1` is okay, the optimization is easily justified.
-Without `Uninit`, however, `x` is either "some arbitrary bit pattern" or `1`, and doing the same optimization becomes much harder to justify.[^3]
+Without `Uninit`, however, `x` is either "some arbitrary bit pattern" or `1`, and doing the same optimization becomes much harder to justify.[^4]
-[^3]: We could argue that we can reorder when the non-deterministic choice is made, but then we have to prove that the hard to analyze code does not observe `x`. `Uninit` avoids that unnecessary extra proof burden.
+[^4]: We could argue that we can reorder when the non-deterministic choice is made, but then we have to prove that the hard to analyze code does not observe `x`. `Uninit` avoids that unnecessary extra proof burden.
Finally, `Uninit` is also a better choice for interpreters like miri.
Such interpreters have a hard time dealing with operations of the form "just choose any of these values" (i.e., non-deterministic operations), because if they want to fully explore all possible program executions, that means they have to try every possible value.
## 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`.[^4]
+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. :)
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)!
-[^4]: And just to be clear, I am talking about a pointer or byte in the model of an optimized *programming language* here. When modeling hardware, everything is different.
-
#### Footnotes
projects / web.git / blobdiff