diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 65a7a3d5d..0bf3bbab1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -65,13 +65,16 @@ import org.jacodb.ets.model.EtsStaticFieldRef import org.jacodb.ets.model.EtsStrictEqExpr import org.jacodb.ets.model.EtsStrictNotEqExpr import org.jacodb.ets.model.EtsStringConstant +import org.jacodb.ets.model.EtsStringLiteralType import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsSubExpr import org.jacodb.ets.model.EtsThis +import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsTypeOfExpr import org.jacodb.ets.model.EtsUnaryExpr import org.jacodb.ets.model.EtsUnaryPlusExpr import org.jacodb.ets.model.EtsUndefinedConstant +import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsUnsignedRightShiftExpr import org.jacodb.ets.model.EtsValue @@ -89,6 +92,7 @@ import org.usvm.api.allocateConcreteRef import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArrayLength import org.usvm.api.makeSymbolicPrimitive +import org.usvm.api.memcpy import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type import org.usvm.isAllocatedConcreteHeapRef @@ -120,6 +124,8 @@ import org.usvm.util.SymbolResolutionResult import org.usvm.util.isResolved import org.usvm.util.mkFieldLValue import org.usvm.util.mkRegisterStackLValue +import org.usvm.util.mkStringBackingLValue +import org.usvm.util.mkStringBackingLengthLValue import org.usvm.util.resolveEtsMethods import org.usvm.util.resolveImportInfo @@ -592,15 +598,97 @@ class TsExprResolver( if (expr.type == EtsStringType) { return resolveAfterResolved(expr.left, expr.right) { lhs, rhs -> val lhsString = concreteStringValue(lhs) - ?: error("Symbolic string concatenation is not supported for left operand: $lhs") val rhsString = concreteStringValue(rhs) - ?: error("Symbolic string concatenation is not supported for right operand: $rhs") - ctx.mkStringConstant(lhsString + rhsString, scope) + if (lhsString != null && rhsString != null) { + return@resolveAfterResolved ctx.mkStringConstant(lhsString + rhsString, scope) + } + + val left = stringOperand(lhs, expr.left.type) + val right = stringOperand(rhs, expr.right.type) + + with(ctx) { + val leftChars = scope.calcOnState { + memory.read(mkStringBackingLValue(left)) + } + val rightChars = scope.calcOnState { + memory.read(mkStringBackingLValue(right)) + } + val leftLength = scope.calcOnState { + memory.read(mkStringBackingLengthLValue(leftChars)) + } + val rightLength = scope.calcOnState { + memory.read(mkStringBackingLengthLValue(rightChars)) + } + val resultLength = mkBvAddExpr(leftLength, rightLength) + + val nonNegative = mkBvSignedGreaterOrEqualExpr(resultLength, mkBv(0)) + val withinMaximum = mkBvSignedLessOrEqualExpr(resultLength, mkBv(options.maxArraySize)) + val resultWithinBound = mkAnd(nonNegative, withinMaximum) + scope.fork(resultWithinBound, blockOnFalseState = { + terminateAsUnsupported( + reason = "String concatenation result exceeds the configured length bound " + + options.maxArraySize, + ) + }) ?: return@resolveAfterResolved null + + scope.calcOnState { + val result = memory.allocConcrete(EtsStringType) + val resultChars = memory.allocConcrete(EtsArrayType(EtsNumberType, dimensions = 1)) + memory.write( + mkStringBackingLValue(result), + resultChars, + guard = trueExpr, + ) + memory.write(mkStringBackingLengthLValue(resultChars), resultLength, guard = trueExpr) + boundedStringBackingRefs += result + + memory.memcpy( + srcRef = leftChars, + dstRef = resultChars, + type = stringBackingArrayDescriptor, + elementSort = bv16Sort, + fromSrc = mkBv(0), + fromDst = mkBv(0), + length = leftLength, + ) + memory.memcpy( + srcRef = rightChars, + dstRef = resultChars, + type = stringBackingArrayDescriptor, + elementSort = bv16Sort, + fromSrc = mkBv(0), + fromDst = leftLength, + length = rightLength, + ) + + result + } + } } } return resolveBinaryOperator(TsBinaryOperator.Add, expr) } + private fun stringOperand(value: UExpr<*>, type: EtsType): UHeapRef = with(ctx) { + concreteStringValue(value)?.let { return mkStringConstant(it, scope) } + + if (!isStringOperandType(type) || value.sort != addressSort || value.isFakeObject()) { + throw UnsupportedOperationException("Unsupported string concatenation operand: $type, $value") + } + val ref = value.asExpr(addressSort) + if (scope.calcOnState { ref !in boundedStringBackingRefs }) { + throw UnsupportedOperationException("String concatenation needs a modeled string backing for $ref") + } + + ref + } + + private fun isStringOperandType(type: EtsType): Boolean = when (type) { + is EtsStringType, is EtsStringLiteralType -> true + is EtsUnionType -> type.types.isNotEmpty() && type.types.all(::isStringOperandType) + else -> false + } + private fun concreteStringValue(value: UExpr<*>): String? = with(ctx) { when { value == trueExpr -> "true" diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringConcatTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringConcatTest.kt new file mode 100644 index 000000000..1cbe5ddec --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsSymbolicStringConcatTest.kt @@ -0,0 +1,370 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.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.test.assertTrue +import kotlin.time.Duration + +class TsSymbolicStringConcatTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/SymbolicStringConcat.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + + private val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + throwExceptionOnStepFailure = true, + ) + + @Test + fun `symbolic concatenation preserves code units and replays witnesses`() { + for ((name, expected) in mapOf( + "append" to { value: String -> value + "!" }, + "prepend" to { value: String -> "\u03A9" + value }, + "utf16" to { value: String -> value + "\u0000\uD83D\uDE00" }, + "primitives" to { value: String -> value + "truenullundefined1.5" }, + )) { + discoverProperties( + method = method(name), + { input, result -> result.value == expected(input.value) }, + invariants = arrayOf({ input, result -> result.value == expected(input.value) }), + ) + } + discoverProperties( + method = method("combine"), + { left, right, result -> result.value == left.value + right.value }, + invariants = arrayOf({ left, right, result -> result.value == left.value + right.value }), + ) + discoverProperties( + method = method("combineTwo"), + { left, right, result -> + left.value.length == 1 && right.value.length == 1 && result.value.length == 2 + }, + invariants = arrayOf({ left, right, result -> + val expected = if (left.value.length == 1 && right.value.length == 1) { + left.value + right.value + } else { + "" + } + + result.value == expected + }), + ) + discoverProperties( + method = method("appendLength"), + { input, result -> input.value.isEmpty() && result.number == 1.0 }, + { input, result -> input.value.isNotEmpty() && result.number == 0.0 }, + invariants = arrayOf({ input, result -> result.number == (if (input.value.isEmpty()) 1.0 else 0.0) }), + ) + + val methods = scene.projectClasses.single { it.name == "SymbolicStringConcat" }.methods + .filter { + it.name in setOf("append", "prepend", "combine", "combineTwo", "appendLength", "utf16", "primitives") + } + .associateBy { it.name } + val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> + methods.mapValues { (_, method) -> + val result = machine.analyzeWithOutcome(listOf(method)) + assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason) + result.states.map { state -> TsTestResolver().resolve(method, state) } + } + } + + assertEquals(7, tests.size) + verifyWitnesses(tests) + + assertEquals( + setOf(0.0, 1.0), + tests.getValue("appendLength").map { + assertIs(it.returnValue).number + }.toSet(), + ) + assertTrue( + tests.getValue("combineTwo").any { test -> + val inputs = test.before.parameters.map { assertIs(it).value } + inputs.all { it.length == 1 } && assertIs(test.returnValue).value.length == 2 + }, + "No witness copied two nonempty symbolic strings", + ) + + replay(tests, source.readText()) + } + + @Test + fun `string union operands concatenate and replay both logical branches`() { + val methods = mapOf( + "appendLogicalAnd" to { value: String -> (if (value.isEmpty()) "" else "a") + "!" }, + "prependLogicalAnd" to { value: String -> "!" + (if (value.isEmpty()) "" else "a") }, + ) + for ((name, expected) in methods) { + discoverProperties( + method = method(name), + { input, result -> input.value.isEmpty() && result.value == expected(input.value) }, + { input, result -> input.value.isNotEmpty() && result.value == expected(input.value) }, + invariants = arrayOf({ input, result -> result.value == expected(input.value) }), + ) + } + + val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions(maxArraySize = 8)).use { machine -> + methods.keys.associateWith { name -> + val method = method(name) + val analysis = machine.analyzeWithOutcome(listOf(method)) + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.isEmpty(), "$name: ${analysis.unsupportedPaths}") + + analysis.states.map { state -> TsTestResolver().resolve(method, state) } + } + } + + for ((name, generated) in tests) { + val inputs = generated.map { test -> assertIs(test.before.parameters.single()).value } + assertTrue(inputs.any { it.isEmpty() }, "No empty-input witness for $name") + assertTrue(inputs.any { it.isNotEmpty() }, "No nonempty-input witness for $name") + } + + replay(tests, source.readText()) + } + + @Test + fun `concatenation result respects the witness length bound`() { + val source = getResourcePath("/models/SymbolicStringConcat.ts") + val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + val method = scene.projectClasses.single { it.name == "SymbolicStringConcat" } + .methods + .single { it.name == "appendLength" } + val (unsupportedPaths, tests) = TsMachine( + scene, + options = machineOptions.copy(throwExceptionOnStepFailure = false), + tsOptions = TsOptions(maxArraySize = 2), + ).use { machine -> + val result = machine.analyzeWithOutcome(listOf(method)) + assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason) + result.unsupportedPaths to result.states.map { state -> TsTestResolver().resolve(method, state) } + } + + assertTrue(unsupportedPaths.any { "result exceeds the configured length bound" in it }) + assertEquals( + setOf(0.0, 1.0), + tests.map { assertIs(it.returnValue).number }.toSet(), + ) + tests.forEach { test -> + val input = assertIs(test.before.parameters.single()).value + assertTrue(input.length <= 1, "Concatenated witness exceeds the configured bound") + } + + replay(mapOf("appendLength" to tests), source.readText()) + } + + @Test + fun `typed and literal string fields concatenate with modeled backing`() { + for (name in listOf("fromField", "fromEmptyLiteralField", "fromNonemptyLiteralField")) { + discoverProperties( + method = method(name), + { holder, result -> + val value = (holder.properties.getValue("value") as? TsTestValue.TsString)?.value + value != null && result.value == value + "!" + }, + invariants = arrayOf({ holder, result -> + val value = (holder.properties.getValue("value") as? TsTestValue.TsString)?.value + value != null && result.value == value + "!" + }), + ) + } + + val names = setOf("fromField", "fromEmptyLiteralField", "fromNonemptyLiteralField") + val methods = scene.projectClasses.single { it.name == "SymbolicStringConcat" }.methods + .filter { it.name in names } + .associateBy { it.name } + assertEquals(names, methods.keys) + + val analyses = TsMachine( + scene, + options = machineOptions.copy(stateCollectionStrategy = StateCollectionStrategy.ALL), + tsOptions = TsOptions(maxArraySize = 5), + ).use { machine -> + methods.mapValues { (_, method) -> + machine.analyzeWithOutcome(listOf(method)) + } + } + + val expectedLiterals = mapOf( + "fromEmptyLiteralField" to "", + "fromNonemptyLiteralField" to "A\u0000\uD83D\uDE00", + ) + val script = buildString { + appendLine(source.readText()) + analyses.forEach { (name, analysis) -> + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason, name) + assertTrue( + analysis.unsupportedPaths.none { "modeled string backing" in it }, + "$name: ${analysis.unsupportedPaths}", + ) + if (name in expectedLiterals) { + assertTrue(analysis.unsupportedPaths.isEmpty(), "$name: ${analysis.unsupportedPaths}") + } + + val method = methods.getValue(name) + val tests = analysis.states.map { state -> TsTestResolver().resolve(method, state) } + assertTrue(tests.isNotEmpty(), "$name produced no witnesses") + tests.forEachIndexed { index, test -> + val holder = assertIs(test.before.parameters.single()) + val value = assertIs(holder.properties.getValue("value")).value + val result = assertIs(test.returnValue).value + expectedLiterals[name]?.let { expected -> assertEquals(expected, value, test.toString()) } + assertEquals(value + "!", result, test.toString()) + + appendLine( + "if (new SymbolicStringConcat().$name({ value: ${jsString(value)} }) " + + "!== ${jsString(result)}) {" + ) + appendLine(" throw Error('$name witness $index');") + appendLine("}") + } + } + } + val typedValues = analyses.getValue("fromField").states.map { state -> + val test = TsTestResolver().resolve(methods.getValue("fromField"), state) + val holder = assertIs(test.before.parameters.single()) + assertIs(holder.properties.getValue("value")).value + } + assertTrue(typedValues.any { it.isEmpty() }) + assertTrue(typedValues.any { it.isNotEmpty() }) + + assertNodeReplay( + source = script, + directory = directory, + name = "string-field-concat", + timeoutMessage = "Node replay timed out", + failureContext = script.take(1000), + ) + } + + @Test + fun `concatenation result has modeled backing for string equality`() { + discoverProperties( + method = method("appendEquals"), + { input, result -> input.value.length != 1 && result.number == 3.0 }, + { input, result -> input.value == "a" && result.number == 1.0 }, + { input, result -> input.value.length == 1 && input.value != "a" && result.number == 0.0 }, + invariants = arrayOf({ input, result -> + result.number == (if (input.value.length != 1) 3.0 else if (input.value == "a") 1.0 else 0.0) + }), + ) + + val method = scene.projectClasses.single { it.name == "SymbolicStringConcat" } + .methods + .single { it.name == "appendEquals" } + val (unsupportedPaths, tests) = TsMachine( + scene, + options = machineOptions, + tsOptions = TsOptions(maxArraySize = 4), + ).use { machine -> + val result = machine.analyzeWithOutcome(listOf(method)) + assertEquals(TsAnalysisStopReason.EXHAUSTED, result.stopReason) + result.unsupportedPaths to result.states.map { state -> TsTestResolver().resolve(method, state) } + } + + assertTrue(unsupportedPaths.isEmpty(), unsupportedPaths.toString()) + assertEquals( + setOf(0.0, 1.0, 3.0), + tests.map { assertIs(it.returnValue).number }.toSet(), + ) + tests.forEach { test -> + val input = assertIs(test.before.parameters.single()).value + val expected = if (input.length != 1) 3.0 else if (input == "a") 1.0 else 0.0 + assertEquals(expected, assertIs(test.returnValue).number) + } + + replay(mapOf("appendEquals" to tests), source.readText()) + } + + private fun verifyWitnesses(tests: Map>) { + tests.forEach { (name, generated) -> + assertTrue(generated.isNotEmpty(), "No $name witnesses") + generated.forEach { test -> verifyWitness(name, test) } + } + } + + private fun method(name: String) = getMethod(methodName = name, className = "SymbolicStringConcat") + + private fun verifyWitness(name: String, test: TsTest) { + val inputs = test.before.parameters.map { assertIs(it).value } + val expected = when (name) { + "append" -> inputs.single() + "!" + "prepend" -> "\u03A9" + inputs.single() + "combine" -> inputs[0] + inputs[1] + "combineTwo" -> if (inputs[0].length == 1 && inputs[1].length == 1) { + inputs[0] + inputs[1] + } else { + "" + } + "utf16" -> inputs.single() + "\u0000\uD83D\uDE00" + "primitives" -> inputs.single() + "truenullundefined1.5" + "appendLength" -> null + else -> error("Unexpected method: $name") + } + + if (expected != null) { + assertEquals(expected, assertIs(test.returnValue).value, test.toString()) + } else { + val value = if (inputs.single().isEmpty()) 1.0 else 0.0 + assertEquals(value, assertIs(test.returnValue).number, test.toString()) + } + } + + private fun replay(tests: Map>, source: String) { + val statements = tests.flatMap { (name, generated) -> + generated.mapIndexed { index, test -> replayStatement(name, index, test) } + } + val script = buildString { + appendLine(source) + statements.forEach(::appendLine) + } + assertNodeReplay( + source = script, + directory = directory, + name = "symbolic-string-concat", + timeoutMessage = "Node replay timed out", + failureContext = script.take(1000), + ) + } + + private fun replayStatement(name: String, index: Int, test: TsTest): String { + 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") + } + + return """ + if (new SymbolicStringConcat().$name($args) !== $expected) { + throw Error('$name witness $index'); + } + """.trimIndent() + } +} diff --git a/usvm-ts/src/test/resources/models/SymbolicStringConcat.ts b/usvm-ts/src/test/resources/models/SymbolicStringConcat.ts new file mode 100644 index 000000000..6ff1da35f --- /dev/null +++ b/usvm-ts/src/test/resources/models/SymbolicStringConcat.ts @@ -0,0 +1,73 @@ +class StringHolder { + value: string; +} + +class EmptyLiteralStringHolder { + value: "" = ""; +} + +class NonemptyLiteralStringHolder { + value: "A\u0000\uD83D\uDE00" = "A\u0000\uD83D\uDE00"; +} + +class SymbolicStringConcat { + append(value: string): string { + return value + "!"; + } + + appendLogicalAnd(value: string): string { + return (value && "a") + "!"; + } + + prependLogicalAnd(value: string): string { + return "!" + (value && "a"); + } + + prepend(value: string): string { + return "\u03a9" + value; + } + + combine(left: string, right: string): string { + return left + right; + } + + combineTwo(left: string, right: string): string { + if (left.length !== 1) return ""; + if (right.length !== 1) return ""; + + return left + right; + } + + appendLength(value: string): number { + const result = value + "!"; + return result.length === 1 ? 1 : 0; + } + + appendEquals(value: string): number { + if (value.length !== 1) return 3; + + return value + "!" === "a!" ? 1 : 0; + } + + utf16(value: string): string { + return value + "\u0000\uD83D\uDE00"; + } + + primitives(value: string): string { + return value + true + null + undefined + 1.5; + } + + fromField(holder: StringHolder): string { + if (holder.value.length === 0) return holder.value + "!"; + + return holder.value + "!"; + } + + fromEmptyLiteralField(holder: EmptyLiteralStringHolder): string { + return holder.value + "!"; + } + + fromNonemptyLiteralField(holder: NonemptyLiteralStringHolder): string { + return holder.value + "!"; + } +}