show pointer as Rust struct

[web.git] / 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 85ba4aa679a615069221de05d17dc6a94a9f9669..35a5c159dbd9d32c4847f6e9af54ad0d63f2e066 100644 (file)
--- a/personal/_posts/2018-07-24-pointers-and-bytes.md
+++ b/personal/_posts/2018-07-24-pointers-and-bytes.md
@@ -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]