From 06029907787f959fa976f551ea189a928af74dba Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 2 Oct 2026 20:01:50 +0300 Subject: [PATCH 01/20] [TS] Materialize symbolic string input witnesses --- .../org/usvm/machine/expr/ReadLength.kt | 15 ++- .../usvm/machine/interpreter/TsInterpreter.kt | 13 ++ .../usvm/machine/TsSymbolicStringInputTest.kt | 112 ++++++++++++++++++ .../kotlin/org/usvm/util/TsTestResolver.kt | 44 +++++-- .../resources/models/SymbolicStringInput.ts | 13 ++ 5 files changed, 183 insertions(+), 14 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt create mode 100644 usvm-ts/src/test/resources/models/SymbolicStringInput.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt index 86444e1054..823cdaaf0b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt @@ -5,6 +5,7 @@ import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsUnknownType import org.usvm.UExpr @@ -14,6 +15,7 @@ import org.usvm.machine.interpreter.TsStepScope import org.usvm.sizeSort import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.mkFieldLValue // Handles reading the `length` property. fun TsContext.readLengthProperty( @@ -34,8 +36,17 @@ fun TsContext.readLengthProperty( } is EtsStringType -> { - // Strings are treated as arrays of characters (represented as strings). - EtsArrayType(EtsStringType, dimensions = 1) + val charsRef = scope.calcOnState { + val valueLValue = mkFieldLValue(addressSort, instance, field = "value") + memory.read(valueLValue) + } + + return readArrayLength( + scope = scope, + array = charsRef, + arrayType = EtsArrayType(EtsNumberType, dimensions = 1), + maxArraySize = maxArraySize, + ) } else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type") diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index f5ea96ef7a..ceb615390f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -811,6 +811,19 @@ class TsInterpreter( state.pathConstraints += mkNot(mkHeapRefEq(ref, mkUndefinedValue())) state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType) + + // String constants store UTF-16 code units in their `value` array. + // Give symbolic inputs the same backing representation and bound its length. + val charsType = EtsArrayType(EtsNumberType, dimensions = 1) + val valueLValue = mkFieldLValue(addressSort, ref, field = "value") + val charsRef = state.memory.read(valueLValue).asExpr(addressSort) + state.pathConstraints += mkNot(mkHeapRefEq(charsRef, mkUndefinedValue())) + state.pathConstraints += state.memory.types.evalTypeEquals(charsRef, charsType) + + val lengthLValue = mkArrayLengthLValue(charsRef, charsType) + val length = state.memory.read(lengthLValue).asExpr(sizeSort) + state.pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) + state.pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)) } val parameterSort = typeToSort(parameterType) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt new file mode 100644 index 0000000000..36c10c4c6c --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt @@ -0,0 +1,112 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +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 + +class TsSymbolicStringInputTest { + @TempDir + lateinit var directory: Path + + @Test + fun `symbolic string witnesses replay including empty and nonempty values`() { + val source = getResourcePath("/models/SymbolicStringInput.ts") + val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + val methods = scene.projectClasses.single { it.name == "SymbolicStringInput" }.methods + .filter { it.name in setOf("identity", "lengthOne", "literal") } + .associateBy { it.name } + val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + val tests = TsMachine(scene, options = options, tsOptions = TsOptions()).use { machine -> + methods.mapValues { (_, method) -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + val identityTests = tests.getValue("identity") + assertTrue(identityTests.isNotEmpty()) + identityTests.forEach { test -> + val input = assertIs(test.before.parameters.single()).value + val result = assertIs(test.returnValue).value + assertEquals(input, result) + } + + val lengthTests = tests.getValue("lengthOne") + assertEquals(setOf(0.0, 1.0), lengthTests.map { test -> + assertIs(test.returnValue).number + }.toSet()) + assertTrue(lengthTests.any { test -> + assertIs(test.before.parameters.single()).value.isEmpty() + }) + assertTrue(lengthTests.any { test -> + assertIs(test.before.parameters.single()).value.isNotEmpty() + }) + + val literalTests = tests.getValue("literal") + assertTrue(literalTests.isNotEmpty()) + literalTests.forEach { test -> + assertEquals("A\u0000\u03a9\uD83D\uDE00", assertIs(test.returnValue).value) + } + + val script = buildString { + appendLine(source.readText()) + tests.forEach { (name, generated) -> + generated.forEachIndexed { index, test -> + val args = test.before.parameters.joinToString { value -> + jsString(assertIs(value).value) + } + val expected = when (val result = test.returnValue) { + is TsTestValue.TsString -> jsString(result.value) + is TsTestValue.TsNumber -> result.number.toString() + else -> error("Unexpected result for $name: $result") + } + + appendLine("if (new SymbolicStringInput().$name($args) !== $expected) {") + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } + } + } + val replay = directory.resolve("replay.ts") + val output = directory.resolve("replay.out") + replay.writeText(script) + + val process = ProcessBuilder("node", "--experimental-strip-types", replay.toString()) + .redirectErrorStream(true) + .redirectOutput(output.toFile()) + .start() + try { + assertTrue(process.waitFor(10, TimeUnit.SECONDS), "String witness replay timed out") + assertEquals(0, process.exitValue(), "${output.readText()}\n$script") + } finally { + if (process.isAlive) process.destroyForcibly() + } + } + + private fun jsString(value: String): String = value.map { "\\u%04x".format(it.code) }.joinToString( + separator = "", + prefix = "\"", + postfix = "\"", + ) +} 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 2f950432f0..5375f7daf8 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -1,5 +1,6 @@ package org.usvm.util +import io.ksmt.expr.KBitVec16Value import io.ksmt.expr.KFpValue import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType @@ -250,11 +251,7 @@ open class TsTestStateResolver( } is EtsStringType -> { - if (isAllocatedConcreteHeapRef(concreteRef)) { - resolveAllocatedString(concreteRef) - } else { - TsTestValue.TsString("String construction is not yet implemented") - } + resolveString(heapRef, concreteRef) } else -> error("Unexpected type: $type") @@ -306,13 +303,32 @@ open class TsTestStateResolver( return TsTestValue.TsArray(values) } - private fun resolveAllocatedString( - ref: UConcreteHeapRef, - ): TsTestValue.TsString { - val value = ctx.getStringConstantValue(ref) ?: run { - error("String constant not found for ref: $ref") + private fun resolveString( + heapRef: UHeapRef, + concreteRef: UConcreteHeapRef, + ): TsTestValue.TsString = with(ctx) { + getStringConstantValue(concreteRef)?.let { return TsTestValue.TsString(it) } + + val valueLValue = mkFieldLValue(addressSort, heapRef, field = "value") + val charsRef = evaluateInModel(memory.read(valueLValue)) as UConcreteHeapRef + if (charsRef.address == 0) { + return TsTestValue.TsString("") + } + + val charsType = EtsArrayType(EtsNumberType, dimensions = 1) + val lengthLValue = mkArrayLengthLValue(charsRef, charsType) + val length = evaluateInModel(memory.read(lengthLValue)).extractInt() + require(length in 0..MAX_STRING_LENGTH) { "Unsupported symbolic string length: $length" } + + val value = buildString(length) { + repeat(length) { index -> + val elementLValue = mkArrayIndexLValue(bv16Sort, charsRef, mkSizeExpr(index), charsType) + val element = evaluateInModel(memory.read(elementLValue)) as KBitVec16Value + append(element.shortValue.toInt().toChar()) + } } - return TsTestValue.TsString(value) + + TsTestValue.TsString(value) } fun resolveThisInstance(): TsTestValue { @@ -396,12 +412,16 @@ open class TsTestStateResolver( is EtsLiteralType -> TODO() EtsNullType -> TODO() EtsNeverType -> TODO() - EtsStringType -> TsTestValue.TsString("String construction is not yet implemented") + EtsStringType -> error("String values must be resolved from heap references") EtsVoidType -> TODO() else -> error("Unexpected type: $type") } } + private companion object { + const val MAX_STRING_LENGTH = 10_000 + } + private fun resolveClass( refType: EtsRefType, ): EtsClass { diff --git a/usvm-ts/src/test/resources/models/SymbolicStringInput.ts b/usvm-ts/src/test/resources/models/SymbolicStringInput.ts new file mode 100644 index 0000000000..aee26dc818 --- /dev/null +++ b/usvm-ts/src/test/resources/models/SymbolicStringInput.ts @@ -0,0 +1,13 @@ +class SymbolicStringInput { + identity(value: string): string { + return value; + } + + lengthOne(value: string): number { + return value.length === 1 ? 1 : 0; + } + + literal(): string { + return "A\u0000\u03a9\uD83D\uDE00"; + } +} From 0e5a513330938b67f851f4716c25daf3ea370a0d Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 2 Oct 2026 20:21:03 +0300 Subject: [PATCH 02/20] [TS] Keep symbolic string witness stable across snapshots --- .../org/usvm/machine/TsSymbolicStringInputTest.kt | 10 ++++++++-- .../src/test/kotlin/org/usvm/util/TsTestResolver.kt | 13 +++++++++---- .../test/resources/models/SymbolicStringInput.ts | 4 ++++ 3 files changed, 21 insertions(+), 6 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt index 36c10c4c6c..60b63cd6a2 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt @@ -29,7 +29,7 @@ class TsSymbolicStringInputTest { val source = getResourcePath("/models/SymbolicStringInput.ts") val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) val methods = scene.projectClasses.single { it.name == "SymbolicStringInput" }.methods - .filter { it.name in setOf("identity", "lengthOne", "literal") } + .filter { it.name in setOf("identity", "lengthOne", "literal", "literalLength") } .associateBy { it.name } val options = UMachineOptions( pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), @@ -49,7 +49,7 @@ class TsSymbolicStringInputTest { identityTests.forEach { test -> val input = assertIs(test.before.parameters.single()).value val result = assertIs(test.returnValue).value - assertEquals(input, result) + assertEquals(input, result, message = test.toString()) } val lengthTests = tests.getValue("lengthOne") @@ -69,6 +69,12 @@ class TsSymbolicStringInputTest { assertEquals("A\u0000\u03a9\uD83D\uDE00", assertIs(test.returnValue).value) } + val literalLengthTests = tests.getValue("literalLength") + assertTrue(literalLengthTests.isNotEmpty()) + literalLengthTests.forEach { test -> + assertEquals(5.0, assertIs(test.returnValue).number) + } + val script = buildString { appendLine(source.readText()) tests.forEach { (name, generated) -> 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 5375f7daf8..d1185bb57b 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -309,21 +309,26 @@ open class TsTestStateResolver( ): TsTestValue.TsString = with(ctx) { getStringConstantValue(concreteRef)?.let { return TsTestValue.TsString(it) } - val valueLValue = mkFieldLValue(addressSort, heapRef, field = "value") - val charsRef = evaluateInModel(memory.read(valueLValue)) as UConcreteHeapRef + // Symbolic strings have no mutable value field in the final state. Resolve + // their backing array from the model in both before and after snapshots. + val allocated = isAllocatedConcreteHeapRef(concreteRef) + val stringMemory = if (allocated) finalStateMemory else model + val stringRef = if (allocated) heapRef else concreteRef + val valueLValue = mkFieldLValue(addressSort, stringRef, field = "value") + val charsRef = evaluateInModel(stringMemory.read(valueLValue)) as UConcreteHeapRef if (charsRef.address == 0) { return TsTestValue.TsString("") } val charsType = EtsArrayType(EtsNumberType, dimensions = 1) val lengthLValue = mkArrayLengthLValue(charsRef, charsType) - val length = evaluateInModel(memory.read(lengthLValue)).extractInt() + val length = evaluateInModel(stringMemory.read(lengthLValue)).extractInt() require(length in 0..MAX_STRING_LENGTH) { "Unsupported symbolic string length: $length" } val value = buildString(length) { repeat(length) { index -> val elementLValue = mkArrayIndexLValue(bv16Sort, charsRef, mkSizeExpr(index), charsType) - val element = evaluateInModel(memory.read(elementLValue)) as KBitVec16Value + val element = evaluateInModel(stringMemory.read(elementLValue)) as KBitVec16Value append(element.shortValue.toInt().toChar()) } } diff --git a/usvm-ts/src/test/resources/models/SymbolicStringInput.ts b/usvm-ts/src/test/resources/models/SymbolicStringInput.ts index aee26dc818..fceed39598 100644 --- a/usvm-ts/src/test/resources/models/SymbolicStringInput.ts +++ b/usvm-ts/src/test/resources/models/SymbolicStringInput.ts @@ -10,4 +10,8 @@ class SymbolicStringInput { literal(): string { return "A\u0000\u03a9\uD83D\uDE00"; } + + literalLength(): number { + return "A\u0000\u03a9\uD83D\uDE00".length; + } } From f4638b843fc41f3d96c629adf34436193c678a57 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 2 Oct 2026 21:17:10 +0300 Subject: [PATCH 03/20] [TS] Isolate string backing and share witness length bound --- .../main/kotlin/org/usvm/machine/TsContext.kt | 4 + .../org/usvm/machine/expr/ReadLength.kt | 24 +++-- .../usvm/machine/interpreter/TsInterpreter.kt | 4 +- .../kotlin/org/usvm/machine/state/TsState.kt | 12 +-- .../main/kotlin/org/usvm/util/LValueUtil.kt | 14 +++ .../usvm/machine/TsSymbolicStringInputTest.kt | 100 +++++++++++++++--- .../kotlin/org/usvm/util/TsTestResolver.kt | 19 ++-- .../resources/models/SymbolicStringInput.ts | 11 ++ 8 files changed, 146 insertions(+), 42 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 e58f45f474..9a939c7e06 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -17,6 +17,7 @@ import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberLiteralType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsParameterRef +import org.jacodb.ets.model.EtsRawType import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStringLiteralType @@ -66,6 +67,9 @@ class TsContext( val unresolvedSort: TsUnresolvedSort = TsUnresolvedSort(this) + /** Array storage for UTF-16 code units; ordinary TypeScript arrays never use this region. */ + internal val stringBackingArrayDescriptor: EtsType = EtsRawType(kind = "usvm.ts.string.backing") + val voidSort: TsVoidSort by lazy { TsVoidSort(this) } val voidValue: TsVoidValue by lazy { TsVoidValue(this) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt index 823cdaaf0b..61fa030a29 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt @@ -5,17 +5,20 @@ import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsLocal -import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUnknownType import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.collection.array.length.UArrayLengthLValue import org.usvm.machine.TsContext +import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.sizeSort import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue +import org.usvm.util.mkStringBackingLengthLValue // Handles reading the `length` property. fun TsContext.readLengthProperty( @@ -43,8 +46,7 @@ fun TsContext.readLengthProperty( return readArrayLength( scope = scope, - array = charsRef, - arrayType = EtsArrayType(EtsNumberType, dimensions = 1), + lengthLValue = mkStringBackingLengthLValue(charsRef), maxArraySize = maxArraySize, ) } @@ -53,23 +55,23 @@ fun TsContext.readLengthProperty( } // Read the length of the array. - return readArrayLength(scope, instance, arrayType, maxArraySize) + return readArrayLength( + scope = scope, + lengthLValue = mkArrayLengthLValue(instance, arrayType), + maxArraySize = maxArraySize, + ) } // Reads the length of the array and returns it as a fp64 expression. fun TsContext.readArrayLength( scope: TsStepScope, - array: UHeapRef, - arrayType: EtsArrayType, + lengthLValue: UArrayLengthLValue, maxArraySize: Int, ): UExpr? { - checkNotFake(array) + checkNotFake(lengthLValue.ref) // Read the length of the array. - val length = scope.calcOnState { - val lengthLValue = mkArrayLengthLValue(array, arrayType) - memory.read(lengthLValue) - } + val length = scope.calcOnState { memory.read(lengthLValue) } // Check that the length is within the allowed bounds. ensureLengthBounds(scope, length, maxArraySize) ?: return null diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index ceb615390f..e69a972c17 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -82,6 +82,7 @@ import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.mkRegisterStackLValue +import org.usvm.util.mkStringBackingLengthLValue import org.usvm.util.resolveEtsMethods import org.usvm.util.type import org.usvm.utils.ensureSat @@ -743,6 +744,7 @@ class TsInterpreter( ctx = ctx, ownership = MutabilityOwnership(), entrypoint = method, + maxStringLength = options.maxArraySize, targets = UTargetsSet.from(targets), ) @@ -820,7 +822,7 @@ class TsInterpreter( state.pathConstraints += mkNot(mkHeapRefEq(charsRef, mkUndefinedValue())) state.pathConstraints += state.memory.types.evalTypeEquals(charsRef, charsType) - val lengthLValue = mkArrayLengthLValue(charsRef, charsType) + val lengthLValue = mkStringBackingLengthLValue(charsRef) val length = state.memory.read(lengthLValue).asExpr(sizeSort) state.pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) state.pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 019257dd38..1c753d2e83 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -1,6 +1,5 @@ package org.usvm.machine.state -import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBlockCfg import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsFile @@ -48,6 +47,7 @@ class TsState( ctx: TsContext, ownership: MutabilityOwnership, override val entrypoint: EtsMethod, + val maxStringLength: Int, callStack: UCallStack = UCallStack(), pathConstraints: UPathConstraints = UPathConstraints(ctx, ownership), memory: UMemory = UMemory(ctx, ownership, pathConstraints.typeConstraints), @@ -254,20 +254,17 @@ class TsState( memory.types.allocate(ref.address, EtsStringType) // Initialize char array - val valueType = EtsArrayType(EtsNumberType, dimensions = 1) - val descriptor = ctx.arrayDescriptorOf(valueType) - - val charArray = memory.allocConcrete(valueType.elementType) + val charArray = memory.allocConcrete(EtsNumberType) memory.initializeArray( arrayHeapRef = charArray, - type = descriptor, + type = stringBackingArrayDescriptor, sort = bv16Sort, sizeSort = sizeSort, contents = value.asSequence().map { mkBv(it.code, bv16Sort) }, ) // Write char array to `ref.value` - val valueLValue = mkFieldLValue(addressSort, ref, "value") + val valueLValue = mkFieldLValue(addressSort, ref, field = "value") memory.write(valueLValue, charArray, guard = trueExpr) ref @@ -289,6 +286,7 @@ class TsState( ctx = ctx, ownership = cloneOwnership, entrypoint = entrypoint, + maxStringLength = maxStringLength, callStack = callStack.clone(), pathConstraints = clonedConstraints, memory = memory.clone(clonedConstraints.typeConstraints, newThisOwnership, cloneOwnership), diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt index 8b319bd539..a4e8104319 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt @@ -1,5 +1,6 @@ package org.usvm.util +import io.ksmt.sort.KBv16Sort import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsField import org.jacodb.ets.model.EtsFieldSignature @@ -76,6 +77,19 @@ fun mkArrayLengthLValue( return UArrayLengthLValue(ref, descriptor, sizeSort) } +internal fun mkStringBackingLengthLValue( + ref: UHeapRef, +): UArrayLengthLValue = with(ref.tctx) { + UArrayLengthLValue(ref, stringBackingArrayDescriptor, sizeSort) +} + +internal fun mkStringBackingElementLValue( + ref: UHeapRef, + index: UExpr, +): UArrayIndexLValue = with(ref.tctx) { + UArrayIndexLValue(bv16Sort, ref, index, stringBackingArrayDescriptor) +} + fun mkRegisterStackLValue( sort: Sort, idx: Int, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt index 60b63cd6a2..26bc796a60 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt @@ -24,6 +24,13 @@ class TsSymbolicStringInputTest { @TempDir lateinit var directory: Path + private val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + @Test fun `symbolic string witnesses replay including empty and nonempty values`() { val source = getResourcePath("/models/SymbolicStringInput.ts") @@ -31,14 +38,7 @@ class TsSymbolicStringInputTest { val methods = scene.projectClasses.single { it.name == "SymbolicStringInput" }.methods .filter { it.name in setOf("identity", "lengthOne", "literal", "literalLength") } .associateBy { it.name } - val options = UMachineOptions( - pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), - solverType = SolverType.YICES, - solverTimeout = Duration.INFINITE, - typeOperationsTimeout = Duration.INFINITE, - ) - - val tests = TsMachine(scene, options = options, tsOptions = TsOptions()).use { machine -> + val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> methods.mapValues { (_, method) -> machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } } @@ -94,8 +94,84 @@ class TsSymbolicStringInputTest { } } } - val replay = directory.resolve("replay.ts") - val output = directory.resolve("replay.out") + assertReplay(script, name = "basic-strings") + } + + @Test + fun `string backing cannot alias an input number array`() { + val source = getResourcePath("/models/SymbolicStringInput.ts") + val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + val method = scene.projectClasses.single { it.name == "SymbolicStringInput" } + .methods.single { it.name == "independentArrayLength" } + + val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + + assertTrue(tests.isNotEmpty()) + assertEquals(setOf(0.0, 2.0), tests.map { test -> + assertIs(test.returnValue).number + }.toSet()) + + val script = buildString { + appendLine(source.readText()) + tests.forEachIndexed { index, test -> + val input = assertIs(test.before.parameters[0]).value + val array = assertIs>(test.before.parameters[1]) + val elements = array.values.joinToString { value -> + assertIs(value).number.toString() + } + val expected = assertIs(test.returnValue).number + + appendLine("if (new SymbolicStringInput().independentArrayLength(${jsString(input)}, [$elements]) !== $expected) {") + appendLine(" throw Error('array alias witness $index');") + appendLine("}") + } + } + assertReplay(script, name = "array-isolation") + } + + @Test + fun `configured string bound is shared with concrete test extraction`() { + val source = getResourcePath("/models/SymbolicStringInput.ts") + val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + val method = scene.projectClasses.single { it.name == "SymbolicStringInput" } + .methods.single { it.name == "lengthIs10001" } + val maxStringLength = 10_001 + + val tests = TsMachine( + scene, + options = machineOptions, + tsOptions = TsOptions(maxArraySize = maxStringLength), + ).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + + assertEquals(setOf(0.0, 1.0), tests.map { test -> + assertIs(test.returnValue).number + }.toSet()) + val longWitness = tests.single { test -> + assertIs(test.returnValue).number == 1.0 + } + assertEquals(maxStringLength, assertIs(longWitness.before.parameters.single()).value.length) + + val script = buildString { + appendLine(source.readText()) + tests.forEachIndexed { index, test -> + val input = assertIs(test.before.parameters.single()).value + val expected = assertIs(test.returnValue).number + + appendLine("if (new SymbolicStringInput().lengthIs10001(${jsString(input)}) !== $expected) {") + appendLine(" throw Error('string bound witness $index');") + appendLine("}") + } + } + assertReplay(script, name = "string-bound") + } + + private fun assertReplay(script: String, name: String) { + val replay = directory.resolve("$name.ts") + val output = directory.resolve("$name.out") replay.writeText(script) val process = ProcessBuilder("node", "--experimental-strip-types", replay.toString()) @@ -103,8 +179,8 @@ class TsSymbolicStringInputTest { .redirectOutput(output.toFile()) .start() try { - assertTrue(process.waitFor(10, TimeUnit.SECONDS), "String witness replay timed out") - assertEquals(0, process.exitValue(), "${output.readText()}\n$script") + assertTrue(process.waitFor(10, TimeUnit.SECONDS), "$name replay timed out") + assertEquals(0, process.exitValue(), "${output.readText()}\n${script.take(1000)}") } finally { if (process.isAlive) process.destroyForcibly() } 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 d1185bb57b..69332871f5 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -64,8 +64,8 @@ class TsTestResolver { prepareForResolve(state) - val beforeMemoryScope = MemoryScope(this, model, memory, method, resolvedLValuesToFakeObjects) - val afterMemoryScope = MemoryScope(this, model, memory, method, resolvedLValuesToFakeObjects) + val beforeMemoryScope = MemoryScope(this, model, memory, method, resolvedLValuesToFakeObjects, state.maxStringLength) + val afterMemoryScope = MemoryScope(this, model, memory, method, resolvedLValuesToFakeObjects, state.maxStringLength) val result = when (val res = state.methodResult) { is TsMethodResult.NoCall -> { @@ -159,7 +159,8 @@ class TsTestResolver { finalStateMemory: UReadOnlyMemory, method: EtsMethod, resolvedLValuesToFakeObjects: List, UConcreteHeapRef>>, - ) : TsTestStateResolver(ctx, model, finalStateMemory, method, resolvedLValuesToFakeObjects) { + maxStringLength: Int, + ) : TsTestStateResolver(ctx, model, finalStateMemory, method, resolvedLValuesToFakeObjects, maxStringLength) { fun resolveState(): TsParametersState { val thisInstance = resolveThisInstance() val parameters = resolveParameters() @@ -175,6 +176,7 @@ open class TsTestStateResolver( private val finalStateMemory: UReadOnlyMemory, val method: EtsMethod, val resolvedLValuesToFakeObjects: List, UConcreteHeapRef>>, + val maxStringLength: Int, ) { fun resolveLValue( lValue: ULValue<*, *>, @@ -320,14 +322,13 @@ open class TsTestStateResolver( return TsTestValue.TsString("") } - val charsType = EtsArrayType(EtsNumberType, dimensions = 1) - val lengthLValue = mkArrayLengthLValue(charsRef, charsType) + val lengthLValue = mkStringBackingLengthLValue(charsRef) val length = evaluateInModel(stringMemory.read(lengthLValue)).extractInt() - require(length in 0..MAX_STRING_LENGTH) { "Unsupported symbolic string length: $length" } + require(length in 0..maxStringLength) { "Unsupported symbolic string length: $length" } val value = buildString(length) { repeat(length) { index -> - val elementLValue = mkArrayIndexLValue(bv16Sort, charsRef, mkSizeExpr(index), charsType) + val elementLValue = mkStringBackingElementLValue(charsRef, mkSizeExpr(index)) val element = evaluateInModel(stringMemory.read(elementLValue)) as KBitVec16Value append(element.shortValue.toInt().toChar()) } @@ -423,10 +424,6 @@ open class TsTestStateResolver( } } - private companion object { - const val MAX_STRING_LENGTH = 10_000 - } - private fun resolveClass( refType: EtsRefType, ): EtsClass { diff --git a/usvm-ts/src/test/resources/models/SymbolicStringInput.ts b/usvm-ts/src/test/resources/models/SymbolicStringInput.ts index fceed39598..2b67f41025 100644 --- a/usvm-ts/src/test/resources/models/SymbolicStringInput.ts +++ b/usvm-ts/src/test/resources/models/SymbolicStringInput.ts @@ -14,4 +14,15 @@ class SymbolicStringInput { literalLength(): number { return "A\u0000\u03a9\uD83D\uDE00".length; } + + independentArrayLength(value: string, array: number[]): number { + if (value.length !== 1 || array.length !== 1) return 0; + + array.length = 0; + return value.length === 0 ? 1 : 2; + } + + lengthIs10001(value: string): number { + return value.length === 10001 ? 1 : 0; + } } From c7729f65620d3aef1bc86a3805338cbde4d12aac Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 2 Oct 2026 22:25:19 +0300 Subject: [PATCH 04/20] [TS] Format symbolic string regression tests --- .../usvm/machine/TsSymbolicStringInputTest.kt | 59 +++++++++++++------ .../kotlin/org/usvm/util/TsTestResolver.kt | 18 +++++- 2 files changed, 56 insertions(+), 21 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt index 26bc796a60..46c9fb14d3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt @@ -53,15 +53,22 @@ class TsSymbolicStringInputTest { } val lengthTests = tests.getValue("lengthOne") - assertEquals(setOf(0.0, 1.0), lengthTests.map { test -> - assertIs(test.returnValue).number - }.toSet()) - assertTrue(lengthTests.any { test -> - assertIs(test.before.parameters.single()).value.isEmpty() - }) - assertTrue(lengthTests.any { test -> - assertIs(test.before.parameters.single()).value.isNotEmpty() - }) + assertEquals( + setOf(0.0, 1.0), + lengthTests.map { test -> + assertIs(test.returnValue).number + }.toSet() + ) + assertTrue( + lengthTests.any { test -> + assertIs(test.before.parameters.single()).value.isEmpty() + } + ) + assertTrue( + lengthTests.any { test -> + assertIs(test.before.parameters.single()).value.isNotEmpty() + } + ) val literalTests = tests.getValue("literal") assertTrue(literalTests.isNotEmpty()) @@ -102,16 +109,20 @@ class TsSymbolicStringInputTest { val source = getResourcePath("/models/SymbolicStringInput.ts") val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) val method = scene.projectClasses.single { it.name == "SymbolicStringInput" } - .methods.single { it.name == "independentArrayLength" } + .methods + .single { it.name == "independentArrayLength" } val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } } assertTrue(tests.isNotEmpty()) - assertEquals(setOf(0.0, 2.0), tests.map { test -> - assertIs(test.returnValue).number - }.toSet()) + assertEquals( + setOf(0.0, 2.0), + tests.map { test -> + assertIs(test.returnValue).number + }.toSet() + ) val script = buildString { appendLine(source.readText()) @@ -122,8 +133,11 @@ class TsSymbolicStringInputTest { assertIs(value).number.toString() } val expected = assertIs(test.returnValue).number + val encodedInput = jsString(input) - appendLine("if (new SymbolicStringInput().independentArrayLength(${jsString(input)}, [$elements]) !== $expected) {") + appendLine( + "if (new SymbolicStringInput().independentArrayLength($encodedInput, [$elements]) !== $expected) {" + ) appendLine(" throw Error('array alias witness $index');") appendLine("}") } @@ -136,7 +150,8 @@ class TsSymbolicStringInputTest { val source = getResourcePath("/models/SymbolicStringInput.ts") val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) val method = scene.projectClasses.single { it.name == "SymbolicStringInput" } - .methods.single { it.name == "lengthIs10001" } + .methods + .single { it.name == "lengthIs10001" } val maxStringLength = 10_001 val tests = TsMachine( @@ -147,13 +162,19 @@ class TsSymbolicStringInputTest { machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } } - assertEquals(setOf(0.0, 1.0), tests.map { test -> - assertIs(test.returnValue).number - }.toSet()) + assertEquals( + setOf(0.0, 1.0), + tests.map { test -> + assertIs(test.returnValue).number + }.toSet() + ) val longWitness = tests.single { test -> assertIs(test.returnValue).number == 1.0 } - assertEquals(maxStringLength, assertIs(longWitness.before.parameters.single()).value.length) + assertEquals( + maxStringLength, + assertIs(longWitness.before.parameters.single()).value.length + ) val script = buildString { appendLine(source.readText()) 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 69332871f5..b17b1e9bd4 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -64,8 +64,22 @@ class TsTestResolver { prepareForResolve(state) - val beforeMemoryScope = MemoryScope(this, model, memory, method, resolvedLValuesToFakeObjects, state.maxStringLength) - val afterMemoryScope = MemoryScope(this, model, memory, method, resolvedLValuesToFakeObjects, state.maxStringLength) + val beforeMemoryScope = MemoryScope( + this, + model, + memory, + method, + resolvedLValuesToFakeObjects, + state.maxStringLength + ) + val afterMemoryScope = MemoryScope( + this, + model, + memory, + method, + resolvedLValuesToFakeObjects, + state.maxStringLength + ) val result = when (val res = state.methodResult) { is TsMethodResult.NoCall -> { From 7138e49b37b526a10ef802d450f007fe17f07177 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 06:56:02 +0300 Subject: [PATCH 05/20] [TS] Share Node replay helpers across regression suites --- .../usvm/machine/TsSymbolicStringInputTest.kt | 53 +++++++++---------- .../machine/call/TsArrayShiftReplayTest.kt | 34 +++--------- .../call/TsInstanceCallReceiverTest.kt | 34 +++--------- .../test/kotlin/org/usvm/util/NodeReplay.kt | 40 ++++++++++++++ 4 files changed, 81 insertions(+), 80 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/util/NodeReplay.kt diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt index 46c9fb14d3..f5d6ff060f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt @@ -10,16 +10,18 @@ import org.usvm.SolverType import org.usvm.UMachineOptions import org.usvm.api.TsTestValue import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay import org.usvm.util.getResourcePath +import org.usvm.util.jsString 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 +private const val REPLAY_FAILURE_CONTEXT_LIMIT = 1000 + class TsSymbolicStringInputTest { @TempDir lateinit var directory: Path @@ -101,7 +103,13 @@ class TsSymbolicStringInputTest { } } } - assertReplay(script, name = "basic-strings") + assertNodeReplay( + source = script, + directory = directory, + name = "basic-strings", + timeoutMessage = "basic-strings replay timed out", + failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), + ) } @Test @@ -142,7 +150,13 @@ class TsSymbolicStringInputTest { appendLine("}") } } - assertReplay(script, name = "array-isolation") + assertNodeReplay( + source = script, + directory = directory, + name = "array-isolation", + timeoutMessage = "array-isolation replay timed out", + failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), + ) } @Test @@ -187,29 +201,12 @@ class TsSymbolicStringInputTest { appendLine("}") } } - assertReplay(script, name = "string-bound") - } - - private fun assertReplay(script: String, name: String) { - val replay = directory.resolve("$name.ts") - val output = directory.resolve("$name.out") - replay.writeText(script) - - val process = ProcessBuilder("node", "--experimental-strip-types", replay.toString()) - .redirectErrorStream(true) - .redirectOutput(output.toFile()) - .start() - try { - assertTrue(process.waitFor(10, TimeUnit.SECONDS), "$name replay timed out") - assertEquals(0, process.exitValue(), "${output.readText()}\n${script.take(1000)}") - } finally { - if (process.isAlive) process.destroyForcibly() - } + assertNodeReplay( + source = script, + directory = directory, + name = "string-bound", + timeoutMessage = "string-bound replay timed out", + failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), + ) } - - private fun jsString(value: String): String = value.map { "\\u%04x".format(it.code) }.joinToString( - separator = "", - prefix = "\"", - postfix = "\"", - ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt index 2a844e606d..793a1d98ff 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt @@ -14,9 +14,9 @@ import org.usvm.api.TsTestValue import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.jsString 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 @@ -64,7 +64,12 @@ class TsArrayShiftReplayTest { appendLine("}") } } - assertReplay(script, index) + assertNodeReplay( + source = script, + directory = directory, + name = "replay$index", + timeoutMessage = "Replay timed out", + ) } } } @@ -436,29 +441,6 @@ class TsArrayShiftReplayTest { else -> error("Unsupported replay value: $value") } - private fun jsString(value: String): String = value.map { "\\u%04x".format(it.code) }.joinToString( - separator = "", - prefix = "\"", - postfix = "\"", - ) - - private fun assertReplay(source: String, index: Int) { - val script = directory.resolve("replay$index.ts") - val output = directory.resolve("replay$index.out") - script.writeText(source) - val process = ProcessBuilder("node", "--experimental-strip-types", script.toString()) - .redirectErrorStream(true) - .redirectOutput(output.toFile()) - .start() - - try { - assertTrue(process.waitFor(10, TimeUnit.SECONDS), "Replay timed out") - assertEquals(0, process.exitValue(), "${output.readText()}\n$source") - } finally { - if (process.isAlive) process.destroyForcibly() - } - } - private data class ReplayCase( val name: String, val parameters: String, diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt index a38ba9b3fe..72293e5b07 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt @@ -15,11 +15,11 @@ import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay import org.usvm.util.getResourcePath +import org.usvm.util.jsString 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 @@ -81,7 +81,12 @@ class TsInstanceCallReceiverTest { appendLine("}") } } - assertReplay(replay, case.method) + assertNodeReplay( + source = replay, + directory = directory, + name = case.method, + timeoutMessage = "Receiver replay timed out", + ) } } } @@ -98,29 +103,6 @@ class TsInstanceCallReceiverTest { else -> error("Unsupported receiver input: $value") } - private fun jsString(value: String): String = value.map { "\\u%04x".format(it.code) }.joinToString( - separator = "", - prefix = "\"", - postfix = "\"", - ) - - private fun assertReplay(source: String, name: String) { - val script = directory.resolve("$name.ts") - val output = directory.resolve("$name.out") - script.writeText(source) - val process = ProcessBuilder("node", "--experimental-strip-types", script.toString()) - .redirectErrorStream(true) - .redirectOutput(output.toFile()) - .start() - - try { - assertTrue(process.waitFor(10, TimeUnit.SECONDS), "Receiver replay timed out") - assertEquals(0, process.exitValue(), "${output.readText()}\n$source") - } finally { - if (process.isAlive) process.destroyForcibly() - } - } - private data class Case( val method: String, val results: Set, diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/NodeReplay.kt b/usvm-ts/src/test/kotlin/org/usvm/util/NodeReplay.kt new file mode 100644 index 0000000000..3c48906fa2 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/util/NodeReplay.kt @@ -0,0 +1,40 @@ +package org.usvm.util + +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.assertTrue + +private const val NODE_REPLAY_TIMEOUT_SECONDS = 10L + +fun jsString(value: String): String = value.map { "\\u%04x".format(it.code) }.joinToString( + separator = "", + prefix = "\"", + postfix = "\"", +) + +fun assertNodeReplay( + source: String, + directory: Path, + name: String, + timeoutMessage: String, + failureContext: String = source, +) { + val script = directory.resolve("$name.ts") + val output = directory.resolve("$name.out") + script.writeText(source) + + val process = ProcessBuilder("node", "--experimental-strip-types", script.toString()) + .redirectErrorStream(true) + .redirectOutput(output.toFile()) + .start() + + try { + assertTrue(process.waitFor(NODE_REPLAY_TIMEOUT_SECONDS, TimeUnit.SECONDS), timeoutMessage) + assertEquals(0, process.exitValue(), "${output.readText()}\n$failureContext") + } finally { + if (process.isAlive) process.destroyForcibly() + } +} From 5b866c7f2108c47dea3b45bd52c59f5b1f8aaf6d Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 07:18:07 +0300 Subject: [PATCH 06/20] [TS] Reject unbacked symbolic string witnesses --- .../usvm/machine/TsSymbolicStringInputTest.kt | 56 +++++++++++++++++++ .../kotlin/org/usvm/util/TsTestResolver.kt | 5 +- .../resources/models/SymbolicStringInput.ts | 8 +++ 3 files changed, 68 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt index f5d6ff060f..f214fb0e7d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt @@ -10,6 +10,7 @@ import org.usvm.SolverType import org.usvm.UMachineOptions import org.usvm.api.TsTestValue import org.usvm.util.TsTestResolver +import org.usvm.util.TsUnsupportedWitnessException import org.usvm.util.assertNodeReplay import org.usvm.util.getResourcePath import org.usvm.util.jsString @@ -209,4 +210,59 @@ class TsSymbolicStringInputTest { failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), ) } + + @Test + fun `string inferred from any without backing cannot become an empty witness`() { + val source = getResourcePath("/models/SymbolicStringInput.ts") + val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + val method = scene.projectClasses.single { it.name == "SymbolicStringInput" } + .methods + .single { it.name == "anyStringLength" } + + val states = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> + machine.analyze(listOf(method)) + } + + assertTrue(states.isNotEmpty()) + val resolutions = states.map { state -> runCatching { TsTestResolver().resolve(method, state) } } + val unsupported = resolutions.mapNotNull { it.exceptionOrNull() } + assertTrue( + unsupported.isNotEmpty(), + "Expected an unbacked symbolic string: $resolutions", + ) + unsupported.forEach { failure -> + assertIs(failure) + assertTrue("missing backing array" in failure.message.orEmpty(), failure.toString()) + } + + val supported = resolutions.mapNotNull { it.getOrNull() } + assertTrue(supported.isNotEmpty()) + val script = buildString { + appendLine(source.readText()) + appendLine("if (new SymbolicStringInput().anyStringLength(\"\") !== 2) throw Error('empty string');") + appendLine("if (new SymbolicStringInput().anyStringLength(\"x\") !== 1) throw Error('one-char string');") + supported.forEachIndexed { index, test -> + val input = when (val value = test.before.parameters.single()) { + TsTestValue.TsUndefined -> "undefined" + TsTestValue.TsNull -> "null" + is TsTestValue.TsBoolean -> value.value.toString() + is TsTestValue.TsNumber -> value.number.toString() + is TsTestValue.TsString -> jsString(value.value) + else -> error("Unexpected input for anyStringLength: $value") + } + val expected = assertIs(test.returnValue).number + + appendLine("if (new SymbolicStringInput().anyStringLength($input) !== $expected) {") + appendLine(" throw Error('any string witness $index');") + appendLine("}") + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "any-string", + timeoutMessage = "any-string replay timed out", + ) + } } 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 b17b1e9bd4..1e45549f0e 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -55,6 +55,9 @@ import org.usvm.model.UModelBase import org.usvm.sizeSort import org.usvm.types.first +/** A satisfying state lacks the modeled data needed to emit a concrete witness. */ +class TsUnsupportedWitnessException(message: String) : IllegalStateException(message) + class TsTestResolver { private val resolvedLValuesToFakeObjects: MutableList, UConcreteHeapRef>> = mutableListOf() @@ -333,7 +336,7 @@ open class TsTestStateResolver( val valueLValue = mkFieldLValue(addressSort, stringRef, field = "value") val charsRef = evaluateInModel(stringMemory.read(valueLValue)) as UConcreteHeapRef if (charsRef.address == 0) { - return TsTestValue.TsString("") + throw TsUnsupportedWitnessException("Symbolic string is missing backing array: $concreteRef") } val lengthLValue = mkStringBackingLengthLValue(charsRef) diff --git a/usvm-ts/src/test/resources/models/SymbolicStringInput.ts b/usvm-ts/src/test/resources/models/SymbolicStringInput.ts index 2b67f41025..dc1d2b7710 100644 --- a/usvm-ts/src/test/resources/models/SymbolicStringInput.ts +++ b/usvm-ts/src/test/resources/models/SymbolicStringInput.ts @@ -4,6 +4,8 @@ class SymbolicStringInput { } lengthOne(value: string): number { + if (value.length === 0) return 0; + return value.length === 1 ? 1 : 0; } @@ -25,4 +27,10 @@ class SymbolicStringInput { lengthIs10001(value: string): number { return value.length === 10001 ? 1 : 0; } + + anyStringLength(value: any): number { + if (typeof value !== "string") return 0; + + return value.length === 1 ? 1 : 2; + } } From 127ecb5df35366c550a32725cf4e6af25208f673 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 08:17:58 +0300 Subject: [PATCH 07/20] [TS] Compare string values in equality operators Implement supported string equality cases and preserve explicit unsupported outcomes for unbacked symbolic witnesses. Reuse shared Node replay tests. --- .../ts/calls/CurrentTsCallsSymbolicEngine.kt | 15 +- .../main/kotlin/org/usvm/machine/TsMachine.kt | 27 +- .../usvm/machine/interpreter/TsInterpreter.kt | 13 + .../usvm/machine/operator/TsBinaryOperator.kt | 303 ++++++++++++++++-- .../kotlin/org/usvm/machine/state/TsState.kt | 17 + .../org/usvm/machine/TsStringEqualityTest.kt | 277 ++++++++++++++++ .../call/TsUnknownCallDispatcherTest.kt | 33 ++ .../test/resources/models/StringEquality.ts | 58 ++++ 8 files changed, 707 insertions(+), 36 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt create mode 100644 usvm-ts/src/test/resources/models/StringEquality.ts diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt index b7767ed426..69da1df9d2 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt @@ -149,19 +149,29 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine { MachineResult( states = entryObserver.reachedStates, stopReason = outcome.stopReason, + unsupportedPaths = outcome.unsupportedPaths, ) } val states = analysis.states if (states.isEmpty()) { val status = when (analysis.stopReason) { - TsAnalysisStopReason.EXHAUSTED -> CallsSymbolicStatus.UNREACHED + TsAnalysisStopReason.EXHAUSTED -> { + if (analysis.unsupportedPaths.isEmpty()) { + CallsSymbolicStatus.UNREACHED + } else { + CallsSymbolicStatus.UNSUPPORTED + } + } // The machine options above disable every stop condition except the per-target timeout. - TsAnalysisStopReason.STOPPED -> CallsSymbolicStatus.TIMEOUT + TsAnalysisStopReason.STOPPED -> { + CallsSymbolicStatus.TIMEOUT + } } return result( status = status, startedAt = startedAt, + diagnostic = analysis.unsupportedPaths.joinToString().ifEmpty { null }, ) } @@ -284,6 +294,7 @@ internal class CurrentTsCallsSymbolicEngine : CallsSymbolicEngine { private data class MachineResult( val states: List, val stopReason: TsAnalysisStopReason, + val unsupportedPaths: List, ) } 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 5c5d344b3b..ca75767d69 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -49,6 +49,8 @@ enum class TsAnalysisStopReason { data class TsAnalysisResult( val states: List, val stopReason: TsAnalysisStopReason, + /** Reasons for satisfiable paths excluded by an explicit engine model bound. */ + val unsupportedPaths: List, ) class TsMachine( @@ -101,6 +103,7 @@ class TsMachine( ) private val cfgStatistics = CfgStatisticsImpl(graph) + /** Returns supported states only. Call [analyzeWithOutcome] to inspect excluded unsupported paths. */ fun analyze( methods: List, targets: List = emptyList(), @@ -154,6 +157,7 @@ class TsMachine( val observers = mutableListOf>(coverageStatistics) observers.add(statesCollector) + val unsupportedPaths = mutableSetOf() if (tsOptions.enableVisualization) { observers += TsStateVisualizer() @@ -202,10 +206,25 @@ class TsMachine( ) } + val supportedObserver = CompositeUMachineObserver(observers) + val outcomeObserver = object : UMachineObserver by supportedObserver { + override fun onStateTerminated(state: TsState, stateReachable: Boolean) { + val unsupportedReason = state.unsupportedReason + if (unsupportedReason != null) { + if (stateReachable) { + unsupportedPaths += unsupportedReason + } + return + } + + supportedObserver.onStateTerminated(state, stateReachable) + } + } + run( interpreter, pathSelector, - observer = CompositeUMachineObserver(observers), + observer = outcomeObserver, isStateTerminated = { state -> state.callStack.isEmpty() }, stopStrategy = stopStrategy ) @@ -216,7 +235,11 @@ class TsMachine( TsAnalysisStopReason.STOPPED } - return TsAnalysisResult(states = statesCollector.collectedStates, stopReason = stopReason) + return TsAnalysisResult( + states = statesCollector.collectedStates, + stopReason = stopReason, + unsupportedPaths = unsupportedPaths.toList(), + ) } override fun close() { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index e69a972c17..b15e04d2b1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -151,6 +151,18 @@ class TsInterpreter( } } } + } catch (e: UnsupportedOperationException) { + if (throwExceptionOnStepFailure) { + throw e + } + + val reason = e.message?.takeIf(String::isNotBlank) ?: "Unsupported TypeScript operation" + state.terminateAsUnsupported(reason) + + return StepResult( + forkedStates = scope.stepResult().forkedStates, + originalStateAlive = true, + ) } catch (e: Exception) { if (throwExceptionOnStepFailure) { throw e @@ -826,6 +838,7 @@ class TsInterpreter( val length = state.memory.read(lengthLValue).asExpr(sizeSort) state.pathConstraints += mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) state.pathConstraints += mkBvSignedLessOrEqualExpr(length, mkBv(options.maxArraySize)) + state.boundedStringBackingRefs += ref } val parameterSort = typeToSort(parameterType) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 9e4e1db477..03f28f177a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -4,23 +4,159 @@ import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr import io.ksmt.utils.cast import mu.KotlinLogging +import org.jacodb.ets.model.EtsStringType import org.usvm.UAddressSort import org.usvm.UBoolExpr import org.usvm.UBoolSort +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.UIteExpr import org.usvm.USort +import org.usvm.api.evalTypeEquals +import org.usvm.isFalse +import org.usvm.isTrue import org.usvm.machine.TsContext +import org.usvm.machine.TsSizeSort import org.usvm.machine.expr.mkNumericExpr import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.types.ExprWithTypeConstraint import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.util.boolToFp +import org.usvm.util.mkFieldLValue +import org.usvm.util.mkStringBackingElementLValue +import org.usvm.util.mkStringBackingLengthLValue private val logger = KotlinLogging.logger {} +/** Strings are primitive values even though the TS heap stores their UTF-16 contents behind references. */ +private fun TsContext.stringValueEquals( + lhs: UHeapRef, + rhs: UHeapRef, + sameReference: UBoolExpr, + activeGuard: UBoolExpr, + scope: TsStepScope, +): UBoolExpr? { + val lhsConstant = (lhs as? UConcreteHeapRef)?.let(::getStringConstantValue) + val rhsConstant = (rhs as? UConcreteHeapRef)?.let(::getStringConstantValue) + if (lhsConstant != null && rhsConstant != null) { + return if (lhsConstant == rhsConstant) trueExpr else falseExpr + } + + val (lhsIsString, rhsIsString) = scope.calcOnState { + memory.types.evalTypeEquals(lhs, EtsStringType) to memory.types.evalTypeEquals(rhs, EtsStringType) + } + if (lhsIsString.isFalse || rhsIsString.isFalse) return falseExpr + + val bothStrings = mkAnd(lhsIsString, rhsIsString) + val missingBacking = scope.calcOnState { + (lhsConstant == null && lhs !in boundedStringBackingRefs) || + (rhsConstant == null && rhs !in boundedStringBackingRefs) + } + // An alias of a known literal has that literal's value without reading a symbolic backing array. + val knownLiteralAlias = if (lhsConstant != null || rhsConstant != null) sameReference else falseExpr + val notBothStrings = mkNot(bothStrings) + val lhsNullish = mkOr(mkHeapRefEq(lhs, mkTsNullValue()), mkHeapRefEq(lhs, mkUndefinedValue())) + val rhsNullish = mkOr(mkHeapRefEq(rhs, mkTsNullValue()), mkHeapRefEq(rhs, mkUndefinedValue())) + if (missingBacking) { + val supportedWithoutBacking = mkOr( + mkNot(activeGuard), + knownLiteralAlias, + lhsNullish, + rhsNullish, + notBothStrings, + ) + scope.fork(supportedWithoutBacking, blockOnFalseState = { + terminateAsUnsupported(reason = "String equality needs a modeled string backing for dynamic references") + }) ?: return null + return falseExpr + } + + val comparison = scope.calcOnState { + val lhsChars = memory.read(mkFieldLValue(addressSort, lhs, field = "value")) + val rhsChars = memory.read(mkFieldLValue(addressSort, rhs, field = "value")) + val lhsLength = memory.read(mkStringBackingLengthLValue(lhsChars)) + val rhsLength = memory.read(mkStringBackingLengthLValue(rhsChars)) + + StringComparisonData( + lhsChars = lhsChars, + rhsChars = rhsChars, + lhsLength = lhsLength, + rhsLength = rhsLength, + maxLength = maxStringLength, + ) + } + + val zero = mkBv(0) + val maximum = mkBv(comparison.maxLength) + val boundedLengths = mkAnd( + if (lhsConstant == null) { + mkAnd( + mkBvSignedGreaterOrEqualExpr(comparison.lhsLength, zero), + mkBvSignedLessOrEqualExpr(comparison.lhsLength, maximum), + ) + } else { + trueExpr + }, + if (rhsConstant == null) { + mkAnd( + mkBvSignedGreaterOrEqualExpr(comparison.rhsLength, zero), + mkBvSignedLessOrEqualExpr(comparison.rhsLength, maximum), + ) + } else { + trueExpr + }, + ) + val supported = mkOr( + mkNot(activeGuard), + knownLiteralAlias, + lhsNullish, + rhsNullish, + notBothStrings, + boundedLengths, + ) + scope.fork(supported, blockOnFalseState = { + terminateAsUnsupported(reason = "String equality requires symbolic string length in 0..$maxStringLength") + }) ?: return null + + // Known literals supply a tighter comparison bound; all other string lengths are constrained above. + val comparisonLength = lhsConstant?.length ?: rhsConstant?.length ?: comparison.maxLength + val equalCharacters = (0 until comparisonLength).map { index -> + val position = mkBv(index) + val lhsCharacter = scope.calcOnState { + memory.read(mkStringBackingElementLValue(comparison.lhsChars, position)) + } + val rhsCharacter = scope.calcOnState { + memory.read(mkStringBackingElementLValue(comparison.rhsChars, position)) + } + mkImplies(mkBvSignedLessExpr(position, comparison.lhsLength), mkEq(lhsCharacter, rhsCharacter)) + } + + return mkAnd(lhsIsString, rhsIsString, mkEq(comparison.lhsLength, comparison.rhsLength), mkAnd(equalCharacters)) +} + +private data class StringComparisonData( + val lhsChars: UHeapRef, + val rhsChars: UHeapRef, + val lhsLength: UExpr, + val rhsLength: UExpr, + val maxLength: Int, +) + +private fun TsContext.referenceOrStringValueEquals( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + activeGuard: UBoolExpr = trueExpr, +): UBoolExpr? { + val sameReference = mkHeapRefEq(lhs, rhs) + if (sameReference.isTrue) return trueExpr + + val equalStringValues = stringValueEquals(lhs, rhs, sameReference, activeGuard, scope) ?: return null + return mkOr(sameReference, equalStringValues) +} + sealed interface TsBinaryOperator { fun TsContext.onBool( @@ -41,12 +177,26 @@ sealed interface TsBinaryOperator { scope: TsStepScope, ): UExpr<*>? + fun TsContext.onRefWithGuard( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UExpr<*>? = onRef(lhs, rhs, scope) + fun TsContext.resolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, ): UExpr<*>? + fun TsContext.resolveFakeObjectWithGuard( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UExpr<*>? = resolveFakeObject(lhs, rhs, scope) + fun TsContext.internalResolve( lhs: UExpr<*>, rhs: UExpr<*>, @@ -57,10 +207,13 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, + activeGuard: UBoolExpr = trueExpr, ): UExpr<*>? { if (lhs is UIteExpr<*>) { - val trueBranch = resolve(lhs.trueBranch, rhs, scope) ?: return null - val falseBranch = resolve(lhs.falseBranch, rhs, scope) ?: return null + val trueBranchGuard = mkAnd(activeGuard, lhs.condition) + val falseBranchGuard = mkAnd(activeGuard, mkNot(lhs.condition)) + val trueBranch = resolve(lhs.trueBranch, rhs, scope, trueBranchGuard) ?: return null + val falseBranch = resolve(lhs.falseBranch, rhs, scope, falseBranchGuard) ?: return null return lhs.ctx.mkIte( lhs.condition, trueBranch.asExpr(falseBranch.sort), @@ -69,8 +222,10 @@ sealed interface TsBinaryOperator { } if (rhs is UIteExpr<*>) { - val trueBranch = resolve(lhs, rhs.trueBranch, scope) ?: return null - val falseBranch = resolve(lhs, rhs.falseBranch, scope) ?: return null + val trueBranchGuard = mkAnd(activeGuard, rhs.condition) + val falseBranchGuard = mkAnd(activeGuard, mkNot(rhs.condition)) + val trueBranch = resolve(lhs, rhs.trueBranch, scope, trueBranchGuard) ?: return null + val falseBranch = resolve(lhs, rhs.falseBranch, scope, falseBranchGuard) ?: return null return lhs.ctx.mkIte( rhs.condition, trueBranch.asExpr(falseBranch.sort), @@ -82,7 +237,7 @@ sealed interface TsBinaryOperator { val rhsValue = rhs.extractSingleValueFromFakeObjectOrNull(scope) ?: rhs if (lhsValue.isFakeObject() || rhsValue.isFakeObject()) { - return resolveFakeObject(lhsValue, rhsValue, scope) + return resolveFakeObjectWithGuard(lhsValue, rhsValue, scope, activeGuard) } val lhsSort = lhsValue.sort @@ -90,7 +245,12 @@ sealed interface TsBinaryOperator { return when (lhsSort) { boolSort -> onBool(lhsValue.asExpr(boolSort), rhsValue.asExpr(boolSort), scope) fp64Sort -> onFp(lhsValue.asExpr(fp64Sort), rhsValue.asExpr(fp64Sort), scope) - addressSort -> onRef(lhsValue.asExpr(addressSort), rhsValue.asExpr(addressSort), scope) + addressSort -> onRefWithGuard( + lhsValue.asExpr(addressSort), + rhsValue.asExpr(addressSort), + scope, + activeGuard, + ) else -> TODO("Unsupported sort $lhsSort") } } @@ -98,11 +258,13 @@ sealed interface TsBinaryOperator { return internalResolve(lhsValue, rhsValue, scope) } + @Suppress("LongMethod") fun TsContext.commonResolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, resultSort: R, + activeGuard: UBoolExpr = trueExpr, reduce: (List>) -> UExpr, ): UExpr? { check(lhs.isFakeObject() || rhs.isFakeObject()) @@ -180,9 +342,10 @@ sealed interface TsBinaryOperator { ) // fake(ref) + fake(ref) - val refRefExpr = onRef(lhsRef, rhsRef, scope)?.asExpr(resultSort) ?: return null + val refRefGuard = mkAnd(activeGuard, lhsType.refTypeExpr, rhsType.refTypeExpr) + val refRefExpr = onRefWithGuard(lhsRef, rhsRef, scope, refRefGuard)?.asExpr(resultSort) ?: return null conjuncts += ExprWithTypeConstraint( - constraint = mkAnd(lhsType.refTypeExpr, rhsType.refTypeExpr), + constraint = refRefGuard, expr = refRefExpr ) } @@ -259,7 +422,12 @@ sealed interface TsBinaryOperator { ) // fake(ref) + ref - val refRefExpr = onRef(lhsRef, rhsRef, scope)?.asExpr(resultSort) ?: return null + val refRefExpr = onRefWithGuard( + lhsRef, + rhsRef, + scope, + mkAnd(activeGuard, lhsType.refTypeExpr), + )?.asExpr(resultSort) ?: return null conjuncts += ExprWithTypeConstraint( constraint = lhsType.refTypeExpr, expr = refRefExpr @@ -344,7 +512,12 @@ sealed interface TsBinaryOperator { ) // ref + fake(ref) - val refRefExpr = onRef(lhsRef, rhsRef, scope)?.asExpr(resultSort) ?: return null + val refRefExpr = onRefWithGuard( + lhsRef, + rhsRef, + scope, + mkAnd(activeGuard, rhsType.refTypeExpr), + )?.asExpr(resultSort) ?: return null conjuncts += ExprWithTypeConstraint( constraint = rhsType.refTypeExpr, expr = refRefExpr @@ -383,16 +556,24 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UBoolExpr { + ): UBoolExpr? = onRefWithGuard(lhs, rhs, scope, trueExpr) + + override fun TsContext.onRefWithGuard( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UBoolExpr? { // Note: in JavaScript, `null == undefined` val lhsIsNull = mkEq(lhs, mkTsNullValue()) val rhsIsNull = mkEq(rhs, mkTsNullValue()) val lhsIsUndefined = mkEq(lhs, mkUndefinedValue()) val rhsIsUndefined = mkEq(rhs, mkUndefinedValue()) + val referenceEquality = referenceOrStringValueEquals(lhs, rhs, scope, activeGuard) ?: return null return mkOr( mkAnd(lhsIsUndefined, rhsIsNull), mkAnd(lhsIsNull, rhsIsUndefined), - mkHeapRefEq(lhs, rhs) + referenceEquality, ) } @@ -400,21 +581,28 @@ sealed interface TsBinaryOperator { lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UBoolExpr { + ): UBoolExpr? = resolveFakeObjectWithGuard(lhs, rhs, scope, trueExpr) + + override fun TsContext.resolveFakeObjectWithGuard( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UBoolExpr? { return commonResolveFakeObject( lhs, rhs, scope, - boolSort + boolSort, + activeGuard, ) { conjuncts -> mkAnd(conjuncts.map { (condition, value) -> mkImplies(condition, value) }) } - ?: error("Should not be null") } override fun TsContext.internalResolve( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UBoolExpr { + ): UBoolExpr? { check(!lhs.isFakeObject() && !rhs.isFakeObject()) // bool == bool @@ -508,29 +696,47 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { return with(Eq) { - onRef(lhs, rhs, scope).not() + onRef(lhs, rhs, scope)?.not() } } + override fun TsContext.onRefWithGuard( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UExpr<*>? = with(Eq) { + onRefWithGuard(lhs, rhs, scope, activeGuard)?.not() + } + override fun TsContext.resolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { return with(Eq) { - resolveFakeObject(lhs, rhs, scope).not() + resolveFakeObject(lhs, rhs, scope)?.not() } } + override fun TsContext.resolveFakeObjectWithGuard( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UExpr<*>? = with(Eq) { + resolveFakeObjectWithGuard(lhs, rhs, scope, activeGuard)?.not() + } + override fun TsContext.internalResolve( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UExpr<*> { + ): UExpr<*>? { return with(Eq) { - internalResolve(lhs, rhs, scope).not() + internalResolve(lhs, rhs, scope)?.not() } } } @@ -556,15 +762,27 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UBoolExpr { - return mkHeapRefEq(lhs, rhs) - } + ): UBoolExpr? = onRefWithGuard(lhs, rhs, scope, trueExpr) + + override fun TsContext.onRefWithGuard( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UBoolExpr? = referenceOrStringValueEquals(lhs, rhs, scope, activeGuard) override fun TsContext.resolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UBoolExpr { + ): UBoolExpr? = resolveFakeObjectWithGuard(lhs, rhs, scope, trueExpr) + + override fun TsContext.resolveFakeObjectWithGuard( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UBoolExpr? { check(lhs.isFakeObject() || rhs.isFakeObject()) var lhsValue: UExpr<*> = lhs @@ -643,14 +861,17 @@ sealed interface TsBinaryOperator { if (lhsValue.sort == addressSort && rhsValue.sort == addressSort) { val left = lhsValue.asExpr(addressSort) val right = rhsValue.asExpr(addressSort) + val lhsRefGuard = if (lhs.isFakeObject()) lhs.getFakeType(scope).refTypeExpr else trueExpr + val rhsRefGuard = if (rhs.isFakeObject()) rhs.getFakeType(scope).refTypeExpr else trueExpr + val refComparisonGuard = mkAnd(activeGuard, typeConstraint, lhsRefGuard, rhsRefGuard) return mkAnd( typeConstraint, - mkHeapRefEq(left, right) + onRefWithGuard(left, right, scope, refComparisonGuard) ?: return null ) } val looseEqualityConstraint = with(Eq) { - resolve(lhsValue, rhsValue, scope)?.asExpr(boolSort) ?: error("Should not be encountered") + resolve(lhsValue, rhsValue, scope, activeGuard)?.asExpr(boolSort) ?: return null } return mkAnd(typeConstraint, looseEqualityConstraint) @@ -693,22 +914,40 @@ sealed interface TsBinaryOperator { lhs: UHeapRef, rhs: UHeapRef, scope: TsStepScope, - ): UBoolExpr { + ): UBoolExpr? { return with(StrictEq) { - onRef(lhs, rhs, scope).not() + onRef(lhs, rhs, scope)?.not() } } + override fun TsContext.onRefWithGuard( + lhs: UHeapRef, + rhs: UHeapRef, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UBoolExpr? = with(StrictEq) { + onRefWithGuard(lhs, rhs, scope, activeGuard)?.not() + } + override fun TsContext.resolveFakeObject( lhs: UExpr<*>, rhs: UExpr<*>, scope: TsStepScope, - ): UBoolExpr { + ): UBoolExpr? { return with(StrictEq) { - resolveFakeObject(lhs, rhs, scope).not() + resolveFakeObject(lhs, rhs, scope)?.not() } } + override fun TsContext.resolveFakeObjectWithGuard( + lhs: UExpr<*>, + rhs: UExpr<*>, + scope: TsStepScope, + activeGuard: UBoolExpr, + ): UBoolExpr? = with(StrictEq) { + resolveFakeObjectWithGuard(lhs, rhs, scope, activeGuard)?.not() + } + override fun TsContext.internalResolve( lhs: UExpr<*>, rhs: UExpr<*>, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 1c753d2e83..4dd9f42851 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -81,6 +81,13 @@ class TsState( * for identical string values. */ var stringConstantAllocatedRefs: UPersistentHashMap = persistentHashMapOf(), + /** + * References whose string backing and length bound have been modeled. + * A new symbolic string producer must register its reference here after creating the backing model. + * String literals are recognized separately through [TsContext.getStringConstantValue]. + */ + var boundedStringBackingRefs: Set = emptySet(), + var unsupportedReason: String? = null, private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( ctx = ctx, @@ -93,6 +100,14 @@ class TsState( forkPoints = forkPoints, targets = targets, ) { + /** Terminates a satisfiable path that the TypeScript model cannot execute soundly. */ + fun terminateAsUnsupported(reason: String) { + require(reason.isNotBlank()) + + unsupportedReason = reason + while (callStack.isNotEmpty()) callStack.pop() + } + fun getSortForLocal(idx: Int): USort? { val localToSort = localToSortStack.last() return localToSort[idx] @@ -308,6 +323,8 @@ class TsState( dfltObject = dfltObject, dfltObjectFieldSorts = dfltObjectFieldSorts, stringConstantAllocatedRefs = stringConstantAllocatedRefs, + boundedStringBackingRefs = boundedStringBackingRefs, + unsupportedReason = unsupportedReason, activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt new file mode 100644 index 0000000000..bf81ad5717 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt @@ -0,0 +1,277 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsTestResolver +import org.usvm.util.TsUnsupportedWitnessException +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import org.usvm.util.jsString +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsStringEqualityTest { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/StringEquality.ts") + private val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + private val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + throwExceptionOnStepFailure = true, + ) + + @Test + fun `string equality and inequality produce replayable witnesses`() { + val expected = mapOf) -> Int>( + "equalsA" to { args -> if (args[0] == "a") 1 else 2 }, + "notEqualsA" to { args -> if (args[0] != "a") 1 else 2 }, + "equalsEmpty" to { args -> if (args[0].isEmpty()) 1 else 2 }, + "equalsUnicode" to { args -> if (args[0] == "\uD83D\uDE00") 1 else 2 }, + "equalsOther" to { args -> if (args[0] == args[1]) 1 else 2 }, + "equalsAtLengthOne" to { args -> + if (args[0].length != 1 || args[1].length != 1) 3 else if (args[0] == args[1]) 1 else 2 + }, + "looselyEqualsOther" to { args -> if (args[0] == args[1]) 1 else 2 }, + "looselyNotEqualsOther" to { args -> if (args[0] != args[1]) 1 else 2 }, + ) + val tests = expected.mapValues { (name, _) -> analyze(name) } + + tests.forEach { (name, generated) -> + val expectedResults = if (name == "equalsAtLengthOne") setOf(1, 2, 3) else setOf(1, 2) + assertEquals(expectedResults, generated.map { resultNumber(it) }.toSet(), name) + generated.forEach { test -> + val inputs = test.before.parameters.map { assertIs(it).value } + assertEquals(expected.getValue(name)(inputs), resultNumber(test), "$name: $test") + } + } + + replay(tests) + } + + @Test + fun `null and undefined strict and loose equality remain distinct`() { + val tests = mapOf("nullAndUndefined" to analyze("nullAndUndefined")) + + assertEquals(setOf(2), tests.getValue("nullAndUndefined").map(::resultNumber).toSet()) + + replay(tests) + } + + @Test + fun `default string bound can compare two symbolic inputs`() { + val tests = analyze("equalsOther", maxStringLength = 1_000) + + assertEquals(setOf(1, 2), tests.map(::resultNumber).toSet()) + + replay(mapOf("equalsOther" to tests)) + } + + @Test + fun `any and unknown string alternatives are explicit unsupported paths`() { + val generated = listOf("equalsAnyStrings", "equalsUnknownStrings").associateWith { name -> + val method = scene.projectClasses.single { it.name == "StringEquality" } + .methods + .single { it.name == name } + val analysis = TsMachine( + scene, + options = options.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), + tsOptions = TsOptions(maxArraySize = 4), + ).use { machine -> + machine.analyzeWithOutcome(listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason, name) + assertTrue(analysis.unsupportedPaths.any { "modeled string backing" in it }, name) + val tests = analysis.states.map { state -> TsTestResolver().resolve(method, state) } + assertTrue(tests.isNotEmpty(), name) + assertTrue(tests.all { resultNumber(it) == 3 }, "$name: $tests") + + tests + } + + replayDynamic(generated) + replayLongMismatch() + + val method = scene.projectClasses.single { it.name == "StringEquality" } + .methods + .single { it.name == "equalsAnyStrings" } + val ordinaryStates = TsMachine( + scene, + options = options, + tsOptions = TsOptions(maxArraySize = 4), + ).use { machine -> + machine.analyze(listOf(method)) + } + val ordinaryTests = ordinaryStates.map { state -> TsTestResolver().resolve(method, state) } + assertTrue(ordinaryTests.none { resultNumber(it) in setOf(1, 2) }) + } + + @Test + fun `two unmodeled string references do not yield equality witnesses`() { + val method = scene.projectClasses.single { it.name == "StringEquality" } + .methods + .single { it.name == "looselyEqualsDynamicStrings" } + val analysis = TsMachine( + scene, + options = options.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), + tsOptions = TsOptions(maxArraySize = 4), + ).use { machine -> + machine.analyzeWithOutcome(listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.any { "modeled string backing" in it }) + val unsupportedWitnesses = mutableListOf() + val tests = analysis.states.mapNotNull { state -> + try { + TsTestResolver().resolve(method, state) + } catch (failure: TsUnsupportedWitnessException) { + unsupportedWitnesses += failure + null + } + } + + assertTrue(unsupportedWitnesses.isNotEmpty(), "Expected an unbacked string witness") + assertTrue(unsupportedWitnesses.all { "missing backing array" in it.message.orEmpty() }) + assertTrue(tests.none { resultNumber(it) in setOf(1, 2) }, "$tests") + } + + @Test + fun `unsupported fork does not consume covered-new slot or stop before supported result`() { + val method = scene.projectClasses.single { it.name == "StringEquality" } + .methods + .single { it.name == "equalsAnyDirect" } + val analysis = TsMachine( + scene, + options = options.copy(collectedStatesLimit = 1), + tsOptions = TsOptions(maxArraySize = 4), + ).use { machine -> + machine.analyzeWithOutcome(listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.any { "modeled string backing" in it }) + val tests = analysis.states.map { state -> TsTestResolver().resolve(method, state) } + val supported = tests.filter { test -> + test.before.parameters[0] !is TsTestValue.TsString && resultNumber(test) == 2 + } + assertTrue(supported.isNotEmpty(), "$tests") + + replayDynamic(mapOf("equalsAnyDirect" to supported)) + } + + private fun analyze(name: String, maxStringLength: Int = 4): List { + val method = scene.projectClasses.single { it.name == "StringEquality" } + .methods + .single { it.name == name } + val analysis = TsMachine( + scene, + options = options, + tsOptions = TsOptions(maxArraySize = maxStringLength), + ).use { machine -> + machine.analyzeWithOutcome(listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason, name) + assertTrue(analysis.states.isNotEmpty(), name) + assertTrue(analysis.states.all { it.methodResult is TsMethodResult.Success }, name) + + return analysis.states.map { state -> TsTestResolver().resolve(method, state) } + } + + private fun resultNumber(test: TsTest): Int = + assertIs(test.returnValue).number.toInt() + + private fun replay(tests: Map>) { + val script = buildString { + appendLine(source.readText()) + tests.forEach { (name, generated) -> + generated.forEachIndexed { index, test -> + val args = test.before.parameters.joinToString { value -> + jsString(assertIs(value).value) + } + val expected = resultNumber(test) + + appendLine("if (new StringEquality().$name($args) !== $expected) {") + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "string-equality", + timeoutMessage = "Node replay timed out", + ) + } + + private fun replayDynamic(tests: Map>) { + val script = buildString { + appendLine(source.readText()) + tests.forEach { (name, generated) -> + generated.forEachIndexed { index, test -> + val left = jsDynamic(test.before.parameters[0]) + val right = jsString(assertIs(test.before.parameters[1]).value) + + appendLine("if (new StringEquality().$name($left, $right) !== ${resultNumber(test)}) {") + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "dynamic-string-equality", + timeoutMessage = "Node replay timed out", + ) + } + + private fun jsDynamic(value: TsTestValue): String = when (value) { + is TsTestValue.TsBoolean -> value.value.toString() + is TsTestValue.TsNumber -> value.number.toString() + TsTestValue.TsNull -> "null" + TsTestValue.TsUndefined -> "undefined" + is TsTestValue.TsClass -> "{}" + is TsTestValue.TsArray<*> -> "[]" + else -> error("Unexpected string alternative: $value") + } + + private fun replayLongMismatch() { + val script = buildString { + appendLine(source.readText()) + appendLine("const left = 'a'.repeat(4) + 'x';") + appendLine("const right = 'a'.repeat(4) + 'y';") + appendLine("if (new StringEquality().equalsAnyStrings(left, right) !== 2) throw Error('long any');") + appendLine("if (new StringEquality().equalsUnknownStrings(left, right) !== 2) throw Error('long unknown');") + } + + assertNodeReplay( + source = script, + directory = directory, + name = "long-string-equality", + timeoutMessage = "Node replay timed out", + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt index 4abb82bb0b..083104b732 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallDispatcherTest.kt @@ -28,6 +28,7 @@ import org.usvm.UMachineOptions import org.usvm.api.targets.ReachabilityObserver import org.usvm.api.targets.TsReachabilityTarget import org.usvm.isTrue +import org.usvm.machine.TsAnalysisStopReason import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions @@ -52,6 +53,38 @@ class TsUnknownCallDispatcherTest { ) private val fullScene = EtsScene(listOf(sourceFile)) + @Test + fun `unsupported model exception is reported without a successful state`() { + val method = method(fullScene, "declaredMethodWithoutBodyContinues") + val dispatcher = TsUnknownCallDispatcher { _, _ -> + throw UnsupportedOperationException("The call model is not implemented") + } + + val outcome = TsMachine( + scene = fullScene, + options = allStatesMachineOptions, + tsOptions = TsOptions(), + unknownCallDispatcher = dispatcher, + ).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertEquals(listOf("The call model is not implemented"), outcome.unsupportedPaths) + + assertFailsWith { + TsMachine( + scene = fullScene, + options = allStatesMachineOptions.copy(throwExceptionOnStepFailure = true), + tsOptions = TsOptions(), + unknownCallDispatcher = dispatcher, + ).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + } + } + @Test fun `every model or fallback decision is reported through the interpreter observer`() { val cases = listOf( diff --git a/usvm-ts/src/test/resources/models/StringEquality.ts b/usvm-ts/src/test/resources/models/StringEquality.ts new file mode 100644 index 0000000000..b861925d4f --- /dev/null +++ b/usvm-ts/src/test/resources/models/StringEquality.ts @@ -0,0 +1,58 @@ +class StringEquality { + equalsA(value: string): number { + return value === "a" ? 1 : 2; + } + + notEqualsA(value: string): number { + return value !== "a" ? 1 : 2; + } + + equalsEmpty(value: string): number { + return value === "" ? 1 : 2; + } + + equalsUnicode(value: string): number { + return value === "\uD83D\uDE00" ? 1 : 2; + } + + equalsOther(left: string, right: string): number { + return left === right ? 1 : 2; + } + + equalsAtLengthOne(left: string, right: string): number { + if (left.length !== 1 || right.length !== 1) return 3; + + return left === right ? 1 : 2; + } + + looselyEqualsOther(left: string, right: string): number { + return left == right ? 1 : 2; + } + + looselyNotEqualsOther(left: string, right: string): number { + return left != right ? 1 : 2; + } + + equalsAnyStrings(left: any, right: string): number { + if (typeof left !== "string") return 3; + return left === right ? 1 : 2; + } + + equalsUnknownStrings(left: unknown, right: string): number { + if (typeof left !== "string") return 3; + return left === right ? 1 : 2; + } + + equalsAnyDirect(left: any, right: string): number { + return left === right ? 1 : 2; + } + + looselyEqualsDynamicStrings(left: any, right: any): number { + if (typeof left !== "string" || typeof right !== "string") return 3; + return left == right ? 1 : 2; + } + + nullAndUndefined(): number { + return null === undefined ? 1 : null == undefined ? 2 : 3; + } +} From da7376df11d98070ea137d3a565cca6ff97d5d8c Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 4 Oct 2026 01:00:47 +0300 Subject: [PATCH 08/20] [TS] Check string equality through discoverProperties --- .../org/usvm/machine/TsStringEqualityTest.kt | 59 ++++++++++++++++--- 1 file changed, 51 insertions(+), 8 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt index bf81ad5717..a559ed3107 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt @@ -12,6 +12,7 @@ import org.usvm.UMachineOptions import org.usvm.api.TsTest import org.usvm.api.TsTestValue import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsMethodTestRunner import org.usvm.util.TsTestResolver import org.usvm.util.TsUnsupportedWitnessException import org.usvm.util.assertNodeReplay @@ -24,13 +25,13 @@ import kotlin.test.assertIs import kotlin.test.assertTrue import kotlin.time.Duration -class TsStringEqualityTest { +class TsStringEqualityTest : TsMethodTestRunner() { @TempDir lateinit var directory: Path private val source = getResourcePath("/models/StringEquality.ts") - private val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) - private val options = UMachineOptions( + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + private val analysisOptions = UMachineOptions( pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), solverType = SolverType.YICES, solverTimeout = Duration.INFINITE, @@ -52,6 +53,36 @@ class TsStringEqualityTest { "looselyEqualsOther" to { args -> if (args[0] == args[1]) 1 else 2 }, "looselyNotEqualsOther" to { args -> if (args[0] != args[1]) 1 else 2 }, ) + + expected.forEach { (name, expectedResult) -> + val method = getMethod(methodName = name, className = "StringEquality") + if (name == "equalsOther" || name == "equalsAtLengthOne" || + name == "looselyEqualsOther" || name == "looselyNotEqualsOther") { + val results = if (name == "equalsAtLengthOne") listOf(1, 2, 3) else listOf(1, 2) + discoverProperties( + method = method, + *results.map { expectedNumber -> + { left: TsTestValue.TsString, right: TsTestValue.TsString, result: TsTestValue.TsNumber -> + result.number == expectedNumber.toDouble() && + result.number == expectedResult(listOf(left.value, right.value)).toDouble() + } + }.toTypedArray(), + invariants = arrayOf({ left, right, result -> + result.number == expectedResult(listOf(left.value, right.value)).toDouble() + }), + ) + } else { + discoverProperties( + method = method, + { input, result -> result.number == 1.0 && expectedResult(listOf(input.value)) == 1 }, + { input, result -> result.number == 2.0 && expectedResult(listOf(input.value)) == 2 }, + invariants = arrayOf({ input, result -> + result.number == expectedResult(listOf(input.value)).toDouble() + }), + ) + } + } + val tests = expected.mapValues { (name, _) -> analyze(name) } tests.forEach { (name, generated) -> @@ -68,6 +99,12 @@ class TsStringEqualityTest { @Test fun `null and undefined strict and loose equality remain distinct`() { + discoverProperties( + method = getMethod(methodName = "nullAndUndefined", className = "StringEquality"), + { result -> result.number == 2.0 }, + invariants = arrayOf({ result -> result.number == 2.0 }), + ) + val tests = mapOf("nullAndUndefined" to analyze("nullAndUndefined")) assertEquals(setOf(2), tests.getValue("nullAndUndefined").map(::resultNumber).toSet()) @@ -77,6 +114,12 @@ class TsStringEqualityTest { @Test fun `default string bound can compare two symbolic inputs`() { + discoverProperties( + method = getMethod(methodName = "equalsOther", className = "StringEquality"), + { left, right, result -> left.value == right.value && result.number == 1.0 }, + { left, right, result -> left.value != right.value && result.number == 2.0 }, + ) + val tests = analyze("equalsOther", maxStringLength = 1_000) assertEquals(setOf(1, 2), tests.map(::resultNumber).toSet()) @@ -92,7 +135,7 @@ class TsStringEqualityTest { .single { it.name == name } val analysis = TsMachine( scene, - options = options.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), + options = analysisOptions.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), tsOptions = TsOptions(maxArraySize = 4), ).use { machine -> machine.analyzeWithOutcome(listOf(method)) @@ -115,7 +158,7 @@ class TsStringEqualityTest { .single { it.name == "equalsAnyStrings" } val ordinaryStates = TsMachine( scene, - options = options, + options = analysisOptions, tsOptions = TsOptions(maxArraySize = 4), ).use { machine -> machine.analyze(listOf(method)) @@ -131,7 +174,7 @@ class TsStringEqualityTest { .single { it.name == "looselyEqualsDynamicStrings" } val analysis = TsMachine( scene, - options = options.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), + options = analysisOptions.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), tsOptions = TsOptions(maxArraySize = 4), ).use { machine -> machine.analyzeWithOutcome(listOf(method)) @@ -161,7 +204,7 @@ class TsStringEqualityTest { .single { it.name == "equalsAnyDirect" } val analysis = TsMachine( scene, - options = options.copy(collectedStatesLimit = 1), + options = analysisOptions.copy(collectedStatesLimit = 1), tsOptions = TsOptions(maxArraySize = 4), ).use { machine -> machine.analyzeWithOutcome(listOf(method)) @@ -184,7 +227,7 @@ class TsStringEqualityTest { .single { it.name == name } val analysis = TsMachine( scene, - options = options, + options = analysisOptions, tsOptions = TsOptions(maxArraySize = maxStringLength), ).use { machine -> machine.analyzeWithOutcome(listOf(method)) From e5527a3b67f476045aebea61a66bdc6e93c7b965 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 4 Oct 2026 01:31:28 +0300 Subject: [PATCH 09/20] [TS] Format discoverProperties string equality checks --- .../org/usvm/machine/TsStringEqualityTest.kt | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt index a559ed3107..6b65a64be0 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringEqualityTest.kt @@ -54,15 +54,26 @@ class TsStringEqualityTest : TsMethodTestRunner() { "looselyNotEqualsOther" to { args -> if (args[0] != args[1]) 1 else 2 }, ) + val twoParameterMethods = setOf( + "equalsOther", + "equalsAtLengthOne", + "looselyEqualsOther", + "looselyNotEqualsOther", + ) + expected.forEach { (name, expectedResult) -> val method = getMethod(methodName = name, className = "StringEquality") - if (name == "equalsOther" || name == "equalsAtLengthOne" || - name == "looselyEqualsOther" || name == "looselyNotEqualsOther") { + + if (name in twoParameterMethods) { val results = if (name == "equalsAtLengthOne") listOf(1, 2, 3) else listOf(1, 2) discoverProperties( method = method, *results.map { expectedNumber -> - { left: TsTestValue.TsString, right: TsTestValue.TsString, result: TsTestValue.TsNumber -> + { + left: TsTestValue.TsString, + right: TsTestValue.TsString, + result: TsTestValue.TsNumber, + -> result.number == expectedNumber.toDouble() && result.number == expectedResult(listOf(left.value, right.value)).toDouble() } From d527c48853f1d309f67cba4bf6d30bc326d1fdb3 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 03:08:18 +0300 Subject: [PATCH 10/20] [TS] Evaluate instanceof against runtime constructor values --- .../main/kotlin/org/usvm/machine/TsContext.kt | 13 ++ .../org/usvm/machine/expr/TsExprResolver.kt | 128 +++++++++---- .../samples/types/RuntimeInstanceofTest.kt | 169 ++++++++++++++++++ .../samples/types/RuntimeInstanceof.ts | 52 ++++++ 4 files changed, 323 insertions(+), 39 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 66184e3d19..ba1114837c 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 @@ -19,6 +19,8 @@ import org.jacodb.ets.model.EtsBooleanConstant import org.jacodb.ets.model.EtsCastExpr import org.jacodb.ets.model.EtsCaughtExceptionRef 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 @@ -89,6 +91,7 @@ import org.usvm.api.allocateConcreteRef import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArrayLength import org.usvm.api.makeSymbolicPrimitive +import org.usvm.api.typeStreamOf import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type import org.usvm.isAllocatedConcreteHeapRef @@ -114,6 +117,7 @@ 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.util.EtsHierarchy import org.usvm.util.SymbolResolutionResult import org.usvm.util.isResolved @@ -208,6 +212,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) } @@ -375,47 +381,49 @@ class TsExprResolver( return mkStringConstant("boolean", scope) } if (arg.sort == addressSort) { - val ref = arg.asExpr(addressSort) - return mkIte( - condition = mkHeapRefEq(ref, mkTsNullValue()), - trueBranch = mkStringConstant("object", scope), - falseBranch = mkIte( - condition = mkHeapRefEq(ref, mkUndefinedValue()), - trueBranch = mkStringConstant("undefined", scope), - falseBranch = mkIte( - condition = scope.calcOnState { - val unwrappedRef = ref.unwrapRefWithPathConstraint(scope) - - // TODO: adhoc: "expand" ITE - if (unwrappedRef is UIteExpr<*>) { - val trueBranch = unwrappedRef.trueBranch - val falseBranch = unwrappedRef.falseBranch - if (trueBranch.isFakeObject() || falseBranch.isFakeObject()) { - val unwrappedTrueExpr = - trueBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) - val unwrappedFalseExpr = - falseBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) - return@calcOnState mkIte( - condition = unwrappedRef.condition, - trueBranch = memory.types.evalTypeEquals(unwrappedTrueExpr, EtsStringType), - falseBranch = memory.types.evalTypeEquals(unwrappedFalseExpr, EtsStringType), - ) - } - } - - memory.types.evalTypeEquals(unwrappedRef, EtsStringType) - }, - trueBranch = mkStringConstant("string", scope), - falseBranch = mkStringConstant("object", scope), - ) - ) - ) + return resolveReferenceTypeof(arg.asExpr(addressSort)) } logger.error { "visit(${expr::class.simpleName}) is not implemented yet" } error("Not supported $expr") } + private fun resolveReferenceTypeof(ref: UHeapRef): UExpr = with(ctx) { + val functionValue = mkStringConstant("function", scope) + if (ref is UConcreteHeapRef && classConstructorSignature(ref) != null) return functionValue + + val objectValue = mkStringConstant("object", scope) + val stringValue = mkStringConstant("string", scope) + val undefinedValue = mkStringConstant("undefined", scope) + + val isClassConstructor = classConstructorRefs() + .map { constructorRef -> mkHeapRefEq(ref, constructorRef) } + .let { matches -> if (matches.isEmpty()) falseExpr else mkOr(matches) } + val isString = scope.calcOnState { + val unwrappedRef = ref.unwrapRefWithPathConstraint(scope) + val ite = unwrappedRef as? UIteExpr<*> + + // TODO: adhoc: "expand" ITE + if (ite != null && (ite.trueBranch.isFakeObject() || ite.falseBranch.isFakeObject())) { + val unwrappedTrueExpr = ite.trueBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) + val unwrappedFalseExpr = ite.falseBranch.asExpr(addressSort).unwrapRefWithPathConstraint(scope) + mkIte( + condition = ite.condition, + trueBranch = memory.types.evalTypeEquals(unwrappedTrueExpr, EtsStringType), + falseBranch = memory.types.evalTypeEquals(unwrappedFalseExpr, EtsStringType), + ) + } else { + memory.types.evalTypeEquals(unwrappedRef, EtsStringType) + } + } + val isUndefined = mkHeapRefEq(ref, mkUndefinedValue()) + val isNull = mkHeapRefEq(ref, mkTsNullValue()) + val objectOrString = mkIte(isString, stringValue, objectValue) + val objectOrFunction = mkIte(isClassConstructor, functionValue, objectOrString) + val notNull = mkIte(isUndefined, undefinedValue, objectOrFunction) + mkIte(isNull, objectValue, notNull) + } + override fun visit(expr: EtsDeleteExpr): UExpr? = with(ctx) { logger.warn { "delete operator is not fully supported, the result may not be accurate" @@ -888,12 +896,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 @@ -1311,6 +1359,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 b60b14e9c3334ef285918b2914502548d8efe820 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 03:39:03 +0300 Subject: [PATCH 11/20] [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 ba1114837c..dc94db7cc3 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.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 @@ -332,6 +333,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}") @@ -920,7 +929,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 82205d62d3a2fc68c85a2fd289444d26733ff626 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 04:02:27 +0300 Subject: [PATCH 12/20] [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 dc94db7cc3..52b12c5183 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,7 +21,6 @@ import org.jacodb.ets.model.EtsCaughtExceptionRef 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 @@ -333,10 +332,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 } @@ -938,7 +934,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 ea519907adbdacee542248082cd1c5e121d154d5 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 04:27:45 +0300 Subject: [PATCH 13/20] [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 52b12c5183..2d989fce10 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 @@ -935,6 +935,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 50436384931e4d2875a17e0effc5bf0ece1de6fd Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 04:50:57 +0300 Subject: [PATCH 14/20] [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 2d989fce10..8d2afea47e 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 @@ -935,6 +935,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 0a3e516173f7154cf276fce863aba92bcb89668e Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 05:31:36 +0300 Subject: [PATCH 15/20] 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 | 89 ++++++++++---- .../samples/types/RuntimeInstanceofTest.kt | 114 ++++++++++++++++-- .../kotlin/org/usvm/util/TsTestResolver.kt | 10 ++ .../samples/types/RuntimeInstanceof.ts | 65 ++++++++++ 6 files changed, 292 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 8d2afea47e..40d6f20d92 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 @@ -18,6 +18,7 @@ import org.jacodb.ets.model.EtsBitXorExpr import org.jacodb.ets.model.EtsBooleanConstant import org.jacodb.ets.model.EtsCastExpr 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 @@ -95,6 +96,7 @@ import org.usvm.api.typeStreamOf import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.machine.TS_TYPE_ERROR_TYPE import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext import org.usvm.machine.TsOptions @@ -909,29 +911,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 @@ -976,6 +956,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 1e45549f0e..ab0c7b129c 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.TsUnresolvedSort import org.usvm.machine.expr.extractDouble @@ -143,6 +144,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 0544984235a6f480886139beaa29fb6bb9dc7ee3 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 06:07:57 +0300 Subject: [PATCH 16/20] 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 dfb0e15f6c09dda17acd70b73eb973dec2cecc73 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 06:27:59 +0300 Subject: [PATCH 17/20] 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 bcc2f508b9d3df3a45c16c671ea4f0e1907dff48 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 06:43:24 +0300 Subject: [PATCH 18/20] [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 40d6f20d92..9f94f38c80 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 @@ -973,9 +973,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 f408fcc3dacd1773d4c070862300dc3d392f4548 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 08:51:55 +0300 Subject: [PATCH 19/20] [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 bab79630bbf10cb08559ce1410cf69c1e3c2601e Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 4 Oct 2026 01:22:48 +0300 Subject: [PATCH 20/20] [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"))) }