From 7aeb92347d10c266bbc24c89b13da9e2ff484028 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 03:08:18 +0300 Subject: [PATCH 01/17] [TS] Evaluate instanceof against runtime constructor values --- .../main/kotlin/org/usvm/machine/TsContext.kt | 13 ++ .../org/usvm/machine/expr/TsExprResolver.kt | 56 +++++- .../samples/types/RuntimeInstanceofTest.kt | 169 ++++++++++++++++++ .../samples/types/RuntimeInstanceof.ts | 52 ++++++ 4 files changed, 286 insertions(+), 4 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt create mode 100644 usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 9a939c7e06..a394c69d8f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -8,6 +8,7 @@ import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanLiteralType import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsEnumValueType import org.jacodb.ets.model.EtsGenericType import org.jacodb.ets.model.EtsLexicalEnvType @@ -91,6 +92,18 @@ class TsContext( // String constant caching at context level private val stringConstants: MutableMap = mutableMapOf() + private val classConstructorRefs: MutableMap = mutableMapOf() + private val constructorSignatures: MutableMap = mutableMapOf() + + fun classConstructorRef(signature: EtsClassSignature): UConcreteHeapRef = + classConstructorRefs.getOrPut(signature) { + allocateStaticRef().also { constructorSignatures[it] = signature } + } + + fun classConstructorSignature(ref: UConcreteHeapRef): EtsClassSignature? = constructorSignatures[ref] + + fun classConstructorRefs(): Collection = classConstructorRefs.values + /** * Reverse mapping from heap references to their original string constant values. * This is used during test resolution to retrieve the actual string content when diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index f0e08bd301..e5425f444f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -21,6 +21,7 @@ import org.jacodb.ets.model.EtsCaughtExceptionRef import org.jacodb.ets.model.EtsClassCategory import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsClassValueRef import org.jacodb.ets.model.EtsClosureFieldRef import org.jacodb.ets.model.EtsConstant import org.jacodb.ets.model.EtsDeleteExpr @@ -101,6 +102,7 @@ import org.usvm.api.allocateConcreteRef import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArrayLength import org.usvm.api.memcpy +import org.usvm.api.typeStreamOf import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type import org.usvm.isAllocatedConcreteHeapRef @@ -128,6 +130,7 @@ import org.usvm.machine.types.EtsNominalType import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.sizeSort import org.usvm.types.singleOrNull +import org.usvm.types.TypesResult import org.usvm.util.EtsHierarchy import org.usvm.util.SymbolResolutionResult import org.usvm.util.arrayStorageType @@ -234,6 +237,8 @@ class TsExprResolver( return simpleValueResolver.visit(value) } + override fun visit(value: EtsClassValueRef): UExpr = ctx.classConstructorRef(value.signature) + override fun visit(value: EtsParameterRef): UExpr? { return simpleValueResolver.visit(value) } @@ -476,6 +481,7 @@ class TsExprResolver( val functionValue = mkStringConstant("function", scope) val isKnownFunction = scope.calcOnState { ref is UConcreteHeapRef && ( + classConstructorSignature(ref) != null || associatedFunction[ref] != null || memory.types.getTypeStream(ref).singleOrNull() is EtsFunctionType ) @@ -1151,12 +1157,52 @@ class TsExprResolver( } override fun visit(expr: EtsInstanceOfExpr): UExpr? = with(ctx) { - val arg = resolve(expr.arg)?.asExpr(addressSort) ?: return null - val checkType = expr.checkType as? EtsRefType ?: return falseExpr + val arg = resolve(expr.arg) ?: return null + val checkValue = expr.checkValue - scope.calcOnState { - memory.types.evalIsSubtype(arg, EtsNominalType(checkType)) + val checkType = if (checkValue == null) { + // Legacy EtsIR contains only a static target. New frontend IR always evaluates the RHS. + expr.checkType as? EtsRefType + ?: return falseExpr + } else { + val constructor = resolve(checkValue) ?: return null + if (constructor.sort != addressSort || + constructor == mkTsNullValue() || + constructor == mkUndefinedValue() + ) { + throw UnsupportedOperationException( + "Non-callable instanceof RHS requires a TypeError object, which is not modeled" + ) + } + + val constructorRef = constructor as? UConcreteHeapRef + ?: throw UnsupportedOperationException("Symbolic instanceof constructor identity is not modeled") + val signature = classConstructorSignature(constructorRef) + ?: throw UnsupportedOperationException("Unknown instanceof constructor value: $constructorRef") + val clazz = scene.projectAndSdkClasses.singleOrNull { it.signature == signature } + ?: throw UnsupportedOperationException("Unknown instanceof class: $signature") + if (clazz.methods.any { it.name == "%computed" && it.modifiers.isStatic }) { + throw UnsupportedOperationException("Custom Symbol.hasInstance may override instanceof for $signature") + } + + EtsClassType(signature) } + + if (arg.sort != addressSort) return falseExpr + val objectRef = arg.asExpr(addressSort) + if (isAllocatedConcreteHeapRef(objectRef) && checkType is EtsClassType) { + val objectTypes = scope.calcOnState { memory.typeStreamOf(objectRef).take(2) } + val objectType = (objectTypes as? TypesResult.SuccessfulTypesResult)?.types?.singleOrNull() as? EtsClassType + if (objectType != null) { + val objectClass = hierarchy.classesForType(objectType).singleOrNull() + ?: throw UnsupportedOperationException("Unknown instanceof receiver class: $objectType") + val constructorClass = hierarchy.classesForType(checkType).singleOrNull() + ?: throw UnsupportedOperationException("Unknown instanceof constructor class: $checkType") + return mkBool(constructorClass in hierarchy.getAncestors(objectClass)) + } + } + + scope.calcOnState { memory.types.evalIsSubtype(objectRef, EtsNominalType(checkType)) } } // endregion @@ -1599,6 +1645,8 @@ class TsSimpleValueResolver( return resolveLocal(value) } + override fun visit(value: EtsClassValueRef): UExpr = ctx.classConstructorRef(value.signature) + override fun visit(value: EtsConstant): UExpr = with(ctx) { logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } error("Not supported $value") diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt new file mode 100644 index 0000000000..ad7359e7ff --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -0,0 +1,169 @@ +package org.usvm.samples.types + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import java.nio.file.Path +import java.util.concurrent.TimeUnit +import kotlin.io.path.readText +import kotlin.io.path.writeText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class RuntimeInstanceofTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val tsPath = "/samples/types/RuntimeInstanceof.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `dynamic constructor value selects both outcomes`() { + val method = getMethod(methodName = "dynamicConstructor", className = "RuntimeInstanceof") + val outcome = analyze("dynamicConstructor") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + val cases = outcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + val input = assertIs(test.before.parameters.single()).value + val actual = assertIs(test.returnValue).number + assertEquals(if (input) 1.0 else 0.0, actual) + input to actual + } + assertEquals(setOf(false, true), cases.map { it.first }.toSet()) + + replay(cases.map { (input, actual) -> + "if (new RuntimeInstanceof().dynamicConstructor($input) !== ${actual.toInt()}) throw Error('dynamic $input');" + }) + } + + @Test + fun `typeof recognizes constructor values stored in a local`() { + val method = getMethod(methodName = "aliasedClassTypeof", className = "RuntimeInstanceof") + val outcome = analyze("aliasedClassTypeof") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + val inputs = outcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + assertEquals(1.0, assertIs(test.returnValue).number) + assertIs(test.before.parameters.single()).value + } + assertEquals(setOf(false, true), inputs.toSet()) + + replay(inputs.map { input -> + "if (new RuntimeInstanceof().aliasedClassTypeof($input) !== 1) throw Error('typeof $input');" + }) + } + + @Test + fun `direct and inherited checks use declared class identity`() { + val expected = mapOf( + "directConstructor" to 1.0, + "unrelatedConstructor" to 0.0, + "classTypeof" to 1.0, + "primitiveLeft" to 0.0, + ) + + expected.forEach { (methodName, expectedResult) -> + val method = getMethod(methodName = methodName, className = "RuntimeInstanceof") + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty(), methodName) + outcome.states.forEach { state -> + assertIs(state.methodResult, methodName) + val test = TsTestResolver().resolve(method, state) + assertEquals(expectedResult, assertIs(test.returnValue).number, methodName) + } + } + + replay(expected.map { (methodName, expectedResult) -> + "if (new RuntimeInstanceof().$methodName() !== ${expectedResult.toInt()}) throw Error('$methodName');" + }) + } + + @Test + fun `subclass instance belongs to declared parent constructor`() { + val method = getMethod(methodName = "inheritedConstructor", className = "RuntimeInstanceof") + val outcome = analyze("inheritedConstructor") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + outcome.states.forEach { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + assertEquals(1.0, assertIs(test.returnValue).number) + } + + replay(listOf( + "if (new RuntimeInstanceof().inheritedConstructor(new InstanceChild()) !== 1) throw Error('parent');" + )) + } + + @Test + fun `non callable RHS and custom hasInstance are explicitly unsupported`() { + val nonCallable = analyze("nonCallableRight") + val custom = analyze("customHasInstance") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, nonCallable.stopReason) + assertTrue(nonCallable.states.isEmpty()) + assertTrue(nonCallable.unsupportedPaths.any { "TypeError" in it }, "${nonCallable.unsupportedPaths}") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, custom.stopReason) + assertTrue(custom.states.isEmpty()) + assertTrue(custom.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${custom.unsupportedPaths}") + + replay(listOf( + "let typeError = false; try { new RuntimeInstanceof().nonCallableRight(); } " + + "catch (error) { typeError = error instanceof TypeError; } " + + "if (!typeError) throw Error('TypeError');", + "if (new RuntimeInstanceof().customHasInstance() !== false) throw Error('custom hasInstance');", + )) + } + + private fun analyze(methodName: String) = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> + machine.analyzeWithOutcome(methods = listOf(getMethod(methodName = methodName, className = "RuntimeInstanceof"))) + } + + private fun replay(assertions: List) { + val script = directory.resolve("runtime-instanceof.ts") + val output = directory.resolve("runtime-instanceof.out") + script.writeText(buildString { + appendLine(getResourcePath(tsPath).readText()) + assertions.forEach(::appendLine) + }) + + val process = ProcessBuilder("node", "--experimental-strip-types", script.toString()) + .redirectErrorStream(true) + .redirectOutput(output.toFile()) + .start() + + assertTrue(process.waitFor(30, TimeUnit.SECONDS), "Node replay timed out") + assertEquals(0, process.exitValue(), output.readText()) + } + + private val machineOptions = UMachineOptions( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = 30.seconds, + ) +} diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts new file mode 100644 index 0000000000..aa7e33fd7d --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts @@ -0,0 +1,52 @@ +// @ts-nocheck + +class RuntimeInstanceof { + dynamicConstructor(useA: boolean): number { + const ctor = useA ? InstanceA : InstanceB; + return new InstanceA() instanceof ctor ? 1 : 0; + } + + directConstructor(): number { + return new InstanceA() instanceof InstanceA ? 1 : 0; + } + + inheritedConstructor(instance: InstanceChild): number { + return instance instanceof InstanceParent ? 1 : 0; + } + + unrelatedConstructor(): number { + return new InstanceA() instanceof InstanceB ? 1 : 0; + } + + classTypeof(): number { + return typeof InstanceA === "function" ? 1 : 0; + } + + aliasedClassTypeof(useA: boolean): number { + const ctor = useA ? InstanceA : InstanceB; + return typeof ctor === "function" ? 1 : 0; + } + + primitiveLeft(): number { + return 42 instanceof InstanceA ? 1 : 0; + } + + nonCallableRight(): boolean { + const ctor: any = 42; + return new InstanceA() instanceof ctor; + } + + customHasInstance(): boolean { + return new InstanceCustom() instanceof InstanceCustom; + } +} + +class InstanceA {} +class InstanceB {} +class InstanceParent {} +class InstanceChild extends InstanceParent { childMarker: number = 1; } +class InstanceCustom { + static [Symbol.hasInstance](_value: unknown): boolean { + return false; + } +} From 453c9849f96f338f0292368405efcb37bd46fa3b Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 03:39:03 +0300 Subject: [PATCH 02/17] [TS] Guard inherited hasInstance and constructor inputs --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 34 +++++++++++++--- .../org/usvm/machine/expr/TsExprResolver.kt | 13 +++++- .../samples/types/RuntimeInstanceofTest.kt | 40 ++++++++++++++++++- .../samples/types/RuntimeInstanceof.ts | 22 ++++++++++ 4 files changed, 101 insertions(+), 8 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 ca75767d69..f817f13d9f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -1,6 +1,7 @@ package org.usvm.machine import mu.KotlinLogging +import org.jacodb.ets.model.EtsClassValueType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStmt @@ -113,12 +114,15 @@ class TsMachine( methods: List, targets: List = emptyList(), ): TsAnalysisResult { - val initialStates = mutableMapOf() - methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) } + val (initialStates, unsupportedPaths) = createInitialStates(methods, targets) + + if (initialStates.isEmpty()) { + return TsAnalysisResult(emptyList(), TsAnalysisStopReason.EXHAUSTED, unsupportedPaths.toList()) + } val methodsToTrackCoverage = when (options.coverageZone) { - CoverageZone.METHOD, CoverageZone.TRANSITIVE -> methods.toHashSet() + CoverageZone.METHOD, CoverageZone.TRANSITIVE -> initialStates.keys.toHashSet() CoverageZone.CLASS -> TODO("Unsupported yet") } @@ -157,8 +161,6 @@ class TsMachine( val observers = mutableListOf>(coverageStatistics) observers.add(statesCollector) - val unsupportedPaths = mutableSetOf() - if (tsOptions.enableVisualization) { observers += TsStateVisualizer() } @@ -196,7 +198,7 @@ class TsMachine( if (logger.isInfoEnabled) { observers.add( StatisticsByMethodPrinter( - getMethods = { methods }, + getMethods = { initialStates.keys.toList() }, print = logger::info, getMethodSignature = { it.humanReadableSignature }, coverageStatistics = coverageStatistics, @@ -242,6 +244,26 @@ class TsMachine( ) } + private fun createInitialStates( + methods: List, + targets: List, + ): Pair, MutableSet> { + val initialStates = mutableMapOf() + val unsupportedPaths = mutableSetOf() + + methods.forEach { method -> + val constructorParameter = method.parameters.firstOrNull { it.type is EtsClassValueType } + if (constructorParameter != null) { + unsupportedPaths += "Constructor-typed parameter '${constructorParameter.name}' " + + "in ${method.humanReadableSignature} is not modeled" + } else { + initialStates[method] = interpreter.getInitialState(method, targets) + } + } + + return initialStates to unsupportedPaths + } + override fun close() { components.close() } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index e5425f444f..6226006dad 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -22,6 +22,7 @@ import org.jacodb.ets.model.EtsClassCategory import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsClassValueRef +import org.jacodb.ets.model.EtsClassValueType import org.jacodb.ets.model.EtsClosureFieldRef import org.jacodb.ets.model.EtsConstant import org.jacodb.ets.model.EtsDeleteExpr @@ -401,6 +402,14 @@ class TsExprResolver( override fun visit(expr: EtsCastExpr): UExpr<*>? = with(ctx) { val resolvedExpr = resolve(expr.arg) ?: return@with null + if (resolvedExpr is UConcreteHeapRef && + classConstructorSignature(resolvedExpr) != null && + expr.type is EtsClassValueType + ) { + // TypeScript assertions do not change the identity of a constructor at runtime. + return@with resolvedExpr + } + return when (resolvedExpr.sort) { fp64Sort -> { logger.error("Unsupported cast from fp ${expr.arg} to ${expr.type}") @@ -1181,7 +1190,9 @@ class TsExprResolver( ?: throw UnsupportedOperationException("Unknown instanceof constructor value: $constructorRef") val clazz = scene.projectAndSdkClasses.singleOrNull { it.signature == signature } ?: throw UnsupportedOperationException("Unknown instanceof class: $signature") - if (clazz.methods.any { it.name == "%computed" && it.modifiers.isStatic }) { + val hasComputedStaticMethod = hierarchy.getAncestors(clazz) + .any { ancestor -> ancestor.methods.any { it.name == "%computed" && it.modifiers.isStatic } } + if (hasComputedStaticMethod) { throw UnsupportedOperationException("Custom Symbol.hasInstance may override instanceof for $signature") } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt index ad7359e7ff..e1262edd68 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -76,6 +76,8 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { fun `direct and inherited checks use declared class identity`() { val expected = mapOf( "directConstructor" to 1.0, + "castConstructor" to 1.0, + "nonNullConstructor" to 1.0, "unrelatedConstructor" to 0.0, "classTypeof" to 1.0, "primitiveLeft" to 0.0, @@ -87,7 +89,7 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") - assertTrue(outcome.states.isNotEmpty(), methodName) + assertTrue(outcome.states.isNotEmpty(), "$methodName: ${outcome.unsupportedPaths}") outcome.states.forEach { state -> assertIs(state.methodResult, methodName) val test = TsTestResolver().resolve(method, state) @@ -123,6 +125,7 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { fun `non callable RHS and custom hasInstance are explicitly unsupported`() { val nonCallable = analyze("nonCallableRight") val custom = analyze("customHasInstance") + val inherited = analyze("inheritedHasInstance") assertEquals(TsAnalysisStopReason.EXHAUSTED, nonCallable.stopReason) assertTrue(nonCallable.states.isEmpty()) @@ -132,14 +135,49 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { assertTrue(custom.states.isEmpty()) assertTrue(custom.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${custom.unsupportedPaths}") + assertEquals(TsAnalysisStopReason.EXHAUSTED, inherited.stopReason) + assertTrue(inherited.states.isEmpty()) + assertTrue(inherited.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${inherited.unsupportedPaths}") + replay(listOf( "let typeError = false; try { new RuntimeInstanceof().nonCallableRight(); } " + "catch (error) { typeError = error instanceof TypeError; } " + "if (!typeError) throw Error('TypeError');", "if (new RuntimeInstanceof().customHasInstance() !== false) throw Error('custom hasInstance');", + "if (new RuntimeInstanceof().inheritedHasInstance(new InstanceHasInstanceChild()) !== false) " + + "throw Error('inherited hasInstance');", + )) + } + + @Test + fun `constructor typed input has an explicit unsupported outcome`() { + val outcome = analyze("constructorParameter") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + "${outcome.unsupportedPaths}") + + replay(listOf( + "if (new RuntimeInstanceof().constructorParameter(InstanceA) !== true) throw Error('A input');", + "if (new RuntimeInstanceof().constructorParameter(InstanceB) !== false) throw Error('B input');", )) } + @Test + fun `unsupported constructor input does not hide another entrypoint`() { + val methods = listOf("constructorParameter", "directConstructor") + .map { getMethod(methodName = it, className = "RuntimeInstanceof") } + val outcome = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> + machine.analyzeWithOutcome(methods = methods) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.any { "constructorParameter" in it }, "${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + outcome.states.forEach { state -> assertIs(state.methodResult) } + } + private fun analyze(methodName: String) = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> machine.analyzeWithOutcome(methods = listOf(getMethod(methodName = methodName, className = "RuntimeInstanceof"))) } diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts index aa7e33fd7d..96da11729c 100644 --- a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts +++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts @@ -10,6 +10,14 @@ class RuntimeInstanceof { return new InstanceA() instanceof InstanceA ? 1 : 0; } + castConstructor(): number { + return new InstanceA() instanceof (InstanceA as typeof InstanceA) ? 1 : 0; + } + + nonNullConstructor(): number { + return new InstanceA() instanceof InstanceA! ? 1 : 0; + } + inheritedConstructor(instance: InstanceChild): number { return instance instanceof InstanceParent ? 1 : 0; } @@ -39,6 +47,14 @@ class RuntimeInstanceof { customHasInstance(): boolean { return new InstanceCustom() instanceof InstanceCustom; } + + inheritedHasInstance(instance: InstanceHasInstanceChild): boolean { + return instance instanceof InstanceHasInstanceChild; + } + + constructorParameter(ctor: typeof InstanceA): boolean { + return new InstanceA() instanceof ctor; + } } class InstanceA {} @@ -50,3 +66,9 @@ class InstanceCustom { return false; } } +class InstanceHasInstanceParent { + static [Symbol.hasInstance](_value: unknown): boolean { + return false; + } +} +class InstanceHasInstanceChild extends InstanceHasInstanceParent { hasInstanceChildMarker: number = 1; } From fdb7e66dbf1a4036c03a7cc4e7ec7ea608520fd7 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 04:02:27 +0300 Subject: [PATCH 03/17] [TS] Preserve constructor casts and reject nullish instances --- .../org/usvm/machine/expr/TsExprResolver.kt | 8 ++---- .../samples/types/RuntimeInstanceofTest.kt | 26 +++++++++++++++++++ .../samples/types/RuntimeInstanceof.ts | 22 ++++++++++++++++ 3 files changed, 50 insertions(+), 6 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 6226006dad..120b64053b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -22,7 +22,6 @@ import org.jacodb.ets.model.EtsClassCategory import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsClassValueRef -import org.jacodb.ets.model.EtsClassValueType import org.jacodb.ets.model.EtsClosureFieldRef import org.jacodb.ets.model.EtsConstant import org.jacodb.ets.model.EtsDeleteExpr @@ -402,10 +401,7 @@ class TsExprResolver( override fun visit(expr: EtsCastExpr): UExpr<*>? = with(ctx) { val resolvedExpr = resolve(expr.arg) ?: return@with null - if (resolvedExpr is UConcreteHeapRef && - classConstructorSignature(resolvedExpr) != null && - expr.type is EtsClassValueType - ) { + if (resolvedExpr is UConcreteHeapRef && classConstructorSignature(resolvedExpr) != null) { // TypeScript assertions do not change the identity of a constructor at runtime. return@with resolvedExpr } @@ -1199,7 +1195,7 @@ class TsExprResolver( EtsClassType(signature) } - if (arg.sort != addressSort) return falseExpr + if (arg.sort != addressSort || arg == mkUndefinedValue() || arg == mkTsNullValue()) return falseExpr val objectRef = arg.asExpr(addressSort) if (isAllocatedConcreteHeapRef(objectRef) && checkType is EtsClassType) { val objectTypes = scope.calcOnState { memory.typeStreamOf(objectRef).take(2) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt index e1262edd68..47d4f63f71 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -78,6 +78,9 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { "directConstructor" to 1.0, "castConstructor" to 1.0, "nonNullConstructor" to 1.0, + "anyConstructor" to 1.0, + "unknownConstructor" to 1.0, + "objectConstructor" to 1.0, "unrelatedConstructor" to 0.0, "classTypeof" to 1.0, "primitiveLeft" to 0.0, @@ -102,6 +105,29 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { }) } + @Test + fun `nullish left operands are not class instances`() { + val methods = listOf("undefinedLeft", "nullLeft") + + methods.forEach { methodName -> + val method = getMethod(methodName = methodName, className = "RuntimeInstanceof") + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty(), methodName) + outcome.states.forEach { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + assertEquals(0.0, assertIs(test.returnValue).number, methodName) + } + } + + replay(methods.map { methodName -> + "if (new RuntimeInstanceof().$methodName() !== 0) throw Error('$methodName');" + }) + } + @Test fun `subclass instance belongs to declared parent constructor`() { val method = getMethod(methodName = "inheritedConstructor", className = "RuntimeInstanceof") diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts index 96da11729c..cc76b1fcbd 100644 --- a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts +++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts @@ -18,6 +18,18 @@ class RuntimeInstanceof { return new InstanceA() instanceof InstanceA! ? 1 : 0; } + anyConstructor(): number { + return new InstanceA() instanceof (InstanceA as any) ? 1 : 0; + } + + unknownConstructor(): number { + return new InstanceA() instanceof (InstanceA as unknown as typeof InstanceA) ? 1 : 0; + } + + objectConstructor(): number { + return new InstanceA() instanceof (InstanceA as object as typeof InstanceA) ? 1 : 0; + } + inheritedConstructor(instance: InstanceChild): number { return instance instanceof InstanceParent ? 1 : 0; } @@ -39,6 +51,16 @@ class RuntimeInstanceof { return 42 instanceof InstanceA ? 1 : 0; } + undefinedLeft(): number { + const value: any = undefined; + return value instanceof InstanceA ? 1 : 0; + } + + nullLeft(): number { + const value: any = null; + return value instanceof InstanceA ? 1 : 0; + } + nonCallableRight(): boolean { const ctor: any = 42; return new InstanceA() instanceof ctor; From 8ab6fdac3d3ddfb84177badb5f541d60436fc750 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 04:27:45 +0300 Subject: [PATCH 04/17] [TS] Check instanceof against any receiver payload --- .../org/usvm/machine/expr/TsExprResolver.kt | 15 ++++++++ .../samples/types/RuntimeInstanceofTest.kt | 36 +++++++++++++++++++ .../samples/types/RuntimeInstanceof.ts | 4 +++ 3 files changed, 55 insertions(+) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 120b64053b..319a8f8c19 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -1196,6 +1196,21 @@ class TsExprResolver( } if (arg.sort != addressSort || arg == mkUndefinedValue() || arg == mkTsNullValue()) return falseExpr + if (arg.isFakeObject()) { + val fakeType = arg.getFakeType(scope) + val refValue = arg.extractRef(scope) + val isInstance = scope.calcOnState { + memory.types.evalIsSubtype(refValue, EtsNominalType(checkType)) + } + + return mkAnd( + fakeType.refTypeExpr, + mkHeapRefEq(refValue, mkTsNullValue()).not(), + mkHeapRefEq(refValue, mkUndefinedValue()).not(), + isInstance, + ) + } + val objectRef = arg.asExpr(addressSort) if (isAllocatedConcreteHeapRef(objectRef) && checkType is EtsClassType) { val objectTypes = scope.calcOnState { memory.typeStreamOf(objectRef).take(2) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt index 47d4f63f71..c15a538679 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -128,6 +128,42 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { }) } + @Test + fun `any receiver can contain an instance of the checked class`() { + val method = getMethod(methodName = "anyLeft", className = "RuntimeInstanceof") + val outcome = analyze("anyLeft") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + val cases = outcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + val input = test.before.parameters.single() + val actual = assertIs(test.returnValue).number + input to actual + } + assertEquals(setOf(0.0, 1.0), cases.map { it.second }.toSet(), "$cases") + + val generatedAssertions = cases.mapIndexed { index, (input, actual) -> + val argument = when (input) { + is TsTestValue.TsClass -> "new ${input.name}()" + is TsTestValue.TsBoolean -> input.value.toString() + is TsTestValue.TsNumber -> input.number.toString() + TsTestValue.TsNull -> "null" + TsTestValue.TsUndefined -> "undefined" + else -> error("Cannot replay generated instanceof input: $input") + } + + "if (new RuntimeInstanceof().anyLeft($argument) !== ${actual.toInt()}) " + + "throw Error('generated instanceof case $index');" + } + replay(generatedAssertions + listOf( + "if (new RuntimeInstanceof().anyLeft(new InstanceA()) !== 1) throw Error('A instance');", + "if (new RuntimeInstanceof().anyLeft(new InstanceB()) !== 0) throw Error('B instance');", + "if (new RuntimeInstanceof().anyLeft(42) !== 0) throw Error('primitive');", + )) + } + @Test fun `subclass instance belongs to declared parent constructor`() { val method = getMethod(methodName = "inheritedConstructor", className = "RuntimeInstanceof") diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts index cc76b1fcbd..883afec7be 100644 --- a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts +++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts @@ -51,6 +51,10 @@ class RuntimeInstanceof { return 42 instanceof InstanceA ? 1 : 0; } + anyLeft(value: any): number { + return value instanceof InstanceA ? 1 : 0; + } + undefinedLeft(): number { const value: any = undefined; return value instanceof InstanceA ? 1 : 0; From 8aa605d5907b27d6b28b1a7bdd9743e36be78361 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 04:50:57 +0300 Subject: [PATCH 05/17] [TS] Handle class constructors on instanceof left side --- .../org/usvm/machine/expr/TsExprResolver.kt | 10 ++++++ .../samples/types/RuntimeInstanceofTest.kt | 35 +++++++++++++++++++ .../samples/types/RuntimeInstanceof.ts | 14 ++++++++ 3 files changed, 59 insertions(+) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 319a8f8c19..9a32970105 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -1196,6 +1196,16 @@ class TsExprResolver( } if (arg.sort != addressSort || arg == mkUndefinedValue() || arg == mkTsNullValue()) return falseExpr + if (arg is UConcreteHeapRef && classConstructorSignature(arg) != null) { + if (checkType is EtsClassType && scene.projectClasses.any { it.signature == checkType.signature }) { + return falseExpr + } + + throw UnsupportedOperationException( + "instanceof on a class constructor against an SDK or unknown class is not modeled" + ) + } + if (arg.isFakeObject()) { val fakeType = arg.getFakeType(scope) val refValue = arg.extractRef(scope) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt index c15a538679..e8f2782428 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -164,6 +164,41 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { )) } + @Test + fun `class constructor values are not instances of project classes`() { + val methods = listOf("constructorLeft", "constructorAliasLeft", "anyConstructorLeft") + + methods.forEach { methodName -> + val method = getMethod(methodName = methodName, className = "RuntimeInstanceof") + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty(), methodName) + + val tests = outcome.states.map { state -> + assertIs(state.methodResult, methodName) + val test = TsTestResolver().resolve(method, state) + assertEquals(0.0, assertIs(test.returnValue).number, methodName) + test + } + + if (methodName == "constructorAliasLeft") { + val inputs = tests.map { test -> + assertIs(test.before.parameters.single()).value + } + assertEquals(setOf(false, true), inputs.toSet()) + } + } + + replay(listOf( + "if (new RuntimeInstanceof().constructorLeft() !== 0) throw Error('direct ctor LHS');", + "if (new RuntimeInstanceof().constructorAliasLeft(true) !== 0) throw Error('A ctor LHS');", + "if (new RuntimeInstanceof().constructorAliasLeft(false) !== 0) throw Error('B ctor LHS');", + "if (new RuntimeInstanceof().anyConstructorLeft() !== 0) throw Error('any ctor LHS');", + )) + } + @Test fun `subclass instance belongs to declared parent constructor`() { val method = getMethod(methodName = "inheritedConstructor", className = "RuntimeInstanceof") diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts index 883afec7be..a69ac9229d 100644 --- a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts +++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts @@ -55,6 +55,20 @@ class RuntimeInstanceof { return value instanceof InstanceA ? 1 : 0; } + constructorLeft(): number { + return InstanceA instanceof InstanceA ? 1 : 0; + } + + constructorAliasLeft(useA: boolean): number { + const ctor = useA ? InstanceA : InstanceB; + return ctor instanceof InstanceA ? 1 : 0; + } + + anyConstructorLeft(): number { + const value: any = InstanceA; + return value instanceof InstanceA ? 1 : 0; + } + undefinedLeft(): number { const value: any = undefined; return value instanceof InstanceA ? 1 : 0; From 89226121bc06adeecf7425c9bb78156912b76c45 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 05:31:36 +0300 Subject: [PATCH 06/17] Model instanceof TypeError for known non-callable values --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 30 ++++- .../kotlin/org/usvm/machine/TsRuntimeError.kt | 17 +++ .../org/usvm/machine/expr/TsExprResolver.kt | 88 ++++++++++---- .../samples/types/RuntimeInstanceofTest.kt | 114 ++++++++++++++++-- .../kotlin/org/usvm/util/TsTestResolver.kt | 10 ++ .../samples/types/RuntimeInstanceof.ts | 65 ++++++++++ 6 files changed, 291 insertions(+), 33 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt 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 f817f13d9f..65872e7688 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -1,10 +1,15 @@ package org.usvm.machine import mu.KotlinLogging +import org.jacodb.ets.model.EtsAliasType import org.jacodb.ets.model.EtsClassValueType +import org.jacodb.ets.model.EtsGenericType +import org.jacodb.ets.model.EtsIntersectionType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnionType import org.usvm.CoverageZone import org.usvm.StateCollectionStrategy import org.usvm.UMachine @@ -252,7 +257,10 @@ class TsMachine( val unsupportedPaths = mutableSetOf() methods.forEach { method -> - val constructorParameter = method.parameters.firstOrNull { it.type is EtsClassValueType } + val genericParameters = method.typeParameters.filterIsInstance().associateBy { it.typeName } + val constructorParameter = method.parameters.firstOrNull { + it.type.containsConstructorValue(genericParameters) + } if (constructorParameter != null) { unsupportedPaths += "Constructor-typed parameter '${constructorParameter.name}' " + "in ${method.humanReadableSignature} is not modeled" @@ -268,3 +276,23 @@ class TsMachine( components.close() } } + +private fun EtsType.containsConstructorValue( + genericParameters: Map, + visitedGenerics: Set = emptySet(), +): Boolean = when (this) { + is EtsClassValueType -> true + is EtsUnionType -> types.any { it.containsConstructorValue(genericParameters, visitedGenerics) } + is EtsIntersectionType -> types.any { it.containsConstructorValue(genericParameters, visitedGenerics) } + is EtsAliasType -> originalType.containsConstructorValue(genericParameters, visitedGenerics) + is EtsGenericType -> { + if (typeName in visitedGenerics) { + false + } else { + val declaration = genericParameters[typeName] + listOfNotNull(constraint, defaultType, declaration?.constraint, declaration?.defaultType) + .any { it.containsConstructorValue(genericParameters, visitedGenerics + typeName) } + } + } + else -> false +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt new file mode 100644 index 0000000000..9a6d36d630 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt @@ -0,0 +1,17 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFileSignature + +private val runtimeFile = EtsFileSignature( + projectName = "usvm.ts.runtime", + fileName = "TypeError", +) +private val typeErrorSignature = EtsClassSignature( + name = "TypeError", + file = runtimeFile, +) + +/** Type identity of terminal JavaScript TypeError exceptions produced by the interpreter. */ +internal val TS_TYPE_ERROR_TYPE = EtsClassType(typeErrorSignature) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 9a32970105..26cfb074a8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -107,6 +107,7 @@ import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isTrue +import org.usvm.machine.TS_TYPE_ERROR_TYPE import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext import org.usvm.machine.TsOptions @@ -1170,29 +1171,7 @@ class TsExprResolver( expr.checkType as? EtsRefType ?: return falseExpr } else { - val constructor = resolve(checkValue) ?: return null - if (constructor.sort != addressSort || - constructor == mkTsNullValue() || - constructor == mkUndefinedValue() - ) { - throw UnsupportedOperationException( - "Non-callable instanceof RHS requires a TypeError object, which is not modeled" - ) - } - - val constructorRef = constructor as? UConcreteHeapRef - ?: throw UnsupportedOperationException("Symbolic instanceof constructor identity is not modeled") - val signature = classConstructorSignature(constructorRef) - ?: throw UnsupportedOperationException("Unknown instanceof constructor value: $constructorRef") - val clazz = scene.projectAndSdkClasses.singleOrNull { it.signature == signature } - ?: throw UnsupportedOperationException("Unknown instanceof class: $signature") - val hasComputedStaticMethod = hierarchy.getAncestors(clazz) - .any { ancestor -> ancestor.methods.any { it.name == "%computed" && it.modifiers.isStatic } } - if (hasComputedStaticMethod) { - throw UnsupportedOperationException("Custom Symbol.hasInstance may override instanceof for $signature") - } - - EtsClassType(signature) + resolveInstanceofConstructor(checkValue) ?: return null } if (arg.sort != addressSort || arg == mkUndefinedValue() || arg == mkTsNullValue()) return falseExpr @@ -1237,6 +1216,69 @@ class TsExprResolver( scope.calcOnState { memory.types.evalIsSubtype(objectRef, EtsNominalType(checkType)) } } + private fun resolveInstanceofConstructor(checkValue: EtsEntity): EtsClassType? = with(ctx) { + val constructor = resolve(checkValue) ?: return null + if (constructor.sort == fp64Sort || constructor.sort == boolSort) return throwInstanceofTypeError() + if (constructor == mkTsNullValue() || constructor == mkUndefinedValue()) return throwInstanceofTypeError() + + if (constructor.sort != addressSort || constructor.isFakeObject()) { + throw UnsupportedOperationException("Unresolved instanceof RHS callability is not modeled") + } + + val constructorRef = constructor as? UConcreteHeapRef + ?: throw UnsupportedOperationException("Symbolic instanceof constructor identity is not modeled") + if (getStringConstantValue(constructorRef) != null) return throwInstanceofTypeError() + + val signature = classConstructorSignature(constructorRef) + ?: return resolveNonConstructorInstanceofRight(constructorRef) + val clazz = scene.projectAndSdkClasses.singleOrNull { it.signature == signature } + ?: throw UnsupportedOperationException("Unknown instanceof class: $signature") + val hasComputedStaticMethod = hierarchy.getAncestors(clazz) + .any { ancestor -> ancestor.methods.any { it.name == "%computed" && it.modifiers.isStatic } } + if (hasComputedStaticMethod) { + throw UnsupportedOperationException("Custom Symbol.hasInstance may override instanceof for $signature") + } + + EtsClassType(signature) + } + + private fun resolveNonConstructorInstanceofRight(ref: UConcreteHeapRef): Nothing? = with(ctx) { + val objectTypes = if (isAllocatedConcreteHeapRef(ref)) { + scope.calcOnState { memory.typeStreamOf(ref).take(n = 2) } + } else { + null + } + val objectType = (objectTypes as? TypesResult.SuccessfulTypesResult)?.types?.singleOrNull() + if (objectType == EtsStringType) return throwInstanceofTypeError() + + val objectClass = (objectType as? EtsClassType)?.let { type -> + scene.projectClasses.singleOrNull { it.signature == type.signature } + } + if (objectClass != null) { + // Computed members may include Symbol.hasInstance, so their instances need a separate model. + val ordinaryObject = objectClass.category == EtsClassCategory.CLASS || + objectClass.category == EtsClassCategory.OBJECT + val hasComputedMember = hierarchy.getAncestors(objectClass).any { ancestor -> + ancestor.methods.any { it.name == "%computed" || it.name == "Symbol.hasInstance" } || + ancestor.fields.any { it.name == "%computed" || it.name == "Symbol.hasInstance" } + } + val isFunction = scope.calcOnState { associatedFunction[ref] != null } + + if (ordinaryObject && !hasComputedMember && !isFunction) return throwInstanceofTypeError() + } + + throw UnsupportedOperationException("Unknown instanceof constructor value: $ref") + } + + private fun throwInstanceofTypeError(): Nothing? { + scope.doWithState { + val exception = memory.allocConcrete(TS_TYPE_ERROR_TYPE) + methodResult = TsMethodResult.TsException(exception, TS_TYPE_ERROR_TYPE) + } + + return null + } + // endregion // region CALL diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt index e8f2782428..d1f46d4b23 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -6,6 +6,7 @@ import org.junit.jupiter.api.io.TempDir import org.usvm.StateCollectionStrategy import org.usvm.UMachineOptions import org.usvm.api.TsTestValue +import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsAnalysisStopReason import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions @@ -52,6 +53,25 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { }) } + @Test + fun `returned class value keeps constructor identity`() { + val method = getMethod(methodName = "returnedConstructor", className = "RuntimeInstanceof") + val outcome = analyze("returnedConstructor") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + outcome.states.forEach { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + assertEquals(1.0, assertIs(test.returnValue).number) + } + + replay(listOf( + "if (new RuntimeInstanceof().returnedConstructor() !== 1) throw Error('returned constructor');" + )) + } + @Test fun `typeof recognizes constructor values stored in a local`() { val method = getMethod(methodName = "aliasedClassTypeof", className = "RuntimeInstanceof") @@ -219,15 +239,47 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { } @Test - fun `non callable RHS and custom hasInstance are explicitly unsupported`() { - val nonCallable = analyze("nonCallableRight") + fun `non callable RHS throws a TypeError object`() { + val methods = listOf( + "nonCallableRight", + "booleanRight", + "stringRight", + "nullRight", + "undefinedRight", + "objectRight", + "classInstanceRight", + ) + + methods.forEach { methodName -> + val method = getMethod(methodName = methodName, className = "RuntimeInstanceof") + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty(), methodName) + outcome.states.forEach { state -> + val exception = assertIs(state.methodResult) + assertEquals("TypeError", exception.type.typeName) + assertTrue(isAllocatedConcreteHeapRef(exception.value)) + + val test = TsTestResolver().resolve(method, state) + val objectException = assertIs(test.returnValue) + assertEquals("TypeError", assertIs(objectException.value).name) + } + } + + replay(methods.map { methodName -> + "let caught$methodName = false; try { new RuntimeInstanceof().$methodName(); } " + + "catch (error) { caught$methodName = error instanceof TypeError; } " + + "if (!caught$methodName) throw Error('$methodName TypeError');" + }) + } + + @Test + fun `custom hasInstance is explicitly unsupported`() { val custom = analyze("customHasInstance") val inherited = analyze("inheritedHasInstance") - assertEquals(TsAnalysisStopReason.EXHAUSTED, nonCallable.stopReason) - assertTrue(nonCallable.states.isEmpty()) - assertTrue(nonCallable.unsupportedPaths.any { "TypeError" in it }, "${nonCallable.unsupportedPaths}") - assertEquals(TsAnalysisStopReason.EXHAUSTED, custom.stopReason) assertTrue(custom.states.isEmpty()) assertTrue(custom.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${custom.unsupportedPaths}") @@ -237,15 +289,29 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { assertTrue(inherited.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${inherited.unsupportedPaths}") replay(listOf( - "let typeError = false; try { new RuntimeInstanceof().nonCallableRight(); } " + - "catch (error) { typeError = error instanceof TypeError; } " + - "if (!typeError) throw Error('TypeError');", "if (new RuntimeInstanceof().customHasInstance() !== false) throw Error('custom hasInstance');", "if (new RuntimeInstanceof().inheritedHasInstance(new InstanceHasInstanceChild()) !== false) " + "throw Error('inherited hasInstance');", )) } + @Test + fun `symbolic RHS stays explicitly unsupported until callability is modeled`() { + val outcome = analyze("unresolvedRight") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.unsupportedPaths.any { "Unresolved instanceof RHS callability" in it }, + "${outcome.unsupportedPaths}") + + replay(listOf( + "if (new RuntimeInstanceof().unresolvedRight(InstanceA) !== true) throw Error('callable RHS');", + "let threwTypeError = false; try { new RuntimeInstanceof().unresolvedRight(42); } " + + "catch (error) { threwTypeError = error instanceof TypeError; } " + + "if (!threwTypeError) throw Error('non-callable RHS');", + )) + } + @Test fun `constructor typed input has an explicit unsupported outcome`() { val outcome = analyze("constructorParameter") @@ -261,6 +327,36 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { )) } + @Test + fun `constructor containing input types have explicit unsupported outcomes`() { + val methods = listOf( + "constructorUnionParameter", + "nullableConstructorParameter", + "constructorAliasParameter", + "constructorIntersectionParameter", + "genericConstructorParameter", + ) + + methods.forEach { methodName -> + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}") + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + "$methodName: ${outcome.unsupportedPaths}") + } + + replay(listOf( + "if (new RuntimeInstanceof().constructorUnionParameter(InstanceA) !== true) throw Error('union A');", + "if (new RuntimeInstanceof().constructorUnionParameter(InstanceB) !== true) throw Error('union B');", + "if (new RuntimeInstanceof().nullableConstructorParameter(null) !== true) throw Error('nullable null');", + "if (new RuntimeInstanceof().nullableConstructorParameter(InstanceA) !== true) throw Error('nullable A');", + "if (new RuntimeInstanceof().constructorAliasParameter(InstanceA) !== true) throw Error('alias');", + "if (new RuntimeInstanceof().constructorIntersectionParameter(InstanceA) !== true) throw Error('intersection');", + "if (new RuntimeInstanceof().genericConstructorParameter(InstanceA) !== true) throw Error('generic');", + )) + } + @Test fun `unsupported constructor input does not hide another entrypoint`() { val methods = listOf("constructorParameter", "directConstructor") diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 3ddbe5bc3c..9dd242ac27 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -39,6 +39,7 @@ import org.usvm.collection.field.UFieldLValue import org.usvm.isAllocated import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isTrue +import org.usvm.machine.TS_TYPE_ERROR_TYPE import org.usvm.machine.TsContext import org.usvm.machine.expr.TrackedObjectProperty import org.usvm.machine.expr.TsUnresolvedSort @@ -149,6 +150,15 @@ class TsTestResolver { try { // Dispatch based on the exception type, similar to string const resolution when (res.type) { + TS_TYPE_ERROR_TYPE -> { + val concreteRef = evaluateInModel(res.value) as? UConcreteHeapRef + check(concreteRef != null && isAllocatedConcreteHeapRef(concreteRef)) + + TsTestValue.TsException.ObjectException( + TsTestValue.TsClass(name = "TypeError", properties = emptyMap()) + ) + } + is EtsStringType -> { val concreteRef = evaluateInModel(res.value) as? UConcreteHeapRef if (concreteRef != null && isAllocatedConcreteHeapRef(concreteRef)) { diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts index a69ac9229d..6100475b5f 100644 --- a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts +++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts @@ -6,6 +6,15 @@ class RuntimeInstanceof { return new InstanceA() instanceof ctor ? 1 : 0; } + constructorValue(): typeof InstanceA { + return InstanceA; + } + + returnedConstructor(): number { + const ctor = this.constructorValue(); + return new InstanceA() instanceof ctor && typeof ctor === "function" ? 1 : 0; + } + directConstructor(): number { return new InstanceA() instanceof InstanceA ? 1 : 0; } @@ -84,6 +93,40 @@ class RuntimeInstanceof { return new InstanceA() instanceof ctor; } + booleanRight(): boolean { + const ctor: any = true; + return new InstanceA() instanceof ctor; + } + + stringRight(): boolean { + const ctor: any = "not a constructor"; + return new InstanceA() instanceof ctor; + } + + nullRight(): boolean { + const ctor: any = null; + return new InstanceA() instanceof ctor; + } + + undefinedRight(): boolean { + const ctor: any = undefined; + return new InstanceA() instanceof ctor; + } + + objectRight(): boolean { + const ctor: any = {}; + return new InstanceA() instanceof ctor; + } + + classInstanceRight(): boolean { + const ctor: any = new InstanceB(); + return new InstanceA() instanceof ctor; + } + + unresolvedRight(ctor: any): boolean { + return new InstanceA() instanceof ctor; + } + customHasInstance(): boolean { return new InstanceCustom() instanceof InstanceCustom; } @@ -95,8 +138,30 @@ class RuntimeInstanceof { constructorParameter(ctor: typeof InstanceA): boolean { return new InstanceA() instanceof ctor; } + + constructorUnionParameter(ctor: typeof InstanceA | typeof InstanceB): boolean { + return typeof ctor === "function"; + } + + nullableConstructorParameter(ctor: typeof InstanceA | null): boolean { + return ctor === null || typeof ctor === "function"; + } + + constructorAliasParameter(ctor: InstanceConstructorAlias): boolean { + return typeof ctor === "function"; + } + + constructorIntersectionParameter(ctor: typeof InstanceA & { marker?: number }): boolean { + return typeof ctor === "function"; + } + + genericConstructorParameter(ctor: T): boolean { + return typeof ctor === "function"; + } } +type InstanceConstructorAlias = typeof InstanceA | typeof InstanceB; + class InstanceA {} class InstanceB {} class InstanceParent {} From fbb8f5f2b65fbf6c30af608a3f6ffb9104e093bd Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 06:07:57 +0300 Subject: [PATCH 07/17] Guard nested constructor-valued TypeScript inputs --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 102 +++++++++++++++++- .../samples/types/RuntimeInstanceofTest.kt | 76 +++++++++++++ .../samples/types/RuntimeInstanceof.ts | 35 ++++++ 3 files changed, 208 insertions(+), 5 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 65872e7688..9144104572 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -2,13 +2,20 @@ package org.usvm.machine import mu.KotlinLogging import org.jacodb.ets.model.EtsAliasType +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsClassValueType +import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsGenericType import org.jacodb.ets.model.EtsIntersectionType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.model.EtsTupleType import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUnionType import org.usvm.CoverageZone import org.usvm.StateCollectionStrategy @@ -255,11 +262,12 @@ class TsMachine( ): Pair, MutableSet> { val initialStates = mutableMapOf() val unsupportedPaths = mutableSetOf() + val classesBySignature = analysisScene.projectAndSdkClasses.associateBy { it.signature } methods.forEach { method -> val genericParameters = method.typeParameters.filterIsInstance().associateBy { it.typeName } val constructorParameter = method.parameters.firstOrNull { - it.type.containsConstructorValue(genericParameters) + it.type.containsConstructorValue(genericParameters, classesBySignature) } if (constructorParameter != null) { unsupportedPaths += "Constructor-typed parameter '${constructorParameter.name}' " + @@ -279,20 +287,104 @@ class TsMachine( private fun EtsType.containsConstructorValue( genericParameters: Map, + classesBySignature: Map, visitedGenerics: Set = emptySet(), + visitedClasses: Set = emptySet(), ): Boolean = when (this) { is EtsClassValueType -> true - is EtsUnionType -> types.any { it.containsConstructorValue(genericParameters, visitedGenerics) } - is EtsIntersectionType -> types.any { it.containsConstructorValue(genericParameters, visitedGenerics) } - is EtsAliasType -> originalType.containsConstructorValue(genericParameters, visitedGenerics) + is EtsUnionType -> types.any { + it.containsConstructorValue(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + } + is EtsIntersectionType -> types.any { + it.containsConstructorValue(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + } + is EtsTupleType -> types.any { + it.containsConstructorValue(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + } + is EtsArrayType -> elementType.containsConstructorValue( + genericParameters, + classesBySignature, + visitedGenerics, + visitedClasses, + ) + is EtsClassType -> containsConstructorValueInClass( + genericParameters, + classesBySignature, + visitedGenerics, + visitedClasses, + ) + is EtsUnclearRefType -> typeParameters.any { + it.containsConstructorValue(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + } + is EtsAliasType -> originalType.containsConstructorValue( + genericParameters, + classesBySignature, + visitedGenerics, + visitedClasses, + ) is EtsGenericType -> { if (typeName in visitedGenerics) { false } else { val declaration = genericParameters[typeName] listOfNotNull(constraint, defaultType, declaration?.constraint, declaration?.defaultType) - .any { it.containsConstructorValue(genericParameters, visitedGenerics + typeName) } + .any { + it.containsConstructorValue( + genericParameters, + classesBySignature, + visitedGenerics + typeName, + visitedClasses, + ) + } } } else -> false } + +private fun EtsClassType.containsConstructorValueInClass( + genericParameters: Map, + classesBySignature: Map, + visitedGenerics: Set, + visitedClasses: Set, +): Boolean { + val constructorInTypeArguments = typeParameters.any { + it.containsConstructorValue(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + } + if (constructorInTypeArguments) { + return true + } + + if (signature in visitedClasses) { + return false + } + + val clazz = classesBySignature[signature] ?: return false + val nextVisitedClasses = visitedClasses + signature + val constructorInFields = clazz.fields.any { field -> + !field.modifiers.isStatic && field.type.containsConstructorValue( + genericParameters, + classesBySignature, + visitedGenerics, + nextVisitedClasses, + ) + } + if (constructorInFields) { + return true + } + + val superClass = clazz.superClass ?: return false + val superClasses = if (superClass.file == EtsFileSignature.UNKNOWN) { + classesBySignature.values.filter { it.name == superClass.name } + } else { + listOfNotNull(classesBySignature[superClass]) + } + + return superClasses.any { parent -> + EtsClassType(parent.signature).containsConstructorValue( + genericParameters, + classesBySignature, + visitedGenerics, + nextVisitedClasses, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt index d1f46d4b23..1e0884fd41 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -357,6 +357,82 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { )) } + @Test + fun `constructor arrays have an explicit unsupported outcome`() { + val methods = listOf("constructorArrayParameter", "constructorNestedArrayParameter") + + methods.forEach { methodName -> + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}") + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + "$methodName: ${outcome.unsupportedPaths}") + } + + replay(listOf( + "if (new RuntimeInstanceof().constructorArrayParameter([InstanceA]) !== true) throw Error('array');", + "if (new RuntimeInstanceof().constructorNestedArrayParameter([[InstanceA]]) !== true) " + + "throw Error('nested array');", + )) + } + + @Test + fun `constructor tuple has an explicit unsupported outcome`() { + val outcome = analyze("constructorTupleParameter") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + "${outcome.unsupportedPaths}") + + replay(listOf( + "if (new RuntimeInstanceof().constructorTupleParameter([InstanceA]) !== true) throw Error('tuple');" + )) + } + + @Test + fun `constructor value in class type argument has an explicit unsupported outcome`() { + val outcome = analyze("constructorBoxParameter") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty(), "${outcome.states}") + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + "${outcome.unsupportedPaths}") + + replay(listOf( + "const box = new InstanceConstructorBox(); box.value = InstanceA; " + + "if (new RuntimeInstanceof().constructorBoxParameter(box) !== true) throw Error('box');", + )) + } + + @Test + fun `constructor values in object fields have explicit unsupported outcomes`() { + val methods = listOf( + "structuralConstructorParameter", + "recursiveConstructorParameter", + "inheritedConstructorParameter", + ) + + methods.forEach { methodName -> + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}") + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + "$methodName: ${outcome.unsupportedPaths}") + } + + replay(listOf( + "if (new RuntimeInstanceof().structuralConstructorParameter({ ctor: InstanceA }) !== true) " + + "throw Error('structural');", + "const holder = new InstanceRecursiveHolder(); holder.ctor = InstanceA; " + + "if (new RuntimeInstanceof().recursiveConstructorParameter(holder) !== true) throw Error('recursive');", + "const inherited = new InstanceInheritedHolder(); inherited.ctor = InstanceA; " + + "if (new RuntimeInstanceof().inheritedConstructorParameter(inherited) !== true) throw Error('inherited');", + )) + } + @Test fun `unsupported constructor input does not hide another entrypoint`() { val methods = listOf("constructorParameter", "directConstructor") diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts index 6100475b5f..5917835226 100644 --- a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts +++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts @@ -158,12 +158,47 @@ class RuntimeInstanceof { genericConstructorParameter(ctor: T): boolean { return typeof ctor === "function"; } + + constructorTupleParameter(ctors: [typeof InstanceA]): boolean { + return new InstanceA() instanceof ctors[0]; + } + + constructorArrayParameter(ctors: (typeof InstanceA)[]): boolean { + return ctors.length === 1 && new InstanceA() instanceof ctors[0]; + } + + constructorNestedArrayParameter(ctors: (typeof InstanceA)[][]): boolean { + return new InstanceA() instanceof ctors[0][0]; + } + + constructorBoxParameter(box: InstanceConstructorBox): boolean { + return typeof box.value === "function"; + } + + structuralConstructorParameter(holder: { ctor: typeof InstanceA }): boolean { + return typeof holder.ctor === "function"; + } + + recursiveConstructorParameter(holder: InstanceRecursiveHolder): boolean { + return typeof holder.ctor === "function"; + } + + inheritedConstructorParameter(holder: InstanceInheritedHolder): boolean { + return typeof holder.ctor === "function"; + } } type InstanceConstructorAlias = typeof InstanceA | typeof InstanceB; class InstanceA {} class InstanceB {} +class InstanceConstructorBox { value!: T; } +class InstanceRecursiveHolder { + next?: InstanceRecursiveHolder; + ctor!: typeof InstanceA; +} +class InstanceConstructorBase { ctor!: typeof InstanceA; } +class InstanceInheritedHolder extends InstanceConstructorBase {} class InstanceParent {} class InstanceChild extends InstanceParent { childMarker: number = 1; } class InstanceCustom { From 8de747cbfda1901cf7ceec81a121fa870cdf9fdc Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 06:27:59 +0300 Subject: [PATCH 08/17] Guard inherited generic TypeScript input fields --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 104 +++++++++++------- .../samples/types/RuntimeInstanceofTest.kt | 38 +++++++ .../samples/types/RuntimeInstanceof.ts | 17 +++ 3 files changed, 122 insertions(+), 37 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 9144104572..da08c28390 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -266,11 +266,13 @@ class TsMachine( methods.forEach { method -> val genericParameters = method.typeParameters.filterIsInstance().associateBy { it.typeName } - val constructorParameter = method.parameters.firstOrNull { - it.type.containsConstructorValue(genericParameters, classesBySignature) + val unsupportedParameter = method.parameters.firstNotNullOfOrNull { parameter -> + val gap = parameter.type.constructorInputGap(genericParameters, classesBySignature) + gap?.let { parameter to it } } - if (constructorParameter != null) { - unsupportedPaths += "Constructor-typed parameter '${constructorParameter.name}' " + + if (unsupportedParameter != null) { + val (parameter, gap) = unsupportedParameter + unsupportedPaths += "${gap.description} '${parameter.name}' " + "in ${method.humanReadableSignature} is not modeled" } else { initialStates[method] = interpreter.getInitialState(method, targets) @@ -285,38 +287,43 @@ class TsMachine( } } -private fun EtsType.containsConstructorValue( +private enum class ConstructorInputGap(val description: String) { + CONSTRUCTOR_VALUE("Constructor-typed parameter"), + UNRESOLVED_INHERITED_GENERIC("Unresolved inherited generic field in parameter"), +} + +private fun EtsType.constructorInputGap( genericParameters: Map, classesBySignature: Map, visitedGenerics: Set = emptySet(), visitedClasses: Set = emptySet(), -): Boolean = when (this) { - is EtsClassValueType -> true - is EtsUnionType -> types.any { - it.containsConstructorValue(genericParameters, classesBySignature, visitedGenerics, visitedClasses) +): ConstructorInputGap? = when (this) { + is EtsClassValueType -> ConstructorInputGap.CONSTRUCTOR_VALUE + is EtsUnionType -> types.firstNotNullOfOrNull { + it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) } - is EtsIntersectionType -> types.any { - it.containsConstructorValue(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + is EtsIntersectionType -> types.firstNotNullOfOrNull { + it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) } - is EtsTupleType -> types.any { - it.containsConstructorValue(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + is EtsTupleType -> types.firstNotNullOfOrNull { + it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) } - is EtsArrayType -> elementType.containsConstructorValue( + is EtsArrayType -> elementType.constructorInputGap( genericParameters, classesBySignature, visitedGenerics, visitedClasses, ) - is EtsClassType -> containsConstructorValueInClass( + is EtsClassType -> constructorInputGapInClass( genericParameters, classesBySignature, visitedGenerics, visitedClasses, ) - is EtsUnclearRefType -> typeParameters.any { - it.containsConstructorValue(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + is EtsUnclearRefType -> typeParameters.firstNotNullOfOrNull { + it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) } - is EtsAliasType -> originalType.containsConstructorValue( + is EtsAliasType -> originalType.constructorInputGap( genericParameters, classesBySignature, visitedGenerics, @@ -324,12 +331,12 @@ private fun EtsType.containsConstructorValue( ) is EtsGenericType -> { if (typeName in visitedGenerics) { - false + null } else { val declaration = genericParameters[typeName] listOfNotNull(constraint, defaultType, declaration?.constraint, declaration?.defaultType) - .any { - it.containsConstructorValue( + .firstNotNullOfOrNull { + it.constructorInputGap( genericParameters, classesBySignature, visitedGenerics + typeName, @@ -338,53 +345,76 @@ private fun EtsType.containsConstructorValue( } } } - else -> false + else -> null } -private fun EtsClassType.containsConstructorValueInClass( +private fun EtsClassType.constructorInputGapInClass( genericParameters: Map, classesBySignature: Map, visitedGenerics: Set, visitedClasses: Set, -): Boolean { - val constructorInTypeArguments = typeParameters.any { - it.containsConstructorValue(genericParameters, classesBySignature, visitedGenerics, visitedClasses) +): ConstructorInputGap? { + val typeArgumentGap = typeParameters.firstNotNullOfOrNull { + it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) } - if (constructorInTypeArguments) { - return true + if (typeArgumentGap != null) { + return typeArgumentGap } if (signature in visitedClasses) { - return false + return null } - val clazz = classesBySignature[signature] ?: return false + val clazz = classesBySignature[signature] ?: return null val nextVisitedClasses = visitedClasses + signature - val constructorInFields = clazz.fields.any { field -> - !field.modifiers.isStatic && field.type.containsConstructorValue( + val fieldGap = clazz.fields.firstNotNullOfOrNull { field -> + if (field.modifiers.isStatic) return@firstNotNullOfOrNull null + + field.type.constructorInputGap( genericParameters, classesBySignature, visitedGenerics, nextVisitedClasses, ) } - if (constructorInFields) { - return true + if (fieldGap != null) { + return fieldGap } - val superClass = clazz.superClass ?: return false + val superClass = clazz.superClass ?: return null val superClasses = if (superClass.file == EtsFileSignature.UNKNOWN) { classesBySignature.values.filter { it.name == superClass.name } } else { listOfNotNull(classesBySignature[superClass]) } - return superClasses.any { parent -> - EtsClassType(parent.signature).containsConstructorValue( + return superClasses.firstNotNullOfOrNull { parent -> + val parentGap = EtsClassType(parent.signature).constructorInputGap( genericParameters, classesBySignature, visitedGenerics, nextVisitedClasses, ) + if (parentGap != null) return@firstNotNullOfOrNull parentGap + + // The frontend omits extends type arguments, so an inherited T may contain a constructor. + val parentGenerics = parent.typeParameters.filterIsInstance() + .mapTo(mutableSetOf()) { it.typeName } + val unresolvedGenericField = parent.fields.any { field -> + !field.modifiers.isStatic && field.type.containsGeneric(parentGenerics) + } + if (unresolvedGenericField) ConstructorInputGap.UNRESOLVED_INHERITED_GENERIC else null } } + +private fun EtsType.containsGeneric(names: Set): Boolean = when (this) { + is EtsGenericType -> typeName in names + is EtsUnionType -> types.any { it.containsGeneric(names) } + is EtsIntersectionType -> types.any { it.containsGeneric(names) } + is EtsTupleType -> types.any { it.containsGeneric(names) } + is EtsArrayType -> elementType.containsGeneric(names) + is EtsClassType -> typeParameters.any { it.containsGeneric(names) } + is EtsUnclearRefType -> typeParameters.any { it.containsGeneric(names) } + is EtsAliasType -> originalType.containsGeneric(names) + else -> false +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt index 1e0884fd41..4d87959ea0 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -433,6 +433,44 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { )) } + @Test + fun `inherited generic fields have explicit unsupported outcomes`() { + val methods = listOf("inheritedGenericConstructorParameter", "inheritedGenericNumberParameter") + + methods.forEach { methodName -> + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}") + assertTrue(outcome.unsupportedPaths.any { "Unresolved inherited generic" in it }, + "$methodName: ${outcome.unsupportedPaths}") + } + + replay(listOf( + "const holder = new InstanceInheritedGenericConstructor(); holder.ctor = InstanceA; " + + "if (new RuntimeInstanceof().inheritedGenericConstructorParameter(holder) !== true) " + + "throw Error('inherited generic');", + "const numberHolder = new InstanceInheritedGenericNumber(); numberHolder.ctor = 1; " + + "if (new RuntimeInstanceof().inheritedGenericNumberParameter(numberHolder) !== true) " + + "throw Error('inherited generic number');", + )) + } + + @Test + fun `concrete inherited number field remains supported`() { + val outcome = analyze("inheritedConcreteNumberParameter") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + + replay(listOf( + "const holder = new InstanceInheritedConcreteNumber(); holder.value = 1; " + + "if (new RuntimeInstanceof().inheritedConcreteNumberParameter(holder) !== true) " + + "throw Error('inherited concrete number');", + )) + } + @Test fun `unsupported constructor input does not hide another entrypoint`() { val methods = listOf("constructorParameter", "directConstructor") diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts index 5917835226..613f71f7bc 100644 --- a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts +++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts @@ -186,6 +186,18 @@ class RuntimeInstanceof { inheritedConstructorParameter(holder: InstanceInheritedHolder): boolean { return typeof holder.ctor === "function"; } + + inheritedGenericConstructorParameter(holder: InstanceInheritedGenericConstructor): boolean { + return typeof holder.ctor === "function"; + } + + inheritedGenericNumberParameter(holder: InstanceInheritedGenericNumber): boolean { + return typeof holder.ctor === "number"; + } + + inheritedConcreteNumberParameter(holder: InstanceInheritedConcreteNumber): boolean { + return holder.value === 1; + } } type InstanceConstructorAlias = typeof InstanceA | typeof InstanceB; @@ -199,6 +211,11 @@ class InstanceRecursiveHolder { } class InstanceConstructorBase { ctor!: typeof InstanceA; } class InstanceInheritedHolder extends InstanceConstructorBase {} +class InstanceGenericConstructorBase { ctor!: T; } +class InstanceInheritedGenericConstructor extends InstanceGenericConstructorBase {} +class InstanceInheritedGenericNumber extends InstanceGenericConstructorBase {} +class InstanceConcreteNumberBase { value!: number; } +class InstanceInheritedConcreteNumber extends InstanceConcreteNumberBase {} class InstanceParent {} class InstanceChild extends InstanceParent { childMarker: number = 1; } class InstanceCustom { From b9a4702538b565efdb376d48756b457d523d73ee Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 06:43:24 +0300 Subject: [PATCH 09/17] [TS] Reject computed static fields for instanceof --- .../org/usvm/machine/expr/TsExprResolver.kt | 11 ++++++++--- .../usvm/samples/types/RuntimeInstanceofTest.kt | 14 ++++++++++++++ .../resources/samples/types/RuntimeInstanceof.ts | 15 +++++++++++++++ 3 files changed, 37 insertions(+), 3 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 26cfb074a8..87dc9f14a1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -1233,9 +1233,14 @@ class TsExprResolver( ?: return resolveNonConstructorInstanceofRight(constructorRef) val clazz = scene.projectAndSdkClasses.singleOrNull { it.signature == signature } ?: throw UnsupportedOperationException("Unknown instanceof class: $signature") - val hasComputedStaticMethod = hierarchy.getAncestors(clazz) - .any { ancestor -> ancestor.methods.any { it.name == "%computed" && it.modifiers.isStatic } } - if (hasComputedStaticMethod) { + val hasPotentialCustomHasInstance = hierarchy.getAncestors(clazz).any { ancestor -> + ancestor.methods.any { method -> + method.modifiers.isStatic && (method.name == "%computed" || method.name == "Symbol.hasInstance") + } || ancestor.fields.any { field -> + field.modifiers.isStatic && (field.name == "%computed" || field.name == "Symbol.hasInstance") + } + } + if (hasPotentialCustomHasInstance) { throw UnsupportedOperationException("Custom Symbol.hasInstance may override instanceof for $signature") } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt index 4d87959ea0..85cf0805ef 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -279,6 +279,8 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { fun `custom hasInstance is explicitly unsupported`() { val custom = analyze("customHasInstance") val inherited = analyze("inheritedHasInstance") + val customField = analyze(methodName = "customHasInstanceField") + val inheritedField = analyze(methodName = "inheritedHasInstanceField") assertEquals(TsAnalysisStopReason.EXHAUSTED, custom.stopReason) assertTrue(custom.states.isEmpty()) @@ -288,10 +290,22 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { assertTrue(inherited.states.isEmpty()) assertTrue(inherited.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${inherited.unsupportedPaths}") + assertEquals(TsAnalysisStopReason.EXHAUSTED, customField.stopReason) + assertTrue(customField.states.isEmpty()) + assertTrue(customField.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${customField.unsupportedPaths}") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, inheritedField.stopReason) + assertTrue(inheritedField.states.isEmpty()) + assertTrue(inheritedField.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${inheritedField.unsupportedPaths}") + replay(listOf( "if (new RuntimeInstanceof().customHasInstance() !== false) throw Error('custom hasInstance');", "if (new RuntimeInstanceof().inheritedHasInstance(new InstanceHasInstanceChild()) !== false) " + "throw Error('inherited hasInstance');", + "if (new RuntimeInstanceof().customHasInstanceField() !== false) " + + "throw Error('field hasInstance');", + "if (new RuntimeInstanceof().inheritedHasInstanceField(new InstanceHasInstanceFieldChild()) !== false) " + + "throw Error('inherited field hasInstance');", )) } diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts index 613f71f7bc..aa1f335e6a 100644 --- a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts +++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts @@ -135,6 +135,14 @@ class RuntimeInstanceof { return instance instanceof InstanceHasInstanceChild; } + customHasInstanceField(): boolean { + return new InstanceCustomField() instanceof InstanceCustomField; + } + + inheritedHasInstanceField(instance: InstanceHasInstanceFieldChild): boolean { + return instance instanceof InstanceHasInstanceFieldChild; + } + constructorParameter(ctor: typeof InstanceA): boolean { return new InstanceA() instanceof ctor; } @@ -229,3 +237,10 @@ class InstanceHasInstanceParent { } } class InstanceHasInstanceChild extends InstanceHasInstanceParent { hasInstanceChildMarker: number = 1; } +class InstanceCustomField { + static [Symbol.hasInstance] = (_value: unknown): boolean => false; +} +class InstanceHasInstanceFieldParent { + static [Symbol.hasInstance] = (_value: unknown): boolean => false; +} +class InstanceHasInstanceFieldChild extends InstanceHasInstanceFieldParent { hasInstanceFieldChildMarker: number = 1; } From 4a8d829ca06f34b25ac8d96230456f0cd5c05232 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 08:51:55 +0300 Subject: [PATCH 10/17] [TS] Reuse shared Node replay for instanceof tests --- .../samples/types/RuntimeInstanceofTest.kt | 22 ++++++++----------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt index 85cf0805ef..242f5fd6da 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -13,11 +13,10 @@ import org.usvm.machine.TsOptions import org.usvm.machine.state.TsMethodResult import org.usvm.util.TsMethodTestRunner import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay import org.usvm.util.getResourcePath import java.nio.file.Path -import java.util.concurrent.TimeUnit import kotlin.io.path.readText -import kotlin.io.path.writeText import kotlin.test.assertEquals import kotlin.test.assertIs import kotlin.test.assertTrue @@ -504,20 +503,17 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { } private fun replay(assertions: List) { - val script = directory.resolve("runtime-instanceof.ts") - val output = directory.resolve("runtime-instanceof.out") - script.writeText(buildString { + val source = buildString { appendLine(getResourcePath(tsPath).readText()) assertions.forEach(::appendLine) - }) - - val process = ProcessBuilder("node", "--experimental-strip-types", script.toString()) - .redirectErrorStream(true) - .redirectOutput(output.toFile()) - .start() + } - assertTrue(process.waitFor(30, TimeUnit.SECONDS), "Node replay timed out") - assertEquals(0, process.exitValue(), output.readText()) + assertNodeReplay( + source = source, + directory = directory, + name = "runtime-instanceof", + timeoutMessage = "Node replay timed out", + ) } private val machineOptions = UMachineOptions( From 40c5f18e46b480234b9cc081bed327c303954d55 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 4 Oct 2026 01:22:48 +0300 Subject: [PATCH 11/17] [TS] Check runtime instanceof results through discoverProperties --- .../samples/types/RuntimeInstanceofTest.kt | 61 ++++++++++++++++++- 1 file changed, 60 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt index 242f5fd6da..b02a29d870 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -33,6 +33,14 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { @Test fun `dynamic constructor value selects both outcomes`() { val method = getMethod(methodName = "dynamicConstructor", className = "RuntimeInstanceof") + + discoverProperties( + method = method, + { input, result -> input.value && result.number == 1.0 }, + { input, result -> !input.value && result.number == 0.0 }, + invariants = arrayOf({ input, result -> result.number == (if (input.value) 1.0 else 0.0) }), + ) + val outcome = analyze("dynamicConstructor") assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) @@ -55,6 +63,9 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { @Test fun `returned class value keeps constructor identity`() { val method = getMethod(methodName = "returnedConstructor", className = "RuntimeInstanceof") + + discoverConstant("returnedConstructor", expected = 1.0) + val outcome = analyze("returnedConstructor") assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) @@ -74,6 +85,14 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { @Test fun `typeof recognizes constructor values stored in a local`() { val method = getMethod(methodName = "aliasedClassTypeof", className = "RuntimeInstanceof") + + discoverProperties( + method = method, + { input, result -> input.value && result.number == 1.0 }, + { input, result -> !input.value && result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 1.0 }), + ) + val outcome = analyze("aliasedClassTypeof") assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) @@ -107,6 +126,9 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { expected.forEach { (methodName, expectedResult) -> val method = getMethod(methodName = methodName, className = "RuntimeInstanceof") + + discoverConstant(methodName, expected = expectedResult) + val outcome = analyze(methodName) assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) @@ -130,6 +152,9 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { methods.forEach { methodName -> val method = getMethod(methodName = methodName, className = "RuntimeInstanceof") + + discoverConstant(methodName, expected = 0.0) + val outcome = analyze(methodName) assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) @@ -150,6 +175,14 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { @Test fun `any receiver can contain an instance of the checked class`() { val method = getMethod(methodName = "anyLeft", className = "RuntimeInstanceof") + + discoverProperties( + method = method, + { _, result -> result.number == 0.0 }, + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 0.0 || result.number == 1.0 }), + ) + val outcome = analyze("anyLeft") assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) @@ -189,6 +222,17 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { methods.forEach { methodName -> val method = getMethod(methodName = methodName, className = "RuntimeInstanceof") + if (methodName == "constructorAliasLeft") { + discoverProperties( + method = method, + { input, result -> input.value && result.number == 0.0 }, + { input, result -> !input.value && result.number == 0.0 }, + invariants = arrayOf({ _, result -> result.number == 0.0 }), + ) + } else { + discoverConstant(methodName, expected = 0.0) + } + val outcome = analyze(methodName) assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) @@ -221,6 +265,13 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { @Test fun `subclass instance belongs to declared parent constructor`() { val method = getMethod(methodName = "inheritedConstructor", className = "RuntimeInstanceof") + + discoverProperties( + method = method, + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 1.0 }), + ) + val outcome = analyze("inheritedConstructor") assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) @@ -470,7 +521,7 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { } @Test - fun `concrete inherited number field remains supported`() { + fun `concrete inherited number input is not excluded by the constructor guard`() { val outcome = analyze("inheritedConcreteNumberParameter") assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) @@ -498,6 +549,14 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { outcome.states.forEach { state -> assertIs(state.methodResult) } } + private fun discoverConstant(methodName: String, expected: Double) { + discoverProperties( + method = getMethod(methodName = methodName, className = "RuntimeInstanceof"), + { result -> result.number == expected }, + invariants = arrayOf({ result -> result.number == expected }), + ) + } + private fun analyze(methodName: String) = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> machine.analyzeWithOutcome(methods = listOf(getMethod(methodName = methodName, className = "RuntimeInstanceof"))) } From 161b3fd101f614784200bda29204695d03d26253 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 11 Oct 2026 20:25:28 +0300 Subject: [PATCH 12/17] [TS] Integrate runtime instanceof with current interpreter --- usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt | 2 -- .../kotlin/org/usvm/machine/expr/TsExprResolver.kt | 6 ++++-- .../org/usvm/samples/types/RuntimeInstanceofTest.kt | 9 +++++++++ .../test/resources/samples/types/RuntimeInstanceof.ts | 10 ++++++++++ 4 files changed, 23 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index a394c69d8f..fa079747fe 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -102,8 +102,6 @@ class TsContext( fun classConstructorSignature(ref: UConcreteHeapRef): EtsClassSignature? = constructorSignatures[ref] - fun classConstructorRefs(): Collection = classConstructorRefs.values - /** * Reverse mapping from heap references to their original string constant values. * This is used during test resolution to retrieve the actual string content when diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 87dc9f14a1..875769f8d7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -130,8 +130,8 @@ import org.usvm.machine.state.newStmt import org.usvm.machine.types.EtsNominalType import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.sizeSort -import org.usvm.types.singleOrNull import org.usvm.types.TypesResult +import org.usvm.types.singleOrNull import org.usvm.util.EtsHierarchy import org.usvm.util.SymbolResolutionResult import org.usvm.util.arrayStorageType @@ -485,9 +485,11 @@ class TsExprResolver( } val functionValue = mkStringConstant("function", scope) + val isClassConstructor = ref is UConcreteHeapRef && classConstructorSignature(ref) != null + if (isClassConstructor) return functionValue + val isKnownFunction = scope.calcOnState { ref is UConcreteHeapRef && ( - classConstructorSignature(ref) != null || associatedFunction[ref] != null || memory.types.getTypeStream(ref).singleOrNull() is EtsFunctionType ) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt index b02a29d870..6c7a94c623 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -325,6 +325,15 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { }) } + @Test + fun `non callable RHS TypeError reaches the catch block`() { + discoverConstant(methodName = "caughtNonCallableRight", expected = 1.0) + + replay(listOf( + "if (new RuntimeInstanceof().caughtNonCallableRight() !== 1) throw Error('caught TypeError');" + )) + } + @Test fun `custom hasInstance is explicitly unsupported`() { val custom = analyze("customHasInstance") diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts index aa1f335e6a..bb68ea27a0 100644 --- a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts +++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts @@ -93,6 +93,16 @@ class RuntimeInstanceof { return new InstanceA() instanceof ctor; } + caughtNonCallableRight(): number { + try { + const ctor: any = 42; + new InstanceA() instanceof ctor; + return 0; + } catch { + return 1; + } + } + booleanRight(): boolean { const ctor: any = true; return new InstanceA() instanceof ctor; From 35f9e1a163ffc623871a08b1899712bc8348b72e Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 15:02:55 +0300 Subject: [PATCH 13/17] [TS] Support SDK prototype identities and clarify constructor checks --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 169 +---------------- .../kotlin/org/usvm/machine/TsRuntimeSdk.kt | 50 +++++ .../org/usvm/machine/expr/TsExprResolver.kt | 115 +++++++----- .../org/usvm/machine/types/EtsNominalType.kt | 5 + .../machine/types/TsConstructorInputGuard.kt | 176 ++++++++++++++++++ .../main/kotlin/org/usvm/util/EtsHierarchy.kt | 2 +- .../types/RuntimeBuiltinInstanceofTest.kt | 81 ++++++++ .../samples/types/RuntimeSdkInstanceofTest.kt | 57 ++++++ .../samples/types/RuntimeBuiltinInstanceof.ts | 38 ++++ .../samples/types/RuntimeSdkClasses.ts | 4 + .../samples/types/RuntimeSdkInstanceof.ts | 8 + 11 files changed, 502 insertions(+), 203 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/types/TsConstructorInputGuard.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeBuiltinInstanceofTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeSdkInstanceofTest.kt create mode 100644 usvm-ts/src/test/resources/samples/types/RuntimeBuiltinInstanceof.ts create mode 100644 usvm-ts/src/test/resources/samples/types/RuntimeSdkClasses.ts create mode 100644 usvm-ts/src/test/resources/samples/types/RuntimeSdkInstanceof.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 da08c28390..b7aeaf2032 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -1,22 +1,9 @@ package org.usvm.machine import mu.KotlinLogging -import org.jacodb.ets.model.EtsAliasType -import org.jacodb.ets.model.EtsArrayType -import org.jacodb.ets.model.EtsClass -import org.jacodb.ets.model.EtsClassSignature -import org.jacodb.ets.model.EtsClassType -import org.jacodb.ets.model.EtsClassValueType -import org.jacodb.ets.model.EtsFileSignature -import org.jacodb.ets.model.EtsGenericType -import org.jacodb.ets.model.EtsIntersectionType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStmt -import org.jacodb.ets.model.EtsTupleType -import org.jacodb.ets.model.EtsType -import org.jacodb.ets.model.EtsUnclearRefType -import org.jacodb.ets.model.EtsUnionType import org.usvm.CoverageZone import org.usvm.StateCollectionStrategy import org.usvm.UMachine @@ -30,6 +17,7 @@ import org.usvm.machine.call.deduplicateEtsFilesBySignature 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.TsTypeSystem import org.usvm.ps.createPathSelector import org.usvm.statistics.CompositeUMachineObserver @@ -93,13 +81,14 @@ class TsMachine( ) } ?: scene - private val graph = TsGraph(analysisScene) - private val typeSystem = TsTypeSystem(analysisScene, typeOperationsTimeout = 1.seconds, graph.hierarchy) + 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 ctx = TsContext( - scene = analysisScene, + scene = runtimeScene, components = components, - applicationAndSdkClasses = scene.projectAndSdkClasses, + applicationAndSdkClasses = runtimeScene.projectAndSdkClasses, ) private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher( models = requireNotNull(resolvedUnknownCallModels), @@ -262,18 +251,12 @@ class TsMachine( ): Pair, MutableSet> { val initialStates = mutableMapOf() val unsupportedPaths = mutableSetOf() - val classesBySignature = analysisScene.projectAndSdkClasses.associateBy { it.signature } + val constructorInputs = TsConstructorInputGuard(runtimeScene) methods.forEach { method -> - val genericParameters = method.typeParameters.filterIsInstance().associateBy { it.typeName } - val unsupportedParameter = method.parameters.firstNotNullOfOrNull { parameter -> - val gap = parameter.type.constructorInputGap(genericParameters, classesBySignature) - gap?.let { parameter to it } - } - if (unsupportedParameter != null) { - val (parameter, gap) = unsupportedParameter - unsupportedPaths += "${gap.description} '${parameter.name}' " + - "in ${method.humanReadableSignature} is not modeled" + val unsupportedReason = constructorInputs.unsupportedReason(method) + if (unsupportedReason != null) { + unsupportedPaths += unsupportedReason } else { initialStates[method] = interpreter.getInitialState(method, targets) } @@ -286,135 +269,3 @@ class TsMachine( components.close() } } - -private enum class ConstructorInputGap(val description: String) { - CONSTRUCTOR_VALUE("Constructor-typed parameter"), - UNRESOLVED_INHERITED_GENERIC("Unresolved inherited generic field in parameter"), -} - -private fun EtsType.constructorInputGap( - genericParameters: Map, - classesBySignature: Map, - visitedGenerics: Set = emptySet(), - visitedClasses: Set = emptySet(), -): ConstructorInputGap? = when (this) { - is EtsClassValueType -> ConstructorInputGap.CONSTRUCTOR_VALUE - is EtsUnionType -> types.firstNotNullOfOrNull { - it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) - } - is EtsIntersectionType -> types.firstNotNullOfOrNull { - it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) - } - is EtsTupleType -> types.firstNotNullOfOrNull { - it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) - } - is EtsArrayType -> elementType.constructorInputGap( - genericParameters, - classesBySignature, - visitedGenerics, - visitedClasses, - ) - is EtsClassType -> constructorInputGapInClass( - genericParameters, - classesBySignature, - visitedGenerics, - visitedClasses, - ) - is EtsUnclearRefType -> typeParameters.firstNotNullOfOrNull { - it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) - } - is EtsAliasType -> originalType.constructorInputGap( - genericParameters, - classesBySignature, - visitedGenerics, - visitedClasses, - ) - is EtsGenericType -> { - if (typeName in visitedGenerics) { - null - } else { - val declaration = genericParameters[typeName] - listOfNotNull(constraint, defaultType, declaration?.constraint, declaration?.defaultType) - .firstNotNullOfOrNull { - it.constructorInputGap( - genericParameters, - classesBySignature, - visitedGenerics + typeName, - visitedClasses, - ) - } - } - } - else -> null -} - -private fun EtsClassType.constructorInputGapInClass( - genericParameters: Map, - classesBySignature: Map, - visitedGenerics: Set, - visitedClasses: Set, -): ConstructorInputGap? { - val typeArgumentGap = typeParameters.firstNotNullOfOrNull { - it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) - } - if (typeArgumentGap != null) { - return typeArgumentGap - } - - if (signature in visitedClasses) { - return null - } - - val clazz = classesBySignature[signature] ?: return null - val nextVisitedClasses = visitedClasses + signature - val fieldGap = clazz.fields.firstNotNullOfOrNull { field -> - if (field.modifiers.isStatic) return@firstNotNullOfOrNull null - - field.type.constructorInputGap( - genericParameters, - classesBySignature, - visitedGenerics, - nextVisitedClasses, - ) - } - if (fieldGap != null) { - return fieldGap - } - - val superClass = clazz.superClass ?: return null - val superClasses = if (superClass.file == EtsFileSignature.UNKNOWN) { - classesBySignature.values.filter { it.name == superClass.name } - } else { - listOfNotNull(classesBySignature[superClass]) - } - - return superClasses.firstNotNullOfOrNull { parent -> - val parentGap = EtsClassType(parent.signature).constructorInputGap( - genericParameters, - classesBySignature, - visitedGenerics, - nextVisitedClasses, - ) - if (parentGap != null) return@firstNotNullOfOrNull parentGap - - // The frontend omits extends type arguments, so an inherited T may contain a constructor. - val parentGenerics = parent.typeParameters.filterIsInstance() - .mapTo(mutableSetOf()) { it.typeName } - val unresolvedGenericField = parent.fields.any { field -> - !field.modifiers.isStatic && field.type.containsGeneric(parentGenerics) - } - if (unresolvedGenericField) ConstructorInputGap.UNRESOLVED_INHERITED_GENERIC else null - } -} - -private fun EtsType.containsGeneric(names: Set): Boolean = when (this) { - is EtsGenericType -> typeName in names - is EtsUnionType -> types.any { it.containsGeneric(names) } - is EtsIntersectionType -> types.any { it.containsGeneric(names) } - is EtsTupleType -> types.any { it.containsGeneric(names) } - is EtsArrayType -> elementType.containsGeneric(names) - is EtsClassType -> typeParameters.any { it.containsGeneric(names) } - is EtsUnclearRefType -> typeParameters.any { it.containsGeneric(names) } - is EtsAliasType -> originalType.containsGeneric(names) - else -> false -} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt new file mode 100644 index 0000000000..750211116c --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt @@ -0,0 +1,50 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassCategory +import org.jacodb.ets.model.EtsClassImpl +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsScene +import org.usvm.util.EtsHierarchy + +private val runtimeSdkFile = EtsHierarchy.OBJECT_CLASS.signature.file + +/** + * Minimal prototype identities for the standard Object, Function and Array constructors. + * These declarations support runtime membership checks, not execution of their standard-library APIs. + * Preserve explicitly loaded SDK declarations; add only the missing core identities. Identity-only declarations + * are interfaces so the input generator does not invent ordinary instances for functions and arrays, which use + * their existing dedicated runtime representations. + */ +internal fun EtsScene.withCoreRuntimeSdk(): EtsScene { + val objectSignature = sdkClasses.singleOrNull { it.name == "Object" }?.signature + ?: EtsHierarchy.OBJECT_CLASS.signature + val missingClasses = listOf("Object", "Function", "Array") + .filter { name -> sdkClasses.none { it.name == name } } + .map { name -> + EtsClassImpl( + signature = EtsClassSignature(name = name, file = runtimeSdkFile), + fields = emptyList(), + methods = emptyList(), + category = EtsClassCategory.INTERFACE, + superClass = if (name == "Object") null else objectSignature, + ) + } + if (missingClasses.isEmpty()) return this + + val coreSdk = EtsFile(signature = runtimeSdkFile, classes = missingClasses, namespaces = emptyList()) + return EtsScene(projectFiles = projectFiles, sdkFiles = sdkFiles + coreSdk, projectName = projectName) +} + +/** An undeclared frontend local denotes a standard-library constructor, rather than a project binding. */ +internal fun EtsScene.sdkConstructorForGlobal(local: EtsLocal): EtsClass? = + sdkClasses.singleOrNull { it.name == local.name } + +internal fun EtsScene.runtimeFunctionType(): EtsClassType { + val functionClass = sdkClasses.singleOrNull { it.name == "Function" } + ?: throw UnsupportedOperationException("SDK Function identity is ambiguous or unavailable") + return EtsClassType(functionClass.signature) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 875769f8d7..a17a381b19 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -123,6 +123,8 @@ import org.usvm.machine.interpreter.markResolved import org.usvm.machine.interpreter.setResolvedValue import org.usvm.machine.operator.TsBinaryOperator import org.usvm.machine.operator.TsUnaryOperator +import org.usvm.machine.runtimeFunctionType +import org.usvm.machine.sdkConstructorForGlobal import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.lastStmt import org.usvm.machine.state.localsCount @@ -130,7 +132,6 @@ import org.usvm.machine.state.newStmt import org.usvm.machine.types.EtsNominalType import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.sizeSort -import org.usvm.types.TypesResult import org.usvm.types.singleOrNull import org.usvm.util.EtsHierarchy import org.usvm.util.SymbolResolutionResult @@ -1173,19 +1174,14 @@ class TsExprResolver( expr.checkType as? EtsRefType ?: return falseExpr } else { - resolveInstanceofConstructor(checkValue) ?: return null + resolveRuntimeConstructor(checkValue, operation = RuntimeConstructorOperation.INSTANCEOF) ?: return null } if (arg.sort != addressSort || arg == mkUndefinedValue() || arg == mkTsNullValue()) return falseExpr - if (arg is UConcreteHeapRef && classConstructorSignature(arg) != null) { - if (checkType is EtsClassType && scene.projectClasses.any { it.signature == checkType.signature }) { - return falseExpr - } - - throw UnsupportedOperationException( - "instanceof on a class constructor against an SDK or unknown class is not modeled" + val isFunctionObject = arg is UConcreteHeapRef && ( + classConstructorSignature(arg) != null || scope.calcOnState { associatedFunction[arg] != null } ) - } + if (isFunctionObject) return runtimeInstanceof(scene.runtimeFunctionType(), checkType) if (arg.isFakeObject()) { val fakeType = arg.getFakeType(scope) @@ -1196,45 +1192,60 @@ class TsExprResolver( return mkAnd( fakeType.refTypeExpr, - mkHeapRefEq(refValue, mkTsNullValue()).not(), - mkHeapRefEq(refValue, mkUndefinedValue()).not(), + mkNotNullOrUndefined(refValue), isInstance, ) } val objectRef = arg.asExpr(addressSort) if (isAllocatedConcreteHeapRef(objectRef) && checkType is EtsClassType) { - val objectTypes = scope.calcOnState { memory.typeStreamOf(objectRef).take(2) } - val objectType = (objectTypes as? TypesResult.SuccessfulTypesResult)?.types?.singleOrNull() as? EtsClassType - if (objectType != null) { - val objectClass = hierarchy.classesForType(objectType).singleOrNull() - ?: throw UnsupportedOperationException("Unknown instanceof receiver class: $objectType") - val constructorClass = hierarchy.classesForType(checkType).singleOrNull() - ?: throw UnsupportedOperationException("Unknown instanceof constructor class: $checkType") - return mkBool(constructorClass in hierarchy.getAncestors(objectClass)) - } + // allocConcrete records one runtime type, even when the frontend local has a union type. + // The stream utility keeps absent, ambiguous or timed-out identities unresolved instead of choosing one. + val objectType = scope.calcOnState { memory.typeStreamOf(objectRef).singleOrNull() } as? EtsClassType + if (objectType != null) return runtimeInstanceof(objectType, checkType) } - scope.calcOnState { memory.types.evalIsSubtype(objectRef, EtsNominalType(checkType)) } + val isInstance = scope.calcOnState { memory.types.evalIsSubtype(objectRef, EtsNominalType(checkType)) } + mkAnd(mkNotNullOrUndefined(objectRef), isInstance) + } + + private fun runtimeInstanceof(objectType: EtsRefType, checkType: EtsRefType): UExpr = with(ctx) { + val objectClass = hierarchy.classesForType(objectType).singleOrNull() + ?: throw UnsupportedOperationException("Unknown instanceof receiver class: $objectType") + val constructorClass = hierarchy.classesForType(checkType).singleOrNull() + ?: throw UnsupportedOperationException("Unknown instanceof constructor class: $checkType") + mkBool(constructorClass in hierarchy.getAncestors(objectClass)) } - private fun resolveInstanceofConstructor(checkValue: EtsEntity): EtsClassType? = with(ctx) { - val constructor = resolve(checkValue) ?: return null - if (constructor.sort == fp64Sort || constructor.sort == boolSort) return throwInstanceofTypeError() - if (constructor == mkTsNullValue() || constructor == mkUndefinedValue()) return throwInstanceofTypeError() + /** + * Resolve the evaluated identity once. `instanceof` can invoke a custom Symbol.hasInstance on its RHS, + * whereas `new` requires [[Construct]]; an ordinary object with that symbol is still not constructable. + */ + private fun resolveRuntimeConstructor( + value: EtsEntity, + operation: RuntimeConstructorOperation, + ): EtsClassType? = with(ctx) { + val constructor = resolve(value) ?: return null + if (constructor.sort == fp64Sort || constructor.sort == boolSort) return throwTypeError() + if (constructor == mkTsNullValue() || constructor == mkUndefinedValue()) return throwTypeError() if (constructor.sort != addressSort || constructor.isFakeObject()) { - throw UnsupportedOperationException("Unresolved instanceof RHS callability is not modeled") + val target = if (operation == RuntimeConstructorOperation.INSTANCEOF) { + "instanceof RHS" + } else { + "new constructor" + } + throw UnsupportedOperationException("Unresolved $target callability is not modeled") } val constructorRef = constructor as? UConcreteHeapRef - ?: throw UnsupportedOperationException("Symbolic instanceof constructor identity is not modeled") - if (getStringConstantValue(constructorRef) != null) return throwInstanceofTypeError() + ?: throw UnsupportedOperationException("Symbolic ${operation.operator} constructor identity is not modeled") + if (getStringConstantValue(constructorRef) != null) return throwTypeError() val signature = classConstructorSignature(constructorRef) - ?: return resolveNonConstructorInstanceofRight(constructorRef) - val clazz = scene.projectAndSdkClasses.singleOrNull { it.signature == signature } - ?: throw UnsupportedOperationException("Unknown instanceof class: $signature") + ?: return rejectNonConstructorValue(constructorRef, operation) + val clazz = hierarchy.classesForType(EtsClassType(signature)).singleOrNull() + ?: throw UnsupportedOperationException("Unknown or ambiguous ${operation.operator} class: $signature") val hasPotentialCustomHasInstance = hierarchy.getAncestors(clazz).any { ancestor -> ancestor.methods.any { method -> method.modifiers.isStatic && (method.name == "%computed" || method.name == "Symbol.hasInstance") @@ -1242,24 +1253,28 @@ class TsExprResolver( field.modifiers.isStatic && (field.name == "%computed" || field.name == "Symbol.hasInstance") } } - if (hasPotentialCustomHasInstance) { + val hasUnsupportedInstanceOverride = operation == RuntimeConstructorOperation.INSTANCEOF && + hasPotentialCustomHasInstance + if (hasUnsupportedInstanceOverride) { throw UnsupportedOperationException("Custom Symbol.hasInstance may override instanceof for $signature") } - EtsClassType(signature) + EtsClassType(clazz.signature) } - private fun resolveNonConstructorInstanceofRight(ref: UConcreteHeapRef): Nothing? = with(ctx) { - val objectTypes = if (isAllocatedConcreteHeapRef(ref)) { - scope.calcOnState { memory.typeStreamOf(ref).take(n = 2) } + private fun rejectNonConstructorValue( + ref: UConcreteHeapRef, + operation: RuntimeConstructorOperation, + ): Nothing? = with(ctx) { + val objectType = if (isAllocatedConcreteHeapRef(ref)) { + scope.calcOnState { memory.typeStreamOf(ref).singleOrNull() } } else { null } - val objectType = (objectTypes as? TypesResult.SuccessfulTypesResult)?.types?.singleOrNull() - if (objectType == EtsStringType) return throwInstanceofTypeError() + if (objectType == EtsStringType) return throwTypeError() val objectClass = (objectType as? EtsClassType)?.let { type -> - scene.projectClasses.singleOrNull { it.signature == type.signature } + hierarchy.classesForType(type).singleOrNull() } if (objectClass != null) { // Computed members may include Symbol.hasInstance, so their instances need a separate model. @@ -1271,13 +1286,15 @@ class TsExprResolver( } val isFunction = scope.calcOnState { associatedFunction[ref] != null } - if (ordinaryObject && !hasComputedMember && !isFunction) return throwInstanceofTypeError() + val mayHandleInstanceof = operation == RuntimeConstructorOperation.INSTANCEOF && hasComputedMember + val isKnownNonConstructor = ordinaryObject && !mayHandleInstanceof && !isFunction + if (isKnownNonConstructor) return throwTypeError() } - throw UnsupportedOperationException("Unknown instanceof constructor value: $ref") + throw UnsupportedOperationException("Unknown ${operation.operator} constructor value: $ref") } - private fun throwInstanceofTypeError(): Nothing? { + private fun throwTypeError(): Nothing? { scope.doWithState { val exception = memory.allocConcrete(TS_TYPE_ERROR_TYPE) methodResult = TsMethodResult.TsException(exception, TS_TYPE_ERROR_TYPE) @@ -1709,6 +1726,12 @@ class TsSimpleValueResolver( val currentMethod = scope.calcOnState { lastEnteredMethod } if (local !in currentMethod.getDeclaredLocals()) { + val isParameter = currentMethod.parameters.any { it.name == local.name } + if (!isParameter && local.type is EtsFunctionType) { + val sdkConstructor = ctx.scene.sdkConstructorForGlobal(local) + if (sdkConstructor != null) return ctx.classConstructorRef(sdkConstructor.signature) + } + if (local.type is EtsFunctionType) { // TODO: function pointers should be "singletons" return scope.calcOnState { memory.allocConcrete(local.type) } @@ -1777,3 +1800,9 @@ class TsSimpleValueResolver( error("Should not be called") } } + +/** The RHS protocols differ: instanceof uses @@hasInstance, while new requires [[Construct]]. */ +private enum class RuntimeConstructorOperation(val operator: String) { + INSTANCEOF(operator = "instanceof"), + NEW(operator = "new"), +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsNominalType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsNominalType.kt index 22505c64b7..7d52ee868f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsNominalType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsNominalType.kt @@ -3,6 +3,11 @@ package org.usvm.machine.types import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsType +/** + * Runtime membership in the declared class hierarchy, rather than TypeScript structural assignability. + * For example, unrelated classes A and B can have identical fields but `new A() instanceof B` is false. + * This wrapper prevents field-shape constraints from being used as JavaScript prototype-chain checks. + */ internal data class EtsNominalType(val type: EtsRefType) : EtsType { override val typeName: String get() = "NominalType $type" diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsConstructorInputGuard.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsConstructorInputGuard.kt new file mode 100644 index 0000000000..bcf29d5ca5 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsConstructorInputGuard.kt @@ -0,0 +1,176 @@ +package org.usvm.machine.types + +import org.jacodb.ets.model.EtsAliasType +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsClassValueType +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsGenericType +import org.jacodb.ets.model.EtsIntersectionType +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsTupleType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsUnionType +import org.usvm.util.humanReadableSignature + +/** + * Rejects input shapes for which we cannot generate a faithful constructor-valued witness. + * + * A class constructor is a function object, not an instance of that class. The current input generator would + * materialize constructor-typed values as ordinary instances and lose their callable identity. Inspect nested + * parameter types and instance fields before starting analysis so that this gap has an explicit unsupported outcome. + * This is an entrypoint-wide bound: an unsupported field excludes the method even if its body does not read it. + */ +internal class TsConstructorInputGuard(scene: EtsScene) { + private val classesBySignature = scene.projectAndSdkClasses.associateBy { it.signature } + + fun unsupportedReason(method: EtsMethod): String? { + val genericParameters = method.typeParameters.filterIsInstance().associateBy { it.typeName } + val unsupportedParameter = method.parameters.firstNotNullOfOrNull { parameter -> + val gap = parameter.type.constructorInputGap(genericParameters, classesBySignature) + gap?.let { parameter to it } + } ?: return null + val (parameter, gap) = unsupportedParameter + + return "${gap.description} '${parameter.name}' in ${method.humanReadableSignature} is not modeled" + } +} + +private enum class ConstructorInputGap(val description: String) { + CONSTRUCTOR_VALUE("Constructor-typed parameter"), + UNRESOLVED_INHERITED_GENERIC("Unresolved inherited generic field in parameter"), +} + +// Visited sets describe the current traversal path, so recursive classes and generic constraints terminate +// without hiding a constructor-valued sibling field. Static fields do not belong to an input object's payload. +private fun EtsType.constructorInputGap( + genericParameters: Map, + classesBySignature: Map, + visitedGenerics: Set = emptySet(), + visitedClasses: Set = emptySet(), +): ConstructorInputGap? = when (this) { + is EtsClassValueType -> ConstructorInputGap.CONSTRUCTOR_VALUE + is EtsUnionType -> types.firstNotNullOfOrNull { + it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + } + is EtsIntersectionType -> types.firstNotNullOfOrNull { + it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + } + is EtsTupleType -> types.firstNotNullOfOrNull { + it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + } + is EtsArrayType -> elementType.constructorInputGap( + genericParameters, + classesBySignature, + visitedGenerics, + visitedClasses, + ) + is EtsClassType -> constructorInputGapInClass( + genericParameters, + classesBySignature, + visitedGenerics, + visitedClasses, + ) + is EtsUnclearRefType -> typeParameters.firstNotNullOfOrNull { + it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + } + is EtsAliasType -> originalType.constructorInputGap( + genericParameters, + classesBySignature, + visitedGenerics, + visitedClasses, + ) + is EtsGenericType -> { + if (typeName in visitedGenerics) { + null + } else { + val declaration = genericParameters[typeName] + listOfNotNull(constraint, defaultType, declaration?.constraint, declaration?.defaultType) + .firstNotNullOfOrNull { + it.constructorInputGap( + genericParameters, + classesBySignature, + visitedGenerics + typeName, + visitedClasses, + ) + } + } + } + else -> null +} + +private fun EtsClassType.constructorInputGapInClass( + genericParameters: Map, + classesBySignature: Map, + visitedGenerics: Set, + visitedClasses: Set, +): ConstructorInputGap? { + val typeArgumentGap = typeParameters.firstNotNullOfOrNull { + it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) + } + if (typeArgumentGap != null) { + return typeArgumentGap + } + + if (signature in visitedClasses) { + return null + } + + val clazz = classesBySignature[signature] ?: return null + val nextVisitedClasses = visitedClasses + signature + val fieldGap = clazz.fields.firstNotNullOfOrNull { field -> + if (field.modifiers.isStatic) return@firstNotNullOfOrNull null + + field.type.constructorInputGap( + genericParameters, + classesBySignature, + visitedGenerics, + nextVisitedClasses, + ) + } + if (fieldGap != null) { + return fieldGap + } + + val superClass = clazz.superClass ?: return null + val superClasses = if (superClass.file == EtsFileSignature.UNKNOWN) { + classesBySignature.values.filter { it.name == superClass.name } + } else { + listOfNotNull(classesBySignature[superClass]) + } + + return superClasses.firstNotNullOfOrNull { parent -> + val parentGap = EtsClassType(parent.signature).constructorInputGap( + genericParameters, + classesBySignature, + visitedGenerics, + nextVisitedClasses, + ) + if (parentGap != null) return@firstNotNullOfOrNull parentGap + + // The frontend omits extends type arguments. Even an apparent numeric specialization may hide a + // constructor in an inherited T, so reject this shape until superclass arguments are available. + val parentGenerics = parent.typeParameters.filterIsInstance() + .mapTo(mutableSetOf()) { it.typeName } + val unresolvedGenericField = parent.fields.any { field -> + !field.modifiers.isStatic && field.type.containsGeneric(parentGenerics) + } + if (unresolvedGenericField) ConstructorInputGap.UNRESOLVED_INHERITED_GENERIC else null + } +} + +private fun EtsType.containsGeneric(names: Set): Boolean = when (this) { + is EtsGenericType -> typeName in names + is EtsUnionType -> types.any { it.containsGeneric(names) } + is EtsIntersectionType -> types.any { it.containsGeneric(names) } + is EtsTupleType -> types.any { it.containsGeneric(names) } + is EtsArrayType -> elementType.containsGeneric(names) + is EtsClassType -> typeParameters.any { it.containsGeneric(names) } + is EtsUnclearRefType -> typeParameters.any { it.containsGeneric(names) } + is EtsAliasType -> originalType.containsGeneric(names) + else -> false +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index 813957d1aa..87dc00d4f0 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -45,7 +45,7 @@ class EtsHierarchy(private val scene: EtsScene) { } result.takeIf { it.isNotEmpty() } - }.flatten().toMutableSet() + classesForType(OBJECT_CLASS) + }.flatten().toMutableSet() + scene.sdkClasses.filter { it.name == "Object" } } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeBuiltinInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeBuiltinInstanceofTest.kt new file mode 100644 index 0000000000..363c89ea4e --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeBuiltinInstanceofTest.kt @@ -0,0 +1,81 @@ +package org.usvm.samples.types + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText + +class RuntimeBuiltinInstanceofTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val tsPath = "/samples/types/RuntimeBuiltinInstanceof.ts" + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `core SDK prototype identities match JavaScript membership`() { + val expected = mapOf( + "constructorObject" to 1.0, + "constructorFunction" to 1.0, + "constructorArray" to 0.0, + "sdkConstructorFunction" to 1.0, + "sdkConstructorObject" to 1.0, + "sdkConstructorArray" to 0.0, + "functionObject" to 1.0, + "functionFunction" to 1.0, + "functionProjectClass" to 0.0, + "instanceObject" to 1.0, + "instanceFunction" to 0.0, + "arrayObject" to 1.0, + "arrayArray" to 1.0, + "primitiveObject" to 0.0, + "nullObject" to 0.0, + "stringObject" to 0.0, + "localShadow" to 0.0, + "callParameterShadow" to 0.0, + ) + + expected.forEach { (methodName, result) -> + discoverProperties( + method = getMethod(methodName = methodName, className = "RuntimeBuiltinInstanceof"), + { value -> value.number == result }, + invariants = arrayOf({ value -> value.number == result }), + ) + } + + replay(expected.map { (methodName, result) -> + "if (new RuntimeBuiltinInstanceof().$methodName() !== ${result.toInt()}) throw Error('$methodName');" + }) + } + + @Test + fun `conditional SDK constructor preserves both selected identities`() { + discoverProperties( + method = getMethod(methodName = "conditionalBuiltin", className = "RuntimeBuiltinInstanceof"), + { input, result -> input.value && result.number == 1.0 }, + { input, result -> !input.value && result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 1.0 }), + ) + + replay(listOf( + "if (new RuntimeBuiltinInstanceof().conditionalBuiltin(true) !== 1) throw Error('Function alias');", + "if (new RuntimeBuiltinInstanceof().conditionalBuiltin(false) !== 1) throw Error('Object alias');" + )) + } + + private fun replay(assertions: List) { + val source = getResourcePath(tsPath).readText() + "\n" + assertions.joinToString(separator = "\n") + + assertNodeReplay( + source = source, + directory = directory, + name = "runtime-builtin-instanceof", + timeoutMessage = "Core SDK Node replay timed out", + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeSdkInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeSdkInstanceofTest.kt new file mode 100644 index 0000000000..e149afad44 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeSdkInstanceofTest.kt @@ -0,0 +1,57 @@ +package org.usvm.samples.types + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText + +class RuntimeSdkInstanceofTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val tsPath = "/samples/types/RuntimeSdkInstanceof.ts" + private val sdkPath = "/samples/types/RuntimeSdkClasses.ts" + override val scene: EtsScene = EtsScene( + projectFiles = listOf(loadEtsFileAutoConvert(getResourcePath(tsPath))), + sdkFiles = listOf(loadEtsFileAutoConvert(getResourcePath(sdkPath))), + ) + + @Test + fun `explicit SDK classes retain constructor and inherited instance identities`() { + val expected = mapOf("constructorObject" to 1.0, "constructorFunction" to 1.0, "constructorParent" to 0.0) + + expected.forEach { (methodName, result) -> + discoverProperties( + method = getMethod(methodName = methodName, className = "RuntimeSdkInstanceof"), + { value -> value.number == result }, + invariants = arrayOf({ value -> value.number == result }), + ) + } + + discoverProperties( + method = getMethod(methodName = "inherited", className = "RuntimeSdkInstanceof"), + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 1.0 }), + ) + + val sdkSource = getResourcePath(sdkPath).readText().replace("export class", "class") + val source = sdkSource + "\n" + getResourcePath(tsPath).readText().lineSequence() + .filterNot { it.startsWith("import ") }.joinToString(separator = "\n") + val assertions = expected.map { (methodName, result) -> + "if (new RuntimeSdkInstanceof().$methodName() !== ${result.toInt()}) throw Error('$methodName');" + } + "if (new RuntimeSdkInstanceof().inherited(new RuntimeSdkChild()) !== 1) throw Error('SDK inheritance');" + + assertNodeReplay( + source = source + "\n" + assertions.joinToString(separator = "\n"), + directory = directory, + name = "runtime-sdk-instanceof", + timeoutMessage = "Explicit SDK Node replay timed out", + ) + } +} diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeBuiltinInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeBuiltinInstanceof.ts new file mode 100644 index 0000000000..4c8574dc44 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/RuntimeBuiltinInstanceof.ts @@ -0,0 +1,38 @@ +class BuiltinProjectClass {} + +class RuntimeBuiltinInstanceof { + constructorObject(): number { return BuiltinProjectClass instanceof Object ? 1 : 0; } + constructorFunction(): number { return BuiltinProjectClass instanceof Function ? 1 : 0; } + constructorArray(): number { return BuiltinProjectClass instanceof Array ? 1 : 0; } + sdkConstructorFunction(): number { return Array instanceof Function ? 1 : 0; } + sdkConstructorObject(): number { return Function instanceof Object ? 1 : 0; } + sdkConstructorArray(): number { return Object instanceof Array ? 1 : 0; } + functionObject(): number { const fn = () => 1; return fn instanceof Object ? 1 : 0; } + functionFunction(): number { const fn = () => 1; return fn instanceof Function ? 1 : 0; } + functionProjectClass(): number { const fn = () => 1; return fn instanceof BuiltinProjectClass ? 1 : 0; } + instanceObject(): number { return new BuiltinProjectClass() instanceof Object ? 1 : 0; } + instanceFunction(): number { return new BuiltinProjectClass() instanceof Function ? 1 : 0; } + arrayObject(): number { return [] instanceof Object ? 1 : 0; } + arrayArray(): number { return [] instanceof Array ? 1 : 0; } + primitiveObject(): number { return 42 instanceof Object ? 1 : 0; } + nullObject(): number { return null instanceof Object ? 1 : 0; } + stringObject(): number { return "text" instanceof Object ? 1 : 0; } + + conditionalBuiltin(useFunction: boolean): number { + const ctor = useFunction ? Function : Object; + return BuiltinProjectClass instanceof ctor ? 1 : 0; + } + + localShadow(): number { + const Object = BuiltinProjectClass; + return BuiltinProjectClass instanceof Object ? 1 : 0; + } + + parameterShadow(Object: any): number { + return BuiltinProjectClass instanceof Object ? 1 : 0; + } + + callParameterShadow(): number { + return this.parameterShadow(BuiltinProjectClass); + } +} diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeSdkClasses.ts b/usvm-ts/src/test/resources/samples/types/RuntimeSdkClasses.ts new file mode 100644 index 0000000000..48cb61d653 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/RuntimeSdkClasses.ts @@ -0,0 +1,4 @@ +export class RuntimeSdkParent {} +export class RuntimeSdkChild extends RuntimeSdkParent { + sdkMarker: number = 1; +} diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeSdkInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeSdkInstanceof.ts new file mode 100644 index 0000000000..a013459edd --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/RuntimeSdkInstanceof.ts @@ -0,0 +1,8 @@ +import { RuntimeSdkParent, RuntimeSdkChild } from "./RuntimeSdkClasses"; + +class RuntimeSdkInstanceof { + constructorObject(): number { return RuntimeSdkChild instanceof Object ? 1 : 0; } + constructorFunction(): number { return RuntimeSdkChild instanceof Function ? 1 : 0; } + constructorParent(): number { return RuntimeSdkChild instanceof RuntimeSdkParent ? 1 : 0; } + inherited(value: RuntimeSdkChild): number { return value instanceof RuntimeSdkParent ? 1 : 0; } +} From 322c9b0551b58dd23f3de776891c0b92e8b074bf Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 15:40:37 +0300 Subject: [PATCH 14/17] [TS] Keep SDK prototypes out of witnesses and preserve boxed function identity --- .../kotlin/org/usvm/machine/TsRuntimeSdk.kt | 22 +++++++--- .../org/usvm/machine/expr/TsExprResolver.kt | 44 +++++++++++-------- .../org/usvm/machine/types/TsTypeSystem.kt | 3 +- .../usvm/machine/types/TsTypeSystemTest.kt | 30 +++++++++++++ .../types/RuntimeBuiltinInstanceofTest.kt | 23 ++++++++++ .../samples/types/RuntimeBuiltinInstanceof.ts | 20 +++++++++ 6 files changed, 116 insertions(+), 26 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt index 750211116c..d62c53db72 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt @@ -6,18 +6,23 @@ import org.jacodb.ets.model.EtsClassImpl import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsScene import org.usvm.util.EtsHierarchy private val runtimeSdkFile = EtsHierarchy.OBJECT_CLASS.signature.file +private val runtimePrototypeFile = EtsFileSignature(projectName = "usvm-runtime-sdk", fileName = "PrototypeIdentities") + +/** Synthetic Function and Array identities cannot be materialized as ordinary class instances. */ +internal fun EtsClassType.isCoreRuntimePrototypeIdentity(): Boolean = signature.file == runtimePrototypeFile /** * Minimal prototype identities for the standard Object, Function and Array constructors. * These declarations support runtime membership checks, not execution of their standard-library APIs. - * Preserve explicitly loaded SDK declarations; add only the missing core identities. Identity-only declarations - * are interfaces so the input generator does not invent ordinary instances for functions and arrays, which use - * their existing dedicated runtime representations. + * Preserve explicitly loaded SDK declarations; add only the missing core identities. Synthetic Function and Array + * declarations have a reserved signature and are excluded from instantiable type streams: functions and arrays + * use their existing dedicated runtime representations. Object remains an ordinary object input candidate. */ internal fun EtsScene.withCoreRuntimeSdk(): EtsScene { val objectSignature = sdkClasses.singleOrNull { it.name == "Object" }?.signature @@ -26,7 +31,10 @@ internal fun EtsScene.withCoreRuntimeSdk(): EtsScene { .filter { name -> sdkClasses.none { it.name == name } } .map { name -> EtsClassImpl( - signature = EtsClassSignature(name = name, file = runtimeSdkFile), + signature = EtsClassSignature( + name = name, + file = if (name == "Object") runtimeSdkFile else runtimePrototypeFile, + ), fields = emptyList(), methods = emptyList(), category = EtsClassCategory.INTERFACE, @@ -35,8 +43,10 @@ internal fun EtsScene.withCoreRuntimeSdk(): EtsScene { } if (missingClasses.isEmpty()) return this - val coreSdk = EtsFile(signature = runtimeSdkFile, classes = missingClasses, namespaces = emptyList()) - return EtsScene(projectFiles = projectFiles, sdkFiles = sdkFiles + coreSdk, projectName = projectName) + val coreSdkFiles = missingClasses.groupBy { it.signature.file }.map { (file, classes) -> + EtsFile(signature = file, classes = classes, namespaces = emptyList()) + } + return EtsScene(projectFiles = projectFiles, sdkFiles = sdkFiles + coreSdkFiles, projectName = projectName) } /** An undeclared frontend local denotes a standard-library constructor, rather than a project binding. */ diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index a17a381b19..894acb3c6a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -93,6 +93,7 @@ import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.NAMED_FUNCTION_REFERENCE_PREFIX import org.jacodb.ets.utils.getDeclaredLocals +import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef @@ -1178,38 +1179,43 @@ class TsExprResolver( } if (arg.sort != addressSort || arg == mkUndefinedValue() || arg == mkTsNullValue()) return falseExpr - val isFunctionObject = arg is UConcreteHeapRef && ( - classConstructorSignature(arg) != null || scope.calcOnState { associatedFunction[arg] != null } - ) - if (isFunctionObject) return runtimeInstanceof(scene.runtimeFunctionType(), checkType) - if (arg.isFakeObject()) { val fakeType = arg.getFakeType(scope) val refValue = arg.extractRef(scope) - val isInstance = scope.calcOnState { - memory.types.evalIsSubtype(refValue, EtsNominalType(checkType)) - } + val isInstance = referenceInstanceof(refValue, checkType) - return mkAnd( - fakeType.refTypeExpr, - mkNotNullOrUndefined(refValue), - isInstance, - ) + return mkAnd(fakeType.refTypeExpr, isInstance) } - val objectRef = arg.asExpr(addressSort) - if (isAllocatedConcreteHeapRef(objectRef) && checkType is EtsClassType) { + referenceInstanceof(arg.asExpr(addressSort), checkType) + } + + private fun referenceInstanceof(ref: UHeapRef, checkType: EtsRefType): UBoolExpr = with(ctx) { + if (ref == mkUndefinedValue() || ref == mkTsNullValue()) return falseExpr + if (ref is UIteExpr<*>) { + val trueValue = referenceInstanceof(ref.trueBranch.asExpr(addressSort), checkType) + val falseValue = referenceInstanceof(ref.falseBranch.asExpr(addressSort), checkType) + return mkIte(ref.condition, trueValue, falseValue) + } + + // Wrappers and conditional values retain the represented function's identity. + val isFunctionObject = ref is UConcreteHeapRef && ( + classConstructorSignature(ref) != null || scope.calcOnState { associatedFunction[ref] != null } + ) + if (isFunctionObject) return runtimeInstanceof(scene.runtimeFunctionType(), checkType) + + if (isAllocatedConcreteHeapRef(ref) && checkType is EtsClassType) { // allocConcrete records one runtime type, even when the frontend local has a union type. // The stream utility keeps absent, ambiguous or timed-out identities unresolved instead of choosing one. - val objectType = scope.calcOnState { memory.typeStreamOf(objectRef).singleOrNull() } as? EtsClassType + val objectType = scope.calcOnState { memory.typeStreamOf(ref).singleOrNull() } as? EtsClassType if (objectType != null) return runtimeInstanceof(objectType, checkType) } - val isInstance = scope.calcOnState { memory.types.evalIsSubtype(objectRef, EtsNominalType(checkType)) } - mkAnd(mkNotNullOrUndefined(objectRef), isInstance) + val isInstance = scope.calcOnState { memory.types.evalIsSubtype(ref, EtsNominalType(checkType)) } + mkAnd(mkNotNullOrUndefined(ref), isInstance) } - private fun runtimeInstanceof(objectType: EtsRefType, checkType: EtsRefType): UExpr = with(ctx) { + private fun runtimeInstanceof(objectType: EtsRefType, checkType: EtsRefType): UBoolExpr = with(ctx) { val objectClass = hierarchy.classesForType(objectType).singleOrNull() ?: throw UnsupportedOperationException("Unknown instanceof receiver class: $objectType") val constructorClass = hierarchy.classesForType(checkType).singleOrNull() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index b167374f86..e63b31039d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -25,6 +25,7 @@ import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsVoidType +import org.usvm.machine.isCoreRuntimePrototypeIdentity import org.usvm.types.USupportTypeStream import org.usvm.types.UTypeStream import org.usvm.types.UTypeSystem @@ -271,7 +272,7 @@ class TsTypeSystem( is EtsArrayType -> isInstantiable(t.elementType) // array if elements instantiable is EtsTupleType -> t.types.all { isInstantiable(it) } // tuple if each element instantiable is EtsFunctionType -> true // function literals always possible - is EtsClassType -> true // class instantiation possible + is EtsClassType -> !t.isCoreRuntimePrototypeIdentity() else -> false } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt index af2cb291a0..4489cf7433 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt @@ -17,6 +17,8 @@ import org.jacodb.ets.model.EtsTupleType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnknownType import org.junit.jupiter.api.Test +import org.usvm.machine.withCoreRuntimeSdk +import org.usvm.types.TypesResult import org.usvm.util.EtsHierarchy import org.usvm.util.type import kotlin.test.assertFalse @@ -47,6 +49,34 @@ class TsTypeSystemTest { nonObjects.forEach { assertFalse(typeSystem.isSupertype(EtsObjectType, it), it.typeName) } } + @Test + fun `core SDK prototype identities are not ordinary object witnesses`() { + val scene = EtsScene(projectFiles = emptyList()).withCoreRuntimeSdk() + val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, hierarchy = EtsHierarchy(scene)) + val prototypes = scene.sdkClasses.filter { it.name == "Function" || it.name == "Array" } + + assertTrue(typeSystem.isInstantiable(EtsHierarchy.OBJECT_CLASS)) + prototypes.forEach { assertFalse(typeSystem.isInstantiable(it.type), it.name) } + val result = typeSystem.topTypeStream().take(n = 20) as TypesResult.SuccessfulTypesResult + prototypes.forEach { assertFalse(it.type in result.types, it.name) } + } + + @Test + fun `core SDK bootstrap preserves explicitly loaded SDK declarations`() { + val fileSignature = EtsFileSignature(projectName = "sdk", fileName = "function.ts") + val functionClass = EtsClassImpl( + signature = EtsClassSignature(name = "Function", file = fileSignature), + fields = emptyList(), + methods = emptyList(), + ) + val file = EtsFile(signature = fileSignature, classes = listOf(functionClass), namespaces = emptyList()) + val scene = EtsScene(projectFiles = emptyList(), sdkFiles = listOf(file)).withCoreRuntimeSdk() + val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, hierarchy = EtsHierarchy(scene)) + + assertTrue(scene.sdkClasses.single { it.name == "Function" } === functionClass) + assertTrue(typeSystem.isInstantiable(functionClass.type)) + } + @Test fun `auxiliary type is a subtype of a class containing its properties`() { val fileSignature = EtsFileSignature(projectName = "test", fileName = "types.ts") diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeBuiltinInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeBuiltinInstanceofTest.kt index 363c89ea4e..41f3c26fc4 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeBuiltinInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeBuiltinInstanceofTest.kt @@ -29,6 +29,8 @@ class RuntimeBuiltinInstanceofTest : TsMethodTestRunner() { "functionObject" to 1.0, "functionFunction" to 1.0, "functionProjectClass" to 0.0, + "boxedConstructorFunction" to 1.0, + "boxedFunctionFunction" to 1.0, "instanceObject" to 1.0, "instanceFunction" to 0.0, "arrayObject" to 1.0, @@ -68,6 +70,27 @@ class RuntimeBuiltinInstanceofTest : TsMethodTestRunner() { )) } + @Test + fun `boxed conditional functions preserve runtime membership`() { + val methods = listOf("boxedConstructorChoice", "boxedFunctionChoice") + + methods.forEach { methodName -> + discoverProperties( + method = getMethod(methodName = methodName, className = "RuntimeBuiltinInstanceof"), + { input, result -> input.value && result.number == 1.0 }, + { input, result -> !input.value && result.number == 0.0 }, + invariants = arrayOf({ input, result -> result.number == if (input.value) 1.0 else 0.0 }), + ) + } + + replay(methods.flatMap { methodName -> + listOf( + "if (new RuntimeBuiltinInstanceof().$methodName(true) !== 1) throw Error('$methodName(true)');", + "if (new RuntimeBuiltinInstanceof().$methodName(false) !== 0) throw Error('$methodName(false)');", + ) + }) + } + private fun replay(assertions: List) { val source = getResourcePath(tsPath).readText() + "\n" + assertions.joinToString(separator = "\n") diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeBuiltinInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeBuiltinInstanceof.ts index 4c8574dc44..bb45ee1ee7 100644 --- a/usvm-ts/src/test/resources/samples/types/RuntimeBuiltinInstanceof.ts +++ b/usvm-ts/src/test/resources/samples/types/RuntimeBuiltinInstanceof.ts @@ -10,6 +10,16 @@ class RuntimeBuiltinInstanceof { functionObject(): number { const fn = () => 1; return fn instanceof Object ? 1 : 0; } functionFunction(): number { const fn = () => 1; return fn instanceof Function ? 1 : 0; } functionProjectClass(): number { const fn = () => 1; return fn instanceof BuiltinProjectClass ? 1 : 0; } + boxedConstructorFunction(): number { + const box: any = { value: BuiltinProjectClass }; + return box.value instanceof Function ? 1 : 0; + } + + boxedFunctionFunction(): number { + const box: any = { value: () => 1 }; + return box.value instanceof Function ? 1 : 0; + } + instanceObject(): number { return new BuiltinProjectClass() instanceof Object ? 1 : 0; } instanceFunction(): number { return new BuiltinProjectClass() instanceof Function ? 1 : 0; } arrayObject(): number { return [] instanceof Object ? 1 : 0; } @@ -23,6 +33,16 @@ class RuntimeBuiltinInstanceof { return BuiltinProjectClass instanceof ctor ? 1 : 0; } + boxedConstructorChoice(useFunction: boolean): number { + const box: any = { value: useFunction ? BuiltinProjectClass : 42 }; + return box.value instanceof Function ? 1 : 0; + } + + boxedFunctionChoice(useFunction: boolean): number { + const box: any = { value: useFunction ? (() => 1) : 42 }; + return box.value instanceof Function ? 1 : 0; + } + localShadow(): number { const Object = BuiltinProjectClass; return BuiltinProjectClass instanceof Object ? 1 : 0; From ddc203c0b208b841b7540b962d7fc652e32fa38f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 15:50:29 +0300 Subject: [PATCH 15/17] [TS] Preserve model dispatch guards with runtime SDK classes --- usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 b7aeaf2032..112b95bce2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -88,7 +88,8 @@ class TsMachine( private val ctx = TsContext( scene = runtimeScene, components = components, - applicationAndSdkClasses = runtimeScene.projectAndSdkClasses, + // Model bodies are reachable only through their dispatcher and its domain guards. + applicationAndSdkClasses = scene.projectClasses + runtimeScene.sdkClasses, ) private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher( models = requireNotNull(resolvedUnknownCallModels), From 55e17c6210ff3932371ad495c37c1b38601b257f Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 16:31:09 +0300 Subject: [PATCH 16/17] [TS] Defer constructor field bounds until input reads --- .../main/kotlin/org/usvm/machine/TsMachine.kt | 2 +- .../kotlin/org/usvm/machine/expr/ReadField.kt | 16 ++ .../machine/types/TsConstructorInputGuard.kt | 166 +++--------------- .../samples/types/RuntimeInstanceofTest.kt | 76 +++++++- .../samples/types/RuntimeInstanceof.ts | 29 +++ 5 files changed, 138 insertions(+), 151 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 112b95bce2..405ce95895 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -252,7 +252,7 @@ class TsMachine( ): Pair, MutableSet> { val initialStates = mutableMapOf() val unsupportedPaths = mutableSetOf() - val constructorInputs = TsConstructorInputGuard(runtimeScene) + val constructorInputs = TsConstructorInputGuard() methods.forEach { method -> val unsupportedReason = constructorInputs.unsupportedReason(method) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index bb6aa77b95..5eb05dfa69 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -6,6 +6,7 @@ import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsField import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsGenericType import org.jacodb.ets.model.EtsInstanceFieldRef import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsNullType @@ -36,6 +37,7 @@ import org.usvm.machine.types.TsUnresolvedValue import org.usvm.machine.types.iteUnresolvedValue import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.machine.types.mkFakeValue +import org.usvm.machine.types.requiresConstructorWitness import org.usvm.machine.types.toAuxiliaryType import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult @@ -225,6 +227,20 @@ private fun TsContext.prepareInitialInputField( activeInitial: UBoolExpr, hierarchy: EtsHierarchy, ): TsUnresolvedValue? { + // A write, deletion or absent property can make the declared initial value irrelevant. + // Do not reject the entire input object just because another field needs a constructor witness. + val unsupportedInitial = when { + declaration?.type?.requiresConstructorWitness() == true -> "Constructor-typed input field" + declaration?.type is EtsGenericType -> "Unresolved generic input field" + else -> null + } + if (unsupportedInitial != null) { + scope.fork(mkNot(activeInitial), blockOnFalseState = { + terminateAsUnsupported(reason = "$unsupportedInitial is not modeled") + }) ?: return null + return value + } + val optional = declaration?.optional == true val sort = declaration?.let { typeToSort(it.type) } ?: unresolvedSort val expectedKind = when (sort) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsConstructorInputGuard.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsConstructorInputGuard.kt index bcf29d5ca5..0ee059c218 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsConstructorInputGuard.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsConstructorInputGuard.kt @@ -2,175 +2,51 @@ package org.usvm.machine.types import org.jacodb.ets.model.EtsAliasType import org.jacodb.ets.model.EtsArrayType -import org.jacodb.ets.model.EtsClass -import org.jacodb.ets.model.EtsClassSignature -import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsClassValueType -import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsGenericType import org.jacodb.ets.model.EtsIntersectionType import org.jacodb.ets.model.EtsMethod -import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsTupleType import org.jacodb.ets.model.EtsType -import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUnionType import org.usvm.util.humanReadableSignature /** - * Rejects input shapes for which we cannot generate a faithful constructor-valued witness. - * - * A class constructor is a function object, not an instance of that class. The current input generator would - * materialize constructor-typed values as ordinary instances and lose their callable identity. Inspect nested - * parameter types and instance fields before starting analysis so that this gap has an explicit unsupported outcome. - * This is an entrypoint-wide bound: an unsupported field excludes the method even if its body does not read it. + * Bounds inputs that themselves require a callable constructor witness, rather than an ordinary object. + * Instance inputs are structural field maps: neither their class declarations nor generic arguments imply + * that every declared field is used. Check those fields only when their initial values are actually read. */ -internal class TsConstructorInputGuard(scene: EtsScene) { - private val classesBySignature = scene.projectAndSdkClasses.associateBy { it.signature } - +internal class TsConstructorInputGuard { fun unsupportedReason(method: EtsMethod): String? { val genericParameters = method.typeParameters.filterIsInstance().associateBy { it.typeName } - val unsupportedParameter = method.parameters.firstNotNullOfOrNull { parameter -> - val gap = parameter.type.constructorInputGap(genericParameters, classesBySignature) - gap?.let { parameter to it } + val parameter = method.parameters.firstOrNull { + it.type.requiresConstructorWitness(genericParameters) } ?: return null - val (parameter, gap) = unsupportedParameter - return "${gap.description} '${parameter.name}' in ${method.humanReadableSignature} is not modeled" + return "Constructor-typed parameter '${parameter.name}' in ${method.humanReadableSignature} is not modeled" } } -private enum class ConstructorInputGap(val description: String) { - CONSTRUCTOR_VALUE("Constructor-typed parameter"), - UNRESOLVED_INHERITED_GENERIC("Unresolved inherited generic field in parameter"), -} - -// Visited sets describe the current traversal path, so recursive classes and generic constraints terminate -// without hiding a constructor-valued sibling field. Static fields do not belong to an input object's payload. -private fun EtsType.constructorInputGap( - genericParameters: Map, - classesBySignature: Map, +/** Inspect the value's own type, without traversing instance declarations or their type arguments. */ +internal fun EtsType.requiresConstructorWitness( + genericParameters: Map = emptyMap(), visitedGenerics: Set = emptySet(), - visitedClasses: Set = emptySet(), -): ConstructorInputGap? = when (this) { - is EtsClassValueType -> ConstructorInputGap.CONSTRUCTOR_VALUE - is EtsUnionType -> types.firstNotNullOfOrNull { - it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) - } - is EtsIntersectionType -> types.firstNotNullOfOrNull { - it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) - } - is EtsTupleType -> types.firstNotNullOfOrNull { - it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) - } - is EtsArrayType -> elementType.constructorInputGap( - genericParameters, - classesBySignature, - visitedGenerics, - visitedClasses, - ) - is EtsClassType -> constructorInputGapInClass( - genericParameters, - classesBySignature, - visitedGenerics, - visitedClasses, - ) - is EtsUnclearRefType -> typeParameters.firstNotNullOfOrNull { - it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) - } - is EtsAliasType -> originalType.constructorInputGap( - genericParameters, - classesBySignature, - visitedGenerics, - visitedClasses, - ) +): Boolean = when (this) { + is EtsClassValueType -> true + is EtsUnionType -> types.any { it.requiresConstructorWitness(genericParameters, visitedGenerics) } + is EtsIntersectionType -> types.any { it.requiresConstructorWitness(genericParameters, visitedGenerics) } + is EtsTupleType -> types.any { it.requiresConstructorWitness(genericParameters, visitedGenerics) } + is EtsArrayType -> elementType.requiresConstructorWitness(genericParameters, visitedGenerics) + is EtsAliasType -> originalType.requiresConstructorWitness(genericParameters, visitedGenerics) is EtsGenericType -> { if (typeName in visitedGenerics) { - null + false } else { val declaration = genericParameters[typeName] - listOfNotNull(constraint, defaultType, declaration?.constraint, declaration?.defaultType) - .firstNotNullOfOrNull { - it.constructorInputGap( - genericParameters, - classesBySignature, - visitedGenerics + typeName, - visitedClasses, - ) - } + listOfNotNull(constraint, defaultType, declaration?.constraint, declaration?.defaultType).any { + it.requiresConstructorWitness(genericParameters, visitedGenerics + typeName) + } } } - else -> null -} - -private fun EtsClassType.constructorInputGapInClass( - genericParameters: Map, - classesBySignature: Map, - visitedGenerics: Set, - visitedClasses: Set, -): ConstructorInputGap? { - val typeArgumentGap = typeParameters.firstNotNullOfOrNull { - it.constructorInputGap(genericParameters, classesBySignature, visitedGenerics, visitedClasses) - } - if (typeArgumentGap != null) { - return typeArgumentGap - } - - if (signature in visitedClasses) { - return null - } - - val clazz = classesBySignature[signature] ?: return null - val nextVisitedClasses = visitedClasses + signature - val fieldGap = clazz.fields.firstNotNullOfOrNull { field -> - if (field.modifiers.isStatic) return@firstNotNullOfOrNull null - - field.type.constructorInputGap( - genericParameters, - classesBySignature, - visitedGenerics, - nextVisitedClasses, - ) - } - if (fieldGap != null) { - return fieldGap - } - - val superClass = clazz.superClass ?: return null - val superClasses = if (superClass.file == EtsFileSignature.UNKNOWN) { - classesBySignature.values.filter { it.name == superClass.name } - } else { - listOfNotNull(classesBySignature[superClass]) - } - - return superClasses.firstNotNullOfOrNull { parent -> - val parentGap = EtsClassType(parent.signature).constructorInputGap( - genericParameters, - classesBySignature, - visitedGenerics, - nextVisitedClasses, - ) - if (parentGap != null) return@firstNotNullOfOrNull parentGap - - // The frontend omits extends type arguments. Even an apparent numeric specialization may hide a - // constructor in an inherited T, so reject this shape until superclass arguments are available. - val parentGenerics = parent.typeParameters.filterIsInstance() - .mapTo(mutableSetOf()) { it.typeName } - val unresolvedGenericField = parent.fields.any { field -> - !field.modifiers.isStatic && field.type.containsGeneric(parentGenerics) - } - if (unresolvedGenericField) ConstructorInputGap.UNRESOLVED_INHERITED_GENERIC else null - } -} - -private fun EtsType.containsGeneric(names: Set): Boolean = when (this) { - is EtsGenericType -> typeName in names - is EtsUnionType -> types.any { it.containsGeneric(names) } - is EtsIntersectionType -> types.any { it.containsGeneric(names) } - is EtsTupleType -> types.any { it.containsGeneric(names) } - is EtsArrayType -> elementType.containsGeneric(names) - is EtsClassType -> typeParameters.any { it.containsGeneric(names) } - is EtsUnclearRefType -> typeParameters.any { it.containsGeneric(names) } - is EtsAliasType -> originalType.containsGeneric(names) else -> false } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt index 6c7a94c623..f5f7639590 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -385,6 +385,72 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { )) } + @Test + fun `unused constructor fields do not exclude structural input objects`() { + val methods = listOf( + "unreadConstructorField", + "unreadNestedConstructorField", + "unreadGenericConstructorField", + "unreadInheritedGenericConstructorField", + ) + + methods.forEach { methodName -> + discoverProperties( + method = getMethod(methodName = methodName, className = "RuntimeInstanceof"), + { _, result -> result.number == 1.0 }, + { _, result -> result.number == 0.0 }, + invariants = arrayOf({ input, result -> + val marker = input.properties["marker"] as? TsTestValue.TsNumber + result.number == if (marker?.number == 7.0) 1.0 else 0.0 + }), + ) + } + + replay(methods.flatMap { methodName -> + listOf( + "if (new RuntimeInstanceof().$methodName({ marker: 7 } as any) !== 1) throw Error('$methodName 7');", + "if (new RuntimeInstanceof().$methodName({ marker: 3 } as any) !== 0) throw Error('$methodName 3');", + ) + }) + } + + @Test + fun `writing a constructor field before reading it needs no callable input witness`() { + discoverProperties( + method = getMethod(methodName = "overwrittenConstructorField", className = "RuntimeInstanceof"), + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 1.0 }), + ) + + replay(listOf( + "if (new RuntimeInstanceof().overwrittenConstructorField({} as any) !== 1) throw Error('overwritten ctor');" + )) + } + + @Test + fun `unsupported field read preserves paths that do not read the constructor`() { + val method = getMethod(methodName = "conditionalConstructorField", className = "RuntimeInstanceof") + + discoverProperties( + method = method, + { _, read, result -> !read.value && result.number == 1.0 }, + { _, read, result -> !read.value && result.number == 0.0 }, + invariants = arrayOf({ input, read, result -> + val marker = input.properties["marker"] as? TsTestValue.TsNumber + val expected = if (marker?.number == 7.0) 1.0 else 0.0 + + read.value == false && result.number == expected + }), + ) + + val outcome = analyze("conditionalConstructorField") + + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed input field" in it }, + "${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + } + @Test fun `constructor typed input has an explicit unsupported outcome`() { val outcome = analyze("constructorParameter") @@ -465,12 +531,12 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { } @Test - fun `constructor value in class type argument has an explicit unsupported outcome`() { + fun `reading an unresolved generic field has an explicit unsupported outcome`() { val outcome = analyze("constructorBoxParameter") assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) assertTrue(outcome.states.isEmpty(), "${outcome.states}") - assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + assertTrue(outcome.unsupportedPaths.any { "Unresolved generic input field" in it }, "${outcome.unsupportedPaths}") replay(listOf( @@ -492,7 +558,7 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}") - assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed input field" in it }, "$methodName: ${outcome.unsupportedPaths}") } @@ -507,7 +573,7 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { } @Test - fun `inherited generic fields have explicit unsupported outcomes`() { + fun `reading inherited generic fields has explicit unsupported outcomes`() { val methods = listOf("inheritedGenericConstructorParameter", "inheritedGenericNumberParameter") methods.forEach { methodName -> @@ -515,7 +581,7 @@ class RuntimeInstanceofTest : TsMethodTestRunner() { assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}") - assertTrue(outcome.unsupportedPaths.any { "Unresolved inherited generic" in it }, + assertTrue(outcome.unsupportedPaths.any { "Unresolved generic input field" in it }, "$methodName: ${outcome.unsupportedPaths}") } diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts index bb68ea27a0..a701d1e5e0 100644 --- a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts +++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts @@ -153,6 +153,32 @@ class RuntimeInstanceof { return instance instanceof InstanceHasInstanceFieldChild; } + unreadConstructorField(holder: { marker: number; ctor: typeof InstanceA }): number { + return holder.marker === 7 ? 1 : 0; + } + + unreadNestedConstructorField(holder: { marker: number; nested: { ctor: typeof InstanceA } }): number { + return holder.marker === 7 ? 1 : 0; + } + + unreadGenericConstructorField(holder: InstancePayload): number { + return holder.marker === 7 ? 1 : 0; + } + + unreadInheritedGenericConstructorField(holder: InstanceInheritedPayload): number { + return holder.marker === 7 ? 1 : 0; + } + + overwrittenConstructorField(holder: { ctor: typeof InstanceA }): number { + holder.ctor = InstanceA; + return typeof holder.ctor === "function" ? 1 : 0; + } + + conditionalConstructorField(holder: { marker: number; ctor: typeof InstanceA }, read: boolean): number { + if (read) return typeof holder.ctor === "function" ? 1 : 0; + return holder.marker === 7 ? 1 : 0; + } + constructorParameter(ctor: typeof InstanceA): boolean { return new InstanceA() instanceof ctor; } @@ -254,3 +280,6 @@ class InstanceHasInstanceFieldParent { static [Symbol.hasInstance] = (_value: unknown): boolean => false; } class InstanceHasInstanceFieldChild extends InstanceHasInstanceFieldParent { hasInstanceFieldChildMarker: number = 1; } + +class InstancePayload { marker!: number; value!: T; } +class InstanceInheritedPayload extends InstancePayload {} From f175f2d47ab17424287dd47fa43086c2d4098788 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 16:31:12 +0300 Subject: [PATCH 17/17] [TS] Load core declarations from the bundled TypeScript SDK --- .../kotlin/org/usvm/machine/TsRuntimeSdk.kt | 75 ++++++++++--------- .../main/kotlin/org/usvm/util/EtsHierarchy.kt | 6 +- .../usvm/machine/types/TsTypeSystemTest.kt | 14 ++++ 3 files changed, 58 insertions(+), 37 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt index d62c53db72..966ce27b7d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt @@ -1,52 +1,57 @@ package org.usvm.machine +import org.jacodb.ets.dto.EtsFileDto +import org.jacodb.ets.dto.toEtsFile import org.jacodb.ets.model.EtsClass -import org.jacodb.ets.model.EtsClassCategory -import org.jacodb.ets.model.EtsClassImpl -import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFile -import org.jacodb.ets.model.EtsFileSignature import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.etsIrSerializerScript +import org.jacodb.ets.utils.generateEtsIR import org.usvm.util.EtsHierarchy +import kotlin.io.path.deleteIfExists +import kotlin.io.path.inputStream -private val runtimeSdkFile = EtsHierarchy.OBJECT_CLASS.signature.file -private val runtimePrototypeFile = EtsFileSignature(projectName = "usvm-runtime-sdk", fileName = "PrototypeIdentities") +private val coreRuntimeClassNames = setOf("Object", "Function", "Array") -/** Synthetic Function and Array identities cannot be materialized as ordinary class instances. */ -internal fun EtsClassType.isCoreRuntimePrototypeIdentity(): Boolean = signature.file == runtimePrototypeFile +// JacoDB ships the matching TypeScript lib*.d.ts next to its frontend. Single-file conversion supports +// declarations, while project mode deliberately skips them. Cache the DTO, not mutable scene-owned classes. +private val coreRuntimeSdk: EtsFileDto by lazy { + val library = etsIrSerializerScript(EtsIrProvider.TS_FRONTEND).resolveSibling("lib.es5.d.ts") + val ir = generateEtsIR(library, loadEntrypoints = false, provider = EtsIrProvider.TS_FRONTEND) + try { + val file = ir.inputStream().use { EtsFileDto.loadFromJson(it) } + file.copy( + classes = file.classes.filter { it.signature.name in coreRuntimeClassNames }, + namespaces = emptyList(), + ) + } finally { + ir.deleteIfExists() + } +} + +/** Standard Function and Array declarations use dedicated values, not ordinary class-instance witnesses. */ +internal fun EtsClassType.isCoreRuntimePrototypeIdentity(): Boolean = + signature.file == EtsHierarchy.OBJECT_CLASS.signature.file && + signature.name in setOf("Function", "Array") /** - * Minimal prototype identities for the standard Object, Function and Array constructors. - * These declarations support runtime membership checks, not execution of their standard-library APIs. - * Preserve explicitly loaded SDK declarations; add only the missing core identities. Synthetic Function and Array - * declarations have a reserved signature and are excluded from instantiable type streams: functions and arrays - * use their existing dedicated runtime representations. Object remains an ordinary object input candidate. + * Load Object, Function and Array from the standard declarations bundled in the pinned JacoDB dependency. + * Keep their signatures and members and preserve SDK declarations supplied by the caller. Declaration files + * describe prototypes and APIs; executing an SDK API still requires an interpreter implementation or model. */ internal fun EtsScene.withCoreRuntimeSdk(): EtsScene { - val objectSignature = sdkClasses.singleOrNull { it.name == "Object" }?.signature - ?: EtsHierarchy.OBJECT_CLASS.signature - val missingClasses = listOf("Object", "Function", "Array") - .filter { name -> sdkClasses.none { it.name == name } } - .map { name -> - EtsClassImpl( - signature = EtsClassSignature( - name = name, - file = if (name == "Object") runtimeSdkFile else runtimePrototypeFile, - ), - fields = emptyList(), - methods = emptyList(), - category = EtsClassCategory.INTERFACE, - superClass = if (name == "Object") null else objectSignature, - ) - } - if (missingClasses.isEmpty()) return this - - val coreSdkFiles = missingClasses.groupBy { it.signature.file }.map { (file, classes) -> - EtsFile(signature = file, classes = classes, namespaces = emptyList()) - } - return EtsScene(projectFiles = projectFiles, sdkFiles = sdkFiles + coreSdkFiles, projectName = projectName) + val missingNames = coreRuntimeClassNames - sdkClasses.map { it.name }.toSet() + if (missingNames.isEmpty()) return this + + val library = coreRuntimeSdk.toEtsFile() + val classes = library.classes.filter { it.name in missingNames } + check(classes.map { it.name }.toSet() == missingNames) { "Core TypeScript SDK declarations are missing" } + val file = EtsFile(signature = library.signature, classes = classes, namespaces = emptyList()) + + return EtsScene(projectFiles = projectFiles, sdkFiles = sdkFiles + file, projectName = projectName) } /** An undeclared frontend local denotes a standard-library constructor, rather than a project binding. */ diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index 87dc00d4f0..4de206a4f2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -118,11 +118,13 @@ class EtsHierarchy(private val scene: EtsScene) { } companion object { - // TODO use real one + private val objectFile = EtsFileSignature(projectName = "", fileName = "lib.es5.d.ts") + + // The Object declaration in the TypeScript library bundled by JacoDB. val OBJECT_CLASS = EtsClassType( signature = EtsClassSignature( name = "Object", - file = EtsFileSignature(projectName = "ES2015", fileName = "BuiltinClass") + file = objectFile ), ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt index 4489cf7433..7db0ac6cd7 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt @@ -61,6 +61,20 @@ class TsTypeSystemTest { prototypes.forEach { assertFalse(it.type in result.types, it.name) } } + @Test + fun `core SDK uses bundled TypeScript declarations with their members`() { + val scene = EtsScene(projectFiles = emptyList()).withCoreRuntimeSdk() + val objectClass = scene.sdkClasses.single { it.name == "Object" } + val functionClass = scene.sdkClasses.single { it.name == "Function" } + val arrayClass = scene.sdkClasses.single { it.name == "Array" } + + assertTrue(objectClass.signature == EtsHierarchy.OBJECT_CLASS.signature) + assertTrue(objectClass.methods.any { it.name == "hasOwnProperty" }) + assertTrue(functionClass.methods.any { it.name == "apply" }) + assertTrue(arrayClass.methods.any { it.name == "slice" }) + assertTrue(scene.sdkClasses.all { it.signature.file.fileName == "lib.es5.d.ts" }) + } + @Test fun `core SDK bootstrap preserves explicitly loaded SDK declarations`() { val fileSignature = EtsFileSignature(projectName = "sdk", fileName = "function.ts")