Skip to content

Commit

Permalink
Define immutability UB in terms of bytes
Browse files Browse the repository at this point in the history
This is part of the feedback on #1385.

Ralf made the point that the immutability definition could be restated
solely in terms of bytes, which has the added benefit of no longer
requiring the note on padding (since it's a natural consequence of the
byte version.)

The new wording for shared references also clarifies the case of mutable
references behind shared ones, and reintroduces some of the transitivity
property that I removed in my previous commit. The wording is separate
from that for immutable bindings, since those don't have transitive
immutability.

This also bumps the definition of bytes pointed to by references and
pointers into its own subsection, so that it can be linked to by the UB
definition, to avoid duplication.

Co-authored-by: Ralf Jung <post@ralfj.de>
  • Loading branch information
ivanbakel and RalfJung committed Jul 24, 2023
1 parent 69a6f70 commit 70886e3
Showing 1 changed file with 14 additions and 7 deletions.
21 changes: 14 additions & 7 deletions src/behavior-considered-undefined.md
Original file line number Diff line number Diff line change
Expand Up @@ -42,12 +42,14 @@ code.
All this also applies when values of these
types are passed in a (nested) field of a compound type, but not behind
pointer indirections.
* Mutating immutable data. All bytes inside a [`const`] item are immutable.
Moreover, the bytes of a value pointed to by a shared reference, or bytes owned by an immutable binding are immutable, unless those bytes are part of an [`UnsafeCell<U>`].
Immutability also affects bytes which are not reachable from safe code, such as padding; it also affects uninitialized bytes.
* Mutating immutable bytes. All bytes inside a [`const`] item are immutable.
The bytes owned by an immutable binding are immutable, unless those bytes are part of an [`UnsafeCell<U>`].

Moreover, the bytes [pointed to] by a shared reference, including transitively through other references (both shared and mutable) and `Box`es, are immutable: transitivity includes those references stored in fields of compound types.

A mutation is any write of more than 0 bytes which overlaps with any of the relevant bytes.
Writes which do not modify the byte contents (i.e. writes of a byte's value to that byte) are still mutations.

> **Note**: Writes which do not modify the byte contents (i.e. writes of a byte's value to that byte) are still mutations.
* Invoking undefined behavior via compiler intrinsics.
* Executing code compiled with platform features that the current platform
does not support (see [`target_feature`]), *except* if the platform explicitly documents this to be safe.
Expand Down Expand Up @@ -94,13 +96,16 @@ reading uninitialized memory is permitted are inside `union`s and in "padding"
> vice versa, undefined behavior in Rust can cause adverse affects on code
> executed by any FFI calls to other languages.
### Pointed-to bytes

The span of bytes a pointer or reference "points to" is determined by the pointer value and the size of the pointee type (using `size_of_val`).

### Dangling pointers
[dangling]: #dangling-pointers

A reference/pointer is "dangling" if it is null or not all of the bytes it
points to are part of the same live allocation (so in particular they all have to be
part of *some* allocation). The span of bytes it points to is determined by the
pointer value and the size of the pointee type (using `size_of_val`).
[points to] are part of the same live allocation (so in particular they all have to be
part of *some* allocation).

If the size is 0, then the pointer must either point inside of a live allocation
(including pointing just after the last byte of the allocation), or it must be
Expand All @@ -124,3 +129,5 @@ must never exceed `isize::MAX`.
[dereference expression]: expressions/operator-expr.md#the-dereference-operator
[place expression context]: expressions.md#place-expressions-and-value-expressions
[rules]: inline-assembly.md#rules-for-inline-assembly
[points to]: #pointed-to-bytes
[pointed to]: #pointed-to-bytes

0 comments on commit 70886e3

Please sign in to comment.