[Calls] Configure frozen class probe models budgets and search receipts

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,

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,

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,13 +92,16 @@ 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,
     val seed: Long = 17,
     val profile: CallsExperimentProfile = CallsExperimentProfile.FROZEN_STOP,
     val classes: List<CallsClassStartCase>,
     val retainRawStateDiagnostics: Boolean = false,
+    val frozenModelIds: Set<String>? = null,
+    val maxInputCollectionSize: Int? = null,
 ) {
     init {
         require(schemaVersion == 1 && classes.size == expectedClassCount && expectedClassCount > 0)
@@ -408,7 +412,9 @@ private fun runRawClassAnalysis(args: List<String>, exploratory: Boolean) {
     val bytes = Files.readAllBytes(manifestPath)
     val manifest = CallsExperimentJson.json.decodeFromString<CallsClassStartManifest>(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<String>, 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<String>, 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<String>, exploratory: Boolean) {
 }
 
 private const val CLASS_START_ARGUMENT_COUNT = 3
-private const val EXPLORATORY_BUDGET_MILLIS = 30_000L
-private const val EXPLORATORY_SEED = 17L

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<T extends number>(value: T): number { return value > 0 ? 1 : 0; }
                 logical<T extends boolean>(value: T): number { return value ? 1 : 0; }
                 reference<T extends string>(value: T): number { return value.length; }
-                defaulted<T = number>(value: T): boolean { return typeof value === 'number'; }
+                defaulted<T = number>(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<IllegalArgumentException> {
+            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<String>? = 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,
         )