typo
authorRalf Jung <post@ralfj.de>
Tue, 24 Jul 2018 21:41:36 +0000 (23:41 +0200)
committerRalf Jung <post@ralfj.de>
Tue, 24 Jul 2018 21:48:40 +0000 (23:48 +0200)
ralf/_posts/2018-07-24-pointers-and-bytes.md

index 5d7a40b..26afca5 100644 (file)
@@ -137,11 +137,11 @@ 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).[^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.
+[^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 a "const-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.
+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.
 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.