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

Topic: Is this possible to fix without API break?


Shnatsel (Jun 28 2019 at 16:20, on Zulip):

This code is unsound: https://github.com/sile/libflate/blob/cbf1289f967c8fdff3b8ff3e06256ff7b62cc914/src/gzip.rs#L1122
If a panic occurs before mem::forget() is reached, drop()is called on uninitialized data of arbitrary type. I've been trying to come up with a way to fix this, but to no avail. Is this fixable without breaking the API? And how does one rewrite something like that in safe Rust?

RalfJ (Jun 28 2019 at 16:35, on Zulip):

@Shnatsel from a superficial glance, looks like a case for this crate? https://crates.io/crates/take_mut

RalfJ (Jun 28 2019 at 16:36, on Zulip):

I've also seen proposals to add such functionality to libstd

Shnatsel (Jun 28 2019 at 16:36, on Zulip):

Take &mut? Is that even legal?

RalfJ (Jun 28 2019 at 16:36, on Zulip):

replacing with mem::uninitialized.... shivers

RalfJ (Jun 28 2019 at 16:37, on Zulip):

Take &mut? Is that even legal?

what that crate does is considered to be legal, AFAIK. I have even proven it correct, but in a simplified model of Rust that does not have panics, so that proof only tells half the story.

Shnatsel (Jun 28 2019 at 16:37, on Zulip):

Good enough for me. Thanks a lot!

RalfJ (Jun 28 2019 at 16:38, on Zulip):

notice that this turns panics into aborts

RalfJ (Jun 28 2019 at 16:39, on Zulip):

https://docs.rs/take_mut/0.2.2/take_mut/fn.take.html

Shnatsel (Jun 28 2019 at 16:41, on Zulip):

Oh, so the proof under a model without panics actually applies for the most part. Neat!

centril (Jun 28 2019 at 16:50, on Zulip):

This is one of the cases I'd like to have an effect/restriction system for "provably cannot panic"

RalfJ (Jun 28 2019 at 16:54, on Zulip):

yeah that would be useful here. still seems too niche though to warrant the global cost of such an effect system.

Shnatsel (Jun 28 2019 at 16:55, on Zulip):

https://github.com/viperproject/prusti-dev can prove it for you

RalfJ (Jun 28 2019 at 16:55, on Zulip):

that's safe-code-only though

RalfJ (Jun 28 2019 at 16:55, on Zulip):

and a very limited but growing subset. but one day hopefully it can :)

centril (Jun 28 2019 at 16:58, on Zulip):

I think the global cost of an effect system gets amortized by the number of effects/restrictions (const, panic, async, ...)

centril (Jun 28 2019 at 16:59, on Zulip):

but... it's nice to know that something cannot panic purely as a sanity check rather than for soundness purposes

gnzlbg (Jun 28 2019 at 17:34, on Zulip):

There are so many weird effects, that I'm not sure we will ever get an effect system

gnzlbg (Jun 28 2019 at 17:36, on Zulip):

also the current situation where some effects are on by default while some are off is weird to handle generically

gnzlbg (Jun 28 2019 at 17:36, on Zulip):

and we have compiler flags that turn effects on/off globally

Last update: Nov 19 2019 at 17:45UTC