diff --git a/usvm-ts-calls/CLASS_START_SMOKE.md b/usvm-ts-calls/CLASS_START_SMOKE.md new file mode 100644 index 0000000000..731f17074c --- /dev/null +++ b/usvm-ts-calls/CLASS_START_SMOKE.md @@ -0,0 +1,123 @@ +# 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. 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`. + +`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 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 +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 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. + +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 new file mode 100644 index 0000000000..295a72353c --- /dev/null +++ b/usvm-ts-calls/scripts/run-class-start-smoke.py @@ -0,0 +1,244 @@ +#!/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')} + files['frontendOverrides'] = {name: os.environ.get(name) for name in ('ETS_FRONTEND_SCRIPT', 'ETS_FRONTEND_DIR')} + 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) + elif (child / 'unknown-calls.jsonl').exists(): + result['unknownCalls'] = [json.loads(line) for line in (child / 'unknown-calls.jsonl').read_text().splitlines()] + 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 + + +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) + 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) + 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 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()) + 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'] + 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), args.command, 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/run-class-symbolic-probe.py b/usvm-ts-calls/scripts/run-class-symbolic-probe.py new file mode 100644 index 0000000000..c47f4c4ea1 --- /dev/null +++ b/usvm-ts-calls/scripts/run-class-symbolic-probe.py @@ -0,0 +1,181 @@ +#!/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 +import zipfile + +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 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') + 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): + 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(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'), + '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"]}') + 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 = 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: + 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, + '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_start_smoke.py b/usvm-ts-calls/scripts/test_run_class_start_smoke.py new file mode 100644 index 0000000000..aeaf6332c1 --- /dev/null +++ b/usvm-ts-calls/scripts/test_run_class_start_smoke.py @@ -0,0 +1,101 @@ +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) + (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') + + self.assertTrue(result['started']) + self.assertFalse(result['qualifyingStarted']) + 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__': + unittest.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..e6c6097219 --- /dev/null +++ b/usvm-ts-calls/scripts/test_run_class_symbolic_probe.py @@ -0,0 +1,115 @@ +import importlib.util +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) +SPEC.loader.exec_module(probe) + + +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)] + 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 = {'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] + + 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_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) + 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..21690c3dfe --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt @@ -0,0 +1,265 @@ +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 constraintIds: List, + val modelCount: Int, + val resultKind: String, + val symbolicResultId: Long? = 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 sourceEnteredStatementKinds: Map, + val sourceMappedIrUniverse: List, + val sourceMappedIrEntered: List, + val statementUniverseSha256: String, + val stateSnapshots: CallsClassRawJournalMetadata, + val symbolicExpressions: CallsClassRawJournalMetadata, + 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 snapshots = CallsClassRawSnapshotStore(output = output) + 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 + 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) + sourceKinds.merge(stmt::class.java.simpleName, 1L, Long::plus) + } + + 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) + } + + fun recordStoppedPrefix(state: TsState, reason: String) { + stoppedStates++ + 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") + } + } + + 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) { + 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, + ) + } + } + 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, + 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, + sourceEnteredStatementKinds = sourceKinds, + sourceMappedIrUniverse = universe, + sourceMappedIrEntered = entered.toList(), + statementUniverseSha256 = callsArtifactSha256(encodedUniverse), + stateSnapshots = journals.first, + symbolicExpressions = journals.second, + ) + } + + 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/CallsClassRawSnapshotStore.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStore.kt new file mode 100644 index 0000000000..e76fab4afc --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStore.kt @@ -0,0 +1,138 @@ +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" } + runCatching { + 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 + } + }.onFailure { failed = true }.getOrThrow() + } + + 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" } + 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) + } + val gzip = GZIPOutputStream(sink) + val added = gzip.bufferedWriter(Charsets.UTF_8).use { writer -> write(writer) } + output.force(true) + records += added + }.onFailure { failed = true }.getOrThrow() + } + + 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 UNSIGNED_BYTE_MASK) + }, + complete = complete && !failed, + ) + } +} + +private const val UNSIGNED_BYTE_MASK = 0xff 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..267aea925e --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartIrCache.kt @@ -0,0 +1,91 @@ +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) + +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()) +} + +internal fun startupIrFiles(root: Path): Map = Files.walk(root).use { paths -> + val regularFiles = paths.filter { Files.isRegularFile(it) }.sorted() + + regularFiles.iterator().asSequence().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..548c40027b --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt @@ -0,0 +1,684 @@ +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 +import org.jacodb.ets.model.EtsClassCategory +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.ANONYMOUS_METHOD_PREFIX +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.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 + +@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 timeQuantumMillis: Long = 25, + 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) + 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, + 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 generatedInitialStates: Int = 0, + val generatedInitialMethodCount: Int = 0, + 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, + 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, + 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 = {}, + 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 + 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 + val generatedInitialStates: Int get() = initial.size + val generatedInitialMethodCount: Int get() = initialMethods.size + + 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 + 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. */ + override 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++ + originalEntryObserver(stmt) + 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 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) + } + + 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 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 = 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) + if (original) originalStepCallbacks++ + 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) = 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 && 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) + 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 targetDeclarations = emptyList() + var methods = emptyList() + var entryPoints = 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 + 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 declarations = scene.projectClasses.filter { owner -> + val file = owner.signature.file.fileName.replace('\\', '/') + owner.name == case.className && (file == case.sourceFile || file.endsWith("/${case.sourceFile}")) + } + 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)) + 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" } + 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, + sourceFile = case.sourceFile, + sourceText = sourceText, + output = output, + ) + } else { + null + } + rawObserver = raw + 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, + generatedInitialStates = current.generatedInitialStates, + generatedInitialMethodCount = current.generatedInitialMethodCount, + stageElapsedMillis = elapsed, + targetSignature = target.signature.toString(), + methodSignatures = methods.map { it.signature.toString() }, + firstOriginalStep = current.firstOriginalStep, + entryPointEligibility = entryPoints, + ) + writeCallsArtifactAtomically(output.resolve("progress.json"), encodeCallsArtifact(progress)) + }, + unknownCallObserver = { event -> + unknownCalls += event.toCallsClassUnknownCallEvent(eventIndex = unknownCalls.size + 1) + 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 = !exploratory, + ), + 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 = interpreterObserver, + machineObserverFactory = factory, + ).use { machine -> + checkpoint(next = "INITIAL_STATE") + val analysisStarted = TimeSource.Monotonic.markNow() + try { + outcome = machine.analyzeWithMetadata( + methods = independentMethods, + configureInitialState = { method, state -> + machineObserver.registerInitialState(method = method, state = state) + }, + ) + } finally { + analysisElapsedMillis = analysisStarted.elapsedNow().inWholeMilliseconds + raw?.retainRemainingStates(selector = remainingSelector) + } + } + 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 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, + 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, + generatedInitialStates = metrics?.generatedInitialStates ?: 0, + generatedInitialMethodCount = metrics?.generatedInitialMethodCount ?: 0, + 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}" + }, + 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)) +} + +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 d646403e69..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 @@ -10,6 +10,8 @@ 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)) @@ -104,6 +106,8 @@ internal fun frontendIdentity(args: List): String { 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/CallsClassRawSnapshotStoreTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStoreTest.kt new file mode 100644 index 0000000000..bfe96f919d --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassRawSnapshotStoreTest.kt @@ -0,0 +1,126 @@ +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.assertFailsWith +import kotlin.test.assertFalse +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 new file mode 100644 index 0000000000..a55db490f7 --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt @@ -0,0 +1,256 @@ +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) + } + + @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) + 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.gz"))) + } + + @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, + exploratory: Boolean = false, + ): 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, + 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, encodeClassStartManifest(manifest)) + val output = directory.resolve("output") + + 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"))) + } +} 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)