From c35a18967046b55a7a321c1009a70366d264df95 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 20 Oct 2026 12:24:03 +0300 Subject: [PATCH] Configure frozen class probe models budgets and search receipts --- .../org/usvm/ts/calls/CallsClassExperiment.kt | 2 +- .../usvm/ts/calls/CallsClassRawAnalysis.kt | 5 ++ .../org/usvm/ts/calls/CallsClassStartSmoke.kt | 16 +++-- .../usvm/ts/calls/CallsClassStartSmokeTest.kt | 72 ++++++++++++++++++- 4 files changed, 86 insertions(+), 9 deletions(-) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassExperiment.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassExperiment.kt index d907cc13c0..867bc26ec5 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassExperiment.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassExperiment.kt @@ -519,7 +519,7 @@ private const val LONG_CLASS_BUDGET_MILLIS = 120_000L private const val FIRST_CLASS_CHECKPOINT_MILLIS = 1_000L private const val SECOND_CLASS_CHECKPOINT_MILLIS = 5_000L private const val THIRD_CLASS_CHECKPOINT_MILLIS = 10_000L -private val CLASS_SEARCH_BUDGETS_MILLIS = listOf(SHORT_CLASS_BUDGET_MILLIS, LONG_CLASS_BUDGET_MILLIS) +internal val CLASS_SEARCH_BUDGETS_MILLIS = listOf(SHORT_CLASS_BUDGET_MILLIS, LONG_CLASS_BUDGET_MILLIS) private val CLASS_COVERAGE_CHECKPOINTS_MILLIS = listOf( FIRST_CLASS_CHECKPOINT_MILLIS, SECOND_CLASS_CHECKPOINT_MILLIS, diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt index e58b693eb1..7f31983563 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassRawAnalysis.kt @@ -3,6 +3,7 @@ package org.usvm.ts.calls import kotlinx.serialization.Serializable import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsStmt +import org.usvm.PathSelectionStrategy import org.usvm.UPathSelector import org.usvm.machine.TsEntryPointTimeQuantumEvent import org.usvm.machine.TsSolverQueryEvent @@ -70,6 +71,8 @@ internal data class CallsClassRawAnalysis( val journalFinalizeMillis: Long = 0, val timeQuantumMillis: Long, val collectedStatesLimit: Int? = null, + val solverLimitMillis: Long = 250, + val pathSelectionStrategy: PathSelectionStrategy = PathSelectionStrategy.BFS, val profile: CallsExperimentProfile, val seed: Long, val returnedStates: Long, @@ -370,6 +373,8 @@ internal class ClassRawAnalysisObserver( drainSnapshotElapsedNanos = drainSnapshotNanos, journalFinalizeMillis = journalFinalizeMillis, timeQuantumMillis = manifest.timeQuantumMillis, + solverLimitMillis = manifest.solverLimitMillis, + pathSelectionStrategy = manifest.pathSelectionStrategy, profile = manifest.profile, seed = manifest.seed, collectedStatesLimit = manifest.collectedStatesLimit, diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt index 101299f964..11e509dc90 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsClassStartSmoke.kt @@ -16,6 +16,7 @@ import org.jacodb.ets.model.EtsThrowStmt import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX import org.jacodb.ets.utils.loadEtsProjectFromIR import org.usvm.CoverageZone +import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.StateCollectionStrategy import org.usvm.UMachineOptions @@ -91,6 +92,7 @@ internal data class CallsClassStartManifest( val expectedClassCount: Int = 200, val budgetMillis: Long = 2_000, val solverLimitMillis: Long = 250, + val pathSelectionStrategy: PathSelectionStrategy = CALLS_PATH_SELECTION_STRATEGY, val collectedStatesLimit: Int? = 10, val forkLimit: ULong? = null, val timeQuantumMillis: Long = 25, @@ -98,6 +100,8 @@ internal data class CallsClassStartManifest( val profile: CallsExperimentProfile = CallsExperimentProfile.FROZEN_STOP, val classes: List, val retainRawStateDiagnostics: Boolean = false, + val frozenModelIds: Set? = null, + val maxInputCollectionSize: Int? = null, ) { init { require(schemaVersion == 1 && classes.size == expectedClassCount && expectedClassCount > 0) @@ -408,7 +412,9 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { val bytes = Files.readAllBytes(manifestPath) val manifest = CallsExperimentJson.json.decodeFromString(bytes.toString(Charsets.UTF_8)) if (exploratory) { - require(manifest.budgetMillis == EXPLORATORY_BUDGET_MILLIS && manifest.seed == EXPLORATORY_SEED) + require(manifest.budgetMillis in CLASS_SEARCH_BUDGETS_MILLIS) { + "Symbolic probes support exactly 30 and 120 second budgets" + } require(manifest.collectedStatesLimit == null) { "The exploratory probe has no terminal-state cap" } } require(manifest.toolRevision == CallsBuildIdentity.toolRevision) { "Smoke runtime revision changed" } @@ -578,7 +584,7 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { TsMachine( scene = scene, options = UMachineOptions( - pathSelectionStrategies = listOf(CALLS_PATH_SELECTION_STRATEGY), + pathSelectionStrategies = listOf(manifest.pathSelectionStrategy), stateCollectionStrategy = StateCollectionStrategy.ALL, randomSeed = manifest.seed, collectedStatesLimit = manifest.collectedStatesLimit, @@ -594,12 +600,14 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { ), tsOptions = TsOptions( unknownCallModelSelection = if (manifest.profile.usesFrozenModels) { - TsUnknownCallModelSelection.All + manifest.frozenModelIds?.let(TsUnknownCallModelSelection::Only) + ?: TsUnknownCallModelSelection.All } else { TsUnknownCallModelSelection.Only(emptySet()) }, unknownCallFallback = manifest.profile.fallback, eraseTypeAssertions = true, + maxInputCollectionSize = manifest.maxInputCollectionSize, classCoverageTargets = setOf(target.signature), ), machineObserver = machineObserver, @@ -696,5 +704,3 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { } private const val CLASS_START_ARGUMENT_COUNT = 3 -private const val EXPLORATORY_BUDGET_MILLIS = 30_000L -private const val EXPLORATORY_SEED = 17L diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt index 6001d019fd..65afbc132d 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassStartSmokeTest.kt @@ -10,6 +10,7 @@ import org.jacodb.ets.model.EtsSourceSpan import org.jacodb.ets.model.EtsStmtLocation import org.jacodb.ets.model.EtsUndefinedType import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy import org.usvm.ts.pbt.backend.PropertyRunConfiguration import org.usvm.ts.pbt.backend.PropertyRunStatus import org.usvm.ts.pbt.fastcheck.FastCheckBackend @@ -226,7 +227,10 @@ class CallsClassStartSmokeTest { numeric(value: T): number { return value > 0 ? 1 : 0; } logical(value: T): number { return value ? 1 : 0; } reference(value: T): number { return value.length; } - defaulted(value: T): boolean { return typeof value === 'number'; } + defaulted(value: T): boolean { + if (typeof value === 'number') return true; + return false; + } } """.trimIndent() @@ -245,7 +249,8 @@ class CallsClassStartSmokeTest { assertTrue(values("logical").all { it is JsConcreteValue.Boolean }) assertTrue(values("reference").all { it is JsConcreteValue.String }) val failures = Files.readAllLines(directory.resolve("output/input-extraction-failures.jsonl")) - assertTrue(values("defaulted").isNotEmpty()) + // Distinct return paths force both kinds; one unconstrained return permits an arbitrary solver witness. + assertTrue(values("defaulted").any { it is JsConcreteValue.Number }) assertTrue(values("defaulted").any { it !is JsConcreteValue.Number }) assertTrue(failures.isEmpty(), failures.toString()) } @@ -432,12 +437,68 @@ class CallsClassStartSmokeTest { assertTrue(raw.sourceEnteredStatementKinds.getOrDefault("EtsDefineDataPropertyStmt", 0) > 0, raw.toString()) } + @Test + fun `explicit frozen model IDs preserve an empty catalog`() { + val source = "export class Target { run(): number { const map = new Map(); return map.size; } }" + val result = runFixture(sourceText = source, frozenModelIds = emptySet(), exploratory = true) + + assertTrue(result.started, result.toString()) + assertTrue(result.unsupportedCall, result.toString()) + val calls = result.unknownCalls.filter { it.callee.enclosingClass == "Map" } + assertTrue(calls.isNotEmpty()) + assertTrue(calls.all { it.decision == CallsUnknownCallDecisionKind.RESIDUAL_FALLBACK }) + assertTrue(calls.all { it.outcome == "PATH_STOPPED" && it.modelId == null }) + } + + @Test + fun `symbolic probe accepts the long class budget and retains its identity`() { + val result = runFixture( + sourceText = "export class Target { read(value: number): number { return value > 0 ? 1 : -1; } }", + exploratory = true, + budgetMillis = 120_000, + solverLimitMillis = 1_000, + timeQuantumMillis = 250, + seed = 23, + pathSelectionStrategy = PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM, + ) + + val analysis = checkNotNull(result.rawAnalysis) + assertEquals(120_000L, analysis.budgetMillis) + assertEquals(1_000L, analysis.solverLimitMillis) + assertEquals(250L, analysis.timeQuantumMillis) + assertEquals(23L, analysis.seed) + assertEquals(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM, analysis.pathSelectionStrategy) + assertTrue(result.started, result.toString()) + assertTrue(analysis.sourceMappedIrEntered.isNotEmpty()) + assertFalse(analysis.rawStateDiagnosticsEnabled) + } + + @Test + fun `symbolic probe rejects budgets outside the declared class treatments`() { + val failure = assertFailsWith { + runFixture( + sourceText = "export class Target { read(): number { return 1; } }", + exploratory = true, + budgetMillis = 60_000, + ) + } + + assertEquals("Symbolic probes support exactly 30 and 120 second budgets", failure.message) + assertFalse(Files.exists(directory.resolve("output"))) + } + private fun runFixture( sourceText: String, profile: CallsExperimentProfile = CallsExperimentProfile.FROZEN_STOP, exploratory: Boolean = false, retainRawStateDiagnostics: Boolean = false, forkLimit: ULong? = null, + frozenModelIds: Set? = null, + budgetMillis: Long = if (exploratory) 30_000 else 2_000, + solverLimitMillis: Long = 250, + timeQuantumMillis: Long = 25, + seed: Long = 17, + pathSelectionStrategy: PathSelectionStrategy = PathSelectionStrategy.BFS, ): CallsClassStartResult { val source = directory.resolve("Target.ts") Files.writeString(source, sourceText) @@ -461,9 +522,14 @@ class CallsClassStartSmokeTest { ledgerSha256 = "b".repeat(64), expectedClassCount = 1, profile = profile, - budgetMillis = if (exploratory) 30_000 else 2_000, + budgetMillis = budgetMillis, + solverLimitMillis = solverLimitMillis, + timeQuantumMillis = timeQuantumMillis, + seed = seed, + pathSelectionStrategy = pathSelectionStrategy, collectedStatesLimit = if (exploratory) null else 10, forkLimit = forkLimit, + frozenModelIds = frozenModelIds, classes = listOf(case), retainRawStateDiagnostics = retainRawStateDiagnostics, )