Stream: t-lang/wg-unsafe-code-guidelines

Topic: exhaustiveness checking


nikomatsakis (Aug 08 2018 at 18:21, on Zulip):

So @RalfJ and I had a good chat about exhaustiveness checking and uninhabited types and how to think about it today. @RalfJ I was wondering, I know you've been going crazy with the blog posts lately, were you planning on trying to write that up?

scottmcm (Aug 08 2018 at 20:34, on Zulip):

Huzzah! I was sad that RFC got postponed...

RalfJ (Aug 08 2018 at 22:44, on Zulip):

TBH I thought I would end my blog post streak for now and get back to getting some work done ;)

RalfJ (Aug 08 2018 at 22:45, on Zulip):

Also isnt this closer to an RFC already?^^

nikomatsakis (Aug 08 2018 at 23:08, on Zulip):

heh :) ok -- I might be up to try writing it out

RalfJ (Aug 10 2018 at 07:19, on Zulip):

Thanks! Let me know if I should write some part of that.

nikomatsakis (Aug 10 2018 at 10:01, on Zulip):

I started a post, here is a draft, but I am not happy with it:

https://gist.github.com/nikomatsakis/b1d007abeb57b8f3eb35cd9b51e98dbc

nikomatsakis (Aug 10 2018 at 10:01, on Zulip):

for one thing, I spent most of the time so far introducing the problems etc

nikomatsakis (Aug 10 2018 at 10:02, on Zulip):

I think I might start over and just cut to the chase, then come back and talk a bit about the tensions :)

nikomatsakis (Aug 10 2018 at 10:12, on Zulip):

and I suppose I should think about drafting something for the UCG repo

RalfJ (Aug 11 2018 at 13:53, on Zulip):

Oh wow that's a long post you wrote^^

RalfJ (Aug 11 2018 at 13:53, on Zulip):

TBH I would probably start with the ! pattern

RalfJ (Aug 11 2018 at 13:54, on Zulip):

and the fact that it does not require code to follow the pattern, because it is expressing some kind of "proof" that this case cannot happen

RalfJ (Aug 11 2018 at 13:55, on Zulip):

which then leads us to auto-generating that pattern -- feasible only because no code must be generated

RalfJ (Aug 11 2018 at 13:55, on Zulip):

and then the problems of doing so when & is involved

RalfJ (Aug 11 2018 at 13:59, on Zulip):

I think by now we have so much code that handles &T where the memory is not fully initialized, we cannot reasonably make that requirement. Someone posted an example where this might be useful in the internals thread for my model, I still need to look at that in more detail.
But my gut feeling right now is that having a &! is not insta-UB. that is, however, not in contradiction with auto-never'ing it; that would just give us UB more selectively and for a different reason (namely, the ! pattern that the user did not write).

Nicole Mazzuca (Aug 11 2018 at 15:05, on Zulip):

yeah, I think looking at https://github.com/rust-lang/rfcs/pull/1892#issuecomment-412278317, it's entirely reasonable that the guarantees of &mut T (and &T), at a compiler level, should be object with read-[write] capabilities of size_of_val(r). I don't think it's reasonable to change this at this point.

alercah (Aug 12 2018 at 19:11, on Zulip):

I think that requiring &T point to a valid value always also goes against the desire to make a reference aliasing model that allows split_at_mut to work, as well?

alercah (Aug 12 2018 at 19:11, on Zulip):

Since that implies that an invariant that's currently directly on the reference types is instead going to be about accesses and uses.

nikomatsakis (Aug 13 2018 at 17:05, on Zulip):

and the fact that it does not require code to follow the pattern, because it is expressing some kind of "proof" that this case cannot happen

yes, I need to rework it

nikomatsakis (Aug 13 2018 at 17:08, on Zulip):

But my gut feeling right now is that having a &! is not insta-UB. that is, however, not in contradiction with auto-never'ing it; that would just give us UB more selectively and for a different reason (namely, the ! pattern that the user did not write).

the key thing for me was that auto-never could treat &! as "effectively uninhabited", but that we could lint against this "in or around" unsafe code, since we now have a way to explicitly talk about it as well. Not sure if that's a good idea or not, but it's at least a possibility for a "third way"

nikomatsakis (Aug 13 2018 at 17:08, on Zulip):

@alercah I don't think I fully understand what you're saying

nikomatsakis (Aug 13 2018 at 18:17, on Zulip):

@RalfJ ok take a look at this new version of the post

nikomatsakis (Aug 13 2018 at 18:17, on Zulip):

(and anyone else)

RalfJ (Aug 13 2018 at 18:20, on Zulip):

I think that requiring &T point to a valid value always also goes against the desire to make a reference aliasing model that allows split_at_mut to work, as well?

I do not see the contradiction here. Both the input and the output of split_and_mut always point to properly initialized data.

RalfJ (Aug 13 2018 at 18:27, on Zulip):

@nikomatsakis that looks great!

RalfJ (Aug 13 2018 at 18:27, on Zulip):

I like it.

RalfJ (Aug 13 2018 at 18:30, on Zulip):

I think you promised that the unsafe section would come back to why products only auto-never when all fields do, but the unsafe section does not say anything about that

nikomatsakis (Aug 13 2018 at 18:35, on Zulip):

@RalfJ oh, right, I cut that

nikomatsakis (Aug 13 2018 at 18:35, on Zulip):

I can maybe add back a bit

RalfJ (Aug 13 2018 at 18:35, on Zulip):

yeah I think that'd be good

RalfJ (Aug 13 2018 at 18:35, on Zulip):

it seems non-obvious

RalfJ (Aug 13 2018 at 18:36, on Zulip):

in fact I am not even very clear why we do it :D

nikomatsakis (Aug 13 2018 at 18:36, on Zulip):

it has to do with uninitialized data

nikomatsakis (Aug 13 2018 at 18:36, on Zulip):

in particular, otherwise,

nikomatsakis (Aug 13 2018 at 18:36, on Zulip):

there would be valid patterns one could write

nikomatsakis (Aug 13 2018 at 18:36, on Zulip):

e.g., match x.value { (y, _) => .. } where x: Uninit<(u32,!)>

nikomatsakis (Aug 13 2018 at 18:37, on Zulip):

I wanted the invariant that autonever nevers adds a pattern that could have had a body

RalfJ (Aug 13 2018 at 18:37, on Zulip):

ah. yes that makes sense.

RalfJ (Aug 13 2018 at 18:38, on Zulip):

reminds me of the failed optimizations to make any struct with an uninhabited field a ZST

RalfJ (Aug 13 2018 at 18:38, on Zulip):

and then someone though of partial initialization :P

nikomatsakis (Aug 13 2018 at 18:39, on Zulip):

yes I think they are related :)

nikomatsakis (Aug 13 2018 at 18:39, on Zulip):

I thought about citing that in the post but thought it'd be too much

alercah (Aug 13 2018 at 20:09, on Zulip):

The split_at_mut thing is about trying to make a version that doesn't require you to destructure and rebuild the slice manually. That requires changing the rules so that multiple &mut can coexist if they aren't used in a conflicting way, at least in some limited scope. This to me feels generally in the direction of making the requirements be about the actual use of a type.

alercah (Aug 13 2018 at 20:10, on Zulip):

So if &! was instantly UB, I feel that would be moving in the opposite direction.

RalfJ (Aug 13 2018 at 20:57, on Zulip):

@alercah the multiple &mut never coexist. One stops being used before the other is created.

RalfJ (Aug 13 2018 at 20:57, on Zulip):

That's how my model allows split_at_mut

alercah (Aug 13 2018 at 21:03, on Zulip):

@RalfJ I mean inside split_at_mut.

RalfJ (Aug 13 2018 at 21:12, on Zulip):

Yes, that's what I was talking about.

alercah (Aug 13 2018 at 21:18, on Zulip):

How would you write it, then?

RalfJ (Aug 13 2018 at 21:27, on Zulip):

Just like it already is in libcore right now

RalfJ (Aug 13 2018 at 21:28, on Zulip):

notice that self does not get used again

RalfJ (Aug 13 2018 at 21:34, on Zulip):

but really we should have this discussion in the stacked-borrows topic :D

nikomatsakis (Aug 13 2018 at 21:55, on Zulip):

posted on my blog

nikomatsakis (Aug 13 2018 at 21:55, on Zulip):

I should probably open an internals thread

nikomatsakis (Aug 13 2018 at 21:57, on Zulip):

done: internals thread

alercah (Aug 13 2018 at 22:43, on Zulip):

I was thinking a hypothetical version that doesn't use from_raw_parts_mut, like Niko talked about in an older blog post.

Last update: Nov 20 2019 at 11:35UTC