Fix false positive use of uninit bytes when calling libc::pthread_condattr_destroy

[5225225]

Fixes: #1931

[5225225]

Hm. Not sure why that's failing, seeing as 64 bit linux is the machine I'm testing on and ./miri test works fine.

[RalfJung]

Thanks for your first Miri PR! 🎉

Hm. Not sure why that's failing, seeing as 64 bit linux is the machine I'm testing on and ./miri test works fine.

Seems like you got that fixed? Our CI runs tests on the Linux host that use other OSes as target, so I assume that is what happened.

[5225225]

Yeah, the 64 bit linux error was me not adding ignore-windows to the files, the error coming from linux and not windows confused me. No worries, got it fixed now in any case.

Will fix the comments after work

[5225225]

One... somewhat questionable thing we do is actually set the value of the libc::pthread_mutex (or any other pthread type, really) to be Uninit on destroy.

Which would mean that simply having a destroyed pthread_mutex is UB, if you've not got it inside a MaybeUninit, and if we're assuming having an uninit variable as a local is instant UB. The standard library, at least for RWLock, doesn't keep the object inside a MaybeUninit, it's just an UnsafeCell.

I guess the technically more correct thing to do here would be to have hidden state to keep track of which objects have been destroyed and which haven't, and trigger UB if you try to init an init object, or destroy an uninit object. And then just overwrite the object with arbitrary but still defined bytes(zeros, I suppose)?

Not sure. The tests pass as is, but that is presumably miri just not checking "oh that thing that had uninit written to it is actually not in a MaybeUninit, that's instant UB!"

[RalfJung]

Which would mean that simply having a destroyed pthread_mutex is UB, if you've not got it inside a MaybeUninit, and if we're assuming having an uninit variable as a local is instant UB. The standard library, at least for RWLock, doesn't keep the object inside a MaybeUninit, it's just an UnsafeCell.

So, can you use this to cause a UB error from the standard library? If destroy is only ever called in drop, then I think there is no way that this uninit memory would ever be used at its real type again, so there'd be no way to trigger UB. This might be a more subtle soundness argument than that code anticipated, but it seems good enough for now. We should just add a comment on the Miri side explaining this.

[5225225]

If destroy is only ever called in drop, then I think there is no way that this uninit memory would ever be used at its real type again, so there'd be no way to trigger UB.

Does being behind a reference mean you're not being used as your real type? I guess if you're going to be dropped, and you hold a &mut anyways, it's fine because no one else can see the uninit values, and it's fine to hold a &mut T where T's validity invariants are broken (as long as you're careful to not observe those broken invariants). (Which would mean it's sound to, say, write uninit into Foo(u8) in drop, as long as you're very careful to not see the u8 after that).

In any case, I added a comment explaining it.

[RalfJung]

LGTM aside from some comment tweaks. Can you also squash the last commit into the previous one?

[5225225]

Okay, applied the changes, and I'm happy with the way the comment reads. Also yeah, squashed the rustfmt commit.

[RalfJung]

Great, thanks a lot!

@bors r+

[bors]

📌 Commit fd830e7 has been approved by RalfJung

[bors]

⌛ Testing commit fd830e7 with merge 23a9d02...

[bors]

☀️ Test successful - checks-actions
Approved by: RalfJung
Pushing 23a9d02 to master...