Could this explain why parametricity is not enough for dropck

code review
1

Doubts in my mind after reading dropck can be bypassed via a trait object method and rust-lang/rfcs#1238/. Hope someone can help to clear.

is the following snippet a proof of

parametricity is not enough for dropck

as commented.

pub struct Foo<T>(T);

//T is not bounded
pub fn bar<T>(t: &T) {
    unsafe {
        //doing some evil things here
        //use after free
        std::ptr::read(std::mem::transmute::<&T, *mut T>(t));
    }
}

impl<T> Foo<T> {
    pub fn foo(&self) {
        bar(&self.0);
    }
}

impl<T> Drop for Foo<T> {
    fn drop(&mut self) {
        //even though T is not bounded, but it has one impl *foo* that
        //does something evil, so parametricity is not enough here
        self.foo();
    }
}

fn main() {
    let (f, s);
    s = String::from("hello");
    f = Foo(Box::new(&s));
}
2

The issue in question has been fixed several years ago. Your code is not proof of any sort of soundness bug, because it uses unsafe and explicitly corrupts memory. So I'm not sure what you are getting at.

3

Yes, you're right. I'm not proving the unsoundness of dropcker rust uses nowdays or anything here. Just to ask help to check if my understanding of "dropck based on parametricity is not enough" is correct.

Rather, it seems to be a flaw in the "parametricity" argument -- that is, today, we consider the definition of drop "uninteresting" if B does not have any bounds, with the intention of screening out code that treats instances of B opaquely. But we overlooked closures or trait objects that may consume a B instance and which (hence) "encapsulate" bounds. That's...pretty unfortunate.

According to nikomatsakis, the buggy dropck based on parametricity before rfcs#1238 considered the definition of drop "uninteresting" if T does not have any bounds, and why it's buggy is because of overlook of closures or traits objects that may consume a B instance and which (hence) "encapsulate" bounds.

To my mind, the code above which explains itself, is probably another case to prove parametricity is not sufficient. Because the drop of Foo calls bar which does not "encapsulate" bounds (beyond cased mentioned by nikomatsakis). If ignoring dropck on T due to pure parametricity analysis, then unsoundness are introduced. Is this reasoning correct?

Btw, I explicitly use unsafe here to demonstrate something bad could happen if we use inner T when dropping Foo if we don't ensure lifetime introduced by T strictly outlives Foo.

4

This topic was automatically closed 90 days after the last reply. We invite you to open a new topic if you have further questions or comments.