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 9a3d0b4c94..60173bd83b 100644 --- a/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt +++ b/usvm-core/src/main/kotlin/org/usvm/ps/PathSelectorFactory.kt @@ -36,6 +36,7 @@ private fun createPathSelector( cfgStatisticsFactory: () -> CfgStatistics? = { null }, callGraphStatisticsFactory: () -> CallGraphStatistics? = { null }, loopStatisticFactory: () -> StateLoopTracker<*, Statement, State>? = { null }, + coverageDistanceCalculatorFactory: () -> CallStackDistanceCalculator? = { null }, ): UPathSelector where Target : UTarget, State : UState<*, Method, Statement, *, Target, State> { @@ -69,14 +70,16 @@ private fun 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( @@ -153,6 +156,7 @@ fun createPathSelector( cfgStatisticsFactory: () -> CfgStatistics? = { null }, callGraphStatisticsFactory: () -> CallGraphStatistics? = { null }, loopStatisticFactory: () -> StateLoopTracker<*, Statement, State>? = { null }, + coverageDistanceCalculatorFactory: () -> CallStackDistanceCalculator? = { null }, ): UPathSelector where Target : UTarget, State : UState<*, Method, Statement, *, Target, State> = createPathSelector( listOf(initialState), @@ -161,7 +165,8 @@ fun createPathSelector( coverageStatisticsFactory, cfgStatisticsFactory, callGraphStatisticsFactory, - loopStatisticFactory + loopStatisticFactory, + coverageDistanceCalculatorFactory, ) fun createPathSelector( @@ -173,6 +178,7 @@ fun createPathSelector( cfgStatisticsFactory: () -> CfgStatistics? = { null }, callGraphStatisticsFactory: () -> CallGraphStatistics? = { null }, loopStatisticFactory: () -> StateLoopTracker<*, Statement, State>? = { null }, + coverageDistanceCalculatorFactory: () -> CallStackDistanceCalculator? = { null }, ): UPathSelector where Target : UTarget, State : UState<*, Method, Statement, *, Target, State> { val hasSingleEntryPoint = initialStates.size == 1 val hasUnlimitedScheduling = options.timeout == Duration.INFINITE && @@ -185,7 +191,8 @@ fun createPathSelector( coverageStatisticsFactory, cfgStatisticsFactory, callGraphStatisticsFactory, - loopStatisticFactory + loopStatisticFactory, + coverageDistanceCalculatorFactory, ) } @@ -202,7 +209,8 @@ fun createPathSelector( coverageStatisticsFactory, cfgStatisticsFactory, callGraphStatisticsFactory, - loopStatisticFactory + loopStatisticFactory, + coverageDistanceCalculatorFactory, ) val coverageStatistics = coverageStatisticsFactory() @@ -317,15 +325,16 @@ private fun , applicationGraph: ApplicationGraph, random: Random? = null, + distanceCalculator: CallStackDistanceCalculator? = null, ): UPathSelector { - 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 > createClosestToUncoveredRandomPathSelector( + distance: StateWeighter, + random: Random, +): UPathSelector = WeightedPathSelector( + priorityCollectionFactory = { RandomizedPriorityCollection(compareById()) { random.nextDouble() } }, + weighter = { 1.0 / max(distance.weight(it).toDouble(), 1.0) }, +) + fun > createForkDepthPathSelector( random: Random? = null, ): UPathSelector { diff --git a/usvm-core/src/test/kotlin/org/usvm/ps/ClosestToUncoveredRandomPathSelectorTest.kt b/usvm-core/src/test/kotlin/org/usvm/ps/ClosestToUncoveredRandomPathSelectorTest.kt new file mode 100644 index 0000000000..a7365dde31 --- /dev/null +++ b/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() + val countedCfg = object : CfgStatistics 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( + 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() + goal + val coverage = CoverageStatistics( + 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), + ) + } +} 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 7c03bb6e5c..d244d948c9 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 @@ -572,6 +572,7 @@ private fun runRawClassAnalysis(args: List, exploratory: Boolean) { TsMachine( scene = scene, options = UMachineOptions( + pathSelectionStrategies = listOf(CALLS_PATH_SELECTION_STRATEGY), stateCollectionStrategy = StateCollectionStrategy.ALL, randomSeed = manifest.seed, collectedStatesLimit = manifest.collectedStatesLimit, diff --git a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt b/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt index 9b32e22127..b0974e53b2 100644 --- a/usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/dsl/TsPropertyTest.kt +++ b/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) { 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, ) diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt index 10bf82289f..8e2cadda37 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/usvm/UsvmPropertySearcher.kt +++ b/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(), ) { 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 bdbbfa40fd..afbeb7e848 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -5,6 +5,7 @@ import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStmt import org.usvm.CoverageZone +import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.StateCollectionStrategy import org.usvm.UMachine @@ -37,6 +38,7 @@ import org.usvm.statistics.collectors.CoveredNewStatesCollector import org.usvm.statistics.collectors.StatesCollector import org.usvm.statistics.collectors.TargetsReachedStatesCollector import org.usvm.statistics.constraints.SoftConstraintsObserver +import org.usvm.statistics.distances.CallStackDistanceCalculator import org.usvm.statistics.distances.CfgStatisticsImpl import org.usvm.statistics.distances.PlainCallGraphStatistics import org.usvm.stopstrategies.StopStrategy @@ -78,9 +80,13 @@ data class TsMachineAnalysisResult( val runtimeLimited: Boolean get() = unsupportedPaths.isNotEmpty() } +/** Symbolically executes TypeScript entry points with shared coverage guidance. */ class TsMachine( scene: EtsScene, - override val options: UMachineOptions = UMachineOptions(solverType = SolverType.YICES), + override val options: UMachineOptions = UMachineOptions( + solverType = SolverType.YICES, + pathSelectionStrategies = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM), + ), private val tsOptions: TsOptions, private val machineObserver: UMachineObserver? = null, private val observer: TsInterpreterObserver? = null, @@ -149,6 +155,24 @@ class TsMachine( throwExceptionOnStepFailure = options.throwExceptionOnStepFailure, ) private val cfgStatistics = CfgStatisticsImpl(graph) + private val externallyCoveredStatements = hashSetOf() + private var coverageDistanceCalculator: CallStackDistanceCalculator? = null + + /** + * Reports caller-confirmed coverage on the analysis thread, including before analysis starts. + * This removes distance goals without changing native coverage counters or refreshing queued weights. + * Reports are retained across analyses on this machine. + */ + fun markCovered(statements: Collection): Boolean { + var changed = false + for (statement in statements) { + if (externallyCoveredStatements.add(statement)) { + coverageDistanceCalculator?.removeTarget(graph.methodOf(statement), statement) + changed = true + } + } + return changed + } /** Returns supported states only. Call [analyzeWithOutcome] to inspect excluded unsupported paths. */ fun analyze( @@ -192,6 +216,7 @@ class TsMachine( targets: List = emptyList(), configureInitialState: (EtsMethod, TsState) -> Unit = { _, _ -> }, ): TsMachineAnalysisResult { + coverageDistanceCalculator = null interpreter.resetStepFailure() failureTrackingUnknownCallObserver.reset() @@ -213,11 +238,7 @@ class TsMachine( applicationGraph = graph, ) - val callGraphStatistics: PlainCallGraphStatistics = - when (options.targetSearchDepth) { - 0u -> PlainCallGraphStatistics() - else -> TODO("Unsupported yet") - } + val callGraphStatistics = createCallGraphStatistics() val timeStatistics = createTimeStatistics() @@ -229,6 +250,7 @@ class TsMachine( coverageStatisticsFactory = { coverageStatistics }, cfgStatisticsFactory = { cfgStatistics }, callGraphStatisticsFactory = { callGraphStatistics }, + coverageDistanceCalculatorFactory = { getCoverageDistanceCalculator(coverageStatistics) }, ) val statesCollector = createStatesCollector(coverageStatistics) @@ -325,6 +347,19 @@ class TsMachine( ) } + private fun createCallGraphStatistics(): PlainCallGraphStatistics = when (options.targetSearchDepth) { + 0u -> PlainCallGraphStatistics() + else -> TODO("Unsupported yet") + } + + private fun getCoverageDistanceCalculator( + coverageStatistics: CoverageStatistics, + ): CallStackDistanceCalculator = coverageDistanceCalculator ?: CallStackDistanceCalculator( + targets = coverageStatistics.getUncoveredStatements().filterNot { it in externallyCoveredStatements }, + cfgStatistics = cfgStatistics, + applicationGraph = graph, + ).also { coverageDistanceCalculator = it } + private fun createStatesCollector( coverageStatistics: CoverageStatistics, ): StatesCollector = when (options.stateCollectionStrategy) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineExternalCoverageTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineExternalCoverageTest.kt new file mode 100644 index 0000000000..d2ce585a46 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsMachineExternalCoverageTest.kt @@ -0,0 +1,103 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.CoverageZone +import org.usvm.PathSelectionStrategy +import org.usvm.StateCollectionStrategy +import org.usvm.machine.state.TsState +import org.usvm.statistics.UMachineObserver +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.getResourcePath +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue +import kotlin.time.Duration + +/** External coverage affects scheduling only, independently of native collection and stopping. */ +class TsMachineExternalCoverageTest : TsMethodTestRunner() { + override val scene = EtsScene( + projectFiles = listOf( + loadEtsFileAutoConvert( + getResourcePath("/samples/coverage/ClassCoverage.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + + @Test + fun `TypeScript defaults to NURS and respects an explicit strategy`() { + TsMachine(scene = scene, tsOptions = TsOptions()).use { machine -> + assertEquals( + expected = listOf(PathSelectionStrategy.CLOSEST_TO_UNCOVERED_RANDOM), + actual = machine.options.pathSelectionStrategies, + ) + } + val explicitOptions = options.copy(pathSelectionStrategies = listOf(PathSelectionStrategy.BFS)) + + TsMachine(scene = scene, options = explicitOptions, tsOptions = TsOptions()).use { machine -> + assertEquals(expected = listOf(PathSelectionStrategy.BFS), actual = machine.options.pathSelectionStrategies) + } + } + + @Test + fun `external saturation before analysis neither stops execution nor suppresses native witnesses`() { + val method = getMethod(methodName = "entry", className = "HelperCoverage") + val statements = scene.projectClasses.flatMap { owner -> owner.methods.flatMap { it.cfg.stmts } } + val analysisOptions = options.copy( + coverageZone = CoverageZone.CLASS, + stateCollectionStrategy = StateCollectionStrategy.COVERED_NEW, + stopOnCoverage = 100, + timeout = Duration.INFINITE, + ) + + TsMachine(scene = scene, options = analysisOptions, tsOptions = TsOptions()).use { machine -> + assertTrue(machine.markCovered(statements)) + assertFalse(machine.markCovered(statements)) + + repeat(2) { + val result = machine.analyzeWithMetadata(methods = listOf(method)) + + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = result.stopReason) + assertEquals(expected = 2, actual = result.states.size) + assertFalse(result.engineFailed) + } + } + } + + @Test + fun `external coverage can arrive on the analysis thread while paths are queued`() { + val method = getMethod(methodName = "entry", className = "HelperCoverage") + val statements = scene.projectClasses.flatMap { owner -> owner.methods.flatMap { it.cfg.stmts } } + lateinit var machine: TsMachine + var reported = false + val observer = object : UMachineObserver { + override fun onStatePeeked(state: TsState) { + if (!reported) { + reported = machine.markCovered(statements) + } + } + } + val analysisOptions = options.copy( + coverageZone = CoverageZone.CLASS, + stateCollectionStrategy = StateCollectionStrategy.COVERED_NEW, + stopOnCoverage = 0, + timeout = Duration.INFINITE, + ) + machine = TsMachine( + scene = scene, + options = analysisOptions, + tsOptions = TsOptions(), + machineObserver = observer, + ) + + val result = machine.use { it.analyzeWithMetadata(methods = listOf(method)) } + + assertTrue(reported) + assertEquals(expected = TsAnalysisStopReason.EXHAUSTED, actual = result.stopReason) + assertEquals(expected = 2, actual = result.states.size) + assertFalse(result.engineFailed) + } +} diff --git a/usvm-util/src/main/kotlin/org/usvm/algorithms/DeterministicPriorityCollection.kt b/usvm-util/src/main/kotlin/org/usvm/algorithms/DeterministicPriorityCollection.kt index af9eb77830..a2b866e182 100644 --- a/usvm-util/src/main/kotlin/org/usvm/algorithms/DeterministicPriorityCollection.kt +++ b/usvm-util/src/main/kotlin/org/usvm/algorithms/DeterministicPriorityCollection.kt @@ -17,10 +17,12 @@ class DeterministicPriorityCollection(private val comparator: Compa override val count: Int get() = priorityQueue.size + if (topElement == null) 0 else 1 override fun peek(): T { - if (topElement == null) { - topElement = priorityQueue.remove() - } - return topElement!!.first + val currentTop = topElement + if (currentTop != null) return currentTop.first + + val next = priorityQueue.remove() + topElement = next + return next.first } override fun update(element: T, priority: Priority) { @@ -44,7 +46,7 @@ class DeterministicPriorityCollection(private val comparator: Compa assert({ !priorityQueue.any { (e, _) -> e == element } }) { "Element already exists in priority queue" } val currentTop = topElement - if (currentTop != null && comparator.compare(currentTop.second, priority) < 0) { + if (currentTop != null && comparator.compare(currentTop.second, priority) > 0) { topElement = element to priority priorityQueue.add(currentTop) return diff --git a/usvm-util/src/test/kotlin/org/usvm/algorithms/DeterministicPriorityCollectionTest.kt b/usvm-util/src/test/kotlin/org/usvm/algorithms/DeterministicPriorityCollectionTest.kt new file mode 100644 index 0000000000..c5d182a099 --- /dev/null +++ b/usvm-util/src/test/kotlin/org/usvm/algorithms/DeterministicPriorityCollectionTest.kt @@ -0,0 +1,62 @@ +package org.usvm.algorithms + +import org.junit.jupiter.api.Test +import kotlin.test.assertEquals + +internal class DeterministicPriorityCollectionTest { + @Test + fun `adding a worse priority keeps the cached minimum`() { + val collection = DeterministicPriorityCollection(naturalOrder()) + collection.add(element = "first", priority = 1) + assertEquals("first", collection.peek()) + + collection.add(element = "second", priority = 2) + + assertEquals("first", collection.peek()) + collection.remove("first") + assertEquals("second", collection.peek()) + assertEquals(1, collection.count) + } + + @Test + fun `adding a better priority replaces the cached minimum`() { + val collection = DeterministicPriorityCollection(naturalOrder()) + collection.add(element = "second", priority = 2) + assertEquals("second", collection.peek()) + + collection.add(element = "first", priority = 1) + + assertEquals("first", collection.peek()) + collection.remove("first") + assertEquals("second", collection.peek()) + assertEquals(1, collection.count) + } + + @Test + fun `adding a worse priority keeps the cached maximum with reverse order`() { + val collection = DeterministicPriorityCollection(reverseOrder()) + collection.add(element = "first", priority = 2) + assertEquals("first", collection.peek()) + + collection.add(element = "second", priority = 1) + + assertEquals("first", collection.peek()) + collection.remove("first") + assertEquals("second", collection.peek()) + assertEquals(1, collection.count) + } + + @Test + fun `adding a better priority replaces the cached maximum with reverse order`() { + val collection = DeterministicPriorityCollection(reverseOrder()) + collection.add(element = "second", priority = 1) + assertEquals("second", collection.peek()) + + collection.add(element = "first", priority = 2) + + assertEquals("first", collection.peek()) + collection.remove("first") + assertEquals("second", collection.peek()) + assertEquals(1, collection.count) + } +}