Check return types #615

bakkot · 2024-09-17T17:58:41Z

Based on #613.

This will give errors for cases like

<emu-clause id="example" type="abstract operation">
  <h1>
    Example (): a Number
  </h1>
  <dl class="header"></dl>
  <emu-alg>
    1. Return 0.
  </emu-alg>
</emu-clause>

such as

Error: test.emu:13:23: returned value (0) does not look plausibly assignable to algorithm's return type (Number)
hint: you returned a mathematical value, but this algorithm returns an ES language Number

Fixes #609 by moving the logic for checking for returned abrupt completions out of an ad-hoc bit of Algorithm.ts and into the typechecker as part of a more general facility for checking the return types from algorithms.

This also drops the special handling for GeneratorYield and instead adds a new attribute, "skip return checks", which will need to be added to it as well as Completion and NormalCompletion and any other algorithms which are doing weird stuff in the future. As such, this is a breaking change (but only very slightly).

This introduces no new errors on ecma262, ecma402, or proposal-temporal except for the three algorithms called out in the previous paragraph, which will be fixed by adding the new attribute when upstreaming this change.

The actual logic, in inspectReturns, is pleasingly simple: we just look for Return Foo., parse Foo the same way we parse arguments to AO calls, and compare its type to the algorithm's return type the same way we'd compare a call argument to the corresponding AO's corresponding parameter type. We also look for ? and Throw and etc so we can ensure the containing algorithm returns an abrupt completion.

src/type-logic.ts

michaelficarra · 2024-09-18T01:30:00Z

spec/index.html

@@ -212,6 +212,7 @@ <h1>Structured Headers</h1>
            <li><b>for:</b> The type of value to which a clause of type "concrete method" or "internal method" applies.</li>
            <li><b>redefinition:</b> If "true", the name of the operation will not automatically link (i.e., it will not automatically be given an aoid).</li>
            <li><b>skip global checks:</b> If "true", disables consistency checks for this AO which require knowing every callsite.</li>
+            <li><b>skip return checks:</b> If "true", disables checking that the returned values from this AO correspond to its declared return type.</li>


Instead of skipping return checks, shouldn't we be asserting that the return check fails? That way if it is later changed in such a way that it passes, we know we can remove the annotation.

That would probably be better but I don't want to do the work to implement it. PRs welcome.

OK actually that was trivial, done.

src/typechecker.ts

michaelficarra · 2024-09-18T01:32:24Z

src/typechecker.ts

@@ -179,6 +185,37 @@ const getExpressionVisitor =
    }
  };

+type ErrorForUsingTypeXAsTypeY =
+  | null
+  | 'number-to-math'


For completion's sake, shouldn't we have bigint-to-real?

Sure I guess. That's not related to this PR but I can fold it in.

michaelficarra · 2024-09-18T01:34:50Z

src/typechecker.ts

+                '\nhint: you passed a mathematical value, but this position takes an ES language BigInt';
+              break;
+            }
+            case 'other': {


Instead of testing for null above, either use a default or (if you're looking to get an exhaustivity check from TS), fallthrough with case null: here.

The test for null guards the whole error-producing logic, not just this switch case.

src/typechecker.ts

michaelficarra · 2024-09-18T01:38:12Z

src/typechecker.ts

@@ -332,6 +435,152 @@ function isConsumedAsCompletion(expr: Expr, path: PathItem[]) {
  return false;
 }

+// returns a boolean to indicate whether this line can return an abrupt completion, or null to indicate we should stop caring


I don't really like that. Can't we make an enum for it?

Then we couldn't use ||=.

just implement Functor 😛

michaelficarra

I think we're missing tests where the completiony-ness of an Abstract Closure doesn't match that of the containing algorithm (in both ways).

bakkot · 2024-09-18T01:54:52Z

I think we're missing tests where the completiony-ness of an Abstract Closure doesn't match that of the containing algorithm (in both ways).

We have an assertion that this is not an error:

<emu-clause id="example" type="abstract operation">
<h1>
  ExampleAlg (): a mathematical value
</h1>
<dl class="header">
</dl>
<emu-alg>
  1. Let _addend_ be 41.
  1. Let _closure_ be a new Abstract Closure with parameters (_x_) that captures _addend_ and performs the following steps when called:
    1. Return _x_ + ? ExampleCompletionAO(_addend_).
  1. Let _val_ be ! _closure_(1).
  1. Return _val_.
</emu-alg>
</emu-clause>

What else are you looking for?

michaelficarra · 2024-09-18T01:59:26Z

Ah that's right, I misread this test and thought they were both returning completion records. Then the only one we're missing is one where the algorithm returns a completion but the AC returns a non-completion.

bakkot · 2024-09-18T02:08:17Z

Then the only one we're missing is one where the algorithm returns a completion but the AC returns a non-completion.

That wouldn't be an error even with no handling of ACs because values returned from AOs which return completions are automatically boxed into NormalCompletion.

michaelficarra · 2024-09-18T02:16:33Z

I wouldn't expect the Return steps inside an AC to auto-wrap in NormalCompletion just because the containing algorithm is declared to return a completion. If that's how it currently works, it shouldn't be.

bakkot · 2024-09-18T02:51:27Z

I wouldn't expect the Return steps inside an AC to auto-wrap in NormalCompletion just because the containing algorithm is declared to return a completion. If that's how it currently works, it shouldn't be.

It's not, but ACs don't have return types. The bodies of ACs are exempt from the return type analysis entirely.

My point is that if the body incorrectly weren't exempt from the analysis, such that a return in the body of the AC were to be incorrectly considered to be returning from the containing AO, and we had e.g. return 0 in an AO declared to return a normal completion containing a real number, that still wouldn't be an error (because of the auto-boxing logic).

So there's no test you could write here which would fail under any code we could have written. So there's no reason to have a test.

michaelficarra

I might call this something else now, but LGTM either way.

jmdyck · 2024-09-19T01:16:00Z

I wouldn't expect the Return steps inside an AC to auto-wrap in NormalCompletion just because the containing algorithm is declared to return a completion. If that's how it currently works, it shouldn't be.

The spec isn't entirely clear on this point. 5.2.3.5 "Implicit Normal Completion" says "In algorithms within abstract operations which are declared to return a Completion Record, ..." which would seem to include an AC within such an AO.

Maybe that section should carve out an exception for ACs. But then the question might arise as to whether ACs have their own rule for implicit NormalCompletion. Some seem to be written under the assumption of auto-wrapping.

(Tangent: maybe ACs should explicitly state their return type.)

michaelficarra reviewed Sep 18, 2024

View reviewed changes

src/type-logic.ts Outdated Show resolved Hide resolved

michaelficarra reviewed Sep 18, 2024

View reviewed changes

src/typechecker.ts Outdated Show resolved Hide resolved

michaelficarra reviewed Sep 18, 2024

View reviewed changes

src/typechecker.ts Outdated Show resolved Hide resolved

michaelficarra reviewed Sep 18, 2024

View reviewed changes

bakkot force-pushed the handle-completions-better branch from 5a93027 to 53462ac Compare September 18, 2024 02:19

bakkot force-pushed the check-return-types branch from 36b9f1c to a805c61 Compare September 18, 2024 02:53

michaelficarra approved these changes Sep 19, 2024

View reviewed changes

Base automatically changed from handle-completions-better to main September 22, 2024 17:47

bakkot added 6 commits September 22, 2024 10:48

check return types

1bfa658

handle abstract closures

61b87ee

add attribute for skipping return checks

2c75261

fixup after rebase

21e92ad

address comments

239c00a

make skip-return-checks xfail

5741bfc

bakkot force-pushed the check-return-types branch from 795a6dd to 5741bfc Compare September 22, 2024 17:48

bakkot merged commit 36fc866 into main Sep 22, 2024
2 checks passed

bakkot deleted the check-return-types branch September 22, 2024 17:50

bakkot mentioned this pull request Sep 22, 2024

Version 20.0.0 #617

Merged

Graysonbarton mentioned this pull request Oct 31, 2024

[Snyk] Upgrade ecmarkup from 18.3.1 to 20.0.0 Graysonbarton/ecma262#6

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Check return types #615

Check return types #615

bakkot commented Sep 17, 2024 •

edited

Loading

michaelficarra Sep 18, 2024

bakkot Sep 18, 2024

bakkot Sep 18, 2024

michaelficarra Sep 18, 2024

bakkot Sep 18, 2024

michaelficarra Sep 18, 2024

bakkot Sep 18, 2024

michaelficarra Sep 18, 2024

bakkot Sep 18, 2024

michaelficarra Sep 18, 2024

bakkot Sep 18, 2024

michaelficarra left a comment

bakkot commented Sep 18, 2024

michaelficarra commented Sep 18, 2024

bakkot commented Sep 18, 2024

michaelficarra commented Sep 18, 2024

bakkot commented Sep 18, 2024

michaelficarra left a comment

jmdyck commented Sep 19, 2024

Check return types #615

Check return types #615

Conversation

bakkot commented Sep 17, 2024 • edited Loading

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

michaelficarra left a comment

Choose a reason for hiding this comment

bakkot commented Sep 18, 2024

michaelficarra commented Sep 18, 2024

bakkot commented Sep 18, 2024

michaelficarra commented Sep 18, 2024

bakkot commented Sep 18, 2024

michaelficarra left a comment

Choose a reason for hiding this comment

jmdyck commented Sep 19, 2024

bakkot commented Sep 17, 2024 •

edited

Loading