Fix unsound return types being allowed for autorecover #3595
Conversation
autorecover from trn now allows box returns, but not trns
|
Can you add one or more test cases that demonstrate code samples that currently do compile, but will have a compile error under the new change? |
Added a minimal test case which also demonstrates why it results in unsoundness. I can't find an example which demonstrates unsoundness without extracting (i.e. returning |
minimal-cases/issue-3571/3571.pony
Outdated
| let a_ref: A ref = bad.extract_trn() | ||
| let a_val: A val = (consume val bad).a_alias | ||
|
|
||
| env.out.print((a_ref is a_val).string()) |
There was a problem hiding this comment.
The minimal cases directory is for bugs that we don't know how to write automated tests for at this time.
If this is a test case that should cause a compiler error, it should go in the gtest suite instead (for example, in badpony.cc, or in one of the other similar compile error test files if you find a more appropriate place) so that it can have automated regression testing.
There was a problem hiding this comment.
Ah, whoops sorry. Misread what you meant by test case
There was a problem hiding this comment.
Thank you for mentioning badpony.cc
jasoncarr0
changed the title
|
|
||
| TEST_ERRORS_1(src, | ||
| "receiver type is not a subtype of target type") | ||
| } |
There was a problem hiding this comment.
This compiles today but is unsound
| " let a_box: A box = good.extract_box()\n"; | ||
|
|
||
| TEST_COMPILE(src); | ||
| } |
There was a problem hiding this comment.
This doesn't compile today but is sound
|
|
||
| TEST_ERRORS_1(src, | ||
| "receiver type is not a subtype of target type") | ||
| } |
There was a problem hiding this comment.
This doesn't compile either before or after, and is unsound to allow
| " dest.store(consume a_trn)\n"; | ||
|
|
||
| TEST_COMPILE(src); | ||
| } |
There was a problem hiding this comment.
This compiles both before and after and is sound
|
|
||
| TEST_ERRORS_1(src, | ||
| "receiver type is not a subtype of target type") | ||
| } |
There was a problem hiding this comment.
Extra case to ensure we don't allow non-ephemeral trn (which of course just becomes box)
|
@jemc did this need a changelog entry? |
I forgot to apply the label in the changelog bot that would make it automatically add the changelog entry. Sorry!
|
Sorry, I forgot to label it for the changelog bot. changelog entry added in 292efcc |
|
@jemc @jasoncarr0 are the releases notes I put at #3605 (comment) good or do they need to be modified? |
|
Looks good 👍 |
The existing autorecover code was checking whether it was safe to write to the recovery cap, regardless of whether it was an argument. That's correct for arguments, but for result types we need to ensure that it's safe to extract.
Safety to extract is derived from Steed's extracting table: a type is safe to extract if results in itself under extracting viewpoint adaptation. Thus it is unsound to extract
trnfromtrn, but it is sound to extractbox.Creating this now for any discussion on soundness/methods since it's a bit out of the blue that box would be safe to extract, but it shouldn't be surprising, since we can already get
boxout of the contents oftrn.Side note: the relevance of viewpoint adaptation may mean that we can use it to allow recovery in more places (in exchange for resulting in a weaker type). So that later we can call
ref (): T refmethods ontrnand get back abox.That said, we can turn
boxreturns off if it's too much of an addition to make without RFCFixes #3571