Skip to content

Commit

Permalink
make skip-return-checks xfail
Browse files Browse the repository at this point in the history
  • Loading branch information
bakkot committed Sep 18, 2024
1 parent a805c61 commit 795a6dd
Show file tree
Hide file tree
Showing 3 changed files with 94 additions and 41 deletions.
2 changes: 1 addition & 1 deletion spec/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -212,7 +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>
<li><b>skip return checks:</b> If "true", disables checking that the returned values from this AO correspond to its declared return type. Adding this to an AO which does not require it will produce a warning.</li>
</ul>
</li>
</ol>
Expand Down
36 changes: 29 additions & 7 deletions src/typechecker.ts
Original file line number Diff line number Diff line change
Expand Up @@ -283,11 +283,9 @@ export function typecheck(spec: Spec) {
)
? null
: false;
const returnType =
biblioEntry?._skipReturnChecks || signature?.return == null
? null
: typeFromExprType(signature.return);
const returnType = signature?.return == null ? null : typeFromExprType(signature.return);
let numberOfAbstractClosuresWeAreWithin = 0;
let hadReturnIssue = false;
const walkLines = (list: OrderedListNode) => {
for (const line of list.contents) {
let thisLineIsAbstractClosure = false;
Expand Down Expand Up @@ -324,7 +322,17 @@ export function typecheck(spec: Spec) {
thisLineIsAbstractClosure = true;
++numberOfAbstractClosuresWeAreWithin;
} else if (numberOfAbstractClosuresWeAreWithin === 0) {
const lineHadCompletionReturn = inspectReturns(warn, item, returnType, spec.biblio);
const returnWarn = biblioEntry?._skipReturnChecks
? () => {
hadReturnIssue = true;
}
: warn;
const lineHadCompletionReturn = inspectReturns(
returnWarn,
item,
returnType,
spec.biblio,
);
if (hasPossibleCompletionReturn != null) {
if (lineHadCompletionReturn == null) {
hasPossibleCompletionReturn = null;
Expand All @@ -350,11 +358,25 @@ export function typecheck(spec: Spec) {
isPossiblyAbruptCompletion(returnType) &&
hasPossibleCompletionReturn === false
) {
if (biblioEntry!._skipReturnChecks) {
hadReturnIssue = true;
} else {
spec.warn({
type: 'node',
ruleId: 'completion-algorithm-lacks-completiony-thing',
message:
'this algorithm is declared as returning an abrupt completion, but there is no step which might plausibly return an abrupt completion',
node,
});
}
}

if (biblioEntry?._skipReturnChecks && !hadReturnIssue) {
spec.warn({
type: 'node',
ruleId: 'completion-algorithm-lacks-completiony-thing',
ruleId: 'unnecessary-attribute',
message:
'this algorithm is declared as returning an abrupt completion, but there is no step which might plausibly return an abrupt completion',
'this algorithm has the "skip return check" attribute, but there is nothing which would cause an issue if it were removed',
node,
});
}
Expand Down
97 changes: 64 additions & 33 deletions test/typecheck.js
Original file line number Diff line number Diff line change
Expand Up @@ -598,39 +598,6 @@ describe('typechecking completions', () => {
</emu-alg>
</emu-clause>
`);

await assertLintFree(`
<emu-clause id="sec-completion-ao" type="abstract operation">
<h1>
Completion (
_completionRecord_: a Completion Record,
): a Completion Record
</h1>
<dl class="header">
<dt>skip return checks</dt>
<dd>true</dd>
</dl>
<emu-alg>
1. Assert: _completionRecord_ is a Completion Record.
1. Return _completionRecord_.
</emu-alg>
</emu-clause>
<emu-clause id="sec-normalcompletion" type="abstract operation">
<h1>
NormalCompletion (
_value_: any value except a Completion Record,
): a normal completion
</h1>
<dl class="header">
<dt>skip return checks</dt>
<dd>true</dd>
</dl>
<emu-alg>
1. Return Completion Record { [[Type]]: ~normal~, [[Value]]: _value_, [[Target]]: ~empty~ }.
</emu-alg>
</emu-clause>
`);
});
});

Expand Down Expand Up @@ -1916,6 +1883,70 @@ describe('error location', () => {
});
});

describe('skip return checks', () => {
it('respects the "skip return checks" attribute', async () => {
await assertLintFree(`
<emu-clause id="sec-completion-ao" type="abstract operation">
<h1>
Completion (
_completionRecord_: a Completion Record,
): a Completion Record
</h1>
<dl class="header">
<dt>skip return checks</dt>
<dd>true</dd>
</dl>
<emu-alg>
1. Assert: _completionRecord_ is a Completion Record.
1. Return _completionRecord_.
</emu-alg>
</emu-clause>
`);

await assertLintFree(`
<emu-clause id="example" type="abstract operation">
<h1>
ExampleAlg (): either a normal completion containing a Number or an abrupt completion
</h1>
<dl class="header">
<dt>skip return checks</dt>
<dd>true</dd>
</dl>
<emu-alg>
1. Let _foo_ be 0.
1. Return _foo_.
</emu-alg>
</emu-clause>
`);
});

it('warns when the "skip return checks" attribute is unnecessary', async () => {
await assertLint(
positioned`
<emu-clause id="example" type="abstract operation">
<h1>
ExampleAlg (): a mathematical value
</h1>
<dl class="header">
<dt>skip return checks</dt>
<dd>true</dd>
</dl>
${M}<emu-alg>
1. Let _foo_ be 0.
1. Return _foo_.
</emu-alg>
</emu-clause>
`,
{
ruleId: 'unnecessary-attribute',
nodeType: 'emu-alg',
message:
'this algorithm has the "skip return check" attribute, but there is nothing which would cause an issue if it were removed',
},
);
});
});

describe('special cases', () => {
it('NormalCompletion takes one argument', async () => {
await assertLint(
Expand Down

0 comments on commit 795a6dd

Please sign in to comment.