From 9b643b8e5030cf3d260b3296a8f635556a5a18ef Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 19 Sep 2026 13:27:30 +0300 Subject: [PATCH 01/10] Add reproducible TypeScript unknown-call census --- usvm-ts/build.gradle.kts | 9 + .../unknown-call-census/MODEL_SELECTION.md | 41 ++ .../experiments/unknown-call-census/README.md | 19 + .../development-corpus.json | 75 +++ .../usvm/census/UnknownCallCensusArtifacts.kt | 204 +++++++ .../org/usvm/census/UnknownCallCensusCli.kt | 121 ++++ .../usvm/census/UnknownCallCensusRunner.kt | 577 ++++++++++++++++++ .../census/UnknownCallCensusAggregatorTest.kt | 80 +++ 8 files changed, 1126 insertions(+) create mode 100644 usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md create mode 100644 usvm-ts/experiments/unknown-call-census/README.md create mode 100644 usvm-ts/experiments/unknown-call-census/development-corpus.json create mode 100644 usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusArtifacts.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusCli.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusAggregatorTest.kt diff --git a/usvm-ts/build.gradle.kts b/usvm-ts/build.gradle.kts index 96de26034a..396ad3082b 100644 --- a/usvm-ts/build.gradle.kts +++ b/usvm-ts/build.gradle.kts @@ -8,6 +8,7 @@ import kotlin.time.Duration plugins { id("usvm.kotlin-conventions") + kotlin("plugin.serialization") version Versions.kotlin } dependencies { @@ -21,6 +22,7 @@ dependencies { implementation(Libs.ksmt_cvc5) implementation(Libs.ksmt_symfpu) implementation(Libs.ksmt_runner) + implementation(Libs.kotlinx_serialization_json) testImplementation(Libs.mockk) testImplementation(Libs.junit_jupiter_params) @@ -32,6 +34,13 @@ dependencies { testImplementation("org.burningwave:core:12.62.7") } +tasks.register("runUnknownCallCensus") { + group = "verification" + description = "Runs or summarizes the TypeScript unknown-call census." + classpath = sourceSets.main.get().runtimeClasspath + mainClass.set("org.usvm.census.UnknownCallCensusCliKt") +} + val generateSdkIR by tasks.registering { group = "build" description = "Generates SDK IR using ArkAnalyzer." diff --git a/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md b/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md new file mode 100644 index 0000000000..60181d0f0e --- /dev/null +++ b/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md @@ -0,0 +1,41 @@ +# Finite development model selection + +Selection frozen on 2026-09-19 before any held-out TS Calls evaluation. This is a development decision for a small pilot, not evidence that the selected models improve coverage. + +## Evidence used + +- Approximation audit #368 at `303409613c30ea5dcdabc1f97ac8092d753765b1`, which audits current source `41961f7b66c30c8a2a7507c67a79396f495f4520` and historical source `3728ba45ab092422e2cb2e57ed6fe2377425b622`. +- The frozen development manifest in `development-corpus.json` and its primary `EMPTY_FRESH` census. The corrected local pilot attempted 79 functions from three pinned projects: 58 completed, 6 timed out, and 15 ended with a boundary tool error. It observed 813 repeated events at 41 stable sites in 23 containing functions. These counts are retained with the raw artifact and must be regenerated after transplanting the census onto the accepted integration head. +- Stable-site prevalence rather than repeated loop-event totals. The largest repeated groups were application callback or dispatch limitations: `BSTreeKV.compare` (390 events, 3 sites), iterator `next` (141 events, 2 sites), and `Array.isArray` (120 events, 1 site). Project-defined `Stack.pop` accounted for 18 events at 3 sites; it is not the built-in `Array.pop` target. No built-in `Array.shift` site was observed. + +The primary profile disables optional catalog models but leaves mandatory semantics and legacy pre-dispatch approximations unchanged. Therefore the census is an inventory of observed unknown-call decisions, not every approximate or unresolved call in the engine. Tool errors, timeouts, and omitted call-resolution candidate tails also limit prevalence interpretation. + +## Decision + +The finite modeled set is exactly: + +```text +ts.array.pop +ts.array.shift +``` + +The control set is empty. Both existing models were implemented before this census and are retained as the bounded EtsIR-body and symbolic-memory-intrinsic mechanism pair from #368. They must not be described as census-selected. Their common experiment domain is the narrow dense, ordinary, mutable one-dimensional array domain in the #368 audit. Calls outside that admitted domain remain residual. + +No new model family is admitted for the pilot: + +- `BSTreeKV.compare` and the project `Stack` methods require application-call/callback resolution shared by every profile, not optional treatment models. +- Iterator `next` needs stateful iterator representation and completion/alias validation. +- `Array.isArray` has one stable development site and still needs proven target provenance plus rank/proxy bounds. +- The remaining scattered standard calls do not establish both prevalence and a reviewed bounded semantic contract. + +This is an acceptable no-new-family result. A later family requires a separate bounded implementation task, original-JavaScript validation, and a refrozen model set before held-out outcomes are inspected. + +## Content identity + +At audited source `41961f7b66c30c8a2a7507c67a79396f495f4520`: + +- `ArrayModels.ts` source SHA-256: `9f40d3abce58e3412a0206eabd9fdb0547e12c2ebd832ce48b260b3339518e26`. +- `TsArrayShiftIntrinsicModel.kt` SHA-256: `ff6dd634cf660c83e203b82c927a28e88859f0bc6b9f24bec2fa97d738dc9e11`. +- Empty catalog fingerprint: `e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855`. + +Recompute the source hashes on the accepted #380/integration head and record the exact engine commit/tree, built JAR hashes, JacoDB `ddb127d9ef`, native frontend, solver, Node and options. The catalog fingerprint identifies only the sorted ID set. `ts.array.shift` has no EtsIR artifact. For `ts.array.pop`, record the generated `etsIrHash` from the actual accepted runtime load when the downstream harness exposes it; until then it is explicitly unavailable rather than invented. diff --git a/usvm-ts/experiments/unknown-call-census/README.md b/usvm-ts/experiments/unknown-call-census/README.md new file mode 100644 index 0000000000..4521b8acac --- /dev/null +++ b/usvm-ts/experiments/unknown-call-census/README.md @@ -0,0 +1,19 @@ +# TypeScript unknown-call development census + +This census measures unknown-call events on a frozen development corpus. The projects and revisions were selected before current measurements and come from the historical TypeScript experiment corpus. They are development evidence and must not be reused as held-out evaluation projects. The manifest admits only `.ts` sources, excludes declarations and common test suffixes, excludes synthetic anonymous and initializer entry methods, sorts stable repository-relative file/function identities, and takes the bounded prefix recorded in `limits`. Unknown calls reached inside nested source functions retain their actual containing-function identity. + +The primary profile disables every optional unknown-call model and uses `FRESH_SYMBOLIC_RETURN`. Mandatory engine semantics and the legacy approximations that run before unknown-call dispatch remain enabled and identical across profiles. Therefore this census measures observed unknown-call decisions, not every call handled approximately by the engine. The raw artifact keeps every repeated event, while the summary separately deduplicates containing functions and stable source sites. Existing `ts.array.shift` and `ts.array.pop` models validate the mechanism but are not described as census-selected. + +Prepare each repository below `CHECKOUT_ROOT` at the exact revision recorded in `development-corpus.json`, then run: + +```sh +./gradlew :usvm-ts:runUnknownCallCensus --args='census --manifest usvm-ts/experiments/unknown-call-census/development-corpus.json --checkout-root /absolute/path/to/checkouts --output /absolute/path/to/results' +``` + +The command refuses a checkout whose Git `HEAD` differs from the manifest. It writes `raw.jsonl` incrementally and creates `summary.json`. Regenerate the summary without rerunning symbolic execution using: + +```sh +./gradlew :usvm-ts:runUnknownCallCensus --args='summarize --input /absolute/path/to/results/raw.jsonl --output /absolute/path/to/results/summary.json' +``` + +`EMPTY_STOP` can be added as a separate profile when stopping-site counts are needed. Do not combine its counts with the primary `EMPTY_FRESH` profile. diff --git a/usvm-ts/experiments/unknown-call-census/development-corpus.json b/usvm-ts/experiments/unknown-call-census/development-corpus.json new file mode 100644 index 0000000000..bae98e588e --- /dev/null +++ b/usvm-ts/experiments/unknown-call-census/development-corpus.json @@ -0,0 +1,75 @@ +{ + "schemaVersion": 1, + "projects": [ + { + "id": "the-algorithms-typescript", + "repository": "https://github.com/TheAlgorithms/TypeScript.git", + "revision": "19b4ced86c99815f142d4a46a028f55487b8038a", + "path": "TheAlgorithms-TypeScript", + "license": "MIT", + "licenseFile": "LICENSE", + "include": [ + "maths", + "search", + "sorts", + "bit_manipulation", + "dynamic_programming" + ], + "includeSuffixes": [ + ".ts" + ], + "excludeSuffixes": [ + ".test.ts", + ".spec.ts", + ".d.ts" + ] + }, + { + "id": "javascript-datastructures-algorithms", + "repository": "https://github.com/loiane/javascript-datastructures-algorithms.git", + "revision": "e8ee8f9b8a07589533c4243a210d4cea7b090b10", + "path": "javascript-datastructures-algorithms", + "license": "MIT", + "licenseFile": "LICENSE", + "include": [ + "src" + ], + "includeSuffixes": [ + ".ts" + ], + "excludeSuffixes": [ + ".test.ts", + ".spec.ts", + ".d.ts" + ] + }, + { + "id": "typescript-collections", + "repository": "https://github.com/basarat/typescript-collections.git", + "revision": "309bb1b6955b403b212309531607b8d17df152e5", + "path": "typescript-collections", + "license": "MIT", + "licenseFile": "LICENSE", + "include": [ + "src/lib" + ], + "includeSuffixes": [ + ".ts" + ], + "excludeSuffixes": [ + ".test.ts", + ".spec.ts", + ".d.ts" + ] + } + ], + "profiles": [ + "EMPTY_FRESH" + ], + "limits": { + "projectTimeoutSeconds": 300, + "methodTimeoutSeconds": 5, + "maxFiles": 20, + "maxMethods": 40 + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusArtifacts.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusArtifacts.kt new file mode 100644 index 0000000000..fb6371182b --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusArtifacts.kt @@ -0,0 +1,204 @@ +package org.usvm.census + +import kotlinx.serialization.Serializable +import kotlinx.serialization.json.Json +import kotlinx.serialization.json.JsonObject +import kotlinx.serialization.json.contentOrNull +import kotlinx.serialization.json.jsonPrimitive + +internal const val CENSUS_SCHEMA_VERSION = 1 + +internal val censusJson = Json { + encodeDefaults = true + ignoreUnknownKeys = true + prettyPrint = true +} + +@Serializable +internal data class UnknownCallCensusManifest( + val schemaVersion: Int, + val projects: List, + val profiles: List = listOf(UnknownCallCensusProfile.EMPTY_FRESH), + val limits: UnknownCallCensusLimits = UnknownCallCensusLimits(), +) + +@Serializable +internal data class UnknownCallCensusProject( + val id: String, + val repository: String, + val revision: String, + val path: String, + val license: String, + val licenseFile: String, + val include: List = emptyList(), + val includeSuffixes: List = listOf(".ts"), + val excludeSuffixes: List = listOf(".test.ts", ".spec.ts", ".d.ts"), +) + +@Serializable +internal enum class UnknownCallCensusProfile { + EMPTY_FRESH, + EMPTY_STOP, +} + +@Serializable +internal data class UnknownCallCensusLimits( + val projectTimeoutSeconds: Long = 300, + val methodTimeoutSeconds: Long = 10, + val maxFiles: Int = 100, + val maxMethods: Int = 1_000, +) + +@Serializable +internal data class UnknownCallCensusSummary( + val schemaVersion: Int = CENSUS_SCHEMA_VERSION, + val profiles: Map, +) + +@Serializable +internal data class UnknownCallCensusProfileSummary( + val projects: Int, + val functionsAnalyzed: Int, + val functionsCompleted: Int, + val functionsWithUnknownCalls: Int, + val uniqueSites: Int, + val rawEvents: Int, + val eventsByFailureReason: Map, + val eventsByDecision: Map, + val eventsByCallee: Map, + val uniqueSitesByCallee: Map, + val timeouts: List, + val errors: List, +) + +@Serializable +internal data class UnknownCallCensusIssue( + val projectId: String, + val functionId: String? = null, + val message: String? = null, +) + +internal object UnknownCallCensusAggregator { + fun summarize(lines: Sequence): UnknownCallCensusSummary { + val profiles = linkedMapOf() + + lines.filter(String::isNotBlank).forEachIndexed { index, line -> + val record = censusJson.parseToJsonElement(line) as? JsonObject + ?: error("Raw census record ${index + 1} is not a JSON object") + val kind = record.requiredString("kind", index) + if (kind == "run_start" || kind == "run_result") { + return@forEachIndexed + } + + val profile = record.requiredString("profile", index) + val accumulator = profiles.getOrPut(profile, ::ProfileAccumulator) + + when (kind) { + "unknown_call" -> accumulator.addUnknownCall(record, index) + "method_result" -> accumulator.addMethodResult(record, index) + "project_result" -> accumulator.addProjectResult(record, index) + else -> error("Raw census record ${index + 1} has unknown kind '$kind'") + } + } + + val summaries = profiles.toSortedMap().mapValues { (_, accumulator) -> accumulator.toSummary() } + return UnknownCallCensusSummary(profiles = summaries) + } +} + +private class ProfileAccumulator { + private val projects = hashSetOf() + private val functions = hashSetOf() + private val completedFunctions = hashSetOf() + private val functionsWithUnknownCalls = hashSetOf() + private val sites = hashSetOf() + private var rawEvents = 0 + private val eventsByFailureReason = hashMapOf() + private val eventsByDecision = hashMapOf() + private val eventsByCallee = hashMapOf() + private val sitesByCallee = hashMapOf>() + private val timeouts = mutableListOf() + private val errors = mutableListOf() + + fun addUnknownCall(record: JsonObject, index: Int) { + val projectId = record.requiredString("projectId", index) + val functionId = record.requiredString("functionId", index) + val siteId = record.requiredString("siteId", index) + val calleeId = record.requiredString("calleeId", index) + val failureReason = record.requiredString("failureReason", index) + val decision = record.requiredString("decision", index) + + projects += projectId + functionsWithUnknownCalls += functionId + sites += siteId + rawEvents++ + eventsByFailureReason.increment(failureReason) + eventsByDecision.increment(decision) + eventsByCallee.increment(calleeId) + sitesByCallee.getOrPut(calleeId, ::hashSetOf).add(siteId) + } + + fun addMethodResult(record: JsonObject, index: Int) { + val projectId = record.requiredString("projectId", index) + val functionId = record.requiredString("functionId", index) + val status = record.requiredString("status", index) + val issue = UnknownCallCensusIssue( + projectId = projectId, + functionId = functionId, + message = record.optionalString("error"), + ) + + projects += projectId + functions += functionId + when (status) { + "completed" -> completedFunctions += functionId + "timeout" -> timeouts += issue + "tool_error" -> errors += issue + } + } + + fun addProjectResult(record: JsonObject, index: Int) { + val projectId = record.requiredString("projectId", index) + val status = record.requiredString("status", index) + val issue = UnknownCallCensusIssue( + projectId = projectId, + message = record.optionalString("error"), + ) + + projects += projectId + when (status) { + "timeout" -> timeouts += issue + "tool_error" -> errors += issue + } + } + + fun toSummary(): UnknownCallCensusProfileSummary = UnknownCallCensusProfileSummary( + projects = projects.size, + functionsAnalyzed = functions.size, + functionsCompleted = completedFunctions.size, + functionsWithUnknownCalls = functionsWithUnknownCalls.size, + uniqueSites = sites.size, + rawEvents = rawEvents, + eventsByFailureReason = eventsByFailureReason.toSortedMap(), + eventsByDecision = eventsByDecision.toSortedMap(), + eventsByCallee = eventsByCallee.toSortedMap(), + uniqueSitesByCallee = sitesByCallee.toSortedMap().mapValues { (_, sites) -> sites.size }, + timeouts = timeouts.sortedWith(issueComparator), + errors = errors.sortedWith(issueComparator), + ) +} + +private val issueComparator = compareBy( + UnknownCallCensusIssue::projectId, + { it.functionId.orEmpty() }, + { it.message.orEmpty() }, +) + +private fun MutableMap.increment(key: String) { + this[key] = getOrDefault(key, defaultValue = 0) + 1 +} + +private fun JsonObject.requiredString(name: String, recordIndex: Int): String = + optionalString(name) ?: error("Raw census record ${recordIndex + 1} has no string '$name'") + +private fun JsonObject.optionalString(name: String): String? = get(name)?.jsonPrimitive?.contentOrNull diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusCli.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusCli.kt new file mode 100644 index 0000000000..8ef9f469f0 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusCli.kt @@ -0,0 +1,121 @@ +package org.usvm.census + +import kotlinx.serialization.SerializationException +import kotlinx.serialization.decodeFromString +import kotlinx.serialization.encodeToString +import java.nio.charset.StandardCharsets +import java.nio.file.Files +import java.nio.file.Path +import kotlin.system.exitProcess + +internal class UnknownCallCensusCli( + private val output: Appendable = System.out, + private val errors: Appendable = System.err, +) { + @Suppress("TooGenericExceptionCaught") + fun run(args: Array): Int = try { + when (args.firstOrNull()) { + "census" -> runCensus(parseOptions(args.drop(1), CENSUS_OPTIONS)) + "summarize" -> runSummarize(parseOptions(args.drop(1), SUMMARY_OPTIONS)) + "--help", "-h", null -> { + output.appendLine(usage()) + EXIT_SUCCESS + } + + else -> cliError("Unknown command '${args.first()}'") + } + } catch (error: CensusCliException) { + errors.appendLine("unknown-call-census: ${error.message}") + errors.appendLine("Run with --help for usage.") + EXIT_ERROR + } catch (error: SerializationException) { + errors.appendLine("unknown-call-census: invalid JSON: ${error.message}") + EXIT_ERROR + } catch (error: Exception) { + errors.appendLine("unknown-call-census: ${error.message ?: error::class.simpleName}") + EXIT_ERROR + } + + private fun runCensus(options: Map): Int { + val manifestPath = options.requiredPath("--manifest") + val checkoutRoot = options.requiredPath("--checkout-root") + val outputDirectory = options.requiredPath("--output") + val manifest = censusJson.decodeFromString( + Files.readString(manifestPath, StandardCharsets.UTF_8) + ) + val summary = UnknownCallCensusRunner( + manifest = manifest, + manifestPath = manifestPath, + checkoutRoot = checkoutRoot, + outputDirectory = outputDirectory, + ).run() + + output.appendLine(censusJson.encodeToString(summary)) + return EXIT_SUCCESS + } + + private fun runSummarize(options: Map): Int { + val input = options.requiredPath("--input") + val outputPath = options.requiredPath("--output") + val summary = Files.newBufferedReader(input, StandardCharsets.UTF_8).useLines { lines -> + UnknownCallCensusAggregator.summarize(lines) + } + outputPath.parent?.let(Files::createDirectories) + Files.writeString( + outputPath, + censusJson.encodeToString(summary) + System.lineSeparator(), + StandardCharsets.UTF_8, + ) + output.appendLine(censusJson.encodeToString(summary)) + + return EXIT_SUCCESS + } + + private fun parseOptions(args: List, allowedOptions: Set): Map { + val parsed = linkedMapOf() + var index = 0 + while (index < args.size) { + val option = args[index] + if (option !in allowedOptions) { + cliError("Unknown option '$option'") + } + if (index + 1 >= args.size) { + cliError("Missing value for '$option'") + } + if (parsed.put(option, args[index + 1]) != null) { + cliError("Option '$option' was specified more than once") + } + index += 2 + } + + return parsed + } + + private fun usage(): String = """ + Usage: + unknown-call-census census --manifest --checkout-root --output + unknown-call-census summarize --input --output + + The census command validates pinned Git revisions, writes append-only raw.jsonl records, + and regenerates summary.json. The summarize command deterministically rebuilds a summary + from an existing raw artifact. + """.trimIndent() + + private companion object { + val CENSUS_OPTIONS = setOf("--manifest", "--checkout-root", "--output") + val SUMMARY_OPTIONS = setOf("--input", "--output") + const val EXIT_SUCCESS = 0 + const val EXIT_ERROR = 1 + } +} + +private class CensusCliException(message: String) : IllegalArgumentException(message) + +private fun cliError(message: String): Nothing = throw CensusCliException(message) + +private fun Map.requiredPath(option: String): Path = + get(option)?.let(Path::of) ?: cliError("Missing required option '$option'") + +fun main(args: Array) { + exitProcess(UnknownCallCensusCli().run(args)) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt new file mode 100644 index 0000000000..eb10f41e50 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt @@ -0,0 +1,577 @@ +package org.usvm.census + +import kotlinx.serialization.encodeToString +import kotlinx.serialization.json.JsonObject +import kotlinx.serialization.json.buildJsonObject +import kotlinx.serialization.json.put +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsSourceSpan +import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME +import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME +import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.call.TsBuiltInUnknownCallModels +import org.usvm.machine.call.TsResidualCallPolicy +import org.usvm.machine.call.TsUnknownCallDecision +import org.usvm.machine.call.TsUnknownCallEvent +import org.usvm.machine.call.TsUnknownCallModelSelection +import java.io.BufferedWriter +import java.nio.charset.StandardCharsets +import java.nio.file.Files +import java.nio.file.Path +import java.nio.file.StandardOpenOption +import java.security.MessageDigest +import java.time.Instant +import kotlin.io.path.absolute +import kotlin.io.path.createDirectories +import kotlin.io.path.exists +import kotlin.io.path.isDirectory +import kotlin.io.path.name +import kotlin.io.path.pathString +import kotlin.time.Duration.Companion.seconds +import kotlin.time.TimeSource + +internal class UnknownCallCensusRunner( + private val manifest: UnknownCallCensusManifest, + private val manifestPath: Path, + private val checkoutRoot: Path, + private val outputDirectory: Path, +) { + fun run(): UnknownCallCensusSummary { + validateManifest() + outputDirectory.createDirectories() + val rawOutput = outputDirectory.resolve(RAW_FILE_NAME) + + CensusRecordWriter(rawOutput).use { writer -> + val startedAt = Instant.now() + writer.write(runStartRecord(startedAt)) + + manifest.profiles.forEach { profile -> + manifest.projects.forEach { project -> runProject(project, profile, writer) } + } + + writer.write( + buildJsonObject { + put("kind", "run_result") + put("schemaVersion", CENSUS_SCHEMA_VERSION) + put("startedAt", startedAt.toString()) + put("finishedAt", Instant.now().toString()) + put("status", "completed") + } + ) + } + + val summary = Files.newBufferedReader(rawOutput, StandardCharsets.UTF_8).useLines { lines -> + UnknownCallCensusAggregator.summarize(lines) + } + Files.writeString( + outputDirectory.resolve(SUMMARY_FILE_NAME), + censusJson.encodeToString(summary) + System.lineSeparator(), + StandardCharsets.UTF_8, + ) + + return summary + } + + @Suppress("TooGenericExceptionCaught") + private fun runProject( + project: UnknownCallCensusProject, + profile: UnknownCallCensusProfile, + writer: CensusRecordWriter, + ) { + val projectStart = TimeSource.Monotonic.markNow() + val normalizedCheckoutRoot = checkoutRoot.normalize().absolute() + val projectRoot = normalizedCheckoutRoot.resolve(project.path).normalize() + + try { + require(projectRoot.startsWith(normalizedCheckoutRoot)) { + "Project checkout escapes the configured checkout root: $projectRoot" + } + require(projectRoot.isDirectory()) { "Project checkout does not exist: $projectRoot" } + val licenseFile = projectRoot.resolve(project.licenseFile).normalize() + require(licenseFile.startsWith(projectRoot)) { "Project license file escapes its checkout: $licenseFile" } + require(licenseFile.exists()) { + "Project license file does not exist: ${project.licenseFile}" + } + validateRevision(projectRoot, project.revision) + + val loadedFiles = loadProjectFiles(project, projectRoot) + val files = selectFiles(project, loadedFiles) + val scene = EtsScene( + projectFiles = files, + projectName = project.id, + ) + val methods = scene.projectClasses + .flatMap { it.methods } + .filterNot { it.cfg.stmts.isEmpty() } + .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) } + .filterNot { it.name == DEFAULT_FILE_METHOD_NAME } + .filterNot { it.name == INSTANCE_INIT_METHOD_NAME } + .filterNot { it.name == STATIC_INIT_METHOD_NAME } + .sortedBy { functionId(project.id, projectRoot, it.signature, loadedFiles.pathsBySignature) } + .take(manifest.limits.maxMethods) + + var rawEvents = 0 + var completedMethods = 0 + var timedOutMethods = 0 + var failedMethods = 0 + var projectTimedOut = false + + for (method in methods) { + if (projectStart.elapsedNow() >= manifest.limits.projectTimeoutSeconds.seconds) { + projectTimedOut = true + break + } + + val result = runMethod( + project = project, + projectRoot = projectRoot, + scene = scene, + method = method, + profile = profile, + pathsBySignature = loadedFiles.pathsBySignature, + writer = writer, + ) + rawEvents += result.events + when (result.status) { + MethodStatus.COMPLETED -> completedMethods++ + MethodStatus.TIMEOUT -> timedOutMethods++ + MethodStatus.TOOL_ERROR -> failedMethods++ + } + } + + writer.write( + buildJsonObject { + putCommonProjectFields(project, profile) + put("kind", "project_result") + put("status", if (projectTimedOut) "timeout" else "completed") + put("filesSelected", files.size) + put("methodsSelected", methods.size) + put("methodsCompleted", completedMethods) + put("methodsTimedOut", timedOutMethods) + put("methodsFailed", failedMethods) + put("rawEvents", rawEvents) + put("durationMillis", projectStart.elapsedNow().inWholeMilliseconds) + if (projectTimedOut) { + put("error", "Project timeout reached before all selected methods were analyzed") + } + } + ) + } catch (error: Exception) { + writer.write( + buildJsonObject { + putCommonProjectFields(project, profile) + put("kind", "project_result") + put("status", "tool_error") + put("durationMillis", projectStart.elapsedNow().inWholeMilliseconds) + put("error", boundedError(error)) + } + ) + } + } + + @Suppress("TooGenericExceptionCaught") + private fun runMethod( + project: UnknownCallCensusProject, + projectRoot: Path, + scene: EtsScene, + method: EtsMethod, + profile: UnknownCallCensusProfile, + pathsBySignature: Map, + writer: CensusRecordWriter, + ): MethodRunResult { + val entryFunctionId = functionId(project.id, projectRoot, method.signature, pathsBySignature) + val observer = RecordingCensusObserver( + project = project, + projectRoot = projectRoot, + profile = profile, + entryFunctionId = entryFunctionId, + pathsBySignature = pathsBySignature, + writer = writer, + ) + val methodTimeout = manifest.limits.methodTimeoutSeconds.seconds + val machineOptions = UMachineOptions( + randomSeed = 0, + timeout = methodTimeout, + solverType = SolverType.YICES, + ) + val emptyModelSelection = TsUnknownCallModelSelection.Only(emptySet()) + val tsOptions = TsOptions( + unknownCallModelSelection = emptyModelSelection, + unknownCallFallback = profile.fallback, + ) + + val analysisStart = TimeSource.Monotonic.markNow() + var status = MethodStatus.COMPLETED + var errorText: String? = null + + try { + TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + observer = observer, + ).use { machine -> + machine.analyze(methods = listOf(method)) + } + + if (analysisStart.elapsedNow() >= methodTimeout) { + status = MethodStatus.TIMEOUT + errorText = "Machine timeout reached" + } + } catch (error: Exception) { + status = MethodStatus.TOOL_ERROR + errorText = boundedError(error) + } + + writer.write( + buildJsonObject { + putCommonProjectFields(project, profile) + put("kind", "method_result") + put("functionId", entryFunctionId) + put("status", status.serializedName) + put("durationMillis", analysisStart.elapsedNow().inWholeMilliseconds) + put("rawEvents", observer.eventCount) + errorText?.let { put("error", it) } + } + ) + + return MethodRunResult(status = status, events = observer.eventCount) + } + + private fun selectFiles( + project: UnknownCallCensusProject, + loadedFiles: LoadedProjectFiles, + ): List = loadedFiles.files.asSequence() + .map { file -> file to requireNotNull(loadedFiles.pathsBySignature[file.signature]) } + .filter { (_, fileName) -> project.includeSuffixes.any(fileName::endsWith) } + .filterNot { (_, fileName) -> project.excludeSuffixes.any(fileName::endsWith) } + .distinctBy { (_, fileName) -> fileName } + .sortedBy { (_, fileName) -> fileName } + .take(manifest.limits.maxFiles) + .map { (file, _) -> file } + .toList() + + private fun loadProjectFiles(project: UnknownCallCensusProject, projectRoot: Path): LoadedProjectFiles { + val sourceRoots = project.include.ifEmpty { listOf("") } + val files = mutableListOf() + val pathsBySignature = hashMapOf() + + sourceRoots.forEach { relativePath -> + val sourceRoot = projectRoot.resolve(relativePath).normalize() + require(sourceRoot.startsWith(projectRoot)) { "Configured source root escapes project checkout: $sourceRoot" } + require(sourceRoot.isDirectory()) { "Configured source root does not exist: $sourceRoot" } + val loadedFiles = loadEtsProjectAutoConvert( + sourceRoot, + provider = EtsIrProvider.TS_FRONTEND, + ).projectFiles + + loadedFiles.forEach { file -> + val sourcePath = repositoryRelativeSourcePath( + rawPath = file.signature.fileName, + sourceRoot = sourceRoot, + sourceRootRelativePath = relativePath, + projectRoot = projectRoot, + ) + val previousPath = pathsBySignature.put(file.signature, sourcePath) + require(previousPath == null || previousPath == sourcePath) { + "Conflicting source paths for ${file.signature}: $previousPath and $sourcePath" + } + } + files += loadedFiles + } + + return LoadedProjectFiles(files = files, pathsBySignature = pathsBySignature) + } + + private fun validateManifest() { + require(manifest.schemaVersion == CENSUS_SCHEMA_VERSION) { + "Unsupported census manifest schema ${manifest.schemaVersion}" + } + require(manifest.projects.isNotEmpty()) { "Census manifest must contain at least one project" } + require(manifest.profiles.isNotEmpty()) { "Census manifest must contain at least one profile" } + require(manifest.projects.map { it.id }.distinct().size == manifest.projects.size) { + "Census project IDs must be unique" + } + require(manifest.profiles.distinct().size == manifest.profiles.size) { + "Census profiles must be unique" + } + require(manifest.limits.projectTimeoutSeconds > 0) { "Project timeout must be positive" } + require(manifest.limits.methodTimeoutSeconds > 0) { "Method timeout must be positive" } + require(manifest.limits.maxFiles > 0) { "File limit must be positive" } + require(manifest.limits.maxMethods > 0) { "Method limit must be positive" } + val fullGitRevision = Regex("[0-9a-fA-F]{40}") + manifest.projects.forEach { project -> + require(project.id.isNotBlank()) { "Census project ID must not be blank" } + require(project.repository.isNotBlank()) { "Census project repository must not be blank" } + require(project.revision.matches(fullGitRevision)) { + "Project ${project.id} must use a full 40-character Git revision" + } + require(project.path.isNotBlank()) { "Project ${project.id} checkout path must not be blank" } + require(!Path.of(project.path).isAbsolute) { "Project ${project.id} checkout path must be relative" } + require(project.license.isNotBlank()) { "Project ${project.id} license must not be blank" } + require(project.licenseFile.isNotBlank()) { "Project ${project.id} license file must not be blank" } + require(!Path.of(project.licenseFile).isAbsolute) { + "Project ${project.id} license file must be relative" + } + require(project.include.none(String::isBlank)) { "Project ${project.id} source roots must not be blank" } + require(project.includeSuffixes.isNotEmpty() && project.includeSuffixes.none(String::isBlank)) { + "Project ${project.id} included source suffixes must not be empty or blank" + } + } + } + + private fun runStartRecord(startedAt: Instant): JsonObject = buildJsonObject { + val emptyModelSelection = TsUnknownCallModelSelection.Only(emptySet()) + val emptyCatalogFingerprint = TsBuiltInUnknownCallModels.catalog(emptyModelSelection).fingerprint + + put("kind", "run_start") + put("schemaVersion", CENSUS_SCHEMA_VERSION) + put("startedAt", startedAt.toString()) + put("manifestSha256", sha256(Files.readAllBytes(manifestPath))) + put("toolRevision", gitObject(Path.of("."), ref = "HEAD") ?: "unknown") + put("toolTree", gitObject(Path.of("."), ref = "HEAD^{tree}") ?: "unknown") + put("jacodbArtifact", runtimeArtifactName(EtsScene::class.java)) + put("frontendProvider", EtsIrProvider.TS_FRONTEND.name) + put("solver", SolverType.YICES.name) + put("javaVersion", System.getProperty("java.version")) + put("randomSeed", 0) + put("unknownCallModelSelection", "NONE") + put("unknownCallModelCatalogFingerprint", emptyCatalogFingerprint) + put("legacyApproximationPolicy", "UNCHANGED") + put("projectTimeoutSeconds", manifest.limits.projectTimeoutSeconds) + put("methodTimeoutSeconds", manifest.limits.methodTimeoutSeconds) + put("maxFiles", manifest.limits.maxFiles) + put("maxMethods", manifest.limits.maxMethods) + } + + private fun validateRevision(projectRoot: Path, expectedRevision: String) { + val actualRevision = gitObject(projectRoot, ref = "HEAD") + ?: error("Cannot read Git revision for project checkout $projectRoot") + require(actualRevision.equals(expectedRevision, ignoreCase = true)) { + "Project checkout $projectRoot is at $actualRevision, expected $expectedRevision" + } + } + + private fun gitObject(directory: Path, ref: String): String? = runCatching { + val process = ProcessBuilder("git", "-C", directory.pathString, "rev-parse", ref) + .redirectErrorStream(true) + .start() + val output = process.inputStream.bufferedReader().use { it.readText() }.trim() + if (process.waitFor() == 0) output else null + }.getOrNull() + + private fun sha256(bytes: ByteArray): String = MessageDigest.getInstance("SHA-256") + .digest(bytes) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + + private companion object { + const val RAW_FILE_NAME = "raw.jsonl" + const val SUMMARY_FILE_NAME = "summary.json" + } +} + +private fun runtimeArtifactName(type: Class<*>): String = runCatching { + Path.of(type.protectionDomain.codeSource.location.toURI()).name +}.getOrDefault("unknown") + +private class RecordingCensusObserver( + private val project: UnknownCallCensusProject, + private val projectRoot: Path, + private val profile: UnknownCallCensusProfile, + private val entryFunctionId: String, + private val pathsBySignature: Map, + private val writer: CensusRecordWriter, +) : TsInterpreterObserver { + var eventCount: Int = 0 + private set + + override fun onUnknownCall(event: TsUnknownCallEvent) { + eventCount++ + val containingSignature = event.callSite.location.method.signature + val functionId = functionId(project.id, projectRoot, containingSignature, pathsBySignature) + val sourceSpan = event.callSite.location.origin + val sourceFile = sourcePath(containingSignature, projectRoot, pathsBySignature) + val siteId = siteId(functionId, sourceSpan, event.callSite.location.index) + val decision = event.decision.serializedName + + writer.write( + buildJsonObject { + putCommonProjectFields(project, profile) + put("kind", "unknown_call") + put("entryFunctionId", entryFunctionId) + put("functionId", functionId) + put("siteId", siteId) + put("sourceFile", sourceFile) + sourceSpan?.let { span -> + put("startLine", span.startLine) + put("startColumn", span.startColumn) + put("endLine", span.endLine) + put("endColumn", span.endColumn) + } + put("statementIndex", event.callSite.location.index) + put("calleeId", calleeId(projectRoot, event.callee, pathsBySignature)) + put("calleeName", event.callee.name) + put("failureReason", event.failureReason.name) + put("decision", decision) + put("outcome", event.outcome.name) + put("eventIndex", eventCount) + } + ) + } +} + +internal class CensusRecordWriter(output: Path) : AutoCloseable { + private val writer: BufferedWriter = Files.newBufferedWriter( + output, + StandardCharsets.UTF_8, + StandardOpenOption.CREATE, + StandardOpenOption.TRUNCATE_EXISTING, + StandardOpenOption.WRITE, + ) + + fun write(record: JsonObject) { + writer.appendLine(record.toString()) + writer.flush() + } + + override fun close() { + writer.close() + } +} + +private enum class MethodStatus(val serializedName: String) { + COMPLETED("completed"), + TIMEOUT("timeout"), + TOOL_ERROR("tool_error"), +} + +private data class MethodRunResult( + val status: MethodStatus, + val events: Int, +) + +private data class LoadedProjectFiles( + val files: List, + val pathsBySignature: Map, +) + +private val UnknownCallCensusProfile.fallback: TsResidualCallPolicy + get() = when (this) { + UnknownCallCensusProfile.EMPTY_FRESH -> TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN + UnknownCallCensusProfile.EMPTY_STOP -> TsResidualCallPolicy.STOP_PATH + } + +private val TsUnknownCallDecision.serializedName: String + get() = when (this) { + is TsUnknownCallDecision.ModelApplied -> "MODEL_APPLIED:$modelId" + is TsUnknownCallDecision.ResidualFallback -> "RESIDUAL_FALLBACK:${policy.name}" + } + +private fun JsonObjectBuilderScope.putCommonProjectFields( + project: UnknownCallCensusProject, + profile: UnknownCallCensusProfile, +) { + put("schemaVersion", CENSUS_SCHEMA_VERSION) + put("projectId", project.id) + put("projectRevision", project.revision) + put("profile", profile.name) +} + +private typealias JsonObjectBuilderScope = kotlinx.serialization.json.JsonObjectBuilder + +private fun functionId( + projectId: String, + projectRoot: Path, + signature: EtsMethodSignature, + pathsBySignature: Map, +): String { + val sourceFile = sourcePath(signature, projectRoot, pathsBySignature) + return "$projectId:$sourceFile:${signatureKey(signature)}" +} + +private fun calleeId( + projectRoot: Path, + signature: EtsMethodSignature, + pathsBySignature: Map, +): String { + val sourceFile = sourcePath(signature, projectRoot, pathsBySignature) + return "$sourceFile:${signatureKey(signature)}" +} + +private fun sourcePath( + signature: EtsMethodSignature, + projectRoot: Path, + pathsBySignature: Map, +): String = pathsBySignature[signature.enclosingClass.file] + ?: normalizedSourcePath(signature.enclosingClass.file.fileName, projectRoot) + +private fun signatureKey(signature: EtsMethodSignature): String { + val parameters = signature.parameters.joinToString(separator = ",") { parameter -> parameter.type.toString() } + return "${signature.enclosingClass.name}:${signature.name}($parameters)->${signature.returnType}" +} + +private fun siteId(functionId: String, sourceSpan: EtsSourceSpan?, statementIndex: Int): String = + if (sourceSpan == null) { + "$functionId:ir-index:$statementIndex" + } else { + "$functionId:${sourceSpan.startLine}:${sourceSpan.startColumn}:${sourceSpan.endLine}:${sourceSpan.endColumn}" + } + +private fun normalizedSourcePath(rawPath: String, projectRoot: Path): String { + val normalizedRawPath = rawPath.normalizedSeparators().removePrefix("@") + val sourcePath = runCatching { Path.of(rawPath).normalize().absolute() }.getOrNull() + val normalizedRoot = projectRoot.normalize().absolute() + + return when { + sourcePath != null && sourcePath.startsWith(normalizedRoot) -> { + normalizedRoot.relativize(sourcePath).pathString.normalizedSeparators() + } + + Path.of(rawPath).isAbsolute -> "external/${Path.of(rawPath).name}" + else -> normalizedRawPath.removePrefix("./") + } +} + +private fun repositoryRelativeSourcePath( + rawPath: String, + sourceRoot: Path, + sourceRootRelativePath: String, + projectRoot: Path, +): String { + val raw = Path.of(rawPath) + if (raw.isAbsolute) { + return normalizedSourcePath(rawPath, projectRoot) + } + + val sourceRelativePath = normalizedSourcePath(rawPath, sourceRoot) + val normalizedSourceRoot = sourceRootRelativePath.normalizedSeparators().trim('/') + return listOf(normalizedSourceRoot, sourceRelativePath) + .filter(String::isNotEmpty) + .joinToString(separator = "/") +} + +private fun String.normalizedSeparators(): String = replace('\\', '/') + +private fun boundedError(error: Throwable): String { + val type = error::class.qualifiedName ?: error::class.simpleName ?: "Throwable" + val message = error.message + ?.replace('\n', ' ') + ?.replace(JVM_IDENTITY_SUFFIX, "@") + ?.take(MAX_ERROR_LENGTH) + return if (message.isNullOrBlank()) type else "$type: $message" +} + +private const val MAX_ERROR_LENGTH = 1_000 +private const val DEFAULT_FILE_METHOD_NAME = "%dflt" +private val JVM_IDENTITY_SUFFIX = Regex("@[0-9a-fA-F]{6,16}") diff --git a/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusAggregatorTest.kt b/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusAggregatorTest.kt new file mode 100644 index 0000000000..7a53307a56 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusAggregatorTest.kt @@ -0,0 +1,80 @@ +package org.usvm.census + +import kotlin.test.Test +import kotlin.test.assertEquals + +class UnknownCallCensusAggregatorTest { + @Test + fun `summary keeps repeated events separate from stable sites and preserves failures`() { + val rawRecords = sequenceOf( + unknownCallRecord(siteId = "project:file:fn:1:1:1:8", failureReason = "ANY_RECEIVER"), + unknownCallRecord(siteId = "project:file:fn:1:1:1:8", failureReason = "ANY_RECEIVER"), + unknownCallRecord(siteId = "project:file:fn:2:1:2:8", failureReason = "METHOD_BODY_UNAVAILABLE"), + methodRecord(functionId = "project:file:fn", status = "completed"), + methodRecord(functionId = "project:file:timeout", status = "timeout", error = "Machine timeout reached"), + methodRecord(functionId = "project:file:error", status = "tool_error", error = "frontend failed"), + projectRecord(projectId = "project", status = "completed"), + projectRecord(projectId = "broken", status = "tool_error", error = "checkout missing"), + ) + + val summary = UnknownCallCensusAggregator.summarize(rawRecords) + + val profile = requireNotNull(summary.profiles["EMPTY_FRESH"]) + assertEquals(2, profile.projects) + assertEquals(3, profile.functionsAnalyzed) + assertEquals(1, profile.functionsCompleted) + assertEquals(1, profile.functionsWithUnknownCalls) + assertEquals(2, profile.uniqueSites) + assertEquals(3, profile.rawEvents) + assertEquals(mapOf("ANY_RECEIVER" to 2, "METHOD_BODY_UNAVAILABLE" to 1), profile.eventsByFailureReason) + assertEquals(mapOf("RESIDUAL_FALLBACK:FRESH_SYMBOLIC_RETURN" to 3), profile.eventsByDecision) + assertEquals(mapOf("external:unknown" to 3), profile.eventsByCallee) + assertEquals(mapOf("external:unknown" to 2), profile.uniqueSitesByCallee) + assertEquals(listOf("project:file:timeout"), profile.timeouts.mapNotNull { it.functionId }) + assertEquals(2, profile.errors.size) + } + + private fun unknownCallRecord(siteId: String, failureReason: String): String = """ + { + "kind":"unknown_call", + "schemaVersion":1, + "projectId":"project", + "projectRevision":"0000000000000000000000000000000000000000", + "profile":"EMPTY_FRESH", + "functionId":"project:file:fn", + "siteId":"$siteId", + "calleeId":"external:unknown", + "failureReason":"$failureReason", + "decision":"RESIDUAL_FALLBACK:FRESH_SYMBOLIC_RETURN" + } + """.trimIndent() + + private fun methodRecord(functionId: String, status: String, error: String? = null): String { + val errorField = error?.let { ",\"error\":\"$it\"" }.orEmpty() + return """ + { + "kind":"method_result", + "schemaVersion":1, + "projectId":"project", + "projectRevision":"0000000000000000000000000000000000000000", + "profile":"EMPTY_FRESH", + "functionId":"$functionId", + "status":"$status"$errorField + } + """.trimIndent() + } + + private fun projectRecord(projectId: String, status: String, error: String? = null): String { + val errorField = error?.let { ",\"error\":\"$it\"" }.orEmpty() + return """ + { + "kind":"project_result", + "schemaVersion":1, + "projectId":"$projectId", + "projectRevision":"0000000000000000000000000000000000000000", + "profile":"EMPTY_FRESH", + "status":"$status"$errorField + } + """.trimIndent() + } +} From 16973b94892cb373cb975fc58afa98623787c833 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 19 Sep 2026 13:30:55 +0300 Subject: [PATCH 02/10] Record final development census selection --- usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md b/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md index 60181d0f0e..a1647250da 100644 --- a/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md +++ b/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md @@ -5,8 +5,8 @@ Selection frozen on 2026-09-19 before any held-out TS Calls evaluation. This is ## Evidence used - Approximation audit #368 at `303409613c30ea5dcdabc1f97ac8092d753765b1`, which audits current source `41961f7b66c30c8a2a7507c67a79396f495f4520` and historical source `3728ba45ab092422e2cb2e57ed6fe2377425b622`. -- The frozen development manifest in `development-corpus.json` and its primary `EMPTY_FRESH` census. The corrected local pilot attempted 79 functions from three pinned projects: 58 completed, 6 timed out, and 15 ended with a boundary tool error. It observed 813 repeated events at 41 stable sites in 23 containing functions. These counts are retained with the raw artifact and must be regenerated after transplanting the census onto the accepted integration head. -- Stable-site prevalence rather than repeated loop-event totals. The largest repeated groups were application callback or dispatch limitations: `BSTreeKV.compare` (390 events, 3 sites), iterator `next` (141 events, 2 sites), and `Array.isArray` (120 events, 1 site). Project-defined `Stack.pop` accounted for 18 events at 3 sites; it is not the built-in `Array.pop` target. No built-in `Array.shift` site was observed. +- The frozen development manifest in `development-corpus.json` and its primary `EMPTY_FRESH` census. The post-commit local pilot attempted 79 functions from three pinned projects: 58 completed, 6 timed out, and 15 ended with a boundary tool error. It observed 768 repeated events at 41 stable sites in 23 containing functions. These counts are retained with the raw artifact and must be regenerated after transplanting the census onto the accepted integration head. +- Stable-site prevalence rather than repeated loop-event totals. The largest repeated groups were application callback or dispatch limitations: `BSTreeKV.compare` (390 events, 3 sites), iterator `next` (122 events, 2 sites), and `Array.isArray` (102 events, 1 site). Project-defined `Stack.pop` accounted for 14 events at 3 sites; it is not the built-in `Array.pop` target. No built-in `Array.shift` site was observed. The primary profile disables optional catalog models but leaves mandatory semantics and legacy pre-dispatch approximations unchanged. Therefore the census is an inventory of observed unknown-call decisions, not every approximate or unresolved call in the engine. Tool errors, timeouts, and omitted call-resolution candidate tails also limit prevalence interpretation. From a26053ef8e19ff243360cd96d96e2332eda9ccef Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 19 Sep 2026 14:02:46 +0300 Subject: [PATCH 03/10] Fix unknown-call census validity --- usvm-ts/build.gradle.kts | 1 + .../unknown-call-census/MODEL_SELECTION.md | 6 +- .../experiments/unknown-call-census/README.md | 6 +- .../development-corpus.json | 2 +- .../usvm/census/UnknownCallCensusArtifacts.kt | 17 +- .../usvm/census/UnknownCallCensusRunner.kt | 246 ++++++++++++++---- .../census/UnknownCallCensusAggregatorTest.kt | 23 +- 7 files changed, 232 insertions(+), 69 deletions(-) diff --git a/usvm-ts/build.gradle.kts b/usvm-ts/build.gradle.kts index 396ad3082b..7c3cffc452 100644 --- a/usvm-ts/build.gradle.kts +++ b/usvm-ts/build.gradle.kts @@ -37,6 +37,7 @@ dependencies { tasks.register("runUnknownCallCensus") { group = "verification" description = "Runs or summarizes the TypeScript unknown-call census." + workingDir(rootProject.projectDir) classpath = sourceSets.main.get().runtimeClasspath mainClass.set("org.usvm.census.UnknownCallCensusCliKt") } diff --git a/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md b/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md index a1647250da..4d26464bc4 100644 --- a/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md +++ b/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md @@ -5,8 +5,8 @@ Selection frozen on 2026-09-19 before any held-out TS Calls evaluation. This is ## Evidence used - Approximation audit #368 at `303409613c30ea5dcdabc1f97ac8092d753765b1`, which audits current source `41961f7b66c30c8a2a7507c67a79396f495f4520` and historical source `3728ba45ab092422e2cb2e57ed6fe2377425b622`. -- The frozen development manifest in `development-corpus.json` and its primary `EMPTY_FRESH` census. The post-commit local pilot attempted 79 functions from three pinned projects: 58 completed, 6 timed out, and 15 ended with a boundary tool error. It observed 768 repeated events at 41 stable sites in 23 containing functions. These counts are retained with the raw artifact and must be regenerated after transplanting the census onto the accepted integration head. -- Stable-site prevalence rather than repeated loop-event totals. The largest repeated groups were application callback or dispatch limitations: `BSTreeKV.compare` (390 events, 3 sites), iterator `next` (122 events, 2 sites), and `Array.isArray` (102 events, 1 site). Project-defined `Stack.pop` accounted for 14 events at 3 sites; it is not the built-in `Array.pop` target. No built-in `Array.shift` site was observed. +- The frozen development manifest in `development-corpus.json` and its primary `EMPTY_FRESH` census. The first local pilot attempted 79 functions from three pinned projects and produced 768 repeated events at 41 stable source sites. Review found that its entry-file bound also removed imported support files and that swallowed interpreter failures appeared completed. Its preserved raw artifact is preliminary diagnostic evidence, not valid prevalence or completion evidence. Corrected counts must come from the rerun on the accepted integration head. +- The preliminary artifact identified large repeated groups such as `BSTreeKV.compare`, iterator `next`, and `Array.isArray`, but those counts require corrected rerun confirmation. Its project-defined `Stack.pop` observations were manufactured by omitting the imported `stack.ts` support file and must not be used for model selection. No new family is admitted from this preliminary artifact. The primary profile disables optional catalog models but leaves mandatory semantics and legacy pre-dispatch approximations unchanged. Therefore the census is an inventory of observed unknown-call decisions, not every approximate or unresolved call in the engine. Tool errors, timeouts, and omitted call-resolution candidate tails also limit prevalence interpretation. @@ -23,7 +23,7 @@ The control set is empty. Both existing models were implemented before this cens No new model family is admitted for the pilot: -- `BSTreeKV.compare` and the project `Stack` methods require application-call/callback resolution shared by every profile, not optional treatment models. +- Application callbacks and dispatch limitations such as `BSTreeKV.compare` require shared call-resolution work, not optional treatment models. - Iterator `next` needs stateful iterator representation and completion/alias validation. - `Array.isArray` has one stable development site and still needs proven target provenance plus rank/proxy bounds. - The remaining scattered standard calls do not establish both prevalence and a reviewed bounded semantic contract. diff --git a/usvm-ts/experiments/unknown-call-census/README.md b/usvm-ts/experiments/unknown-call-census/README.md index 4521b8acac..14ef92ea4b 100644 --- a/usvm-ts/experiments/unknown-call-census/README.md +++ b/usvm-ts/experiments/unknown-call-census/README.md @@ -1,8 +1,8 @@ # TypeScript unknown-call development census -This census measures unknown-call events on a frozen development corpus. The projects and revisions were selected before current measurements and come from the historical TypeScript experiment corpus. They are development evidence and must not be reused as held-out evaluation projects. The manifest admits only `.ts` sources, excludes declarations and common test suffixes, excludes synthetic anonymous and initializer entry methods, sorts stable repository-relative file/function identities, and takes the bounded prefix recorded in `limits`. Unknown calls reached inside nested source functions retain their actual containing-function identity. +This census measures unknown-call events on a frozen development corpus. The projects and revisions were selected before current measurements and come from the historical TypeScript experiment corpus. They are development evidence and must not be reused as held-out evaluation projects. The manifest admits only `.ts` entry files, excludes declarations and common test suffixes, excludes synthetic anonymous and initializer entry methods, sorts stable repository-relative file/function identities, and takes the bounded entry-file prefix recorded in `limits`. The execution scene retains every loaded support file so the entry-file bound does not remove imported callees. Unknown calls reached inside nested source functions retain their actual containing-function identity. -The primary profile disables every optional unknown-call model and uses `FRESH_SYMBOLIC_RETURN`. Mandatory engine semantics and the legacy approximations that run before unknown-call dispatch remain enabled and identical across profiles. Therefore this census measures observed unknown-call decisions, not every call handled approximately by the engine. The raw artifact keeps every repeated event, while the summary separately deduplicates containing functions and stable source sites. Existing `ts.array.shift` and `ts.array.pop` models validate the mechanism but are not described as census-selected. +The primary profile disables every optional unknown-call model and uses `FRESH_SYMBOLIC_RETURN`. Mandatory engine semantics and the legacy approximations that run before unknown-call dispatch remain enabled and identical across profiles. Therefore this census measures observed unknown-call decisions, not every call handled approximately by the engine. The raw artifact keeps every repeated event, while the summary separately deduplicates containing functions and stable source sites. A stable source site can contain multiple lowered IR calls; raw records retain the statement index and callee identity. Method results distinguish complete analysis from partial analysis stopped by an engine or recording failure. Existing `ts.array.shift` and `ts.array.pop` models validate the mechanism but are not described as census-selected. Prepare each repository below `CHECKOUT_ROOT` at the exact revision recorded in `development-corpus.json`, then run: @@ -10,7 +10,7 @@ Prepare each repository below `CHECKOUT_ROOT` at the exact revision recorded in ./gradlew :usvm-ts:runUnknownCallCensus --args='census --manifest usvm-ts/experiments/unknown-call-census/development-corpus.json --checkout-root /absolute/path/to/checkouts --output /absolute/path/to/results' ``` -The command refuses a checkout whose Git `HEAD` differs from the manifest. It writes `raw.jsonl` incrementally and creates `summary.json`. Regenerate the summary without rerunning symbolic execution using: +The command refuses a checkout whose Git `HEAD` differs from the manifest or whose working tree contains tracked or untracked changes. It creates `raw.jsonl` without overwriting prior evidence, writes records incrementally, and creates `summary.json`. Use a new output directory for every run. Regenerate the summary without rerunning symbolic execution using: ```sh ./gradlew :usvm-ts:runUnknownCallCensus --args='summarize --input /absolute/path/to/results/raw.jsonl --output /absolute/path/to/results/summary.json' diff --git a/usvm-ts/experiments/unknown-call-census/development-corpus.json b/usvm-ts/experiments/unknown-call-census/development-corpus.json index bae98e588e..0730213e8e 100644 --- a/usvm-ts/experiments/unknown-call-census/development-corpus.json +++ b/usvm-ts/experiments/unknown-call-census/development-corpus.json @@ -1,5 +1,5 @@ { - "schemaVersion": 1, + "schemaVersion": 2, "projects": [ { "id": "the-algorithms-typescript", diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusArtifacts.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusArtifacts.kt index fb6371182b..c4e1d06173 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusArtifacts.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusArtifacts.kt @@ -4,9 +4,10 @@ import kotlinx.serialization.Serializable import kotlinx.serialization.json.Json import kotlinx.serialization.json.JsonObject import kotlinx.serialization.json.contentOrNull +import kotlinx.serialization.json.intOrNull import kotlinx.serialization.json.jsonPrimitive -internal const val CENSUS_SCHEMA_VERSION = 1 +internal const val CENSUS_SCHEMA_VERSION = 2 internal val censusJson = Json { encodeDefaults = true @@ -60,6 +61,7 @@ internal data class UnknownCallCensusProfileSummary( val projects: Int, val functionsAnalyzed: Int, val functionsCompleted: Int, + val functionsPartial: Int, val functionsWithUnknownCalls: Int, val uniqueSites: Int, val rawEvents: Int, @@ -67,6 +69,7 @@ internal data class UnknownCallCensusProfileSummary( val eventsByDecision: Map, val eventsByCallee: Map, val uniqueSitesByCallee: Map, + val partials: List, val timeouts: List, val errors: List, ) @@ -76,6 +79,7 @@ internal data class UnknownCallCensusIssue( val projectId: String, val functionId: String? = null, val message: String? = null, + val failureCount: Int = 0, ) internal object UnknownCallCensusAggregator { @@ -110,6 +114,7 @@ private class ProfileAccumulator { private val projects = hashSetOf() private val functions = hashSetOf() private val completedFunctions = hashSetOf() + private val partialFunctions = hashSetOf() private val functionsWithUnknownCalls = hashSetOf() private val sites = hashSetOf() private var rawEvents = 0 @@ -117,6 +122,7 @@ private class ProfileAccumulator { private val eventsByDecision = hashMapOf() private val eventsByCallee = hashMapOf() private val sitesByCallee = hashMapOf>() + private val partials = mutableListOf() private val timeouts = mutableListOf() private val errors = mutableListOf() @@ -146,12 +152,17 @@ private class ProfileAccumulator { projectId = projectId, functionId = functionId, message = record.optionalString("error"), + failureCount = record.optionalInt("failureCount") ?: 0, ) projects += projectId functions += functionId when (status) { "completed" -> completedFunctions += functionId + "partial" -> { + partialFunctions += functionId + partials += issue + } "timeout" -> timeouts += issue "tool_error" -> errors += issue } @@ -176,6 +187,7 @@ private class ProfileAccumulator { projects = projects.size, functionsAnalyzed = functions.size, functionsCompleted = completedFunctions.size, + functionsPartial = partialFunctions.size, functionsWithUnknownCalls = functionsWithUnknownCalls.size, uniqueSites = sites.size, rawEvents = rawEvents, @@ -183,6 +195,7 @@ private class ProfileAccumulator { eventsByDecision = eventsByDecision.toSortedMap(), eventsByCallee = eventsByCallee.toSortedMap(), uniqueSitesByCallee = sitesByCallee.toSortedMap().mapValues { (_, sites) -> sites.size }, + partials = partials.sortedWith(issueComparator), timeouts = timeouts.sortedWith(issueComparator), errors = errors.sortedWith(issueComparator), ) @@ -202,3 +215,5 @@ private fun JsonObject.requiredString(name: String, recordIndex: Int): String = optionalString(name) ?: error("Raw census record ${recordIndex + 1} has no string '$name'") private fun JsonObject.optionalString(name: String): String? = get(name)?.jsonPrimitive?.contentOrNull + +private fun JsonObject.optionalInt(name: String): Int? = get(name)?.jsonPrimitive?.intOrNull diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt index eb10f41e50..d93155a518 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt @@ -8,13 +8,16 @@ import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsNamespaceSignature import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsSourceSpan import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX +import org.jacodb.ets.utils.EtsIrGenerationException import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME -import org.jacodb.ets.utils.loadEtsProjectAutoConvert +import org.jacodb.ets.utils.generateEtsIR +import org.jacodb.ets.utils.loadEtsProjectFromIR import org.usvm.SolverType import org.usvm.UMachineOptions import org.usvm.machine.TsInterpreterObserver @@ -38,6 +41,7 @@ import kotlin.io.path.exists import kotlin.io.path.isDirectory import kotlin.io.path.name import kotlin.io.path.pathString +import kotlin.time.Duration import kotlin.time.Duration.Companion.seconds import kotlin.time.TimeSource @@ -51,6 +55,10 @@ internal class UnknownCallCensusRunner( validateManifest() outputDirectory.createDirectories() val rawOutput = outputDirectory.resolve(RAW_FILE_NAME) + val summaryOutput = outputDirectory.resolve(SUMMARY_FILE_NAME) + require(!rawOutput.exists() && !summaryOutput.exists()) { + "Census output already contains raw.jsonl or summary.json: $outputDirectory" + } CensusRecordWriter(rawOutput).use { writer -> val startedAt = Instant.now() @@ -75,7 +83,7 @@ internal class UnknownCallCensusRunner( UnknownCallCensusAggregator.summarize(lines) } Files.writeString( - outputDirectory.resolve(SUMMARY_FILE_NAME), + summaryOutput, censusJson.encodeToString(summary) + System.lineSeparator(), StandardCharsets.UTF_8, ) @@ -90,6 +98,7 @@ internal class UnknownCallCensusRunner( writer: CensusRecordWriter, ) { val projectStart = TimeSource.Monotonic.markNow() + val projectTimeout = manifest.limits.projectTimeoutSeconds.seconds val normalizedCheckoutRoot = checkoutRoot.normalize().absolute() val projectRoot = normalizedCheckoutRoot.resolve(project.path).normalize() @@ -104,14 +113,19 @@ internal class UnknownCallCensusRunner( "Project license file does not exist: ${project.licenseFile}" } validateRevision(projectRoot, project.revision) + validateCleanCheckout(projectRoot) - val loadedFiles = loadProjectFiles(project, projectRoot) - val files = selectFiles(project, loadedFiles) + val loadedFiles = loadProjectFiles(project, projectRoot, projectStart, projectTimeout) + val entryFiles = selectFiles(project, loadedFiles) + val sceneFiles = loadedFiles.files + .distinctBy { file -> requireNotNull(loadedFiles.pathsBySignature[file.signature]) } + .sortedBy { file -> requireNotNull(loadedFiles.pathsBySignature[file.signature]) } val scene = EtsScene( - projectFiles = files, + projectFiles = sceneFiles, projectName = project.id, ) - val methods = scene.projectClasses + val methods = entryFiles + .flatMap { it.allClasses } .flatMap { it.methods } .filterNot { it.cfg.stmts.isEmpty() } .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) } @@ -123,12 +137,13 @@ internal class UnknownCallCensusRunner( var rawEvents = 0 var completedMethods = 0 + var partialMethods = 0 var timedOutMethods = 0 var failedMethods = 0 var projectTimedOut = false for (method in methods) { - if (projectStart.elapsedNow() >= manifest.limits.projectTimeoutSeconds.seconds) { + if (projectStart.elapsedNow() >= projectTimeout) { projectTimedOut = true break } @@ -145,6 +160,7 @@ internal class UnknownCallCensusRunner( rawEvents += result.events when (result.status) { MethodStatus.COMPLETED -> completedMethods++ + MethodStatus.PARTIAL -> partialMethods++ MethodStatus.TIMEOUT -> timedOutMethods++ MethodStatus.TOOL_ERROR -> failedMethods++ } @@ -155,9 +171,11 @@ internal class UnknownCallCensusRunner( putCommonProjectFields(project, profile) put("kind", "project_result") put("status", if (projectTimedOut) "timeout" else "completed") - put("filesSelected", files.size) + put("sceneFiles", sceneFiles.size) + put("filesSelected", entryFiles.size) put("methodsSelected", methods.size) put("methodsCompleted", completedMethods) + put("methodsPartial", partialMethods) put("methodsTimedOut", timedOutMethods) put("methodsFailed", failedMethods) put("rawEvents", rawEvents) @@ -167,19 +185,32 @@ internal class UnknownCallCensusRunner( } } ) + } catch (error: ProjectTimeoutException) { + writeProjectFailure(project, profile, writer, "timeout", projectStart, error) } catch (error: Exception) { - writer.write( - buildJsonObject { - putCommonProjectFields(project, profile) - put("kind", "project_result") - put("status", "tool_error") - put("durationMillis", projectStart.elapsedNow().inWholeMilliseconds) - put("error", boundedError(error)) - } - ) + writeProjectFailure(project, profile, writer, "tool_error", projectStart, error) } } + private fun writeProjectFailure( + project: UnknownCallCensusProject, + profile: UnknownCallCensusProfile, + writer: CensusRecordWriter, + status: String, + projectStart: TimeSource.Monotonic.ValueTimeMark, + error: Throwable, + ) { + writer.write( + buildJsonObject { + putCommonProjectFields(project, profile) + put("kind", "project_result") + put("status", status) + put("durationMillis", projectStart.elapsedNow().inWholeMilliseconds) + put("error", boundedError(error)) + } + ) + } + @Suppress("TooGenericExceptionCaught") private fun runMethod( project: UnknownCallCensusProject, @@ -204,6 +235,7 @@ internal class UnknownCallCensusRunner( randomSeed = 0, timeout = methodTimeout, solverType = SolverType.YICES, + throwExceptionOnStepFailure = true, ) val emptyModelSelection = TsUnknownCallModelSelection.Only(emptySet()) val tsOptions = TsOptions( @@ -214,6 +246,7 @@ internal class UnknownCallCensusRunner( val analysisStart = TimeSource.Monotonic.markNow() var status = MethodStatus.COMPLETED var errorText: String? = null + var failureCount = 0 try { TsMachine( @@ -222,7 +255,25 @@ internal class UnknownCallCensusRunner( tsOptions = tsOptions, observer = observer, ).use { machine -> - machine.analyze(methods = listOf(method)) + try { + machine.analyze(methods = listOf(method)) + } catch (error: Exception) { + status = MethodStatus.PARTIAL + failureCount++ + errorText = boundedError(error) + } catch (error: NotImplementedError) { + status = MethodStatus.PARTIAL + failureCount++ + errorText = boundedError(error) + } + } + + if (observer.recordingFailureCount > 0) { + failureCount += observer.recordingFailureCount + errorText = combineErrors(errorText, observer.recordingFailureMessage) + if (status == MethodStatus.COMPLETED) { + status = MethodStatus.PARTIAL + } } if (analysisStart.elapsedNow() >= methodTimeout) { @@ -231,6 +282,11 @@ internal class UnknownCallCensusRunner( } } catch (error: Exception) { status = MethodStatus.TOOL_ERROR + failureCount++ + errorText = boundedError(error) + } catch (error: NotImplementedError) { + status = MethodStatus.TOOL_ERROR + failureCount++ errorText = boundedError(error) } @@ -242,6 +298,7 @@ internal class UnknownCallCensusRunner( put("status", status.serializedName) put("durationMillis", analysisStart.elapsedNow().inWholeMilliseconds) put("rawEvents", observer.eventCount) + put("failureCount", failureCount) errorText?.let { put("error", it) } } ) @@ -262,19 +319,47 @@ internal class UnknownCallCensusRunner( .map { (file, _) -> file } .toList() - private fun loadProjectFiles(project: UnknownCallCensusProject, projectRoot: Path): LoadedProjectFiles { + private fun loadProjectFiles( + project: UnknownCallCensusProject, + projectRoot: Path, + projectStart: TimeSource.Monotonic.ValueTimeMark, + projectTimeout: Duration, + ): LoadedProjectFiles { val sourceRoots = project.include.ifEmpty { listOf("") } val files = mutableListOf() val pathsBySignature = hashMapOf() sourceRoots.forEach { relativePath -> + ensureWithinProjectTimeout(projectStart, projectTimeout) + val remaining = projectTimeout - projectStart.elapsedNow() + val sourceRoot = projectRoot.resolve(relativePath).normalize() - require(sourceRoot.startsWith(projectRoot)) { "Configured source root escapes project checkout: $sourceRoot" } + require(sourceRoot.startsWith(projectRoot)) { + "Configured source root escapes project checkout: $sourceRoot" + } require(sourceRoot.isDirectory()) { "Configured source root does not exist: $sourceRoot" } - val loadedFiles = loadEtsProjectAutoConvert( - sourceRoot, - provider = EtsIrProvider.TS_FRONTEND, - ).projectFiles + val generatedIr = try { + generateEtsIR( + projectPath = sourceRoot, + isProject = true, + loadEntrypoints = false, + timeout = remaining, + provider = EtsIrProvider.TS_FRONTEND, + ) + } catch (error: EtsIrGenerationException) { + ensureWithinProjectTimeout(projectStart, projectTimeout, cause = error) + throw error + } + val loadedFiles = try { + loadEtsProjectFromIR( + projectFilesPath = generatedIr, + sdkFilesPath = null, + ).projectFiles + } finally { + generatedIr.toFile().deleteRecursively() + } + + ensureWithinProjectTimeout(projectStart, projectTimeout) loadedFiles.forEach { file -> val sourcePath = repositoryRelativeSourcePath( @@ -294,6 +379,16 @@ internal class UnknownCallCensusRunner( return LoadedProjectFiles(files = files, pathsBySignature = pathsBySignature) } + private fun ensureWithinProjectTimeout( + projectStart: TimeSource.Monotonic.ValueTimeMark, + projectTimeout: Duration, + cause: Throwable? = null, + ) { + if (projectStart.elapsedNow() >= projectTimeout) { + throw ProjectTimeoutException("Project timeout reached during frontend conversion", cause) + } + } + private fun validateManifest() { require(manifest.schemaVersion == CENSUS_SCHEMA_VERSION) { "Unsupported census manifest schema ${manifest.schemaVersion}" @@ -363,8 +458,19 @@ internal class UnknownCallCensusRunner( } } - private fun gitObject(directory: Path, ref: String): String? = runCatching { - val process = ProcessBuilder("git", "-C", directory.pathString, "rev-parse", ref) + private fun validateCleanCheckout(projectRoot: Path) { + val status = gitOutput( + directory = projectRoot, + arguments = listOf("status", "--porcelain=v1", "--untracked-files=normal"), + ) ?: error("Cannot inspect Git status for project checkout $projectRoot") + require(status.isBlank()) { "Project checkout has tracked or untracked changes: $projectRoot" } + } + + private fun gitObject(directory: Path, ref: String): String? = + gitOutput(directory, arguments = listOf("rev-parse", ref)) + + private fun gitOutput(directory: Path, arguments: List): String? = runCatching { + val process = ProcessBuilder(listOf("git", "-C", directory.pathString) + arguments) .redirectErrorStream(true) .start() val output = process.inputStream.bufferedReader().use { it.readText() }.trim() @@ -395,39 +501,52 @@ private class RecordingCensusObserver( ) : TsInterpreterObserver { var eventCount: Int = 0 private set + var recordingFailureCount: Int = 0 + private set + var recordingFailureMessage: String? = null + private set + @Suppress("TooGenericExceptionCaught") override fun onUnknownCall(event: TsUnknownCallEvent) { - eventCount++ - val containingSignature = event.callSite.location.method.signature - val functionId = functionId(project.id, projectRoot, containingSignature, pathsBySignature) - val sourceSpan = event.callSite.location.origin - val sourceFile = sourcePath(containingSignature, projectRoot, pathsBySignature) - val siteId = siteId(functionId, sourceSpan, event.callSite.location.index) - val decision = event.decision.serializedName + try { + val containingSignature = event.callSite.location.method.signature + val functionId = functionId(project.id, projectRoot, containingSignature, pathsBySignature) + val sourceSpan = event.callSite.location.origin + val sourceFile = sourcePath(containingSignature, projectRoot, pathsBySignature) + val siteId = siteId(functionId, sourceSpan, event.callSite.location.index) + val decision = event.decision.serializedName + val eventIndex = eventCount + 1 - writer.write( - buildJsonObject { - putCommonProjectFields(project, profile) - put("kind", "unknown_call") - put("entryFunctionId", entryFunctionId) - put("functionId", functionId) - put("siteId", siteId) - put("sourceFile", sourceFile) - sourceSpan?.let { span -> - put("startLine", span.startLine) - put("startColumn", span.startColumn) - put("endLine", span.endLine) - put("endColumn", span.endColumn) + writer.write( + buildJsonObject { + putCommonProjectFields(project, profile) + put("kind", "unknown_call") + put("entryFunctionId", entryFunctionId) + put("functionId", functionId) + put("siteId", siteId) + put("sourceFile", sourceFile) + sourceSpan?.let { span -> + put("startLine", span.startLine) + put("startColumn", span.startColumn) + put("endLine", span.endLine) + put("endColumn", span.endColumn) + } + put("statementIndex", event.callSite.location.index) + put("calleeId", calleeId(projectRoot, event.callee, pathsBySignature)) + put("calleeName", event.callee.name) + put("failureReason", event.failureReason.name) + put("decision", decision) + put("outcome", event.outcome.name) + put("eventIndex", eventIndex) } - put("statementIndex", event.callSite.location.index) - put("calleeId", calleeId(projectRoot, event.callee, pathsBySignature)) - put("calleeName", event.callee.name) - put("failureReason", event.failureReason.name) - put("decision", decision) - put("outcome", event.outcome.name) - put("eventIndex", eventCount) + ) + eventCount = eventIndex + } catch (error: Exception) { + recordingFailureCount++ + if (recordingFailureMessage == null) { + recordingFailureMessage = "Unknown-call event recording failed: ${boundedError(error)}" } - ) + } } } @@ -435,8 +554,7 @@ internal class CensusRecordWriter(output: Path) : AutoCloseable { private val writer: BufferedWriter = Files.newBufferedWriter( output, StandardCharsets.UTF_8, - StandardOpenOption.CREATE, - StandardOpenOption.TRUNCATE_EXISTING, + StandardOpenOption.CREATE_NEW, StandardOpenOption.WRITE, ) @@ -452,6 +570,7 @@ internal class CensusRecordWriter(output: Path) : AutoCloseable { private enum class MethodStatus(val serializedName: String) { COMPLETED("completed"), + PARTIAL("partial"), TIMEOUT("timeout"), TOOL_ERROR("tool_error"), } @@ -518,9 +637,14 @@ private fun sourcePath( private fun signatureKey(signature: EtsMethodSignature): String { val parameters = signature.parameters.joinToString(separator = ",") { parameter -> parameter.type.toString() } - return "${signature.enclosingClass.name}:${signature.name}($parameters)->${signature.returnType}" + val namespace = signature.enclosingClass.namespace?.qualifiedName() + val className = listOfNotNull(namespace, signature.enclosingClass.name).joinToString(separator = "::") + return "$className:${signature.name}($parameters)->${signature.returnType}" } +private fun EtsNamespaceSignature.qualifiedName(): String = + listOfNotNull(namespace?.qualifiedName(), name).joinToString(separator = "::") + private fun siteId(functionId: String, sourceSpan: EtsSourceSpan?, statementIndex: Int): String = if (sourceSpan == null) { "$functionId:ir-index:$statementIndex" @@ -572,6 +696,14 @@ private fun boundedError(error: Throwable): String { return if (message.isNullOrBlank()) type else "$type: $message" } +private fun combineErrors(primary: String?, additional: String?): String? = when { + primary == null -> additional + additional == null -> primary + else -> "$primary; $additional".take(MAX_ERROR_LENGTH) +} + +private class ProjectTimeoutException(message: String, cause: Throwable? = null) : RuntimeException(message, cause) + private const val MAX_ERROR_LENGTH = 1_000 private const val DEFAULT_FILE_METHOD_NAME = "%dflt" private val JVM_IDENTITY_SUFFIX = Regex("@[0-9a-fA-F]{6,16}") diff --git a/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusAggregatorTest.kt b/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusAggregatorTest.kt index 7a53307a56..6807cdaffa 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusAggregatorTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusAggregatorTest.kt @@ -11,6 +11,12 @@ class UnknownCallCensusAggregatorTest { unknownCallRecord(siteId = "project:file:fn:1:1:1:8", failureReason = "ANY_RECEIVER"), unknownCallRecord(siteId = "project:file:fn:2:1:2:8", failureReason = "METHOD_BODY_UNAVAILABLE"), methodRecord(functionId = "project:file:fn", status = "completed"), + methodRecord( + functionId = "project:file:partial", + status = "partial", + error = "step failed", + failureCount = 2, + ), methodRecord(functionId = "project:file:timeout", status = "timeout", error = "Machine timeout reached"), methodRecord(functionId = "project:file:error", status = "tool_error", error = "frontend failed"), projectRecord(projectId = "project", status = "completed"), @@ -21,8 +27,9 @@ class UnknownCallCensusAggregatorTest { val profile = requireNotNull(summary.profiles["EMPTY_FRESH"]) assertEquals(2, profile.projects) - assertEquals(3, profile.functionsAnalyzed) + assertEquals(4, profile.functionsAnalyzed) assertEquals(1, profile.functionsCompleted) + assertEquals(1, profile.functionsPartial) assertEquals(1, profile.functionsWithUnknownCalls) assertEquals(2, profile.uniqueSites) assertEquals(3, profile.rawEvents) @@ -30,6 +37,8 @@ class UnknownCallCensusAggregatorTest { assertEquals(mapOf("RESIDUAL_FALLBACK:FRESH_SYMBOLIC_RETURN" to 3), profile.eventsByDecision) assertEquals(mapOf("external:unknown" to 3), profile.eventsByCallee) assertEquals(mapOf("external:unknown" to 2), profile.uniqueSitesByCallee) + assertEquals(listOf("project:file:partial"), profile.partials.mapNotNull { it.functionId }) + assertEquals(2, profile.partials.single().failureCount) assertEquals(listOf("project:file:timeout"), profile.timeouts.mapNotNull { it.functionId }) assertEquals(2, profile.errors.size) } @@ -49,17 +58,23 @@ class UnknownCallCensusAggregatorTest { } """.trimIndent() - private fun methodRecord(functionId: String, status: String, error: String? = null): String { + private fun methodRecord( + functionId: String, + status: String, + error: String? = null, + failureCount: Int = 0, + ): String { val errorField = error?.let { ",\"error\":\"$it\"" }.orEmpty() return """ { "kind":"method_result", - "schemaVersion":1, + "schemaVersion":2, "projectId":"project", "projectRevision":"0000000000000000000000000000000000000000", "profile":"EMPTY_FRESH", "functionId":"$functionId", - "status":"$status"$errorField + "status":"$status", + "failureCount":$failureCount$errorField } """.trimIndent() } From 48f34bc64d8676c543b261e876dc4911848e5d33 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 19 Sep 2026 14:07:28 +0300 Subject: [PATCH 04/10] Record corrected unknown-call census --- .../experiments/unknown-call-census/MODEL_SELECTION.md | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md b/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md index 4d26464bc4..953fb1c259 100644 --- a/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md +++ b/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md @@ -5,8 +5,9 @@ Selection frozen on 2026-09-19 before any held-out TS Calls evaluation. This is ## Evidence used - Approximation audit #368 at `303409613c30ea5dcdabc1f97ac8092d753765b1`, which audits current source `41961f7b66c30c8a2a7507c67a79396f495f4520` and historical source `3728ba45ab092422e2cb2e57ed6fe2377425b622`. -- The frozen development manifest in `development-corpus.json` and its primary `EMPTY_FRESH` census. The first local pilot attempted 79 functions from three pinned projects and produced 768 repeated events at 41 stable source sites. Review found that its entry-file bound also removed imported support files and that swallowed interpreter failures appeared completed. Its preserved raw artifact is preliminary diagnostic evidence, not valid prevalence or completion evidence. Corrected counts must come from the rerun on the accepted integration head. -- The preliminary artifact identified large repeated groups such as `BSTreeKV.compare`, iterator `next`, and `Array.isArray`, but those counts require corrected rerun confirmation. Its project-defined `Stack.pop` observations were manufactured by omitting the imported `stack.ts` support file and must not be used for model selection. No new family is admitted from this preliminary artifact. +- The frozen development manifest in `development-corpus.json` and its corrected primary `EMPTY_FRESH` census at tool commit `b04a8ed16410fd3c5e8bc049304f9b649c11ee48`. It attempted the same 79 entry functions from three pinned projects: 43 completed, 35 ended with explicit partial-analysis diagnostics, one timed out, and none ended with a boundary tool error. It observed 82 repeated events at 26 stable source sites in 19 containing functions. The generated and standalone-regenerated summaries are byte-identical with SHA-256 `bf52a4cf5f03f867f594990c1f458ddb1d244c01679bf3a1fd852019aa3ce145`. +- Stable-source-site prevalence rather than repeated loop-event totals. The largest corrected groups were `BSTreeKV.compare` (24 events, 3 sites), the built-in array `pop` reached inside the restored project `Stack.pop` body (10 events, 1 site), `charAt` (7 events, 2 sites), `parseInt` (7 events, 2 sites), and callbacks (6 events, 3 sites). No built-in `Array.shift` site was observed. The high partial-analysis count limits prevalence interpretation. +- The first local pilot attempted the same functions but produced 768 events at 41 sites. Review found that its entry-file bound removed imported support files and that swallowed interpreter failures appeared completed. Its preserved raw artifact is preliminary diagnostic evidence only; in particular, its 52 project `Stack` resolution events were harness-induced and are excluded from selection evidence. The primary profile disables optional catalog models but leaves mandatory semantics and legacy pre-dispatch approximations unchanged. Therefore the census is an inventory of observed unknown-call decisions, not every approximate or unresolved call in the engine. Tool errors, timeouts, and omitted call-resolution candidate tails also limit prevalence interpretation. @@ -24,6 +25,7 @@ The control set is empty. Both existing models were implemented before this cens No new model family is admitted for the pilot: - Application callbacks and dispatch limitations such as `BSTreeKV.compare` require shared call-resolution work, not optional treatment models. +- The corrected array `pop` observation confirms one development source site for the already selected mechanism. It does not retrospectively make that pre-census model census-selected. - Iterator `next` needs stateful iterator representation and completion/alias validation. - `Array.isArray` has one stable development site and still needs proven target provenance plus rank/proxy bounds. - The remaining scattered standard calls do not establish both prevalence and a reviewed bounded semantic contract. @@ -32,10 +34,10 @@ This is an acceptable no-new-family result. A later family requires a separate b ## Content identity -At audited source `41961f7b66c30c8a2a7507c67a79396f495f4520`: +At accepted #380 source `3134d06515bca61ba2a357a67697ac8620b0e420` and corrected census tool tree `f9ba380951630b62ef55e7aae7d90f2fab55298b`: - `ArrayModels.ts` source SHA-256: `9f40d3abce58e3412a0206eabd9fdb0547e12c2ebd832ce48b260b3339518e26`. - `TsArrayShiftIntrinsicModel.kt` SHA-256: `ff6dd634cf660c83e203b82c927a28e88859f0bc6b9f24bec2fa97d738dc9e11`. - Empty catalog fingerprint: `e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855`. -Recompute the source hashes on the accepted #380/integration head and record the exact engine commit/tree, built JAR hashes, JacoDB `ddb127d9ef`, native frontend, solver, Node and options. The catalog fingerprint identifies only the sorted ID set. `ts.array.shift` has no EtsIR artifact. For `ts.array.pop`, record the generated `etsIrHash` from the actual accepted runtime load when the downstream harness exposes it; until then it is explicitly unavailable rather than invented. +The corrected run used JacoDB `ddb127d9ef`, the native `TS_FRONTEND`, Yices, OpenJDK 21.0.12, Node 26.5.0, random seed 0, a 300-second project budget, a 5-second method budget, at most 20 entry files and 40 entry methods per project. The catalog fingerprint identifies only the sorted ID set. `ts.array.shift` has no EtsIR artifact. For `ts.array.pop`, the generated `etsIrHash` remains unavailable from the built-in wrapper and must not be invented. From add0df7b5d18c708dc697b7340f6a15dcd46f801 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 19 Sep 2026 14:15:28 +0300 Subject: [PATCH 05/10] Preserve census partial failures past timeout --- .../usvm/census/UnknownCallCensusRunner.kt | 33 ++++++++++++++++--- .../census/UnknownCallCensusRunnerTest.kt | 33 +++++++++++++++++++ 2 files changed, 61 insertions(+), 5 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt index d93155a518..e27ebccd60 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt @@ -276,10 +276,14 @@ internal class UnknownCallCensusRunner( } } - if (analysisStart.elapsedNow() >= methodTimeout) { - status = MethodStatus.TIMEOUT - errorText = "Machine timeout reached" - } + val finalOutcome = methodOutcomeAfterTimeoutCheck( + status = status, + error = errorText, + elapsed = analysisStart.elapsedNow(), + timeout = methodTimeout, + ) + status = finalOutcome.status + errorText = finalOutcome.error } catch (error: Exception) { status = MethodStatus.TOOL_ERROR failureCount++ @@ -568,13 +572,32 @@ internal class CensusRecordWriter(output: Path) : AutoCloseable { } } -private enum class MethodStatus(val serializedName: String) { +internal enum class MethodStatus(val serializedName: String) { COMPLETED("completed"), PARTIAL("partial"), TIMEOUT("timeout"), TOOL_ERROR("tool_error"), } +internal data class MethodOutcome( + val status: MethodStatus, + val error: String?, +) + +internal fun methodOutcomeAfterTimeoutCheck( + status: MethodStatus, + error: String?, + elapsed: Duration, + timeout: Duration, +): MethodOutcome = if (status == MethodStatus.COMPLETED && elapsed >= timeout) { + MethodOutcome( + status = MethodStatus.TIMEOUT, + error = "Machine timeout reached", + ) +} else { + MethodOutcome(status = status, error = error) +} + private data class MethodRunResult( val status: MethodStatus, val events: Int, diff --git a/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt b/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt new file mode 100644 index 0000000000..d1eb3117bf --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt @@ -0,0 +1,33 @@ +package org.usvm.census + +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.time.Duration.Companion.seconds + +class UnknownCallCensusRunnerTest { + @Test + fun `elapsed timeout preserves a partial failure`() { + val outcome = methodOutcomeAfterTimeoutCheck( + status = MethodStatus.PARTIAL, + error = "Interpreter step failed", + elapsed = 6.seconds, + timeout = 5.seconds, + ) + + assertEquals(MethodStatus.PARTIAL, outcome.status) + assertEquals("Interpreter step failed", outcome.error) + } + + @Test + fun `elapsed timeout marks a completed analysis as timed out`() { + val outcome = methodOutcomeAfterTimeoutCheck( + status = MethodStatus.COMPLETED, + error = null, + elapsed = 6.seconds, + timeout = 5.seconds, + ) + + assertEquals(MethodStatus.TIMEOUT, outcome.status) + assertEquals("Machine timeout reached", outcome.error) + } +} From 4d31db48a6ce2f4882af5c0f32a1843a02acba25 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 19 Sep 2026 23:57:59 +0300 Subject: [PATCH 06/10] Adapt census metadata to merged model API --- usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md | 3 +-- .../main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt | 5 ----- 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md b/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md index 953fb1c259..dec09468b7 100644 --- a/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md +++ b/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md @@ -38,6 +38,5 @@ At accepted #380 source `3134d06515bca61ba2a357a67697ac8620b0e420` and corrected - `ArrayModels.ts` source SHA-256: `9f40d3abce58e3412a0206eabd9fdb0547e12c2ebd832ce48b260b3339518e26`. - `TsArrayShiftIntrinsicModel.kt` SHA-256: `ff6dd634cf660c83e203b82c927a28e88859f0bc6b9f24bec2fa97d738dc9e11`. -- Empty catalog fingerprint: `e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855`. -The corrected run used JacoDB `ddb127d9ef`, the native `TS_FRONTEND`, Yices, OpenJDK 21.0.12, Node 26.5.0, random seed 0, a 300-second project budget, a 5-second method budget, at most 20 entry files and 40 entry methods per project. The catalog fingerprint identifies only the sorted ID set. `ts.array.shift` has no EtsIR artifact. For `ts.array.pop`, the generated `etsIrHash` remains unavailable from the built-in wrapper and must not be invented. +The corrected run used JacoDB `ddb127d9ef`, the native `TS_FRONTEND`, Yices, OpenJDK 21.0.12, Node 26.5.0, random seed 0, a 300-second project budget, a 5-second method budget, at most 20 entry files and 40 entry methods per project. Its run metadata records `unknownCallModelSelection` as `NONE`. `ts.array.shift` has no EtsIR artifact. For `ts.array.pop`, the generated `etsIrHash` remains unavailable from the built-in wrapper and must not be invented. diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt index e27ebccd60..2241ef27be 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt @@ -23,7 +23,6 @@ import org.usvm.UMachineOptions import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions -import org.usvm.machine.call.TsBuiltInUnknownCallModels import org.usvm.machine.call.TsResidualCallPolicy import org.usvm.machine.call.TsUnknownCallDecision import org.usvm.machine.call.TsUnknownCallEvent @@ -431,9 +430,6 @@ internal class UnknownCallCensusRunner( } private fun runStartRecord(startedAt: Instant): JsonObject = buildJsonObject { - val emptyModelSelection = TsUnknownCallModelSelection.Only(emptySet()) - val emptyCatalogFingerprint = TsBuiltInUnknownCallModels.catalog(emptyModelSelection).fingerprint - put("kind", "run_start") put("schemaVersion", CENSUS_SCHEMA_VERSION) put("startedAt", startedAt.toString()) @@ -446,7 +442,6 @@ internal class UnknownCallCensusRunner( put("javaVersion", System.getProperty("java.version")) put("randomSeed", 0) put("unknownCallModelSelection", "NONE") - put("unknownCallModelCatalogFingerprint", emptyCatalogFingerprint) put("legacyApproximationPolicy", "UNCHANGED") put("projectTimeoutSeconds", manifest.limits.projectTimeoutSeconds) put("methodTimeoutSeconds", manifest.limits.methodTimeoutSeconds) From 94d535859ec92301dea76b77492584b675ecdf17 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 20 Sep 2026 00:23:00 +0300 Subject: [PATCH 07/10] Harden census reproducibility boundaries --- .../org/usvm/census/UnknownCallCensusCli.kt | 2 +- .../usvm/census/UnknownCallCensusRunner.kt | 289 ++++++++++++++++-- .../census/UnknownCallCensusRunnerTest.kt | 93 ++++++ 3 files changed, 350 insertions(+), 34 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusCli.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusCli.kt index 8ef9f469f0..89d69b85d5 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusCli.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusCli.kt @@ -63,7 +63,7 @@ internal class UnknownCallCensusCli( outputPath.parent?.let(Files::createDirectories) Files.writeString( outputPath, - censusJson.encodeToString(summary) + System.lineSeparator(), + censusJson.encodeToString(summary) + "\n", StandardCharsets.UTF_8, ) output.appendLine(censusJson.encodeToString(summary)) diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt index 2241ef27be..b3d9c566af 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt @@ -32,8 +32,14 @@ import java.nio.charset.StandardCharsets import java.nio.file.Files import java.nio.file.Path import java.nio.file.StandardOpenOption +import java.nio.file.attribute.PosixFilePermission +import java.nio.file.attribute.PosixFilePermissions import java.security.MessageDigest import java.time.Instant +import java.util.concurrent.CompletableFuture +import java.util.concurrent.ExecutionException +import java.util.concurrent.TimeUnit +import java.util.concurrent.TimeoutException import kotlin.io.path.absolute import kotlin.io.path.createDirectories import kotlin.io.path.exists @@ -41,6 +47,7 @@ import kotlin.io.path.isDirectory import kotlin.io.path.name import kotlin.io.path.pathString import kotlin.time.Duration +import kotlin.time.Duration.Companion.milliseconds import kotlin.time.Duration.Companion.seconds import kotlin.time.TimeSource @@ -83,7 +90,7 @@ internal class UnknownCallCensusRunner( } Files.writeString( summaryOutput, - censusJson.encodeToString(summary) + System.lineSeparator(), + censusJson.encodeToString(summary) + "\n", StandardCharsets.UTF_8, ) @@ -98,21 +105,29 @@ internal class UnknownCallCensusRunner( ) { val projectStart = TimeSource.Monotonic.markNow() val projectTimeout = manifest.limits.projectTimeoutSeconds.seconds - val normalizedCheckoutRoot = checkoutRoot.normalize().absolute() - val projectRoot = normalizedCheckoutRoot.resolve(project.path).normalize() try { - require(projectRoot.startsWith(normalizedCheckoutRoot)) { - "Project checkout escapes the configured checkout root: $projectRoot" - } - require(projectRoot.isDirectory()) { "Project checkout does not exist: $projectRoot" } - val licenseFile = projectRoot.resolve(project.licenseFile).normalize() - require(licenseFile.startsWith(projectRoot)) { "Project license file escapes its checkout: $licenseFile" } - require(licenseFile.exists()) { - "Project license file does not exist: ${project.licenseFile}" - } - validateRevision(projectRoot, project.revision) - validateCleanCheckout(projectRoot) + // A checkout entry may itself be a symlink. Its validated Git repository is the provenance boundary. + val projectRoot = canonicalProjectCheckout( + checkoutRoot = checkoutRoot, + relativePath = project.path, + ) + canonicalExistingProjectPath( + projectRoot = projectRoot, + relativePath = project.licenseFile, + kind = "Project license file", + requireDirectory = false, + ) + + validateRevision( + projectRoot = projectRoot, + expectedRevision = project.revision, + timeout = remainingProjectBudget(projectStart, projectTimeout, phase = "Git revision validation"), + ) + validateCleanCheckout( + projectRoot = projectRoot, + timeout = remainingProjectBudget(projectStart, projectTimeout, phase = "Git status validation"), + ) val loadedFiles = loadProjectFiles(project, projectRoot, projectStart, projectTimeout) val entryFiles = selectFiles(project, loadedFiles) @@ -336,11 +351,12 @@ internal class UnknownCallCensusRunner( ensureWithinProjectTimeout(projectStart, projectTimeout) val remaining = projectTimeout - projectStart.elapsedNow() - val sourceRoot = projectRoot.resolve(relativePath).normalize() - require(sourceRoot.startsWith(projectRoot)) { - "Configured source root escapes project checkout: $sourceRoot" - } - require(sourceRoot.isDirectory()) { "Configured source root does not exist: $sourceRoot" } + val sourceRoot = canonicalExistingProjectPath( + projectRoot = projectRoot, + relativePath = relativePath, + kind = "Configured source root", + requireDirectory = true, + ) val generatedIr = try { generateEtsIR( projectPath = sourceRoot, @@ -392,6 +408,19 @@ internal class UnknownCallCensusRunner( } } + private fun remainingProjectBudget( + projectStart: TimeSource.Monotonic.ValueTimeMark, + projectTimeout: Duration, + phase: String, + ): Duration { + val remaining = projectTimeout - projectStart.elapsedNow() + if (remaining <= Duration.ZERO) { + throw ProjectTimeoutException("Project timeout reached during $phase") + } + + return remaining + } + private fun validateManifest() { require(manifest.schemaVersion == CENSUS_SCHEMA_VERSION) { "Unsupported census manifest schema ${manifest.schemaVersion}" @@ -434,8 +463,14 @@ internal class UnknownCallCensusRunner( put("schemaVersion", CENSUS_SCHEMA_VERSION) put("startedAt", startedAt.toString()) put("manifestSha256", sha256(Files.readAllBytes(manifestPath))) - put("toolRevision", gitObject(Path.of("."), ref = "HEAD") ?: "unknown") - put("toolTree", gitObject(Path.of("."), ref = "HEAD^{tree}") ?: "unknown") + put( + "toolRevision", + gitObject(Path.of("."), ref = "HEAD", timeout = RUN_METADATA_GIT_TIMEOUT) ?: "unknown", + ) + put( + "toolTree", + gitObject(Path.of("."), ref = "HEAD^{tree}", timeout = RUN_METADATA_GIT_TIMEOUT) ?: "unknown", + ) put("jacodbArtifact", runtimeArtifactName(EtsScene::class.java)) put("frontendProvider", EtsIrProvider.TS_FRONTEND.name) put("solver", SolverType.YICES.name) @@ -449,32 +484,70 @@ internal class UnknownCallCensusRunner( put("maxMethods", manifest.limits.maxMethods) } - private fun validateRevision(projectRoot: Path, expectedRevision: String) { - val actualRevision = gitObject(projectRoot, ref = "HEAD") + private fun validateRevision(projectRoot: Path, expectedRevision: String, timeout: Duration) { + val actualRevision = gitObject( + directory = projectRoot, + ref = "HEAD", + timeout = timeout, + timeoutFailure = { + ProjectTimeoutException("Project timeout reached during Git revision validation") + }, + ) ?: error("Cannot read Git revision for project checkout $projectRoot") require(actualRevision.equals(expectedRevision, ignoreCase = true)) { "Project checkout $projectRoot is at $actualRevision, expected $expectedRevision" } } - private fun validateCleanCheckout(projectRoot: Path) { + private fun validateCleanCheckout(projectRoot: Path, timeout: Duration) { val status = gitOutput( directory = projectRoot, arguments = listOf("status", "--porcelain=v1", "--untracked-files=normal"), + timeout = timeout, + timeoutFailure = { + ProjectTimeoutException("Project timeout reached during Git status validation") + }, ) ?: error("Cannot inspect Git status for project checkout $projectRoot") require(status.isBlank()) { "Project checkout has tracked or untracked changes: $projectRoot" } } - private fun gitObject(directory: Path, ref: String): String? = - gitOutput(directory, arguments = listOf("rev-parse", ref)) + private fun gitObject( + directory: Path, + ref: String, + timeout: Duration, + timeoutFailure: (() -> ProjectTimeoutException)? = null, + ): String? = gitOutput( + directory = directory, + arguments = listOf("rev-parse", ref), + timeout = timeout, + timeoutFailure = timeoutFailure, + ) - private fun gitOutput(directory: Path, arguments: List): String? = runCatching { - val process = ProcessBuilder(listOf("git", "-C", directory.pathString) + arguments) - .redirectErrorStream(true) - .start() - val output = process.inputStream.bufferedReader().use { it.readText() }.trim() - if (process.waitFor() == 0) output else null - }.getOrNull() + private fun gitOutput( + directory: Path, + arguments: List, + timeout: Duration, + timeoutFailure: (() -> ProjectTimeoutException)? = null, + ): String? { + val result = runCatching { + boundedProcessOutput( + command = listOf("git", "-C", directory.pathString) + arguments, + timeout = timeout, + maxOutputBytes = MAX_GIT_OUTPUT_BYTES, + ) + }.getOrNull() ?: return null + + return when (result) { + is BoundedProcessOutput.Completed -> { + if (result.exitCode == 0 && !result.truncated) result.output.trim() else null + } + + BoundedProcessOutput.TimedOut -> { + timeoutFailure?.let { throw it() } + null + } + } + } private fun sha256(bytes: ByteArray): String = MessageDigest.getInstance("SHA-256") .digest(bytes) @@ -483,9 +556,159 @@ internal class UnknownCallCensusRunner( private companion object { const val RAW_FILE_NAME = "raw.jsonl" const val SUMMARY_FILE_NAME = "summary.json" + const val MAX_GIT_OUTPUT_BYTES = 64 * 1024 + val RUN_METADATA_GIT_TIMEOUT = 10.seconds } } +internal fun canonicalProjectCheckout(checkoutRoot: Path, relativePath: String): Path { + val canonicalCheckoutRoot = checkoutRoot.toRealPath() + val configuredProjectRoot = canonicalCheckoutRoot.resolve(relativePath).normalize() + require(configuredProjectRoot.startsWith(canonicalCheckoutRoot)) { + "Project checkout escapes the configured checkout root: $configuredProjectRoot" + } + require(configuredProjectRoot.isDirectory()) { + "Project checkout does not exist: $configuredProjectRoot" + } + + return configuredProjectRoot.toRealPath() +} + +internal fun canonicalExistingProjectPath( + projectRoot: Path, + relativePath: String, + kind: String, + requireDirectory: Boolean, +): Path { + val canonicalProjectRoot = projectRoot.toRealPath() + val configuredPath = canonicalProjectRoot.resolve(relativePath).normalize() + require(configuredPath.startsWith(canonicalProjectRoot)) { + "$kind escapes project checkout: $configuredPath" + } + require(configuredPath.exists()) { "$kind does not exist: $relativePath" } + if (requireDirectory) { + require(configuredPath.isDirectory()) { "$kind is not a directory: $configuredPath" } + } + + val canonicalPath = configuredPath.toRealPath() + require(canonicalPath.startsWith(canonicalProjectRoot)) { + "$kind escapes project checkout through a symbolic link: $configuredPath" + } + + return canonicalPath +} + +internal sealed interface BoundedProcessOutput { + data class Completed( + val exitCode: Int, + val output: String, + val truncated: Boolean, + ) : BoundedProcessOutput + + data object TimedOut : BoundedProcessOutput +} + +internal fun boundedProcessOutput( + command: List, + timeout: Duration, + maxOutputBytes: Int, +): BoundedProcessOutput { + require(timeout > Duration.ZERO) { "Process timeout must be positive" } + require(maxOutputBytes > 0) { "Process output limit must be positive" } + + val outputFile = createSecureProcessOutputFile() + var process: Process? = null + try { + val processStart = TimeSource.Monotonic.markNow() + val startedProcess = ProcessBuilder(command) + .redirectErrorStream(true) + .redirectOutput(outputFile.toFile()) + .start() + process = startedProcess + startedProcess.outputStream.close() + + val remaining = timeout - processStart.elapsedNow() + val completed = remaining > Duration.ZERO && startedProcess.waitFor( + remaining.inWholeMilliseconds.coerceAtLeast(minimumValue = 1), + TimeUnit.MILLISECONDS, + ) + if (!completed) { + terminateProcessTreeBestEffort(startedProcess) + return BoundedProcessOutput.TimedOut + } + + val bytes = Files.newInputStream(outputFile).use { input -> + input.readNBytes(maxOutputBytes + 1) + } + val truncated = bytes.size > maxOutputBytes + val capturedBytes = if (truncated) bytes.copyOf(maxOutputBytes) else bytes + return BoundedProcessOutput.Completed( + exitCode = startedProcess.exitValue(), + output = capturedBytes.toString(StandardCharsets.UTF_8), + truncated = truncated, + ) + } finally { + process?.takeIf(Process::isAlive)?.let(::terminateProcessTreeBestEffort) + runCatching { Files.deleteIfExists(outputFile) } + } +} + +private fun createSecureProcessOutputFile(): Path { + val ownerOnlyPermissions = PosixFilePermissions.asFileAttribute( + setOf(PosixFilePermission.OWNER_READ, PosixFilePermission.OWNER_WRITE), + ) + return try { + Files.createTempFile("unknown-call-census-git-", ".output", ownerOnlyPermissions) + } catch (_: UnsupportedOperationException) { + Files.createTempFile("unknown-call-census-git-", ".output") + } +} + +private fun terminateProcessTree(process: Process) { + val descendants = process.toHandle().descendants().use { handles -> + handles.iterator().asSequence().toList() + } + val processTree = listOf(process.toHandle()) + descendants + processTree.asReversed().forEach(ProcessHandle::destroy) + + if (!awaitTermination(processTree, PROCESS_TERMINATION_GRACE)) { + processTree.asReversed() + .filter(ProcessHandle::isAlive) + .forEach(ProcessHandle::destroyForcibly) + awaitTermination(processTree, PROCESS_TERMINATION_GRACE) + } + + process.waitFor(PROCESS_TERMINATION_GRACE.inWholeMilliseconds, TimeUnit.MILLISECONDS) +} + +private fun terminateProcessTreeBestEffort(process: Process) { + try { + terminateProcessTree(process) + } catch (_: InterruptedException) { + Thread.currentThread().interrupt() + process.destroyForcibly() + } catch (_: Exception) { + process.destroyForcibly() + } +} + +private fun awaitTermination(processes: List, timeout: Duration): Boolean { + val exits = processes.map(ProcessHandle::onExit).toTypedArray() + return try { + CompletableFuture.allOf(*exits).get(timeout.inWholeMilliseconds, TimeUnit.MILLISECONDS) + true + } catch (_: TimeoutException) { + false + } catch (_: ExecutionException) { + false + } catch (_: InterruptedException) { + Thread.currentThread().interrupt() + false + } +} + +private val PROCESS_TERMINATION_GRACE = 500.milliseconds + private fun runtimeArtifactName(type: Class<*>): String = runCatching { Path.of(type.protectionDomain.codeSource.location.toURI()).name }.getOrDefault("unknown") diff --git a/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt b/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt index d1eb3117bf..32f550d2d4 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt @@ -1,10 +1,103 @@ package org.usvm.census +import java.nio.file.Files +import kotlin.io.path.createDirectories +import kotlin.io.path.createTempDirectory import kotlin.test.Test import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.milliseconds import kotlin.time.Duration.Companion.seconds class UnknownCallCensusRunnerTest { + @Test + fun `canonical project checkout accepts a checkout symlink`() { + val temporaryRoot = createTempDirectory("census-path-test-") + try { + val checkoutRoot = temporaryRoot.resolve("checkouts").createDirectories() + val actualProjectRoot = temporaryRoot.resolve("project").createDirectories() + Files.createSymbolicLink(checkoutRoot.resolve("project"), actualProjectRoot) + + val canonicalPath = canonicalProjectCheckout( + checkoutRoot = checkoutRoot, + relativePath = "project", + ) + + assertEquals(actualProjectRoot.toRealPath(), canonicalPath) + } finally { + temporaryRoot.toFile().deleteRecursively() + } + } + + @Test + fun `canonical project path accepts an in-root directory`() { + val temporaryRoot = createTempDirectory("census-path-test-") + try { + val projectRoot = temporaryRoot.resolve("project").createDirectories() + val sourceRoot = projectRoot.resolve("src").createDirectories() + + val canonicalPath = canonicalExistingProjectPath( + projectRoot = projectRoot, + relativePath = "src", + kind = "Configured source root", + requireDirectory = true, + ) + + assertEquals(sourceRoot.toRealPath(), canonicalPath) + } finally { + temporaryRoot.toFile().deleteRecursively() + } + } + + @Test + fun `canonical project path rejects a symbolic-link escape`() { + val temporaryRoot = createTempDirectory("census-path-test-") + try { + val projectRoot = temporaryRoot.resolve("project").createDirectories() + val externalRoot = temporaryRoot.resolve("external").createDirectories() + Files.createSymbolicLink(projectRoot.resolve("escaped"), externalRoot) + + val error = assertFailsWith { + canonicalExistingProjectPath( + projectRoot = projectRoot, + relativePath = "escaped", + kind = "Configured source root", + requireDirectory = true, + ) + } + + assertTrue(error.message.orEmpty().contains("symbolic link")) + } finally { + temporaryRoot.toFile().deleteRecursively() + } + } + + @Test + fun `bounded process output reports truncation`() { + val result = boundedProcessOutput( + command = listOf("sh", "-c", "printf 1234567890"), + timeout = 2.seconds, + maxOutputBytes = 5, + ) + + val completed = assertIs(result) + assertEquals("12345", completed.output) + assertTrue(completed.truncated) + } + + @Test + fun `bounded process output times out and reaps the process`() { + val result = boundedProcessOutput( + command = listOf("sh", "-c", "sleep 30"), + timeout = 100.milliseconds, + maxOutputBytes = 1_024, + ) + + assertEquals(BoundedProcessOutput.TimedOut, result) + } + @Test fun `elapsed timeout preserves a partial failure`() { val outcome = methodOutcomeAfterTimeoutCheck( From ca179d37a2e911201e7d9180eff37b689f52514c Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 20 Sep 2026 00:40:07 +0300 Subject: [PATCH 08/10] Bound census subprocess output while running --- .../usvm/census/UnknownCallCensusRunner.kt | 112 +++++++++++++++--- .../census/UnknownCallCensusRunnerTest.kt | 45 +++++-- 2 files changed, 129 insertions(+), 28 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt index b3d9c566af..c0932a6d97 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt @@ -28,12 +28,12 @@ import org.usvm.machine.call.TsUnknownCallDecision import org.usvm.machine.call.TsUnknownCallEvent import org.usvm.machine.call.TsUnknownCallModelSelection import java.io.BufferedWriter +import java.io.IOException +import java.io.InputStream import java.nio.charset.StandardCharsets import java.nio.file.Files import java.nio.file.Path import java.nio.file.StandardOpenOption -import java.nio.file.attribute.PosixFilePermission -import java.nio.file.attribute.PosixFilePermissions import java.security.MessageDigest import java.time.Instant import java.util.concurrent.CompletableFuture @@ -616,17 +616,26 @@ internal fun boundedProcessOutput( require(timeout > Duration.ZERO) { "Process timeout must be positive" } require(maxOutputBytes > 0) { "Process output limit must be positive" } - val outputFile = createSecureProcessOutputFile() var process: Process? = null + var outputReader: Thread? = null try { val processStart = TimeSource.Monotonic.markNow() val startedProcess = ProcessBuilder(command) .redirectErrorStream(true) - .redirectOutput(outputFile.toFile()) .start() process = startedProcess startedProcess.outputStream.close() + val outputCollector = BoundedOutputCollector(maxOutputBytes) + val startedOutputReader = Thread( + { outputCollector.drain(startedProcess.inputStream) }, + "unknown-call-census-output-reader", + ).apply { + isDaemon = true + start() + } + outputReader = startedOutputReader + val remaining = timeout - processStart.elapsedNow() val completed = remaining > Duration.ZERO && startedProcess.waitFor( remaining.inWholeMilliseconds.coerceAtLeast(minimumValue = 1), @@ -634,34 +643,98 @@ internal fun boundedProcessOutput( ) if (!completed) { terminateProcessTreeBestEffort(startedProcess) + closeProcessOutputBestEffort(startedProcess) + joinBestEffort(startedOutputReader, PROCESS_TERMINATION_GRACE) return BoundedProcessOutput.TimedOut } - val bytes = Files.newInputStream(outputFile).use { input -> - input.readNBytes(maxOutputBytes + 1) + val outputRead = joinWithinTimeout( + thread = startedOutputReader, + timeout = timeout - processStart.elapsedNow(), + ) + if (!outputRead) { + closeProcessOutputBestEffort(startedProcess) + joinBestEffort(startedOutputReader, PROCESS_TERMINATION_GRACE) + return BoundedProcessOutput.TimedOut } - val truncated = bytes.size > maxOutputBytes - val capturedBytes = if (truncated) bytes.copyOf(maxOutputBytes) else bytes + + outputCollector.failure?.let { throw it } return BoundedProcessOutput.Completed( exitCode = startedProcess.exitValue(), - output = capturedBytes.toString(StandardCharsets.UTF_8), - truncated = truncated, + output = outputCollector.output(), + truncated = outputCollector.truncated, ) } finally { process?.takeIf(Process::isAlive)?.let(::terminateProcessTreeBestEffort) - runCatching { Files.deleteIfExists(outputFile) } + process?.let(::closeProcessOutputBestEffort) + outputReader?.takeIf(Thread::isAlive)?.let { reader -> + joinBestEffort(reader, PROCESS_TERMINATION_GRACE) + } } } -private fun createSecureProcessOutputFile(): Path { - val ownerOnlyPermissions = PosixFilePermissions.asFileAttribute( - setOf(PosixFilePermission.OWNER_READ, PosixFilePermission.OWNER_WRITE), - ) - return try { - Files.createTempFile("unknown-call-census-git-", ".output", ownerOnlyPermissions) - } catch (_: UnsupportedOperationException) { - Files.createTempFile("unknown-call-census-git-", ".output") +private class BoundedOutputCollector(private val maxOutputBytes: Int) { + private val retainedOutput = ByteArray(maxOutputBytes) + private var retainedBytes = 0 + + var truncated: Boolean = false + private set + + var failure: Exception? = null + private set + + fun drain(input: InputStream) { + val buffer = ByteArray(PROCESS_OUTPUT_BUFFER_BYTES) + try { + input.use { + var readBytes = it.read(buffer) + while (readBytes >= 0) { + retain(buffer, readBytes) + readBytes = it.read(buffer) + } + } + } catch (error: IOException) { + failure = error + } } + + private fun retain(buffer: ByteArray, readBytes: Int) { + val retainedFromChunk = minOf(readBytes, maxOutputBytes - retainedBytes) + if (retainedFromChunk > 0) { + buffer.copyInto( + destination = retainedOutput, + destinationOffset = retainedBytes, + endIndex = retainedFromChunk, + ) + retainedBytes += retainedFromChunk + } + if (retainedFromChunk < readBytes) { + truncated = true + } + } + + fun output(): String = retainedOutput.copyOf(retainedBytes).toString(StandardCharsets.UTF_8) +} + +private fun joinWithinTimeout(thread: Thread, timeout: Duration): Boolean { + if (timeout <= Duration.ZERO) { + return !thread.isAlive + } + + thread.join(timeout.inWholeMilliseconds.coerceAtLeast(minimumValue = 1)) + return !thread.isAlive +} + +private fun joinBestEffort(thread: Thread, timeout: Duration) { + try { + joinWithinTimeout(thread, timeout) + } catch (_: InterruptedException) { + Thread.currentThread().interrupt() + } +} + +private fun closeProcessOutputBestEffort(process: Process) { + runCatching { process.inputStream.close() } } private fun terminateProcessTree(process: Process) { @@ -708,6 +781,7 @@ private fun awaitTermination(processes: List, timeout: Duration): } private val PROCESS_TERMINATION_GRACE = 500.milliseconds +private const val PROCESS_OUTPUT_BUFFER_BYTES = 8 * 1024 private fun runtimeArtifactName(type: Class<*>): String = runCatching { Path.of(type.protectionDomain.codeSource.location.toURI()).name diff --git a/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt b/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt index 32f550d2d4..3dd99516b6 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt @@ -6,10 +6,12 @@ import kotlin.io.path.createTempDirectory import kotlin.test.Test import kotlin.test.assertEquals import kotlin.test.assertFailsWith +import kotlin.test.assertFalse import kotlin.test.assertIs import kotlin.test.assertTrue import kotlin.time.Duration.Companion.milliseconds import kotlin.time.Duration.Companion.seconds +import kotlin.time.TimeSource class UnknownCallCensusRunnerTest { @Test @@ -75,27 +77,52 @@ class UnknownCallCensusRunnerTest { } @Test - fun `bounded process output reports truncation`() { + fun `bounded process output drains excess while producer remains alive`() { val result = boundedProcessOutput( - command = listOf("sh", "-c", "printf 1234567890"), - timeout = 2.seconds, + command = listOf( + "sh", + "-c", + "yes 1234567890 | head -n 20000; sleep 0.1; printf done", + ), + timeout = 5.seconds, maxOutputBytes = 5, ) val completed = assertIs(result) + assertEquals(0, completed.exitCode) assertEquals("12345", completed.output) assertTrue(completed.truncated) } @Test fun `bounded process output times out and reaps the process`() { - val result = boundedProcessOutput( - command = listOf("sh", "-c", "sleep 30"), - timeout = 100.milliseconds, - maxOutputBytes = 1_024, - ) + val temporaryRoot = createTempDirectory("census-process-test-") + try { + val childPidFile = temporaryRoot.resolve("child.pid") + val start = TimeSource.Monotonic.markNow() + val result = boundedProcessOutput( + command = listOf( + "sh", + "-c", + "sleep 30 & child=\$!; printf %s \"\$child\" > \"\$1\"; wait", + "census-timeout-test", + childPidFile.toString(), + ), + timeout = 500.milliseconds, + maxOutputBytes = 1_024, + ) - assertEquals(BoundedProcessOutput.TimedOut, result) + assertEquals(BoundedProcessOutput.TimedOut, result) + assertTrue(start.elapsedNow() < 3.seconds) + + val childPid = Files.readString(childPidFile).toLong() + val childIsAlive = ProcessHandle.of(childPid) + .map(ProcessHandle::isAlive) + .orElse(false) + assertFalse(childIsAlive) + } finally { + temporaryRoot.toFile().deleteRecursively() + } } @Test From c1e07845c393374f743220dfe7febb4bc208c3b4 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 20 Sep 2026 12:03:39 +0300 Subject: [PATCH 09/10] Use coverage-guided census sampling --- .../experiments/unknown-call-census/README.md | 4 +- .../development-corpus.json | 11 +- .../usvm/census/UnknownCallCensusArtifacts.kt | 5 +- .../usvm/census/UnknownCallCensusRunner.kt | 178 ++++++++++++++---- .../census/UnknownCallCensusRunnerTest.kt | 21 +++ 5 files changed, 179 insertions(+), 40 deletions(-) diff --git a/usvm-ts/experiments/unknown-call-census/README.md b/usvm-ts/experiments/unknown-call-census/README.md index 14ef92ea4b..ac4b45f1a2 100644 --- a/usvm-ts/experiments/unknown-call-census/README.md +++ b/usvm-ts/experiments/unknown-call-census/README.md @@ -1,8 +1,8 @@ # TypeScript unknown-call development census -This census measures unknown-call events on a frozen development corpus. The projects and revisions were selected before current measurements and come from the historical TypeScript experiment corpus. They are development evidence and must not be reused as held-out evaluation projects. The manifest admits only `.ts` entry files, excludes declarations and common test suffixes, excludes synthetic anonymous and initializer entry methods, sorts stable repository-relative file/function identities, and takes the bounded entry-file prefix recorded in `limits`. The execution scene retains every loaded support file so the entry-file bound does not remove imported callees. Unknown calls reached inside nested source functions retain their actual containing-function identity. +This census measures unknown-call events on a frozen development corpus. The projects and revisions were selected before current measurements and come from the historical TypeScript experiment corpus. They are development evidence and must not be reused as held-out evaluation projects. The manifest admits only `.ts` entry files, excludes declarations and common test suffixes, and excludes synthetic anonymous and initializer entry methods. A class is eligible when it contains at least `minMethodsPerClass` methods with at least `minStatementsPerMethod` IR statements. That threshold qualifies the class but does not discard its shorter ordinary methods. Eligible classes and their methods are ordered by stable SHA-256 ranks derived from the manifest seed and repository-relative identities. Methods are then taken round-robin across the selected classes, so `maxMethods` does not collapse the sample onto the first large class. The execution scene retains every loaded support file. Unknown calls reached inside nested source functions retain their actual containing-function identity. -The primary profile disables every optional unknown-call model and uses `FRESH_SYMBOLIC_RETURN`. Mandatory engine semantics and the legacy approximations that run before unknown-call dispatch remain enabled and identical across profiles. Therefore this census measures observed unknown-call decisions, not every call handled approximately by the engine. The raw artifact keeps every repeated event, while the summary separately deduplicates containing functions and stable source sites. A stable source site can contain multiple lowered IR calls; raw records retain the statement index and callee identity. Method results distinguish complete analysis from partial analysis stopped by an engine or recording failure. Existing `ts.array.shift` and `ts.array.pop` models validate the mechanism but are not described as census-selected. +The primary profile disables every optional unknown-call model and uses `FRESH_SYMBOLIC_RETURN`. Search uses `CLOSEST_TO_UNCOVERED_RANDOM` with the manifest seed and does not stop merely because the entry method reaches 100% statement coverage. Mandatory engine semantics and the legacy approximations that run before unknown-call dispatch remain enabled and identical across profiles. Therefore this census measures observed unknown-call decisions, not every call handled approximately by the engine. The raw artifact keeps every repeated event, while the summary separately deduplicates containing functions and stable source sites. A stable source site can contain multiple lowered IR calls; raw records retain the statement index and callee identity. Method results distinguish analysis that returned normally from partial analysis stopped by an engine or recording failure; a normal return does not claim exhaustive behavior outside the configured budgets and engine semantics. Existing `ts.array.shift` and `ts.array.pop` models validate the mechanism but are not described as census-selected. Prepare each repository below `CHECKOUT_ROOT` at the exact revision recorded in `development-corpus.json`, then run: diff --git a/usvm-ts/experiments/unknown-call-census/development-corpus.json b/usvm-ts/experiments/unknown-call-census/development-corpus.json index 0730213e8e..b491f520d3 100644 --- a/usvm-ts/experiments/unknown-call-census/development-corpus.json +++ b/usvm-ts/experiments/unknown-call-census/development-corpus.json @@ -66,10 +66,13 @@ "profiles": [ "EMPTY_FRESH" ], + "randomSeed": 0, "limits": { - "projectTimeoutSeconds": 300, - "methodTimeoutSeconds": 5, - "maxFiles": 20, - "maxMethods": 40 + "projectTimeoutSeconds": 900, + "methodTimeoutSeconds": 30, + "maxClasses": 40, + "maxMethods": 40, + "minMethodsPerClass": 1, + "minStatementsPerMethod": 8 } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusArtifacts.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusArtifacts.kt index c4e1d06173..c6aa0b3c1a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusArtifacts.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusArtifacts.kt @@ -20,6 +20,7 @@ internal data class UnknownCallCensusManifest( val schemaVersion: Int, val projects: List, val profiles: List = listOf(UnknownCallCensusProfile.EMPTY_FRESH), + val randomSeed: Long = 0, val limits: UnknownCallCensusLimits = UnknownCallCensusLimits(), ) @@ -46,8 +47,10 @@ internal enum class UnknownCallCensusProfile { internal data class UnknownCallCensusLimits( val projectTimeoutSeconds: Long = 300, val methodTimeoutSeconds: Long = 10, - val maxFiles: Int = 100, + val maxClasses: Int = 100, val maxMethods: Int = 1_000, + val minMethodsPerClass: Int = 1, + val minStatementsPerMethod: Int = 1, ) @Serializable diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt index c0932a6d97..514eac2a61 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt @@ -4,6 +4,7 @@ import kotlinx.serialization.encodeToString import kotlinx.serialization.json.JsonObject import kotlinx.serialization.json.buildJsonObject import kotlinx.serialization.json.put +import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsMethod @@ -12,12 +13,14 @@ import org.jacodb.ets.model.EtsNamespaceSignature import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsSourceSpan import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX +import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.EtsIrGenerationException import org.jacodb.ets.utils.EtsIrProvider import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME import org.jacodb.ets.utils.generateEtsIR import org.jacodb.ets.utils.loadEtsProjectFromIR +import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.UMachineOptions import org.usvm.machine.TsInterpreterObserver @@ -130,7 +133,7 @@ internal class UnknownCallCensusRunner( ) val loadedFiles = loadProjectFiles(project, projectRoot, projectStart, projectTimeout) - val entryFiles = selectFiles(project, loadedFiles) + val selection = selectMethods(project, projectRoot, loadedFiles) val sceneFiles = loadedFiles.files .distinctBy { file -> requireNotNull(loadedFiles.pathsBySignature[file.signature]) } .sortedBy { file -> requireNotNull(loadedFiles.pathsBySignature[file.signature]) } @@ -138,16 +141,7 @@ internal class UnknownCallCensusRunner( projectFiles = sceneFiles, projectName = project.id, ) - val methods = entryFiles - .flatMap { it.allClasses } - .flatMap { it.methods } - .filterNot { it.cfg.stmts.isEmpty() } - .filterNot { it.name.startsWith(ANONYMOUS_METHOD_PREFIX) } - .filterNot { it.name == DEFAULT_FILE_METHOD_NAME } - .filterNot { it.name == INSTANCE_INIT_METHOD_NAME } - .filterNot { it.name == STATIC_INIT_METHOD_NAME } - .sortedBy { functionId(project.id, projectRoot, it.signature, loadedFiles.pathsBySignature) } - .take(manifest.limits.maxMethods) + val methods = selection.methods var rawEvents = 0 var completedMethods = 0 @@ -186,7 +180,9 @@ internal class UnknownCallCensusRunner( put("kind", "project_result") put("status", if (projectTimedOut) "timeout" else "completed") put("sceneFiles", sceneFiles.size) - put("filesSelected", entryFiles.size) + put("candidateFiles", selection.candidateFiles) + put("eligibleClasses", selection.eligibleClasses) + put("classesSelected", selection.selectedClasses) put("methodsSelected", methods.size) put("methodsCompleted", completedMethods) put("methodsPartial", partialMethods) @@ -246,7 +242,9 @@ internal class UnknownCallCensusRunner( ) val methodTimeout = manifest.limits.methodTimeoutSeconds.seconds val machineOptions = UMachineOptions( - randomSeed = 0, + pathSelectionStrategies = listOf(CENSUS_PATH_SELECTION_STRATEGY), + randomSeed = manifest.randomSeed, + stopOnCoverage = CENSUS_STOP_ON_COVERAGE, timeout = methodTimeout, solverType = SolverType.YICES, throwExceptionOnStepFailure = true, @@ -324,18 +322,82 @@ internal class UnknownCallCensusRunner( return MethodRunResult(status = status, events = observer.eventCount) } - private fun selectFiles( + private fun selectMethods( project: UnknownCallCensusProject, + projectRoot: Path, loadedFiles: LoadedProjectFiles, - ): List = loadedFiles.files.asSequence() - .map { file -> file to requireNotNull(loadedFiles.pathsBySignature[file.signature]) } - .filter { (_, fileName) -> project.includeSuffixes.any(fileName::endsWith) } - .filterNot { (_, fileName) -> project.excludeSuffixes.any(fileName::endsWith) } - .distinctBy { (_, fileName) -> fileName } - .sortedBy { (_, fileName) -> fileName } - .take(manifest.limits.maxFiles) - .map { (file, _) -> file } - .toList() + ): SelectedMethods { + val candidateFiles = loadedFiles.files.asSequence() + .map { file -> file to requireNotNull(loadedFiles.pathsBySignature[file.signature]) } + .filter { (_, fileName) -> project.includeSuffixes.any(fileName::endsWith) } + .filterNot { (_, fileName) -> project.excludeSuffixes.any(fileName::endsWith) } + .distinctBy { (_, fileName) -> fileName } + .sortedBy { (_, fileName) -> fileName } + .map { (file, _) -> file } + .toList() + + val eligibleClasses = candidateFiles + .flatMap { file -> file.allClasses } + .map { clazz -> + val classId = classId(project.id, projectRoot, clazz.signature, loadedFiles.pathsBySignature) + val methods = clazz.methods + .asSequence() + .filterNot { method -> method.cfg.stmts.isEmpty() } + .filterNot { method -> method.name.startsWith(ANONYMOUS_METHOD_PREFIX) } + .filterNot { method -> method.name == DEFAULT_ARK_METHOD_NAME } + .filterNot { method -> method.name == INSTANCE_INIT_METHOD_NAME } + .filterNot { method -> method.name == STATIC_INIT_METHOD_NAME } + .sortedWith( + compareBy( + { method -> + stableSelectionRank( + seed = manifest.randomSeed, + identity = functionId( + project.id, + projectRoot, + method.signature, + loadedFiles.pathsBySignature, + ), + ) + }, + { method -> + functionId( + project.id, + projectRoot, + method.signature, + loadedFiles.pathsBySignature, + ) + }, + ) + ) + .toList() + + SelectedClass(classId = classId, methods = methods) + } + .filter { selectedClass -> + selectedClass.methods.count { method -> + method.cfg.stmts.size >= manifest.limits.minStatementsPerMethod + } >= manifest.limits.minMethodsPerClass + } + + val selectedClasses = eligibleClasses + .sortedWith( + compareBy( + { selectedClass -> stableSelectionRank(manifest.randomSeed, selectedClass.classId) }, + SelectedClass::classId, + ) + ) + .take(manifest.limits.maxClasses) + val selectedMethods = roundRobin(selectedClasses.map(SelectedClass::methods)) + .take(manifest.limits.maxMethods) + + return SelectedMethods( + candidateFiles = candidateFiles.size, + eligibleClasses = eligibleClasses.size, + selectedClasses = selectedClasses.size, + methods = selectedMethods, + ) + } private fun loadProjectFiles( project: UnknownCallCensusProject, @@ -435,8 +497,10 @@ internal class UnknownCallCensusRunner( } require(manifest.limits.projectTimeoutSeconds > 0) { "Project timeout must be positive" } require(manifest.limits.methodTimeoutSeconds > 0) { "Method timeout must be positive" } - require(manifest.limits.maxFiles > 0) { "File limit must be positive" } + require(manifest.limits.maxClasses > 0) { "Class limit must be positive" } require(manifest.limits.maxMethods > 0) { "Method limit must be positive" } + require(manifest.limits.minMethodsPerClass > 0) { "Minimum methods per class must be positive" } + require(manifest.limits.minStatementsPerMethod > 0) { "Minimum statements per method must be positive" } val fullGitRevision = Regex("[0-9a-fA-F]{40}") manifest.projects.forEach { project -> require(project.id.isNotBlank()) { "Census project ID must not be blank" } @@ -475,13 +539,17 @@ internal class UnknownCallCensusRunner( put("frontendProvider", EtsIrProvider.TS_FRONTEND.name) put("solver", SolverType.YICES.name) put("javaVersion", System.getProperty("java.version")) - put("randomSeed", 0) + put("pathSelectionStrategy", CENSUS_PATH_SELECTION_STRATEGY.name) + put("randomSeed", manifest.randomSeed) + put("stopOnCoverage", CENSUS_STOP_ON_COVERAGE) put("unknownCallModelSelection", "NONE") put("legacyApproximationPolicy", "UNCHANGED") put("projectTimeoutSeconds", manifest.limits.projectTimeoutSeconds) put("methodTimeoutSeconds", manifest.limits.methodTimeoutSeconds) - put("maxFiles", manifest.limits.maxFiles) + put("maxClasses", manifest.limits.maxClasses) put("maxMethods", manifest.limits.maxMethods) + put("minMethodsPerClass", manifest.limits.minMethodsPerClass) + put("minStatementsPerMethod", manifest.limits.minStatementsPerMethod) } private fun validateRevision(projectRoot: Path, expectedRevision: String, timeout: Duration) { @@ -549,10 +617,6 @@ internal class UnknownCallCensusRunner( } } - private fun sha256(bytes: ByteArray): String = MessageDigest.getInstance("SHA-256") - .digest(bytes) - .joinToString(separator = "") { byte -> "%02x".format(byte) } - private companion object { const val RAW_FILE_NAME = "raw.jsonl" const val SUMMARY_FILE_NAME = "summary.json" @@ -900,6 +964,18 @@ private data class LoadedProjectFiles( val pathsBySignature: Map, ) +private data class SelectedClass( + val classId: String, + val methods: List, +) + +private data class SelectedMethods( + val candidateFiles: Int, + val eligibleClasses: Int, + val selectedClasses: Int, + val methods: List, +) + private val UnknownCallCensusProfile.fallback: TsResidualCallPolicy get() = when (this) { UnknownCallCensusProfile.EMPTY_FRESH -> TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN @@ -934,6 +1010,18 @@ private fun functionId( return "$projectId:$sourceFile:${signatureKey(signature)}" } +private fun classId( + projectId: String, + projectRoot: Path, + signature: EtsClassSignature, + pathsBySignature: Map, +): String { + val sourceFile = sourcePath(signature.file, projectRoot, pathsBySignature) + val namespace = signature.namespace?.qualifiedName() + val className = listOfNotNull(namespace, signature.name).joinToString(separator = "::") + return "$projectId:$sourceFile:$className" +} + private fun calleeId( projectRoot: Path, signature: EtsMethodSignature, @@ -947,8 +1035,14 @@ private fun sourcePath( signature: EtsMethodSignature, projectRoot: Path, pathsBySignature: Map, -): String = pathsBySignature[signature.enclosingClass.file] - ?: normalizedSourcePath(signature.enclosingClass.file.fileName, projectRoot) +): String = sourcePath(signature.enclosingClass.file, projectRoot, pathsBySignature) + +private fun sourcePath( + signature: EtsFileSignature, + projectRoot: Path, + pathsBySignature: Map, +): String = pathsBySignature[signature] + ?: normalizedSourcePath(signature.fileName, projectRoot) private fun signatureKey(signature: EtsMethodSignature): String { val parameters = signature.parameters.joinToString(separator = ",") { parameter -> parameter.type.toString() } @@ -1002,6 +1096,23 @@ private fun repositoryRelativeSourcePath( private fun String.normalizedSeparators(): String = replace('\\', '/') +internal fun stableSelectionRank(seed: Long, identity: String): String = sha256( + "$seed\u0000$identity".toByteArray(StandardCharsets.UTF_8) +) + +internal fun roundRobin(groups: List>): List { + val maxGroupSize = groups.maxOfOrNull(List::size) ?: return emptyList() + return buildList { + repeat(maxGroupSize) { index -> + groups.forEach { group -> group.getOrNull(index)?.let(::add) } + } + } +} + +private fun sha256(bytes: ByteArray): String = MessageDigest.getInstance("SHA-256") + .digest(bytes) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + private fun boundedError(error: Throwable): String { val type = error::class.qualifiedName ?: error::class.simpleName ?: "Throwable" val message = error.message @@ -1020,5 +1131,6 @@ private fun combineErrors(primary: String?, additional: String?): String? = when private class ProjectTimeoutException(message: String, cause: Throwable? = null) : RuntimeException(message, cause) private const val MAX_ERROR_LENGTH = 1_000 -private const val DEFAULT_FILE_METHOD_NAME = "%dflt" +private const val CENSUS_STOP_ON_COVERAGE = 0 +private val CENSUS_PATH_SELECTION_STRATEGY = PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM private val JVM_IDENTITY_SUFFIX = Regex("@[0-9a-fA-F]{6,16}") diff --git a/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt b/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt index 3dd99516b6..7c07d66f35 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/census/UnknownCallCensusRunnerTest.kt @@ -150,4 +150,25 @@ class UnknownCallCensusRunnerTest { assertEquals(MethodStatus.TIMEOUT, outcome.status) assertEquals("Machine timeout reached", outcome.error) } + + @Test + fun `stable selection rank is reproducible and seed dependent`() { + val rank = stableSelectionRank(seed = 0, identity = "project:file:Class") + + assertEquals(rank, stableSelectionRank(seed = 0, identity = "project:file:Class")) + assertTrue(rank != stableSelectionRank(seed = 1, identity = "project:file:Class")) + } + + @Test + fun `round robin selects across classes before taking later methods`() { + val methodsByClass = listOf( + listOf("a1", "a2", "a3"), + listOf("b1"), + listOf("c1", "c2"), + ) + + val methods = roundRobin(methodsByClass) + + assertEquals(listOf("a1", "b1", "c1", "a2", "c2", "a3"), methods) + } } From ad7d4e56f08638ec78455f5ef69c48c8e773a2b1 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 20 Sep 2026 12:30:45 +0300 Subject: [PATCH 10/10] Document seeded census results --- .../unknown-call-census/MODEL_SELECTION.md | 16 +- .../experiments/unknown-call-census/README.md | 2 + .../org/usvm/census/CensusMethodSelection.kt | 98 +++ .../usvm/census/UnknownCallCensusProcess.kt | 237 +++++++ .../usvm/census/UnknownCallCensusRecording.kt | 280 ++++++++ .../usvm/census/UnknownCallCensusRunner.kt | 600 +----------------- 6 files changed, 633 insertions(+), 600 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/census/CensusMethodSelection.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusProcess.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRecording.kt diff --git a/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md b/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md index dec09468b7..ce9640fff7 100644 --- a/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md +++ b/usvm-ts/experiments/unknown-call-census/MODEL_SELECTION.md @@ -1,15 +1,15 @@ # Finite development model selection -Selection frozen on 2026-09-19 before any held-out TS Calls evaluation. This is a development decision for a small pilot, not evidence that the selected models improve coverage. +Selection was frozen on 2026-09-19 before any held-out TS Calls evaluation. This is a development decision from a three-project pilot, not evidence that the selected models improve coverage. ## Evidence used - Approximation audit #368 at `303409613c30ea5dcdabc1f97ac8092d753765b1`, which audits current source `41961f7b66c30c8a2a7507c67a79396f495f4520` and historical source `3728ba45ab092422e2cb2e57ed6fe2377425b622`. -- The frozen development manifest in `development-corpus.json` and its corrected primary `EMPTY_FRESH` census at tool commit `b04a8ed16410fd3c5e8bc049304f9b649c11ee48`. It attempted the same 79 entry functions from three pinned projects: 43 completed, 35 ended with explicit partial-analysis diagnostics, one timed out, and none ended with a boundary tool error. It observed 82 repeated events at 26 stable source sites in 19 containing functions. The generated and standalone-regenerated summaries are byte-identical with SHA-256 `bf52a4cf5f03f867f594990c1f458ddb1d244c01679bf3a1fd852019aa3ce145`. -- Stable-source-site prevalence rather than repeated loop-event totals. The largest corrected groups were `BSTreeKV.compare` (24 events, 3 sites), the built-in array `pop` reached inside the restored project `Stack.pop` body (10 events, 1 site), `charAt` (7 events, 2 sites), `parseInt` (7 events, 2 sites), and callbacks (6 events, 3 sites). No built-in `Array.shift` site was observed. The high partial-analysis count limits prevalence interpretation. -- The first local pilot attempted the same functions but produced 768 events at 41 sites. Review found that its entry-file bound removed imported support files and that swallowed interpreter failures appeared completed. Its preserved raw artifact is preliminary diagnostic evidence only; in particular, its 52 project `Stack` resolution events were harness-induced and are excluded from selection evidence. +- The frozen development manifest in `development-corpus.json` and the primary `EMPTY_FRESH` census at tool commit `c1e07845c393374f743220dfe7febb4bc208c3b4`, tree `bc524f2b9ba451b378db1bce362722a7b534c931`. It analyzed 97 entry functions from three pinned projects: 45 completed, 36 ended with explicit partial-analysis diagnostics, 16 reached the 30-second method timeout, and none ended with a boundary tool error. It observed 7,002 repeated events at 36 stable source sites in 26 containing functions. +- The sample covered 11 source files in TheAlgorithms/TypeScript, 37 in javascript-datastructures-algorithms, and 14 in typescript-collections. Stable sites were distributed 9, 7, and 20 across those projects. This replaces the obsolete lexicographic/BFS run, whose result is diagnostic only and is excluded from selection evidence. +- Stable-source-site prevalence rather than repeated loop-event totals. The largest groups were iterator `Symbol.iterator` and `next` (4 sites each), `Error` construction (4), `Object.keys` (3), iterator `has` (3), and the project callback `Heap.compare` (3). Built-in array `pop` occurred at one source site; no built-in `Array.shift` site was observed. The 1,918 repeated `pop` events and 3,630 repeated `FactoryDictionary.defaultFactoryFunction` events arise from repeated exploration and must not be read as independent prevalence observations. -The primary profile disables optional catalog models but leaves mandatory semantics and legacy pre-dispatch approximations unchanged. Therefore the census is an inventory of observed unknown-call decisions, not every approximate or unresolved call in the engine. Tool errors, timeouts, and omitted call-resolution candidate tails also limit prevalence interpretation. +The primary profile disables optional catalog models but leaves mandatory semantics and legacy pre-dispatch approximations unchanged. Therefore the census is an inventory of observed unknown-call decisions, not every approximate or unresolved call in the engine. The 36 partial analyses, 16 timeouts, three-project scope, and omitted call-resolution candidate tails limit prevalence interpretation. Additional development projects must be pinned before their results are inspected; held-out projects remain separate and cannot influence model selection. ## Decision @@ -34,9 +34,11 @@ This is an acceptable no-new-family result. A later family requires a separate b ## Content identity -At accepted #380 source `3134d06515bca61ba2a357a67697ac8620b0e420` and corrected census tool tree `f9ba380951630b62ef55e7aae7d90f2fab55298b`: +At accepted #380 source `3134d06515bca61ba2a357a67697ac8620b0e420`: - `ArrayModels.ts` source SHA-256: `9f40d3abce58e3412a0206eabd9fdb0547e12c2ebd832ce48b260b3339518e26`. - `TsArrayShiftIntrinsicModel.kt` SHA-256: `ff6dd634cf660c83e203b82c927a28e88859f0bc6b9f24bec2fa97d738dc9e11`. -The corrected run used JacoDB `ddb127d9ef`, the native `TS_FRONTEND`, Yices, OpenJDK 21.0.12, Node 26.5.0, random seed 0, a 300-second project budget, a 5-second method budget, at most 20 entry files and 40 entry methods per project. Its run metadata records `unknownCallModelSelection` as `NONE`. `ts.array.shift` has no EtsIR artifact. For `ts.array.pop`, the generated `etsIrHash` remains unavailable from the built-in wrapper and must not be invented. +The accepted run used JacoDB `ddb127d9ef`, the native `TS_FRONTEND`, Yices, OpenJDK 21.0.12, Node 26.5.0, random seed 0, `CLOSEST_TO_UNCOVERED_RANDOM`, no coverage-based early stop, a 900-second project budget, and a 30-second method budget. A class qualified when it had at least one ordinary method with at least eight IR statements. Up to 40 classes and 40 methods were selected per project by stable seeded ranks and class round-robin. The raw artifact SHA-256 is `a091dff2d393e131a83e76cc71af51dd38dcd821e2e01ee007cfe8aa56ab6c08`; the generated and standalone-regenerated summaries are byte-identical with SHA-256 `7c59fbfa09af54de1e74ed65f4c762629013688d109305a970b421ee32781d00`; the manifest SHA-256 is `4adba5861339782e1f514f01525561a67aa9f01a6abe914b3d371ff77e1c1bbb`. + +Run metadata records `unknownCallModelSelection` as `NONE`. `ts.array.shift` has no EtsIR artifact. For `ts.array.pop`, the generated `etsIrHash` remains unavailable from the built-in wrapper and must not be invented. diff --git a/usvm-ts/experiments/unknown-call-census/README.md b/usvm-ts/experiments/unknown-call-census/README.md index ac4b45f1a2..46d637c07c 100644 --- a/usvm-ts/experiments/unknown-call-census/README.md +++ b/usvm-ts/experiments/unknown-call-census/README.md @@ -2,6 +2,8 @@ This census measures unknown-call events on a frozen development corpus. The projects and revisions were selected before current measurements and come from the historical TypeScript experiment corpus. They are development evidence and must not be reused as held-out evaluation projects. The manifest admits only `.ts` entry files, excludes declarations and common test suffixes, and excludes synthetic anonymous and initializer entry methods. A class is eligible when it contains at least `minMethodsPerClass` methods with at least `minStatementsPerMethod` IR statements. That threshold qualifies the class but does not discard its shorter ordinary methods. Eligible classes and their methods are ordered by stable SHA-256 ranks derived from the manifest seed and repository-relative identities. Methods are then taken round-robin across the selected classes, so `maxMethods` does not collapse the sample onto the first large class. The execution scene retains every loaded support file. Unknown calls reached inside nested source functions retain their actual containing-function identity. +The three-project manifest is a reproducible development pilot, not the final corpus. Extend it by pinning additional projects and changing the seed or limits before inspecting their census results. Freeze that expanded development manifest before using it to revise the model catalog. Keep held-out evaluation projects in a separate manifest and never use their outcomes to choose models or tune these thresholds. + The primary profile disables every optional unknown-call model and uses `FRESH_SYMBOLIC_RETURN`. Search uses `CLOSEST_TO_UNCOVERED_RANDOM` with the manifest seed and does not stop merely because the entry method reaches 100% statement coverage. Mandatory engine semantics and the legacy approximations that run before unknown-call dispatch remain enabled and identical across profiles. Therefore this census measures observed unknown-call decisions, not every call handled approximately by the engine. The raw artifact keeps every repeated event, while the summary separately deduplicates containing functions and stable source sites. A stable source site can contain multiple lowered IR calls; raw records retain the statement index and callee identity. Method results distinguish analysis that returned normally from partial analysis stopped by an engine or recording failure; a normal return does not claim exhaustive behavior outside the configured budgets and engine semantics. Existing `ts.array.shift` and `ts.array.pop` models validate the mechanism but are not described as census-selected. Prepare each repository below `CHECKOUT_ROOT` at the exact revision recorded in `development-corpus.json`, then run: diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/CensusMethodSelection.kt b/usvm-ts/src/main/kotlin/org/usvm/census/CensusMethodSelection.kt new file mode 100644 index 0000000000..2e0b22322b --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/census/CensusMethodSelection.kt @@ -0,0 +1,98 @@ +package org.usvm.census + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX +import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME +import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME +import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME +import java.nio.file.Path + +internal fun selectCensusMethods( + manifest: UnknownCallCensusManifest, + project: UnknownCallCensusProject, + projectRoot: Path, + loadedFiles: LoadedProjectFiles, +): CensusMethodSelection { + val candidateFiles = loadedFiles.files.asSequence() + .map { file -> file to requireNotNull(loadedFiles.pathsBySignature[file.signature]) } + .filter { (_, fileName) -> project.includeSuffixes.any(fileName::endsWith) } + .filterNot { (_, fileName) -> project.excludeSuffixes.any(fileName::endsWith) } + .distinctBy { (_, fileName) -> fileName } + .sortedBy { (_, fileName) -> fileName } + .map { (file, _) -> file } + .toList() + + val eligibleClasses = candidateFiles + .flatMap { file -> file.allClasses } + .map { clazz -> + val classId = classId(project.id, projectRoot, clazz.signature, loadedFiles.pathsBySignature) + val methods = clazz.methods + .asSequence() + .filterNot { method -> method.cfg.stmts.isEmpty() } + .filterNot { method -> method.name.startsWith(ANONYMOUS_METHOD_PREFIX) } + .filterNot { method -> method.name == DEFAULT_ARK_METHOD_NAME } + .filterNot { method -> method.name == INSTANCE_INIT_METHOD_NAME } + .filterNot { method -> method.name == STATIC_INIT_METHOD_NAME } + .sortedWith( + compareBy( + { method -> + stableSelectionRank( + seed = manifest.randomSeed, + identity = functionId( + project.id, + projectRoot, + method.signature, + loadedFiles.pathsBySignature, + ), + ) + }, + { method -> + functionId( + project.id, + projectRoot, + method.signature, + loadedFiles.pathsBySignature, + ) + }, + ) + ) + .toList() + + SelectedClass(classId = classId, methods = methods) + } + .filter { selectedClass -> + selectedClass.methods.count { method -> + method.cfg.stmts.size >= manifest.limits.minStatementsPerMethod + } >= manifest.limits.minMethodsPerClass + } + + val selectedClasses = eligibleClasses + .sortedWith( + compareBy( + { selectedClass -> stableSelectionRank(manifest.randomSeed, selectedClass.classId) }, + SelectedClass::classId, + ) + ) + .take(manifest.limits.maxClasses) + val selectedMethods = roundRobin(selectedClasses.map(SelectedClass::methods)) + .take(manifest.limits.maxMethods) + + return CensusMethodSelection( + candidateFiles = candidateFiles.size, + eligibleClasses = eligibleClasses.size, + selectedClasses = selectedClasses.size, + methods = selectedMethods, + ) +} + +private data class SelectedClass( + val classId: String, + val methods: List, +) + +internal data class CensusMethodSelection( + val candidateFiles: Int, + val eligibleClasses: Int, + val selectedClasses: Int, + val methods: List, +) diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusProcess.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusProcess.kt new file mode 100644 index 0000000000..fe870c3174 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusProcess.kt @@ -0,0 +1,237 @@ +package org.usvm.census + +import java.io.IOException +import java.io.InputStream +import java.nio.charset.StandardCharsets +import java.nio.file.Path +import java.util.concurrent.CompletableFuture +import java.util.concurrent.ExecutionException +import java.util.concurrent.TimeUnit +import java.util.concurrent.TimeoutException +import kotlin.io.path.exists +import kotlin.io.path.isDirectory +import kotlin.time.Duration +import kotlin.time.Duration.Companion.milliseconds +import kotlin.time.TimeSource + +internal fun canonicalProjectCheckout(checkoutRoot: Path, relativePath: String): Path { + val canonicalCheckoutRoot = checkoutRoot.toRealPath() + val configuredProjectRoot = canonicalCheckoutRoot.resolve(relativePath).normalize() + require(configuredProjectRoot.startsWith(canonicalCheckoutRoot)) { + "Project checkout escapes the configured checkout root: $configuredProjectRoot" + } + require(configuredProjectRoot.isDirectory()) { + "Project checkout does not exist: $configuredProjectRoot" + } + + return configuredProjectRoot.toRealPath() +} + +internal fun canonicalExistingProjectPath( + projectRoot: Path, + relativePath: String, + kind: String, + requireDirectory: Boolean, +): Path { + val canonicalProjectRoot = projectRoot.toRealPath() + val configuredPath = canonicalProjectRoot.resolve(relativePath).normalize() + require(configuredPath.startsWith(canonicalProjectRoot)) { + "$kind escapes project checkout: $configuredPath" + } + require(configuredPath.exists()) { "$kind does not exist: $relativePath" } + if (requireDirectory) { + require(configuredPath.isDirectory()) { "$kind is not a directory: $configuredPath" } + } + + val canonicalPath = configuredPath.toRealPath() + require(canonicalPath.startsWith(canonicalProjectRoot)) { + "$kind escapes project checkout through a symbolic link: $configuredPath" + } + + return canonicalPath +} + +internal sealed interface BoundedProcessOutput { + data class Completed( + val exitCode: Int, + val output: String, + val truncated: Boolean, + ) : BoundedProcessOutput + + data object TimedOut : BoundedProcessOutput +} + +internal fun boundedProcessOutput( + command: List, + timeout: Duration, + maxOutputBytes: Int, +): BoundedProcessOutput { + require(timeout > Duration.ZERO) { "Process timeout must be positive" } + require(maxOutputBytes > 0) { "Process output limit must be positive" } + + var process: Process? = null + var outputReader: Thread? = null + try { + val processStart = TimeSource.Monotonic.markNow() + val startedProcess = ProcessBuilder(command) + .redirectErrorStream(true) + .start() + process = startedProcess + startedProcess.outputStream.close() + + val outputCollector = BoundedOutputCollector(maxOutputBytes) + val startedOutputReader = Thread( + { outputCollector.drain(startedProcess.inputStream) }, + "unknown-call-census-output-reader", + ).apply { + isDaemon = true + start() + } + outputReader = startedOutputReader + + val remaining = timeout - processStart.elapsedNow() + val completed = remaining > Duration.ZERO && startedProcess.waitFor( + remaining.inWholeMilliseconds.coerceAtLeast(minimumValue = 1), + TimeUnit.MILLISECONDS, + ) + if (!completed) { + terminateProcessTreeBestEffort(startedProcess) + closeProcessOutputBestEffort(startedProcess) + joinBestEffort(startedOutputReader, PROCESS_TERMINATION_GRACE) + return BoundedProcessOutput.TimedOut + } + + val outputRead = joinWithinTimeout( + thread = startedOutputReader, + timeout = timeout - processStart.elapsedNow(), + ) + if (!outputRead) { + closeProcessOutputBestEffort(startedProcess) + joinBestEffort(startedOutputReader, PROCESS_TERMINATION_GRACE) + return BoundedProcessOutput.TimedOut + } + + outputCollector.failure?.let { throw it } + return BoundedProcessOutput.Completed( + exitCode = startedProcess.exitValue(), + output = outputCollector.output(), + truncated = outputCollector.truncated, + ) + } finally { + process?.takeIf(Process::isAlive)?.let(::terminateProcessTreeBestEffort) + process?.let(::closeProcessOutputBestEffort) + outputReader?.takeIf(Thread::isAlive)?.let { reader -> + joinBestEffort(reader, PROCESS_TERMINATION_GRACE) + } + } +} + +private class BoundedOutputCollector(private val maxOutputBytes: Int) { + private val retainedOutput = ByteArray(maxOutputBytes) + private var retainedBytes = 0 + + var truncated: Boolean = false + private set + + var failure: Exception? = null + private set + + fun drain(input: InputStream) { + val buffer = ByteArray(PROCESS_OUTPUT_BUFFER_BYTES) + try { + input.use { + var readBytes = it.read(buffer) + while (readBytes >= 0) { + retain(buffer, readBytes) + readBytes = it.read(buffer) + } + } + } catch (error: IOException) { + failure = error + } + } + + private fun retain(buffer: ByteArray, readBytes: Int) { + val retainedFromChunk = minOf(readBytes, maxOutputBytes - retainedBytes) + if (retainedFromChunk > 0) { + buffer.copyInto( + destination = retainedOutput, + destinationOffset = retainedBytes, + endIndex = retainedFromChunk, + ) + retainedBytes += retainedFromChunk + } + if (retainedFromChunk < readBytes) { + truncated = true + } + } + + fun output(): String = retainedOutput.copyOf(retainedBytes).toString(StandardCharsets.UTF_8) +} + +private fun joinWithinTimeout(thread: Thread, timeout: Duration): Boolean { + if (timeout <= Duration.ZERO) { + return !thread.isAlive + } + + thread.join(timeout.inWholeMilliseconds.coerceAtLeast(minimumValue = 1)) + return !thread.isAlive +} + +private fun joinBestEffort(thread: Thread, timeout: Duration) { + try { + joinWithinTimeout(thread, timeout) + } catch (_: InterruptedException) { + Thread.currentThread().interrupt() + } +} + +private fun closeProcessOutputBestEffort(process: Process) { + runCatching { process.inputStream.close() } +} + +private fun terminateProcessTree(process: Process) { + val descendants = process.toHandle().descendants().use { handles -> + handles.iterator().asSequence().toList() + } + val processTree = listOf(process.toHandle()) + descendants + processTree.asReversed().forEach(ProcessHandle::destroy) + + if (!awaitTermination(processTree, PROCESS_TERMINATION_GRACE)) { + processTree.asReversed() + .filter(ProcessHandle::isAlive) + .forEach(ProcessHandle::destroyForcibly) + awaitTermination(processTree, PROCESS_TERMINATION_GRACE) + } + + process.waitFor(PROCESS_TERMINATION_GRACE.inWholeMilliseconds, TimeUnit.MILLISECONDS) +} + +private fun terminateProcessTreeBestEffort(process: Process) { + try { + terminateProcessTree(process) + } catch (_: InterruptedException) { + Thread.currentThread().interrupt() + process.destroyForcibly() + } catch (_: Exception) { + process.destroyForcibly() + } +} + +private fun awaitTermination(processes: List, timeout: Duration): Boolean { + val exits = processes.map(ProcessHandle::onExit).toTypedArray() + return try { + CompletableFuture.allOf(*exits).get(timeout.inWholeMilliseconds, TimeUnit.MILLISECONDS) + true + } catch (_: TimeoutException) { + false + } catch (_: ExecutionException) { + false + } catch (_: InterruptedException) { + Thread.currentThread().interrupt() + false + } +} + +private val PROCESS_TERMINATION_GRACE = 500.milliseconds +private const val PROCESS_OUTPUT_BUFFER_BYTES = 8 * 1024 diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRecording.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRecording.kt new file mode 100644 index 0000000000..b9f1044ee0 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRecording.kt @@ -0,0 +1,280 @@ +package org.usvm.census + +import kotlinx.serialization.json.JsonObject +import kotlinx.serialization.json.buildJsonObject +import kotlinx.serialization.json.put +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsMethodSignature +import org.jacodb.ets.model.EtsNamespaceSignature +import org.jacodb.ets.model.EtsSourceSpan +import org.usvm.PathSelectionStrategy +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.call.TsUnknownCallDecision +import org.usvm.machine.call.TsUnknownCallEvent +import java.io.BufferedWriter +import java.nio.charset.StandardCharsets +import java.nio.file.Files +import java.nio.file.Path +import java.nio.file.StandardOpenOption +import java.security.MessageDigest +import kotlin.io.path.absolute +import kotlin.io.path.name +import kotlin.io.path.pathString +import kotlin.time.Duration + +internal class RecordingCensusObserver( + private val project: UnknownCallCensusProject, + private val projectRoot: Path, + private val profile: UnknownCallCensusProfile, + private val entryFunctionId: String, + private val pathsBySignature: Map, + private val writer: CensusRecordWriter, +) : TsInterpreterObserver { + var eventCount: Int = 0 + private set + var recordingFailureCount: Int = 0 + private set + var recordingFailureMessage: String? = null + private set + + @Suppress("TooGenericExceptionCaught") + override fun onUnknownCall(event: TsUnknownCallEvent) { + try { + val containingSignature = event.callSite.location.method.signature + val functionId = functionId(project.id, projectRoot, containingSignature, pathsBySignature) + val sourceSpan = event.callSite.location.origin + val sourceFile = sourcePath(containingSignature, projectRoot, pathsBySignature) + val siteId = siteId(functionId, sourceSpan, event.callSite.location.index) + val decision = event.decision.serializedName + val eventIndex = eventCount + 1 + + writer.write( + buildJsonObject { + putCommonProjectFields(project, profile) + put("kind", "unknown_call") + put("entryFunctionId", entryFunctionId) + put("functionId", functionId) + put("siteId", siteId) + put("sourceFile", sourceFile) + sourceSpan?.let { span -> + put("startLine", span.startLine) + put("startColumn", span.startColumn) + put("endLine", span.endLine) + put("endColumn", span.endColumn) + } + put("statementIndex", event.callSite.location.index) + put("calleeId", calleeId(projectRoot, event.callee, pathsBySignature)) + put("calleeName", event.callee.name) + put("failureReason", event.failureReason.name) + put("decision", decision) + put("outcome", event.outcome.name) + put("eventIndex", eventIndex) + } + ) + eventCount = eventIndex + } catch (error: Exception) { + recordingFailureCount++ + if (recordingFailureMessage == null) { + recordingFailureMessage = "Unknown-call event recording failed: ${boundedError(error)}" + } + } + } +} + +internal class CensusRecordWriter(output: Path) : AutoCloseable { + private val writer: BufferedWriter = Files.newBufferedWriter( + output, + StandardCharsets.UTF_8, + StandardOpenOption.CREATE_NEW, + StandardOpenOption.WRITE, + ) + + fun write(record: JsonObject) { + writer.appendLine(record.toString()) + writer.flush() + } + + override fun close() { + writer.close() + } +} + +internal enum class MethodStatus(val serializedName: String) { + COMPLETED("completed"), + PARTIAL("partial"), + TIMEOUT("timeout"), + TOOL_ERROR("tool_error"), +} + +internal data class MethodOutcome( + val status: MethodStatus, + val error: String?, +) + +internal fun methodOutcomeAfterTimeoutCheck( + status: MethodStatus, + error: String?, + elapsed: Duration, + timeout: Duration, +): MethodOutcome = if (status == MethodStatus.COMPLETED && elapsed >= timeout) { + MethodOutcome( + status = MethodStatus.TIMEOUT, + error = "Machine timeout reached", + ) +} else { + MethodOutcome(status = status, error = error) +} + +private val TsUnknownCallDecision.serializedName: String + get() = when (this) { + is TsUnknownCallDecision.ModelApplied -> "MODEL_APPLIED:$modelId" + is TsUnknownCallDecision.ResidualFallback -> "RESIDUAL_FALLBACK:${policy.name}" + } + +internal fun JsonObjectBuilderScope.putCommonProjectFields( + project: UnknownCallCensusProject, + profile: UnknownCallCensusProfile, +) { + put("schemaVersion", CENSUS_SCHEMA_VERSION) + put("projectId", project.id) + put("projectRevision", project.revision) + put("profile", profile.name) +} + +internal typealias JsonObjectBuilderScope = kotlinx.serialization.json.JsonObjectBuilder + +internal fun functionId( + projectId: String, + projectRoot: Path, + signature: EtsMethodSignature, + pathsBySignature: Map, +): String { + val sourceFile = sourcePath(signature, projectRoot, pathsBySignature) + return "$projectId:$sourceFile:${signatureKey(signature)}" +} + +internal fun classId( + projectId: String, + projectRoot: Path, + signature: EtsClassSignature, + pathsBySignature: Map, +): String { + val sourceFile = sourcePath(signature.file, projectRoot, pathsBySignature) + val namespace = signature.namespace?.qualifiedName() + val className = listOfNotNull(namespace, signature.name).joinToString(separator = "::") + return "$projectId:$sourceFile:$className" +} + +private fun calleeId( + projectRoot: Path, + signature: EtsMethodSignature, + pathsBySignature: Map, +): String { + val sourceFile = sourcePath(signature, projectRoot, pathsBySignature) + return "$sourceFile:${signatureKey(signature)}" +} + +private fun sourcePath( + signature: EtsMethodSignature, + projectRoot: Path, + pathsBySignature: Map, +): String = sourcePath(signature.enclosingClass.file, projectRoot, pathsBySignature) + +private fun sourcePath( + signature: EtsFileSignature, + projectRoot: Path, + pathsBySignature: Map, +): String = pathsBySignature[signature] + ?: normalizedSourcePath(signature.fileName, projectRoot) + +private fun signatureKey(signature: EtsMethodSignature): String { + val parameters = signature.parameters.joinToString(separator = ",") { parameter -> parameter.type.toString() } + val namespace = signature.enclosingClass.namespace?.qualifiedName() + val className = listOfNotNull(namespace, signature.enclosingClass.name).joinToString(separator = "::") + return "$className:${signature.name}($parameters)->${signature.returnType}" +} + +private fun EtsNamespaceSignature.qualifiedName(): String = + listOfNotNull(namespace?.qualifiedName(), name).joinToString(separator = "::") + +private fun siteId(functionId: String, sourceSpan: EtsSourceSpan?, statementIndex: Int): String = + if (sourceSpan == null) { + "$functionId:ir-index:$statementIndex" + } else { + "$functionId:${sourceSpan.startLine}:${sourceSpan.startColumn}:${sourceSpan.endLine}:${sourceSpan.endColumn}" + } + +private fun normalizedSourcePath(rawPath: String, projectRoot: Path): String { + val normalizedRawPath = rawPath.normalizedSeparators().removePrefix("@") + val sourcePath = runCatching { Path.of(rawPath).normalize().absolute() }.getOrNull() + val normalizedRoot = projectRoot.normalize().absolute() + + return when { + sourcePath != null && sourcePath.startsWith(normalizedRoot) -> { + normalizedRoot.relativize(sourcePath).pathString.normalizedSeparators() + } + + Path.of(rawPath).isAbsolute -> "external/${Path.of(rawPath).name}" + else -> normalizedRawPath.removePrefix("./") + } +} + +internal fun repositoryRelativeSourcePath( + rawPath: String, + sourceRoot: Path, + sourceRootRelativePath: String, + projectRoot: Path, +): String { + val raw = Path.of(rawPath) + if (raw.isAbsolute) { + return normalizedSourcePath(rawPath, projectRoot) + } + + val sourceRelativePath = normalizedSourcePath(rawPath, sourceRoot) + val normalizedSourceRoot = sourceRootRelativePath.normalizedSeparators().trim('/') + return listOf(normalizedSourceRoot, sourceRelativePath) + .filter(String::isNotEmpty) + .joinToString(separator = "/") +} + +private fun String.normalizedSeparators(): String = replace('\\', '/') + +internal fun stableSelectionRank(seed: Long, identity: String): String = sha256( + "$seed\u0000$identity".toByteArray(StandardCharsets.UTF_8) +) + +internal fun roundRobin(groups: List>): List { + val maxGroupSize = groups.maxOfOrNull(List::size) ?: return emptyList() + return buildList { + repeat(maxGroupSize) { index -> + groups.forEach { group -> group.getOrNull(index)?.let(::add) } + } + } +} + +internal fun sha256(bytes: ByteArray): String = MessageDigest.getInstance("SHA-256") + .digest(bytes) + .joinToString(separator = "") { byte -> "%02x".format(byte) } + +internal fun boundedError(error: Throwable): String { + val type = error::class.qualifiedName ?: error::class.simpleName ?: "Throwable" + val message = error.message + ?.replace('\n', ' ') + ?.replace(JVM_IDENTITY_SUFFIX, "@") + ?.take(MAX_ERROR_LENGTH) + return if (message.isNullOrBlank()) type else "$type: $message" +} + +internal fun combineErrors(primary: String?, additional: String?): String? = when { + primary == null -> additional + additional == null -> primary + else -> "$primary; $additional".take(MAX_ERROR_LENGTH) +} + +internal class ProjectTimeoutException(message: String, cause: Throwable? = null) : RuntimeException(message, cause) + +private const val MAX_ERROR_LENGTH = 1_000 +internal const val CENSUS_STOP_ON_COVERAGE = 0 +internal val CENSUS_PATH_SELECTION_STRATEGY = PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM +private val JVM_IDENTITY_SUFFIX = Regex("@[0-9a-fA-F]{6,16}") diff --git a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt index 514eac2a61..4666162d04 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/census/UnknownCallCensusRunner.kt @@ -4,53 +4,29 @@ import kotlinx.serialization.encodeToString import kotlinx.serialization.json.JsonObject import kotlinx.serialization.json.buildJsonObject import kotlinx.serialization.json.put -import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsMethod -import org.jacodb.ets.model.EtsMethodSignature -import org.jacodb.ets.model.EtsNamespaceSignature import org.jacodb.ets.model.EtsScene -import org.jacodb.ets.model.EtsSourceSpan -import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX -import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.EtsIrGenerationException import org.jacodb.ets.utils.EtsIrProvider -import org.jacodb.ets.utils.INSTANCE_INIT_METHOD_NAME -import org.jacodb.ets.utils.STATIC_INIT_METHOD_NAME import org.jacodb.ets.utils.generateEtsIR import org.jacodb.ets.utils.loadEtsProjectFromIR -import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.UMachineOptions -import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.call.TsResidualCallPolicy -import org.usvm.machine.call.TsUnknownCallDecision -import org.usvm.machine.call.TsUnknownCallEvent import org.usvm.machine.call.TsUnknownCallModelSelection -import java.io.BufferedWriter -import java.io.IOException -import java.io.InputStream import java.nio.charset.StandardCharsets import java.nio.file.Files import java.nio.file.Path -import java.nio.file.StandardOpenOption -import java.security.MessageDigest import java.time.Instant -import java.util.concurrent.CompletableFuture -import java.util.concurrent.ExecutionException -import java.util.concurrent.TimeUnit -import java.util.concurrent.TimeoutException -import kotlin.io.path.absolute import kotlin.io.path.createDirectories import kotlin.io.path.exists -import kotlin.io.path.isDirectory import kotlin.io.path.name import kotlin.io.path.pathString import kotlin.time.Duration -import kotlin.time.Duration.Companion.milliseconds import kotlin.time.Duration.Companion.seconds import kotlin.time.TimeSource @@ -133,7 +109,12 @@ internal class UnknownCallCensusRunner( ) val loadedFiles = loadProjectFiles(project, projectRoot, projectStart, projectTimeout) - val selection = selectMethods(project, projectRoot, loadedFiles) + val selection = selectCensusMethods( + manifest = manifest, + project = project, + projectRoot = projectRoot, + loadedFiles = loadedFiles, + ) val sceneFiles = loadedFiles.files .distinctBy { file -> requireNotNull(loadedFiles.pathsBySignature[file.signature]) } .sortedBy { file -> requireNotNull(loadedFiles.pathsBySignature[file.signature]) } @@ -322,83 +303,6 @@ internal class UnknownCallCensusRunner( return MethodRunResult(status = status, events = observer.eventCount) } - private fun selectMethods( - project: UnknownCallCensusProject, - projectRoot: Path, - loadedFiles: LoadedProjectFiles, - ): SelectedMethods { - val candidateFiles = loadedFiles.files.asSequence() - .map { file -> file to requireNotNull(loadedFiles.pathsBySignature[file.signature]) } - .filter { (_, fileName) -> project.includeSuffixes.any(fileName::endsWith) } - .filterNot { (_, fileName) -> project.excludeSuffixes.any(fileName::endsWith) } - .distinctBy { (_, fileName) -> fileName } - .sortedBy { (_, fileName) -> fileName } - .map { (file, _) -> file } - .toList() - - val eligibleClasses = candidateFiles - .flatMap { file -> file.allClasses } - .map { clazz -> - val classId = classId(project.id, projectRoot, clazz.signature, loadedFiles.pathsBySignature) - val methods = clazz.methods - .asSequence() - .filterNot { method -> method.cfg.stmts.isEmpty() } - .filterNot { method -> method.name.startsWith(ANONYMOUS_METHOD_PREFIX) } - .filterNot { method -> method.name == DEFAULT_ARK_METHOD_NAME } - .filterNot { method -> method.name == INSTANCE_INIT_METHOD_NAME } - .filterNot { method -> method.name == STATIC_INIT_METHOD_NAME } - .sortedWith( - compareBy( - { method -> - stableSelectionRank( - seed = manifest.randomSeed, - identity = functionId( - project.id, - projectRoot, - method.signature, - loadedFiles.pathsBySignature, - ), - ) - }, - { method -> - functionId( - project.id, - projectRoot, - method.signature, - loadedFiles.pathsBySignature, - ) - }, - ) - ) - .toList() - - SelectedClass(classId = classId, methods = methods) - } - .filter { selectedClass -> - selectedClass.methods.count { method -> - method.cfg.stmts.size >= manifest.limits.minStatementsPerMethod - } >= manifest.limits.minMethodsPerClass - } - - val selectedClasses = eligibleClasses - .sortedWith( - compareBy( - { selectedClass -> stableSelectionRank(manifest.randomSeed, selectedClass.classId) }, - SelectedClass::classId, - ) - ) - .take(manifest.limits.maxClasses) - val selectedMethods = roundRobin(selectedClasses.map(SelectedClass::methods)) - .take(manifest.limits.maxMethods) - - return SelectedMethods( - candidateFiles = candidateFiles.size, - eligibleClasses = eligibleClasses.size, - selectedClasses = selectedClasses.size, - methods = selectedMethods, - ) - } - private fun loadProjectFiles( project: UnknownCallCensusProject, projectRoot: Path, @@ -625,512 +529,22 @@ internal class UnknownCallCensusRunner( } } -internal fun canonicalProjectCheckout(checkoutRoot: Path, relativePath: String): Path { - val canonicalCheckoutRoot = checkoutRoot.toRealPath() - val configuredProjectRoot = canonicalCheckoutRoot.resolve(relativePath).normalize() - require(configuredProjectRoot.startsWith(canonicalCheckoutRoot)) { - "Project checkout escapes the configured checkout root: $configuredProjectRoot" - } - require(configuredProjectRoot.isDirectory()) { - "Project checkout does not exist: $configuredProjectRoot" - } - - return configuredProjectRoot.toRealPath() -} - -internal fun canonicalExistingProjectPath( - projectRoot: Path, - relativePath: String, - kind: String, - requireDirectory: Boolean, -): Path { - val canonicalProjectRoot = projectRoot.toRealPath() - val configuredPath = canonicalProjectRoot.resolve(relativePath).normalize() - require(configuredPath.startsWith(canonicalProjectRoot)) { - "$kind escapes project checkout: $configuredPath" - } - require(configuredPath.exists()) { "$kind does not exist: $relativePath" } - if (requireDirectory) { - require(configuredPath.isDirectory()) { "$kind is not a directory: $configuredPath" } - } - - val canonicalPath = configuredPath.toRealPath() - require(canonicalPath.startsWith(canonicalProjectRoot)) { - "$kind escapes project checkout through a symbolic link: $configuredPath" - } - - return canonicalPath -} - -internal sealed interface BoundedProcessOutput { - data class Completed( - val exitCode: Int, - val output: String, - val truncated: Boolean, - ) : BoundedProcessOutput - - data object TimedOut : BoundedProcessOutput -} - -internal fun boundedProcessOutput( - command: List, - timeout: Duration, - maxOutputBytes: Int, -): BoundedProcessOutput { - require(timeout > Duration.ZERO) { "Process timeout must be positive" } - require(maxOutputBytes > 0) { "Process output limit must be positive" } - - var process: Process? = null - var outputReader: Thread? = null - try { - val processStart = TimeSource.Monotonic.markNow() - val startedProcess = ProcessBuilder(command) - .redirectErrorStream(true) - .start() - process = startedProcess - startedProcess.outputStream.close() - - val outputCollector = BoundedOutputCollector(maxOutputBytes) - val startedOutputReader = Thread( - { outputCollector.drain(startedProcess.inputStream) }, - "unknown-call-census-output-reader", - ).apply { - isDaemon = true - start() - } - outputReader = startedOutputReader - - val remaining = timeout - processStart.elapsedNow() - val completed = remaining > Duration.ZERO && startedProcess.waitFor( - remaining.inWholeMilliseconds.coerceAtLeast(minimumValue = 1), - TimeUnit.MILLISECONDS, - ) - if (!completed) { - terminateProcessTreeBestEffort(startedProcess) - closeProcessOutputBestEffort(startedProcess) - joinBestEffort(startedOutputReader, PROCESS_TERMINATION_GRACE) - return BoundedProcessOutput.TimedOut - } - - val outputRead = joinWithinTimeout( - thread = startedOutputReader, - timeout = timeout - processStart.elapsedNow(), - ) - if (!outputRead) { - closeProcessOutputBestEffort(startedProcess) - joinBestEffort(startedOutputReader, PROCESS_TERMINATION_GRACE) - return BoundedProcessOutput.TimedOut - } - - outputCollector.failure?.let { throw it } - return BoundedProcessOutput.Completed( - exitCode = startedProcess.exitValue(), - output = outputCollector.output(), - truncated = outputCollector.truncated, - ) - } finally { - process?.takeIf(Process::isAlive)?.let(::terminateProcessTreeBestEffort) - process?.let(::closeProcessOutputBestEffort) - outputReader?.takeIf(Thread::isAlive)?.let { reader -> - joinBestEffort(reader, PROCESS_TERMINATION_GRACE) - } - } -} - -private class BoundedOutputCollector(private val maxOutputBytes: Int) { - private val retainedOutput = ByteArray(maxOutputBytes) - private var retainedBytes = 0 - - var truncated: Boolean = false - private set - - var failure: Exception? = null - private set - - fun drain(input: InputStream) { - val buffer = ByteArray(PROCESS_OUTPUT_BUFFER_BYTES) - try { - input.use { - var readBytes = it.read(buffer) - while (readBytes >= 0) { - retain(buffer, readBytes) - readBytes = it.read(buffer) - } - } - } catch (error: IOException) { - failure = error - } - } - - private fun retain(buffer: ByteArray, readBytes: Int) { - val retainedFromChunk = minOf(readBytes, maxOutputBytes - retainedBytes) - if (retainedFromChunk > 0) { - buffer.copyInto( - destination = retainedOutput, - destinationOffset = retainedBytes, - endIndex = retainedFromChunk, - ) - retainedBytes += retainedFromChunk - } - if (retainedFromChunk < readBytes) { - truncated = true - } - } - - fun output(): String = retainedOutput.copyOf(retainedBytes).toString(StandardCharsets.UTF_8) -} - -private fun joinWithinTimeout(thread: Thread, timeout: Duration): Boolean { - if (timeout <= Duration.ZERO) { - return !thread.isAlive - } - - thread.join(timeout.inWholeMilliseconds.coerceAtLeast(minimumValue = 1)) - return !thread.isAlive -} - -private fun joinBestEffort(thread: Thread, timeout: Duration) { - try { - joinWithinTimeout(thread, timeout) - } catch (_: InterruptedException) { - Thread.currentThread().interrupt() - } -} - -private fun closeProcessOutputBestEffort(process: Process) { - runCatching { process.inputStream.close() } -} - -private fun terminateProcessTree(process: Process) { - val descendants = process.toHandle().descendants().use { handles -> - handles.iterator().asSequence().toList() - } - val processTree = listOf(process.toHandle()) + descendants - processTree.asReversed().forEach(ProcessHandle::destroy) - - if (!awaitTermination(processTree, PROCESS_TERMINATION_GRACE)) { - processTree.asReversed() - .filter(ProcessHandle::isAlive) - .forEach(ProcessHandle::destroyForcibly) - awaitTermination(processTree, PROCESS_TERMINATION_GRACE) - } - - process.waitFor(PROCESS_TERMINATION_GRACE.inWholeMilliseconds, TimeUnit.MILLISECONDS) -} - -private fun terminateProcessTreeBestEffort(process: Process) { - try { - terminateProcessTree(process) - } catch (_: InterruptedException) { - Thread.currentThread().interrupt() - process.destroyForcibly() - } catch (_: Exception) { - process.destroyForcibly() - } -} - -private fun awaitTermination(processes: List, timeout: Duration): Boolean { - val exits = processes.map(ProcessHandle::onExit).toTypedArray() - return try { - CompletableFuture.allOf(*exits).get(timeout.inWholeMilliseconds, TimeUnit.MILLISECONDS) - true - } catch (_: TimeoutException) { - false - } catch (_: ExecutionException) { - false - } catch (_: InterruptedException) { - Thread.currentThread().interrupt() - false - } -} - -private val PROCESS_TERMINATION_GRACE = 500.milliseconds -private const val PROCESS_OUTPUT_BUFFER_BYTES = 8 * 1024 - private fun runtimeArtifactName(type: Class<*>): String = runCatching { Path.of(type.protectionDomain.codeSource.location.toURI()).name }.getOrDefault("unknown") -private class RecordingCensusObserver( - private val project: UnknownCallCensusProject, - private val projectRoot: Path, - private val profile: UnknownCallCensusProfile, - private val entryFunctionId: String, - private val pathsBySignature: Map, - private val writer: CensusRecordWriter, -) : TsInterpreterObserver { - var eventCount: Int = 0 - private set - var recordingFailureCount: Int = 0 - private set - var recordingFailureMessage: String? = null - private set - - @Suppress("TooGenericExceptionCaught") - override fun onUnknownCall(event: TsUnknownCallEvent) { - try { - val containingSignature = event.callSite.location.method.signature - val functionId = functionId(project.id, projectRoot, containingSignature, pathsBySignature) - val sourceSpan = event.callSite.location.origin - val sourceFile = sourcePath(containingSignature, projectRoot, pathsBySignature) - val siteId = siteId(functionId, sourceSpan, event.callSite.location.index) - val decision = event.decision.serializedName - val eventIndex = eventCount + 1 - - writer.write( - buildJsonObject { - putCommonProjectFields(project, profile) - put("kind", "unknown_call") - put("entryFunctionId", entryFunctionId) - put("functionId", functionId) - put("siteId", siteId) - put("sourceFile", sourceFile) - sourceSpan?.let { span -> - put("startLine", span.startLine) - put("startColumn", span.startColumn) - put("endLine", span.endLine) - put("endColumn", span.endColumn) - } - put("statementIndex", event.callSite.location.index) - put("calleeId", calleeId(projectRoot, event.callee, pathsBySignature)) - put("calleeName", event.callee.name) - put("failureReason", event.failureReason.name) - put("decision", decision) - put("outcome", event.outcome.name) - put("eventIndex", eventIndex) - } - ) - eventCount = eventIndex - } catch (error: Exception) { - recordingFailureCount++ - if (recordingFailureMessage == null) { - recordingFailureMessage = "Unknown-call event recording failed: ${boundedError(error)}" - } - } - } -} - -internal class CensusRecordWriter(output: Path) : AutoCloseable { - private val writer: BufferedWriter = Files.newBufferedWriter( - output, - StandardCharsets.UTF_8, - StandardOpenOption.CREATE_NEW, - StandardOpenOption.WRITE, - ) - - fun write(record: JsonObject) { - writer.appendLine(record.toString()) - writer.flush() - } - - override fun close() { - writer.close() - } -} - -internal enum class MethodStatus(val serializedName: String) { - COMPLETED("completed"), - PARTIAL("partial"), - TIMEOUT("timeout"), - TOOL_ERROR("tool_error"), -} - -internal data class MethodOutcome( - val status: MethodStatus, - val error: String?, -) - -internal fun methodOutcomeAfterTimeoutCheck( - status: MethodStatus, - error: String?, - elapsed: Duration, - timeout: Duration, -): MethodOutcome = if (status == MethodStatus.COMPLETED && elapsed >= timeout) { - MethodOutcome( - status = MethodStatus.TIMEOUT, - error = "Machine timeout reached", - ) -} else { - MethodOutcome(status = status, error = error) -} - private data class MethodRunResult( val status: MethodStatus, val events: Int, ) -private data class LoadedProjectFiles( +internal data class LoadedProjectFiles( val files: List, val pathsBySignature: Map, ) -private data class SelectedClass( - val classId: String, - val methods: List, -) - -private data class SelectedMethods( - val candidateFiles: Int, - val eligibleClasses: Int, - val selectedClasses: Int, - val methods: List, -) - private val UnknownCallCensusProfile.fallback: TsResidualCallPolicy get() = when (this) { UnknownCallCensusProfile.EMPTY_FRESH -> TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN UnknownCallCensusProfile.EMPTY_STOP -> TsResidualCallPolicy.STOP_PATH } - -private val TsUnknownCallDecision.serializedName: String - get() = when (this) { - is TsUnknownCallDecision.ModelApplied -> "MODEL_APPLIED:$modelId" - is TsUnknownCallDecision.ResidualFallback -> "RESIDUAL_FALLBACK:${policy.name}" - } - -private fun JsonObjectBuilderScope.putCommonProjectFields( - project: UnknownCallCensusProject, - profile: UnknownCallCensusProfile, -) { - put("schemaVersion", CENSUS_SCHEMA_VERSION) - put("projectId", project.id) - put("projectRevision", project.revision) - put("profile", profile.name) -} - -private typealias JsonObjectBuilderScope = kotlinx.serialization.json.JsonObjectBuilder - -private fun functionId( - projectId: String, - projectRoot: Path, - signature: EtsMethodSignature, - pathsBySignature: Map, -): String { - val sourceFile = sourcePath(signature, projectRoot, pathsBySignature) - return "$projectId:$sourceFile:${signatureKey(signature)}" -} - -private fun classId( - projectId: String, - projectRoot: Path, - signature: EtsClassSignature, - pathsBySignature: Map, -): String { - val sourceFile = sourcePath(signature.file, projectRoot, pathsBySignature) - val namespace = signature.namespace?.qualifiedName() - val className = listOfNotNull(namespace, signature.name).joinToString(separator = "::") - return "$projectId:$sourceFile:$className" -} - -private fun calleeId( - projectRoot: Path, - signature: EtsMethodSignature, - pathsBySignature: Map, -): String { - val sourceFile = sourcePath(signature, projectRoot, pathsBySignature) - return "$sourceFile:${signatureKey(signature)}" -} - -private fun sourcePath( - signature: EtsMethodSignature, - projectRoot: Path, - pathsBySignature: Map, -): String = sourcePath(signature.enclosingClass.file, projectRoot, pathsBySignature) - -private fun sourcePath( - signature: EtsFileSignature, - projectRoot: Path, - pathsBySignature: Map, -): String = pathsBySignature[signature] - ?: normalizedSourcePath(signature.fileName, projectRoot) - -private fun signatureKey(signature: EtsMethodSignature): String { - val parameters = signature.parameters.joinToString(separator = ",") { parameter -> parameter.type.toString() } - val namespace = signature.enclosingClass.namespace?.qualifiedName() - val className = listOfNotNull(namespace, signature.enclosingClass.name).joinToString(separator = "::") - return "$className:${signature.name}($parameters)->${signature.returnType}" -} - -private fun EtsNamespaceSignature.qualifiedName(): String = - listOfNotNull(namespace?.qualifiedName(), name).joinToString(separator = "::") - -private fun siteId(functionId: String, sourceSpan: EtsSourceSpan?, statementIndex: Int): String = - if (sourceSpan == null) { - "$functionId:ir-index:$statementIndex" - } else { - "$functionId:${sourceSpan.startLine}:${sourceSpan.startColumn}:${sourceSpan.endLine}:${sourceSpan.endColumn}" - } - -private fun normalizedSourcePath(rawPath: String, projectRoot: Path): String { - val normalizedRawPath = rawPath.normalizedSeparators().removePrefix("@") - val sourcePath = runCatching { Path.of(rawPath).normalize().absolute() }.getOrNull() - val normalizedRoot = projectRoot.normalize().absolute() - - return when { - sourcePath != null && sourcePath.startsWith(normalizedRoot) -> { - normalizedRoot.relativize(sourcePath).pathString.normalizedSeparators() - } - - Path.of(rawPath).isAbsolute -> "external/${Path.of(rawPath).name}" - else -> normalizedRawPath.removePrefix("./") - } -} - -private fun repositoryRelativeSourcePath( - rawPath: String, - sourceRoot: Path, - sourceRootRelativePath: String, - projectRoot: Path, -): String { - val raw = Path.of(rawPath) - if (raw.isAbsolute) { - return normalizedSourcePath(rawPath, projectRoot) - } - - val sourceRelativePath = normalizedSourcePath(rawPath, sourceRoot) - val normalizedSourceRoot = sourceRootRelativePath.normalizedSeparators().trim('/') - return listOf(normalizedSourceRoot, sourceRelativePath) - .filter(String::isNotEmpty) - .joinToString(separator = "/") -} - -private fun String.normalizedSeparators(): String = replace('\\', '/') - -internal fun stableSelectionRank(seed: Long, identity: String): String = sha256( - "$seed\u0000$identity".toByteArray(StandardCharsets.UTF_8) -) - -internal fun roundRobin(groups: List>): List { - val maxGroupSize = groups.maxOfOrNull(List::size) ?: return emptyList() - return buildList { - repeat(maxGroupSize) { index -> - groups.forEach { group -> group.getOrNull(index)?.let(::add) } - } - } -} - -private fun sha256(bytes: ByteArray): String = MessageDigest.getInstance("SHA-256") - .digest(bytes) - .joinToString(separator = "") { byte -> "%02x".format(byte) } - -private fun boundedError(error: Throwable): String { - val type = error::class.qualifiedName ?: error::class.simpleName ?: "Throwable" - val message = error.message - ?.replace('\n', ' ') - ?.replace(JVM_IDENTITY_SUFFIX, "@") - ?.take(MAX_ERROR_LENGTH) - return if (message.isNullOrBlank()) type else "$type: $message" -} - -private fun combineErrors(primary: String?, additional: String?): String? = when { - primary == null -> additional - additional == null -> primary - else -> "$primary; $additional".take(MAX_ERROR_LENGTH) -} - -private class ProjectTimeoutException(message: String, cause: Throwable? = null) : RuntimeException(message, cause) - -private const val MAX_ERROR_LENGTH = 1_000 -private const val CENSUS_STOP_ON_COVERAGE = 0 -private val CENSUS_PATH_SELECTION_STRATEGY = PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM -private val JVM_IDENTITY_SUFFIX = Regex("@[0-9a-fA-F]{6,16}")