-
Notifications
You must be signed in to change notification settings - Fork 606
nail down the final validity rules: references and unions #2337
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
Open
RalfJung
wants to merge
2
commits into
rust-lang:master
Choose a base branch
from
RalfJung:finish-validity
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
+12
−4
Open
Changes from all commits
Commits
Show all changes
2 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
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.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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)
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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. :)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
guilty as charged I'm afraid ^^'
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@RalfJung I agree that this is not stated correctly. It's not about uninhabitedness, this is a validity clause. Inhabitedness is a property of a type, validity is a property of a value of the type.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 implementingNeverImplements. What we want to say is that the value[ptr, never_vtable]: &dyn NeverImplementsis invalid, for the reason that the vtable is for a type that is uninhabited. For the unsized typedyn NeverImplementsitself, 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 havenever_vtableas the metadata.The reasoning for the present case is similar: if
Uis uninhabited, then[U; 1]is uninhabited and&[U; 1]is uninhabited and&[U]is inhabited but has only the valid valuelen = 0; the value[ptr, 1]: &[U]is not valid for the type regardless ofptr. 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.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What is being defined here is whether
dyn NeverImplementsis inhabited. Which depends on the metadata, just like inhabitedness of[!].Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 Traitis inhabited iff the actual dynamic type represented in the metadata is inhabited.