From 06029907787f959fa976f551ea189a928af74dba Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 2 Oct 2026 20:01:50 +0300 Subject: [PATCH 01/11] [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/11] [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/11] [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/11] [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/11] [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/11] [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/11] [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 1d689254a7a7ce3052f5703c98e1d4b68aac19f7 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 02:24:37 +0300 Subject: [PATCH 08/11] [TS] Route thrown values to catch handlers --- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- .../org/usvm/machine/expr/TsExprResolver.kt | 4 +- .../usvm/machine/interpreter/TsInterpreter.kt | 47 +++---- .../kotlin/org/usvm/machine/state/TsState.kt | 3 + .../org/usvm/machine/TsCatchRoutingTest.kt | 118 ++++++++++++++++++ .../org/usvm/samples/lang/Exceptions.kt | 40 ++++++ .../test/resources/samples/lang/Exceptions.ts | 55 ++++++++ 7 files changed, 235 insertions(+), 34 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index 700801642a..c191b31b46 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/buildSrc/src/main/kotlin/Dependencies.kt @@ -6,7 +6,7 @@ object Versions { const val clikt = "5.0.0" const val detekt = "1.23.7" const val ini4j = "0.5.4" - const val jacodb = "ddb127d9ef" + const val jacodb = "7a2cda3bfd9175ba11a60e47ff4a32e6e3e209e2" const val juliet = "1.3.2" const val junit = "5.9.3" const val kotlin = "2.1.0" 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..b07571789c 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 @@ -1023,8 +1023,8 @@ class TsExprResolver( override fun visit(value: EtsStaticFieldRef): UExpr<*>? = handleStaticFieldRef(value) override fun visit(value: EtsCaughtExceptionRef): UExpr? { - logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } - error("Not supported $value") + return scope.calcOnState { caughtException } + ?: throw UnsupportedOperationException("Caught exception value is unavailable") } override fun visit(value: EtsGlobalRef): UExpr? { 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 b15e04d2b1..c07ee50a9c 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 @@ -110,11 +110,17 @@ class TsInterpreter( val result = state.methodResult if (result is TsMethodResult.TsException) { - // TODO catch processing scope.doWithState { + val catcher = stmt.location.method.cfg.catchers(stmt).singleOrNull() + if (catcher != null) { + caughtException = result.value + methodResult = TsMethodResult.NoCall + newStmt(catcher) + return@doWithState + } + leaveUnknownCallModelIfReturning() val returnSite = callStack.pop() - if (callStack.isNotEmpty()) { memory.stack.pop() popLocalToSortStack() @@ -699,37 +705,16 @@ class TsInterpreter( observer?.onThrowStatement(exprResolver.simpleValueResolver, stmt, scope) - val exception = exprResolver.resolve(stmt.exception) - - // Pop the call stack to return to the caller - scope.doWithState { - memory.stack.pop() + val exception = exprResolver.resolve(stmt.exception) ?: return + val exceptionType: EtsType = when (exception.sort) { + ctx.addressSort -> EtsStringType // TODO: improve object type detection + ctx.fp64Sort -> EtsNumberType + ctx.boolSort -> EtsBooleanType + else -> EtsStringType } - if (exception != null) { - val exceptionType: EtsType = when (exception.sort) { - ctx.addressSort -> { - // If it's an object reference, try to determine its type - val ref = exception.asExpr(ctx.addressSort) - // For now, assume it's a generic error type - EtsStringType // TODO: improve type detection - } - - ctx.fp64Sort -> EtsNumberType - - ctx.boolSort -> EtsBooleanType - - else -> EtsStringType - } - - scope.doWithState { - methodResult = TsMethodResult.TsException(exception, exceptionType) - } - } else { - scope.doWithState { - // If we couldn't resolve the exception value, throw a generic exception - methodResult = TsMethodResult.TsException(ctx.mkUndefinedValue(), EtsStringType) - } + scope.doWithState { + methodResult = TsMethodResult.TsException(exception, exceptionType) } } 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 4dd9f42851..7edc418129 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 @@ -87,6 +87,8 @@ class TsState( * String literals are recognized separately through [TsContext.getStringConstantValue]. */ var boundedStringBackingRefs: Set = emptySet(), + /** Exception delivered to the current catch block, before its binding is initialized. */ + var caughtException: UExpr<*>? = null, var unsupportedReason: String? = null, private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( @@ -324,6 +326,7 @@ class TsState( dfltObjectFieldSorts = dfltObjectFieldSorts, stringConstantAllocatedRefs = stringConstantAllocatedRefs, boundedStringBackingRefs = boundedStringBackingRefs, + caughtException = caughtException, unsupportedReason = unsupportedReason, activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt new file mode 100644 index 0000000000..dedd2967d1 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt @@ -0,0 +1,118 @@ +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.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 TsCatchRoutingTest { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/samples/lang/Exceptions.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, + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + + @Test + fun `catch paths retain the thrown value and replay in Node`() { + val tests = listOf("conditionalCatch", "caughtValue", "nestedCatch", "catchesCall", "rethrowToOuter") + .associateWith(::analyze) + + assertEquals(setOf(1, 2), tests.getValue("conditionalCatch").map(::resultNumber).toSet()) + tests.forEach { (name, generated) -> + generated.forEach { test -> assertExpectedResult(name, test) } + } + + replay(tests) + } + + private fun assertExpectedResult(name: String, test: TsTest) { + val input = assertIs(test.before.parameters.single()).number + val expected = when (name) { + "conditionalCatch" -> if (input == 0.0) 2.0 else 1.0 + "caughtValue", "nestedCatch", "catchesCall", "rethrowToOuter" -> input + 1.0 + else -> error("Unexpected method $name") + } + + assertEquals(expected, assertIs(test.returnValue).number, "$name: $test") + } + + private fun analyze(name: String): List { + val method = scene.projectClasses.single { it.name == "Exceptions" } + .methods + .single { it.name == name } + val result = TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(), + ).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason, name) + assertTrue(result.unsupportedPaths.isEmpty(), "$name: ${result.unsupportedPaths}") + assertTrue(result.states.isNotEmpty(), name) + assertTrue(result.states.all { it.methodResult is TsMethodResult.Success }, name) + + return result.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 input = assertIs(test.before.parameters.single()).number + val expected = assertIs(test.returnValue).number + + appendLine("if (new Exceptions().$name($input) !== $expected) {") + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } + } + } + val replay = directory.resolve("catch-routing.ts") + val output = directory.resolve("catch-routing.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), "Node replay timed out") + assertEquals(0, process.exitValue(), output.readText()) + } finally { + if (process.isAlive) process.destroyForcibly() + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Exceptions.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Exceptions.kt index 9bf6919809..b243547c85 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Exceptions.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/Exceptions.kt @@ -98,4 +98,44 @@ class Exceptions : TsMethodTestRunner() { }, ) } + + @Test + fun `conditional catch only handles the throwing path`() { + val method = getMethod("conditionalCatch") + + discoverProperties( + method = method, + { value, result -> (value eq 0) && (result eq 2) }, + { value, result -> !(value eq 0) && (result eq 1) }, + invariants = arrayOf( + { value, result -> if (value eq 0) result eq 2 else result eq 1 }, + ), + ) + } + + @Test + fun `catch binding receives the thrown number`() { + val method = getMethod("caughtValue") + + discoverProperties( + method = method, + { value, result -> result eq (value.number + 1.0) }, + invariants = arrayOf( + { value, result -> result eq (value.number + 1.0) }, + ), + ) + } + + @Test + fun `nested catch uses the nearest handler`() { + val method = getMethod("nestedCatch") + + discoverProperties( + method = method, + { value, result -> result eq (value.number + 1.0) }, + invariants = arrayOf( + { value, result -> result eq (value.number + 1.0) }, + ), + ) + } } diff --git a/usvm-ts/src/test/resources/samples/lang/Exceptions.ts b/usvm-ts/src/test/resources/samples/lang/Exceptions.ts index 898ae1a3e2..cb2d27af54 100644 --- a/usvm-ts/src/test/resources/samples/lang/Exceptions.ts +++ b/usvm-ts/src/test/resources/samples/lang/Exceptions.ts @@ -38,4 +38,59 @@ class Exceptions { } return 42; } + + conditionalCatch(value: number): number { + try { + if (value === 0) { + throw 7; + } + return 1; + } catch { + return 2; + } + } + + caughtValue(value: number): number { + try { + throw value; + } catch (error) { + return error + 1; + } + } + + nestedCatch(value: number): number { + try { + try { + throw value; + } catch (inner) { + return inner + 1; + } + } catch (outer) { + return 99; + } + } + + throwsValue(value: number): number { + throw value; + } + + catchesCall(value: number): number { + try { + return this.throwsValue(value); + } catch (error) { + return error + 1; + } + } + + rethrowToOuter(value: number): number { + try { + try { + throw value; + } catch (inner) { + throw inner; + } + } catch (outer) { + return outer + 1; + } + } } From 2d655b8417985dad788044684fc3a3fda4aff7a3 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 02:53:51 +0300 Subject: [PATCH 09/11] [TS] Satisfy catch routing lint rule --- .../main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 c07ee50a9c..c16d96dd05 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 @@ -111,7 +111,8 @@ class TsInterpreter( val result = state.methodResult if (result is TsMethodResult.TsException) { scope.doWithState { - val catcher = stmt.location.method.cfg.catchers(stmt).singleOrNull() + val catchers = stmt.location.method.cfg.catchers(stmt) + val catcher = catchers.singleOrNull() if (catcher != null) { caughtException = result.value methodResult = TsMethodResult.NoCall From 253e55a72435c5c0aa7cf996b36f1ee745d15c83 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 08:50:30 +0300 Subject: [PATCH 10/11] [TS] Reuse Node replay helper in catch routing tests Keep catch witness assertions and use the shared Node process harness. --- .../org/usvm/machine/TsCatchRoutingTest.kt | 23 ++++++------------- 1 file changed, 7 insertions(+), 16 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt index dedd2967d1..626c3d7fd9 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt @@ -13,11 +13,10 @@ 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.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 @@ -100,19 +99,11 @@ class TsCatchRoutingTest { } } } - val replay = directory.resolve("catch-routing.ts") - val output = directory.resolve("catch-routing.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), "Node replay timed out") - assertEquals(0, process.exitValue(), output.readText()) - } finally { - if (process.isAlive) process.destroyForcibly() - } + assertNodeReplay( + source = script, + directory = directory, + name = "catch-routing", + timeoutMessage = "Node replay timed out", + ) } } From f28990332524479fbd30b11f7f19fe40ee55471b Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sun, 4 Oct 2026 00:50:43 +0300 Subject: [PATCH 11/11] [TS] Check catch results through discoverProperties --- .../org/usvm/machine/TsCatchRoutingTest.kt | 26 ++++++++++++++++--- 1 file changed, 22 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt index 626c3d7fd9..da171b11a3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsCatchRoutingTest.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.assertNodeReplay import org.usvm.util.getResourcePath @@ -22,13 +23,13 @@ import kotlin.test.assertIs import kotlin.test.assertTrue import kotlin.time.Duration -class TsCatchRoutingTest { +class TsCatchRoutingTest : TsMethodTestRunner() { @TempDir lateinit var directory: Path private val source = getResourcePath("/samples/lang/Exceptions.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, @@ -40,6 +41,23 @@ class TsCatchRoutingTest { @Test fun `catch paths retain the thrown value and replay in Node`() { + val conditionalCatch = getMethod(methodName = "conditionalCatch", className = "Exceptions") + discoverProperties( + method = conditionalCatch, + { input, result -> input.number == 0.0 && result.number == 2.0 }, + { input, result -> input.number != 0.0 && result.number == 1.0 }, + invariants = arrayOf({ input, result -> result.number == (if (input.number == 0.0) 2.0 else 1.0) }), + ) + + for (name in listOf("caughtValue", "nestedCatch", "catchesCall", "rethrowToOuter")) { + val method = getMethod(methodName = name, className = "Exceptions") + discoverProperties( + method = method, + { input, result -> result.number == input.number + 1.0 }, + invariants = arrayOf({ input, result -> result.number == input.number + 1.0 }), + ) + } + val tests = listOf("conditionalCatch", "caughtValue", "nestedCatch", "catchesCall", "rethrowToOuter") .associateWith(::analyze) @@ -68,7 +86,7 @@ class TsCatchRoutingTest { .single { it.name == name } val result = TsMachine( scene = scene, - options = options, + options = analysisOptions, tsOptions = TsOptions(), ).use { machine -> machine.analyzeWithOutcome(methods = listOf(method))