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

[type-layout] Document bit validity of structs and padding #1630

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 17 additions & 0 deletions src/type-layout.md
Original file line number Diff line number Diff line change
Expand Up @@ -91,6 +91,7 @@ Slices have the same layout as the section of the array they slice.
> etc.) to slices.

## `str` Layout

String slices are a UTF-8 representation of characters that have the same layout as slices of type `[u8]`.

## Tuple Layout
Expand Down Expand Up @@ -589,6 +590,22 @@ primitive field will have the ABI of the primitive field.
Because this representation delegates type layout to another type, it cannot be
used with any other representation.

## Bit validity of composite types

Each Rust type has "bit validity", which is the set of bit patterns which may
appear in a value of that type. It is [undefined behavior] to produce a value
Comment on lines +595 to +596
Copy link
Contributor

Choose a reason for hiding this comment

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

This may be better in its own section about bit validity in general, rather than introducing the concept in its entirety in a section specifically about composite types.

of a type which violates bit validity (in other words, to initialize a value
to a bit pattern which is not in that type's set of valid bit patterns).
Note that the total set of possible bit patterns for any given byte has 257
elements - 256 initialized bit patterns and one "uninitialized" bit pattern.
Comment on lines +599 to +600
Copy link
Contributor

Choose a reason for hiding this comment

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

This does not include provenance-carrying bytes, which are complicated.

I'd either briefly mention them, or omit this paragraph entirely.


The bit validity of a struct type is the composition of the bit validities
of its fields.

Padding bytes have no bit validity requirement: it is always well-defined
to write any byte value - including an uninitialized byte - to any byte of
padding.
Comment on lines +605 to +607
Copy link
Contributor

Choose a reason for hiding this comment

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

Could be useful to mention that padding bytes will get overwritten whenever a struct value is moved. I don't remember if we mentioned it elsewhere in the chapter though - if it's already there, I don't think it needs to be duplicated here.

Copy link
Contributor Author

@joshlf joshlf Oct 10, 2024

Choose a reason for hiding this comment

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

Looks like there are no existing docs for typed copies (cc @RalfJung). Perhaps we could add a section documenting them?

Copy link
Member

@RalfJung RalfJung Oct 10, 2024

Choose a reason for hiding this comment

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

IMO we ultimately shouldn't document bit validity at all. Bit validity is a derived concept. What actually matters is

  • decoding a low-level representation into a high-level value
  • and inverting that: encoding the value back into a low-level representation

"bit validity" is just the precondition for decoding to be well-defined. If we define decoding, that implicitly defines bit validity as well. But the decode/encode pair also explains other things like padding (and sometimes provenance) being lost on a typed copy.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

IMO bit validity (at least as I've used it) is a tad stronger than that: it also permits unsafe code to assume that it won't see certain values produced by safe Rust. That implies that it also constrains what low-level representations can be produced by the "encoding" operation you described.

I don't see any reason why explicitly documenting encoding and decoding separately is a problem. I'd just want to make sure we can still derive the stronger notion of bit validity that I described from whatever guarantees are made regarding encoding and decoding.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

@chorman0773

It does not permit that, no, as we can relax validity invariants.

Does that hold for bit validities which are explicitly documented? E.g., would we consider unsafe code which assumes that a bool can only be 0 or 1 [1] to be unsound?

[1] https://doc.rust-lang.org/reference/types/boolean.html:

The value false has the bit pattern 0x00 and the value true has the bit pattern 0x01. It is undefined behavior for an object with the boolean type to have any other bit pattern.

Copy link
Member

@RalfJung RalfJung Oct 11, 2024

Choose a reason for hiding this comment

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

IMO bit validity (at least as I've used it) is a tad stronger than that: it also permits unsafe code to assume that it won't see certain values produced by safe Rust. That implies that it also constrains what low-level representations can be produced by the "encoding" operation you described.

That's not a good idea. Whenever unsafe code permits inputs to not satisfy the safety invariant, that code should document what it actually requires. We can and will change validity rules to allow more values, which removes UB and is hence not considered a breaking change. If someone defines an unsafe function with precondition "anything goes, even if it breaks the safety invariant, as long as it satisfies the validity invariant", that unsafe code can become unsound through such a spec change.

I don't see any reason why explicitly documenting encoding and decoding separately is a problem.

It's fully redundant, and therefore makes it harder to form a mental model of this part of unsafe Rust. It makes it seem like one has to learn the encode/code part and the bit validity rules, when that is not actually necessary.

Copy link
Member

Choose a reason for hiding this comment

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

E.g., would we consider unsafe code which assumes that a bool can only be 0 or 1 [1] to be unsound?

That's a question about safety invariants, which are a type system concern, not about validity invariant (which are an opsem concern). It is easier to consider this question with &str since there, validity != safety: it is documented that this is valid UTF-8, so unsafe code may rely on that. But this has nothing to do with validity, and it is in fact not immediate UB to violate the UTF-8 property.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

I don't see any reason why explicitly documenting encoding and decoding separately is a problem.

It's fully redundant, and therefore makes it harder to form a mental model of this part of unsafe Rust. It makes it seem like one has to learn the encode/code part and the bit validity rules, when that is not actually necessary.

Sorry, to clarify, I was agreeing with you here 🙂 Namely, that (for our purposes) just defining encoding/decoding and not mentioning bit validity is fine.

IMO bit validity (at least as I've used it) is a tad stronger than that: it also permits unsafe code to assume that it won't see certain values produced by safe Rust. That implies that it also constrains what low-level representations can be produced by the "encoding" operation you described.

That's not a good idea. Whenever unsafe code permits inputs to not satisfy the safety invariant, that code should document what it actually requires. We can and will change validity rules to allow more values, which removes UB and is hence not considered a breaking change. If someone defines an unsafe function with precondition "anything goes, even if it breaks the safety invariant, as long as it satisfies the validity invariant", that unsafe code can become unsound through such a spec change.

E.g., would we consider unsafe code which assumes that a bool can only be 0 or 1 [1] to be unsound?

That's a question about safety invariants, which are a type system concern, not about validity invariant (which are an opsem concern). It is easier to consider this question with &str since there, validity != safety: it is documented that this is valid UTF-8, so unsafe code may rely on that. But this has nothing to do with validity, and it is in fact not immediate UB to violate the UTF-8 property.

Okay so IIUC, code which assumes (for soundness) that bools are 0x00 or 0x01 is sound, but only in virtue of the fact that bools have a safety invariant of only being 0 or 1? I think that's fine for our purposes.


I do have a more general concern, though.

It seems to me that, as it currently stands, we don't clearly specify in documentation which things are intended to document validity and which are intended to document safety, and furthermore, we don't clearly specify which are merely preconditions (which we could relax in the future) and which are postconditions (which would be a breaking change to relax).

As an example, consider the Reference page on bools:

The value false has the bit pattern 0x00 and the value true has the bit pattern 0x01. It is undefined behavior for an object with the boolean type to have any other bit pattern.

Clearly this is documenting a precondition for soundness, but is it also documenting a safety invariant? Saying "the value false has the bit pattern 0x00 and the value true has the bit pattern 0x01" seems to me to be a promise, but maybe it wasn't intended that way.

The stdlib docs are even more nebulous:

If you cast a bool into an integer, true will be 1 and false will be 0.

Is there some nomenclature convention I'm missing here, or is it just that we haven't gotten around to making our language consistent? Not that it's specifically your responsibility to own this or anything, but I think it's worth stating for the record: the ambiguity of the language - and especially ambiguity which allows preconditions to be misinterpreted as postconditions or invariants - makes it hard for external authors to be confident that they're writing unsafe code correctly. Writing unsafe code is my full-time job and I still keep running into situations where I thought I understood what was being promised only to learn that I was misreading the text.

Copy link
Member

Choose a reason for hiding this comment

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

Okay so IIUC, code which assumes (for soundness) that bools are 0x00 or 0x01 is sound, but only in virtue of the fact that bools have a safety invariant of only being 0 or 1? I think that's fine for our purposes.

Yes.

It seems to me that, as it currently stands, we don't clearly specify in documentation which things are intended to document validity and which are intended to document safety,

Indeed. So far we haven't stably committed to this dichotomy of invariants, and more importantly, we haven't stably committed to how these two invariants are called. Personally I regret calling them "validity invariant" and "safety invariant"; I now think that "language invariant" and "library invariant" are better terms. They go along nicely with the terms "language UB" and "library UB" that we have also been using already (but also not documented stably yet -- mostly because nobody had the time to write that text, I think).

I opened rust-lang/unsafe-code-guidelines#539 to hopefully make progress on this question.


[`align_of_val`]: std::mem::align_of_val
[`size_of_val`]: std::mem::size_of_val
[`align_of`]: std::mem::align_of
Expand Down