From 57b8ed596bffde3a008b8699bf438fb9987c623b Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 25 Jul 2019 20:00:33 +0200 Subject: [PATCH 1/3] glossary: define place, value, representation --- reference/src/glossary.md | 39 +++++++++++++++++++++++++++++++++++---- 1 file changed, 35 insertions(+), 4 deletions(-) diff --git a/reference/src/glossary.md b/reference/src/glossary.md index ef766057..4795ec31 100644 --- a/reference/src/glossary.md +++ b/reference/src/glossary.md @@ -177,10 +177,41 @@ zero-sized type", to refer to zero-sized types with an alignment requirement of For example, `()` is a "1-ZST" but `[u16; 0]` is not because it has an alignment requirement of 2. -### TODO +#### Place -* *rvalue* -* *lvalue* -* *representation* +A *place* (called "lvalue" in C and "glvalue" in C++) is the result of computing a [*place expression*][place-value-expr]. +A place is basically a pointer (pointing to some location in memory, potentially carrying [provenance](#pointer-provenance)), but might contain more information such as size or alignment (the details will have to be determined as the Rust Abstract Machine gets specified more precisely). +A place has a type. +Places cannot be "stored" in memory, only [values](#value) can. + +The key operations on a place are: +* storing a [value](#value) of the same type in it (when it is used on the left-hand side of an assignment), +* turning it into a [pointer value](#value) (when it is used inside `&expr`), +* and loading a [value](#value) of the same type from it (through the place-to-value coercion). + + +#### Value + +A *value* (called "value of the expression" or "rvalue" in C and "prvalue" in C++) is what gets stored in a [place](#place), and also the result of computing a [*value expression*][place-value-expr]. +A value has a type, and it denotes the abstract mathematical concept that is represented by data in our programs. +For example, a value of type `u8` is a mathematical integer in the range `0..256`. +Values can be (according to their type) turned into a list of bytes, which is called a [representation](#representation) of the value. +Values are ephemeral; they arise during the computation of an instruction but are only ever persisted in memory through their representation. +(This is comparable to how run-time data in a program is ephemeral and is only ever persisted in serialized form.) + +#### Representation (relation) + +A *representation* of a [value](#value) is a list of bytes that is used to store or "represent" that value in memory. + +We also sometimes speak of the *representation of a type*; this should more correctly be called the *representation relation* as it relates values of this type to lists of bytes that represent this value. +The term "relation" here is used in the mathematical sense: the representation relation is a predicate that, given a value and a list of bytes, says whether this value is represented by that list of bytes (`val -> list byte -> Prop`). + +The relation should be functional for a fixed list of bytes (i.e., every list of bytes has at most one associated representation). +It is partial in both directions: not all values have a representation (e.g. the mathematical integer `300` has no representation at type `u8`), and not all lists of bytes correspond to a value of a specific type (e.g. lists of the wrong size correspond to no value, and the list consisting of the single byte `0x10` corresponds to no value of type `bool`). +For a fixed value, there can be many representations (e.g., when considering type `#[repr(C)] Pair(u8, u16)`, the second byte is a padding byte so changing it does not affect the value represented by a list of bytes). + +See the [value domain][value-domain] for an example how values and representation relations can be made more precise. [stacked-borrows]: https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md +[value-domain]: https://github.com/rust-lang/unsafe-code-guidelines/tree/master/wip/value-domain.md +[place-value-expr]: https://doc.rust-lang.org/reference/expressions.html#place-expressions-and-value-expressions From 9c8bf98b27c02e5484992037e0ec4eb314e1e921 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Fri, 26 Jul 2019 09:16:51 +0200 Subject: [PATCH 2/3] explain what the type of a place does --- reference/src/glossary.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/reference/src/glossary.md b/reference/src/glossary.md index 4795ec31..3f60d9b7 100644 --- a/reference/src/glossary.md +++ b/reference/src/glossary.md @@ -181,12 +181,12 @@ requirement of 2. A *place* (called "lvalue" in C and "glvalue" in C++) is the result of computing a [*place expression*][place-value-expr]. A place is basically a pointer (pointing to some location in memory, potentially carrying [provenance](#pointer-provenance)), but might contain more information such as size or alignment (the details will have to be determined as the Rust Abstract Machine gets specified more precisely). -A place has a type. -Places cannot be "stored" in memory, only [values](#value) can. +A place has a type, indicating the type of [values](#value) that it stores. +Places cannot be "stored" in memory, only values can. The key operations on a place are: * storing a [value](#value) of the same type in it (when it is used on the left-hand side of an assignment), -* turning it into a [pointer value](#value) (when it is used inside `&expr`), +* turning it into a [pointer value](#value) (when it is used inside `&expr`), which is also the only way to "store" a place, * and loading a [value](#value) of the same type from it (through the place-to-value coercion). @@ -194,6 +194,7 @@ The key operations on a place are: A *value* (called "value of the expression" or "rvalue" in C and "prvalue" in C++) is what gets stored in a [place](#place), and also the result of computing a [*value expression*][place-value-expr]. A value has a type, and it denotes the abstract mathematical concept that is represented by data in our programs. + For example, a value of type `u8` is a mathematical integer in the range `0..256`. Values can be (according to their type) turned into a list of bytes, which is called a [representation](#representation) of the value. Values are ephemeral; they arise during the computation of an instruction but are only ever persisted in memory through their representation. From f0511a21403bdf59ac976a79a5eaf0ea3192d7b1 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 27 Jul 2019 08:58:19 +0200 Subject: [PATCH 3/3] place ops --- reference/src/glossary.md | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/reference/src/glossary.md b/reference/src/glossary.md index 3f60d9b7..cc0972f6 100644 --- a/reference/src/glossary.md +++ b/reference/src/glossary.md @@ -182,13 +182,12 @@ requirement of 2. A *place* (called "lvalue" in C and "glvalue" in C++) is the result of computing a [*place expression*][place-value-expr]. A place is basically a pointer (pointing to some location in memory, potentially carrying [provenance](#pointer-provenance)), but might contain more information such as size or alignment (the details will have to be determined as the Rust Abstract Machine gets specified more precisely). A place has a type, indicating the type of [values](#value) that it stores. -Places cannot be "stored" in memory, only values can. The key operations on a place are: -* storing a [value](#value) of the same type in it (when it is used on the left-hand side of an assignment), -* turning it into a [pointer value](#value) (when it is used inside `&expr`), which is also the only way to "store" a place, -* and loading a [value](#value) of the same type from it (through the place-to-value coercion). - +* Storing a [value](#value) of the same type in it (when it is used on the left-hand side of an assignment). +* Loading a [value](#value) of the same type from it (through the place-to-value coercion). +* Converting between a place (of type `T`) and a pointer value (of type `&T`, `&mut T`, `*const T` or `*mut T`) using the `&` and `*` operators. + This is also the only way a place can be "stored": by converting it to a value first. #### Value