Fix capability checking for gencap-constrained type parameters. #1593

jemc · 2017-02-17T07:22:49Z

This PR fixes the type system bug described in #1328.

jemc · 2017-02-17T07:28:06Z

This is a pretty important bug fix, since the compiler is currently allowing some very unsafe forms when using generics. Due to that, it would be nice to squeeze this into the 0.11.0 release (#1543) if possible.

However, I do want @sylvanc to review this first to make sure that my type system choices here were sound from a formal perspective.

Resolves #1328.

Praetonus · 2017-02-17T07:46:39Z

I haven't followed the investigation made on this bug ; out of curiosity, what was causing the bad type checking?

jemc

@sylvanc here are some specific places where I request your scrutiny.

jemc · 2017-02-17T07:36:24Z

src/libponyc/type/cap.c

  switch(sub)
  {
    case TK_ISO:
      switch(super)
      {
-        case TK_ISO:


This case was already handled by the if (sub == super) return true check above.

jemc · 2017-02-17T07:36:45Z

src/libponyc/type/cap.c

@@ -121,11 +101,8 @@ bool is_cap_sub_cap(token_id sub, token_id subalias, token_id super,
        case TK_REF:
        case TK_VAL:
        case TK_BOX:
-        case TK_CAP_READ:


@sylvanc Note that I removed this case here:

#read == {iso, trn, ref, val, box}

and trn is not a subtype of iso

therefore, using the rule written in the comment above that "every possible instantiation of sub must be a subtype of every possible instantiation of super", trn is not a subtype of #read

Right?

Your logic is excellent, but no :) #read = {ref, val, box}. This is because iso and trn, while they can be read from, cannot be aliased as the same capability, which is the guarantee that #read demands.

Nevertheless, iso is a subtype of #read, which is what's being checked here, so your code is correct.

jemc · 2017-02-17T07:46:14Z

src/libponyc/type/cap.c

-  // Sub and super share the same initial bounds. Some instantiation of the
-  // sub rcap must be a subtype of every instantiation of the super rcap.
+  // Sub and super share the same initial bounds. Every instantiation of the
+  // super rcap must be a supertype of some instantiation of the sub rcap.


Note the subtle difference in the description here, which actually does change the semantics.

This distinction was actually the bulk of the bug, in my opinion, so please check my logic here carefully, as this is a part of the fix that I discovered on my own and didn't discuss with you in our last conversation about this issue.

I basically rewrote the entire switch-case from scratch here. It is very similar to the semantics of is_cap_sub_cap, except some extra cases are allowed when comparing gen-caps to gen-caps.

This is to be expected given the semantics I chose in this description, because the only real distinction from is_cap_sub_cap is the use of "some" instead of "every" in reference to the instantiations of the sub rcap, and this is a distinction without a difference when there is only one possible instantiation of the sub rcap.

Yes, exactly! And this only appears when checking if a typeparamref is a subtype of itself, given some (possibly different) cap.

jemc · 2017-02-17T07:48:24Z

src/libponyc/type/cap.c

+        case TK_CAP_SHARE: // {val, tag}
+        case TK_CAP_SEND:  // {iso, val, tag}
+        case TK_CAP_ALIAS: // {ref, val, box, tag}
+        case TK_CAP_ANY:   // {iso, trn, ref, val, box, tag}


As you can see, I've added comments for all the gencaps to show their expansion inline. I found this really helped me to keep my thinking straight when double-checking all the cases, including the case where I think I found a mistaken return true for the case of trn <: #read (see my next comment).

Comments for those are great.

jemc · 2017-02-17T07:57:33Z

@Praetonus the core of the issue was a conceptual conflation of how type parameter rcaps are checked in subtype.c. Compared to the normal logic for rcap subtype checking, we need special logic for checking constraint rcaps (implemented in this PR as is_cap_sub_cap_constraint), and we need yet a different kind of special logic for checking varying caps of a type parameter reference against eachother (is_cap_sub_cap_bound).

Previously these two different special case rcap checking rules were conflated as one, leading to the over-permissiveness in the previous logic for is_cap_sub_cap_bound, which you found and demonstrated in your snippet.

This PR separates the different cases into different functions in cap.c, makes sure that each case is following the correct (I hope!) rules, and reworks subtype.c so we can keep track of what kind of check we want to do when we finally get to the point of invoking the functions from cap.c.

jemc · 2017-02-17T08:03:11Z

As a side note, GitHub made the diff view of cap.c really impossible to read by jumbling all the lines together from different functions, so when reviewing I suggest maybe just looking at the final revision of the file here instead.

sylvanc · 2017-02-17T11:49:02Z

src/libponyc/type/cap.c

@@ -121,11 +101,8 @@ bool is_cap_sub_cap(token_id sub, token_id subalias, token_id super,
        case TK_REF:
        case TK_VAL:
        case TK_BOX:
-        case TK_CAP_READ:


Your logic is excellent, but no :) #read = {ref, val, box}. This is because iso and trn, while they can be read from, cannot be aliased as the same capability, which is the guarantee that #read demands.

sylvanc · 2017-02-17T11:50:54Z

src/libponyc/type/cap.c

@@ -121,11 +101,8 @@ bool is_cap_sub_cap(token_id sub, token_id subalias, token_id super,
        case TK_REF:
        case TK_VAL:
        case TK_BOX:
-        case TK_CAP_READ:


Nevertheless, iso is a subtype of #read, which is what's being checked here, so your code is correct.

sylvanc · 2017-02-17T11:51:32Z

src/libponyc/type/cap.c

          return true;

        default: {}
      }
      break;

-    case TK_BOX:
+    case TK_CAP_READ: // {iso, trn, ref, val, box}


#read = {ref, val, box}. The code is correct, but the comment isn't :)

sylvanc · 2017-02-17T11:52:50Z

src/libponyc/type/cap.c

+  // possible instantiation of super.
+  switch(super)
+  {
+    case TK_CAP_READ: // {iso, trn, ref, val, box}


This one is wrong. Only ref, val, box should be valid as #read constraints.

sylvanc · 2017-02-17T11:53:45Z

src/libponyc/type/cap.c

          return true;

        default: {}
      }
      break;

-    case TK_CAP_ALIAS:
-      switch(super)
+    case TK_CAP_ALIAS: // {ref, val, box, tag}


Also valid: TK_CAP_SHARE, TK_CAP_READ.

sylvanc · 2017-02-17T12:01:01Z

src/libponyc/type/cap.c

-
-        case TK_TRN_BIND:
+        case TK_CAP_SHARE: // {val, tag}
+        case TK_CAP_ALIAS: // {ref, val, box, tag}


Also TK_CAP_READ.

sylvanc · 2017-02-17T12:04:09Z

src/libponyc/type/cap.c

-        case TK_CAP_READ:
-        case TK_CAP_ALIAS:
+        case TK_CAP_SHARE: // {val, tag}
+        case TK_CAP_ALIAS: // {ref, val, box, tag}


TK_TRN is also in this case a subtype of TK_CAP_READ.

sylvanc · 2017-02-17T12:07:20Z

src/libponyc/type/cap.c

          return true;

        default: {}
      }
      break;

-    case TK_CAP_READ:
-    case TK_CAP_ALIAS:
+    case TK_CAP_READ: // {iso, trn, ref, val, box}


#read = {ref, val, box}. So also a subtype of TK_CAP_ALIAS and TK_CAP_SHARE ?

Actually, hmm, not so sure.

Yes on both counts.

Using the rule: "every instantiation of the super rcap must be a supertype of some instantiation of the sub rcap"

#share == {val, tag}

tag is a supertype of everything, so you can pick any instantiation of #read and it's supertype of it

val is a supertype of itself, which is included in #read

#alias == {ref, val, box, tag}

tag is a supertype of everything, so you can pick any instantiation of #read and it's supertype of it

box is a supertype of val, which is included in #read

val is a supertype of itself, which is included in #read

ref is a supertype of itself, which is included in #read

Ah ha! Yes. You're right.

sylvanc · 2017-02-17T12:09:54Z

src/libponyc/type/subtype.c

  ast_t* sub_cap = cap_fetch(sub);
  ast_t* sub_eph = ast_sibling(sub_cap);
  ast_t* super_cap = cap_fetch(super);
  ast_t* super_eph = ast_sibling(super_cap);

-  if(!is_cap_sub_cap(ast_id(sub_cap), ast_id(sub_eph),
-    ast_id(super_cap), ast_id(super_eph)))
+  if(check_cap == CHECK_CAP_SUB && !is_cap_sub_cap(ast_id(sub_cap),


Should these clauses be in a switch statement on check_cap ?

sylvanc · 2017-02-17T12:11:39Z

packages/itertools/iter.pony

@@ -84,7 +84,7 @@ class Iter[A] is Iterator[A]
    end
    false

-  fun ref collect[B: Seq[A!] = Array[A!]](coll: B): B^ =>
+  fun ref collect[B: Seq[A!] ref = Array[A!]](coll: B): B^ =>


I love that this bug is caught by this PR!

sylvanc · 2017-02-17T12:14:19Z

This looks great. Only problem is my bad choice of names for #read lead you to the conclusion that it should be demanding something... readable. But really it wants "readable and aliasable". Sorry about that.

jemc · 2017-02-17T16:37:10Z

@sylvanc Thanks for the quick review.

Yes, my mistaken understanding of what #read is makes me quite glad I added the comments showing the set of what I thought it was, since it made it easy for you to see the mistake that tripped me up. I will do a commit fixing up the points you noted.

sylvanc · 2017-02-17T16:39:14Z

Yup, the comments served an immediate and highly useful purpose :)

jemc · 2017-02-17T18:51:32Z

@sylvanc I made the fixes you mentioned in 36e032d.

However, I'm now a bit uneasy about this, because I observed the following about this rule for is_cap_sub_cap_bound:

Using the rule: "every instantiation of the super rcap must be a supertype of some instantiation of the sub rcap"

#any includes iso
iso is a subtype of every rcap
therefore, #any is a subtype of every rcap (by the above rule).

Same would be true for #send, which also includes iso

I don't think this is desirable though, because it leads to the allowing the very same unsafe cases that we are intending to disallow in this PR. In fact, when I tried adding that clause, my test case for violating capabilities via #any started failing (successfully violating) again.

This leads me to believe that the rule is still wrong. Can you do some more thinking about this, (I trust your thinking more than mine on disentangling these ideas)?

jemc · 2017-02-24T01:56:01Z

So, I've revised this branch based on lengthy discussion in this week's sync call in which we finished ironing out the logic together.

The original rule for is_cap_sub_cap_bound was correct (only for cases where we compare gencap to gencap - more on this later), but the way it was worded ("some instantiation of sub must be a subtype of every instantiation of super") was somewhat ambiguous, in that it could be read to mean either "there exists some instantiation of sub which is a subtype of every instantiation of super", or "for every instantiation of super, there exists some instantiation of sub which is a subtype of it" - the former is how I was reading it, but the latter is the correct interpretation. I believe that my rephrasing ("every instantiation of super must be a supertype of some instantiation of sub") makes the correct interpretation a bit clearer and more obvious.

However, for cases where either sub or super is a single/specific cap, we want to abandon the above rule and fall back to the original rule for is_cap_sub_cap. This logic is now encoded in the switch/case "truth table" for is_cap_sub_cap_bound.

The PR should be ready for final review, and merging.

jemc force-pushed the fix/gencap-violation branch from 332b4dd to 3cf0fc3 Compare February 17, 2017 07:24

jemc requested a review from sylvanc February 17, 2017 07:28

Fix capability checking for gencap-constrained type parameters.

63afe88

Resolves #1328.

jemc force-pushed the fix/gencap-violation branch from 3cf0fc3 to 63afe88 Compare February 17, 2017 07:29

jemc commented Feb 17, 2017

View reviewed changes

jemc added the changelog - fixed Automatically add "Fixed" CHANGELOG entry on merge label Feb 17, 2017

sylvanc suggested changes Feb 17, 2017

View reviewed changes

Fixes based on sylvanc's code review.

36e032d

jemc added 2 commits February 23, 2017 13:21

Fix subtyping rule in is_cap_sub_cap_bound function.

26ded4e

Merge branch 'master' into fix/gencap-violation

5333ad8

sylvanc approved these changes Feb 24, 2017

View reviewed changes

sylvanc merged commit 97f119c into master Feb 24, 2017

ponylang-main added a commit that referenced this pull request Feb 24, 2017

Update CHANGELOG for PR #1593

c714443

jemc deleted the fix/gencap-violation branch July 6, 2017 02:05

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix capability checking for gencap-constrained type parameters. #1593

Fix capability checking for gencap-constrained type parameters. #1593

jemc commented Feb 17, 2017

jemc commented Feb 17, 2017

Praetonus commented Feb 17, 2017

jemc left a comment

jemc Feb 17, 2017

sylvanc Feb 17, 2017

jemc Feb 17, 2017 •

edited

Loading

sylvanc Feb 17, 2017

sylvanc Feb 17, 2017

jemc Feb 17, 2017 •

edited

Loading

sylvanc Feb 17, 2017

jemc Feb 17, 2017 •

edited

Loading

sylvanc Feb 17, 2017

jemc commented Feb 17, 2017

jemc commented Feb 17, 2017

sylvanc Feb 17, 2017

sylvanc Feb 17, 2017

sylvanc Feb 17, 2017

sylvanc Feb 17, 2017

sylvanc Feb 17, 2017

sylvanc Feb 17, 2017

sylvanc Feb 17, 2017

sylvanc Feb 17, 2017

sylvanc Feb 17, 2017

jemc Feb 17, 2017

sylvanc Feb 17, 2017

sylvanc Feb 17, 2017

sylvanc Feb 17, 2017

sylvanc commented Feb 17, 2017

jemc commented Feb 17, 2017

sylvanc commented Feb 17, 2017

jemc commented Feb 17, 2017

jemc commented Feb 24, 2017

Fix capability checking for gencap-constrained type parameters. #1593

Fix capability checking for gencap-constrained type parameters. #1593

Conversation

jemc commented Feb 17, 2017

jemc commented Feb 17, 2017

Praetonus commented Feb 17, 2017

jemc left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jemc Feb 17, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jemc Feb 17, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jemc Feb 17, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jemc commented Feb 17, 2017

jemc commented Feb 17, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

sylvanc commented Feb 17, 2017

jemc commented Feb 17, 2017

sylvanc commented Feb 17, 2017

jemc commented Feb 17, 2017

jemc commented Feb 24, 2017

jemc Feb 17, 2017 •

edited

Loading

jemc Feb 17, 2017 •

edited

Loading

jemc Feb 17, 2017 •

edited

Loading