nail down the final validity rules: references and unions

[RalfJung]

This translates the following t-opsem FCPs into Reference text:

• Should validity of a reference depend on the *contents* of memory in any way? unsafe-code-guidelines#414 (comment)
• Can references to uninhabited types ever be valid? unsafe-code-guidelines#413 (comment)
• What are the values of a union type? (in particular, what is the validity invariant of a union) unsafe-code-guidelines#438 (comment)

Cc @rust-lang/opsem

@rust-lang/lang you have not FCP'd this yet; please let us know if you want this to go through your own decision process as well.

Fixes rust-lang/unsafe-code-guidelines#413
Fixes rust-lang/unsafe-code-guidelines#414
Fixes rust-lang/unsafe-code-guidelines#438

[RalfJung]

@rustbot label +I-lang-nominated

[RalfJung]

A proposal came up in rust-lang/unsafe-code-guidelines#620 to slightly strengthen the requirements for references / Box to types with a slice tail.

@scottmcm do you have suggestions for how that should be worded?

[RalfJung]

These two lines are for rust-lang/unsafe-code-guidelines#620. We didn't explicitly discuss this case in the opsem FCP.

View changes since the review

[scottmcm]

do you have suggestions for how that should be worded?

I don't have anything concrete.

At least as a mental model -- whether it can be phrased well for a reference I'm less sure -- I wonder if there's a general rule here like saying that the type in the reference must, including looking at the metadata, represent a well-formed and inhabited type. (Part of me wants to say it comes from an unsizing, but there's nothing to unsize to a struct Foo(u32, [f64]); kind of thing, so I don't think that works, but maybe someone can come up with a cleverer phrasing.)

Basically I wish the "length has to be zero for uninhabited elements" and "length bound for non-ZST elements is usize::MAX / sizeof(T)" kinds of things were just corollaries of the general rule, to avoid things like the rust-lang/unsafe-code-guidelines#620 (comment) concern.

[RalfJung]

So what do you think about the wording I put in this PR?

[traviscross]

Thanks @RalfJung. We talked about this in the lang meeting and agreed we'd expect a lang FCP here if we're changing the language.

@rfcbot fcp merge lang

(Eliding opsem here as it's already been FCPed by the opsem team.)

[rust-rfcbot]

@traviscross has proposed to merge this. The next step is review by the rest of the tagged team members:

• @joshtriplett
• @nikomatsakis
• @scottmcm
• @tmandry
• @traviscross

No concerns currently listed.

Once a majority of reviewers approve (and at most 2 approvals are outstanding), this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

cc @rust-lang/lang-advisors: FCP proposed for lang, please feel free to register concerns.
See this document for info about what commands tagged team members can give me.

[joshtriplett]

I reviewed the proposed rules both for unions and for references, and this looks reasonable to me.

@rfcbot reviewed

[scottmcm]

This makes me want a separate language construct for "no, I'm not doing partial overwrite silliness" because this rule has meant that unions are not usable for the cases I wanted, but if this is the right answer for FFI unions and such then so be it.

@rfcbot reviewed

[rust-rfcbot]

🔔 This is now entering its final comment period, as per the review above. 🔔

[RalfJung]

(Eliding opsem here as it's already been FCPed by the opsem team.)

FWIW the unsized type part hasn't been FCP'd by us yet, as mentioned above. We can do that in a separate issue or a joint FCP here.

[traviscross]

@rfcbot fcp cancel

[rust-rfcbot]

@traviscross proposal cancelled.

[traviscross]

Thanks @RalfJung.

@rfcbot fcp merge lang,opsem

(In addition to what was previously FCPed by opsem, opsem is signing off here on what RalfJ mentions in #2337 (comment).)

[rust-rfcbot]

@traviscross has proposed to merge this. The next step is review by the rest of the tagged team members:

• @CAD97
• @RalfJung
• @digama0
• @joshlf
• @joshtriplett
• @nikomatsakis
• @saethlin
• @scottmcm
• @tmandry
• @traviscross

No concerns currently listed.

Once a majority of reviewers approve (and at most 2 approvals are outstanding), this will enter its final comment period. If you spot a major issue that hasn't been raised at any point in this process, please speak up!

cc @rust-lang/lang-advisors: FCP proposed for lang, please feel free to register concerns.
See this document for info about what commands tagged team members can give me.

[RalfJung]

@rfcbot reviewed

[RalfJung]

FWIW @saethlin has ticked their box in rust-lang/unsafe-code-guidelines#620, that should be carried over.

[saethlin]

@rfcbot reviewed

[WaffleLapkin]

I feel like making inhabitedness depend on metadata values is not right / clean.

I would rather make this a separate restriction on the value of the metadata. That is, I would say something along the lines of "A reference or Box<T> must ... have valid metadata" and "slice metadata for a slice type with uninhabited elements, it must be 0".

This allows adding other restrictions in the future, such as the one mentioned by @scottmcm that slice metadata can at most be usize::MAX / size_of::<T>() (for non-ZSTs).

View changes since the review

[RalfJung]

We generally pretty consistently treat the metadata as telling us the "actual type" that we use to inspect the pointee. I think it would be odd do do something else here. It would look like an arbitrary set of rules, rather than just something that falls out of a more general principle.

This allows adding other restrictions in the future, such as the one mentioned by @scottmcm that slice metadata can at most be usize::MAX / size_of::() (for non-ZSTs).

As I mentioned in reply to Scott, that restriction is already present. It follows from the fact that the reference has to be dereferenceable for its actual dynamic size.

[WaffleLapkin]

Hm. It still feels weird to me to do it this way for slices, but if we are consistently doing it this way I suppose that is better.

I suppose the reason it feels weird to me is that in the compiler "inhabitedness" is a property of types, and does not concern the value in any way. If we would like exploit this UB in the compiler, we would have to add an arbitrary rule in the form of "if the tail is a slice of an uninhabited type, assume(len == 0)".

In a way, considering the "actual type" feels more arbitrary to me.

That being said, I imagine we have to consider the "actual type" for trait objects, at which point it's better do the same thing for slices too.

(I'd resolve this conversation, but it appears I don't have permissions for that)

[RalfJung]

The compiler can only statically approximate all these properties using the types, yes. But that's expected, everything on this page is written assuming full knowledge of the current dynamic state (think: Miri, MiniRust). The compiler might get better at approximating things and that should not change the spec!

IOW, I think you're thinking too much like a compiler writer and not enough like a language specifier. :)

[WaffleLapkin]

guilty as charged I'm afraid ^^'

[RalfJung]

I think it is part of inhabitedness. I view inhabitedness as a property of a potentially unsized type and metadata. We use the metadata to figure out what the actual dynamic type is, and then evaluate inhabitedness of that.

That's what it's going to look like in Miri and MiniRust, and IMO it's the structure we should also follow here. I thought it was okay to leave that implicit, but I see that it is too confusing, so I will try to reword.

[digama0]

No, that much I agree with; the part I disagree with is that the consequence is about inhabitedness (of a type). For a type like &dyn NeverImplements, obviously it's going to be inhabited since any types could be implementing NeverImplements. What we want to say is that the value [ptr, never_vtable]: &dyn NeverImplements is invalid, for the reason that the vtable is for a type that is uninhabited. For the unsized type dyn NeverImplements itself, that's a whole separate question, I'm not really sure what validity/inhabitedness means for unsized types since they don't exist on their own but the natural reading is that it is still inhabited, and it has "values" only after fixing the metadata, and there are no valid values which have never_vtable as the metadata.

The reasoning for the present case is similar: if U is uninhabited, then [U; 1] is uninhabited and &[U; 1] is uninhabited and &[U] is inhabited but has only the valid value len = 0; the value [ptr, 1]: &[U] is not valid for the type regardless of ptr. If you would like to say that the type [U] is "uninhabited at len=1" then that's fine but a new concept we haven't discussed before, and also apparently the same thing as just saying [U; 1] is uninhabited.

[RalfJung]

What is being defined here is whether dyn NeverImplements is inhabited. Which depends on the metadata, just like inhabitedness of [!].

[RalfJung]

If you would like to say that the type [U] is "uninhabited at len=1" then that's fine but a new concept we haven't discussed before,

That's exactly what I mean and what I thought we had discussed: for unsized types, inhabitedness depends on the metadata. Slices are inhabited iff the length is 0 or the element type is inhabited. dyn Trait is inhabited iff the actual dynamic type represented in the metadata is inhabited.

[RalfJung]

I have reworded this part to hopefully make it more clear.

[Jules-Bertholet]

In https://rust-lang.zulipchat.com/#narrow/channel/136281-t-opsem/topic/No.20reference.20validity.20vs.20improvements.20to.20closure.20captures/with/624981987, I describe a potential improvement to closure capture inference which may conflict with not having memory-dependent reference validity. (I'm hopeful that we can resolve the conflict.)

[RalfJung]

@CAD97 @digama0 @joshlf friendly checkbox reminder -- from the opsem side the only part we didn't already FCP is the part about unsized types, where we are conservatively saying that we are evaluating inhabitedness of the pointee type using the information about the "actual" type as represented by the reference metadata.

[RalfJung]

@rustbot label +I-opsem-nominated

[CAD97]

@rfcbot reviewed