diff --git a/SPEC.md b/SPEC.md index e800a8d..564178e 100644 --- a/SPEC.md +++ b/SPEC.md @@ -51,6 +51,8 @@ Annotations are TypeScript comments of the form `//@ `. | `autohavoc` | File-level, or before a `//@ verify` function | Abstract every unmodellable expression to a nondeterministic value, so verification rests only on declared contracts (see §2.12). Dafny only. | | `skip` | Before a statement or top-level value declaration | Omit it from the verification model (for side-effect-only code or an intentionally unsupported declaration). | +`lsc` rejects a `//@` comment it does not read: a malformed one, an unknown keyword, or a `requires`, `ensures`, `contract`, `invariant`, `decreases`, `done_with` or `type` placed where nothing takes it. Placement is not checked inside declarations left out on purpose (unselected, `extern` or `skip`), and TypeScript's own `//@ts-…` comments are left alone. + ### 2.2 Spec Expression Grammar At top level, `//@ skip` may precede a function, class, or `const` declaration; diff --git a/examples/nullableArray.ts b/examples/nullableArray.ts index 0e0c639..161da26 100644 --- a/examples/nullableArray.ts +++ b/examples/nullableArray.ts @@ -67,7 +67,6 @@ export function dropOrphans(messages: Message[]): Message[] { let i = 0; while (i < messages.length) { - //@ type i nat //@ invariant i <= messages.length //@ invariant filteredContents.length === messages.length const cur = filteredContents[i]; @@ -80,7 +79,6 @@ export function dropOrphans(messages: Message[]): Message[] { const result: Message[] = []; let j = 0; while (j < messages.length) { - //@ type j nat //@ invariant j <= messages.length //@ invariant result.length <= j const f = filteredContents[j]; diff --git a/examples/readonlyArray.ts b/examples/readonlyArray.ts index bf339a5..395d47e 100644 --- a/examples/readonlyArray.ts +++ b/examples/readonlyArray.ts @@ -14,6 +14,5 @@ export function firstOrZero(xs: readonly number[]): number { export function lengthOf(xs: ReadonlyArray): number { //@ ensures \result === xs.length - //@ type T return xs.length; } diff --git a/examples/toposort.ts b/examples/toposort.ts index 32916e4..c65078e 100644 --- a/examples/toposort.ts +++ b/examples/toposort.ts @@ -72,7 +72,6 @@ export function topologicalSort( let sorted: string[] = []; let qHead = 0; while (qHead < queue.length) { - //@ type qHead nat //@ invariant qHead <= queue.length //@ invariant sorted.length === qHead //@ invariant sorted.length <= nodeIds.length diff --git a/tools/src/config.ts b/tools/src/config.ts index c76da25..8527094 100644 --- a/tools/src/config.ts +++ b/tools/src/config.ts @@ -130,13 +130,14 @@ function parseDirectiveValue(key: keyof OptionSpecs, text: string, source: strin } /** - * Find comment lines, marking those that occur before any code. + * Find comment lines and the comment on each, marking those that occur before + * any code. * * Use the parsed syntax tree to skip strings, regexes, and template text. * Without those boundaries, the scanner can read /[/*]/ as a block comment * or treat a template's closing backtick as the start of another template. */ -function* fileCommentLines(sourceText: string): Generator<{ text: string; index: number; inLeadingRegion: boolean }> { +export function* fileCommentLines(sourceText: string): Generator<{ text: string; comment: string; index: number; inLeadingRegion: boolean }> { // Normalize once so a leading BOM also works before a shebang. sourceText = sourceText.replace(/^\uFEFF/, ""); const lines = sourceText.split(/\r\n|[\n\r\u2028\u2029]/); @@ -163,8 +164,9 @@ function* fileCommentLines(sourceText: string): Generator<{ text: string; index: if (token === ts.SyntaxKind.SingleLineCommentTrivia || token === ts.SyntaxKind.MultiLineCommentTrivia) { const firstLine = sourceFile.getLineAndCharacterOfPosition(scanner.getTokenStart()).line; const lastLine = sourceFile.getLineAndCharacterOfPosition(scanner.getTokenEnd() - 1).line; + const comment = scanner.getTokenText(); for (let index = firstLine; index <= lastLine; index++) { - yield { text: lines[index], index, inLeadingRegion }; + yield { text: lines[index], comment, index, inLeadingRegion }; } } else if (token !== ts.SyntaxKind.WhitespaceTrivia && token !== ts.SyntaxKind.NewLineTrivia && token !== ts.SyntaxKind.ShebangTrivia) { @@ -175,6 +177,22 @@ function* fileCommentLines(sourceText: string): Generator<{ text: string; index: } } +const OPTION_DIRECTIVE = /^[ \t]*\/\/@[ \t]+option(?:[ \t]+(.*?))?[ \t]*$/; +const ALIAS_DIRECTIVE = /^[ \t]*\/\/@[ \t]+([A-Za-z][A-Za-z0-9-]*)[ \t]*$/; + +/** The option a legacy alias such as `//@ safe-slice` sets, if `line` is one. */ +function aliasedOption(line: string): keyof OptionSpecs | undefined { + const alias = line.match(ALIAS_DIRECTIVE)?.[1]; + if (alias === undefined) return undefined; + return KNOWN_KEYS.find(key => "directiveAliases" in OPTION_SPECS[key] && + (OPTION_SPECS[key].directiveAliases as readonly string[]).includes(alias)); +} + +/** Whether `parseFileOptions` reads `line` as an option directive or a legacy alias. */ +export function isOptionDirective(line: string): boolean { + return OPTION_DIRECTIVE.test(line) || aliasedOption(line) !== undefined; +} + /** Parse top-of-file `//@ option key value` directives and legacy aliases. */ export function parseFileOptions(sourceText: string, source: string): ExplicitOptions { const seen = new Map(); @@ -191,7 +209,7 @@ export function parseFileOptions(sourceText: string, source: string): ExplicitOp const parseLine = (lineText: string, index: number, inLeadingRegion: boolean): void => { const line = index + 1; - const optionMatch = lineText.match(/^[ \t]*\/\/@[ \t]+option(?:[ \t]+(.*?))?[ \t]*$/); + const optionMatch = lineText.match(OPTION_DIRECTIVE); if (optionMatch) { if (!inLeadingRegion) fail(`${source}:${line}`, "//@ option directives must appear before the first source statement"); const parts = (optionMatch[1] ?? "").trim().split(/\s+/).filter(Boolean); @@ -206,19 +224,10 @@ export function parseFileOptions(sourceText: string, source: string): ExplicitOp return; } - const aliasMatch = lineText.match(/^[ \t]*\/\/@[ \t]+([A-Za-z][A-Za-z0-9-]*)[ \t]*$/); - if (!aliasMatch) return; - const alias = aliasMatch[1]; - for (const key of KNOWN_KEYS) { - const aliases = "directiveAliases" in OPTION_SPECS[key] - ? OPTION_SPECS[key].directiveAliases as readonly string[] - : []; - if (!aliases.includes(alias)) continue; - // Legacy aliases retain their pre-config placement behavior. New generic - // option directives are deliberately restricted to the file preamble. - setOption(key, true as LscOptions[typeof key], line); - return; - } + // Legacy aliases retain their pre-config placement behavior. New generic + // option directives are deliberately restricted to the file preamble. + const key = aliasedOption(lineText); + if (key) setOption(key, true as LscOptions[typeof key], line); }; for (const { text, index, inLeadingRegion } of fileCommentLines(sourceText)) { diff --git a/tools/src/extract.ts b/tools/src/extract.ts index 795cd28..341cc59 100644 --- a/tools/src/extract.ts +++ b/tools/src/extract.ts @@ -11,7 +11,7 @@ import { initTypeParser } from "./types.js"; import type { RawExpr, RawStmt, RawFunction, RawModule, RawClass, RawConst, RawGhostLet, RawGhostAssign } from "./rawir.js"; import { normalizeBigIntLiteral } from "./rawir.js"; import { setUserNames, freshName } from "./names.js"; -import { DEFAULT_OPTIONS, type LscOptions } from "./config.js"; +import { DEFAULT_OPTIONS, fileCommentLines, isOptionDirective, type LscOptions } from "./config.js"; // ── Expression extraction ──────────────────────────────────── @@ -737,24 +737,82 @@ function extractExpr(node: Expression): RawExpr { const PREFIX = "//@ "; const KEYWORDS = ["requires", "ensures", "contract", "invariant", "decreases", "done_with", "type"] as const; +/** The other directives (SPEC §2.1) besides options, read by keyword elsewhere. */ +const DIRECTIVES = ["verify", "pure", "impure", "skip", "extern", "havoc", "autohavoc", "assert", "assume", + "ghost", "declare-type", "backend", "lean-module"]; export type AnnotKind = (typeof KEYWORDS)[number]; -interface Annotation { kind: AnnotKind; expr: string } +/** `line` is set only for annotations in the file being extracted. */ +interface Annotation { kind: AnnotKind; expr: string; line?: number } + +function parseAnnotation(text: string): Annotation | null { + if (!text.startsWith(PREFIX)) return null; + const content = text.slice(PREFIX.length); + const sp = content.indexOf(" "); + if (sp === -1) return null; + const kw = content.slice(0, sp); + if (!(KEYWORDS as readonly string[]).includes(kw)) return null; + return { kind: kw as AnnotKind, expr: content.slice(sp + 1).trim() }; +} function parseAnnotations(node: Node): Annotation[] { const result: Annotation[] = []; for (const range of node.getLeadingCommentRanges()) { - const text = range.getText().trim(); - if (!text.startsWith(PREFIX)) continue; - const content = text.slice(PREFIX.length); - const sp = content.indexOf(" "); - if (sp === -1) continue; - const kw = content.slice(0, sp); - if (!(KEYWORDS as readonly string[]).includes(kw)) continue; - result.push({ kind: kw as AnnotKind, expr: content.slice(sp + 1).trim() }); + const a = parseAnnotation(range.getText().trim()); + if (!a) continue; + a.line = currentFileLine(node, range.getPos()); + result.push(a); } return result; } +/** The line of `pos` in `node`'s file, when that is the file being extracted. */ +function currentFileLine(node: Node, pos: number): number | undefined { + const sourceFile = node.getSourceFile(); + return sourceFile === _currentSourceFile ? sourceFile.getLineAndColumnAtPos(pos).line : undefined; +} + +/** Lines of the annotations whose value reached the Raw IR. */ +const _readLines = new Set(); +/** Line spans the extractor leaves out on purpose: `//@ skip`, unselected and extern functions. */ +const _skippedSpans: [number, number][] = []; + +/** The annotation's expression, recording that it was read. */ +function readExpr(a: Annotation): string { + if (a.line !== undefined) _readLines.add(a.line); + return a.expr; +} +function annotExprs(annots: Annotation[], kind: AnnotKind): string[] { + return annots.filter(a => a.kind === kind).map(readExpr); +} +/** Only the first is read; a repeated one is reported as unread. */ +function firstAnnotExpr(annots: Annotation[], kind: AnnotKind): string | null { + const a = annots.find(a => a.kind === kind); + return a ? readExpr(a) : null; +} +function skipSpan(node: Node): void { + const first = node.getLeadingCommentRanges()[0]; + const from = first ? node.getSourceFile().getLineAndColumnAtPos(first.getPos()).line : node.getStartLineNumber(); + _skippedSpans.push([from, node.getEndLineNumber()]); +} + +/** Fail on `//@` comments lsc ignores: a malformed or unknown one, or a + * contract annotation where no reader looks. Other directives are checked + * by keyword only. TypeScript's `//@ts-…` comments are not ours. */ +function checkAnnotationsRead(sourceFile: SourceFile): void { + const errors: string[] = []; + for (const { comment, index } of fileCommentLines(sourceFile.getFullText())) { + const text = comment.trim(); + if (!text.startsWith("//@") || text.startsWith("//@ts-")) continue; + const line = index + 1; + const keyword = text.match(/^\/\/@ (\S+)(?: |$)/)?.[1]; + const read = parseAnnotation(text) + ? _readLines.has(line) || _skippedSpans.some(([from, to]) => from <= line && line <= to) + : DIRECTIVES.includes(keyword ?? "") || isOptionDirective(text); + if (!read) errors.push(`${sourceFile.getBaseName()}:${line}: lsc does not read this annotation: ${text}`); + } + if (errors.length > 0) throw new Error(errors.join("\n")); +} + function collectAnnotations(node: Node, body?: Node[]): Annotation[] { const own = parseAnnotations(node); if (body && body.length > 0) return [...own, ...parseAnnotations(body[0])]; @@ -881,8 +939,8 @@ function extractTypeDecl(decl: TypeAliasDeclaration, extraDecls?: TypeDeclInfo[] // Leading `//@ type ` overrides extraction — the declared TS type is // replaced by the annotated backend type. Used to coerce literal unions // (`5 | 15 | 30` → `nat`) and other types LS can't model precisely. - const override = parseAnnotations(decl).find(a => a.kind === "type"); - if (override) return { name, typeParams: tpField, kind: "alias", aliasOf: override.expr }; + const override = firstAnnotExpr(parseAnnotations(decl), "type"); + if (override) return { name, typeParams: tpField, kind: "alias", aliasOf: override }; if (type.isUnion()) { const members = type.getUnionTypes(); @@ -979,7 +1037,9 @@ function extractInterface(decl: InterfaceDeclaration, extraDecls?: TypeDeclInfo[ if (Node.isPropertySignature(member)) { const text = member.getTrailingCommentRanges().map(r => r.getText()).join(" "); const match = text.match(/\/\/@ type (\w+)/); - if (match) overrides.set(member.getName(), match[1]); + if (match) { + overrides.set(member.getName(), readExpr({ kind: "type", expr: match[1], line: currentFileLine(member, member.getEnd()) })); + } } } return extractRecord(decl.getName(), decl.getType(), decl, overrides, extraDecls); @@ -1400,6 +1460,7 @@ function extractStmts(stmts: Node[]): RawStmt[] { // //@ skip — omit this statement from the verification model if (leadingComments.some(r => r.getText().trim() === "//@ skip")) { + skipSpan(s); continue; } @@ -1606,9 +1667,9 @@ function extractStmts(stmts: Node[]): RawStmt[] { result.push({ kind: "while", cond: extractExpr(s.getExpression()), - invariants: annots.filter(a => a.kind === "invariant").map(a => a.expr), - decreases: annots.find(a => a.kind === "decreases")?.expr ?? null, - doneWith: annots.find(a => a.kind === "done_with")?.expr ?? null, + invariants: annotExprs(annots, "invariant"), + decreases: firstAnnotExpr(annots, "decreases"), + doneWith: firstAnnotExpr(annots, "done_with"), body: extractStmts(bodyStmts), line, }); @@ -1656,8 +1717,8 @@ function extractStmts(stmts: Node[]): RawStmt[] { kind: "forof", names, iterable: extractExpr(iterableExpr), - invariants: annots.filter(a => a.kind === "invariant").map(a => a.expr), - doneWith: annots.find(a => a.kind === "done_with")?.expr ?? null, + invariants: annotExprs(annots, "invariant"), + doneWith: firstAnnotExpr(annots, "done_with"), body: extractStmts(bodyStmts), line, }); @@ -1717,9 +1778,9 @@ function extractStmts(stmts: Node[]): RawStmt[] { } let condExpr: RawExpr = cond ? extractExpr(cond) : { kind: "bool", value: true }; - let invariants = annots.filter(a => a.kind === "invariant").map(a => a.expr); - let decreases = annots.find(a => a.kind === "decreases")?.expr ?? null; - let doneWith = annots.find(a => a.kind === "done_with")?.expr ?? null; + let invariants = annotExprs(annots, "invariant"); + let decreases = firstAnnotExpr(annots, "decreases"); + let doneWith = firstAnnotExpr(annots, "done_with"); for (const [from, to] of renames) { for (let k = 0; k < hoisted.length; k++) hoisted[k] = renameRawStmt(hoisted[k], from, to); condExpr = renameRawExpr(condExpr, from, to); @@ -1756,8 +1817,8 @@ function extractStmts(stmts: Node[]): RawStmt[] { kind: "forof", names: [name], iterable: extractExpr(s.getExpression()), - invariants: annots.filter(a => a.kind === "invariant").map(a => a.expr), - doneWith: annots.find(a => a.kind === "done_with")?.expr ?? null, + invariants: annotExprs(annots, "invariant"), + doneWith: firstAnnotExpr(annots, "done_with"), body: extractStmts(bodyStmts), line, }); @@ -1976,7 +2037,9 @@ function extractFunctionInner(fn: FunctionDeclaration, parentAnnotations?: Annot for (const a of annots) { if (a.kind === "type") { const parts = a.expr.split(/\s+/); - if (parts.length === 2) typeAnnotations.push({ name: parts[0], type: parts[1] }); + if (parts.length !== 2) continue; + readExpr(a); + typeAnnotations.push({ name: parts[0], type: parts[1] }); } } @@ -2065,10 +2128,10 @@ function extractFunctionInner(fn: FunctionDeclaration, parentAnnotations?: Annot if (inferred.isAny()) return "unknown"; return _eraseGenerics(typeToString(inferred)); })(), - requires: annots.filter(a => a.kind === "requires").map(a => a.expr), - ensures: annots.filter(a => a.kind === "ensures").map(a => a.expr), - contract: annots.filter(a => a.kind === "contract").map(a => a.expr), - decreases: annots.find(a => a.kind === "decreases")?.expr ?? null, + requires: annotExprs(annots, "requires"), + ensures: annotExprs(annots, "ensures"), + contract: annotExprs(annots, "contract"), + decreases: firstAnnotExpr(annots, "decreases"), pure: hasPureAnnotation(fn, body && Node.isBlock(body) ? body.getStatements() as Node[] : undefined), autohavoc: false, // set in extractModule (file-level directive or per-function) typeAnnotations, @@ -2094,6 +2157,8 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA // here), deduped by qualified name. _externs.clear(); _externSigTypes.length = 0; + _readLines.clear(); + _skippedSpans.length = 0; // Match a `//@ ` directive only as the first non-whitespace on a line, // so prose mentioning an annotation does not activate it. @@ -2204,7 +2269,7 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA const constants: RawConst[] = []; for (const stmt of sourceFile.getStatements()) { if (Node.isVariableStatement(stmt)) { - if (hasLeadingDirective(stmt, "skip")) continue; + if (hasLeadingDirective(stmt, "skip")) { skipSpan(stmt); continue; } for (const decl of stmt.getDeclarationList().getDeclarations()) { if (stmt.getDeclarationList().getFlags() & 2 /* const */) { const init = decl.getInitializer(); @@ -2361,6 +2426,12 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA ); const hasVerifyDirective = nonExternFns.some(hasVerify) || hasVerifiedClassMethod; const fnsToExtract = hasVerifyDirective ? nonExternFns.filter(hasVerify) : nonExternFns; + // A statement holding a selected function keeps its comments checked. + for (const f of allFns) { + if (fnsToExtract.includes(f)) continue; + const wholeStmt = f.parentStmt && !fnsToExtract.some(s => s.parentStmt === f.parentStmt); + skipSpan(wholeStmt ? f.parentStmt! : f.node); + } // `//@ autohavoc` — enable the auto-havoc abstraction (see autohavoc.ts). // File-level: a directive at column 0 (top of file) enables it for every @@ -2739,11 +2810,11 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA // Extract classes with //@ verify methods const classes: RawClass[] = []; for (const cls of sourceFile.getClasses()) { - if (hasLeadingDirective(cls, "skip")) continue; + if (hasLeadingDirective(cls, "skip")) { skipSpan(cls); continue; } const methods: RawFunction[] = []; for (const method of cls.getMethods()) { - if (hasLeadingDirective(method, "skip")) continue; - if (!method.getFullText().includes('//@ verify')) continue; + if (hasLeadingDirective(method, "skip")) { skipSpan(method); continue; } + if (!method.getFullText().includes('//@ verify')) { skipSpan(method); continue; } methods.push(extractFunction(method as any)); } if (methods.length === 0) continue; @@ -2758,6 +2829,8 @@ export function extractModule(sourceFile: SourceFile, options: LscOptions = DEFA // union stringification outside of an extractModule call. _synthArrayUnions = null; + checkAnnotationsRead(sourceFile); + return { file: sourceFile.getFilePath(), typeDecls, diff --git a/tools/tests/unread-annotations.test.ts b/tools/tests/unread-annotations.test.ts new file mode 100644 index 0000000..4b97479 --- /dev/null +++ b/tools/tests/unread-annotations.test.ts @@ -0,0 +1,57 @@ +import { test } from "node:test"; +import assert from "node:assert/strict"; +import { Project, ScriptTarget } from "ts-morph"; +import { extractModule } from "../src/extract.ts"; + +function extract(text: string) { + const project = new Project({ compilerOptions: { strict: true, + target: ScriptTarget.ESNext, lib: ["lib.esnext.d.ts"], types: [], skipLibCheck: true } }); + return extractModule(project.createSourceFile("f.ts", text)); +} + +const inBody = (annotation: string) => + `export function f(x: number): number {\n ${annotation}\n return x;\n}\n`; +const g = "export function g(x: number): number {\n //@ verify\n return x;\n}\n"; + +for (const [name, text, line] of [ + ["a missing space", inBody(String.raw`//@ensures \result > x`), 2], + ["extra spaces", inBody(String.raw`//@ ensures \result > x`), 2], + ["a tab after the keyword", inBody(String.raw`//@ ensures` + "\t" + String.raw`\result > x`), 2], + ["a missing expression", inBody("//@ ensures"), 2], + ["a misspelled keyword", inBody(String.raw`//@ ensure \result > x`), 2], + ["a block-body arrow", String.raw`//@ ensures \result > x` + "\nexport const f = (x: number): number => { return x; };\n", 1], + ["a statement before the function", String.raw`//@ ensures \result > x` + "\nconst unrelated = 1;\n" + inBody(""), 1], + ["a loop body requires", "export function f(n: number): number {\n let i = 0;\n while (i < n) {\n" + + " //@ invariant i <= n\n //@ requires false\n i = i + 1;\n }\n return i;\n}\n", 5], + ["a second decreases", "export function f(n: number): number {\n //@ decreases n\n //@ decreases n + 1\n" + + " return n <= 0 ? 0 : f(n - 1);\n}\n", 3], + ["a misspelled verify outside the selected functions", g + inBody("//@verify"), 6], + ["a tab after a directive", inBody("//@ assert\tfalse"), 2], + ["a selected arrow beside an unselected one", "export const a = (x: number): number => x,\n" + + " b = (x: number): number => {\n //@ verify\n const y = x;\n //@ ensures false\n return y;\n };\n", 5], +] as const) { + test(`an unread annotation with ${name} fails extraction`, () => { + assert.throws(() => extract(text), new RegExp(`^Error: f\\.ts:${line}: lsc does not read this annotation`)); + }); +} + +for (const [name, text] of [ + ["a contract above a function", String.raw`//@ ensures \result > x` + "\nexport function f(x: number): number {\n return x;\n}\n"], + ["a contract above an expression-body arrow", String.raw`//@ ensures \result > x` + "\nexport const f = (x: number): number => x;\n"], +] as const) { + test(`${name} is read`, () => { + assert.deepEqual(extract(text).functions[0].ensures, [String.raw`\result > x`]); + }); +} + +for (const [name, text] of [ + ["a contract in a function outside the selected ones", g + inBody(String.raw`//@ ensures \result > x`)], + ["a skipped statement", "export function f(n: number): number {\n //@ skip\n while (n > 0) {\n //@ requires false\n n = n - 1;\n }\n return n;\n}\n"], + ["a TypeScript directive", inBody("//@ts-ignore")], + ["an option with extra spaces", "//@ option safe-slice true\n" + inBody("")], + ["an option alias after a tab", "//@\tsafe-slice\n" + inBody("")], +] as const) { + test(`${name} still extracts`, () => { + assert.doesNotThrow(() => extract(text)); + }); +}