more editing

Author: RalfJung

wip/memory-interface.md

@@ -4,21 +4,22 @@
 
 The purpose of this document is to describe the interface between a Rust program and memory.
 This interface is a key part of the Rust Abstract Machine: it lets us separate concerns by splitting the Machine (i.e., its specification) into two pieces, connected by this well-defined interface:
-* The *expression/statement semantics* of Rust boils down to explaining which "memroy events" (calls to the memory interface) happen in which order.
+* The *expression/statement semantics* of Rust boils down to explaining which "memroy events" (calls to the memory interface) happen in which order. This part of the specification is *pure* in the sense that it has no "state": everything that needs to be remembered from one expression evaluation to the next is communicated through memory.
 * The Rust *memory model* explains which interactions with the memory are legal (the others are UB), and which values can be returned by reads.
 
-The interface is also opinionated in several ways; this is not intended to be able to support *any imaginable* memory model, but rather start the process of reducing the design space of what we consider a "reasonable" memory model for Rust.
-For example, it explicitly acknowledges that pointers are not just integers and that uninitialized memory is special (both are true for C and C++ as well but you have to read the standard very careful, and consult non-normative defect report responses, to see this).
+The interface shown below is also opinionated in several ways.
+It is not intended to be able to support *any imaginable* memory model, but rather start the process of reducing the design space of what we consider a "reasonable" memory model for Rust.
+For example, it explicitly acknowledges that pointers are not just integers and that uninitialized memory is special (both are true for C and C++ as well but you have to read the standard very careful, and consult [non-normative defect report responses](http://www.open-std.org/jtc1/sc22/wg14/www/docs/dr_260.htm), to see this).
 Another key property of the interface presented below is that it is *untyped*.
-This encodes the fact that in Rust, *operations are typed, but memory is not*---a key difference to C and C++ with their type-based strict aliasing rules.
-At the same time, the memory model provides a *side-effect free* way to turn pointers into "raw bytes", which is *not* [the direction C++ is moving towards](http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2364.pdf), so we might have to revisit this choice later.
+This implies that in Rust, *operations are typed, but memory is not*---a key difference to C and C++ with their type-based strict aliasing rules.
+At the same time, the memory model provides a *side-effect free* way to turn pointers into "raw bytes", which is *not* [the direction C++ is moving towards](http://www.open-std.org/jtc1/sc22/wg14/www/docs/n2364.pdf), and we might have to revisit this choice later if it turns out to not be workable.
 
 ## Pointers
 
 One key question a memory model has to answer is *what is a pointer*.
 It might seem like the answer is just "an integer of appropriate size", but [that is not the case][pointers-complicated].
 This becomes even more prominent with aliasing models such as [Stacked Borrows].
-So we will leave this question open, and treat `Pointer` as an "associated type" of the memory interface
+So the interface will leave it up to the concrete instance to answer this question, and carry `Pointer` as an associated type.
 
 ## Bytes
 
@@ -58,7 +59,7 @@ impl<Pointer: PtrToInt> Byte<Pointer> {
             Byte::Raw(int) => Some(int),
             Byte::Uninit => None,
             Byte::PtrFragment { ptr, idx } =>
-                ptr.get_byte(idx),
+                Some(ptr.get_byte(idx)),
         }
     }
 }
@@ -96,9 +97,10 @@ trait Memory {
     fn read(&mut self, ptr: Self::Pointer, len: u64) -> Result<Vec<Byte<Self::Pointer>>, Error>;
 
     /// Offset the given pointer.
-    fn offset(&mut self, ptr: Self::Pointer, offset: u64, mode: OffsetMode) -> Result<Self::Pointer, Error>;
+    fn offset(&mut self, ptr: Self::Pointer, offset: u64, mode: OffsetMode)
+        -> Result<Self::Pointer, Error>;
 
-    /// Cast the given integer to a pointer.
+    /// Cast the given integer to a pointer.  (The other direction is handled by `PtrToInt` below.)
     fn int_to_ptr(&mut self, int: u64) -> Result<Self::Pointer, Error>;
 }
 
@@ -129,8 +131,6 @@ This is a very basic memory interface that is incomplete in at least the followi
 * To represent [Stacked Borrows], there needs to be a "retag" operation, and that one will in fact be "lightly typed" (it cares about `UnsafeCell`).
 * Maybe we want operations that can compare pointers without casting them to integers.
 
-But I think it can still be useful to provide some basic terminology and grounds for further discussion.
-
 [pointers-complicated]: https://www.ralfj.de/blog/2018/07/24/pointers-and-bytes.html
 [uninit]: https://www.ralfj.de/blog/2019/07/14/uninit.html
 [`Ordering`]: https://doc.rust-lang.org/nightly/core/sync/atomic/enum.Ordering.html

wip/value-domain.md

@@ -23,8 +23,6 @@ enum Value<Pointer> {
     Bool(bool),
     /// A pointer.
     Ptr(Pointer),
-    /// A zero-sized "unit".
-    Unit,
     /// An uninitialized value.
     Uninit,
     /// An n-tuple.
@@ -34,6 +32,8 @@ enum Value<Pointer> {
         idx: u64,
         data: Box<Self>,
     },
+    /// A "bag of raw bytes".
+    RawBag(Vec<Byte<Pointer>>),
     /* ... */
 }
 ```
@@ -46,28 +46,30 @@ We show some examples for how one might want to use this `Value` domain to defin
 
 ### `bool`
 
-The value relation for `bool` relates `Bool(b)` with `[bb]` if and only if `bb.as_int() == Some(if b { 1 } else { 0 })`.
+The value relation for `bool` relates `Bool(b)` with `[r]` if and only if `r.as_int() == Some(if b { 1 } else { 0 })`.
+(`as_int` is defined in [the memory interface][memory-interface].)
 
 ### `()`
 
-The value relation for the `()` type relates `Unit` with the empty list `[]`, and that's it.
+The value relation for the `()` type relates the empty tuple `Tuple([])` (assuming we can use array notation to "match" on `Vec`) with the empty byte list `[]`, and that's it.
 
 ### `!`
 
 The value relation for the `!` type is empty: nothing is related to anything at this type.
 
 ### `#[repr(C)] struct Pair<T, U>(T, U)`
 
-The value relation for `Pair` us based on the value relations for `T` and `U`.
-A value `Tuple([t, u])` (assuming we can use array notation to "match" on `Vec`) is represented by a list of bytes `rt ++ pad1 ++ ru ++ pad2` (using `++` for list concatenation) if:
+The value relation for `Pair` is based on the value relations for `T` and `U`.
+A value `Tuple([t, u])` is represented by a list of bytes `rt ++ pad1 ++ ru ++ pad2` (using `++` for list concatenation) if:
 
 * `t` is represented by `rt` at type `T`.
 * `u` is represented by `ru` at type `U`.
 * The length of `rt ++ pad1` is equal to the offset of the `U` field.
 * The length of the entire list `rt ++ pad1 ++ ru ++ pad2` is equal to the size of `Pair<T, U>`.
 
-This relation demonstrates that value of type `Pair` are always 2-tuples (aka, pairs).
-It also shows that the actual content of the padding bytes is entirely irrelevant, we only care to have the right number of them to "pad" `ru` to the right place and to "pad" the entire list to have the right length.
+This relation specifies that values of type `Pair` are always 2-tuples (aka, pairs).
+It also says that the actual content of the padding bytes is entirely irrelevant, we only care to have the right number of them to "pad" `ru` to the right place and to "pad" the entire list to have the right length.
+So, for example when considering `Pair<u8, u16>`, the value `Tuple[42, 119]` is represented on a little-endian target by `[Raw(42), byte, Raw(119), Raw(0)]` for *any* `byte: Byte`.
 
 ### `&T`/`&mut T`
 
@@ -80,9 +82,14 @@ A value `Ptr(ptr)` is related to `[PtrFragment { ptr, idx: 0 }, ..., PtrFragment
 For the value representation of integer types, there are two different reasonable choices.
 Certainly, a value `Int(i)` where `i` in `0..256` is related to `[b]` if `b.as_int() == Some(i)`.
 
-And then, maybe, we also want to additionally say that value `Uninit` is related to `[Uninit]`.
+And then, maybe, we also want to additionally say that value `Uninit` is related to byte list `[Uninit]`.
 This essentially corresponds to saying that uninitialized memory is a valid representation of a `u8` value (namely, the uninitialized value).
 
+### `union`
+
+The `union` type does not even try to interpret memory, so for a `union` of size `n`, the value relation says that for any byte list `bytes` of that length, `RawBag(bytes)` is related to `bytes`.
+(Note however that [this definition might not be implementable](https://github.com/rust-lang/unsafe-code-guidelines/issues/156).)
+
 ## The role of the value representation in the operational semantics
 
 One key use of the value representation is to define a "typed" interface to memory:
@@ -97,7 +104,7 @@ trait TypedMemory: Memory {
 }
 ```
 
-here, `Type` is some representation of the Rust type system (akin to [`Ty`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/type.Ty.html) in the compiler).
+Here, `Type` is some representation of the Rust type system (akin to [`Ty`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc/ty/type.Ty.html) in the compiler).
 We can implement `TypedMemory` for any `Memory` as follows:
 * For `typed_write`, pick any representation of `val` for `ty`, and call `Memory::write`. If no representation exists, we have UB.
 * For `typed_read`, read `ty.size()` many bytes from memory, and then determine which value this list of bytes represents. If it does not represent any value, we have UB.
@@ -109,13 +116,13 @@ This also means that for types that have padding, the "typed copy" does not pres
 
 ## Relation to validity invariant
 
-One way we *could* also use the value representation (and the author things this is exceedingly elegant) is to define the validity invariant.
+One way we *could* also use the value representation (and the author thinks this is exceedingly elegant) is to define the validity invariant.
 Certainly, it is the case that if a list of bytes is not related to any value for a given type `T`, then that list of bytes is *invalid* for `T` and it should be UB to produce such a list of bytes at type `T`.
 We could decide that this is an "if and only if", i.e., that the validity invariant for a type is exactly "must be in the value representation".
 For many types this is likely what we will do anyway (e.g., for `bool` and `!` and `()` and integers), but for references, this choice would mean that *validity of the reference cannot depend on what memory looks like*---so "dereferencable" and "points to valid data" cannot be part of the validity invariant for references.
 The reason this is so elegant is that, as we have seen above, a "typed copy" already very naturally is UB when the memory that is copied is not a valid representation of `T`.
 This means we do not even need a special clause in our specification for the validity invariant---in fact, the term does not even have to appear in the specification---as everything juts falls out of how a "typed copy" applies the value representation twice.
 
-Justifying the `dereferencable` LLVM attribute is, in this case, left to the aliasing model (e.g. [Stacked Borrows]), just like that is needed to justify the `noalias` attribute.
+Justifying the `dereferencable` LLVM attribute is, in this case, left to the aliasing model (e.g. [Stacked Borrows]), just like the `noalias` attribute.
 
 [Stacked Borrows]: stacked-borrows.md