[TS] Use Yices for all TypeScript machines

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageCell.kt

@@ -2,6 +2,7 @@ package org.usvm.ts.calls
 
 import kotlinx.serialization.Serializable
 import kotlinx.serialization.decodeFromString
+import org.usvm.SolverType
 import org.usvm.ts.pbt.model.encodeToUtf8SafeString
 import java.nio.ByteBuffer
 import java.nio.channels.FileChannel
@@ -37,6 +38,7 @@ internal data class CallsCoverageCellIdentity(
     val nativeFrontendRevision: String,
     val sourceManifest: String,
     val sourceIdentity: CallsCoverageSourceIdentity,
+    val solver: String,
     val projectIndex: Int,
     val functionIndex: Int,
     val profile: CallsExperimentProfile,
@@ -96,6 +98,11 @@ internal fun runCoverageUniverse(
         projectIndex = projectIndex,
         functionIndex = functionIndex,
     )
+    validateCoverageManifestBuild(
+        manifest = source.manifest,
+        runtimeToolRevision = runtimeToolRevision,
+        runtimeNativeFrontendRevision = runtimeNativeFrontendRevision,
+    )
     val output = Path.of(arguments.next()).toAbsolutePath().normalize()
     require(System.getenv("ETS_FRONTEND_SCRIPT") == null) { "ETS_FRONTEND_SCRIPT must be unset" }
 
@@ -199,6 +206,11 @@ private fun parseCoverageCellRequest(
     val projectIndex = arguments.next().toInt()
     val functionIndex = arguments.next().toInt()
     val source = CallsCoverageSource.load(manifestPath, projectIndex = projectIndex, functionIndex = functionIndex)
+    validateCoverageManifestBuild(
+        manifest = source.manifest,
+        runtimeToolRevision = runtimeToolRevision,
+        runtimeNativeFrontendRevision = runtimeNativeFrontendRevision,
+    )
     val profile = CallsExperimentProfile.valueOf(arguments.next())
     val seed = arguments.next().toLong()
     val output = Path.of(arguments.next()).toAbsolutePath().normalize()
@@ -229,11 +241,12 @@ private fun parseCoverageCellRequest(
 
 
     val identity = CallsCoverageCellIdentity(
-        schemaVersion = 2,
+        schemaVersion = 3,
         toolRevision = runtimeToolRevision,
         nativeFrontendRevision = runtimeNativeFrontendRevision,
         sourceManifest = source.manifestPath.toString(),
         sourceIdentity = source.identity,
+        solver = source.manifest.solver,
         projectIndex = projectIndex,
         functionIndex = functionIndex,
         profile = profile,
@@ -271,6 +284,7 @@ private fun loadOrRunCoverageSearch(
             seed = identity.seed,
             budget = identity.budgetMillis.milliseconds,
             solverQueryLimit = identity.solverLimitMillis.milliseconds,
+            solverType = SolverType.valueOf(identity.solver),
             candidateCap = identity.candidateCap,
             onCandidate = { candidate -> appendDurably(candidatePath, encode(candidate)) },
         )
@@ -347,6 +361,19 @@ private fun coverageCheckpoints(
     }
 }
 
+private fun validateCoverageManifestBuild(
+    manifest: CallsExperimentManifest,
+    runtimeToolRevision: String,
+    runtimeNativeFrontendRevision: String,
+) {
+    require(manifest.toolRevision == runtimeToolRevision) {
+        "Coverage manifest tool revision differs from the running build"
+    }
+    require(manifest.nativeFrontendRevision == runtimeNativeFrontendRevision) {
+        "Coverage manifest frontend revision differs from the running build"
+    }
+}
+
 private inline fun <reified T> readLines(path: Path): List<T> = if (Files.exists(path)) {
     Files.readAllLines(path).filter(String::isNotBlank).map { line ->
         CallsExperimentJson.json.decodeFromString<T>(line)

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt

@@ -79,6 +79,7 @@ internal data class CallsCoverageSearchRequest(
     val seed: Long,
     val budget: Duration,
     val solverQueryLimit: Duration,
+    val solverType: SolverType = SolverType.YICES,
     val candidateCap: Int,
     val onCandidate: (CallsCoverageCandidate) -> Unit = {},
 ) {
@@ -203,7 +204,7 @@ internal class CurrentTsCallsCoverageEngine(
             randomSeed = request.seed,
             timeout = request.budget,
             solverTimeout = request.solverQueryLimit,
-            solverType = SolverType.Z3,
+            solverType = request.solverType,
             stopOnCoverage = CALLS_STOP_ON_COVERAGE,
             stopOnTargetsReached = false,
             throwExceptionOnStepFailure = true,

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsExperiment.kt

@@ -5,6 +5,7 @@ import kotlinx.serialization.Serializable
 import kotlinx.serialization.decodeFromString
 import kotlinx.serialization.json.Json
 import org.usvm.PathSelectionStrategy
+import org.usvm.SolverType
 import org.usvm.machine.TsRuntimeFeatureLimitationEvent
 import org.usvm.machine.call.TsResidualCallPolicy
 import org.usvm.machine.call.TsUnknownCallEvent
@@ -77,7 +78,7 @@ internal data class CallsExperimentManifest(
         require(seeds.isNotEmpty() && seeds.distinct().size == seeds.size) { "Seeds must be non-empty and unique" }
         require(perTargetBudgetMillis > 0) { "Per-target budget must be positive" }
         require(projects.isNotEmpty()) { "At least one project is required" }
-        require(solver == "Z3") { "The frozen calls experiment requires the Z3 solver" }
+        require(solver == "YICES" || solver == "Z3") { "Unsupported calls experiment solver: $solver" }
         require(searchPolicy == CALLS_PATH_SELECTION_STRATEGY.name) {
             "The frozen calls experiment requires ${CALLS_PATH_SELECTION_STRATEGY.name} search"
         }
@@ -135,6 +136,7 @@ internal data class CallsSymbolicSearchRequest(
     val expectedNativeFrontendRevision: String,
     val seed: Long,
     val budget: Duration,
+    val solverType: SolverType = SolverType.YICES,
     val unknownCallEventSink: ((TsUnknownCallEvent) -> Unit)? = null,
     val runtimeLimitationEventSink: ((TsRuntimeFeatureLimitationEvent) -> Unit)? = null,
 )
@@ -421,6 +423,7 @@ internal class CallsExperimentRunner(
             expectedNativeFrontendRevision = manifest.nativeFrontendRevision,
             seed = seed,
             budget = manifest.perTargetBudgetMillis.milliseconds,
+            solverType = SolverType.valueOf(manifest.solver),
         )
         val eventWrites = CallsEventWriteTracker()
         val unknownCallSink = callsUnknownCallEventSink(

usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt

@@ -6,7 +6,6 @@ import org.jacodb.ets.model.EtsMethod
 import org.jacodb.ets.model.EtsReturnStmt
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsStmt
-import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachineOptions
 import org.usvm.machine.TsAnalysisStopReason
@@ -176,7 +175,7 @@ internal class CurrentTsCallsSymbolicEngine(
             stateCollectionStrategy = StateCollectionStrategy.REACHED_TARGET,
             randomSeed = request.seed,
             timeout = request.budget,
-            solverType = SolverType.Z3,
+            solverType = request.solverType,
             stopOnCoverage = CALLS_STOP_ON_COVERAGE,
             stopOnTargetsReached = false,
             throwExceptionOnStepFailure = true,

usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt

@@ -1,6 +1,7 @@
 package org.usvm.ts.calls
 
 import org.junit.jupiter.api.io.TempDir
+import org.usvm.SolverType
 import org.usvm.ts.pbt.model.ArrayDomain
 import org.usvm.ts.pbt.model.BooleanDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
@@ -69,6 +70,31 @@ class CallsCoverageExperimentTest {
         assertTrue(universe.probeElapsedMillis >= 0)
     }
 
+    @Test
+    fun `coverage search honors either explicitly configured solver`() {
+        val fixture = fixture(
+            source = """
+                export function classify(flag: boolean): number {
+                  if (flag) return 1;
+                  return 2;
+                }
+            """.trimIndent(),
+            exportName = "classify",
+            inputs = listOf(PropertyInput(name = "flag", domain = BooleanDomain)),
+        )
+        for (solverType in listOf(SolverType.YICES, SolverType.Z3)) {
+            val emitted = mutableListOf<CallsCoverageCandidate>()
+
+            val search = CurrentTsCallsCoverageEngine(testSourceEngine()).search(
+                request = coverageRequest(fixture, onCandidate = emitted::add, solverType = solverType),
+            )
+
+            assertEquals(CallsCoverageSearchStatus.EXHAUSTED, search.status, search.toString())
+            assertEquals(2, search.candidates.size)
+            assertEquals(search.candidates, emitted)
+        }
+    }
+
     @Test
     fun `coverage universe has a denominator without invoking the entry function`() {
         val fixture = fixture(
@@ -273,6 +299,7 @@ class CallsCoverageExperimentTest {
     private fun coverageRequest(
         fixture: CoverageFixture,
         onCandidate: (CallsCoverageCandidate) -> Unit,
+        solverType: SolverType = SolverType.YICES,
     ) = CallsCoverageSearchRequest(
         sourceRoot = fixture.sourceRoot,
         project = fixture.project,
@@ -283,6 +310,7 @@ class CallsCoverageExperimentTest {
         seed = 17,
         budget = 10.seconds,
         solverQueryLimit = 2.seconds,
+        solverType = solverType,
         candidateCap = 8,
         onCandidate = onCandidate,
     )

usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageSourceTest.kt

@@ -2,6 +2,7 @@ package org.usvm.ts.calls
 
 import kotlinx.serialization.decodeFromString
 import org.junit.jupiter.api.io.TempDir
+import org.usvm.SolverType
 import org.usvm.ts.pbt.model.BooleanDomain
 import org.usvm.ts.pbt.model.NumberDomain
 import org.usvm.ts.pbt.model.PropertyInput
@@ -32,6 +33,102 @@ class CallsCoverageSourceTest {
         )
         assertEquals(emptySearch, result.search)
         assertEquals(fixture.source.identity, result.identity.sourceIdentity)
+        assertEquals(3, result.identity.schemaVersion)
+        assertEquals("YICES", result.identity.solver)
+    }
+
+    @Test
+    fun `coverage cell forwards the explicit manifest solver to search`() {
+        val fixture = fixture(solver = "Z3")
+        val solvers = mutableListOf<SolverType>()
+
+        fixture.runCell(searchFunction = { request ->
+            solvers += request.solverType
+            emptySearch
+        })
+
+        val result = CallsExperimentJson.json.decodeFromString<CallsCoverageCellResult>(
+            Files.readString(fixture.output.resolve("result.json")),
+        )
+        assertEquals(listOf(SolverType.Z3), solvers)
+        assertEquals("Z3", result.identity.solver)
+    }
+
+    @Test
+    fun `resumed search rejects a persisted identity from a different solver`() {
+        val fixture = fixture()
+        fixture.persistSearch(solver = "Z3")
+
+        val failure = assertFailsWith<IllegalArgumentException> { fixture.runCell() }
+
+        assertEquals("Cell identity changed", failure.message)
+        fixture.assertNoReplayOrCompletion()
+    }
+
+    @Test
+    fun `resumed search rejects the prior cell schema`() {
+        val fixture = fixture()
+        fixture.persistSearch(schemaVersion = 2)
+
+        val failure = assertFailsWith<IllegalArgumentException> { fixture.runCell() }
+
+        assertEquals("Cell identity changed", failure.message)
+        fixture.assertNoReplayOrCompletion()
+    }
+
+    @Test
+    fun `build mismatch rejects search and universe collection before callbacks`() {
+        val fixture = fixture()
+        var searched = false
+        var probed = false
+        val otherRevision = "2222222222222222222222222222222222222222"
+
+        val searchFailure = assertFailsWith<IllegalArgumentException> {
+            fixture.runCell(runtimeToolRevision = otherRevision, searchFunction = {
+                searched = true
+                emptySearch
+            })
+        }
+        val universeFailure = assertFailsWith<IllegalArgumentException> {
+            fixture.runUniverse(runtimeToolRevision = otherRevision, probeFunction = {
+                probed = true
+                sampleUniverse
+            })
+        }
+
+        assertEquals("Coverage manifest tool revision differs from the running build", searchFailure.message)
+        assertEquals(searchFailure.message, universeFailure.message)
+        assertFalse(searched)
+        assertFalse(probed)
+        assertFalse(Files.exists(fixture.output.resolve("identity.json")))
+        assertFalse(Files.exists(directory.resolve("universe-output/universe.json")))
+    }
+
+    @Test
+    fun `frontend mismatch rejects search and universe collection before callbacks`() {
+        val fixture = fixture()
+        var searched = false
+        var probed = false
+
+        val searchFailure = assertFailsWith<IllegalArgumentException> {
+            fixture.runCell(runtimeNativeFrontendRevision = "bundled:other", searchFunction = {
+                searched = true
+                emptySearch
+            })
+        }
+        val universeFailure = assertFailsWith<IllegalArgumentException> {
+            fixture.runUniverse(runtimeNativeFrontendRevision = "bundled:other", probeFunction = {
+                probed = true
+                sampleUniverse
+            })
+        }
+
+        assertEquals("Coverage manifest frontend revision differs from the running build", searchFailure.message)
+        assertEquals(searchFailure.message, universeFailure.message)
+        assertFalse(searched)
+        assertFalse(probed)
+        assertFalse(Files.exists(fixture.output.resolve("identity.json")))
+        assertFalse(Files.exists(directory.resolve("universe-output/universe.json")))
     }
 
     @Test
@@ -189,7 +286,7 @@ class CallsCoverageSourceTest {
         assertFalse(Files.exists(directory.resolve("universe-output/universe.json")))
     }
 
-    private fun fixture(): Fixture {
+    private fun fixture(solver: String = "YICES"): Fixture {
         val sourceRoot = Files.createDirectory(directory.resolve("source"))
         val sourceFile = sourceRoot.resolve("Fixture.ts")
         Files.writeString(sourceFile, "export function first(flag: boolean): boolean { return flag; }")
@@ -218,7 +315,7 @@ class CallsCoverageSourceTest {
             experimentId = "coverage-identity",
             toolRevision = TOOL_REVISION,
             nativeFrontendRevision = FRONTEND_REVISION,
-            solver = "Z3",
+            solver = solver,
             searchPolicy = CALLS_PATH_SELECTION_STRATEGY.name,
             modelSet = CallsModelSetIdentity(ids = emptySet(), toolRevision = TOOL_REVISION),
             seeds = listOf(17L),
@@ -255,25 +352,30 @@ class CallsCoverageSourceTest {
             Files.writeString(universePath, CallsExperimentJson.json.encodeToUtf8SafeString(record))
         }
 
-        fun runUniverse(probeFunction: (CallsCoverageSource) -> CallsCoverageUniverse): Path {
+        fun runUniverse(
+            runtimeToolRevision: String = TOOL_REVISION,
+            runtimeNativeFrontendRevision: String = FRONTEND_REVISION,
+            probeFunction: (CallsCoverageSource) -> CallsCoverageUniverse,
+        ): Path {
             val output = manifestPath.resolveSibling("universe-output")
             runCoverageUniverse(
                 args = listOf(manifestPath.toString(), "0", "0", output.toString()),
-                runtimeToolRevision = TOOL_REVISION,
-                runtimeNativeFrontendRevision = FRONTEND_REVISION,
+                runtimeToolRevision = runtimeToolRevision,
+                runtimeNativeFrontendRevision = runtimeNativeFrontendRevision,
                 probeFunction = probeFunction,
             )
 
             return output
         }
 
-        fun persistSearch() {
+        fun persistSearch(schemaVersion: Int = 3, solver: String = source.manifest.solver) {
             val identity = CallsCoverageCellIdentity(
-                schemaVersion = 2,
+                schemaVersion = schemaVersion,
                 toolRevision = TOOL_REVISION,
                 nativeFrontendRevision = FRONTEND_REVISION,
                 sourceManifest = manifestPath.toRealPath().toString(),
                 sourceIdentity = source.identity,
+                solver = solver,
                 projectIndex = 0,
                 functionIndex = 0,
                 profile = CallsExperimentProfile.EMPTY_STOP,
@@ -295,6 +397,8 @@ class CallsCoverageSourceTest {
         }
 
         fun runCell(
+            runtimeToolRevision: String = TOOL_REVISION,
+            runtimeNativeFrontendRevision: String = FRONTEND_REVISION,
             searchFunction: (CallsCoverageSearchRequest) -> CallsCoverageSearchResult = {
                 error("Must resume persisted search")
             },
@@ -312,8 +416,8 @@ class CallsCoverageSourceTest {
                     "8",
                     universePath.toString(),
                 ),
-                runtimeToolRevision = TOOL_REVISION,
-                runtimeNativeFrontendRevision = FRONTEND_REVISION,
+                runtimeToolRevision = runtimeToolRevision,
+                runtimeNativeFrontendRevision = runtimeNativeFrontendRevision,
                 searchFunction = searchFunction,
             )
         }