[TS] Reuse closest-to-uncovered NURS for external coverage

usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt

@@ -36,6 +36,7 @@ private fun <Method, Statement, Target, State> createPathSelector(
     cfgStatisticsFactory: () -> CfgStatistics<Method, Statement>? = { null },
     callGraphStatisticsFactory: () -> CallGraphStatistics<Method>? = { null },
     loopStatisticFactory: () -> StateLoopTracker<*, Statement, State>? = { null },
+    coverageDistanceCalculatorFactory: () -> CallStackDistanceCalculator<Method, Statement>? = { null },
 ): UPathSelector<State>
     where Target : UTarget<Statement, Target>,
           State : UState<*, Method, Statement, *, Target, State> {
@@ -69,14 +70,16 @@ private fun <Method, Statement, Target, State> createPathSelector(
             PathSelectionStrategy.CLOSEST_TO_UNCOVERED -> createClosestToUncoveredPathSelector(
                 requireNotNull(coverageStatisticsFactory()) { "Coverage statistics is required for closest to uncovered path selector" },
                 requireNotNull(cfgStatisticsFactory()) { "CFG statistics is required for closest to uncovered path selector" },
-                applicationGraph
+                applicationGraph,
+                distanceCalculator = coverageDistanceCalculatorFactory(),
             )
 
             PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM -> createClosestToUncoveredPathSelector(
                 requireNotNull(coverageStatisticsFactory()) { "Coverage statistics is required for closest to uncovered path selector" },
                 requireNotNull(cfgStatisticsFactory()) { "CFG statistics is required for closest to uncovered path selector" },
                 applicationGraph,
-                random
+                random,
+                distanceCalculator = coverageDistanceCalculatorFactory(),
             )
 
             PathSelectionStrategy.TARGETED -> createTargetedPathSelector<Method, Statement, Target, State>(
@@ -153,6 +156,7 @@ fun <Method, Statement, Target, State> createPathSelector(
     cfgStatisticsFactory: () -> CfgStatistics<Method, Statement>? = { null },
     callGraphStatisticsFactory: () -> CallGraphStatistics<Method>? = { null },
     loopStatisticFactory: () -> StateLoopTracker<*, Statement, State>? = { null },
+    coverageDistanceCalculatorFactory: () -> CallStackDistanceCalculator<Method, Statement>? = { null },
 ): UPathSelector<State> where Target : UTarget<Statement, Target>, State : UState<*, Method, Statement, *, Target, State> =
     createPathSelector(
         listOf(initialState),
@@ -161,7 +165,8 @@ fun <Method, Statement, Target, State> createPathSelector(
         coverageStatisticsFactory,
         cfgStatisticsFactory,
         callGraphStatisticsFactory,
-        loopStatisticFactory
+        loopStatisticFactory,
+        coverageDistanceCalculatorFactory,
     )
 
 fun <Method, Statement, Target, State> createPathSelector(
@@ -173,6 +178,7 @@ fun <Method, Statement, Target, State> createPathSelector(
     cfgStatisticsFactory: () -> CfgStatistics<Method, Statement>? = { null },
     callGraphStatisticsFactory: () -> CallGraphStatistics<Method>? = { null },
     loopStatisticFactory: () -> StateLoopTracker<*, Statement, State>? = { null },
+    coverageDistanceCalculatorFactory: () -> CallStackDistanceCalculator<Method, Statement>? = { null },
 ): UPathSelector<State> where Target : UTarget<Statement, Target>, State : UState<*, Method, Statement, *, Target, State> {
     val hasSingleEntryPoint = initialStates.size == 1
     val hasUnlimitedScheduling = options.timeout == Duration.INFINITE &&
@@ -185,7 +191,8 @@ fun <Method, Statement, Target, State> createPathSelector(
             coverageStatisticsFactory,
             cfgStatisticsFactory,
             callGraphStatisticsFactory,
-            loopStatisticFactory
+            loopStatisticFactory,
+            coverageDistanceCalculatorFactory,
         )
     }
 
@@ -202,7 +209,8 @@ fun <Method, Statement, Target, State> createPathSelector(
             coverageStatisticsFactory,
             cfgStatisticsFactory,
             callGraphStatisticsFactory,
-            loopStatisticFactory
+            loopStatisticFactory,
+            coverageDistanceCalculatorFactory,
         )
 
     val coverageStatistics = coverageStatisticsFactory()
@@ -317,15 +325,16 @@ private fun <Method, Statement, State : UState<*, Method, Statement, *, *, State
     cfgStatistics: CfgStatistics<Method, Statement>,
     applicationGraph: ApplicationGraph<Method, Statement>,
     random: Random? = null,
+    distanceCalculator: CallStackDistanceCalculator<Method, Statement>? = null,
 ): UPathSelector<State> {
-    val distanceCalculator = CallStackDistanceCalculator(
+    val calculator = distanceCalculator ?: CallStackDistanceCalculator(
         targets = coverageStatistics.getUncoveredStatements(),
         cfgStatistics = cfgStatistics,
         applicationGraph
     )
 
     coverageStatistics.addOnCoveredObserver { _, method, statement ->
-        distanceCalculator.removeTarget(
+        calculator.removeTarget(
             method,
             statement
         )
@@ -334,21 +343,25 @@ private fun <Method, Statement, State : UState<*, Method, Statement, *, *, State
     if (random == null) {
         return WeightedPathSelector(
             priorityCollectionFactory = { DeterministicPriorityCollection(Comparator.naturalOrder()) },
-            weighter = { distanceCalculator.calculateDistance(it.currentStatement, it.callStack) }
+            weighter = { calculator.calculateDistance(it.currentStatement, it.callStack) }
         )
     }
 
-    return WeightedPathSelector(
-        priorityCollectionFactory = { RandomizedPriorityCollection(compareById()) { random.nextDouble() } },
-        weighter = {
-            1.0 / max(
-                distanceCalculator.calculateDistance(it.currentStatement, it.callStack).toDouble(),
-                1.0
-            )
-        }
+    return createClosestToUncoveredRandomPathSelector(
+        distance = { calculator.calculateDistance(it.currentStatement, it.callStack) },
+        random = random,
     )
 }
 
+/** NURS weights change only on ordinary add/update; coverage changes never scan queued states. */
+fun <State : UState<*, *, *, *, *, State>> createClosestToUncoveredRandomPathSelector(
+    distance: StateWeighter<State, UInt>,
+    random: Random,
+): UPathSelector<State> = WeightedPathSelector(
+    priorityCollectionFactory = { RandomizedPriorityCollection(compareById()) { random.nextDouble() } },
+    weighter = { 1.0 / max(distance.weight(it).toDouble(), 1.0) },
+)
+
 fun <Method, Statement, State : UState<*, Method, Statement, *, *, State>> createForkDepthPathSelector(
     random: Random? = null,
 ): UPathSelector<State> {

usvm-core/src/test/kotlin/org/usvm/ps/ClosestToUncoveredRandomPathSelectorTest.kt

@@ -0,0 +1,149 @@
+package org.usvm.ps
+
+import io.mockk.every
+import org.junit.jupiter.api.Test
+import org.usvm.PathNode
+import org.usvm.PathSelectionStrategy
+import org.usvm.TestInstruction
+import org.usvm.TestState
+import org.usvm.UMachineOptions
+import org.usvm.appGraph
+import org.usvm.mockState
+import org.usvm.statistics.CoverageStatistics
+import org.usvm.statistics.distances.CallStackDistanceCalculator
+import org.usvm.statistics.distances.CfgStatistics
+import org.usvm.statistics.distances.CfgStatisticsImpl
+import kotlin.test.assertEquals
+import kotlin.test.assertSame
+import kotlin.test.assertTrue
+
+class ClosestToUncoveredRandomPathSelectorTest {
+    private val graph = appGraph {
+        method(name = "method", instructionsCount = 7) {
+            entryPoint(offset = 0)
+            edge(from = 0, to = 1)
+            edge(from = 1, to = 2)
+            edge(from = 0, to = 3)
+            edge(from = 3, to = 4)
+            edge(from = 4, to = 5)
+            edge(from = 5, to = 6)
+            exitPoint(offset = 2)
+            exitPoint(offset = 6)
+        }
+    }
+
+    @Test
+    fun `coverage and peek never recalculate queued weights while update touches only its state`() {
+        val cfg = CfgStatisticsImpl(graph)
+        val evaluated = mutableListOf<TestInstruction>()
+        val countedCfg = object : CfgStatistics<String, TestInstruction> by cfg {
+            override fun getShortestDistanceToExit(method: String, stmtFrom: TestInstruction): UInt {
+                evaluated.add(stmtFrom)
+                return cfg.getShortestDistanceToExit(method, stmtFrom)
+            }
+        }
+        val leftGoal = TestInstruction(method = "method", offset = 1)
+        val rightGoal = TestInstruction(method = "method", offset = 6)
+        val calculator = CallStackDistanceCalculator(
+            targets = listOf(leftGoal, rightGoal),
+            cfgStatistics = countedCfg,
+            applicationGraph = graph,
+        )
+        val nativeCoverage = CoverageStatistics<String, TestInstruction, TestState>(
+            methods = setOf("method"),
+            applicationGraph = graph,
+        )
+        val left = mockState(id = 1u, startMethod = "method", startInstruction = 1)
+        val right = mockState(id = 2u, startMethod = "method", startInstruction = 3)
+        val selector = createPathSelector(
+            initialState = left,
+            options = UMachineOptions(
+                pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
+                randomSeed = 0,
+            ),
+            applicationGraph = graph,
+            coverageStatisticsFactory = { nativeCoverage },
+            cfgStatisticsFactory = { countedCfg },
+            coverageDistanceCalculatorFactory = { calculator },
+        )
+        selector.add(states = listOf(right))
+        assertEquals(expected = listOf(left.currentStatement, right.currentStatement), actual = evaluated)
+        assertSame(expected = left, actual = selector.peek())
+        evaluated.clear()
+
+        assertTrue(calculator.removeTarget(method = "method", statement = leftGoal))
+        repeat(256) { selector.peek() }
+
+        assertTrue(evaluated.isEmpty())
+        assertEquals(expected = 0, actual = nativeCoverage.getTotalCoveredStatements())
+
+        selector.update(state = left)
+
+        assertEquals(expected = listOf(left.currentStatement), actual = evaluated)
+        assertSame(expected = right, actual = selector.peek())
+        evaluated.clear()
+
+        val fork = mockState(id = 3u, startMethod = "method", startInstruction = 2)
+        selector.add(states = listOf(fork))
+
+        assertEquals(expected = listOf(fork.currentStatement), actual = evaluated)
+        assertSame(expected = right, actual = selector.peek())
+        assertEquals(expected = setOf(left, right, fork), actual = selector.drain().toHashSet())
+    }
+
+    @Test
+    fun `native coverage still removes targets from the supplied calculator`() {
+        val cfg = CfgStatisticsImpl(graph)
+        val goal = TestInstruction(method = "method", offset = 1)
+        val calculator = CallStackDistanceCalculator(
+            targets = listOf(goal),
+            cfgStatistics = cfg,
+            applicationGraph = graph,
+        )
+        val state = mockState(id = 1u, startMethod = "method", startInstruction = 1)
+        every { state.pathNode } returns PathNode.root<TestInstruction>() + goal
+        val coverage = CoverageStatistics<String, TestInstruction, TestState>(
+            methods = setOf("method"),
+            applicationGraph = graph,
+        )
+        val selector = createPathSelector(
+            initialState = state,
+            options = UMachineOptions(
+                pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
+            ),
+            applicationGraph = graph,
+            coverageStatisticsFactory = { coverage },
+            cfgStatisticsFactory = { cfg },
+            coverageDistanceCalculatorFactory = { calculator },
+        )
+
+        coverage.onStateTerminated(state = state, stateReachable = true)
+        selector.update(state = state)
+
+        assertEquals(expected = 1, actual = coverage.getTotalCoveredStatements())
+        assertEquals(
+            expected = UInt.MAX_VALUE,
+            actual = calculator.calculateDistance(state.currentStatement, state.callStack),
+        )
+        assertSame(expected = state, actual = selector.peek())
+        assertEquals(expected = listOf(state), actual = selector.drain().toList())
+    }
+
+    @Test
+    fun `covered prefixes can still lead to uncovered successors`() {
+        val goal = TestInstruction(method = "method", offset = 6)
+        val prefix = mockState(id = 1u, startMethod = "method", startInstruction = 3)
+        val calculator = CallStackDistanceCalculator(
+            targets = listOf(prefix.currentStatement, goal),
+            cfgStatistics = CfgStatisticsImpl(graph),
+            applicationGraph = graph,
+        )
+
+        calculator.removeTarget(method = "method", statement = prefix.currentStatement)
+
+        assertEquals(
+            expected = 3u,
+            actual = calculator.calculateDistance(prefix.currentStatement, prefix.callStack),
+        )
+    }
+}

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

@@ -572,6 +572,7 @@ private fun runRawClassAnalysis(args: List<String>, exploratory: Boolean) {
         TsMachine(
             scene = scene,
             options = UMachineOptions(
+                pathSelectionStrategies = listOf(CALLS_PATH_SELECTION_STRATEGY),
                 stateCollectionStrategy = StateCollectionStrategy.ALL,
                 randomSeed = manifest.seed,
                 collectedStatesLimit = manifest.collectedStatesLimit,

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt

@@ -3,6 +3,7 @@ package org.usvm.ts.pbt.dsl
 import kotlinx.serialization.json.Json
 import org.jacodb.ets.utils.EtsIrProvider
 import org.jacodb.ets.utils.loadEtsProjectAutoConvert
+import org.usvm.PathSelectionStrategy
 import org.usvm.SolverType
 import org.usvm.UMachineOptions
 import org.usvm.ts.pbt.backend.ProjectionCapability
@@ -149,6 +150,7 @@ class DslPropertyRunner(sourceRoots: List<Path>) {
         val manifest = compiled.definition.toManifest()
         val mapping = PropertyEtsMapper(scene = scene, sourceRoots = sourceRoots).map(manifest)
         val options = UMachineOptions(
+            pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
             solverType = SolverType.YICES,
             timeout = configuration.timeoutMillis.milliseconds,
         )

usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt

@@ -3,6 +3,7 @@ package org.usvm.ts.pbt.usvm
 import io.ksmt.utils.asExpr
 import org.jacodb.ets.model.EtsScene
 import org.jacodb.ets.model.EtsType
+import org.usvm.PathSelectionStrategy
 import org.usvm.SolverType
 import org.usvm.StateCollectionStrategy
 import org.usvm.UMachineOptions
@@ -31,7 +32,10 @@ import org.usvm.ts.pbt.model.PropertyId
 /** Searches mapped TypeScript predicates for concrete property violations with USVM. */
 class UsvmPropertySearcher(
     private val scene: EtsScene,
-    machineOptions: UMachineOptions = UMachineOptions(solverType = SolverType.YICES),
+    machineOptions: UMachineOptions = UMachineOptions(
+        solverType = SolverType.YICES,
+        pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM),
+    ),
     private val tsOptions: TsOptions = TsOptions(),
     projectionOptions: UsvmProjectionOptions = UsvmProjectionOptions(),
 ) {