From 8f3d5250cd348eae26968210bfa4ebb585597931 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 02:26:59 +0300 Subject: [PATCH 1/2] Keep independent TypeScript entries after unsupported or infeasible inputs --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 26 +++- .../machine/types/TsInitialStateInputGuard.kt | 34 +++++ .../usvm/machine/TsEntryStartupInputsTest.kt | 141 ++++++++++++++++++ .../resources/models/EntryStartupInputs.ts | 25 ++++ 4 files changed, 221 insertions(+), 5 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/types/TsInitialStateInputGuard.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsEntryStartupInputsTest.kt create mode 100644 usvm-ts/src/test/resources/models/EntryStartupInputs.ts 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 aed3433d69..479623269a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -23,6 +23,7 @@ import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState import org.usvm.machine.types.TsConstructorInputGuard +import org.usvm.machine.types.TsInitialStateInputGuard import org.usvm.machine.types.TsTypeSystem import org.usvm.ps.createPathSelector import org.usvm.statistics.CompositeUMachineObserver @@ -59,6 +60,7 @@ data class TsAnalysisResult( val stopReason: TsAnalysisStopReason, /** Reasons for satisfiable paths excluded by an explicit engine model bound. */ val unsupportedPaths: List, + val infeasibleEntryPoints: List = emptyList(), ) /** Terminal states and failure metadata for one TypeScript analysis. */ @@ -69,6 +71,8 @@ data class TsMachineAnalysisResult( val unsupportedCall: Boolean, val engineFailed: Boolean, val unsupportedPaths: List, + /** Entry signatures whose initial constraints were UNSAT, distinct from unsupported inputs. */ + val infeasibleEntryPoints: List = emptyList(), ) { /** Includes execution bounds and unsupported entry inputs retained in [unsupportedPaths]. */ val runtimeLimited: Boolean get() = unsupportedPaths.isNotEmpty() @@ -165,6 +169,7 @@ class TsMachine( states = result.states, stopReason = result.stopReason, unsupportedPaths = result.unsupportedPaths, + infeasibleEntryPoints = result.infeasibleEntryPoints, ) } @@ -184,10 +189,11 @@ class TsMachine( interpreter.resetStepFailure() failureTrackingUnknownCallObserver.reset() - val (initialStates, unsupportedPaths) = createInitialStates(methods, targets, configureInitialState) + val (initialStates, unsupportedPaths, infeasibleEntryPoints) = + createInitialStates(methods, targets, configureInitialState) if (initialStates.isEmpty()) { - return emptyAnalysisResult(unsupportedPaths) + return emptyAnalysisResult(unsupportedPaths, infeasibleEntryPoints) } val methodsToTrackCoverage = @@ -312,6 +318,7 @@ class TsMachine( unsupportedCall = failureTrackingUnknownCallObserver.pathStopped, engineFailed = interpreter.stepFailed, unsupportedPaths = unsupportedPaths.toList(), + infeasibleEntryPoints = infeasibleEntryPoints, ) } @@ -353,26 +360,33 @@ class TsMachine( return if (targets == null) coveredMethods + entryMethods else coveredMethods } - private fun emptyAnalysisResult(unsupportedPaths: Set) = TsMachineAnalysisResult( + private fun emptyAnalysisResult( + unsupportedPaths: Set, + infeasibleEntryPoints: List, + ) = TsMachineAnalysisResult( states = emptyList(), stopReason = TsAnalysisStopReason.EXHAUSTED, timedOut = false, unsupportedCall = false, engineFailed = false, unsupportedPaths = unsupportedPaths.toList(), + infeasibleEntryPoints = infeasibleEntryPoints, ) private fun createInitialStates( methods: List, targets: List, configureInitialState: (EtsMethod, TsState) -> Unit, - ): Pair, MutableSet> { + ): Triple, MutableSet, List> { val initialStates = mutableMapOf() val unsupportedPaths = mutableSetOf() + val infeasibleEntryPoints = mutableListOf() val constructorInputs = TsConstructorInputGuard() + val initialStateInputs = TsInitialStateInputGuard() methods.forEach { method -> val unsupportedReason = constructorInputs.unsupportedReason(method) + ?: initialStateInputs.unsupportedReason(method) if (unsupportedReason != null) { unsupportedPaths += unsupportedReason } else { @@ -381,11 +395,13 @@ class TsMachine( } if (initialState != null) { initialStates[method] = initialState + } else { + infeasibleEntryPoints += method.humanReadableSignature } } } - return initialStates to unsupportedPaths + return Triple(initialStates, unsupportedPaths, infeasibleEntryPoints) } override fun close() { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsInitialStateInputGuard.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsInitialStateInputGuard.kt new file mode 100644 index 0000000000..ae54f53434 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsInitialStateInputGuard.kt @@ -0,0 +1,34 @@ +package org.usvm.machine.types + +import org.jacodb.ets.model.EtsAliasType +import org.jacodb.ets.model.EtsBigIntType +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsGenericType +import org.jacodb.ets.model.EtsIntersectionType +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsType +import org.usvm.util.humanReadableSignature + +/** Bounds only input types whose initial-state construction has no implemented domain. */ +internal class TsInitialStateInputGuard { + fun unsupportedReason(method: EtsMethod): String? { + val genericParameters = method.typeParameters.filterIsInstance().associateBy { it.typeName } + for (parameter in method.parameters) { + val inputType = parameter.type.initialInputType(genericParameters) + val domain = inputType.unsupportedInitialDomain() ?: continue + + return "$domain input parameter '${parameter.name}' in ${method.humanReadableSignature} is not modeled" + } + + return null + } +} + +private fun EtsType.unsupportedInitialDomain(): String? = when (this) { + is EtsFunctionType -> "Callable" + EtsBigIntType -> "BigInt" + is EtsAliasType -> originalType.unsupportedInitialDomain() + // Intersections use each member's sort; unions use the existing unresolved input domain instead. + is EtsIntersectionType -> types.firstNotNullOfOrNull { it.unsupportedInitialDomain() } + else -> null +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsEntryStartupInputsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsEntryStartupInputsTest.kt new file mode 100644 index 0000000000..a31cfd4856 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsEntryStartupInputsTest.kt @@ -0,0 +1,141 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.eq +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFailsWith +import kotlin.test.assertFalse +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class TsEntryStartupInputsTest : TsMethodTestRunner() { + override val scene = EtsScene( + projectFiles = listOf( + loadEtsFileAutoConvert( + path = getResourcePath("/models/EntryStartupInputs.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + private val machineOptions = UMachineOptions( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = 5.seconds, + solverType = SolverType.YICES, + throwExceptionOnStepFailure = true, + ) + + @Test + fun `unsupported entry inputs do not discard supported methods of the same class`() { + val supported = getMethod(methodName = "supported", className = "EntryStartupInputs") + val methods = unsupportedMethods() + supported + val configured = mutableListOf() + + val result = TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + machine.analyzeWithMetadata(methods = methods) { method, _ -> configured += method.name } + } + + assertFalse(result.engineFailed) + assertEquals(listOf("supported"), configured) + assertTrue(result.states.isNotEmpty()) + assertTrue(result.states.all { it.entrypoint == supported }) + assertEquals(3, result.unsupportedPaths.size) + assertTrue(result.unsupportedPaths.any { "Callable input parameter 'reader'" in it }) + assertTrue(result.unsupportedPaths.any { "withBigInt" in it && "BigInt input parameter 'value'" in it }) + assertTrue(result.unsupportedPaths.any { "withGenericBigInt" in it && "BigInt input parameter 'value'" in it }) + + discoverProperties( + method = supported, + { _, value -> value eq 1 }, + { _, value -> value eq 2 }, + invariants = arrayOf({ _, value -> (value eq 1) || (value eq 2) }), + ) + } + + @Test + fun `an entirely unsupported entry set returns explicit per-method reasons`() { + val methods = unsupportedMethods() + + val result = TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + machine.analyzeWithMetadata(methods = methods) + } + + assertFalse(result.engineFailed) + assertTrue(result.states.isEmpty()) + assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason) + assertEquals(3, result.unsupportedPaths.size) + for (method in methods) { + assertTrue(result.unsupportedPaths.any { method.name in it }) + } + } + + @Test + fun `unexpected initial-state configuration errors remain failures`() { + val method = getMethod(methodName = "supported", className = "EntryStartupInputs") + + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + val exception = assertFailsWith { + machine.analyzeWithMetadata(methods = listOf(method)) { _, _ -> + error("Unexpected configuration defect") + } + } + + assertEquals("Unexpected configuration defect", exception.message) + } + } + + @Test + fun `an infeasible entry is distinct from unsupported inputs and does not discard another entry`() { + val infeasible = getMethod(methodName = "supported", className = "EntryStartupInputs") + val independent = getMethod(methodName = "independent", className = "EntryStartupInputs") + val methods = unsupportedMethods() + infeasible + independent + + val result = TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + machine.analyzeWithMetadata(methods = methods) { method, state -> + // Deliberately test the initial solver's UNSAT contract, independently of source feasibility. + if (method == infeasible) { + state.pathConstraints += state.ctx.falseExpr + } + } + } + + assertFalse(result.engineFailed) + assertTrue(result.states.isNotEmpty()) + assertTrue(result.states.all { it.entrypoint == independent }) + assertEquals(3, result.unsupportedPaths.size) + assertEquals(1, result.infeasibleEntryPoints.size) + assertTrue("supported" in result.infeasibleEntryPoints.single()) + } + + @Test + fun `an entirely infeasible entry set is exhausted without an unsupported or engine failure`() { + val method = getMethod(methodName = "supported", className = "EntryStartupInputs") + + val result = TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + machine.analyzeWithMetadata(methods = listOf(method)) { _, state -> + state.pathConstraints += state.ctx.falseExpr + } + } + + assertFalse(result.engineFailed) + assertFalse(result.runtimeLimited) + assertTrue(result.states.isEmpty()) + assertTrue(result.unsupportedPaths.isEmpty()) + assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason) + assertEquals(1, result.infeasibleEntryPoints.size) + assertTrue("supported" in result.infeasibleEntryPoints.single()) + } + + private fun unsupportedMethods() = listOf("withCallback", "withBigInt", "withGenericBigInt").map { name -> + getMethod(methodName = name, className = "EntryStartupInputs") + } +} diff --git a/usvm-ts/src/test/resources/models/EntryStartupInputs.ts b/usvm-ts/src/test/resources/models/EntryStartupInputs.ts new file mode 100644 index 0000000000..ca6885d593 --- /dev/null +++ b/usvm-ts/src/test/resources/models/EntryStartupInputs.ts @@ -0,0 +1,25 @@ +type Reader = (value: number) => number; +type Big = bigint; + +export class EntryStartupInputs { + independent(): number { + return 17; + } + + supported(value: number): number { + if (value > 10) return 1; + return 2; + } + + withCallback(reader: Reader): number { + return reader(2); + } + + withBigInt(value: Big): Big { + return value; + } + + withGenericBigInt(value: T): T { + return value; + } +} From 9570d1652c55b355fe26c6a5e81f56340870c2a5 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Thu, 15 Oct 2026 16:31:59 +0300 Subject: [PATCH 2/2] Introduce a named initial-state creation result Replace the positional Triple with InitialStatesResult and named constructor fields. Keep analyzeWithMetadata within the Detekt length limit without changing its stop-reason behavior. --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 21 ++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) 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 479623269a..80e389983f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -305,11 +305,8 @@ class TsMachine( stopStrategy = stopStrategy, ) - val stopReason = if (pathSelector.isEmpty()) { - TsAnalysisStopReason.EXHAUSTED - } else { - TsAnalysisStopReason.STOPPED - } + val exhausted = pathSelector.isEmpty() + val stopReason = if (exhausted) TsAnalysisStopReason.EXHAUSTED else TsAnalysisStopReason.STOPPED return TsMachineAnalysisResult( states = statesCollector.collectedStates, @@ -373,11 +370,17 @@ class TsMachine( infeasibleEntryPoints = infeasibleEntryPoints, ) + private data class InitialStatesResult( + val initialStates: Map, + val unsupportedPaths: MutableSet, + val infeasibleEntryPoints: List, + ) + private fun createInitialStates( methods: List, targets: List, configureInitialState: (EtsMethod, TsState) -> Unit, - ): Triple, MutableSet, List> { + ): InitialStatesResult { val initialStates = mutableMapOf() val unsupportedPaths = mutableSetOf() val infeasibleEntryPoints = mutableListOf() @@ -401,7 +404,11 @@ class TsMachine( } } - return Triple(initialStates, unsupportedPaths, infeasibleEntryPoints) + return InitialStatesResult( + initialStates = initialStates, + unsupportedPaths = unsupportedPaths, + infeasibleEntryPoints = infeasibleEntryPoints, + ) } override fun close() {