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 86444e1054..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 @@ -6,14 +6,19 @@ import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsLocal 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( @@ -34,31 +39,39 @@ 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, + lengthLValue = mkStringBackingLengthLValue(charsRef), + maxArraySize = maxArraySize, + ) } else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type") } // 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 f5ea96ef7a..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), ) @@ -811,6 +813,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 = mkStringBackingLengthLValue(charsRef) + 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/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/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/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/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/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() + } +} 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/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 2f950432f0..1e45549f0e 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 @@ -54,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() @@ -63,8 +67,22 @@ 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 -> { @@ -158,7 +176,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() @@ -174,6 +193,7 @@ open class TsTestStateResolver( private val finalStateMemory: UReadOnlyMemory, val method: EtsMethod, val resolvedLValuesToFakeObjects: List, UConcreteHeapRef>>, + val maxStringLength: Int, ) { fun resolveLValue( lValue: ULValue<*, *>, @@ -250,11 +270,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 +322,36 @@ 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) } + + // 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) { + throw TsUnsupportedWitnessException("Symbolic string is missing backing array: $concreteRef") + } + + val lengthLValue = mkStringBackingLengthLValue(charsRef) + val length = evaluateInModel(stringMemory.read(lengthLValue)).extractInt() + require(length in 0..maxStringLength) { "Unsupported symbolic string length: $length" } + + val value = buildString(length) { + repeat(length) { index -> + val elementLValue = mkStringBackingElementLValue(charsRef, mkSizeExpr(index)) + val element = evaluateInModel(stringMemory.read(elementLValue)) as KBitVec16Value + append(element.shortValue.toInt().toChar()) + } } - return TsTestValue.TsString(value) + + TsTestValue.TsString(value) } fun resolveThisInstance(): TsTestValue { @@ -396,7 +435,7 @@ 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") } 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/samples/lang/SymbolicStringInput.ts b/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts new file mode 100644 index 0000000000..5802ee7e31 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/lang/SymbolicStringInput.ts @@ -0,0 +1,29 @@ +class SymbolicStringInput { + identity(value: string): string { + return value; + } + + lengthOne(value: string): number { + if (value.length === 0) return 0; + + return value.length === 1 ? 1 : 0; + } + + literal(): string { + return "A\u0000\u03a9\uD83D\uDE00"; + } + + literalLength(): number { + return "A\u0000\u03a9\uD83D\uDE00".length; + } + + 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; + } +}