diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/ConstantTimeFairPathSelector.kt b/usvm-core/src/main/kotlin/org/usvm/ps/ConstantTimeFairPathSelector.kt index 8013846c87..1eaba77d8b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/ConstantTimeFairPathSelector.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/ConstantTimeFairPathSelector.kt @@ -32,6 +32,7 @@ class ConstantTimeFairPathSelector KeyPriority, basePathSelectorFactory: (Key) -> UPathSelector, private val maxTimeQuantum: Duration = Duration.INFINITE, + private val onTimeQuantum: (Key, Duration, Duration) -> Unit = { _, _, _ -> }, ) : KeyedPathSelector(getKey) { private data class KeysQueueElement(val key: Key, var priority: KeyPriority, var elapsed: Duration) @@ -72,6 +73,15 @@ class ConstantTimeFairPathSelector= currentTimeQuantum // When time quantum is exceeded or there is nothing to peek, start peeking the next one if (quantumEnded || isCurrentPathSelectorEmpty) { - stopwatch.stop() + finishTimeQuantum() activeQueue.remove(currentKey) if (!isCurrentPathSelectorEmpty) { currentKey.elapsed += stopwatch.elapsed diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt index 80e5f175a8..9a3d0b4c94 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt @@ -228,7 +228,10 @@ fun createPathSelector( getKeyPriority = getMethodCoverage, basePathSelectorFactory = ::createBasePathSelector, maxTimeQuantum = options.maxEntryPointTimeQuantum, - ) + onTimeQuantum = timeStatistics.onEntryPointTimeQuantum, + ).also { selector -> + timeStatistics.finishTimeQuantum = selector::finishTimeQuantum + } } PathSelectorFairnessStrategy.COMPLETELY_FAIR -> diff --git a/usvm-core/src/main/kotlin/org/usvm/solver/USolverQueryEvent.kt b/usvm-core/src/main/kotlin/org/usvm/solver/USolverQueryEvent.kt new file mode 100644 index 0000000000..bc408e7e17 --- /dev/null +++ b/usvm-core/src/main/kotlin/org/usvm/solver/USolverQueryEvent.kt @@ -0,0 +1,66 @@ +package org.usvm.solver + +import io.ksmt.expr.KExpr +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus +import io.ksmt.sort.KBoolSort +import mu.KLogging +import kotlin.time.Duration +import kotlin.time.TimeSource + +private val logger = object : KLogging() {}.logger + +/** + * One completed KSolver check or checkWithAssumptions call, including a failed call. + * + * Measures wall time inside the check, excluding assertions, model decoding and type solving. + * This is not the total cost of a USolver query, which may perform several SMT checks. + */ +data class USolverQueryEvent( + val elapsedNanos: Long, + val status: KSolverStatus?, + val failure: String?, +) + +/** Observer failures are logged without changing the solver result or exception. */ +fun observeSolverQueries( + solver: KSolver, + observer: (USolverQueryEvent) -> Unit, +): KSolver = ObservedSolver(solver = solver, observer = observer) + +internal class ObservedSolver( + private val solver: KSolver, + private val observer: (USolverQueryEvent) -> Unit, + private val timeSource: TimeSource = TimeSource.Monotonic, +) : KSolver by solver { + override fun check(timeout: Duration): KSolverStatus = measured { solver.check(timeout = timeout) } + + override fun checkWithAssumptions( + assumptions: List>, + timeout: Duration, + ): KSolverStatus = measured { solver.checkWithAssumptions(assumptions = assumptions, timeout = timeout) } + + @Suppress("TooGenericExceptionCaught") // Report every backend failure and rethrow the same exception. + private inline fun measured(block: () -> KSolverStatus): KSolverStatus { + val started = timeSource.markNow() + var status: KSolverStatus? = null + var failure: String? = null + try { + val result = block() + status = result + return result + } catch (error: Throwable) { + failure = error::class.java.name + throw error + } finally { + val event = USolverQueryEvent( + elapsedNanos = started.elapsedNow().inWholeNanoseconds, + status = status, + failure = failure, + ) + runCatching { observer(event) } + .onFailure { error -> logger.warn(error) { "Solver query observer failed while recording an event" } } + } + } +} diff --git a/usvm-core/src/main/kotlin/org/usvm/statistics/TimeStatistics.kt b/usvm-core/src/main/kotlin/org/usvm/statistics/TimeStatistics.kt index e767489bfb..ec434a2e40 100644 --- a/usvm-core/src/main/kotlin/org/usvm/statistics/TimeStatistics.kt +++ b/usvm-core/src/main/kotlin/org/usvm/statistics/TimeStatistics.kt @@ -7,7 +7,11 @@ import kotlin.time.Duration /** * Maintains information about time spent on machine processes. */ -class TimeStatistics> : UMachineObserver { +class TimeStatistics>( + val onEntryPointTimeQuantum: (Method, Duration, Duration) -> Unit = { _, _, _ -> }, +) : UMachineObserver { + internal var finishTimeQuantum: () -> Unit = { } + private val stopwatch = RealTimeStopwatch() private val methodStopwatch = RealTimeStopwatch() @@ -30,6 +34,7 @@ class TimeStatistics> : UMachi override fun onMachineStopped() { check(stopwatch.isRunning) { "Machine stopwatch was not running on machine stopped" } + finishTimeQuantum() stopwatch.stop() methodStopwatch.stop() } diff --git a/usvm-core/src/test/kotlin/org/usvm/ps/ConstantTimeFairPathSelectorQuantumTest.kt b/usvm-core/src/test/kotlin/org/usvm/ps/ConstantTimeFairPathSelectorQuantumTest.kt index f5e7a5bddb..e756838a26 100644 --- a/usvm-core/src/test/kotlin/org/usvm/ps/ConstantTimeFairPathSelectorQuantumTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/ps/ConstantTimeFairPathSelectorQuantumTest.kt @@ -99,6 +99,55 @@ class ConstantTimeFairPathSelectorQuantumTest { assertEquals(expected = "b1", actual = nextState) } + @Test + fun `measured turns preserve overrun and final partial turn exactly once`() { + val stopwatch = TestStopwatch() + val turns = mutableListOf>() + val selector = selector( + stopwatch = stopwatch, + remainingTime = { 30.seconds }, + maxTimeQuantum = 2.seconds, + onTimeQuantum = { key, requested, elapsed -> turns += Triple(key, requested, elapsed) }, + ) + selector.add(states = listOf("a1", "b1", "c1")) + assertEquals(expected = "a1", actual = selector.peek()) + + stopwatch.elapsedRaw = 4L + assertEquals(expected = "b1", actual = selector.peek()) + stopwatch.elapsedRaw = 1L + selector.finishTimeQuantum() + selector.finishTimeQuantum() + + assertEquals( + expected = listOf(Triple('a', 2.seconds, 4.seconds), Triple('b', 2.seconds, 1.seconds)), + actual = turns, + ) + } + + @Test + fun `successive turns of the only remaining key remain distinct`() { + val stopwatch = TestStopwatch() + val turns = mutableListOf>() + val selector = selector( + stopwatch = stopwatch, + remainingTime = { 30.seconds }, + maxTimeQuantum = 2.seconds, + onTimeQuantum = { key, requested, elapsed -> turns += Triple(key, requested, elapsed) }, + ) + selector.add(states = listOf("a1")) + assertEquals(expected = "a1", actual = selector.peek()) + + stopwatch.elapsedRaw = 2L + assertEquals(expected = "a1", actual = selector.peek()) + stopwatch.elapsedRaw = 1L + selector.finishTimeQuantum() + + assertEquals( + expected = listOf(Triple('a', 2.seconds, 2.seconds), Triple('a', 2.seconds, 1.seconds)), + actual = turns, + ) + } + @Test fun `nonpositive turn bounds are rejected`() { for (quantum in listOf(Duration.ZERO, -1.seconds)) { @@ -118,6 +167,7 @@ class ConstantTimeFairPathSelectorQuantumTest { stopwatch: TestStopwatch, remainingTime: () -> Duration, maxTimeQuantum: Duration, + onTimeQuantum: (Char, Duration, Duration) -> Unit = { _, _, _ -> }, ): ConstantTimeFairPathSelector = ConstantTimeFairPathSelector( initialKeys = setOf('a', 'b', 'c'), stopwatch = stopwatch, @@ -126,5 +176,6 @@ class ConstantTimeFairPathSelectorQuantumTest { getKeyPriority = { key -> key }, basePathSelectorFactory = { BfsPathSelector() }, maxTimeQuantum = maxTimeQuantum, + onTimeQuantum = onTimeQuantum, ) } diff --git a/usvm-core/src/test/kotlin/org/usvm/ps/PathSelectorDrainTest.kt b/usvm-core/src/test/kotlin/org/usvm/ps/PathSelectorDrainTest.kt index d3d7b18d33..783fb0b3dd 100644 --- a/usvm-core/src/test/kotlin/org/usvm/ps/PathSelectorDrainTest.kt +++ b/usvm-core/src/test/kotlin/org/usvm/ps/PathSelectorDrainTest.kt @@ -15,6 +15,7 @@ import kotlin.test.assertEquals import kotlin.test.assertFalse import kotlin.test.assertSame import kotlin.test.assertTrue +import kotlin.time.Duration import kotlin.time.Duration.Companion.seconds class PathSelectorDrainTest { @@ -34,6 +35,7 @@ class PathSelectorDrainTest { fun `constant time drain includes unvisited keys without new scheduling events`() { val stopwatch = TestStopwatch() val children = mutableMapOf>() + val turns = mutableListOf>() var stopped = false val selector = ConstantTimeFairPathSelector( initialKeys = setOf('a', 'b', 'c'), @@ -49,11 +51,12 @@ class PathSelectorDrainTest { }, basePathSelectorFactory = { key -> TrackingSelector().also { children[key] = it } }, maxTimeQuantum = 2.seconds, + onTimeQuantum = { key, requested, elapsed -> turns += Triple(key, requested, elapsed) }, ) selector.add(states = listOf("a1", "a2", "b1", "c1")) assertEquals(expected = "a1", actual = selector.peek()) stopwatch.elapsedRaw = 3L - stopwatch.stop() + selector.finishTimeQuantum() stopped = true val drained = selector.drain().toList() @@ -61,6 +64,7 @@ class PathSelectorDrainTest { assertEquals(expected = setOf("a1", "a2", "b1", "c1"), actual = drained.toSet()) assertEquals(expected = 4, actual = drained.size) assertEquals(expected = 1, actual = children.values.sumOf { it.peekCount }) + assertEquals(expected = listOf(Triple('a', 2.seconds, 3.seconds)), actual = turns) assertEquals(expected = 3.seconds, actual = stopwatch.elapsed) assertFalse(stopwatch.isRunning) assertTrue(selector.isEmpty()) diff --git a/usvm-core/src/test/kotlin/org/usvm/solver/ObservedSolverTest.kt b/usvm-core/src/test/kotlin/org/usvm/solver/ObservedSolverTest.kt new file mode 100644 index 0000000000..4650aaadeb --- /dev/null +++ b/usvm-core/src/test/kotlin/org/usvm/solver/ObservedSolverTest.kt @@ -0,0 +1,218 @@ +package org.usvm.solver + +import io.ksmt.KContext +import io.ksmt.expr.KExpr +import io.ksmt.solver.KModel +import io.ksmt.solver.KSolver +import io.ksmt.solver.KSolverConfiguration +import io.ksmt.solver.KSolverStatus +import io.ksmt.solver.yices.KYicesSolver +import io.ksmt.solver.z3.KZ3Solver +import io.ksmt.sort.KBoolSort +import io.mockk.Runs +import io.mockk.every +import io.mockk.just +import io.mockk.mockk +import io.mockk.verify +import org.junit.jupiter.api.Test +import org.junit.jupiter.params.ParameterizedTest +import org.junit.jupiter.params.provider.EnumSource +import org.junit.jupiter.params.provider.ValueSource +import org.usvm.SolverType +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertNull +import kotlin.test.assertSame +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.milliseconds +import kotlin.time.Duration.Companion.seconds +import kotlin.time.TestTimeSource + +class ObservedSolverTest { + @ParameterizedTest + @EnumSource(SolverType::class) + fun `real solvers report every ordinary and assumption check`(solverType: SolverType) { + val events = mutableListOf() + KContext().use { ctx -> + val solver = when (solverType) { + SolverType.YICES -> KYicesSolver(ctx) + SolverType.Z3 -> KZ3Solver(ctx) + } + observeSolverQueries(solver = solver, observer = { event -> events += event }).use { observed -> + val initial = observed.check(timeout = 2.seconds) + observed.push() + observed.assert(ctx.falseExpr) + val asserted = observed.check(timeout = 2.seconds) + observed.pop(n = 1u) + val assumed = observed.checkWithAssumptions(assumptions = listOf(ctx.falseExpr), timeout = 2.seconds) + val final = observed.check(timeout = 2.seconds) + + val expected = listOf(KSolverStatus.SAT, KSolverStatus.UNSAT, KSolverStatus.UNSAT, KSolverStatus.SAT) + assertEquals(expected = expected, actual = listOf(initial, asserted, assumed, final)) + assertEquals(expected = expected, actual = events.map { it.status }) + assertTrue(actual = events.all { it.failure == null && it.elapsedNanos >= 0 }) + } + } + } + + @ParameterizedTest + @EnumSource(KSolverStatus::class) + fun `ordinary checks preserve status and timeout`(status: KSolverStatus) { + val solver = mockk>() + val events = mutableListOf() + every { solver.check(timeout = 2.seconds) } returns status + val observed = observeSolverQueries(solver = solver, observer = { event -> events += event }) + + val result = observed.check(timeout = 2.seconds) + + assertEquals(expected = status, actual = result) + assertEquals(expected = status, actual = events.single().status) + assertNull(actual = events.single().failure) + verify(exactly = 1) { solver.check(timeout = 2.seconds) } + } + + @ParameterizedTest + @EnumSource(KSolverStatus::class) + fun `assumption checks preserve assumptions status and timeout`(status: KSolverStatus) { + val solver = mockk>() + val assumptions = listOf(mockk>()) + val events = mutableListOf() + every { solver.checkWithAssumptions(assumptions = any(), timeout = 2.seconds) } answers { + assertSame(expected = assumptions, actual = firstArg()) + status + } + val observed = observeSolverQueries(solver = solver, observer = { event -> events += event }) + + val result = observed.checkWithAssumptions(assumptions = assumptions, timeout = 2.seconds) + + assertEquals(expected = status, actual = result) + assertEquals(expected = status, actual = events.single().status) + assertNull(actual = events.single().failure) + verify(exactly = 1) { solver.checkWithAssumptions(assumptions = assumptions, timeout = 2.seconds) } + } + + @ParameterizedTest + @ValueSource(booleans = [false, true]) + fun `failed checks report one event and rethrow the same exception`(useAssumptions: Boolean) { + val solver = mockk>() + val failure = IllegalStateException("backend failure") + val events = mutableListOf() + every { solver.check(timeout = any()) } throws failure + every { solver.checkWithAssumptions(assumptions = any(), timeout = any()) } throws failure + val observed = observeSolverQueries(solver = solver, observer = { event -> events += event }) + + val caught = assertFailsWith { + if (useAssumptions) { + observed.checkWithAssumptions(assumptions = emptyList(), timeout = 2.seconds) + } else { + observed.check(timeout = 2.seconds) + } + } + + assertSame(expected = failure, actual = caught) + assertNull(actual = events.single().status) + assertEquals(expected = failure::class.java.name, actual = events.single().failure) + assertTrue(actual = events.single().elapsedNanos >= 0) + } + + @Test + fun `observer failure does not replace a solver result`() { + val solver = mockk>() + val events = mutableListOf() + every { solver.check(timeout = any()) } returns KSolverStatus.SAT + val observed = observeSolverQueries( + solver = solver, + observer = { event -> + events += event + error("observer failure") + }, + ) + + val result = observed.check(timeout = 2.seconds) + + assertEquals(expected = KSolverStatus.SAT, actual = result) + assertEquals(expected = KSolverStatus.SAT, actual = events.single().status) + assertNull(actual = events.single().failure) + } + + @Test + fun `observer failure does not replace a backend exception`() { + val solver = mockk>() + val failure = IllegalStateException("backend failure") + val events = mutableListOf() + every { solver.check(timeout = any()) } throws failure + val observed = observeSolverQueries( + solver = solver, + observer = { event -> + events += event + throw IllegalArgumentException("observer failure") + }, + ) + + val caught = assertFailsWith { observed.check(timeout = 2.seconds) } + + assertSame(expected = failure, actual = caught) + assertNull(actual = events.single().status) + assertEquals(expected = failure::class.java.name, actual = events.single().failure) + } + + @Test + fun `each retry has its own elapsed time excluding observer work`() { + val solver = mockk>() + val clock = TestTimeSource() + val events = mutableListOf() + var checks = 0 + every { solver.checkWithAssumptions(assumptions = any(), timeout = any()) } answers { + checks++ + clock += 3.milliseconds + if (checks == 1) KSolverStatus.UNSAT else KSolverStatus.SAT + } + val observed = ObservedSolver( + solver = solver, + observer = { event -> + events += event + clock += 10.seconds + }, + timeSource = clock, + ) + + val first = observed.checkWithAssumptions(assumptions = emptyList(), timeout = 2.seconds) + val second = observed.checkWithAssumptions(assumptions = emptyList(), timeout = 2.seconds) + + assertEquals(expected = KSolverStatus.UNSAT, actual = first) + assertEquals(expected = KSolverStatus.SAT, actual = second) + assertEquals(expected = listOf(KSolverStatus.UNSAT, KSolverStatus.SAT), actual = events.map { it.status }) + assertEquals(expected = listOf(3_000_000L, 3_000_000L), actual = events.map { it.elapsedNanos }) + verify(exactly = 2) { solver.checkWithAssumptions(assumptions = emptyList(), timeout = 2.seconds) } + } + + @Test + fun `assertions model retrieval and lifecycle are delegated without query events`() { + val solver = mockk>() + val assertion = mockk>() + val model = mockk() + val events = mutableListOf() + every { solver.push() } just Runs + every { solver.assert(assertion) } just Runs + every { solver.model() } returns model + every { solver.pop(n = 1u) } just Runs + every { solver.close() } just Runs + val observed = observeSolverQueries(solver = solver, observer = { event -> events += event }) + + observed.push() + observed.assert(assertion) + val result = observed.model() + observed.pop(n = 1u) + observed.close() + + assertSame(expected = model, actual = result) + assertTrue(actual = events.isEmpty()) + verify(exactly = 1) { + solver.push() + solver.assert(assertion) + solver.model() + solver.pop(n = 1u) + solver.close() + } + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt index 880e00f114..e24176e963 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsComponents.kt @@ -18,11 +18,13 @@ import org.usvm.model.ULazyModelDecoder import org.usvm.solver.UExprTranslator import org.usvm.solver.USolverBase import org.usvm.solver.UTypeSolver +import org.usvm.solver.observeSolverQueries import org.usvm.types.UTypeSystem class TsComponents( private val typeSystem: TsTypeSystem, private val options: UMachineOptions, + private val solverQueryObserver: ((TsSolverQueryEvent) -> Unit)? = null, ) : UComponents { private val closeableResources = mutableListOf() @@ -65,7 +67,11 @@ class TsComponents( val typeSolver = UTypeSolver(typeSystem) - return USolverBase(ctx, smtSolver, typeSolver, translator, decoder, options.solverTimeout) + val observedSolver = solverQueryObserver?.let { observer -> + observeSolverQueries(solver = smtSolver, observer = observer) + } ?: smtSolver + + return USolverBase(ctx, observedSolver, typeSolver, translator, decoder, options.solverTimeout) } fun close() { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsEntryPointTimeQuantumEvent.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsEntryPointTimeQuantumEvent.kt new file mode 100644 index 0000000000..e9a8146608 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsEntryPointTimeQuantumEvent.kt @@ -0,0 +1,11 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsMethod +import kotlin.time.Duration + +/** Selector turn time can exceed the request because an interpreter/solver step cannot be preempted. */ +data class TsEntryPointTimeQuantumEvent( + val entrypoint: EtsMethod, + val requested: Duration, + val elapsed: Duration, +) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index 4e64a3119d..abe997f713 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -15,6 +15,16 @@ import org.usvm.statistics.UInterpreterObserver @Suppress("unused") interface TsInterpreterObserver : UInterpreterObserver { + /** Each completed selector turn, including the final partial turn and repeated turns of one entry point. */ + fun onEntryPointTimeQuantum(event: TsEntryPointTimeQuantumEvent) { + // default empty implementation + } + + /** Actual SMT checks, including retries with soft assumptions; setup queries are also reported. */ + fun onSolverQuery(event: TsSolverQueryEvent) { + // default empty implementation + } + /** * Called after the dispatcher completes a model or fallback decision for an unknown call. * A model decision is reported once after all its satisfiable successor callbacks complete. diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 079d72f26e..54efdbc45f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -76,7 +76,7 @@ class TsMachine( override val options: UMachineOptions = UMachineOptions(solverType = SolverType.YICES), private val tsOptions: TsOptions, private val machineObserver: UMachineObserver? = null, - observer: TsInterpreterObserver? = null, + private val observer: TsInterpreterObserver? = null, unknownCallDispatcher: TsUnknownCallDispatcher? = null, unknownCallModels: TsUnknownCallModelCatalog? = null, ) : UMachine() { @@ -107,7 +107,11 @@ class TsMachine( private val runtimeScene = analysisScene.withCoreRuntimeSdk() private val graph = TsGraph(runtimeScene) private val typeSystem = TsTypeSystem(runtimeScene, typeOperationsTimeout = 1.seconds, graph.hierarchy) - private val components = TsComponents(typeSystem, options) + private val components = TsComponents( + typeSystem = typeSystem, + options = options, + solverQueryObserver = observer?.let { it::onSolverQuery }, + ) private val ctx = TsContext( scene = runtimeScene, components = components, @@ -159,6 +163,14 @@ class TsMachine( ) } + private fun createTimeStatistics(): TimeStatistics = TimeStatistics( + onEntryPointTimeQuantum = { method, requested, elapsed -> + observer?.onEntryPointTimeQuantum( + TsEntryPointTimeQuantumEvent(entrypoint = method, requested = requested, elapsed = elapsed), + ) + }, + ) + fun analyzeWithMetadata( methods: List, targets: List = emptyList(), @@ -190,7 +202,7 @@ class TsMachine( else -> TODO("Unsupported yet") } - val timeStatistics = TimeStatistics() + val timeStatistics = createTimeStatistics() val pathSelector = createPathSelector( initialStates = initialStates, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsSolverQueryEvent.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsSolverQueryEvent.kt new file mode 100644 index 0000000000..c0f2fad44a --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsSolverQueryEvent.kt @@ -0,0 +1,6 @@ +package org.usvm.machine + +import org.usvm.solver.USolverQueryEvent + +/** TS observer API alias for the shared SMT query event. */ +typealias TsSolverQueryEvent = USolverQueryEvent