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

dropck can be bypassed via a trait object method #26656

Closed
arielb1 opened this Issue Jun 29, 2015 · 20 comments

Comments

Projects
None yet
7 participants
@arielb1
Contributor

arielb1 commented Jun 29, 2015

STR

// Using this instead of Fn etc. to take HRTB out of the equation.
trait Trigger<B> { fn fire(&self, b: &mut B); }
impl<B: Button> Trigger<B> for () {
    fn fire(&self, b: &mut B) {
        b.push();
    }
}

// Still unsound Zook
trait Button { fn push(&self); }
struct Zook<B> { button: B, trigger: Box<Trigger<B>+'static> }

impl<B> Drop for Zook<B> {
    fn drop(&mut self) {
        self.trigger.fire(&mut self.button);
    }
}

// AND
struct Bomb { usable: bool }
impl Drop for Bomb { fn drop(&mut self) { self.usable = false; } }
impl Bomb { fn activate(&self) { assert!(self.usable) } }

enum B<'a> { HarmlessButton, BigRedButton(&'a Bomb) }
impl<'a> Button for B<'a> {
    fn push(&self) {
        if let B::BigRedButton(borrowed) = *self {
            borrowed.activate();
        }
    }
}

fn main() {
    let (mut zook, ticking);
    zook = Zook { button: B::HarmlessButton,
                  trigger: Box::new(()) };
    ticking = Bomb { usable: true };
    zook.button = B::BigRedButton(&ticking);
}

This fails the assertion. cc @pnkfelix. I think the problem here is that Box<Trigger<B>+'static> does not require that B: 'static (cc @nikomatsakis).

@alexcrichton

This comment has been minimized.

Show comment
Hide comment
@alexcrichton

alexcrichton Jun 29, 2015

Member

triage: I-nominated

Member

alexcrichton commented Jun 29, 2015

triage: I-nominated

@arielb1 arielb1 changed the title from dropck can be bypassed via a trait method to dropck can be bypassed via a trait object method Jun 29, 2015

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Jul 6, 2015

Contributor

Hmm, so I don't think that the problem has to do with Trigger<B>: 'static requiring that B: 'static per se, though I suppose it might help with the problem. 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.

Contributor

nikomatsakis commented Jul 6, 2015

Hmm, so I don't think that the problem has to do with Trigger<B>: 'static requiring that B: 'static per se, though I suppose it might help with the problem. 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.

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Jul 7, 2015

Contributor

After thinking on this last night, I laid it out in my head this way. There is a properly very similar to variance, let's call it "Type may access X" where X is one of the type parameters declared on Type. It indicates whether having access to a Type<Foo> potentially lets you manipulate the contents of Foo. This can be inferred in a global way just as variance can be inferred by setting up various constraints. The bottom line is what kind of data is reachable through Type.

For convenience, we also write T<...,U,...> may access U to mean T may access V where V is the type parameter for which U is being substituted.

Given some type declared like struct Type<..., X, ...> (possibly with where clauses):

  • If Type has where-clauses that reference X, then Type may access X.
  • If the definition of Type contains a field f: T where T contains (somewhere) Type1<..., X, ...>, and Type1<...X...> may access X, then Type may access X.

In addition there are some ground rules:

  • fn(..., X, ...) may access X
  • Trait<...X,...> may access X

Now the dropck can use these rules to decide when it should enforce stricter rules. In particular, if an lvalue of type T<U> is being dropped at exit from 'a, and T<U> may access U, then U must strictly outlive 'a. Or something like that, I have to review how the dropck rules are formulated exactly. But you get the idea.

The key point is that this property may access is independent from whether a value has a destructor. The intution is "if a destructor got ahold of a value of type T<...U...>, could it wind up dereferencing pointers in U?"

Contributor

nikomatsakis commented Jul 7, 2015

After thinking on this last night, I laid it out in my head this way. There is a properly very similar to variance, let's call it "Type may access X" where X is one of the type parameters declared on Type. It indicates whether having access to a Type<Foo> potentially lets you manipulate the contents of Foo. This can be inferred in a global way just as variance can be inferred by setting up various constraints. The bottom line is what kind of data is reachable through Type.

For convenience, we also write T<...,U,...> may access U to mean T may access V where V is the type parameter for which U is being substituted.

Given some type declared like struct Type<..., X, ...> (possibly with where clauses):

  • If Type has where-clauses that reference X, then Type may access X.
  • If the definition of Type contains a field f: T where T contains (somewhere) Type1<..., X, ...>, and Type1<...X...> may access X, then Type may access X.

In addition there are some ground rules:

  • fn(..., X, ...) may access X
  • Trait<...X,...> may access X

Now the dropck can use these rules to decide when it should enforce stricter rules. In particular, if an lvalue of type T<U> is being dropped at exit from 'a, and T<U> may access U, then U must strictly outlive 'a. Or something like that, I have to review how the dropck rules are formulated exactly. But you get the idea.

The key point is that this property may access is independent from whether a value has a destructor. The intution is "if a destructor got ahold of a value of type T<...U...>, could it wind up dereferencing pointers in U?"

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Jul 7, 2015

Contributor

Some implications of this, presuming this property is inferred in a similar fashion to variance:

  • adding a fn or trait object into a type can be a breaking change. That worried me some, but I realized that it is likely true already, since it also affects the variance calculation (triggers invariance). Now I still worry but less.
Contributor

nikomatsakis commented Jul 7, 2015

Some implications of this, presuming this property is inferred in a similar fashion to variance:

  • adding a fn or trait object into a type can be a breaking change. That worried me some, but I realized that it is likely true already, since it also affects the variance calculation (triggers invariance). Now I still worry but less.
@arielb1

This comment has been minimized.

Show comment
Hide comment
@arielb1

arielb1 Jul 7, 2015

Contributor

Personally I think of the issue as being more related to liveness - every lifetime parameter to a function (or impl) is required to be alive when the function (that can access that impl) is called, but (because of dropck) type parameters passed to a function may not be alive. This is preserved by normal selection (as it can't dig into the dead type and find the dead lifetime), but trait objects (and equivalently, instantiations of generic functions) can "refer to" an impl that witnesses the liveness of the lifetime, and should be treated as such.

Contributor

arielb1 commented Jul 7, 2015

Personally I think of the issue as being more related to liveness - every lifetime parameter to a function (or impl) is required to be alive when the function (that can access that impl) is called, but (because of dropck) type parameters passed to a function may not be alive. This is preserved by normal selection (as it can't dig into the dead type and find the dead lifetime), but trait objects (and equivalently, instantiations of generic functions) can "refer to" an impl that witnesses the liveness of the lifetime, and should be treated as such.

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Jul 7, 2015

Contributor

@arielb1 I don't disagree with all that. It is certainly intentional that dropck allows access to "potentially dead data" in some cases. The original formulation did not, but we found it was very strict. The goal of the "may observe" relation I was discussing is to specify precisely when it is ok to allow access to potentially dead data, because we can be sure that the data will not be used.

/me kind of misses the days when data with dtors was always Send+'static

Contributor

nikomatsakis commented Jul 7, 2015

@arielb1 I don't disagree with all that. It is certainly intentional that dropck allows access to "potentially dead data" in some cases. The original formulation did not, but we found it was very strict. The goal of the "may observe" relation I was discussing is to specify precisely when it is ok to allow access to potentially dead data, because we can be sure that the data will not be used.

/me kind of misses the days when data with dtors was always Send+'static

@arielb1

This comment has been minimized.

Show comment
Hide comment
@arielb1

arielb1 Jul 7, 2015

Contributor

Heh, dtors could always refer to dead types (with unsafe_destructor then).

Contributor

arielb1 commented Jul 7, 2015

Heh, dtors could always refer to dead types (with unsafe_destructor then).

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Jul 7, 2015

Contributor

@arielb1 yes, they were only ever Send+'static in a fictional dream world :)

Contributor

nikomatsakis commented Jul 7, 2015

@arielb1 yes, they were only ever Send+'static in a fictional dream world :)

@pnkfelix

This comment has been minimized.

Show comment
Hide comment
@pnkfelix

pnkfelix Jul 8, 2015

Member

okay clearly the Sound Drop RFC needs some updating. The observation that parametricity is not a sufficient condition is important. I will try to incorporate the comments above into a PR on the rfcs repo (either a new RFC or an amendment to Sound Drop, depending on how bad the damage is).

Member

pnkfelix commented Jul 8, 2015

okay clearly the Sound Drop RFC needs some updating. The observation that parametricity is not a sufficient condition is important. I will try to incorporate the comments above into a PR on the rfcs repo (either a new RFC or an amendment to Sound Drop, depending on how bad the damage is).

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Jul 9, 2015

Contributor

triage: P-high (soundness issue)

Contributor

nikomatsakis commented Jul 9, 2015

triage: P-high (soundness issue)

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Jul 16, 2015

Contributor

The more I think about this, the more I would prefer to back away from the current (unsound, as demonstrated here) parametricity-based reasoning and lean on something simpler (e.g., an unsafe annotation), at least for the time being, if not forever.

Contributor

nikomatsakis commented Jul 16, 2015

The more I think about this, the more I would prefer to back away from the current (unsound, as demonstrated here) parametricity-based reasoning and lean on something simpler (e.g., an unsafe annotation), at least for the time being, if not forever.

@pnkfelix

This comment has been minimized.

Show comment
Hide comment
@pnkfelix

pnkfelix Jul 16, 2015

Member

For the public record

My opinion is that if bugs like this and #26657 were the only known issues with dropck, then I would prefer to try to improve the reasoning performed by dropck, rather than rely on user-provided annotations that are likely to be misunderstood and abused, yielding bugs that are hard to witness (i.e. that I expect naive testing to miss).

However, given that there are also issues with the proposed specialization RFC, I am now investigating adding an unsafe annotation along the lines noted above.

(Still, it would be nice if in parallel with paring back on dropck for the short term, if we also tried to be forward-thinking and not add features that will make it impossible to put back parametricity based reasoning in the future. Okay, that's enough out of me.)

Member

pnkfelix commented Jul 16, 2015

For the public record

My opinion is that if bugs like this and #26657 were the only known issues with dropck, then I would prefer to try to improve the reasoning performed by dropck, rather than rely on user-provided annotations that are likely to be misunderstood and abused, yielding bugs that are hard to witness (i.e. that I expect naive testing to miss).

However, given that there are also issues with the proposed specialization RFC, I am now investigating adding an unsafe annotation along the lines noted above.

(Still, it would be nice if in parallel with paring back on dropck for the short term, if we also tried to be forward-thinking and not add features that will make it impossible to put back parametricity based reasoning in the future. Okay, that's enough out of me.)

@RalfJung

This comment has been minimized.

Show comment
Hide comment
@RalfJung

RalfJung Aug 7, 2015

Member

It took me a while to understand why trait objects even help in circumventing dropck... my current conclusion is that in Zook::Drop, Rust actually can assume that B: Button because we have something of type Box<Trigger<B>> around, which can only be well-formed if B: Button. In other words, the source of the problem is the fact that there are many ways to get a trait bound into a function, not just the annotation at the impl and fn. So, it's not the case that parametricity is not good enough - rather, checking the precondition of parametricitiy (that no assumptions are made about the type) turns out to be harder than expected.
Would that be a fair summary of this issue?

EDIT: I also wonder how Rust chooses the lifetime for B in main. Obviously, that lifetime is only the block suffix starting at &ticking, but that means that in the two lines before this block suffix, we have a type in scope that contains a lifetime that didn't even start yet?

EDIT2: Coming back to my point above: Rust only assumes B: Button in drop when we call trigger.fire. If we call button.push directly instead, even though we can derive B: Button via the Box type, the compiler doesn't actually notice that it has this implicit bound around.

Member

RalfJung commented Aug 7, 2015

It took me a while to understand why trait objects even help in circumventing dropck... my current conclusion is that in Zook::Drop, Rust actually can assume that B: Button because we have something of type Box<Trigger<B>> around, which can only be well-formed if B: Button. In other words, the source of the problem is the fact that there are many ways to get a trait bound into a function, not just the annotation at the impl and fn. So, it's not the case that parametricity is not good enough - rather, checking the precondition of parametricitiy (that no assumptions are made about the type) turns out to be harder than expected.
Would that be a fair summary of this issue?

EDIT: I also wonder how Rust chooses the lifetime for B in main. Obviously, that lifetime is only the block suffix starting at &ticking, but that means that in the two lines before this block suffix, we have a type in scope that contains a lifetime that didn't even start yet?

EDIT2: Coming back to my point above: Rust only assumes B: Button in drop when we call trigger.fire. If we call button.push directly instead, even though we can derive B: Button via the Box type, the compiler doesn't actually notice that it has this implicit bound around.

@pnkfelix

This comment has been minimized.

Show comment
Hide comment
@pnkfelix

pnkfelix Aug 7, 2015

Member

@RalfJung my go-to example when thinking about this is a struct that carries both some object and a callback on that object:

struct S<T> { x: Option<T>, f: fn (T) }

To my mind, S is definitely parametric with respect to T. Given an s: S and with no further knowledge of the particular T, there is nothing one can do with s.x except 1. swap in a None instead, and/or 2. call s.f with the contents of s.x, if any are present.

The above properties are not violations of parametricity. (it is what I see as a celebration of parametricity: it allows one to make very strong statements about what clients can do with instances of S if they do not introduce bounds on T.)

With our current buggy dropck, however, one is allowed to pass the s.x into s.f, yet there is no strictly-outlives relationship enforced between the S and any references within the s.x.

  • Here is a full example illustrating this for the S above: http://is.gd/vqx1OV
  • This is why I have been saying that "parametricity is necessary but not sufficient."
  • We need a stronger check, that ensures that we only allow the weaker region relations on parameter types T that can be proven do not flow into any "negative positions" (e.g. function arguments). Positive positions are okay since those can only create instances of T, they cannot consume the one we have in hand.
Member

pnkfelix commented Aug 7, 2015

@RalfJung my go-to example when thinking about this is a struct that carries both some object and a callback on that object:

struct S<T> { x: Option<T>, f: fn (T) }

To my mind, S is definitely parametric with respect to T. Given an s: S and with no further knowledge of the particular T, there is nothing one can do with s.x except 1. swap in a None instead, and/or 2. call s.f with the contents of s.x, if any are present.

The above properties are not violations of parametricity. (it is what I see as a celebration of parametricity: it allows one to make very strong statements about what clients can do with instances of S if they do not introduce bounds on T.)

With our current buggy dropck, however, one is allowed to pass the s.x into s.f, yet there is no strictly-outlives relationship enforced between the S and any references within the s.x.

  • Here is a full example illustrating this for the S above: http://is.gd/vqx1OV
  • This is why I have been saying that "parametricity is necessary but not sufficient."
  • We need a stronger check, that ensures that we only allow the weaker region relations on parameter types T that can be proven do not flow into any "negative positions" (e.g. function arguments). Positive positions are okay since those can only create instances of T, they cannot consume the one we have in hand.
@RalfJung

This comment has been minimized.

Show comment
Hide comment
@RalfJung

RalfJung Aug 8, 2015

Member

@pnkfelix That's a great example, thanks a lot! I think I understand now.
Btw, the example (and also the original one) can be written without mutable variables in main: http://is.gd/7VVkX5. (In the original one, one can then even get rid of the HarmlessButton variant.)

Member

RalfJung commented Aug 8, 2015

@pnkfelix That's a great example, thanks a lot! I think I understand now.
Btw, the example (and also the original one) can be written without mutable variables in main: http://is.gd/7VVkX5. (In the original one, one can then even get rid of the HarmlessButton variant.)

@arielb1

This comment has been minimized.

Show comment
Hide comment
@arielb1

arielb1 Aug 10, 2015

Contributor

Right. And this can be fixed (after @nikomatsakis's patch) by making fn a dropck type (potentially in the same as trait objects).

On the other hand, ordinary parametricity isn't really the important condition for dropck. Rust code is always perfectly parametric about lifetimes. One theoretical way to make dropck work with specialization is to change the "vtables" during destruction, C++-style, which is basically a gaping violating of parametricity. Even without that, you can safely:

  • have control-flow dependencies on everything you want. This includes branching on "empty" traits (e.g. Send, Sized, Copy given Clone, etc.).
  • even more strongly, get 'static data on everything you want.
  • invert impls. For example, after you branch on your Option<T ~ &'α [$0]>, if you know that T: IntoIterator and that there are no blanket impls for IntoIterator (yay orphan rules), you can safely downcast T to a &'α [$0] with a fresh lifetime, as the reference must have been live for the impl to be available.
Contributor

arielb1 commented Aug 10, 2015

Right. And this can be fixed (after @nikomatsakis's patch) by making fn a dropck type (potentially in the same as trait objects).

On the other hand, ordinary parametricity isn't really the important condition for dropck. Rust code is always perfectly parametric about lifetimes. One theoretical way to make dropck work with specialization is to change the "vtables" during destruction, C++-style, which is basically a gaping violating of parametricity. Even without that, you can safely:

  • have control-flow dependencies on everything you want. This includes branching on "empty" traits (e.g. Send, Sized, Copy given Clone, etc.).
  • even more strongly, get 'static data on everything you want.
  • invert impls. For example, after you branch on your Option<T ~ &'α [$0]>, if you know that T: IntoIterator and that there are no blanket impls for IntoIterator (yay orphan rules), you can safely downcast T to a &'α [$0] with a fresh lifetime, as the reference must have been live for the impl to be available.
@pnkfelix

This comment has been minimized.

Show comment
Hide comment
@pnkfelix

pnkfelix Oct 1, 2015

Member

/me has been officially nagged by @nikomatsakis to put up a PR for the implementation of RFC rust-lang/rfcs#1238

Member

pnkfelix commented Oct 1, 2015

/me has been officially nagged by @nikomatsakis to put up a PR for the implementation of RFC rust-lang/rfcs#1238

@arielb1 arielb1 referenced this issue Oct 20, 2015

Merged

Dropck Eyepatch RFC. #1327

1 of 2 tasks complete
@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Oct 29, 2015

Contributor

This is basically fixed, but we don't have a specific regression test.

Contributor

nikomatsakis commented Oct 29, 2015

This is basically fixed, but we don't have a specific regression test.

@bstrie bstrie added the I-nominated label Nov 29, 2015

@bstrie

This comment has been minimized.

Show comment
Hide comment
@bstrie

bstrie Nov 29, 2015

Contributor

Nominating as this is a soundness bug that has yet to have a priority assigned.

Contributor

bstrie commented Nov 29, 2015

Nominating as this is a soundness bug that has yet to have a priority assigned.

@pnkfelix pnkfelix self-assigned this Dec 3, 2015

@arielb1 arielb1 removed the I-nominated label Dec 3, 2015

@nikomatsakis

This comment has been minimized.

Show comment
Hide comment
@nikomatsakis

nikomatsakis Dec 3, 2015

Contributor

@bstrie this has been fixed, we're just waiting on a regression test.

Contributor

nikomatsakis commented Dec 3, 2015

@bstrie this has been fixed, we're just waiting on a regression test.

pnkfelix added a commit to pnkfelix/rust that referenced this issue Dec 10, 2015

bors added a commit that referenced this issue Dec 11, 2015

Auto merge of #30307 - pnkfelix:fix-issue-26656, r=alexcrichton
Long awaited regression test for dropck on trait object method.

Fix #26656.

bors added a commit that referenced this issue Dec 11, 2015

Auto merge of #30307 - pnkfelix:fix-issue-26656, r=alexcrichton
Long awaited regression test for dropck on trait object method.

Fix #26656.

@bors bors closed this in #30307 Dec 11, 2015

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment