From b0a4d2517f5db007f3611b2404cb960931c8bbd6 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 02:12:48 +0300 Subject: [PATCH 1/8] Add isolated raw class startup smoke probes Prove interpreter entry into frozen original class statements separately from successful transitions. Retain acquisition, frontend, kernel, timeout, and residual-call evidence for every frozen class. --- usvm-ts-calls/CLASS_START_SMOKE.md | 66 +++ .../scripts/run-class-start-smoke.py | 232 ++++++++ .../scripts/test_run_class_start_smoke.py | 97 ++++ .../ts/calls/CallsClassStartAcquisition.kt | 38 ++ .../usvm/ts/calls/CallsClassStartIrCache.kt | 78 +++ .../org/usvm/ts/calls/CallsClassStartSmoke.kt | 508 ++++++++++++++++++ .../org/usvm/ts/calls/CallsExperimentCli.kt | 2 + .../usvm/ts/calls/CallsClassStartSmokeTest.kt | 182 +++++++ 8 files changed, 1203 insertions(+) create mode 100644 usvm-ts-calls/CLASS_START_SMOKE.md create mode 100644 usvm-ts-calls/scripts/run-class-start-smoke.py create mode 100644 usvm-ts-calls/scripts/test_run_class_start_smoke.py create mode 100644 usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartAcquisition.kt create mode 100644 usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt create mode 100644 usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt create mode 100644 usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt diff --git a/usvm-ts-calls/CLASS_START_SMOKE.md b/usvm-ts-calls/CLASS_START_SMOKE.md new file mode 100644 index 0000000000..ccaa6797c3 --- /dev/null +++ b/usvm-ts-calls/CLASS_START_SMOKE.md @@ -0,0 +1,66 @@ +# Raw class startup smoke + +This diagnostic loads the complete frozen target class through the bundled TypeScript frontend, +materializes its IR bodies, and starts a real `TsMachine`. It does not require observation domains, +native replay admission, or serializable class arguments. It makes no native coverage claim. + +Build the installed distribution with `./gradlew :usvm-ts-calls:installDist`. Run the frozen cohort: + +```sh +python3 usvm-ts-calls/scripts/run-class-start-smoke.py \ + --calls usvm-ts-calls/build/install/usvm-ts-calls/bin/usvm-ts-calls \ + --manifest /absolute/path/startup-manifest.json \ + --output /absolute/path/fresh-startup-results +``` + +Each class has an isolated JVM and output directory. The driver retains all manifest classes in +`summary.json`, including pending, acquisition failure, frontend failure, timeout, and kernel failure +rows. The default external child deadline is 60 seconds; `--child-timeout-seconds` controls this +deadline independently of the symbolic budget in the manifest. Timeout kills the entire process +group, including a frontend subprocess. + +## Startup criterion + +`started` requires both a real initial state with a model and an interpreter callback for an original +executable statement of the selected target class. Assignment, unresolved assignment call, standalone +call, conditional, explicit return, and throw callbacks run inside the corresponding interpreter visit, +before expression resolution or unknown-call dispatch. Queue selection alone cannot establish startup. +Synthetic default returns, NOPs, declarations without initializers, foreign classes, and missing source +spans cannot establish it either. A first unsupported residual call can establish startup even when its +successful transition count is zero; this is recorded as `STARTED_WITH_LIMITATION`. + +`originalTargetStatementsEntered` counts source interpreter entries. `targetSuccessfulTransitions` +counts the subset that complete a feasible interpreter transition. The first entry, source location, +initial-state count, and identity are saved durably to `progress.json` before the callback returns. +If a child is killed later, the driver preserves that proven entry and records the process limitation. +`unknown-calls.json` retains ordered model/fallback decisions. Final engine stop reasons, unsupported +paths, source drift, and stage durations are preserved separately. + +`qualifyingStarted` additionally requires `acquisitionComplete` in both the manifest case and its frozen +external acquisition receipt, with all source/config/dependency bytes still matching. Installation +with a `FROZEN` receipt and `acquisitionComplete=false` only supplies diagnostic startup evidence. +The acquisition workflow must establish the complete runtime graph before enabling qualification. + +## Frozen manifest + +Schema version 1 stores `toolRevision`, `nativeFrontendRevision`, `ledgerSha256`, `expectedClassCount` +(default 200), `budgetMillis` (default 2000), `solverLimitMillis` (default 250), `collectedStatesLimit` +(default 10), `seed` (default 17), `profile` (default `FROZEN_STOP`), and `classes`. + +Each case has a safe `classId`, its exact original `identity`, `projectRevision`, absolute `sourceRoot`, +relative `sourceFile`, `className`, and `inputSha256` map. The map must include the complete target source +and every acquired input consumed by the frozen scope. Optional `frontendConfig` freezes the resolved +compiler configuration used in the copied scope. Optional `acquisitionReceipt` is relative to the +manifest directory; `acquisitionSha256` freezes its bytes. Receipt checks bind project revision, source +root, original class identity/source bytes, and the acquired snapshot hashes. A complete case requires +this receipt and its explicit completion evidence. + +The CLI validates the built tool and bundled frontend identities against the manifest. The driver +freezes hashes of its own script, launcher, runtime jars, Java, and Node, plus JVM options and environment. +A resume verifies source and receipt bytes before reusing a final result; changed runtime or manifest +identity requires a new output directory. An interrupted child without a final driver receipt also +requires a fresh attempt directory. + +The shared cache stores immutable frontend IR only, keyed by frozen inputs, resolved compiler config, +frontend revision, and project revision. It verifies every cached file before reuse. Scenes, machines, +initial states, and solver states are always created separately for each class. diff --git a/usvm-ts-calls/scripts/run-class-start-smoke.py b/usvm-ts-calls/scripts/run-class-start-smoke.py new file mode 100644 index 0000000000..5f61db9307 --- /dev/null +++ b/usvm-ts-calls/scripts/run-class-start-smoke.py @@ -0,0 +1,232 @@ +#!/usr/bin/env python3 +"""Isolated raw-class startup probes, retaining every frozen class and failure.""" +import argparse +import hashlib +import json +import os +import re +import signal +import shutil +from pathlib import Path +import subprocess + + +def read(path): + return json.loads(path.read_text(encoding='utf-8')) + + +def sha(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def save(path, value): + path.parent.mkdir(parents=True, exist_ok=True) + temporary = path.with_suffix(path.suffix + '.tmp') + with temporary.open('w', encoding='utf-8') as stream: + json.dump(value, stream, indent=2) + stream.write('\n') + stream.flush() + os.fsync(stream.fileno()) + temporary.replace(path) + + +def freeze(path, value): + if path.exists(): + if read(path) != value: + raise ValueError(f'Frozen startup identity changed: {path}') + else: + save(path, value) + + +def verify_case(case, manifest_directory=None): + root = Path(case['sourceRoot']).resolve(strict=True) + for relative, expected in case['inputSha256'].items(): + name = Path(relative) + if name.is_absolute() or '..' in name.parts: + raise ValueError(f'Unsafe frozen input: {relative}') + actual = (root / name).resolve(strict=True) + if not actual.is_relative_to(root) or sha(actual) != expected: + raise ValueError(f'Frozen startup input changed: {relative}') + receipt_name = case.get('acquisitionReceipt') + if receipt_name is None: + if case.get('acquisitionComplete', False): + raise ValueError('Complete acquisition needs a frozen receipt') + return + if manifest_directory is None: + raise ValueError('Acquisition receipt needs its manifest root') + relative = Path(receipt_name) + if relative.is_absolute() or '..' in relative.parts: + raise ValueError('Unsafe acquisition receipt path') + receipt_path = (manifest_directory / relative).resolve(strict=True) + if not receipt_path.is_relative_to(manifest_directory) or sha(receipt_path) != case.get('acquisitionSha256'): + raise ValueError('Frozen acquisition receipt changed') + receipt = read(receipt_path) + if receipt['projectRevision'] != case['projectRevision'] or Path(receipt['sourceRoot']).resolve() != root: + raise ValueError('Acquisition revision or source root differs') + matching = any(owner['identity'] == case['identity'] and owner['sourceFile'] == case['sourceFile'] + and owner['className'] == case['className'] for owner in receipt['classes']) + if not matching or receipt['originalClassSha256'].get(case['sourceFile']) != case['inputSha256'][case['sourceFile']]: + raise ValueError('Acquisition receipt differs from the frozen original class') + snapshot = receipt['snapshot']['inputSha256'] + if any(snapshot.get(name) != digest for name, digest in case['inputSha256'].items()): + raise ValueError('Startup input is outside its frozen acquired snapshot') + if case.get('acquisitionComplete', False) and not receipt.get('acquisitionComplete', False): + raise ValueError('Installation without graph proof cannot qualify') + + +def runtime_identity(calls): + jars = sorted((calls.parent.parent / 'lib').glob('*.jar')) + if not jars: + raise ValueError('Use the installed Calls distribution with its frozen runtime jars') + files = {'launcher': sha(calls), 'driver': sha(Path(__file__)), + 'jars': {path.name: sha(path) for path in jars}} + java = Path(os.environ['JAVA_HOME']) / 'bin/java' if os.environ.get('JAVA_HOME') else Path(shutil.which('java')) + node = Path(shutil.which('node')) + files.update(java={'path': str(java.resolve(strict=True)), 'sha256': sha(java)}, + node={'path': str(node.resolve(strict=True)), 'sha256': sha(node)}) + files['javaVersion'] = subprocess.check_output([str(java), '-version'], stderr=subprocess.STDOUT, + text=True, timeout=10) + files['JVMEnvironment'] = {name: os.environ.get(name) for name in ('JAVA_OPTS', 'JDK_JAVA_OPTIONS', '_JAVA_OPTIONS')} + return files + + +def validate_result(result, case, fingerprint): + if (result['classId'] != case['classId'] or result['identity'] != case['identity'] + or result['manifestSha256'] != fingerprint): + raise ValueError('Saved startup result identity differs') + started = result['initialStates'] > 0 and result['originalTargetStatementsEntered'] > 0 + if result['started'] != started: + raise ValueError('Startup proof needs a real initial state and original target-class interpreter entry') + if result['targetStatementEntered'] != (result['originalTargetStatementsEntered'] > 0): + raise ValueError('Original target-class entry flag differs from its count') + if result['qualifyingStarted'] and (not started or not case.get('acquisitionComplete', False)): + raise ValueError('Incomplete acquisition cannot establish qualifying startup') + + +def failure_result(case, fingerprint, stage, diagnostic): + return {'classId': case['classId'], 'identity': case['identity'], 'manifestSha256': fingerprint, + 'stage': stage, 'started': False, 'qualifyingStarted': False, 'initialStates': 0, + 'executedSteps': 0, 'targetClassSteps': 0, 'originalTargetClassSteps': 0, + 'syntheticOrUnmappedTargetClassSteps': 0, 'originalTargetStatementsEntered': 0, + 'targetStatementEntered': False, 'targetSuccessfulTransitions': 0, 'startupStatus': 'NOT_STARTED', + 'acquisitionComplete': case.get('acquisitionComplete', False), + 'acquisitionSha256': case.get('acquisitionSha256'), 'stageElapsedMillis': {}, 'diagnostic': diagnostic} + + +def child_result(child, receipt, case, fingerprint): + generated = child / 'result.json' + if generated.exists(): + result = read(generated) + elif (child / 'progress.json').exists(): + result = read(child / 'progress.json') + result.update(stage='SOURCE_ENTRY_CHILD_TIMEOUT' if receipt.get('timedOut') else 'SOURCE_ENTRY_CHILD_EXIT_FAILURE', + timedOut=receipt.get('timedOut', False), engineFailed=not receipt.get('timedOut', False), + startupStatus='STARTED_WITH_LIMITATION', diagnostic=f'Child stopped after durable source entry: {receipt}') + journal = child / 'unknown-calls.json' + if journal.exists(): + result['unknownCalls'] = read(journal) + else: + stage = 'CHILD_TIMEOUT' if receipt.get('timedOut') else 'CHILD_EXIT_FAILURE' + result = failure_result(case, fingerprint, stage, f'Child did not produce result: {receipt}') + validate_result(result, case, fingerprint) + return result + + +def summarize(manifest, output, fingerprint): + rows = [] + for case in manifest['classes']: + path = output / 'classes' / case['classId'] / 'result.json' + if path.exists(): + result = read(path) + validate_result(result, case, fingerprint) + else: + result = failure_result(case, fingerprint, 'PENDING', 'No completed child receipt') + rows.append(result) + qualifying = sum(row['qualifyingStarted'] for row in rows) + summary = {'schemaVersion': 1, 'manifestSha256': fingerprint, + 'expectedClassCount': manifest.get('expectedClassCount', 200), 'classCount': len(rows), + 'startedCount': sum(row['started'] for row in rows), 'qualifyingStartedCount': qualifying, + 'complete': all(row['stage'] != 'PENDING' for row in rows), + 'qualifyingFraction': qualifying / len(rows), 'results': rows, + 'proof': 'Actual initial states plus original target-class interpreter entry; no native coverage claim'} + save(output / 'summary.json', summary) + return summary + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--calls', type=Path, required=True) + parser.add_argument('--manifest', type=Path, required=True) + parser.add_argument('--output', type=Path, required=True) + parser.add_argument('--child-timeout-seconds', type=int, default=60) + args = parser.parse_args() + manifest_path = args.manifest.resolve(strict=True) + manifest = read(manifest_path) + classes = manifest['classes'] + if len(classes) != manifest.get('expectedClassCount', 200) or not classes: + raise ValueError('Frozen startup ledger must retain every class') + if (len({case['classId'] for case in classes}) != len(classes) + or len({case['identity'] for case in classes}) != len(classes)): + raise ValueError('Duplicate startup identity') + if any(re.fullmatch(r'[A-Za-z0-9_-]+', case['classId']) is None for case in classes): + raise ValueError('Unsafe class output identity') + if args.child_timeout_seconds <= 0: + raise ValueError('Child timeout must be positive') + output = args.output.resolve() + output.mkdir(parents=True, exist_ok=True) + calls = args.calls.resolve(strict=True) + fingerprint = sha(manifest_path) + environment = dict(os.environ) + if environment.get('ETS_FRONTEND_SCRIPT') is not None: + raise ValueError('Startup probes require the pinned bundled frontend') + environment['USVM_TS_CALLS_OPTS'] = '-Xms1g -Xmx6g -XX:+UseG1GC' + environment['USVM_TS_STARTUP_IR_CACHE'] = str(output / 'ir-cache') + runtime = runtime_identity(calls) + freeze(output / 'identity.json', {'manifestSha256': fingerprint, 'calls': str(calls), 'runtime': runtime, + 'childTimeoutSeconds': args.child_timeout_seconds, + 'JVMOptions': environment['USVM_TS_CALLS_OPTS']}) + for index, case in enumerate(classes): + directory = output / 'classes' / case['classId'] + result_path = directory / 'result.json' + directory.mkdir(parents=True, exist_ok=True) + try: + verify_case(case, manifest_path.parent) + except (OSError, ValueError) as error: + if result_path.exists(): + raise ValueError(f'Saved startup inputs drifted: {case["classId"]}') from error + save(result_path, failure_result(case, fingerprint, 'ACQUISITION_INPUT_FAILURE', str(error))) + summarize(manifest, output, fingerprint) + continue + if result_path.exists(): + validate_result(read(result_path), case, fingerprint) + continue + child = directory / 'child' + if child.exists(): + raise ValueError(f'Interrupted child needs a fresh attempt directory: {case["classId"]}') + print(f'{index + 1}/{len(classes)} {case["identity"]}', flush=True) + log = directory / 'process.log' + with log.open('w', encoding='utf-8') as stream: + process = subprocess.Popen([str(calls), 'class-start-smoke', str(manifest_path), + case['classId'], str(child)], stdout=stream, + stderr=subprocess.STDOUT, env=environment, start_new_session=True) + try: + code = process.wait(timeout=args.child_timeout_seconds) + receipt = {'exitCode': code, 'log': str(log)} + except subprocess.TimeoutExpired: + os.killpg(process.pid, signal.SIGKILL) + process.wait() + receipt = {'exitCode': None, 'timedOut': True, 'processGroupKilled': True, 'log': str(log)} + save(directory / 'process.json', receipt) + result = child_result(child, receipt, case, fingerprint) + verify_case(case, manifest_path.parent) + save(result_path, result) + summary = summarize(manifest, output, fingerprint) + print(f' started={result["started"]}; qualifying={summary["qualifyingStartedCount"]}/{len(classes)}', flush=True) + summary = summarize(manifest, output, fingerprint) + if runtime_identity(calls) != runtime: + raise ValueError('Runtime changed during the startup run; receipts require a fresh attempt') + print(json.dumps({key: value for key, value in summary.items() if key != 'results'}), flush=True) + + +if __name__ == '__main__': + main() diff --git a/usvm-ts-calls/scripts/test_run_class_start_smoke.py b/usvm-ts-calls/scripts/test_run_class_start_smoke.py new file mode 100644 index 0000000000..23d7961c18 --- /dev/null +++ b/usvm-ts-calls/scripts/test_run_class_start_smoke.py @@ -0,0 +1,97 @@ +import importlib.util +import tempfile +import unittest +from pathlib import Path + +SPEC = importlib.util.spec_from_file_location('smoke', Path(__file__).with_name('run-class-start-smoke.py')) +smoke = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(smoke) + + +class StartupIntegrityTest(unittest.TestCase): + def case(self, directory): + source = directory / 'Target.ts' + source.write_text('export class Target {}') + return {'classId': 'target', 'identity': 'fixture@Target', 'sourceRoot': str(directory), + 'inputSha256': {'Target.ts': smoke.sha(source)}, 'acquisitionComplete': False} + + def test_synthetic_steps_and_incomplete_acquisition_cannot_qualify(self): + case = {'classId': 'target', 'identity': 'fixture@Target', 'acquisitionComplete': False} + result = smoke.failure_result(case, 'frozen', 'STOPPED', 'none') + result.update(initialStates=1, targetClassSteps=2, syntheticOrUnmappedTargetClassSteps=2, started=True) + + with self.assertRaisesRegex(ValueError, 'original target-class interpreter entry'): + smoke.validate_result(result, case, 'frozen') + result.update(originalTargetStatementsEntered=1, targetStatementEntered=True, qualifyingStarted=True) + with self.assertRaisesRegex(ValueError, 'Incomplete acquisition'): + smoke.validate_result(result, case, 'frozen') + + def test_source_drift_is_checked_before_reuse(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + case = self.case(directory) + smoke.verify_case(case) + + (directory / 'Target.ts').write_text('export class Target { value = 1; }') + + with self.assertRaisesRegex(ValueError, 'changed'): + smoke.verify_case(case) + + def test_summary_retains_failed_and_pending_rows(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + cases = [{'classId': 'failed', 'identity': 'one'}, {'classId': 'pending', 'identity': 'two'}] + smoke.save(directory / 'classes/failed/result.json', smoke.failure_result(cases[0], 'frozen', 'FRONTEND', 'unsupported')) + + result = smoke.summarize({'classes': cases, 'expectedClassCount': 2}, directory, 'frozen') + + self.assertEqual(2, result['classCount']) + self.assertEqual(0, result['qualifyingStartedCount']) + self.assertFalse(result['complete']) + self.assertEqual(['FRONTEND', 'PENDING'], [row['stage'] for row in result['results']]) + + def test_changed_manifest_cannot_replace_saved_attempt(self): + with tempfile.TemporaryDirectory() as temporary: + path = Path(temporary) / 'identity.json' + smoke.freeze(path, {'manifestSha256': 'one'}) + + with self.assertRaisesRegex(ValueError, 'changed'): + smoke.freeze(path, {'manifestSha256': 'two'}) + + def test_first_residual_call_can_start_without_successful_transition(self): + case = {'classId': 'target', 'identity': 'fixture@Target', 'acquisitionComplete': False} + result = smoke.failure_result(case, 'frozen', 'STOPPED', 'unsupported') + result.update(initialStates=1, originalTargetStatementsEntered=1, targetStatementEntered=True, + started=True, targetSuccessfulTransitions=0, startupStatus='STARTED_WITH_LIMITATION') + + smoke.validate_result(result, case, 'frozen') + + def test_acquisition_complete_needs_external_frozen_receipt(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + case = self.case(directory) + case['acquisitionComplete'] = True + + with self.assertRaisesRegex(ValueError, 'frozen receipt'): + smoke.verify_case(case, directory) + + def test_durable_entry_survives_child_timeout(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + case = {'classId': 'target', 'identity': 'fixture@Target', 'acquisitionComplete': False} + progress = smoke.failure_result(case, 'frozen', 'SOURCE_CLASS_ENTERED', 'none') + progress.update(initialStates=1, originalTargetStatementsEntered=1, + targetStatementEntered=True, started=True) + smoke.save(directory / 'progress.json', progress) + + result = smoke.child_result(directory, {'timedOut': True}, case, 'frozen') + + self.assertTrue(result['started']) + self.assertFalse(result['qualifyingStarted']) + self.assertTrue(result['timedOut']) + self.assertFalse(result['engineFailed']) + self.assertEqual('STARTED_WITH_LIMITATION', result['startupStatus']) + + +if __name__ == '__main__': + unittest.main() diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartAcquisition.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartAcquisition.kt new file mode 100644 index 0000000000..4a945b39fb --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartAcquisition.kt @@ -0,0 +1,38 @@ +package org.usvm.ts.calls + +import kotlinx.serialization.json.booleanOrNull +import kotlinx.serialization.json.jsonArray +import kotlinx.serialization.json.jsonObject +import kotlinx.serialization.json.jsonPrimitive +import java.nio.file.Files +import java.nio.file.Path + +/** Installation alone never establishes completeness; use the separately frozen acquisition receipt. */ +internal fun CallsClassStartCase.verifyStartupAcquisition(manifestDirectory: Path) { + val receiptName = acquisitionReceipt ?: return + val relative = Path.of(receiptName) + require(!relative.isAbsolute && !relative.startsWith("..")) { "Unsafe acquisition receipt path" } + val directory = manifestDirectory.toRealPath() + val receipt = directory.resolve(relative).toRealPath() + require(receipt.startsWith(directory)) { "Acquisition receipt escapes its manifest root" } + val bytes = Files.readAllBytes(receipt) + require(callsArtifactSha256(bytes) == acquisitionSha256) { "Frozen acquisition receipt changed" } + val value = CallsExperimentJson.json.parseToJsonElement(bytes.toString(Charsets.UTF_8)).jsonObject + require(value["projectRevision"]?.jsonPrimitive?.content == projectRevision) { "Acquisition revision differs" } + val receiptRoot = value.getValue("sourceRoot").jsonPrimitive.content + require(Path.of(receiptRoot).toRealPath() == Path.of(sourceRoot).toRealPath()) { "Acquisition root differs" } + val declared = value.getValue("classes").jsonArray.map { it.jsonObject } + val matchesOriginal = declared.any { owner -> + owner["identity"]?.jsonPrimitive?.content == identity && + owner["sourceFile"]?.jsonPrimitive?.content == sourceFile && + owner["className"]?.jsonPrimitive?.content == className + } + require(matchesOriginal) { "Acquisition receipt does not contain the frozen original class" } + val originalHash = value.getValue("originalClassSha256").jsonObject[sourceFile]?.jsonPrimitive?.content + require(originalHash == inputSha256.getValue(sourceFile)) { "Original target source bytes differ" } + val snapshot = value.getValue("snapshot").jsonObject.getValue("inputSha256").jsonObject + val frozenInputsMatch = inputSha256.all { (name, digest) -> snapshot[name]?.jsonPrimitive?.content == digest } + require(frozenInputsMatch) { "Startup input is outside its frozen acquired snapshot" } + val receiptComplete = value["acquisitionComplete"]?.jsonPrimitive?.booleanOrNull == true + require(!acquisitionComplete || receiptComplete) { "Installation without graph proof cannot qualify" } +} diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt new file mode 100644 index 0000000000..68f665933d --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt @@ -0,0 +1,78 @@ +package org.usvm.ts.calls + +import kotlinx.serialization.Serializable +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.generateEtsIR +import org.usvm.ts.pbt.model.encodeToUtf8SafeString +import java.nio.channels.FileChannel +import java.nio.file.Files +import java.nio.file.Path +import java.nio.file.StandardOpenOption +import kotlin.time.Duration.Companion.seconds + +@Serializable +internal data class CallsClassStartIrCache(val fingerprint: String, val irSha256: Map) + +internal fun startupIrFingerprint(case: CallsClassStartCase): String { + val values = mapOf( + "inputs" to CallsExperimentJson.json.encodeToUtf8SafeString(case.inputSha256.toSortedMap().toMap()), + "frontendConfig" to case.frontendConfig.orEmpty(), + "frontendRevision" to CallsBuildIdentity.nativeFrontendRevision, + "projectRevision" to case.projectRevision, + ) + return callsArtifactSha256(CallsExperimentJson.json.encodeToUtf8SafeString(values).toByteArray()) +} + +internal fun startupIrFiles(root: Path): Map = Files.walk(root).use { paths -> + paths.filter { Files.isRegularFile(it) }.sorted().toList().associate { file -> + root.relativize(file).toString() to callsArtifactSha256(Files.readAllBytes(file)) + } +} + +/** Cache only immutable frontend output, never a machine or symbolic state. */ +internal fun preparedClassStartupIr(case: CallsClassStartCase, scope: Path, output: Path): Path { + val configured = System.getenv("USVM_TS_STARTUP_IR_CACHE") + val root = configured?.let(Path::of) ?: output.resolve("ir-cache") + Files.createDirectories(root) + val fingerprint = startupIrFingerprint(case) + val cache = root.resolve(fingerprint) + val lockPath = root.resolve("$fingerprint.lock") + FileChannel.open(lockPath, StandardOpenOption.CREATE, StandardOpenOption.WRITE).use { channel -> + channel.lock().use { + return prepareLockedStartupIr(cache = cache, scope = scope, output = output, fingerprint = fingerprint) + } + } +} + +private fun prepareLockedStartupIr(cache: Path, scope: Path, output: Path, fingerprint: String): Path { + val identityPath = cache.resolve("identity.json") + val ir = cache.resolve("ir") + if (Files.exists(identityPath)) { + val identity = CallsExperimentJson.json.decodeFromString(Files.readString(identityPath)) + require(identity.fingerprint == fingerprint && startupIrFiles(ir) == identity.irSha256) { + "Frozen frontend cache changed" + } + } else { + if (Files.exists(cache)) cache.toFile().deleteRecursively() + Files.createDirectories(cache) + val generated = generateEtsIR( + keepPartialOutputOnFailure = false, + projectPath = scope, + isProject = true, + loadEntrypoints = false, + timeout = 30.seconds, + provider = EtsIrProvider.TS_FRONTEND, + ) + try { + check(generated.toFile().copyRecursively(ir.toFile(), overwrite = false)) + } finally { + generated.toFile().deleteRecursively() + } + writeCallsArtifactAtomically( + identityPath, + encodeCallsArtifact(CallsClassStartIrCache(fingerprint = fingerprint, irSha256 = startupIrFiles(ir))), + ) + } + Files.copy(identityPath, output.resolve("frontend-identity.json")) + return ir +} diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt new file mode 100644 index 0000000000..2cfbd44c38 --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt @@ -0,0 +1,508 @@ +package org.usvm.ts.calls + +import kotlinx.serialization.Serializable +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsCallExpr +import org.jacodb.ets.model.EtsCallStmt +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsNopStmt +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.utils.loadEtsProjectFromIR +import org.usvm.CoverageZone +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.call.TsUnknownCallEvent +import org.usvm.machine.call.TsUnknownCallModelSelection +import org.usvm.machine.expr.TsSimpleValueResolver +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsState +import org.usvm.machine.state.lastStmt +import org.usvm.statistics.UMachineObserver +import java.nio.file.Files +import java.nio.file.Path +import java.util.IdentityHashMap +import kotlin.time.Duration.Companion.milliseconds +import kotlin.time.TimeSource + +@Serializable +internal data class CallsClassStartCase( + val classId: String, + val identity: String, + val projectRevision: String, + val sourceRoot: String, + val sourceFile: String, + val className: String, + val inputSha256: Map, + val frontendConfig: String? = null, + val acquisitionSha256: String? = null, + val acquisitionReceipt: String? = null, + val acquisitionComplete: Boolean = false, +) { + init { + require(classId.matches(Regex("[A-Za-z0-9_-]+"))) + require(identity.isNotBlank() && className.isNotBlank()) + require(projectRevision.matches(Regex("[0-9a-f]{40}"))) + require(sourceFile in inputSha256) { "The full target source must be frozen" } + inputSha256.forEach { (name, digest) -> + val path = Path.of(name) + require(!path.isAbsolute && path.normalize() == path && !path.startsWith("..")) + require(digest.matches(Regex("[0-9a-f]{64}"))) + } + require(acquisitionSha256 == null || acquisitionSha256.matches(Regex("[0-9a-f]{64}"))) + val hasFrozenReceipt = acquisitionReceipt != null && acquisitionSha256 != null + require(!acquisitionComplete || hasFrozenReceipt) { "Complete acquisition needs a frozen receipt" } + } + + fun verifyInputs(): Path { + val root = Path.of(sourceRoot).toRealPath() + inputSha256.forEach { (name, expected) -> + val file = root.resolve(name).toRealPath() + require(file.startsWith(root)) { "Frozen input escapes its root: $name" } + require(callsArtifactSha256(Files.readAllBytes(file)) == expected) { "Frozen input changed: $name" } + } + return root + } +} + +@Serializable +internal data class CallsClassStartManifest( + val schemaVersion: Int = 1, + val toolRevision: String, + val nativeFrontendRevision: String, + val ledgerSha256: String, + val expectedClassCount: Int = 200, + val budgetMillis: Long = 2_000, + val solverLimitMillis: Long = 250, + val collectedStatesLimit: Int = 10, + val seed: Long = 17, + val profile: CallsExperimentProfile = CallsExperimentProfile.FROZEN_STOP, + val classes: List, +) { + init { + require(schemaVersion == 1 && classes.size == expectedClassCount && expectedClassCount > 0) + require(classes.map { it.classId }.distinct().size == classes.size) + require(classes.map { it.identity }.distinct().size == classes.size) + require(ledgerSha256.matches(Regex("[0-9a-f]{64}"))) + require(budgetMillis > 0 && solverLimitMillis in 1..budgetMillis && collectedStatesLimit > 0) + } +} + +@Serializable +internal data class CallsClassStartResult( + val classId: String, + val identity: String, + val manifestSha256: String, + val stage: String, + val started: Boolean, + val qualifyingStarted: Boolean, + val initialStates: Int, + val executedSteps: Long, + val targetClassSteps: Long, + val originalTargetClassSteps: Long, + val syntheticOrUnmappedTargetClassSteps: Long, + val stageElapsedMillis: Map, + val targetStatementEntered: Boolean = false, + val originalTargetStatementsEntered: Long = 0, + val targetSuccessfulTransitions: Long = 0, + val startupStatus: String = "NOT_STARTED", + val acquisitionComplete: Boolean = false, + val acquisitionSha256: String? = null, + val targetSignature: String? = null, + val methodSignatures: List = emptyList(), + val firstOriginalStep: CallsUnknownCallSite? = null, + val stopReason: String? = null, + val timedOut: Boolean = false, + val unsupportedCall: Boolean = false, + val runtimeLimited: Boolean = false, + val engineFailed: Boolean = false, + val unsupportedPaths: List = emptyList(), + val unknownCalls: List = emptyList(), + val diagnostic: String? = null, +) + +/** A source return must be explicit; a synthetic default constructor return cannot prove startup. */ +internal fun isOriginalClassStartupStep( + stmt: EtsStmt, + target: EtsClassSignature, + sourceFile: String, + sourceText: String, +): Boolean { + if (stmt.location.method.signature.enclosingClass != target || stmt is EtsNopStmt) return false + val origin = stmt.location.origin ?: return false + val normalizedFile = origin.fileName.replace('\\', '/') + val matchesFile = normalizedFile == sourceFile || normalizedFile.endsWith("/$sourceFile") + val validRange = origin.startOffset >= 0 && origin.endOffset > origin.startOffset && + origin.endOffset <= sourceText.length + if (!matchesFile || !validRange) return false + val declarationOnly = origin.nodeKind in setOf( + "ClassDeclaration", "InterfaceDeclaration", "SourceFile", "Constructor", "MethodDeclaration", "Parameter", + ) + if (declarationOnly) return false + if (stmt is EtsReturnStmt && origin.nodeKind != "ReturnStatement") return false + if (origin.nodeKind == "PropertyDeclaration") { + val declaration = sourceText.substring(origin.startOffset, origin.endOffset) + if (!hasStartupFieldInitializer(declaration)) return false + } + return true +} + +/** Recognizes an outer assignment, excluding comments, quoted type literals and function-type arrows. */ +@Suppress("NestedBlockDepth") +internal fun hasStartupFieldInitializer(declaration: String): Boolean { + var quote: Char? = null + var escaped = false + var depth = 0 + var blockComment = false + var lineComment = false + var index = 0 + while (index < declaration.length) { + val char = declaration[index] + val next = declaration.getOrNull(index + 1) + if (blockComment) { + if (char == '*' && next == '/') { + blockComment = false + index++ + } + } else if (lineComment) { + if (char == '\n' || char == '\r') lineComment = false + } else if (quote != null) { + when { + escaped -> escaped = false + char == '\\' -> escaped = true + char == quote -> quote = null + } + } else if (char == '/' && next == '*') { + blockComment = true + index++ + } else if (char == '/' && next == '/') { + lineComment = true + index++ + } else { + when (char) { + '\'', '"', '`' -> { quote = char } + '(', '[', '{' -> { depth++ } + ')', ']', '}' -> { depth-- } + '=' -> { + val previous = declaration.getOrNull(index - 1) + val assignment = depth == 0 && next != '>' && next != '=' && previous !in listOf('=', '!', '<') + if (assignment) return true + } + } + } + index++ + } + return false +} + +internal class ClassStartObserver( + private val target: EtsClassSignature, + private val sourceFile: String, + private val sourceText: String, + private val onFirstOriginalStep: () -> Unit, + private val unknownCallObserver: (TsUnknownCallEvent) -> Unit = {}, +) : UMachineObserver, TsInterpreterObserver { + private val initial = java.util.Collections.newSetFromMap(IdentityHashMap()) + private val seenInitial = java.util.Collections.newSetFromMap(IdentityHashMap()) + private val pending = IdentityHashMap() + private val entered = java.util.Collections.newSetFromMap(IdentityHashMap()) + var executedSteps: Long = 0 + private set + var targetSteps: Long = 0 + private set + var originalSteps: Long = 0 + private set + var originalStepCallbacks: Long = 0 + private set + var originalStatementsEntered: Long = 0 + private set + var firstOriginalStep: CallsUnknownCallSite? = null + private set + val initialStates: Int get() = seenInitial.size + + fun registerInitialState(state: TsState) { initial += state } + + override fun onStatePeeked(state: TsState) { + if (state in initial && state.models.isNotEmpty()) seenInitial += state + entered -= state + pending[state] = state.lastStmt + } + + /** Statement callbacks run inside interpreter visits, before expression resolution or fallback. */ + private fun onStatementEntered(stmt: EtsStmt, scope: TsStepScope) { + val state = scope.calcOnState { this } + val original = + isOriginalClassStartupStep(stmt = stmt, target = target, sourceFile = sourceFile, sourceText = sourceText) + if (!original || state.pathConstraints.isFalse || state in entered) return + entered += state + originalStatementsEntered++ + if (firstOriginalStep == null) { + firstOriginalStep = stmt.toCallsUnknownCallSite() + onFirstOriginalStep() + } + } + + override fun onAssignStatement( + simpleValueResolver: TsSimpleValueResolver, + stmt: EtsAssignStmt, + scope: TsStepScope, + ) { + onStatementEntered(stmt = stmt, scope = scope) + } + + override fun onCallWithUnresolvedArguments( + simpleValueResolver: TsSimpleValueResolver, + expr: EtsCallExpr, + scope: TsStepScope, + ) { + onStatementEntered(stmt = scope.calcOnState { lastStmt }, scope = scope) + } + + override fun onCallStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsCallStmt, scope: TsStepScope) { + onStatementEntered(stmt = stmt, scope = scope) + } + + override fun onIfStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsIfStmt, scope: TsStepScope) { + onStatementEntered(stmt = stmt, scope = scope) + } + + override fun onReturnStatement( + simpleValueResolver: TsSimpleValueResolver, + stmt: EtsReturnStmt, + scope: TsStepScope, + ) { + onStatementEntered(stmt = stmt, scope = scope) + } + + override fun onThrowStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsThrowStmt, scope: TsStepScope) { + onStatementEntered(stmt = stmt, scope = scope) + } + + override fun onUnknownCall(event: TsUnknownCallEvent) { + unknownCallObserver(event) + } + + override fun onState(parent: TsState, forks: Sequence) { + executedSteps++ + val stmt = pending.remove(parent) ?: return + val statementEntered = entered.remove(parent) + if (stmt.location.method.signature.enclosingClass != target) return + targetSteps++ + val parentSucceeded = !parent.pathConstraints.isFalse && parent.unsupportedReason == null + val forkSucceeded = forks.any { !it.pathConstraints.isFalse && it.unsupportedReason == null } + val feasibleTransition = parentSucceeded || forkSucceeded + val original = + isOriginalClassStartupStep(stmt = stmt, target = target, sourceFile = sourceFile, sourceText = sourceText) + if (original) originalStepCallbacks++ + if (!feasibleTransition || !original || !statementEntered) return + originalSteps++ + } +} + +/** Full raw source/IR/machine smoke, independent of observation domains and native coverage admission. */ +@Suppress("LongMethod") +internal fun runClassStartSmoke(args: List) { + require(args.size == CLASS_START_ARGUMENT_COUNT) { + "class-start-smoke requires " + } + val manifestPath = Path.of(args[0]).toRealPath() + val bytes = Files.readAllBytes(manifestPath) + val manifest = CallsExperimentJson.json.decodeFromString(bytes.toString(Charsets.UTF_8)) + require(manifest.toolRevision == CallsBuildIdentity.toolRevision) { "Smoke runtime revision changed" } + require(manifest.nativeFrontendRevision == CallsBuildIdentity.nativeFrontendRevision) { "Smoke frontend changed" } + require(System.getenv("ETS_FRONTEND_SCRIPT") == null) { "Use the pinned bundled frontend" } + val case = manifest.classes.single { it.classId == args[1] } + val output = Path.of(args[2]).toAbsolutePath().normalize() + Files.createDirectories(output) + require(Files.list(output).use { it.findAny().isEmpty }) { "Smoke child output must be fresh" } + val fingerprint = callsArtifactSha256(bytes) + val elapsed = linkedMapOf() + val startedAt = TimeSource.Monotonic.markNow() + var stage = "INPUT_VERIFICATION" + var targetSignature: EtsClassSignature? = null + var methods = emptyList() + var observer: ClassStartObserver? = null + val unknownCalls = mutableListOf() + var outcome: org.usvm.machine.TsMachineAnalysisResult? = null + var lastCheckpointMillis = 0L + fun checkpoint(next: String) { + val now = startedAt.elapsedNow().inWholeMilliseconds + elapsed[stage] = now - lastCheckpointMillis + lastCheckpointMillis = now + stage = next + writeCallsArtifactAtomically( + output.resolve("stage.json"), + encodeCallsArtifact( + mapOf( + "classId" to case.classId, + "identity" to case.identity, + "stage" to stage, + "manifestSha256" to fingerprint, + "elapsedMillis" to startedAt.elapsedNow().inWholeMilliseconds.toString(), + ) + ) + ) + } + val failure = runCatching { + case.verifyStartupAcquisition(manifestDirectory = manifestPath.parent) + val root = case.verifyInputs() + val scope = output.resolve("source") + case.inputSha256.keys.forEach { relative -> + val target = scope.resolve(relative) + Files.createDirectories(target.parent) + Files.copy(root.resolve(relative), target) + } + case.frontendConfig?.let { Files.writeString(scope.resolve("tsconfig.json"), it) } + checkpoint(next = "FRONTEND") + val ir = preparedClassStartupIr(case = case, scope = scope, output = output) + checkpoint(next = "SCENE") + val scene = loadEtsProjectFromIR(projectFilesPath = ir, sdkFilesPath = null) + checkpoint(next = "TARGET") + val targets = scene.projectClasses.filter { owner -> + val file = owner.signature.file.fileName.replace('\\', '/') + owner.name == case.className && (file == case.sourceFile || file.endsWith("/${case.sourceFile}")) + } + require(targets.size == 1) { "Target class is absent or ambiguous: ${targets.size}" } + val target = targets.single() + targetSignature = target.signature + val sourceText = Files.readString(scope.resolve(case.sourceFile)) + methods = target.methods.filter { it.cfg.stmts.isNotEmpty() }.sortedByDescending { method -> + method.cfg.stmts.any { isOriginalClassStartupStep(it, target.signature, case.sourceFile, sourceText) } + } + require(methods.isNotEmpty()) { "Target class has no executable IR bodies" } + checkpoint(next = "MACHINE") + val machineObserver = ClassStartObserver( + target = target.signature, + sourceFile = case.sourceFile, + sourceText = sourceText, + onFirstOriginalStep = { + checkpoint(next = "SOURCE_CLASS_ENTERED") + val current = checkNotNull(observer) + val started = current.initialStates > 0 && current.originalStatementsEntered > 0 + val progress = CallsClassStartResult( + classId = case.classId, + identity = case.identity, + manifestSha256 = fingerprint, + stage = stage, + started = started, + qualifyingStarted = started && case.acquisitionComplete, + initialStates = current.initialStates, + executedSteps = current.executedSteps, + targetClassSteps = current.targetSteps, + originalTargetClassSteps = current.originalSteps, + syntheticOrUnmappedTargetClassSteps = current.targetSteps - current.originalStepCallbacks, + targetStatementEntered = current.originalStatementsEntered > 0, + originalTargetStatementsEntered = current.originalStatementsEntered, + targetSuccessfulTransitions = current.originalSteps, + startupStatus = "STARTED", + acquisitionComplete = case.acquisitionComplete, + acquisitionSha256 = case.acquisitionSha256, + stageElapsedMillis = elapsed, + targetSignature = target.signature.toString(), + methodSignatures = methods.map { it.signature.toString() }, + firstOriginalStep = current.firstOriginalStep, + ) + writeCallsArtifactAtomically(output.resolve("progress.json"), encodeCallsArtifact(progress)) + }, + unknownCallObserver = { event -> + unknownCalls += event.toCallsClassUnknownCallEvent(eventIndex = unknownCalls.size + 1) + writeCallsArtifactAtomically(output.resolve("unknown-calls.json"), encodeCallsArtifact(unknownCalls)) + }, + ) + observer = machineObserver + TsMachine( + scene = scene, + options = UMachineOptions( + stateCollectionStrategy = StateCollectionStrategy.ALL, + randomSeed = manifest.seed, + collectedStatesLimit = manifest.collectedStatesLimit, + timeout = manifest.budgetMillis.milliseconds, + solverTimeout = manifest.solverLimitMillis.milliseconds, + solverType = SolverType.YICES, + coverageZone = CoverageZone.CLASS, + stopOnCoverage = 0, + removeCoveredEntryPoints = false, + throwExceptionOnStepFailure = true, + ), + tsOptions = TsOptions( + unknownCallModelSelection = if (manifest.profile.usesFrozenModels) { + TsUnknownCallModelSelection.All + } else { + TsUnknownCallModelSelection.Only(emptySet()) + }, + unknownCallFallback = manifest.profile.fallback, + eraseTypeAssertions = true, + classCoverageTargets = setOf(target.signature), + ), + machineObserver = machineObserver, + observer = machineObserver, + ).use { machine -> + checkpoint(next = "INITIAL_STATE") + outcome = machine.analyzeWithMetadata( + methods = methods, + configureInitialState = { _, state -> + machineObserver.registerInitialState(state) + } + ) + } + case.verifyInputs() + checkpoint(next = "STOPPED") + }.exceptionOrNull() + val metrics = observer + val drift = runCatching { + case.verifyStartupAcquisition(manifestDirectory = manifestPath.parent) + case.verifyInputs() + }.exceptionOrNull() + val entered = (metrics?.originalStatementsEntered ?: 0) > 0 + val started = (metrics?.initialStates ?: 0) > 0 && entered + val engineFailed = outcome?.engineFailed == true || (failure != null && observer != null) + val limited = outcome?.unsupportedCall == true || outcome?.runtimeLimited == true || engineFailed + val result = CallsClassStartResult( + classId = case.classId, + identity = case.identity, + manifestSha256 = fingerprint, + stage = stage, + started = started, + qualifyingStarted = started && case.acquisitionComplete && drift == null, + initialStates = metrics?.initialStates ?: 0, + executedSteps = metrics?.executedSteps ?: 0, + targetClassSteps = metrics?.targetSteps ?: 0, + originalTargetClassSteps = metrics?.originalSteps ?: 0, + syntheticOrUnmappedTargetClassSteps = (metrics?.targetSteps ?: 0) - (metrics?.originalStepCallbacks ?: 0), + targetStatementEntered = entered, + originalTargetStatementsEntered = metrics?.originalStatementsEntered ?: 0, + targetSuccessfulTransitions = metrics?.originalSteps ?: 0, + acquisitionComplete = case.acquisitionComplete, + acquisitionSha256 = case.acquisitionSha256, + startupStatus = when { + started && limited -> "STARTED_WITH_LIMITATION" + started -> "STARTED" + else -> "NOT_STARTED" + }, + stageElapsedMillis = elapsed, + targetSignature = targetSignature?.toString(), + methodSignatures = methods.map { it.signature.toString() }, + firstOriginalStep = metrics?.firstOriginalStep, + stopReason = outcome?.stopReason?.name, + timedOut = outcome?.timedOut == true, + unsupportedCall = outcome?.unsupportedCall == true, + runtimeLimited = outcome?.runtimeLimited == true, + engineFailed = engineFailed, + unsupportedPaths = outcome?.unsupportedPaths.orEmpty(), + unknownCalls = unknownCalls, + diagnostic = listOfNotNull(failure, drift).distinct().takeIf { it.isNotEmpty() }?.joinToString { + "${it::class.java.name}: ${it.message}" + }, + ) + writeCallsArtifactAtomically(output.resolve("result.json"), encodeCallsArtifact(result)) + System.out.appendLine(encodeCallsArtifact(result)) +} + +private const val CLASS_START_ARGUMENT_COUNT = 3 diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperimentCli.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperimentCli.kt index d646403e69..2e20f7ef3a 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperimentCli.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperimentCli.kt @@ -10,6 +10,7 @@ fun main(args: Array) { when (args.first()) { "class-catalog" -> runClassCatalog(args.drop(1)) + "class-start-smoke" -> runClassStartSmoke(args.drop(1)) "class-prepare" -> runClassPrepare(args.drop(1)) "class-preflight" -> runClassPreflight(args.drop(1)) "class-cell" -> runClassCell(args.drop(1)) @@ -104,6 +105,7 @@ internal fun frontendIdentity(args: List): String { private fun usage(): String = """ Usage: calls class-catalog + calls class-start-smoke calls class-prepare calls class-preflight calls class-cell diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt new file mode 100644 index 0000000000..c561d0ad3a --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt @@ -0,0 +1,182 @@ +package org.usvm.ts.calls + +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsMethodImpl +import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsNopStmt +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsSourceSpan +import org.jacodb.ets.model.EtsStmtLocation +import org.jacodb.ets.model.EtsUndefinedType +import org.junit.jupiter.api.io.TempDir +import java.nio.file.Files +import java.nio.file.Path +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class CallsClassStartSmokeTest { + @TempDir + lateinit var directory: Path + + @Test + fun `synthetic default return and foreign class do not prove original target execution`() { + val target = EtsClassSignature( + name = "Target", + file = EtsFileSignature(projectName = "fixture", fileName = "Target.ts") + ) + val method = EtsMethodImpl( + EtsMethodSignature( + enclosingClass = target, + name = "constructor", + parameters = emptyList(), + returnType = EtsUndefinedType, + ) + ) + val location = EtsStmtLocation(method = method, index = 0) + val synthetic = EtsReturnStmt(location = location, returnValue = null) + val source = "return;" + + assertFalse(isOriginalClassStartupStep(synthetic, target, sourceFile = "Target.ts", sourceText = source)) + location.origin = EtsSourceSpan( + fileName = "Target.ts", startOffset = 0, endOffset = source.length, + startLine = 0, startColumn = 0, endLine = 0, endColumn = source.length, nodeKind = "Constructor", + ) + assertFalse(isOriginalClassStartupStep(synthetic, target, sourceFile = "Target.ts", sourceText = source)) + location.origin = location.origin?.copy(nodeKind = "ReturnStatement") + assertTrue(isOriginalClassStartupStep(synthetic, target, sourceFile = "Target.ts", sourceText = source)) + assertFalse( + isOriginalClassStartupStep( + synthetic, + target.copy(name = "Foreign"), + sourceFile = "Target.ts", + sourceText = source + ) + ) + assertFalse( + isOriginalClassStartupStep(EtsNopStmt(location), target, sourceFile = "Target.ts", sourceText = source) + ) + } + + @Test + fun `uninitialized property and function type arrow are not source initializer assignments`() { + assertFalse(hasStartupFieldInitializer("handler: (value: number) => number;")) + assertFalse(hasStartupFieldInitializer("value: '=';")) + assertFalse(hasStartupFieldInitializer("values: { '=': number };")) + assertFalse(hasStartupFieldInitializer("value /* = */: number;")) + assertFalse(hasStartupFieldInitializer("value: number; // = 1")) + assertFalse(hasStartupFieldInitializer("value /*=> */: (x: number) => number;")) + assertTrue(hasStartupFieldInitializer("handler = (value: number) => value + 1;")) + assertTrue(hasStartupFieldInitializer("value: number = 1;")) + assertTrue(hasStartupFieldInitializer("values: Map=new Map();")) + } + + @Test + fun `input drift and unknown acquisition cannot establish complete provenance`() { + val source = directory.resolve("Target.ts") + Files.writeString(source, "export class Target { value = 1; }") + val case = CallsClassStartCase( + classId = "target", + identity = "fixture@Target", + projectRevision = "a".repeat(40), + sourceRoot = directory.toString(), + sourceFile = "Target.ts", + className = "Target", + inputSha256 = mapOf("Target.ts" to callsArtifactSha256(Files.readAllBytes(source))), + ) + + assertEquals(directory.toRealPath(), case.verifyInputs()) + assertFalse(case.acquisitionComplete) + assertFailsWith { case.copy(acquisitionComplete = true) } + + Files.writeString(source, "export class Target { value = 2; }") + + assertFailsWith { case.verifyInputs() } + } + + @Test + fun `raw full class runs with original source steps without observation domain admission`() { + val result = runFixture( + sourceText = "export class Target { value = 1; read(): number { return this.value; } }", + ) + + assertTrue(result.started, result.toString()) + assertTrue(result.initialStates > 0) + assertTrue(result.originalTargetStatementsEntered > 0) + assertTrue(result.originalTargetClassSteps > 0) + assertFalse(result.qualifyingStarted) + assertTrue(result.methodSignatures.any { it.contains("read") }) + } + + @Test + fun `first unsupported value proves source interpreter entry without a successful transition`() { + val result = runFixture( + sourceText = "declare function externalOperation(): number; " + + "export class Target { constructor() { externalOperation(); } }", + profile = CallsExperimentProfile.EMPTY_STOP, + ) + + assertTrue(result.started, result.toString()) + assertTrue(result.targetStatementEntered) + assertTrue(result.originalTargetStatementsEntered > 0) + assertEquals(0L, result.targetSuccessfulTransitions) + assertEquals("STARTED_WITH_LIMITATION", result.startupStatus) + assertTrue(result.runtimeLimited) + assertFalse(result.qualifyingStarted) + } + + @Test + fun `first residual dispatcher call proves source interpreter entry`() { + val result = runFixture( + sourceText = "export class Target { constructor() { Date.now(); } }", + profile = CallsExperimentProfile.EMPTY_STOP, + ) + + assertTrue(result.started, result.toString()) + assertTrue(result.targetStatementEntered) + assertTrue(result.originalTargetStatementsEntered > 0) + assertTrue(result.unknownCalls.isNotEmpty(), result.toString()) + assertEquals("STARTED_WITH_LIMITATION", result.startupStatus) + assertTrue(result.unsupportedCall) + } + + private fun runFixture( + sourceText: String, + profile: CallsExperimentProfile = CallsExperimentProfile.FROZEN_STOP, + ): CallsClassStartResult { + val source = directory.resolve("Target.ts") + Files.writeString(source, sourceText) + val config = directory.resolve("tsconfig.json") + Files.writeString(config, """{"compilerOptions":{"target":"ES2022","types":[]},"files":["Target.ts"]}""") + val inputs = listOf(source, config).associate { + it.fileName.toString() to callsArtifactSha256(Files.readAllBytes(it)) + } + val case = CallsClassStartCase( + classId = "target", + identity = "fixture@Target", + projectRevision = "a".repeat(40), + sourceRoot = directory.toString(), + sourceFile = "Target.ts", + className = "Target", + inputSha256 = inputs, + ) + val manifest = CallsClassStartManifest( + toolRevision = CallsBuildIdentity.toolRevision, + nativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision, + ledgerSha256 = "b".repeat(64), + expectedClassCount = 1, + profile = profile, + classes = listOf(case), + ) + val path = directory.resolve("manifest.json") + Files.writeString(path, encodeCallsArtifact(manifest)) + val output = directory.resolve("output") + + runClassStartSmoke(listOf(path.toString(), "target", output.toString())) + + return CallsExperimentJson.json.decodeFromString(Files.readString(output.resolve("result.json"))) + } +} From 687adbbf2d489d7bd79afa84ad3953df0bb73c54 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 02:15:37 +0300 Subject: [PATCH 2/8] Retain startup failure stacks and generated state counts --- .../org/usvm/ts/calls/CallsClassStartSmoke.kt | 30 +++++++++++++++++-- 1 file changed, 27 insertions(+), 3 deletions(-) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt index 2cfbd44c38..9cee81222d 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt @@ -115,6 +115,8 @@ internal data class CallsClassStartResult( val startupStatus: String = "NOT_STARTED", val acquisitionComplete: Boolean = false, val acquisitionSha256: String? = null, + val generatedInitialStates: Int = 0, + val generatedInitialMethodCount: Int = 0, val targetSignature: String? = null, val methodSignatures: List = emptyList(), val firstOriginalStep: CallsUnknownCallSite? = null, @@ -126,6 +128,8 @@ internal data class CallsClassStartResult( val unsupportedPaths: List = emptyList(), val unknownCalls: List = emptyList(), val diagnostic: String? = null, + val failureLog: String? = null, + val inputDriftLog: String? = null, ) /** A source return must be explicit; a synthetic default constructor return cannot prove startup. */ @@ -213,6 +217,7 @@ internal class ClassStartObserver( private val seenInitial = java.util.Collections.newSetFromMap(IdentityHashMap()) private val pending = IdentityHashMap() private val entered = java.util.Collections.newSetFromMap(IdentityHashMap()) + private val initialMethods = mutableSetOf() var executedSteps: Long = 0 private set var targetSteps: Long = 0 @@ -226,8 +231,13 @@ internal class ClassStartObserver( var firstOriginalStep: CallsUnknownCallSite? = null private set val initialStates: Int get() = seenInitial.size + val generatedInitialStates: Int get() = initial.size + val generatedInitialMethodCount: Int get() = initialMethods.size - fun registerInitialState(state: TsState) { initial += state } + fun registerInitialState(method: EtsMethod, state: TsState) { + initial += state + initialMethods += method.signature.toString() + } override fun onStatePeeked(state: TsState) { if (state in initial && state.models.isNotEmpty()) seenInitial += state @@ -404,6 +414,8 @@ internal fun runClassStartSmoke(args: List) { startupStatus = "STARTED", acquisitionComplete = case.acquisitionComplete, acquisitionSha256 = case.acquisitionSha256, + generatedInitialStates = current.generatedInitialStates, + generatedInitialMethodCount = current.generatedInitialMethodCount, stageElapsedMillis = elapsed, targetSignature = target.signature.toString(), methodSignatures = methods.map { it.signature.toString() }, @@ -447,8 +459,8 @@ internal fun runClassStartSmoke(args: List) { checkpoint(next = "INITIAL_STATE") outcome = machine.analyzeWithMetadata( methods = methods, - configureInitialState = { _, state -> - machineObserver.registerInitialState(state) + configureInitialState = { method, state -> + machineObserver.registerInitialState(method = method, state = state) } ) } @@ -464,6 +476,14 @@ internal fun runClassStartSmoke(args: List) { val started = (metrics?.initialStates ?: 0) > 0 && entered val engineFailed = outcome?.engineFailed == true || (failure != null && observer != null) val limited = outcome?.unsupportedCall == true || outcome?.runtimeLimited == true || engineFailed + val failureLog = failure?.let { + Files.writeString(output.resolve("failure.log"), it.stackTraceToString()) + "failure.log" + } + val inputDriftLog = drift?.let { + Files.writeString(output.resolve("input-drift.log"), it.stackTraceToString()) + "input-drift.log" + } val result = CallsClassStartResult( classId = case.classId, identity = case.identity, @@ -481,6 +501,8 @@ internal fun runClassStartSmoke(args: List) { targetSuccessfulTransitions = metrics?.originalSteps ?: 0, acquisitionComplete = case.acquisitionComplete, acquisitionSha256 = case.acquisitionSha256, + generatedInitialStates = metrics?.generatedInitialStates ?: 0, + generatedInitialMethodCount = metrics?.generatedInitialMethodCount ?: 0, startupStatus = when { started && limited -> "STARTED_WITH_LIMITATION" started -> "STARTED" @@ -500,6 +522,8 @@ internal fun runClassStartSmoke(args: List) { diagnostic = listOfNotNull(failure, drift).distinct().takeIf { it.isNotEmpty() }?.joinToString { "${it::class.java.name}: ${it.message}" }, + failureLog = failureLog, + inputDriftLog = inputDriftLog, ) writeCallsArtifactAtomically(output.resolve("result.json"), encodeCallsArtifact(result)) System.out.appendLine(encodeCallsArtifact(result)) From 3f11884ce74faf1f02d9fdb4b63d55c4f65fadd9 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 02:32:15 +0300 Subject: [PATCH 3/8] Add frozen four-profile 30-second symbolic class probes Gate the unchanged 200-class cohort on 180 qualifying startup receipts. Retain terminal states, stopped prefixes, queued states, immutable source-mapped IR points, solver metrics, and budget overruns without claiming native coverage. --- usvm-ts-calls/CLASS_START_SMOKE.md | 37 +++ .../scripts/run-class-start-smoke.py | 11 +- .../scripts/run-class-symbolic-probe.py | 150 ++++++++++ .../scripts/test_run_class_symbolic_probe.py | 75 +++++ .../usvm/ts/calls/CallsClassRawAnalysis.kt | 275 ++++++++++++++++++ .../org/usvm/ts/calls/CallsClassStartSmoke.kt | 143 ++++++++- .../org/usvm/ts/calls/CallsExperimentCli.kt | 2 + .../usvm/ts/calls/CallsClassStartSmokeTest.kt | 33 ++- 8 files changed, 708 insertions(+), 18 deletions(-) create mode 100644 usvm-ts-calls/scripts/run-class-symbolic-probe.py create mode 100644 usvm-ts-calls/scripts/test_run_class_symbolic_probe.py create mode 100644 usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt diff --git a/usvm-ts-calls/CLASS_START_SMOKE.md b/usvm-ts-calls/CLASS_START_SMOKE.md index ccaa6797c3..8462bd06df 100644 --- a/usvm-ts-calls/CLASS_START_SMOKE.md +++ b/usvm-ts-calls/CLASS_START_SMOKE.md @@ -64,3 +64,40 @@ requires a fresh attempt directory. The shared cache stores immutable frontend IR only, keyed by frozen inputs, resolved compiler config, frontend revision, and project revision. It verifies every cached file before reuse. Scenes, machines, initial states, and solver states are always created separately for each class. + +## Exploratory four-profile probe + +After a completed startup screen proves at least 180 qualifying starts from the exact original 200 +classes, run the exploratory diagnostic with: + +```sh +python3 usvm-ts-calls/scripts/run-class-symbolic-probe.py \ + --calls usvm-ts-calls/build/install/usvm-ts-calls/bin/usvm-ts-calls \ + --startup-manifest /absolute/path/startup-manifest.json \ + --startup-summary /absolute/path/startup-results/summary.json \ + --output /absolute/path/fresh-symbolic-probe +``` + +This reuses the isolated startup driver and raw loading path through `class-symbolic-probe`. It freezes +all 200 original identities and their ordering in each of `EMPTY_STOP`, `EMPTY_FRESH`, `FROZEN_STOP`, and +`FROZEN_FRESH`, for 800 recorded cells. Every class has a 30-second engine search budget, seed 17, a +250ms solver-check limit, 25ms entry-point quanta, CLASS coverage scope, and no terminal-state cap. +The driver copies and verifies frozen acquisition receipts; it does not run dependency installation. +An unsupported or failed class remains in the same denominator. The current build's complete model +catalog and runtime bytes are frozen before any profile runs. + +Unlike diagnostic startup, interpreter step failures are retained through the machine's failure +metadata while other paths continue. Returned, exceptional, unsupported terminal, stopped-prefix, +and remaining queued states are counted separately. Diagnostic snapshots retain method provenance, +statement text, symbolic result, and path constraints in `states.jsonl`; snapshot failures remain +explicit. Remaining states are drained after the machine has computed its actual stop reason. +Unknown-call events are appended to `unknown-calls.jsonl`. These diagnostic snapshots are not concrete +native witnesses or resumable machine states. + +The raw report freezes the original target's source-mapped IR point universe before search and records +actual interpreter entries in that universe. The driver rejects any changed universe between the four +profiles. This diagnostic is distinct from executable original-source/native replay coverage; the +summary reports native class coverage as unavailable. Setup, actual analysis elapsed time, budget +overruns, solver checks/statuses, entry-point quantum overruns, and engine/unsupported outcomes remain +visible. Missing raw metrics are unavailable rather than fabricated zeroes. The external child deadline +defaults to 120 seconds and does not create a 120-second measurement budget. diff --git a/usvm-ts-calls/scripts/run-class-start-smoke.py b/usvm-ts-calls/scripts/run-class-start-smoke.py index 5f61db9307..ad91f18176 100644 --- a/usvm-ts-calls/scripts/run-class-start-smoke.py +++ b/usvm-ts-calls/scripts/run-class-start-smoke.py @@ -125,6 +125,10 @@ def child_result(child, receipt, case, fingerprint): journal = child / 'unknown-calls.json' if journal.exists(): result['unknownCalls'] = read(journal) + elif (child / 'unknown-calls.jsonl').exists(): + result['unknownCalls'] = [json.loads(line) for line in (child / 'unknown-calls.jsonl').read_text().splitlines()] + if (child / 'states.jsonl').exists(): + result['durableStateSnapshotsPath'] = str(child / 'states.jsonl') else: stage = 'CHILD_TIMEOUT' if receipt.get('timedOut') else 'CHILD_EXIT_FAILURE' result = failure_result(case, fingerprint, stage, f'Child did not produce result: {receipt}') @@ -159,6 +163,8 @@ def main(): parser.add_argument('--manifest', type=Path, required=True) parser.add_argument('--output', type=Path, required=True) parser.add_argument('--child-timeout-seconds', type=int, default=60) + parser.add_argument('--command', choices=('class-start-smoke', 'class-symbolic-probe'), default='class-start-smoke') + parser.add_argument('--ir-cache', type=Path) args = parser.parse_args() manifest_path = args.manifest.resolve(strict=True) manifest = read(manifest_path) @@ -180,10 +186,11 @@ def main(): if environment.get('ETS_FRONTEND_SCRIPT') is not None: raise ValueError('Startup probes require the pinned bundled frontend') environment['USVM_TS_CALLS_OPTS'] = '-Xms1g -Xmx6g -XX:+UseG1GC' - environment['USVM_TS_STARTUP_IR_CACHE'] = str(output / 'ir-cache') + environment['USVM_TS_STARTUP_IR_CACHE'] = str((args.ir_cache or output / 'ir-cache').resolve()) runtime = runtime_identity(calls) freeze(output / 'identity.json', {'manifestSha256': fingerprint, 'calls': str(calls), 'runtime': runtime, 'childTimeoutSeconds': args.child_timeout_seconds, + 'command': args.command, 'irCache': environment['USVM_TS_STARTUP_IR_CACHE'], 'JVMOptions': environment['USVM_TS_CALLS_OPTS']}) for index, case in enumerate(classes): directory = output / 'classes' / case['classId'] @@ -206,7 +213,7 @@ def main(): print(f'{index + 1}/{len(classes)} {case["identity"]}', flush=True) log = directory / 'process.log' with log.open('w', encoding='utf-8') as stream: - process = subprocess.Popen([str(calls), 'class-start-smoke', str(manifest_path), + process = subprocess.Popen([str(calls), args.command, str(manifest_path), case['classId'], str(child)], stdout=stream, stderr=subprocess.STDOUT, env=environment, start_new_session=True) try: diff --git a/usvm-ts-calls/scripts/run-class-symbolic-probe.py b/usvm-ts-calls/scripts/run-class-symbolic-probe.py new file mode 100644 index 0000000000..cf9edf0f9d --- /dev/null +++ b/usvm-ts-calls/scripts/run-class-symbolic-probe.py @@ -0,0 +1,150 @@ +#!/usr/bin/env python3 +"""Frozen 30s, seed17, four-profile raw symbolic diagnostic after the 180/200 startup gate.""" +import argparse +import copy +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys + +SMOKE_SCRIPT = Path(__file__).with_name('run-class-start-smoke.py') +SPEC = importlib.util.spec_from_file_location('startup', SMOKE_SCRIPT) +startup = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(startup) +PROFILES = ('EMPTY_STOP', 'EMPTY_FRESH', 'FROZEN_STOP', 'FROZEN_FRESH') +EXPECTED_CLASSES = 200 +MINIMUM_STARTS = 180 +BUDGET_MILLIS = 30_000 +SEED = 17 + + +def verify_startup_gate(manifest, results, fingerprint): + if len(manifest['classes']) != EXPECTED_CLASSES or manifest.get('expectedClassCount', EXPECTED_CLASSES) != EXPECTED_CLASSES: + raise ValueError('The exploratory denominator must remain the frozen original 200 classes') + if results['manifestSha256'] != fingerprint or not results['complete']: + raise ValueError('Startup gate requires completed results for this exact frozen manifest') + rows = results['results'] + if [row['identity'] for row in rows] != [case['identity'] for case in manifest['classes']]: + raise ValueError('Startup result identities or original ordering differ') + for case, row in zip(manifest['classes'], rows): + startup.validate_result(row, case, fingerprint) + qualifying = sum(row['qualifyingStarted'] for row in rows) + if qualifying != results['qualifyingStartedCount'] or qualifying < MINIMUM_STARTS: + raise ValueError(f'Real startup gate requires {MINIMUM_STARTS}/200; got {qualifying}/200') + return qualifying + + +def profile_manifest(source, profile, catalog, original_directory, output): + result = copy.deepcopy(source) + result.update(toolRevision=catalog['toolRevision'], nativeFrontendRevision=catalog['nativeFrontendRevision'], + budgetMillis=BUDGET_MILLIS, solverLimitMillis=250, timeQuantumMillis=25, + collectedStatesLimit=None, profile=profile, seed=SEED) + for case in result['classes']: + receipt = case.get('acquisitionReceipt') + if receipt is None: + continue + original = (original_directory / receipt).resolve(strict=True) + if startup.sha(original) != case['acquisitionSha256']: + raise ValueError('Frozen acquisition receipt changed before the measurement') + destination = output / 'receipts' / f'{case["acquisitionSha256"]}.json' + destination.parent.mkdir(parents=True, exist_ok=True) + if not destination.exists(): + shutil.copyfile(original, destination) + if startup.sha(destination) != case['acquisitionSha256']: + raise ValueError('Copied acquisition receipt changed') + case['acquisitionReceipt'] = destination.relative_to(output).as_posix() + return result + + +def summarize(output, manifests): + rows = [] + for case in next(iter(manifests.values()))['classes']: + universe_hashes = set() + for profile, manifest in manifests.items(): + path = output / profile / 'classes' / case['classId'] / 'result.json' + fingerprint = startup.sha(output / f'{profile}.json') + result = startup.read(path) if path.exists() else startup.failure_result(case, fingerprint, 'PENDING', 'No child receipt') + startup.validate_result(result, case, fingerprint) + raw = result.get('rawAnalysis') + if raw is not None: + universe_hashes.add(raw['statementUniverseSha256']) + rows.append({'classId': case['classId'], 'identity': case['identity'], 'profile': profile, + 'seed': SEED, 'budgetMillis': BUDGET_MILLIS, 'started': result['started'], + 'startupStatus': result['startupStatus'], 'stage': result['stage'], + 'stopReason': result.get('stopReason'), 'timedOut': result.get('timedOut', False), + 'unsupportedCall': result.get('unsupportedCall', False), + 'engineFailed': result.get('engineFailed', False), 'runtimeLimited': result.get('runtimeLimited', False), + 'rawAnalysisAvailable': raw is not None, + 'returnedStates': raw['returnedStates'] if raw is not None else None, + 'exceptionalStates': raw['exceptionalStates'] if raw is not None else None, + 'stoppedPrefixStates': raw['stoppedPrefixStates'] if raw is not None else None, + 'remainingStates': raw['remainingStates'] if raw is not None else None, + 'stateSnapshotFailures': len(raw['stateSnapshotFailures']) if raw is not None else None, + 'analysisElapsedMillis': raw['analysisElapsedMillis'] if raw is not None else None, + 'budgetOverrunMillis': raw['budgetOverrunMillis'] if raw is not None else None, + 'sourceMappedIrUniverseSize': len(raw['sourceMappedIrUniverse']) if raw is not None else None, + 'sourceMappedIrEnteredSize': len(raw['sourceMappedIrEntered']) if raw is not None else None, + 'sourceMappedIrUniverseSha256': raw['statementUniverseSha256'] if raw is not None else None, + 'nativeClassCoverage': None, 'receipt': str(path), + 'durableStateSnapshotsPath': result.get('durableStateSnapshotsPath'), + 'diagnostic': result.get('diagnostic')}) + if len(universe_hashes) > 1: + raise ValueError(f'Source-mapped IR universe changed between profiles: {case["identity"]}') + summary = {'schemaVersion': 1, 'expectedClassCount': EXPECTED_CLASSES, 'expectedCellCount': EXPECTED_CLASSES * len(PROFILES), + 'budgetMillis': BUDGET_MILLIS, 'seed': SEED, 'profiles': list(PROFILES), 'results': rows, + 'complete': all(row['stage'] != 'PENDING' for row in rows), + 'rawAnalysisAvailableCells': sum(row['rawAnalysisAvailable'] for row in rows), + 'proof': 'Exploratory symbolic source-mapped IR and retained state diagnostics; native coverage is unavailable'} + startup.save(output / 'summary.json', summary) + return summary + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--calls', type=Path, required=True) + parser.add_argument('--startup-manifest', type=Path, required=True) + parser.add_argument('--startup-summary', type=Path, required=True) + parser.add_argument('--output', type=Path, required=True) + parser.add_argument('--child-timeout-seconds', type=int, default=120) + args = parser.parse_args() + manifest_path = args.startup_manifest.resolve(strict=True) + source = startup.read(manifest_path) + startup_results = startup.read(args.startup_summary) + qualifying = verify_startup_gate(source, startup_results, startup.sha(manifest_path)) + for case, result in zip(source['classes'], startup_results['results']): + if result['qualifyingStarted']: + startup.verify_case(case, manifest_path.parent) + output = args.output.resolve() + output.mkdir(parents=True, exist_ok=True) + calls = args.calls.resolve(strict=True) + catalog = json.loads(subprocess.check_output([str(calls), 'class-catalog'], text=True, timeout=60)) + runtime = startup.runtime_identity(calls) + identity = {'startupManifestSha256': startup.sha(manifest_path), 'startupSummarySha256': startup.sha(args.startup_summary), + 'qualifyingStarted': qualifying, 'runtime': runtime, 'driverSha256': startup.sha(Path(__file__)), + 'catalog': catalog, 'profiles': list(PROFILES), 'budgetMillis': BUDGET_MILLIS, 'seed': SEED, + 'collectedStatesLimit': None, 'timeQuantumMillis': 25, 'solverLimitMillis': 250, + 'childTimeoutSeconds': args.child_timeout_seconds} + startup.freeze(output / 'identity.json', identity) + manifests = {} + for profile in PROFILES: + manifest = profile_manifest(source, profile, catalog, manifest_path.parent, output) + startup.freeze(output / f'{profile}.json', manifest) + manifests[profile] = manifest + summarize(output, manifests) + for profile in PROFILES: + print(f'{profile}: frozen 200 classes, 30s, seed17, no terminal-state cap', flush=True) + subprocess.run([sys.executable, str(SMOKE_SCRIPT), '--calls', str(calls), '--command', 'class-symbolic-probe', + '--manifest', str(output / f'{profile}.json'), '--output', str(output / profile), + '--ir-cache', str(output / 'ir-cache'), '--child-timeout-seconds', str(args.child_timeout_seconds)], + check=True) + summarize(output, manifests) + if startup.runtime_identity(calls) != runtime: + raise ValueError('Runtime changed during the four-profile diagnostic') + summary = summarize(output, manifests) + print(json.dumps({key: value for key, value in summary.items() if key != 'results'}), flush=True) + + +if __name__ == '__main__': + main() diff --git a/usvm-ts-calls/scripts/test_run_class_symbolic_probe.py b/usvm-ts-calls/scripts/test_run_class_symbolic_probe.py new file mode 100644 index 0000000000..0c7c6ba222 --- /dev/null +++ b/usvm-ts-calls/scripts/test_run_class_symbolic_probe.py @@ -0,0 +1,75 @@ +import importlib.util +from pathlib import Path +import tempfile +import unittest + +SPEC = importlib.util.spec_from_file_location('probe', Path(__file__).with_name('run-class-symbolic-probe.py')) +probe = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(probe) + + +class SymbolicProbeIntegrityTest(unittest.TestCase): + def gate_fixture(self, qualifying): + classes = [{'classId': f'c{i}', 'identity': f'original-{i}', 'acquisitionComplete': i < qualifying} + for i in range(200)] + rows = [] + for case in classes: + row = probe.startup.failure_result(case, 'frozen', 'STOPPED', 'none') + if case['acquisitionComplete']: + row.update(initialStates=1, targetStatementEntered=True, originalTargetStatementsEntered=1, + started=True, qualifyingStarted=True) + rows.append(row) + return {'expectedClassCount': 200, 'classes': classes}, {'manifestSha256': 'frozen', 'complete': True, + 'qualifyingStartedCount': qualifying, 'results': rows} + + def test_gate_rejects_179_and_preserves_200_denominator_at_180(self): + manifest, results = self.gate_fixture(179) + with self.assertRaisesRegex(ValueError, '180/200'): + probe.verify_startup_gate(manifest, results, 'frozen') + + manifest, results = self.gate_fixture(180) + self.assertEqual(180, probe.verify_startup_gate(manifest, results, 'frozen')) + self.assertEqual(200, len(manifest['classes'])) + + def test_gate_rejects_reordered_or_incomplete_screen(self): + manifest, results = self.gate_fixture(200) + results['results'].reverse() + with self.assertRaisesRegex(ValueError, 'ordering'): + probe.verify_startup_gate(manifest, results, 'frozen') + + manifest, results = self.gate_fixture(200) + results['complete'] = False + with self.assertRaisesRegex(ValueError, 'completed results'): + probe.verify_startup_gate(manifest, results, 'frozen') + + def test_four_modes_keep_original_inputs_and_disable_terminal_cap(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + source = {'classes': [{'classId': 'original', 'identity': 'unchanged', 'inputSha256': {'Target.ts': 'frozen'}}]} + catalog = {'toolRevision': 'new-build', 'nativeFrontendRevision': 'pinned'} + + manifests = [probe.profile_manifest(source, profile, catalog, directory, directory) for profile in probe.PROFILES] + + self.assertEqual(list(probe.PROFILES), [manifest['profile'] for manifest in manifests]) + self.assertTrue(all(manifest['classes'] == source['classes'] for manifest in manifests)) + self.assertTrue(all(manifest['collectedStatesLimit'] is None for manifest in manifests)) + self.assertTrue(all(manifest['budgetMillis'] == 30000 and manifest['seed'] == 17 for manifest in manifests)) + + def test_missing_metrics_are_unavailable_and_pending_cells_remain(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + manifests = {profile: {'classes': [{'classId': 'target', 'identity': 'original'}]} for profile in probe.PROFILES} + for profile, manifest in manifests.items(): + probe.startup.save(directory / f'{profile}.json', manifest) + + summary = probe.summarize(directory, manifests) + + self.assertEqual(4, len(summary['results'])) + self.assertEqual(800, summary['expectedCellCount']) + self.assertFalse(summary['complete']) + self.assertTrue(all(row['returnedStates'] is None for row in summary['results'])) + self.assertTrue(all(row['nativeClassCoverage'] is None for row in summary['results'])) + + +if __name__ == '__main__': + unittest.main() diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt new file mode 100644 index 0000000000..c617a9af1f --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt @@ -0,0 +1,275 @@ +package org.usvm.ts.calls + +import kotlinx.serialization.Serializable +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsStmt +import org.usvm.UPathSelector +import org.usvm.machine.TsEntryPointTimeQuantumEvent +import org.usvm.machine.TsSolverQueryEvent +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState +import org.usvm.machine.state.lastStmt +import org.usvm.statistics.UMachineObserver +import java.nio.file.Files +import java.nio.file.Path +import java.nio.file.StandardOpenOption + +@Serializable +internal data class CallsClassRawIrPoint( + val method: String, + val statementIndex: Int, + val sourceFile: String, + val startOffset: Int, + val endOffset: Int, + val nodeKind: String, +) + +private fun EtsStmt.toClassRawIrPoint(sourceFile: String): CallsClassRawIrPoint { + val origin = checkNotNull(location.origin) + return CallsClassRawIrPoint( + method = location.method.signature.toString(), + statementIndex = location.index, + sourceFile = sourceFile, + startOffset = origin.startOffset, + endOffset = origin.endOffset, + nodeKind = origin.nodeKind, + ) +} + +@Serializable +internal data class CallsClassRawStateSnapshot( + val stateId: String, + val outcome: String, + val entryMethod: String, + val currentMethod: String, + val statementIndex: Int, + val statement: String, + val callStack: List, + val constraints: List, + val modelCount: Int, + val resultKind: String, + val symbolicResult: String? = null, + val unsupportedReason: String? = null, +) + +@Serializable +internal data class CallsClassRawAnalysis( + val budgetMillis: Long, + val analysisElapsedMillis: Long, + val budgetOverrunMillis: Long, + val timeQuantumMillis: Long, + val collectedStatesLimit: Int? = null, + val profile: CallsExperimentProfile, + val seed: Long, + val returnedStates: Long, + val exceptionalStates: Long, + val unsupportedTerminalStates: Long, + val otherReachableTerminalStates: Long, + val unreachableTerminalStates: Long, + val stoppedPrefixStates: Long, + val remainingStates: Long, + val stateSnapshotFailures: List, + val solverCalls: Long, + val solverElapsedNanos: Long, + val solverStatusCounts: Map, + val timeQuantumCount: Long, + val timeQuantumOverruns: Long, + val methodSteps: Map, + val sourceMappedIrUniverse: List, + val sourceMappedIrEntered: List, + val statementUniverseSha256: String, + val terminalStateSnapshots: List, + val stoppedPrefixSnapshots: List, + val remainingStateSnapshots: List, + val proof: String = "Symbolic source-mapped IR entry only; " + + "diagnostic state metadata is not a native replay witness", +) + +/** Retains raw symbolic outcomes without requiring finite native observation domains. */ +internal class ClassRawAnalysisObserver( + private val sourceFile: String, + private val universe: List, + private val output: Path, +) : UMachineObserver { + private val entered = linkedSetOf() + private val terminal = mutableListOf() + private val stopped = mutableListOf() + private val remaining = mutableListOf() + private val snapshotFailures = mutableListOf() + private val methodSteps = linkedMapOf() + private val solverStatuses = linkedMapOf() + private var executingMethod: String? = null + private var returnedStates = 0L + private var exceptionalStates = 0L + private var unsupportedStates = 0L + private var otherStates = 0L + private var unreachableStates = 0L + private var stoppedStates = 0L + private var remainingStates = 0L + private var solverCalls = 0L + private var solverNanos = 0L + private var quantumCount = 0L + private var quantumOverruns = 0L + + fun recordOriginalEntry(stmt: EtsStmt) { + entered += stmt.toClassRawIrPoint(sourceFile = sourceFile) + } + + override fun onStatePeeked(state: TsState) { + val method = state.lastStmt.location.method + executingMethod = method.signature.toString() + } + + override fun onState(parent: TsState, forks: Sequence) { + executingMethod?.let { methodSteps.merge(it, 1L, Long::plus) } + } + + override fun onStateTerminated(state: TsState, stateReachable: Boolean) { + if (!stateReachable) { + unreachableStates++ + return + } + val outcome = when { + state.unsupportedReason != null -> { + unsupportedStates++ + "UNSUPPORTED" + } + state.methodResult is TsMethodResult.TsException -> { + exceptionalStates++ + "THREW" + } + state.methodResult is TsMethodResult.Success -> { + returnedStates++ + "RETURNED" + } + else -> { + otherStates++ + "OTHER_REACHABLE" + } + } + saveSnapshot(state = state, outcome = outcome, destination = terminal) + } + + fun recordStoppedPrefix(state: TsState, reason: String) { + stoppedStates++ + saveSnapshot(state = state, outcome = "STOPPED_PREFIX: $reason", destination = stopped) + } + + /** Drain only after analyzeWithMetadata has computed its real stop reason. */ + fun retainRemainingStates(selector: UPathSelector?) { + selector?.drain()?.forEach { state -> + remainingStates++ + saveSnapshot(state = state, outcome = "SUSPENDED", destination = remaining) + } + } + + fun recordSolverQuery(event: TsSolverQueryEvent) { + solverCalls++ + solverNanos += event.elapsedNanos + solverStatuses.merge(event.status?.name ?: "ERROR", 1L, Long::plus) + } + + fun recordTimeQuantum(event: TsEntryPointTimeQuantumEvent) { + quantumCount++ + if (event.elapsed > event.requested) quantumOverruns++ + } + + private fun saveSnapshot(state: TsState, outcome: String, destination: MutableList) { + val snapshot = runCatching { + val stmt = state.lastStmt + val result = state.methodResult + CallsClassRawStateSnapshot( + stateId = state.id.toString(), + outcome = outcome, + entryMethod = state.entrypoint.signature.toString(), + currentMethod = stmt.location.method.signature.toString(), + statementIndex = stmt.location.index, + statement = stmt.toString(), + callStack = state.callStack.map { it.method.signature.toString() }, + constraints = state.pathConstraints.constraintSequence().map { it.toString() }.toList(), + modelCount = state.models.size, + resultKind = result::class.java.simpleName, + symbolicResult = when (result) { + is TsMethodResult.Success -> result.value.toString() + is TsMethodResult.TsException -> result.value.toString() + else -> null + }, + unsupportedReason = state.unsupportedReason, + ) + } + snapshot.fold( + onSuccess = { + destination += it + val saved = runCatching { + Files.writeString( + output.resolve("states.jsonl"), + encodeCallsArtifact(it) + "\n", + StandardOpenOption.CREATE, + StandardOpenOption.APPEND, + ) + } + saved.exceptionOrNull()?.let { failure -> + snapshotFailures += "${state.id}/$outcome: ${failure::class.java.name}: ${failure.message}" + } + }, + onFailure = { + val diagnostic = "${state.id}/$outcome: ${it::class.java.name}: ${it.message}" + snapshotFailures += diagnostic + Files.writeString( + output.resolve("state-snapshot-failures.jsonl"), + encodeCallsArtifact(mapOf("failure" to diagnostic)) + "\n", + StandardOpenOption.CREATE, + StandardOpenOption.APPEND, + ) + }, + ) + } + + fun result(manifest: CallsClassStartManifest, analysisElapsedMillis: Long): CallsClassRawAnalysis { + val encodedUniverse = encodeCallsArtifact(universe).toByteArray(Charsets.UTF_8) + return CallsClassRawAnalysis( + budgetMillis = manifest.budgetMillis, + analysisElapsedMillis = analysisElapsedMillis, + budgetOverrunMillis = (analysisElapsedMillis - manifest.budgetMillis).coerceAtLeast(0), + timeQuantumMillis = manifest.timeQuantumMillis, + profile = manifest.profile, + seed = manifest.seed, + collectedStatesLimit = manifest.collectedStatesLimit, + returnedStates = returnedStates, + exceptionalStates = exceptionalStates, + unsupportedTerminalStates = unsupportedStates, + otherReachableTerminalStates = otherStates, + unreachableTerminalStates = unreachableStates, + stoppedPrefixStates = stoppedStates, + remainingStates = remainingStates, + stateSnapshotFailures = snapshotFailures, + solverCalls = solverCalls, + solverElapsedNanos = solverNanos, + solverStatusCounts = solverStatuses, + timeQuantumCount = quantumCount, + timeQuantumOverruns = quantumOverruns, + methodSteps = methodSteps, + sourceMappedIrUniverse = universe, + sourceMappedIrEntered = entered.toList(), + statementUniverseSha256 = callsArtifactSha256(encodedUniverse), + terminalStateSnapshots = terminal, + stoppedPrefixSnapshots = stopped, + remainingStateSnapshots = remaining, + ) + } + + companion object { + fun forTarget( + methods: List, + sourceFile: String, + sourceText: String, + output: Path, + ): ClassRawAnalysisObserver { + val target = methods.first().signature.enclosingClass + val universe = methods.flatMap { it.cfg.stmts }.filter { + isOriginalClassStartupStep(stmt = it, target = target, sourceFile = sourceFile, sourceText = sourceText) + }.map { it.toClassRawIrPoint(sourceFile = sourceFile) } + return ClassRawAnalysisObserver(sourceFile = sourceFile, universe = universe, output = output) + } + } +} diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt index 9cee81222d..1b68625923 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt @@ -1,6 +1,7 @@ package org.usvm.ts.calls import kotlinx.serialization.Serializable +import kotlinx.serialization.json.Json import org.jacodb.ets.model.EtsAssignStmt import org.jacodb.ets.model.EtsCallExpr import org.jacodb.ets.model.EtsCallStmt @@ -16,19 +17,26 @@ import org.usvm.CoverageZone import org.usvm.SolverType import org.usvm.StateCollectionStrategy import org.usvm.UMachineOptions +import org.usvm.UPathSelector +import org.usvm.machine.TsEntryPointTimeQuantumEvent import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions +import org.usvm.machine.TsSolverQueryEvent import org.usvm.machine.call.TsUnknownCallEvent import org.usvm.machine.call.TsUnknownCallModelSelection import org.usvm.machine.expr.TsSimpleValueResolver import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.machine.state.lastStmt import org.usvm.statistics.UMachineObserver +import org.usvm.ts.pbt.model.encodeToUtf8SafeString import java.nio.file.Files import java.nio.file.Path +import java.nio.file.StandardOpenOption import java.util.IdentityHashMap +import kotlin.time.Duration import kotlin.time.Duration.Companion.milliseconds import kotlin.time.TimeSource @@ -81,7 +89,8 @@ internal data class CallsClassStartManifest( val expectedClassCount: Int = 200, val budgetMillis: Long = 2_000, val solverLimitMillis: Long = 250, - val collectedStatesLimit: Int = 10, + val collectedStatesLimit: Int? = 10, + val timeQuantumMillis: Long = 25, val seed: Long = 17, val profile: CallsExperimentProfile = CallsExperimentProfile.FROZEN_STOP, val classes: List, @@ -91,10 +100,18 @@ internal data class CallsClassStartManifest( require(classes.map { it.classId }.distinct().size == classes.size) require(classes.map { it.identity }.distinct().size == classes.size) require(ledgerSha256.matches(Regex("[0-9a-f]{64}"))) - require(budgetMillis > 0 && solverLimitMillis in 1..budgetMillis && collectedStatesLimit > 0) + require(budgetMillis > 0 && solverLimitMillis in 1..budgetMillis) + require(collectedStatesLimit == null || collectedStatesLimit > 0) + require(timeQuantumMillis in 1..budgetMillis) } } +/** Explicit null preserves the disabled cap instead of restoring the default startup cap on decode. */ +internal fun encodeClassStartManifest(manifest: CallsClassStartManifest): String { + val json = Json(CallsExperimentJson.json) { explicitNulls = true } + return json.encodeToUtf8SafeString(manifest) +} + @Serializable internal data class CallsClassStartResult( val classId: String, @@ -130,6 +147,7 @@ internal data class CallsClassStartResult( val diagnostic: String? = null, val failureLog: String? = null, val inputDriftLog: String? = null, + val rawAnalysis: CallsClassRawAnalysis? = null, ) /** A source return must be explicit; a synthetic default constructor return cannot prove startup. */ @@ -212,11 +230,15 @@ internal class ClassStartObserver( private val sourceText: String, private val onFirstOriginalStep: () -> Unit, private val unknownCallObserver: (TsUnknownCallEvent) -> Unit = {}, + private val originalEntryObserver: (EtsStmt) -> Unit = {}, ) : UMachineObserver, TsInterpreterObserver { private val initial = java.util.Collections.newSetFromMap(IdentityHashMap()) private val seenInitial = java.util.Collections.newSetFromMap(IdentityHashMap()) private val pending = IdentityHashMap() + private val pendingPaths = IdentityHashMap() + private val pendingResults = IdentityHashMap() private val entered = java.util.Collections.newSetFromMap(IdentityHashMap()) + private val completedAssignments = java.util.Collections.newSetFromMap(IdentityHashMap()) private val initialMethods = mutableSetOf() var executedSteps: Long = 0 private set @@ -242,7 +264,10 @@ internal class ClassStartObserver( override fun onStatePeeked(state: TsState) { if (state in initial && state.models.isNotEmpty()) seenInitial += state entered -= state + completedAssignments -= state pending[state] = state.lastStmt + pendingPaths[state] = state.pathNode + pendingResults[state] = state.methodResult } /** Statement callbacks run inside interpreter visits, before expression resolution or fallback. */ @@ -253,6 +278,7 @@ internal class ClassStartObserver( if (!original || state.pathConstraints.isFalse || state in entered) return entered += state originalStatementsEntered++ + originalEntryObserver(stmt) if (firstOriginalStep == null) { firstOriginalStep = stmt.toCallsUnknownCallSite() onFirstOriginalStep() @@ -275,6 +301,14 @@ internal class ClassStartObserver( onStatementEntered(stmt = scope.calcOnState { lastStmt }, scope = scope) } + override fun onAssignmentCompleted( + simpleValueResolver: TsSimpleValueResolver, + stmt: EtsAssignStmt, + scope: TsStepScope, + ) { + completedAssignments += scope.calcOnState { this } + } + override fun onCallStatement(simpleValueResolver: TsSimpleValueResolver, stmt: EtsCallStmt, scope: TsStepScope) { onStatementEntered(stmt = stmt, scope = scope) } @@ -302,11 +336,16 @@ internal class ClassStartObserver( override fun onState(parent: TsState, forks: Sequence) { executedSteps++ val stmt = pending.remove(parent) ?: return + val previousPath = pendingPaths.remove(parent) + val previousResult = pendingResults.remove(parent) val statementEntered = entered.remove(parent) + val assignmentCompleted = completedAssignments.remove(parent) if (stmt.location.method.signature.enclosingClass != target) return targetSteps++ - val parentSucceeded = !parent.pathConstraints.isFalse && parent.unsupportedReason == null - val forkSucceeded = forks.any { !it.pathConstraints.isFalse && it.unsupportedReason == null } + val parentSucceeded = hasSuccessfulTransition(parent, previousPath, previousResult, assignmentCompleted) + val forkSucceeded = forks.any { + hasSuccessfulTransition(it, previousPath, previousResult, assignmentCompleted = false) + } val feasibleTransition = parentSucceeded || forkSucceeded val original = isOriginalClassStartupStep(stmt = stmt, target = target, sourceFile = sourceFile, sourceText = sourceText) @@ -314,17 +353,36 @@ internal class ClassStartObserver( if (!feasibleTransition || !original || !statementEntered) return originalSteps++ } + + private fun hasSuccessfulTransition( + state: TsState, + previousPath: Any?, + previousResult: TsMethodResult?, + assignmentCompleted: Boolean, + ): Boolean { + val advanced = state.pathNode !== previousPath || state.methodResult !== previousResult || assignmentCompleted + return advanced && !state.pathConstraints.isFalse && state.unsupportedReason == null + } } /** Full raw source/IR/machine smoke, independent of observation domains and native coverage admission. */ @Suppress("LongMethod") -internal fun runClassStartSmoke(args: List) { +internal fun runClassStartSmoke(args: List) = runRawClassAnalysis(args = args, exploratory = false) + +internal fun runClassSymbolicProbe(args: List) = runRawClassAnalysis(args = args, exploratory = true) + +@Suppress("LongMethod") +private fun runRawClassAnalysis(args: List, exploratory: Boolean) { require(args.size == CLASS_START_ARGUMENT_COUNT) { "class-start-smoke requires " } val manifestPath = Path.of(args[0]).toRealPath() val bytes = Files.readAllBytes(manifestPath) val manifest = CallsExperimentJson.json.decodeFromString(bytes.toString(Charsets.UTF_8)) + if (exploratory) { + require(manifest.budgetMillis == EXPLORATORY_BUDGET_MILLIS && manifest.seed == EXPLORATORY_SEED) + require(manifest.collectedStatesLimit == null) { "The exploratory probe has no terminal-state cap" } + } require(manifest.toolRevision == CallsBuildIdentity.toolRevision) { "Smoke runtime revision changed" } require(manifest.nativeFrontendRevision == CallsBuildIdentity.nativeFrontendRevision) { "Smoke frontend changed" } require(System.getenv("ETS_FRONTEND_SCRIPT") == null) { "Use the pinned bundled frontend" } @@ -339,6 +397,9 @@ internal fun runClassStartSmoke(args: List) { var targetSignature: EtsClassSignature? = null var methods = emptyList() var observer: ClassStartObserver? = null + var rawObserver: ClassRawAnalysisObserver? = null + var remainingSelector: UPathSelector? = null + var analysisElapsedMillis = 0L val unknownCalls = mutableListOf() var outcome: org.usvm.machine.TsMachineAnalysisResult? = null var lastCheckpointMillis = 0L @@ -387,6 +448,17 @@ internal fun runClassStartSmoke(args: List) { method.cfg.stmts.any { isOriginalClassStartupStep(it, target.signature, case.sourceFile, sourceText) } } require(methods.isNotEmpty()) { "Target class has no executable IR bodies" } + val raw = if (exploratory) { + ClassRawAnalysisObserver.forTarget( + methods = methods, + sourceFile = case.sourceFile, + sourceText = sourceText, + output = output, + ) + } else { + null + } + rawObserver = raw checkpoint(next = "MACHINE") val machineObserver = ClassStartObserver( target = target.signature, @@ -425,23 +497,56 @@ internal fun runClassStartSmoke(args: List) { }, unknownCallObserver = { event -> unknownCalls += event.toCallsClassUnknownCallEvent(eventIndex = unknownCalls.size + 1) - writeCallsArtifactAtomically(output.resolve("unknown-calls.json"), encodeCallsArtifact(unknownCalls)) + if (exploratory) { + Files.writeString( + output.resolve("unknown-calls.jsonl"), + encodeCallsArtifact(unknownCalls.last()) + "\n", + StandardOpenOption.CREATE, + StandardOpenOption.APPEND, + ) + } else { + writeCallsArtifactAtomically( + output.resolve("unknown-calls.json"), + encodeCallsArtifact(unknownCalls) + ) + } }, + originalEntryObserver = { raw?.recordOriginalEntry(it) }, ) observer = machineObserver + val interpreterObserver = object : TsInterpreterObserver by machineObserver { + override fun onPathStopped(state: TsState, reason: String) { + raw?.recordStoppedPrefix(state = state, reason = reason) + } + + override fun onSolverQuery(event: TsSolverQueryEvent) { + raw?.recordSolverQuery(event) + } + + override fun onEntryPointTimeQuantum(event: TsEntryPointTimeQuantumEvent) { + raw?.recordTimeQuantum(event) + } + } + fun rawMachineObserver(selector: UPathSelector): UMachineObserver { + remainingSelector = selector + return checkNotNull(raw) + } + val factory = if (raw == null) null else ::rawMachineObserver + val timeQuantum = if (exploratory) manifest.timeQuantumMillis.milliseconds else Duration.INFINITE TsMachine( scene = scene, options = UMachineOptions( stateCollectionStrategy = StateCollectionStrategy.ALL, randomSeed = manifest.seed, collectedStatesLimit = manifest.collectedStatesLimit, + maxEntryPointTimeQuantum = timeQuantum, timeout = manifest.budgetMillis.milliseconds, solverTimeout = manifest.solverLimitMillis.milliseconds, solverType = SolverType.YICES, coverageZone = CoverageZone.CLASS, stopOnCoverage = 0, removeCoveredEntryPoints = false, - throwExceptionOnStepFailure = true, + throwExceptionOnStepFailure = !exploratory, ), tsOptions = TsOptions( unknownCallModelSelection = if (manifest.profile.usesFrozenModels) { @@ -454,15 +559,22 @@ internal fun runClassStartSmoke(args: List) { classCoverageTargets = setOf(target.signature), ), machineObserver = machineObserver, - observer = machineObserver, + observer = interpreterObserver, + machineObserverFactory = factory, ).use { machine -> checkpoint(next = "INITIAL_STATE") - outcome = machine.analyzeWithMetadata( - methods = methods, - configureInitialState = { method, state -> - machineObserver.registerInitialState(method = method, state = state) - } - ) + val analysisStarted = TimeSource.Monotonic.markNow() + try { + outcome = machine.analyzeWithMetadata( + methods = methods, + configureInitialState = { method, state -> + machineObserver.registerInitialState(method = method, state = state) + }, + ) + } finally { + analysisElapsedMillis = analysisStarted.elapsedNow().inWholeMilliseconds + raw?.retainRemainingStates(selector = remainingSelector) + } } case.verifyInputs() checkpoint(next = "STOPPED") @@ -524,9 +636,12 @@ internal fun runClassStartSmoke(args: List) { }, failureLog = failureLog, inputDriftLog = inputDriftLog, + rawAnalysis = rawObserver?.result(manifest = manifest, analysisElapsedMillis = analysisElapsedMillis), ) writeCallsArtifactAtomically(output.resolve("result.json"), encodeCallsArtifact(result)) System.out.appendLine(encodeCallsArtifact(result)) } private const val CLASS_START_ARGUMENT_COUNT = 3 +private const val EXPLORATORY_BUDGET_MILLIS = 30_000L +private const val EXPLORATORY_SEED = 17L diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperimentCli.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperimentCli.kt index 2e20f7ef3a..004c03d6d6 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperimentCli.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperimentCli.kt @@ -11,6 +11,7 @@ fun main(args: Array) { when (args.first()) { "class-catalog" -> runClassCatalog(args.drop(1)) "class-start-smoke" -> runClassStartSmoke(args.drop(1)) + "class-symbolic-probe" -> runClassSymbolicProbe(args.drop(1)) "class-prepare" -> runClassPrepare(args.drop(1)) "class-preflight" -> runClassPreflight(args.drop(1)) "class-cell" -> runClassCell(args.drop(1)) @@ -106,6 +107,7 @@ private fun usage(): String = """ Usage: calls class-catalog calls class-start-smoke + calls class-symbolic-probe calls class-prepare calls class-preflight calls class-cell diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt index c561d0ad3a..6f6d94a7d3 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt @@ -143,9 +143,31 @@ class CallsClassStartSmokeTest { assertTrue(result.unsupportedCall) } + @Test + fun `exploratory probe retains residual prefixes and independent source mapped IR universe`() { + val result = runFixture( + sourceText = "export class Target { constructor() { Date.now(); } }", + profile = CallsExperimentProfile.EMPTY_STOP, + exploratory = true, + ) + + assertTrue(result.started, result.toString()) + val raw = checkNotNull(result.rawAnalysis) + assertEquals(30_000L, raw.budgetMillis) + assertEquals(null, raw.collectedStatesLimit) + assertTrue(raw.stoppedPrefixStates > 0) + assertEquals(raw.stoppedPrefixStates, raw.stoppedPrefixSnapshots.size.toLong()) + assertTrue(raw.sourceMappedIrUniverse.isNotEmpty()) + assertTrue(raw.sourceMappedIrEntered.isNotEmpty()) + assertTrue(raw.sourceMappedIrUniverse.containsAll(raw.sourceMappedIrEntered)) + assertTrue(raw.stateSnapshotFailures.isEmpty(), raw.stateSnapshotFailures.toString()) + assertTrue(Files.isRegularFile(directory.resolve("output/states.jsonl"))) + } + private fun runFixture( sourceText: String, profile: CallsExperimentProfile = CallsExperimentProfile.FROZEN_STOP, + exploratory: Boolean = false, ): CallsClassStartResult { val source = directory.resolve("Target.ts") Files.writeString(source, sourceText) @@ -169,13 +191,20 @@ class CallsClassStartSmokeTest { ledgerSha256 = "b".repeat(64), expectedClassCount = 1, profile = profile, + budgetMillis = if (exploratory) 30_000 else 2_000, + collectedStatesLimit = if (exploratory) null else 10, classes = listOf(case), ) val path = directory.resolve("manifest.json") - Files.writeString(path, encodeCallsArtifact(manifest)) + Files.writeString(path, encodeClassStartManifest(manifest)) val output = directory.resolve("output") - runClassStartSmoke(listOf(path.toString(), "target", output.toString())) + val args = listOf(path.toString(), "target", output.toString()) + if (exploratory) { + runClassSymbolicProbe(args) + } else { + runClassStartSmoke(args) + } return CallsExperimentJson.json.decodeFromString(Files.readString(output.resolve("result.json"))) } From da46960c1b7646244b3fab2fc48736ba51034709 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 02:57:36 +0300 Subject: [PATCH 4/8] Bind raw class entries and pin startup runtime provenance Select runtime class declarations without dropping merged interfaces. Keep lowered closure bodies in the scene but enter them through their owning member. Observe actual statement dispatch, reject frontend overrides, and bind the measurement gate and IR cache to verified runtime bytes. --- usvm-ts-calls/CLASS_START_SMOKE.md | 20 ++++++-- .../scripts/run-class-start-smoke.py | 3 +- .../scripts/run-class-symbolic-probe.py | 9 +++- .../scripts/test_run_class_symbolic_probe.py | 10 +++- .../usvm/ts/calls/CallsClassRawAnalysis.kt | 4 ++ .../usvm/ts/calls/CallsClassStartIrCache.kt | 11 +++++ .../org/usvm/ts/calls/CallsClassStartSmoke.kt | 47 +++++++++++++++++-- .../usvm/ts/calls/CallsClassStartSmokeTest.kt | 43 +++++++++++++++++ .../org/usvm/machine/TsInterpreterObserver.kt | 5 ++ .../usvm/machine/interpreter/TsInterpreter.kt | 2 + 10 files changed, 141 insertions(+), 13 deletions(-) diff --git a/usvm-ts-calls/CLASS_START_SMOKE.md b/usvm-ts-calls/CLASS_START_SMOKE.md index 8462bd06df..eb51d70362 100644 --- a/usvm-ts-calls/CLASS_START_SMOKE.md +++ b/usvm-ts-calls/CLASS_START_SMOKE.md @@ -22,9 +22,9 @@ group, including a frontend subprocess. ## Startup criterion `started` requires both a real initial state with a model and an interpreter callback for an original -executable statement of the selected target class. Assignment, unresolved assignment call, standalone -call, conditional, explicit return, and throw callbacks run inside the corresponding interpreter visit, -before expression resolution or unknown-call dispatch. Queue selection alone cannot establish startup. +executable statement of the selected target class. The generic callback runs inside `TsInterpreter.step`, +after step preparation and before statement dispatch, including field definitions. Source attribution +does not run on exception-propagation or failed preparation paths. Queue selection alone cannot establish startup. Synthetic default returns, NOPs, declarations without initializers, foreign classes, and missing source spans cannot establish it either. A first unsupported residual call can establish startup even when its successful transition count is zero; this is recorded as `STARTED_WITH_LIMITATION`. @@ -62,9 +62,21 @@ identity requires a new output directory. An interrupted child without a final d requires a fresh attempt directory. The shared cache stores immutable frontend IR only, keyed by frozen inputs, resolved compiler config, -frontend revision, and project revision. It verifies every cached file before reuse. Scenes, machines, +frontend revision and actual provider binary hash, and project revision. It verifies every cached file before reuse. Scenes, machines, initial states, and solver states are always created separately for each class. +Runtime target lookup requires the exact file, class name, and `CLASS` declaration category. A merged +TypeScript interface remains in the full scene and is listed in the receipt; it cannot compete as the +runtime target. All target IR bodies remain loaded and reported. Compiler-lowered anonymous closures +are marked `LOWERED_CLOSURE_REACHABLE_VIA_OWNER`; they run through their owning member with its allocated +closure environment rather than receiving a fabricated independent closure argument. Declared methods, +constructors, and initialization bodies remain independent entries. The source-mapped IR universe keeps +the complete class, including these dependent closure bodies. + +Both `ETS_FRONTEND_SCRIPT` and `ETS_FRONTEND_DIR` overrides are rejected. The exploratory gate additionally +requires the exact tool/frontend revisions and runtime byte hashes that produced the completed startup +screen; changing the engine, frontend, shared driver, Java, or Node requires a fresh startup screen. + ## Exploratory four-profile probe After a completed startup screen proves at least 180 qualifying starts from the exact original 200 diff --git a/usvm-ts-calls/scripts/run-class-start-smoke.py b/usvm-ts-calls/scripts/run-class-start-smoke.py index ad91f18176..2e61b1a50c 100644 --- a/usvm-ts-calls/scripts/run-class-start-smoke.py +++ b/usvm-ts-calls/scripts/run-class-start-smoke.py @@ -87,6 +87,7 @@ def runtime_identity(calls): files['javaVersion'] = subprocess.check_output([str(java), '-version'], stderr=subprocess.STDOUT, text=True, timeout=10) files['JVMEnvironment'] = {name: os.environ.get(name) for name in ('JAVA_OPTS', 'JDK_JAVA_OPTIONS', '_JAVA_OPTIONS')} + files['frontendOverrides'] = {name: os.environ.get(name) for name in ('ETS_FRONTEND_SCRIPT', 'ETS_FRONTEND_DIR')} return files @@ -183,7 +184,7 @@ def main(): calls = args.calls.resolve(strict=True) fingerprint = sha(manifest_path) environment = dict(os.environ) - if environment.get('ETS_FRONTEND_SCRIPT') is not None: + if environment.get('ETS_FRONTEND_SCRIPT') is not None or environment.get('ETS_FRONTEND_DIR') is not None: raise ValueError('Startup probes require the pinned bundled frontend') environment['USVM_TS_CALLS_OPTS'] = '-Xms1g -Xmx6g -XX:+UseG1GC' environment['USVM_TS_STARTUP_IR_CACHE'] = str((args.ir_cache or output / 'ir-cache').resolve()) diff --git a/usvm-ts-calls/scripts/run-class-symbolic-probe.py b/usvm-ts-calls/scripts/run-class-symbolic-probe.py index cf9edf0f9d..c27f599a94 100644 --- a/usvm-ts-calls/scripts/run-class-symbolic-probe.py +++ b/usvm-ts-calls/scripts/run-class-symbolic-probe.py @@ -37,9 +37,11 @@ def verify_startup_gate(manifest, results, fingerprint): def profile_manifest(source, profile, catalog, original_directory, output): + if (catalog['toolRevision'] != source['toolRevision'] + or catalog['nativeFrontendRevision'] != source['nativeFrontendRevision']): + raise ValueError('Exploratory runtime differs from the exact runtime that proved the startup gate') result = copy.deepcopy(source) - result.update(toolRevision=catalog['toolRevision'], nativeFrontendRevision=catalog['nativeFrontendRevision'], - budgetMillis=BUDGET_MILLIS, solverLimitMillis=250, timeQuantumMillis=25, + result.update(budgetMillis=BUDGET_MILLIS, solverLimitMillis=250, timeQuantumMillis=25, collectedStatesLimit=None, profile=profile, seed=SEED) for case in result['classes']: receipt = case.get('acquisitionReceipt') @@ -121,6 +123,9 @@ def main(): calls = args.calls.resolve(strict=True) catalog = json.loads(subprocess.check_output([str(calls), 'class-catalog'], text=True, timeout=60)) runtime = startup.runtime_identity(calls) + startup_identity = startup.read(args.startup_summary.resolve(strict=True).parent / 'identity.json') + if startup_identity.get('manifestSha256') != startup.sha(manifest_path) or startup_identity.get('runtime') != runtime: + raise ValueError('Exploratory runtime bytes differ from the exact frozen startup runtime') identity = {'startupManifestSha256': startup.sha(manifest_path), 'startupSummarySha256': startup.sha(args.startup_summary), 'qualifyingStarted': qualifying, 'runtime': runtime, 'driverSha256': startup.sha(Path(__file__)), 'catalog': catalog, 'profiles': list(PROFILES), 'budgetMillis': BUDGET_MILLIS, 'seed': SEED, diff --git a/usvm-ts-calls/scripts/test_run_class_symbolic_probe.py b/usvm-ts-calls/scripts/test_run_class_symbolic_probe.py index 0c7c6ba222..1d5c334ae4 100644 --- a/usvm-ts-calls/scripts/test_run_class_symbolic_probe.py +++ b/usvm-ts-calls/scripts/test_run_class_symbolic_probe.py @@ -45,7 +45,8 @@ def test_gate_rejects_reordered_or_incomplete_screen(self): def test_four_modes_keep_original_inputs_and_disable_terminal_cap(self): with tempfile.TemporaryDirectory() as temporary: directory = Path(temporary) - source = {'classes': [{'classId': 'original', 'identity': 'unchanged', 'inputSha256': {'Target.ts': 'frozen'}}]} + source = {'toolRevision': 'new-build', 'nativeFrontendRevision': 'pinned', + 'classes': [{'classId': 'original', 'identity': 'unchanged', 'inputSha256': {'Target.ts': 'frozen'}}]} catalog = {'toolRevision': 'new-build', 'nativeFrontendRevision': 'pinned'} manifests = [probe.profile_manifest(source, profile, catalog, directory, directory) for profile in probe.PROFILES] @@ -55,6 +56,13 @@ def test_four_modes_keep_original_inputs_and_disable_terminal_cap(self): self.assertTrue(all(manifest['collectedStatesLimit'] is None for manifest in manifests)) self.assertTrue(all(manifest['budgetMillis'] == 30000 and manifest['seed'] == 17 for manifest in manifests)) + def test_changed_engine_or_frontend_cannot_reuse_old_startup_gate(self): + source = {'toolRevision': 'frozen-build', 'nativeFrontendRevision': 'frozen-frontend', 'classes': []} + for catalog in [{'toolRevision': 'changed-build', 'nativeFrontendRevision': 'frozen-frontend'}, + {'toolRevision': 'frozen-build', 'nativeFrontendRevision': 'changed-frontend'}]: + with self.assertRaisesRegex(ValueError, 'exact runtime'): + probe.profile_manifest(source, 'EMPTY_STOP', catalog, Path('/tmp'), Path('/tmp')) + def test_missing_metrics_are_unavailable_and_pending_cells_remain(self): with tempfile.TemporaryDirectory() as temporary: directory = Path(temporary) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt index c617a9af1f..bc3f18d801 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt @@ -75,6 +75,7 @@ internal data class CallsClassRawAnalysis( val timeQuantumCount: Long, val timeQuantumOverruns: Long, val methodSteps: Map, + val sourceEnteredStatementKinds: Map, val sourceMappedIrUniverse: List, val sourceMappedIrEntered: List, val statementUniverseSha256: String, @@ -97,6 +98,7 @@ internal class ClassRawAnalysisObserver( private val remaining = mutableListOf() private val snapshotFailures = mutableListOf() private val methodSteps = linkedMapOf() + private val sourceKinds = linkedMapOf() private val solverStatuses = linkedMapOf() private var executingMethod: String? = null private var returnedStates = 0L @@ -113,6 +115,7 @@ internal class ClassRawAnalysisObserver( fun recordOriginalEntry(stmt: EtsStmt) { entered += stmt.toClassRawIrPoint(sourceFile = sourceFile) + sourceKinds.merge(stmt::class.java.simpleName, 1L, Long::plus) } override fun onStatePeeked(state: TsState) { @@ -249,6 +252,7 @@ internal class ClassRawAnalysisObserver( timeQuantumCount = quantumCount, timeQuantumOverruns = quantumOverruns, methodSteps = methodSteps, + sourceEnteredStatementKinds = sourceKinds, sourceMappedIrUniverse = universe, sourceMappedIrEntered = entered.toList(), statementUniverseSha256 = callsArtifactSha256(encodedUniverse), diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt index 68f665933d..b8d4e1daad 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt @@ -13,11 +13,22 @@ import kotlin.time.Duration.Companion.seconds @Serializable internal data class CallsClassStartIrCache(val fingerprint: String, val irSha256: Map) +private fun bundledFrontendBinarySha256(): String { + val location = checkNotNull(EtsIrProvider::class.java.protectionDomain.codeSource).location + val path = Path.of(location.toURI()).toRealPath() + if (Files.isRegularFile(path)) return callsArtifactSha256(Files.readAllBytes(path)) + + val contents = startupIrFiles(path) + require(contents.isNotEmpty()) { "Bundled frontend runtime files are absent" } + return callsArtifactSha256(encodeCallsArtifact(contents).toByteArray(Charsets.UTF_8)) +} + internal fun startupIrFingerprint(case: CallsClassStartCase): String { val values = mapOf( "inputs" to CallsExperimentJson.json.encodeToUtf8SafeString(case.inputSha256.toSortedMap().toMap()), "frontendConfig" to case.frontendConfig.orEmpty(), "frontendRevision" to CallsBuildIdentity.nativeFrontendRevision, + "frontendBinarySha256" to bundledFrontendBinarySha256(), "projectRevision" to case.projectRevision, ) return callsArtifactSha256(CallsExperimentJson.json.encodeToUtf8SafeString(values).toByteArray()) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt index 1b68625923..548c40027b 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt @@ -5,6 +5,7 @@ import kotlinx.serialization.json.Json import org.jacodb.ets.model.EtsAssignStmt import org.jacodb.ets.model.EtsCallExpr import org.jacodb.ets.model.EtsCallStmt +import org.jacodb.ets.model.EtsClassCategory import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsIfStmt import org.jacodb.ets.model.EtsMethod @@ -12,6 +13,7 @@ import org.jacodb.ets.model.EtsNopStmt import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsStmt import org.jacodb.ets.model.EtsThrowStmt +import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX import org.jacodb.ets.utils.loadEtsProjectFromIR import org.usvm.CoverageZone import org.usvm.SolverType @@ -148,8 +150,29 @@ internal data class CallsClassStartResult( val failureLog: String? = null, val inputDriftLog: String? = null, val rawAnalysis: CallsClassRawAnalysis? = null, + val targetDeclarationCandidates: List = emptyList(), + val entryPointEligibility: List = emptyList(), ) +@Serializable +internal data class CallsClassStartEntryPoint( + val methodSignature: String, + val standalone: Boolean, + val reason: String? = null, +) + +/** Compiler-lowered closures need their allocated environment from the owning member's execution. */ +internal fun classStartupEntryPoints( + methods: List, +): List = methods.map { method -> + val requiresClosureBinding = method.name.startsWith(ANONYMOUS_METHOD_PREFIX) + CallsClassStartEntryPoint( + methodSignature = method.signature.toString(), + standalone = !requiresClosureBinding, + reason = if (requiresClosureBinding) "LOWERED_CLOSURE_REACHABLE_VIA_OWNER" else null, + ) +} + /** A source return must be explicit; a synthetic default constructor return cannot prove startup. */ internal fun isOriginalClassStartupStep( stmt: EtsStmt, @@ -271,7 +294,7 @@ internal class ClassStartObserver( } /** Statement callbacks run inside interpreter visits, before expression resolution or fallback. */ - private fun onStatementEntered(stmt: EtsStmt, scope: TsStepScope) { + override fun onStatementEntered(stmt: EtsStmt, scope: TsStepScope) { val state = scope.calcOnState { this } val original = isOriginalClassStartupStep(stmt = stmt, target = target, sourceFile = sourceFile, sourceText = sourceText) @@ -385,7 +408,9 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { } require(manifest.toolRevision == CallsBuildIdentity.toolRevision) { "Smoke runtime revision changed" } require(manifest.nativeFrontendRevision == CallsBuildIdentity.nativeFrontendRevision) { "Smoke frontend changed" } - require(System.getenv("ETS_FRONTEND_SCRIPT") == null) { "Use the pinned bundled frontend" } + require(System.getenv("ETS_FRONTEND_SCRIPT") == null && System.getenv("ETS_FRONTEND_DIR") == null) { + "Use the pinned bundled frontend without script/directory overrides" + } val case = manifest.classes.single { it.classId == args[1] } val output = Path.of(args[2]).toAbsolutePath().normalize() Files.createDirectories(output) @@ -395,7 +420,9 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { val startedAt = TimeSource.Monotonic.markNow() var stage = "INPUT_VERIFICATION" var targetSignature: EtsClassSignature? = null + var targetDeclarations = emptyList() var methods = emptyList() + var entryPoints = emptyList() var observer: ClassStartObserver? = null var rawObserver: ClassRawAnalysisObserver? = null var remainingSelector: UPathSelector? = null @@ -436,11 +463,15 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { checkpoint(next = "SCENE") val scene = loadEtsProjectFromIR(projectFilesPath = ir, sdkFilesPath = null) checkpoint(next = "TARGET") - val targets = scene.projectClasses.filter { owner -> + val declarations = scene.projectClasses.filter { owner -> val file = owner.signature.file.fileName.replace('\\', '/') owner.name == case.className && (file == case.sourceFile || file.endsWith("/${case.sourceFile}")) } - require(targets.size == 1) { "Target class is absent or ambiguous: ${targets.size}" } + targetDeclarations = declarations.map { "${it.signature} [${it.category}] methods=${it.methods.size}" } + val targets = declarations.filter { it.category == EtsClassCategory.CLASS } + require(targets.size == 1) { + "Runtime target class is absent or ambiguous: ${targets.size}; declarations=$targetDeclarations" + } val target = targets.single() targetSignature = target.signature val sourceText = Files.readString(scope.resolve(case.sourceFile)) @@ -448,6 +479,9 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { method.cfg.stmts.any { isOriginalClassStartupStep(it, target.signature, case.sourceFile, sourceText) } } require(methods.isNotEmpty()) { "Target class has no executable IR bodies" } + entryPoints = classStartupEntryPoints(methods) + val independentMethods = methods.filter { !it.name.startsWith(ANONYMOUS_METHOD_PREFIX) } + require(independentMethods.isNotEmpty()) { "Target class has no independently bindable entry points" } val raw = if (exploratory) { ClassRawAnalysisObserver.forTarget( methods = methods, @@ -492,6 +526,7 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { targetSignature = target.signature.toString(), methodSignatures = methods.map { it.signature.toString() }, firstOriginalStep = current.firstOriginalStep, + entryPointEligibility = entryPoints, ) writeCallsArtifactAtomically(output.resolve("progress.json"), encodeCallsArtifact(progress)) }, @@ -566,7 +601,7 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { val analysisStarted = TimeSource.Monotonic.markNow() try { outcome = machine.analyzeWithMetadata( - methods = methods, + methods = independentMethods, configureInitialState = { method, state -> machineObserver.registerInitialState(method = method, state = state) }, @@ -637,6 +672,8 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { failureLog = failureLog, inputDriftLog = inputDriftLog, rawAnalysis = rawObserver?.result(manifest = manifest, analysisElapsedMillis = analysisElapsedMillis), + targetDeclarationCandidates = targetDeclarations, + entryPointEligibility = entryPoints, ) writeCallsArtifactAtomically(output.resolve("result.json"), encodeCallsArtifact(result)) System.out.appendLine(encodeCallsArtifact(result)) diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt index 6f6d94a7d3..e9f1ae9462 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt @@ -164,6 +164,49 @@ class CallsClassStartSmokeTest { assertTrue(Files.isRegularFile(directory.resolve("output/states.jsonl"))) } + @Test + fun `merged interface does not make its runtime class ambiguous`() { + val result = runFixture( + sourceText = "export class Target { value = 1; read(): number { return this.value; } } " + + "export interface Target { read(): number; }", + ) + + assertEquals(2, result.targetDeclarationCandidates.size) + assertTrue(result.targetDeclarationCandidates.any { it.contains("[INTERFACE]") }) + assertTrue(result.targetDeclarationCandidates.any { it.contains("[CLASS]") }) + assertTrue(result.methodSignatures.any { it.contains("read") }) + assertTrue(result.targetSignature != null) + assertTrue(result.stage != "TARGET", result.toString()) + } + + @Test + fun `lowered closures keep complete IR but require their owning member environment`() { + val result = runFixture( + sourceText = "export class Target { value = 1; read(): number { " + + "const callback = () => this.value; return callback(); } }", + ) + + assertTrue(result.started, result.toString()) + val dependent = result.entryPointEligibility.filter { !it.standalone } + assertTrue(dependent.isNotEmpty(), result.toString()) + assertTrue(dependent.all { it.reason == "LOWERED_CLOSURE_REACHABLE_VIA_OWNER" }) + assertTrue(result.methodSignatures.containsAll(dependent.map { it.methodSignature })) + assertTrue(result.entryPointEligibility.any { it.standalone && it.methodSignature.contains("read") }) + assertTrue(result.generatedInitialMethodCount < result.methodSignatures.size) + } + + @Test + fun `generic interpreter entry callback observes source property definitions`() { + val result = runFixture( + sourceText = "export class Target { read(): number { const object = { value: 1 }; return object.value; } }", + exploratory = true, + ) + + assertTrue(result.started, result.toString()) + val raw = checkNotNull(result.rawAnalysis) + assertTrue(raw.sourceEnteredStatementKinds.getOrDefault("EtsDefineDataPropertyStmt", 0) > 0, raw.toString()) + } + private fun runFixture( sourceText: String, profile: CallsExperimentProfile = CallsExperimentProfile.FROZEN_STOP, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index 76d2d7ab2a..1d7d096e9a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -19,6 +19,11 @@ private val logger = KotlinLogging.logger {} @Suppress("unused") interface TsInterpreterObserver : UInterpreterObserver { + /** Called inside the interpreter after step preparation, immediately before statement dispatch. */ + fun onStatementEntered(stmt: EtsStmt, scope: TsStepScope) { + // default empty implementation + } + /** Each completed selector turn, including the final partial turn and repeated turns of one entry point. */ fun onEntryPointTimeQuantum(event: TsEntryPointTimeQuantumEvent) { // default empty implementation diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 4bf84f6057..1249e3c441 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -166,6 +166,8 @@ class TsInterpreter( try { scope.prepareRefinedStringBackings() ?: return scope.stepResult() + observer?.onStatementEntered(stmt, scope) + when (stmt) { is TsVirtualMethodCallStmt -> visitVirtualMethodCall(scope, stmt) is TsConcreteMethodCallStmt -> visitConcreteMethodCall(scope, stmt) From e1f6032e5c6dabfc2766c1ca3577df528065b183 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 03:13:33 +0300 Subject: [PATCH 5/8] Read exploratory frontend identity from the packaged runtime --- .../scripts/run-class-symbolic-probe.py | 25 ++++++++++++++- .../scripts/test_run_class_symbolic_probe.py | 32 +++++++++++++++++++ 2 files changed, 56 insertions(+), 1 deletion(-) diff --git a/usvm-ts-calls/scripts/run-class-symbolic-probe.py b/usvm-ts-calls/scripts/run-class-symbolic-probe.py index c27f599a94..54b43b2f4b 100644 --- a/usvm-ts-calls/scripts/run-class-symbolic-probe.py +++ b/usvm-ts-calls/scripts/run-class-symbolic-probe.py @@ -8,6 +8,7 @@ import shutil import subprocess import sys +import zipfile SMOKE_SCRIPT = Path(__file__).with_name('run-class-start-smoke.py') SPEC = importlib.util.spec_from_file_location('startup', SMOKE_SCRIPT) @@ -20,6 +21,28 @@ SEED = 17 +def runtime_catalog(calls): + catalog = json.loads(subprocess.check_output([str(calls), 'class-catalog'], text=True, timeout=60)) + resource = 'org/usvm/ts/calls/build.properties' + identities = [] + for jar_path in sorted((calls.parent.parent / 'lib').glob('*.jar')): + with zipfile.ZipFile(jar_path) as jar: + if resource not in jar.namelist(): + continue + lines = jar.read(resource).decode('utf-8').splitlines() + properties = dict(line.split('=', 1) for line in lines if '=' in line and not line.startswith('#')) + identities.append(properties) + if len(identities) != 1: + raise ValueError('Expected exactly one packaged Calls build identity') + identity = identities[0] + if catalog['toolRevision'] != identity.get('tool.revision'): + raise ValueError('Catalog differs from the packaged Calls revision') + frontend = identity.get('native.frontend.revision') + if not frontend: + raise ValueError('Packaged Calls build has no native frontend identity') + return {**catalog, 'nativeFrontendRevision': frontend} + + def verify_startup_gate(manifest, results, fingerprint): if len(manifest['classes']) != EXPECTED_CLASSES or manifest.get('expectedClassCount', EXPECTED_CLASSES) != EXPECTED_CLASSES: raise ValueError('The exploratory denominator must remain the frozen original 200 classes') @@ -121,7 +144,7 @@ def main(): output = args.output.resolve() output.mkdir(parents=True, exist_ok=True) calls = args.calls.resolve(strict=True) - catalog = json.loads(subprocess.check_output([str(calls), 'class-catalog'], text=True, timeout=60)) + catalog = runtime_catalog(calls) runtime = startup.runtime_identity(calls) startup_identity = startup.read(args.startup_summary.resolve(strict=True).parent / 'identity.json') if startup_identity.get('manifestSha256') != startup.sha(manifest_path) or startup_identity.get('runtime') != runtime: diff --git a/usvm-ts-calls/scripts/test_run_class_symbolic_probe.py b/usvm-ts-calls/scripts/test_run_class_symbolic_probe.py index 1d5c334ae4..e6c6097219 100644 --- a/usvm-ts-calls/scripts/test_run_class_symbolic_probe.py +++ b/usvm-ts-calls/scripts/test_run_class_symbolic_probe.py @@ -2,6 +2,8 @@ from pathlib import Path import tempfile import unittest +from unittest.mock import patch +import zipfile SPEC = importlib.util.spec_from_file_location('probe', Path(__file__).with_name('run-class-symbolic-probe.py')) probe = importlib.util.module_from_spec(SPEC) @@ -9,6 +11,36 @@ class SymbolicProbeIntegrityTest(unittest.TestCase): + def test_real_catalog_schema_gets_frontend_from_packaged_identity(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + calls = directory / 'bin/calls' + library = directory / 'lib' + library.mkdir() + with zipfile.ZipFile(library / 'calls.jar', 'w') as jar: + jar.writestr('org/usvm/ts/calls/build.properties', + 'tool.revision=frozen-build\nnative.frontend.revision=bundled:frozen-frontend\n') + + with patch.object(probe.subprocess, 'check_output', return_value='{"toolRevision":"frozen-build","ids":["m"]}'): + catalog = probe.runtime_catalog(calls) + + self.assertEqual('bundled:frozen-frontend', catalog['nativeFrontendRevision']) + self.assertEqual(['m'], catalog['ids']) + + def test_catalog_rejects_mismatched_packaged_build(self): + with tempfile.TemporaryDirectory() as temporary: + directory = Path(temporary) + calls = directory / 'bin/calls' + library = directory / 'lib' + library.mkdir() + with zipfile.ZipFile(library / 'calls.jar', 'w') as jar: + jar.writestr('org/usvm/ts/calls/build.properties', + 'tool.revision=different-build\nnative.frontend.revision=bundled:frozen-frontend\n') + + with patch.object(probe.subprocess, 'check_output', return_value='{"toolRevision":"frozen-build","ids":[]}'): + with self.assertRaisesRegex(ValueError, 'packaged Calls revision'): + probe.runtime_catalog(calls) + def gate_fixture(self, qualifying): classes = [{'classId': f'c{i}', 'identity': f'original-{i}', 'acquisitionComplete': i < qualifying} for i in range(200)] From d7de351c94398a4e25aea37d2ff15d3adddeacf8 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 10:24:17 +0300 Subject: [PATCH 6/8] Stream raw class snapshots through shared gzip journals --- usvm-ts-calls/CLASS_START_SMOKE.md | 12 +- .../scripts/run-class-start-smoke.py | 8 +- .../scripts/run-class-symbolic-probe.py | 3 + .../scripts/test_run_class_start_smoke.py | 4 + .../usvm/ts/calls/CallsClassRawAnalysis.kt | 98 ++++++------ .../ts/calls/CallsClassRawSnapshotStore.kt | 140 ++++++++++++++++++ .../calls/CallsClassRawSnapshotStoreTest.kt | 123 +++++++++++++++ .../usvm/ts/calls/CallsClassStartSmokeTest.kt | 6 +- 8 files changed, 332 insertions(+), 62 deletions(-) create mode 100644 usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStore.kt create mode 100644 usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStoreTest.kt diff --git a/usvm-ts-calls/CLASS_START_SMOKE.md b/usvm-ts-calls/CLASS_START_SMOKE.md index eb51d70362..731f17074c 100644 --- a/usvm-ts-calls/CLASS_START_SMOKE.md +++ b/usvm-ts-calls/CLASS_START_SMOKE.md @@ -101,8 +101,16 @@ catalog and runtime bytes are frozen before any profile runs. Unlike diagnostic startup, interpreter step failures are retained through the machine's failure metadata while other paths continue. Returned, exceptional, unsupported terminal, stopped-prefix, and remaining queued states are counted separately. Diagnostic snapshots retain method provenance, -statement text, symbolic result, and path constraints in `states.jsonl`; snapshot failures remain -explicit. Remaining states are drained after the machine has computed its actual stop reason. +statement text, symbolic result, and complete ordered path constraints. Each snapshot is streamed to +`child/states.jsonl.gz`; `constraintIds` and `symbolicResultId` refer to the exact diagnostic strings in +`child/expressions.jsonl.gz`. Expression identity is interned across states, so a shared constraint is +rendered once without truncating its contents or reducing the set of states. The final result contains +only journal references, SHA-256, compressed sizes, record counts, and completion flags; no snapshots +are embedded a second time. Journals contain concatenated complete gzip members, flushed and fsynced +before each state is acknowledged. Standard streaming gzip readers decode them in order. A killed +child retains its earlier completed members; a missing final result or a false completion flag remains +an incomplete measurement. Snapshot failures remain explicit. Remaining states are drained after the +machine has computed its actual stop reason. Unknown-call events are appended to `unknown-calls.jsonl`. These diagnostic snapshots are not concrete native witnesses or resumable machine states. diff --git a/usvm-ts-calls/scripts/run-class-start-smoke.py b/usvm-ts-calls/scripts/run-class-start-smoke.py index 2e61b1a50c..295a72353c 100644 --- a/usvm-ts-calls/scripts/run-class-start-smoke.py +++ b/usvm-ts-calls/scripts/run-class-start-smoke.py @@ -128,11 +128,15 @@ def child_result(child, receipt, case, fingerprint): result['unknownCalls'] = read(journal) elif (child / 'unknown-calls.jsonl').exists(): result['unknownCalls'] = [json.loads(line) for line in (child / 'unknown-calls.jsonl').read_text().splitlines()] - if (child / 'states.jsonl').exists(): - result['durableStateSnapshotsPath'] = str(child / 'states.jsonl') else: stage = 'CHILD_TIMEOUT' if receipt.get('timedOut') else 'CHILD_EXIT_FAILURE' result = failure_result(case, fingerprint, stage, f'Child did not produce result: {receipt}') + for filename in ('states.jsonl.gz', 'states.jsonl'): + if (child / filename).is_file(): + result['durableStateSnapshotsPath'] = str(child / filename) + break + if (child / 'expressions.jsonl.gz').is_file(): + result['durableSymbolicExpressionsPath'] = str(child / 'expressions.jsonl.gz') validate_result(result, case, fingerprint) return result diff --git a/usvm-ts-calls/scripts/run-class-symbolic-probe.py b/usvm-ts-calls/scripts/run-class-symbolic-probe.py index 54b43b2f4b..c47f4c4ea1 100644 --- a/usvm-ts-calls/scripts/run-class-symbolic-probe.py +++ b/usvm-ts-calls/scripts/run-class-symbolic-probe.py @@ -114,6 +114,9 @@ def summarize(output, manifests): 'sourceMappedIrUniverseSha256': raw['statementUniverseSha256'] if raw is not None else None, 'nativeClassCoverage': None, 'receipt': str(path), 'durableStateSnapshotsPath': result.get('durableStateSnapshotsPath'), + 'durableSymbolicExpressionsPath': result.get('durableSymbolicExpressionsPath'), + 'stateSnapshotJournal': raw.get('stateSnapshots') if raw is not None else None, + 'symbolicExpressionJournal': raw.get('symbolicExpressions') if raw is not None else None, 'diagnostic': result.get('diagnostic')}) if len(universe_hashes) > 1: raise ValueError(f'Source-mapped IR universe changed between profiles: {case["identity"]}') diff --git a/usvm-ts-calls/scripts/test_run_class_start_smoke.py b/usvm-ts-calls/scripts/test_run_class_start_smoke.py index 23d7961c18..aeaf6332c1 100644 --- a/usvm-ts-calls/scripts/test_run_class_start_smoke.py +++ b/usvm-ts-calls/scripts/test_run_class_start_smoke.py @@ -83,6 +83,8 @@ def test_durable_entry_survives_child_timeout(self): progress.update(initialStates=1, originalTargetStatementsEntered=1, targetStatementEntered=True, started=True) smoke.save(directory / 'progress.json', progress) + (directory / 'states.jsonl.gz').write_bytes(b'preserved-compressed-states') + (directory / 'expressions.jsonl.gz').write_bytes(b'preserved-compressed-values') result = smoke.child_result(directory, {'timedOut': True}, case, 'frozen') @@ -91,6 +93,8 @@ def test_durable_entry_survives_child_timeout(self): self.assertTrue(result['timedOut']) self.assertFalse(result['engineFailed']) self.assertEqual('STARTED_WITH_LIMITATION', result['startupStatus']) + self.assertEqual(str(directory / 'states.jsonl.gz'), result['durableStateSnapshotsPath']) + self.assertEqual(str(directory / 'expressions.jsonl.gz'), result['durableSymbolicExpressionsPath']) if __name__ == '__main__': diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt index bc3f18d801..21690c3dfe 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt @@ -45,10 +45,10 @@ internal data class CallsClassRawStateSnapshot( val statementIndex: Int, val statement: String, val callStack: List, - val constraints: List, + val constraintIds: List, val modelCount: Int, val resultKind: String, - val symbolicResult: String? = null, + val symbolicResultId: Long? = null, val unsupportedReason: String? = null, ) @@ -79,9 +79,8 @@ internal data class CallsClassRawAnalysis( val sourceMappedIrUniverse: List, val sourceMappedIrEntered: List, val statementUniverseSha256: String, - val terminalStateSnapshots: List, - val stoppedPrefixSnapshots: List, - val remainingStateSnapshots: List, + val stateSnapshots: CallsClassRawJournalMetadata, + val symbolicExpressions: CallsClassRawJournalMetadata, val proof: String = "Symbolic source-mapped IR entry only; " + "diagnostic state metadata is not a native replay witness", ) @@ -93,9 +92,7 @@ internal class ClassRawAnalysisObserver( private val output: Path, ) : UMachineObserver { private val entered = linkedSetOf() - private val terminal = mutableListOf() - private val stopped = mutableListOf() - private val remaining = mutableListOf() + private val snapshots = CallsClassRawSnapshotStore(output = output) private val snapshotFailures = mutableListOf() private val methodSteps = linkedMapOf() private val sourceKinds = linkedMapOf() @@ -150,19 +147,19 @@ internal class ClassRawAnalysisObserver( "OTHER_REACHABLE" } } - saveSnapshot(state = state, outcome = outcome, destination = terminal) + saveSnapshot(state = state, outcome = outcome) } fun recordStoppedPrefix(state: TsState, reason: String) { stoppedStates++ - saveSnapshot(state = state, outcome = "STOPPED_PREFIX: $reason", destination = stopped) + saveSnapshot(state = state, outcome = "STOPPED_PREFIX: $reason") } /** Drain only after analyzeWithMetadata has computed its real stop reason. */ fun retainRemainingStates(selector: UPathSelector?) { selector?.drain()?.forEach { state -> remainingStates++ - saveSnapshot(state = state, outcome = "SUSPENDED", destination = remaining) + saveSnapshot(state = state, outcome = "SUSPENDED") } } @@ -177,59 +174,49 @@ internal class ClassRawAnalysisObserver( if (event.elapsed > event.requested) quantumOverruns++ } - private fun saveSnapshot(state: TsState, outcome: String, destination: MutableList) { - val snapshot = runCatching { - val stmt = state.lastStmt - val result = state.methodResult - CallsClassRawStateSnapshot( - stateId = state.id.toString(), - outcome = outcome, - entryMethod = state.entrypoint.signature.toString(), - currentMethod = stmt.location.method.signature.toString(), - statementIndex = stmt.location.index, - statement = stmt.toString(), - callStack = state.callStack.map { it.method.signature.toString() }, - constraints = state.pathConstraints.constraintSequence().map { it.toString() }.toList(), - modelCount = state.models.size, - resultKind = result::class.java.simpleName, - symbolicResult = when (result) { - is TsMethodResult.Success -> result.value.toString() - is TsMethodResult.TsException -> result.value.toString() - else -> null - }, - unsupportedReason = state.unsupportedReason, - ) + private fun saveSnapshot(state: TsState, outcome: String) { + val saved = runCatching { + snapshots.append { reference -> + val stmt = state.lastStmt + val result = state.methodResult + CallsClassRawStateSnapshot( + stateId = state.id.toString(), + outcome = outcome, + entryMethod = state.entrypoint.signature.toString(), + currentMethod = stmt.location.method.signature.toString(), + statementIndex = stmt.location.index, + statement = stmt.toString(), + callStack = state.callStack.map { it.method.signature.toString() }, + constraintIds = state.pathConstraints.constraintSequence().map(reference).toList(), + modelCount = state.models.size, + resultKind = result::class.java.simpleName, + symbolicResultId = when (result) { + is TsMethodResult.Success -> reference(result.value) + is TsMethodResult.TsException -> reference(result.value) + else -> null + }, + unsupportedReason = state.unsupportedReason, + ) + } } - snapshot.fold( - onSuccess = { - destination += it - val saved = runCatching { - Files.writeString( - output.resolve("states.jsonl"), - encodeCallsArtifact(it) + "\n", - StandardOpenOption.CREATE, - StandardOpenOption.APPEND, - ) - } - saved.exceptionOrNull()?.let { failure -> - snapshotFailures += "${state.id}/$outcome: ${failure::class.java.name}: ${failure.message}" - } - }, - onFailure = { - val diagnostic = "${state.id}/$outcome: ${it::class.java.name}: ${it.message}" - snapshotFailures += diagnostic + saved.exceptionOrNull()?.let { failure -> + val diagnostic = "${state.id}/$outcome: ${failure::class.java.name}: ${failure.message}" + snapshotFailures += diagnostic + // A journal failure must remain visible even when this diagnostic write also fails. + runCatching { Files.writeString( output.resolve("state-snapshot-failures.jsonl"), encodeCallsArtifact(mapOf("failure" to diagnostic)) + "\n", StandardOpenOption.CREATE, StandardOpenOption.APPEND, ) - }, - ) + } + } } fun result(manifest: CallsClassStartManifest, analysisElapsedMillis: Long): CallsClassRawAnalysis { val encodedUniverse = encodeCallsArtifact(universe).toByteArray(Charsets.UTF_8) + val journals = snapshots.finish() return CallsClassRawAnalysis( budgetMillis = manifest.budgetMillis, analysisElapsedMillis = analysisElapsedMillis, @@ -256,9 +243,8 @@ internal class ClassRawAnalysisObserver( sourceMappedIrUniverse = universe, sourceMappedIrEntered = entered.toList(), statementUniverseSha256 = callsArtifactSha256(encodedUniverse), - terminalStateSnapshots = terminal, - stoppedPrefixSnapshots = stopped, - remainingStateSnapshots = remaining, + stateSnapshots = journals.first, + symbolicExpressions = journals.second, ) } diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStore.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStore.kt new file mode 100644 index 0000000000..9fea85996f --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStore.kt @@ -0,0 +1,140 @@ +package org.usvm.ts.calls + +import io.ksmt.expr.KExpr +import kotlinx.serialization.Serializable +import java.io.BufferedWriter +import java.io.FilterOutputStream +import java.nio.channels.Channels +import java.nio.channels.FileChannel +import java.nio.file.Files +import java.nio.file.Path +import java.nio.file.StandardOpenOption +import java.security.MessageDigest +import java.util.IdentityHashMap +import java.util.zip.GZIPOutputStream + +@Serializable +internal data class CallsClassRawJournalMetadata( + val path: String, + val records: Long, + val compressedBytes: Long, + val sha256: String, + val complete: Boolean, + val schemaVersion: Int = 2, + val format: String = "GZIP_JSONL_CONCATENATED_MEMBERS", +) + +@Serializable +internal data class CallsClassRawSymbolicExpression( + val id: Long, + val expressionKind: String, + val sort: String, + val diagnostic: String, +) + +/** + * Each expression diagnostic is rendered once, and every state keeps the complete ordered list of references. + * Neither the state snapshots nor their diagnostic strings accumulate in the final result or in memory. + */ +internal class CallsClassRawSnapshotStore(output: Path) { + private val expressions = IdentityHashMap, Long>() + private val expressionJournal = CallsClassRawGzipJournal(path = output.resolve("expressions.jsonl.gz")) + private val stateJournal = CallsClassRawGzipJournal(path = output.resolve("states.jsonl.gz")) + private var failed = false + + fun append(snapshot: ((KExpr<*>) -> Long) -> CallsClassRawStateSnapshot) { + check(!failed) { "A previous raw snapshot write failed; journals are incomplete" } + try { + var state: CallsClassRawStateSnapshot? = null + expressionJournal.appendBatch { writer -> + var added = 0L + state = snapshot { expression -> + val previous = expressions[expression] + if (previous != null) { + previous + } else { + val id = expressions.size.toLong() + val record = CallsClassRawSymbolicExpression( + id = id, + expressionKind = expression::class.java.name, + sort = expression.sort.toString(), + diagnostic = expression.toString(), + ) + writer.appendLine(encodeCallsArtifact(record)) + expressions[expression] = id + added++ + id + } + } + added + } + val saved = checkNotNull(state) + stateJournal.appendBatch { writer -> + writer.appendLine(encodeCallsArtifact(saved)) + 1L + } + } catch (failure: Throwable) { + failed = true + throw failure + } + } + + fun finish(): Pair { + // Closing both journals is necessary even when the first close fails. + val states = runCatching { stateJournal.finish(complete = !failed) } + val terms = runCatching { expressionJournal.finish(complete = !failed) } + return states.getOrThrow() to terms.getOrThrow() + } +} + +/** A completed, fsynced gzip member per state also preserves all earlier members after process termination. */ +internal class CallsClassRawGzipJournal(private val path: Path) { + private val output = FileChannel.open(path, StandardOpenOption.CREATE_NEW, StandardOpenOption.WRITE) + private var records = 0L + private var failed = false + private var closed = false + + init { + appendBatch { 0L } + } + + fun appendBatch(write: (BufferedWriter) -> Long) { + check(!closed && !failed) { "Raw journal is closed or incomplete" } + try { + val sink = object : FilterOutputStream(Channels.newOutputStream(output)) { + override fun close() = flush() + override fun write(bytes: ByteArray, offset: Int, length: Int) = out.write(bytes, offset, length) + } + val gzip = GZIPOutputStream(sink) + val added = gzip.bufferedWriter(Charsets.UTF_8).use { writer -> write(writer) } + output.force(true) + records += added + } catch (failure: Throwable) { + failed = true + throw failure + } + } + + fun finish(complete: Boolean): CallsClassRawJournalMetadata { + if (!closed) { + output.close() + closed = true + } + val digest = MessageDigest.getInstance("SHA-256") + Files.newInputStream(path).use { input -> + val buffer = ByteArray(DEFAULT_BUFFER_SIZE) + while (true) { + val count = input.read(buffer) + if (count < 0) break + digest.update(buffer, 0, count) + } + } + return CallsClassRawJournalMetadata( + path = path.fileName.toString(), + records = records, + compressedBytes = Files.size(path), + sha256 = digest.digest().joinToString(separator = "") { byte -> "%02x".format(byte.toInt() and 0xff) }, + complete = complete && !failed, + ) + } +} diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStoreTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStoreTest.kt new file mode 100644 index 0000000000..c914ea9da1 --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStoreTest.kt @@ -0,0 +1,123 @@ +package org.usvm.ts.calls + +import io.ksmt.KContext +import kotlinx.serialization.decodeFromString +import org.junit.jupiter.api.io.TempDir +import java.nio.file.Files +import java.nio.file.Path +import java.util.zip.GZIPInputStream +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertFailsWith +import kotlin.test.assertTrue + +class CallsClassRawSnapshotStoreTest { + @TempDir + lateinit var directory: Path + + @Test + fun `shared constraints preserve every state and symbolic value without repeated diagnostics`() { + KContext().use { context -> + val store = CallsClassRawSnapshotStore(output = directory) + val terms = List(2_674) { index -> + val name = "input-$index-${"nested-field-".repeat(n = 64)}" + context.mkConst(name = name, sort = context.boolSort) + } + val diagnosticBytes = terms.sumOf { it.toString().toByteArray().size } + + repeat(times = 547) { state -> + store.append { reference -> + snapshot( + stateId = state.toString(), + constraintIds = terms.map(reference), + symbolicResultId = reference(terms.first()), + ) + } + } + val (states, expressions) = store.finish() + + assertEquals(547L, states.records) + assertEquals(2_674L, expressions.records) + assertTrue(states.complete) + assertTrue(expressions.complete) + assertEquals(callsArtifactSha256(Files.readAllBytes(directory.resolve(states.path))), states.sha256) + assertEquals(callsArtifactSha256(Files.readAllBytes(directory.resolve(expressions.path))), expressions.sha256) + val restoredTerms = readJournal(expressions.path) + assertEquals(terms.map { it.toString() }, restoredTerms.map { it.diagnostic }) + val restoredStates = readJournal(states.path) + assertEquals(547, restoredStates.size) + restoredStates.forEachIndexed { index, state -> + assertEquals(index.toString(), state.stateId) + assertEquals((0L until 2_674L).toList(), state.constraintIds) + assertEquals(0L, state.symbolicResultId) + } + assertTrue(547L * diagnosticBytes > 1_000_000_000L) + assertTrue(expressions.compressedBytes < diagnosticBytes) + assertTrue(states.compressedBytes + expressions.compressedBytes < 547L * diagnosticBytes) + } + } + + @Test + fun `finished gzip members preserve earlier snapshots before final result exists`() { + val journal = CallsClassRawGzipJournal(path = directory.resolve("states.jsonl.gz")) + journal.appendBatch { writer -> + writer.appendLine(encodeCallsArtifact(mapOf("value" to "isolated-\uD800"))) + 1L + } + + val rows = readJournal>("states.jsonl.gz") + + assertEquals(listOf(mapOf("value" to "isolated-\uD800")), rows) + assertFalse(Files.exists(directory.resolve("result.json"))) + assertEquals(1L, journal.finish(complete = true).records) + } + + @Test + fun `partial snapshot failure marks both journals incomplete and rejects later references`() { + KContext().use { context -> + val store = CallsClassRawSnapshotStore(output = directory) + val term = context.mkConst(name = "surviving-expression", sort = context.boolSort) + store.append { reference -> snapshot(stateId = "first", constraintIds = listOf(reference(term))) } + + assertFailsWith { + store.append { reference -> + reference(term) + throw IllegalArgumentException("snapshot failed") + } + } + assertFailsWith { + store.append { snapshot(stateId = "never-committed", constraintIds = emptyList()) } + } + val (states, expressions) = store.finish() + + assertFalse(states.complete) + assertFalse(expressions.complete) + assertEquals(listOf("first"), readJournal(states.path).map { it.stateId }) + assertEquals(1L, expressions.records) + } + } + + private inline fun readJournal(path: String): List = + GZIPInputStream(Files.newInputStream(directory.resolve(path))).bufferedReader().use { reader -> + reader.lineSequence().map { CallsExperimentJson.json.decodeFromString(it) }.toList() + } + + private fun snapshot( + stateId: String, + constraintIds: List, + symbolicResultId: Long? = null, + ): CallsClassRawStateSnapshot = CallsClassRawStateSnapshot( + stateId = stateId, + outcome = "SUSPENDED", + entryMethod = "fixture.entry", + currentMethod = "fixture.current", + statementIndex = 0, + statement = "fixture statement", + callStack = listOf("fixture.entry", "fixture.current"), + constraintIds = constraintIds, + modelCount = 1, + resultKind = "Success", + symbolicResultId = symbolicResultId, + ) +} diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt index e9f1ae9462..a55db490f7 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt @@ -156,12 +156,14 @@ class CallsClassStartSmokeTest { assertEquals(30_000L, raw.budgetMillis) assertEquals(null, raw.collectedStatesLimit) assertTrue(raw.stoppedPrefixStates > 0) - assertEquals(raw.stoppedPrefixStates, raw.stoppedPrefixSnapshots.size.toLong()) + assertTrue(raw.stateSnapshots.records >= raw.stoppedPrefixStates) + assertTrue(raw.stateSnapshots.complete) + assertTrue(raw.symbolicExpressions.complete) assertTrue(raw.sourceMappedIrUniverse.isNotEmpty()) assertTrue(raw.sourceMappedIrEntered.isNotEmpty()) assertTrue(raw.sourceMappedIrUniverse.containsAll(raw.sourceMappedIrEntered)) assertTrue(raw.stateSnapshotFailures.isEmpty(), raw.stateSnapshotFailures.toString()) - assertTrue(Files.isRegularFile(directory.resolve("output/states.jsonl"))) + assertTrue(Files.isRegularFile(directory.resolve("output/states.jsonl.gz"))) } @Test From d7ff7725be9b93379dd3ad9005a1e62e355d2c1e Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 10:59:57 +0300 Subject: [PATCH 7/8] Keep startup IR enumeration compatible with Java 11 Consume the sorted file stream through a Kotlin sequence instead of Stream.toList(), which requires Java 16. Preserve relative-path ordering and hashes. --- .../main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt index b8d4e1daad..267aea925e 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt @@ -35,7 +35,9 @@ internal fun startupIrFingerprint(case: CallsClassStartCase): String { } internal fun startupIrFiles(root: Path): Map = Files.walk(root).use { paths -> - paths.filter { Files.isRegularFile(it) }.sorted().toList().associate { file -> + val regularFiles = paths.filter { Files.isRegularFile(it) }.sorted() + + regularFiles.iterator().asSequence().associate { file -> root.relativize(file).toString() to callsArtifactSha256(Files.readAllBytes(file)) } } From 81aced8678258e67e9e0dc130b3f3fa28cd77e81 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 16:57:51 +0300 Subject: [PATCH 8/8] Fix Detekt findings in raw class snapshot journals --- .../ts/calls/CallsClassRawSnapshotStore.kt | 20 +++++++++---------- .../calls/CallsClassRawSnapshotStoreTest.kt | 7 +++++-- 2 files changed, 14 insertions(+), 13 deletions(-) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStore.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStore.kt index 9fea85996f..e76fab4afc 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStore.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStore.kt @@ -44,7 +44,7 @@ internal class CallsClassRawSnapshotStore(output: Path) { fun append(snapshot: ((KExpr<*>) -> Long) -> CallsClassRawStateSnapshot) { check(!failed) { "A previous raw snapshot write failed; journals are incomplete" } - try { + runCatching { var state: CallsClassRawStateSnapshot? = null expressionJournal.appendBatch { writer -> var added = 0L @@ -73,10 +73,7 @@ internal class CallsClassRawSnapshotStore(output: Path) { writer.appendLine(encodeCallsArtifact(saved)) 1L } - } catch (failure: Throwable) { - failed = true - throw failure - } + }.onFailure { failed = true }.getOrThrow() } fun finish(): Pair { @@ -100,7 +97,7 @@ internal class CallsClassRawGzipJournal(private val path: Path) { fun appendBatch(write: (BufferedWriter) -> Long) { check(!closed && !failed) { "Raw journal is closed or incomplete" } - try { + runCatching { val sink = object : FilterOutputStream(Channels.newOutputStream(output)) { override fun close() = flush() override fun write(bytes: ByteArray, offset: Int, length: Int) = out.write(bytes, offset, length) @@ -109,10 +106,7 @@ internal class CallsClassRawGzipJournal(private val path: Path) { val added = gzip.bufferedWriter(Charsets.UTF_8).use { writer -> write(writer) } output.force(true) records += added - } catch (failure: Throwable) { - failed = true - throw failure - } + }.onFailure { failed = true }.getOrThrow() } fun finish(complete: Boolean): CallsClassRawJournalMetadata { @@ -133,8 +127,12 @@ internal class CallsClassRawGzipJournal(private val path: Path) { path = path.fileName.toString(), records = records, compressedBytes = Files.size(path), - sha256 = digest.digest().joinToString(separator = "") { byte -> "%02x".format(byte.toInt() and 0xff) }, + sha256 = digest.digest().joinToString(separator = "") { byte -> + "%02x".format(byte.toInt() and UNSIGNED_BYTE_MASK) + }, complete = complete && !failed, ) } } + +private const val UNSIGNED_BYTE_MASK = 0xff diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStoreTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStoreTest.kt index c914ea9da1..bfe96f919d 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStoreTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStoreTest.kt @@ -8,8 +8,8 @@ import java.nio.file.Path import java.util.zip.GZIPInputStream import kotlin.test.Test import kotlin.test.assertEquals -import kotlin.test.assertFalse import kotlin.test.assertFailsWith +import kotlin.test.assertFalse import kotlin.test.assertTrue class CallsClassRawSnapshotStoreTest { @@ -42,7 +42,10 @@ class CallsClassRawSnapshotStoreTest { assertTrue(states.complete) assertTrue(expressions.complete) assertEquals(callsArtifactSha256(Files.readAllBytes(directory.resolve(states.path))), states.sha256) - assertEquals(callsArtifactSha256(Files.readAllBytes(directory.resolve(expressions.path))), expressions.sha256) + assertEquals( + callsArtifactSha256(Files.readAllBytes(directory.resolve(expressions.path))), + expressions.sha256, + ) val restoredTerms = readJournal(expressions.path) assertEquals(terms.map { it.toString() }, restoredTerms.map { it.diagnostic }) val restoredStates = readJournal(states.path)