Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add dynamic.layout chapter #15

Closed
wants to merge 14 commits into from
Closed

Conversation

chorman0773
Copy link
Contributor

@chorman0773 chorman0773 commented Feb 27, 2024

This specifies the layouts, representation, and validity invariants of all core language types. It also includes the Guaranteed Discriminant Ellision for Option and Result.

Questions for teams (to be sent directly at a future date):

  • T-opsem: What is the validity invariant of union
  • T-opsem: Do enums need to be able to represent a field of a variant that can never have all fields valid (IE. can enum Foo{Bar(i32, Infallible), Baz} be zero sized in theory)?
  • T-lang: Is the underlying type of DynMetadata<dyn Trait> correct as *const ()?
  • T-lang: Is the layout of #[repr(align(N)] struct Foo{} guaranteed to be size=0, align=N? Is this true for only chosen N values (such as N=1)?
  • T-lang: Are there guarantees about layout of empty enums? Enums with only one variant and no repr? Enums with only one variant with no fields?


[!NOTE]: The minimum size of a type is `0`, and the minimum alignment requirement is `1`. A type that has size `0` and alignment requirement `1` is called a 1-ZST.

[§](r[dynamic.layout.properties.storage]) Storage for a value is suitable for storing a value of a `Sized` type if it is at least the size of that type and the address of the start of the storage satisfies the alignment requirement.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You forgot to define what it means to "satisfy the alignment requirement", the spec only ever said it was a pow2 number


[§](r[dynamic.layout.scalar.int-size]) Each integer type of width `N` has a size exactly equal to `N/8`.

[1NOTE]: The width of the integer type `uN` or `iN` is `N`.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

typo !NOTE


[§](r[dynamic.layout.aggregate.struct-base] The fields of a `struct` definition are each layed at offsets that ensure that each field occupies nonoverlapping storage, which, unless modified by the `repr(packed)` attribute (r#[dynamic.layout.aggregate.packed])) is suitably aligned. The size of a `struct` definition is at least sufficient to store each field, and the alignment requirement of a `struct` definition, unless modified by the `repr(packed)` attribute, is suitable to align each field.

[!NOTE]: The offsets of the fields, sizes, and alignment requirements of two different `struct` types, even with the same field types in the same order, may be different.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

maybe say "same source order" here? Not sure if that's an existing concept

even with the same field types in the same declaration order, may be different unless modified by the repr(C) attribute.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Source order is probably fine since it's it's a note.


[§](r[dynamic.layout.aggregate.repr-packed]) A `struct` or `union` definition with a `repr(packed(N))` repr-attribute, where `N` is an integer power of 2 up to a target-defined value, sets the alignment requirement of each field to the smallest of the alignment requirement of the type and `N`. The `repr(packed(N))` repr-attribute may not be combined with any `repr(align(N))` repr-attributes.

[!NOTE]: The repr-attribute `repr(packed(1))` may be written as `repr(packed)`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think this needs to be normative. dynamic.layout.aggregate.repr-packed-short-form

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That will probably get handled at a higher level, and the note is just there for people just reading the layout section.


[§](r[dynamic.layout.dyn.metadata-validity]) The validity invariant of the vptr type is unspecified, such that the result of unsizing a type as the trait object `dyn Trait+Markers` is valid.

[§](r[dynamic.layout.dyn.metadata-size-align]) The size and alignment requirement acessible from a value of the vptr type obtained as the result of unsizing a type as the trait object `dyn Trait+Markers` is valid are the size and alignment of that type.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

delete "is valid"

[§](r[dynamic.layout.enum.option]) The special type `Option<T>` is an enum type, such that if `T` is one of the following types or a type with an underlying type that is one of the following (recursively), it has the corresponding underlying type.
* `&T`: `*const T`
* `&mut T`: `*mut T`
* fn-ptr type: An unspecified, exposition-only, type with the same size and alignment as `fn()` that is valid for any initialized value
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I can't tell whether or not this accidentally restricts the value from carrying pointer parts. Add more words to clarify


[§](r[dynamic.layout.enum.option-ref-validity]) A value of type `Option<&T>` or `Option<&mut T>` is valid if it corresponds to a pointer with address `0`, or a pointer with an address that satisfies the dynamic alignment requirement of `T`.

[§](r[dynamic.layout.enum.result]) The special type `Result<T,E>` where `E` has size 0 and alignment 1, and `T` is a type mentioned in r#[dynamic.layout.enum.option], then `Result<T,E>` has an underlying type of `Option<T>`. The special type `Result<T,E>` where `T` has size 0 and alignment 1, and `E` is a type mentioned in r#[dynamic.layout.enum.option], then `Result<T,E>` has an underlying type of `Option<T>`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Final type mentioned should be Option<E>


[§](r[dynamic.layout.enum.result]) The special type `Result<T,E>` where `E` has size 0 and alignment 1, and `T` is a type mentioned in r#[dynamic.layout.enum.option], then `Result<T,E>` has an underlying type of `Option<T>`. The special type `Result<T,E>` where `T` has size 0 and alignment 1, and `E` is a type mentioned in r#[dynamic.layout.enum.option], then `Result<T,E>` has an underlying type of `Option<T>`

[§](r[dynamic.layout.enum.result-repr]) Where `Result<T,E>` is a type referred to by r#[dynamic.layout.enum.result] The representation of the value `Err(e)` of type `Result<T,E>` is the same as the representation for `Some(e)` of type `Option<E>` if `T` has size 0 and alignment 1, and `None` of type `Option<T>` otherwise, and the representation of `Ok(t)` of type `Result<T,E>` is the same as the representation for `Some(t)` of type `Option<T>` if `E` has size 0 and alignment 1, and `None` of the type `Option<E>` otherwise.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please describe all the restrictions before the requirements, and also make Option<T> the first in the paragraph and Option<E> the second.

Copy link

@hawkinsw hawkinsw left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for your great work! I hope that following comments are helpful!

spec/dynamic/layout.md Outdated Show resolved Hide resolved
spec/dynamic/layout.md Outdated Show resolved Hide resolved

[§](r[dynamic.layout.pointer.size-align]) The size and alignment of a thin pointer is the same as the size and alignment of `usize`.

[!NOTE] All thin pointers have the same

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Seems to be missing something here.


[!NOTE] All thin pointers have the same

[§](r[dynamic.layout.pointer.repr]) The address of a pointer value is the same as the value of type `usize` computed from the same bytes. The pointer tag of a pointer value is each pointer portion of each byte of the representation.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
[§](r[dynamic.layout.pointer.repr]) The address of a pointer value is the same as the value of type `usize` computed from the same bytes. The pointer tag of a pointer value is each pointer portion of each byte of the representation.
[§](r[dynamic.layout.pointer.repr]) The target of a pointer value is the same as the value of type `usize` computed from the same bytes. The pointer tag of a pointer value is each pointer portion of each byte of the representation.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

address is a term used elsewhere in rust. For example, under the strict provenance API, there are functions to extract the address part that use the name address.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

address is a term used elsewhere in rust. For example, under the strict provenance API, there are functions to extract the address part that use the name address.

Totally understand that. I was just trying to make some language to "show" the reader that the value (in this case) is what determines the target.

Although, now that I reread it, I think that I understand the reason for the use of address: the reader will know (from other places in the standard) that the term identifies the thing being pointed to/at.

Sorry for the spam!

spec/dynamic/layout.md Outdated Show resolved Hide resolved
spec/dynamic/layout.md Outdated Show resolved Hide resolved
Co-authored-by: Will Hawkins <whh8b@obs.cr>

[§](r[dynamic.layout.enum.result-repr]) Where `Result<T,E>` is a type referred to by r#[dynamic.layout.enum.result] The representation of the value `Err(e)` of type `Result<T,E>` is the same as the representation for `Some(e)` of type `Option<E>` if `T` has size 0 and alignment 1, and `None` of type `Option<T>` otherwise, and the representation of `Ok(t)` of type `Result<T,E>` is the same as the representation for `Some(t)` of type `Option<T>` if `E` has size 0 and alignment 1, and `None` of the type `Option<E>` otherwise.
[§](r[dynamic.layout.enum.result-repr]) Where `Result<T,E>` is a type referred to by r#[dynamic.layout.enum.result], if `E` is of size 0 and alignment 1, the representation of `Ok(t)` of type `Result<T,E>` is the same as the representation of `Some(t)` of type `Option<T>` and the represention of `Err(e)` is the same as the representation of `None` of type `Option<T>`. Otherwise, the representation of `Ok(t)` of type `Result<T,E>` is the same as the representation of `None` of type `Option<E>` and the representation of `Err(e)` of type `Result<T,E>` is the same as the representation of `Some(e)` of type `Option<E>`
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Otherwise, where T is of size 0 and alignment 1,

Restating the condition for avoidance of editing mistakes, but using "where" instead of "if" because this is actually exhaustive.

@chorman0773
Copy link
Contributor Author

This is currently blocked on rust-lang/unsafe-code-guidelines#494.


[!NOTE]: Scalar types and pointer types have no padding bytes.

[§](r[dynamic.layout.properties.validity]) Each `Sized` type has a validity invariant, which constrains the values that can be read from storage. Only value bytes are taken into account in determining the validity of a value.
Copy link
Member

@RalfJung RalfJung Mar 5, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is not following t-opsem terminology and also not following the structure that we've been exploring with MiniRust. I don't think the spec should be structured like this. I don't think the spec should even define validity directly; it should define the representation from which validity then follows.

See here and here for some t-opsem definitions, and here for further Zulip discussion on this concern.


[§](r[dynamic.layout.properties.storage]) Storage for a value is suitable for storing a value of a `Sized` type if it is at least the size of that type and the address of the start of the storage satisfies the alignment requirement.

[§](r[dynamic.layout.properties.representation]) Each `Sized` type has a representation which determines how particular values of that type are layed out when read from or written to suitable storage. The representation of a type is exactly its size.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The representation of a type is exactly its size.

I don't know what this means, a representation is a lot more than just the size?

From this definition I can't even tell if you mean what t-opsem calls "layout" or what we call "representation". I think you need to be more clear about what the types are of the object that you are defining.

"representation", in the t-opsem meaning, is a relation between values and byte lists. It encodes a ton of things, not just layout aspects but also validity.

"layout" is much more first-order, it stores concrete data. For instance, the "layout" of a struct is given by the offsets of all its fields as well as the total size and alignment of the struct. I think this chapter should only do layout, not representation (and therefore also not validity). Something like:

Each Sized type has an associated layout that stores all the information required to lay out the type in memory.

Note: The layout is then used by the [representation] to determine how [values] are related to lists of bytes that represent the value in memory.

(I think unsized types may actually also have layout but I'm okay with deferring this to later, I haven't yet explored unsized types in MiniRust)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is trying to encode that the list of bytes that any value becomes is exactly as long as the size property of the type.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is trying to prescribe that the list of bytes that any value becomes is exactly as long as the size property of the type.

Copy link
Member

@RalfJung RalfJung Mar 11, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, okay. In English I would state this as "The length of the representation of a type is equal to the size of the type." Somewhere further up it should have stated what a representation is: "A representation is a list of Bytes", linking to wherever it is defined what a "byte" is.

But again this really screams that it wants to be stated in a notation that is more suited for precise statements than English...

@JoelMarcey JoelMarcey added C-tooling Category: Discussion/Changes related to custom mdbook tooling A-dynamic-layout Area: Related to the Layout/Representation Dynamic Semantics Chapter and removed C-tooling Category: Discussion/Changes related to custom mdbook tooling labels Mar 15, 2024
@chorman0773
Copy link
Contributor Author

Given that we're starting with the reference and won't be working in the spec repo any more, I'm going to close this PR.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
A-dynamic-layout Area: Related to the Layout/Representation Dynamic Semantics Chapter
Development

Successfully merging this pull request may close these issues.

5 participants