[PBT] Exclude pure static empty caches from class statement coverage

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<ts.ClassElement>): 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)

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<string>)).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<string>), [])
+
+  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<string>)
+  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/)

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",