From 06029907787f959fa976f551ea189a928af74dba Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Fri, 2 Oct 2026 20:01:50 +0300 Subject: [PATCH 1/7] [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 2/7] [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 3/7] [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 4/7] [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 5/7] [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 6/7] [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 d418b8507bcf0f44d54c8151d26c8db696f2a25c Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 3 Oct 2026 23:25:47 +0300 Subject: [PATCH 7/7] [TS] Organize symbolic string regression tests --- .../usvm/machine/TsStringWitnessBoundTest.kt | 82 ++++++ .../usvm/machine/TsSymbolicStringInputTest.kt | 268 ------------------ .../samples/arrays/StringArrayIsolation.kt | 75 +++++ .../usvm/samples/lang/SymbolicStringInput.kt | 103 +++++++ .../usvm/util/TsStringWitnessResolverTest.kt | 83 ++++++ .../samples/arrays/StringArrayIsolation.ts | 8 + .../lang}/SymbolicStringInput.ts | 7 - 7 files changed, 351 insertions(+), 275 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsStringWitnessBoundTest.kt delete mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/arrays/StringArrayIsolation.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/samples/lang/SymbolicStringInput.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/util/TsStringWitnessResolverTest.kt create mode 100644 usvm-ts/src/test/resources/samples/arrays/StringArrayIsolation.ts rename usvm-ts/src/test/resources/{models => samples/lang}/SymbolicStringInput.ts (75%) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringWitnessBoundTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringWitnessBoundTest.kt new file mode 100644 index 0000000000..3aff912d1d --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringWitnessBoundTest.kt @@ -0,0 +1,82 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +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.TsMethodTestRunner +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 kotlin.io.path.readText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.time.Duration + +private const val REPLAY_FAILURE_CONTEXT_LIMIT = 1000 + +class TsStringWitnessBoundTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val tsPath = "/samples/lang/SymbolicStringInput.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `configured string bound is shared with concrete test extraction`() { + val method = getMethod(methodName = "lengthIs10001", className = "SymbolicStringInput") + val maxStringLength = 10_001 + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + val tests = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(maxArraySize = maxStringLength), + ).use { machine -> + machine.analyze(methods = 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(getResourcePath(tsPath).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("}") + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "string-bound", + timeoutMessage = "String bound replay timed out", + failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt deleted file mode 100644 index f214fb0e7d..0000000000 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringInputTest.kt +++ /dev/null @@ -1,268 +0,0 @@ -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.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 - -private const val REPLAY_FAILURE_CONTEXT_LIMIT = 1000 - -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") - 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", "literalLength") } - .associateBy { it.name } - val tests = TsMachine(scene, options = machineOptions, 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, message = test.toString()) - } - - 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 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) -> - 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("}") - } - } - } - assertNodeReplay( - source = script, - directory = directory, - name = "basic-strings", - timeoutMessage = "basic-strings replay timed out", - failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), - ) - } - - @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 - val encodedInput = jsString(input) - - appendLine( - "if (new SymbolicStringInput().independentArrayLength($encodedInput, [$elements]) !== $expected) {" - ) - appendLine(" throw Error('array alias witness $index');") - appendLine("}") - } - } - assertNodeReplay( - source = script, - directory = directory, - name = "array-isolation", - timeoutMessage = "array-isolation replay timed out", - failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), - ) - } - - @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("}") - } - } - assertNodeReplay( - source = script, - directory = directory, - name = "string-bound", - timeoutMessage = "string-bound replay timed out", - 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/samples/arrays/StringArrayIsolation.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/StringArrayIsolation.kt new file mode 100644 index 0000000000..99012df656 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/StringArrayIsolation.kt @@ -0,0 +1,75 @@ +package org.usvm.samples.arrays + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import org.usvm.util.jsString +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertIs + +private const val REPLAY_FAILURE_CONTEXT_LIMIT = 1000 + +class StringArrayIsolation : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val tsPath = "/samples/arrays/StringArrayIsolation.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `changing an input array does not change the string length`() { + val method = getMethod(methodName = "independentArrayLength") + + discoverProperties, TsTestValue.TsNumber>( + method = method, + { input, array, result -> + input.value.length == 1 && array.values.size == 1 && result.number == 2.0 + }, + { input, array, result -> + (input.value.length != 1 || array.values.size != 1) && result.number == 0.0 + }, + invariants = arrayOf( + { _, _, result -> result.number != 1.0 }, + ), + ) + } + + @Test + fun `array isolation witnesses replay in JavaScript`() { + val method = getMethod(methodName = "independentArrayLength") + val tests = runner(method, options) + val source = getResourcePath(tsPath).readText() + + val script = buildString { + appendLine(source) + 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 StringArrayIsolation().independentArrayLength(${jsString(input)}, [$elements]) !== $expected) {" + ) + appendLine(" throw Error('array isolation witness $index');") + appendLine("}") + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "string-array-isolation", + timeoutMessage = "Array isolation replay timed out", + failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SymbolicStringInput.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SymbolicStringInput.kt new file mode 100644 index 0000000000..5bc75927dc --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/SymbolicStringInput.kt @@ -0,0 +1,103 @@ +package org.usvm.samples.lang + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import org.usvm.util.jsString +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertIs + +private const val REPLAY_FAILURE_CONTEXT_LIMIT = 1000 + +class SymbolicStringInput : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val tsPath = "/samples/lang/SymbolicStringInput.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `symbolic string input is preserved in the result`() { + val method = getMethod(methodName = "identity") + + discoverProperties( + method = method, + { input, result -> result.value == input.value }, + ) + } + + @Test + fun `empty and one-character strings produce distinct results`() { + val method = getMethod(methodName = "lengthOne") + + discoverProperties( + method = method, + { input, result -> input.value.isEmpty() && result.number == 0.0 }, + { input, result -> input.value.length == 1 && result.number == 1.0 }, + invariants = arrayOf( + { input, result -> result.number == if (input.value.length == 1) 1.0 else 0.0 }, + ), + ) + } + + @Test + fun `literal preserves NUL non-ASCII and a surrogate pair`() { + val method = getMethod(methodName = "literal") + + discoverProperties( + method = method, + { result -> result.value == "A\u0000\u03a9\uD83D\uDE00" }, + ) + } + + @Test + fun `literal length counts UTF-16 code units`() { + val method = getMethod(methodName = "literalLength") + + discoverProperties( + method = method, + { result -> result.number == 5.0 }, + ) + } + + @Test + fun `generated string witnesses replay in JavaScript`() { + val methodNames = listOf("identity", "lengthOne", "literal", "literalLength") + val tests = methodNames.associateWith { name -> runner(getMethod(methodName = name), options) } + val source = getResourcePath(tsPath).readText() + + val script = buildString { + appendLine(source) + tests.forEach { (name, generated) -> + generated.forEachIndexed { index, test -> + val arguments = 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($arguments) !== $expected) {") + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = "symbolic-strings", + timeoutMessage = "Symbolic string replay timed out", + failureContext = script.take(REPLAY_FAILURE_CONTEXT_LIMIT), + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsStringWitnessResolverTest.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsStringWitnessResolverTest.kt new file mode 100644 index 0000000000..730e70de6a --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsStringWitnessResolverTest.kt @@ -0,0 +1,83 @@ +package org.usvm.util + +import org.jacodb.ets.model.EtsScene +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.machine.TsMachine +import org.usvm.machine.TsOptions +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsStringWitnessResolverTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val tsPath = "/samples/lang/SymbolicStringInput.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `string inferred from any without backing cannot become an empty witness`() { + val method = getMethod(methodName = "anyStringLength", className = "SymbolicStringInput") + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + val states = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + ).use { machine -> + machine.analyze(methods = listOf(method)) + } + val resolutions = states.map { state -> runCatching { TsTestResolver().resolve(method, state) } } + + assertTrue(states.isNotEmpty()) + val unsupported = resolutions.mapNotNull { result -> result.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 { result -> result.getOrNull() } + assertTrue(supported.isNotEmpty()) + val script = buildString { + appendLine(getResourcePath(tsPath).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/resources/samples/arrays/StringArrayIsolation.ts b/usvm-ts/src/test/resources/samples/arrays/StringArrayIsolation.ts new file mode 100644 index 0000000000..77300de850 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/arrays/StringArrayIsolation.ts @@ -0,0 +1,8 @@ +class StringArrayIsolation { + independentArrayLength(value: string, array: number[]): number { + if (value.length !== 1 || array.length !== 1) return 0; + + array.length = 0; + return value.length === 0 ? 1 : 2; + } +} diff --git a/usvm-ts/src/test/resources/models/SymbolicStringInput.ts b/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts similarity index 75% rename from usvm-ts/src/test/resources/models/SymbolicStringInput.ts rename to usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts index dc1d2b7710..5802ee7e31 100644 --- a/usvm-ts/src/test/resources/models/SymbolicStringInput.ts +++ b/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts @@ -17,13 +17,6 @@ class SymbolicStringInput { 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; }