You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: wip/memory-interface.md
+28-6
Original file line number
Diff line number
Diff line change
@@ -11,6 +11,7 @@ The interface is also opinionated in several ways; this is not intended to be ab
11
11
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).
12
12
Another key property of the interface presented below is that it is *untyped*.
13
13
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.
14
+
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.
14
15
15
16
## Pointers
16
17
@@ -36,7 +37,7 @@ enum Byte<Pointer> {
36
37
/// The pointer of which this is a byte.
37
38
ptr:Pointer,
38
39
/// Which byte of the pointer this is.
39
-
/// `idx` will always be in `0..size_of::<usize>()`.
40
+
/// `idx` will always be in `0..PTR_SIZE`.
40
41
idx:u8,
41
42
}
42
43
}
@@ -48,21 +49,39 @@ On a 32-bit system, the sequence of 4 bytes representing `ptr: Pointer` is:
Copy file name to clipboardExpand all lines: wip/value-domain.md
+5-4
Original file line number
Diff line number
Diff line change
@@ -4,7 +4,8 @@
4
4
5
5
The purpose of this document is to describe what the set of *all possible values* is in Rust.
6
6
This is an important definition: one key element of a Rust specification will be to define the [representation relation][representation] of every type.
7
-
This relation relates values with lists of bytes, so before we can even start specifying the relation we have to specify the involved domains.
7
+
This relation relates values with lists of bytes: it says, for a given value and list of bytes, if that value is represented by that list.
8
+
However, before we can even start specifying the relation, we have to specify the involved domains.
8
9
`Byte` is defined as part of [the memory interface][memory-interface]; this document is about defining `Value`.
@@ -45,7 +46,7 @@ We show some examples for how one might want to use this `Value` domain to defin
45
46
46
47
### `bool`
47
48
48
-
The value relation for `bool` relates `Bool(true)` with `[Raw(0)]` and `Bool(false)` with [`Raw(1)`], and that's it.
49
+
The value relation for `bool` relates `Bool(b)` with `[bb]`if and only if `bb.as_int() == Some(if b { 1 } else { 0 })`.
49
50
50
51
### `()`
51
52
@@ -72,12 +73,12 @@ It also shows that the actual content of the padding bytes is entirely irrelevan
72
73
73
74
Reference types are tricky.
74
75
But a possible value relation for sized `T` is:
75
-
A value `Ptr(ptr)` is related to `[PtrFragment { ptr, idx: 0 }, ..., PtrFragment { ptr, idx: N-1 }]`where `N == size_of::<usize>()`if `ptr` is non-NULL and aligned to `align_of::<T>()`.
76
+
A value `Ptr(ptr)` is related to `[PtrFragment { ptr, idx: 0 }, ..., PtrFragment { ptr, idx: PTR_SIZE-1 }]` if `ptr` is non-NULL and appropriately aligned (defining alignment is left open for now).
76
77
77
78
### `u8`
78
79
79
80
For the value representation of integer types, there are two different reasonable choices.
80
-
Certainly, a value `Int(i)` where `i` in `0..256` is related to `[Raw(i as u8)]`.
81
+
Certainly, a value `Int(i)` where `i` in `0..256` is related to `[b]` if `b.as_int() == Some(i)`.
81
82
82
83
And then, maybe, we also want to additionally say that value `Uninit` is related to `[Uninit]`.
83
84
This essentially corresponds to saying that uninitialized memory is a valid representation of a `u8` value (namely, the uninitialized value).
0 commit comments