From 236c72b078d5b5639f01b663c70f6cb8d5e3ee81 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 17 Oct 2026 00:15:25 +0300 Subject: [PATCH] [PBT] Exclude pure static empty caches from class statement coverage --- .../src/class-coverage-source.ts | 17 +++++++- .../test/class-coverage-source.test.ts | 40 +++++++++++++++++++ .../scripts/test_class_coverage_replay.py | 20 ++++++++++ 3 files changed, 76 insertions(+), 1 deletion(-) diff --git a/usvm-ts-fast-check/fast-check-adapter/src/class-coverage-source.ts b/usvm-ts-fast-check/fast-check-adapter/src/class-coverage-source.ts index 7ea82753fb..5dae06e9d9 100644 --- a/usvm-ts-fast-check/fast-check-adapter/src/class-coverage-source.ts +++ b/usvm-ts-fast-check/fast-check-adapter/src/class-coverage-source.ts @@ -90,7 +90,13 @@ export function instrumentClassCoverage(file: ts.SourceFile, className: string): if (asynchronous) return unsupported('Async or generator callable properties are unsupported') members.push({ name, node: member, body: initializer.body, publicSurface, isStatic }) } else { - if (isStatic) return unsupported('Static property initialization is outside constructor coverage') + if (isStatic) { + if (!emptyStaticCache(member, selected.members)) { + return unsupported('Static property initialization is outside constructor coverage') + } + // Pure module-loading allocations stay outside the selected constructor/method statement universe. + continue + } initializers.push({ name, node: member, body: initializer, publicSurface: true, isStatic: false }) } } @@ -296,6 +302,15 @@ function memberName(member: ts.ClassElement): string | null { return null } +function emptyStaticCache(member: ts.PropertyDeclaration, members: ts.NodeArray): boolean { + if (!ts.isIdentifier(member.name) || !member.initializer || !ts.isArrayLiteralExpression(member.initializer) + || member.initializer.elements.length !== 0) return false + const name = member.name.text + if (['prototype', '__proto__', 'name', 'length', 'caller', 'arguments'].includes(name)) return false + return !members.some(other => other !== member && memberName(other) === name + && ts.canHaveModifiers(other) && ts.getModifiers(other)?.some(modifier => modifier.kind === ts.SyntaxKind.StaticKeyword)) +} + function executableStatement(node: ts.Statement): boolean { if (ts.isBlock(node) || ts.isEmptyStatement(node) || ts.isLabeledStatement(node) || ts.isFunctionDeclaration(node) || ts.isClassDeclaration(node) || ts.isInterfaceDeclaration(node) diff --git a/usvm-ts-fast-check/fast-check-adapter/test/class-coverage-source.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/class-coverage-source.test.ts index d2a12330dc..0646c172e3 100644 --- a/usvm-ts-fast-check/fast-check-adapter/test/class-coverage-source.test.ts +++ b/usvm-ts-fast-check/fast-check-adapter/test/class-coverage-source.test.ts @@ -99,6 +99,46 @@ test('supports private accessors and expression callable properties', () => { assert.equal((Array.from(runtime.sandbox[result.counterGlobalName] as Set)).length, 3) }) +test('pure static empty caches preserve native state while module loading remains outside class statements', () => { + const source = `export class Target { + private static cache: number[] = []; + value = 1; + run() { Target.cache.push(this.value); return Target.cache.length; } + }` + const result = instrument(source) + + assert.equal(result.reason, null) + assert.equal(result.statements.some(statement => statement.memberName === 'cache'), false) + assert.deepEqual(new Set(result.statements.map(statement => statement.memberName)), new Set(['value', 'run'])) + const original = load(source, null) + const counted = load(result.source!, result.counterGlobalName) + assert.deepEqual(Array.from(counted.sandbox[result.counterGlobalName] as Set), []) + + for (const expected of [1, 2]) { + assert.equal(new original.Target()['run']!(), expected) + assert.equal(new counted.Target()['run']!(), expected) + } + + const hits = new Set(counted.sandbox[result.counterGlobalName] as Set) + assert.deepEqual(hits, new Set(result.statements.map(statement => statement.id))) +}) + +for (const [name, declaration] of [ + ['effectful initializer', 'static cache = effect();'], + ['spread allocation', 'static cache = [...foreign];'], + ['nonempty allocation', 'static cache = [foreign];'], + ['static block', 'static { effect(); }'], + ['builtin property', 'static name = [];'], + ['accessor collision', 'static set cache(value: unknown) { effect(); } static cache = [];'], +] as const) { + test(`static cache admission retains the ${name} boundary`, () => { + const result = instrument(`export class Target { ${declaration} run() { return 1; } }`) + + assert.equal(result.source, null) + assert.match(result.reason!, /Static/) + }) +} + test('retains explicit unsupported dynamic reachability and closure outcomes', () => { assert.match(instrument('export class Target { run(name: string) { return this[name]; } }').reason!, /Computed receiver/) assert.match(instrument('export class Target { run() { return [1].map(x => x + 1); } }').reason!, /Nested closures/) diff --git a/usvm-ts-fast-check/scripts/test_class_coverage_replay.py b/usvm-ts-fast-check/scripts/test_class_coverage_replay.py index 1707952019..589ddfdbb8 100644 --- a/usvm-ts-fast-check/scripts/test_class_coverage_replay.py +++ b/usvm-ts-fast-check/scripts/test_class_coverage_replay.py @@ -84,6 +84,26 @@ def test_always_true_oracle_cannot_hide_changed_scenario_results(self): self.assertEqual(record["creditedStatementIds"], []) + def test_pure_static_cache_preserves_repeated_native_observations_without_module_coverage(self): + (self.root / "Subject.ts").write_text( + "export class Subject { private static cache: number[] = []; " + "value(x: number): number { Subject.cache.push(x); return Subject.cache.length; } }\n", + encoding="utf-8", + ) + self.case["sourceSha256"] = {name: digest(self.root / name) for name in ("Subject.ts", "Properties.ts")} + prepared = self.native("prepare", self.case) + self.assertTrue(prepared["supported"], prepared) + self.assertIn("module-loading", prepared["excludedExecutionScopes"]) + self.assertEqual({statement["memberName"] for statement in prepared["universe"]["statements"]}, {"value"}) + inputs = [{"inputs": [number(value)], "admission": "ADMITTED", "outcome": "HOLDS"} for value in (4, 7)] + + replay = self.native("replay", dict(self.case, prepared=prepared, inputs=inputs)) + + self.assertTrue(all(record["verified"] for record in replay["records"]), replay) + covered = {item for record in replay["records"] for item in record["creditedStatementIds"]} + self.assertEqual(covered, {statement["id"] for statement in prepared["universe"]["statements"]}) + + def test_diagnostic_module_state_does_not_change_the_oracle_input_trajectory(self): (self.root / "Subject.ts").write_text( "export class Subject { value(x: number): number { if (x === 2) return 2; return 1; } }\n",