From 38ff4977a0681fb1469c4ce28c7b5d04f39004c4 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 18:30:30 +0300 Subject: [PATCH] Model built-in String conversion of primitive values --- .../org/usvm/machine/TsInterpreterObserver.kt | 1 + .../org/usvm/machine/expr/StringConversion.kt | 95 +++++++++++ .../org/usvm/machine/expr/TsExprResolver.kt | 4 + .../usvm/machine/TsStringConversionTest.kt | 159 ++++++++++++++++++ .../test/resources/models/StringConversion.ts | 47 ++++++ 5 files changed, 306 insertions(+) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringConversion.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsStringConversionTest.kt create mode 100644 usvm-ts/src/test/resources/models/StringConversion.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index 2030dd3802..566d040c00 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -131,6 +131,7 @@ enum class TsRuntimeFeatureLimitationReason { REGULAR_EXPRESSION_LITERAL, FRONTEND_UNSUPPORTED_VALUE, STRING_CONCAT_OPERAND_CONVERSION, + STRING_PRIMITIVE_CONVERSION, ARRAY_STORAGE_TYPE, ARRAY_NAMED_PROPERTY_READ, ARRAY_NAMED_PROPERTY_WRITE, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringConversion.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringConversion.kt new file mode 100644 index 0000000000..0eca031c17 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/StringConversion.kt @@ -0,0 +1,95 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsAssignStmt +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsPtrCallExpr +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsValue +import org.jacodb.ets.utils.getDeclaredLocals +import org.usvm.UExpr +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.machine.interpreter.getGlobals + +/** Recognize the implicit builtin, excluding source bindings with the same lib declaration type. */ +internal fun TsExprResolver.isBuiltInStringConverter(expr: EtsPtrCallExpr): Boolean { + val builtinCallSite = expr.callee.name == "String" && + expr.callee.enclosingClass == EtsClassSignature.UNKNOWN + if (!builtinCallSite) return false + + val method = scope.calcOnState { lastEnteredMethod } + val assignments = method.cfg.stmts.filterIsInstance() + val visited = mutableSetOf() + var pointer = expr.ptr + while (pointer.name.startsWith("%") && visited.add(pointer)) { + val definition = assignments.singleOrNull { it.lhv == pointer } ?: return false + pointer = definition.rhv as? EtsLocal ?: return false + } + if (pointer.name != "String") return false + + val signature = (expr.ptr.type as? EtsFunctionType)?.signature ?: return false + val parameter = signature.parameters.singleOrNull() ?: return false + val builtinSignature = signature.enclosingClass == EtsClassSignature.UNKNOWN && + signature.name.isEmpty() && signature.returnType == EtsStringType && + parameter.type == EtsAnyType && parameter.isOptional && !parameter.isRest + if (!builtinSignature) return false + + val file = method.enclosingClass?.declaringFile ?: return false + val sourceBinding = method.parameters.any { it.name == pointer.name } || + method.getDeclaredLocals().any { it.name == pointer.name } || + file.getGlobals().any { it.name == pointer.name } || + file.importInfos.any { it.name == pointer.name } + + return !sourceBinding +} + +/** String identity and existing exact primitive conversions; broader ToPrimitive remains explicit. */ +internal fun TsExprResolver.handleStringConverter(args: List): UExpr<*>? = with(ctx) { + val arguments = buildList { + for (argument in args) { + val value = resolve(argument) ?: return null + add(value) + } + } + if (arguments.isEmpty()) return mkStringConstant("", scope) + + val input = arguments.first() + val value = if (input.isFakeObject()) { + val payload = input.extractSingleValueFromFakeObjectOrNull(scope) + if (payload == null) { + stopRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.STRING_PRIMITIVE_CONVERSION, + detail = "String conversion of a mixed runtime kind requires a ToPrimitive model", + ) + return null + } + payload + } else { + input + } + + val constant = concreteStringValue(value) + if (constant != null) return mkStringConstant(constant, scope) + + if (value.sort == boolSort) { + val text = mkIte(value.asExpr(boolSort), mkStringConstant("true", scope), mkStringConstant("false", scope)) + return resolveHeapRef(scope, text) + } + if (value.sort == addressSort) { + val reference = resolveHeapRef(scope, value.asExpr(addressSort)) ?: return null + val referenceConstant = concreteStringValue(reference) + if (referenceConstant != null) return mkStringConstant(referenceConstant, scope) + + val hasStringBacking = scope.calcOnState { reference in boundedStringBackingRefs } + if (hasStringBacking) return reference + } + + stopRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.STRING_PRIMITIVE_CONVERSION, + detail = "String conversion requires a modeled string or exact primitive: $value", + ) + null +} 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 4b5166e925..3bc38202a8 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 @@ -1272,6 +1272,10 @@ class TsExprResolver( return handleNumberConverter(expr.args) } + if (isBuiltInStringConverter(expr)) { + return handleStringConverter(expr.args) + } + when (val result = scope.calcOnState { methodResult }) { is TsMethodResult.Success -> { scope.doWithState { methodResult = TsMethodResult.NoCall } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringConversionTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringConversionTest.kt new file mode 100644 index 0000000000..a158a2dcc9 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsStringConversionTest.kt @@ -0,0 +1,159 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsMethod +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.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.call.TsUnknownCallEvent +import org.usvm.machine.call.TsUnknownCallModelSelection +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 + +class TsStringConversionTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val source = getResourcePath("/models/StringConversion.ts") + override val scene = EtsScene(listOf(loadEtsFileAutoConvert(source, provider = EtsIrProvider.TS_FRONTEND))) + override val tsOptions = TsOptions( + maxArraySize = 8, + eraseTypeAssertions = true, + unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet()), + ) + override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + val analysis = TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions, observer = observer) + .use { machine -> machine.analyzeWithOutcome(listOf(method)) } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, analysis.stopReason) + assertTrue(analysis.unsupportedPaths.isEmpty(), analysis.unsupportedPaths.toString()) + assertTrue(events.isEmpty(), events.toString()) + val tests = analysis.states.map { state -> TsTestResolver().resolve(method, state) } + assertTrue(tests.isNotEmpty(), method.name) + replay(method.name, tests) + tests + } + + init { + options = options.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + } + + @Test + fun `typed and generic string conversion preserves the original symbolic value`() { + for (name in listOf("typed", "generic")) { + discoverProperties( + method = getMethod(methodName = name, className = "StringConversion"), + { input, result -> input.value == result.value }, + invariants = arrayOf({ input, result -> input.value == result.value }), + ) + } + } + + @Test + fun `boolean conversion preserves both outcomes`() { + discoverProperties( + method = getMethod(methodName = "boolean", className = "StringConversion"), + { input, result -> input.value && result.value == "true" }, + { input, result -> !input.value && result.value == "false" }, + invariants = arrayOf({ input, result -> result.value == input.value.toString() }), + ) + } + + @Test + fun `omitted nullish concrete numeric and UTF16 conversion replays exactly`() { + val cases = mapOf("constants" to "|undefined|null|true|false|0|1.5", "codeUnits" to "A\u0000\uD800\uDC00\uDFFF") + + for ((name, expected) in cases) { + discoverProperties( + method = getMethod(methodName = name, className = "StringConversion"), + { result -> result.value == expected }, + invariants = arrayOf({ result -> result.value == expected }), + ) + } + } + + @Test + fun `source bindings named String retain their callable semantics`() { + for ((name, expected) in mapOf("shadowedParameter" to "shadow", "shadowedLocal" to "local")) { + discoverProperties( + method = getMethod(methodName = name, className = "StringConversion"), + { _, result -> result.value == expected }, + invariants = arrayOf({ _, result -> result.value == expected }), + ) + } + } + + @Test + fun `object and symbolic number conversion remain explicit limitations`() { + for (name in listOf("unsupportedObject", "symbolicNumber")) { + val method = getMethod(methodName = name, className = "StringConversion") + val limitations = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event + } + } + + val analysis = TsMachine(scene = scene, options = options, tsOptions = tsOptions, observer = observer) + .use { machine -> machine.analyzeWithOutcome(listOf(method)) } + + assertTrue(analysis.states.isEmpty(), name) + assertTrue(analysis.unsupportedPaths.isNotEmpty(), name) + val conversionLimited = limitations.any { + it.reason == TsRuntimeFeatureLimitationReason.STRING_PRIMITIVE_CONVERSION + } + assertTrue(conversionLimited, name) + } + } + + private fun replay(name: String, tests: List) { + val script = buildString { + appendLine(source.readText()) + for (test in tests) { + val arguments = test.before.parameters.joinToString { value -> + when (value) { + is TsTestValue.TsString -> jsString(value.value) + is TsTestValue.TsBoolean -> value.value.toString() + else -> error("Unexpected conversion input: $value") + } + } + val expected = assertIs(test.returnValue).value + appendLine( + "if (new StringConversion().$name($arguments) !== ${jsString(expected)}) throw new Error('$name');", + ) + } + } + + assertNodeReplay( + source = script, + directory = directory, + name = name, + timeoutMessage = "String replay timed out", + ) + } +} diff --git a/usvm-ts/src/test/resources/models/StringConversion.ts b/usvm-ts/src/test/resources/models/StringConversion.ts new file mode 100644 index 0000000000..e594308829 --- /dev/null +++ b/usvm-ts/src/test/resources/models/StringConversion.ts @@ -0,0 +1,47 @@ +class StringConversion { + typed(value: string): string { + return String(value); + } + + generic(value: string): string { + return this.convert(value); + } + + private convert(value: K): string { + return String(value); + } + + boolean(value: boolean): string { + return String(value); + } + + constants(): string { + return String() + "|" + String(undefined) + "|" + String(null) + "|" + + String(true) + "|" + String(false) + "|" + String(-0) + "|" + String(1.5); + } + + codeUnits(): string { + return this.convert("A\u0000\uD800\uDC00\uDFFF"); + } + + shadowedParameter(value: string): string { + return this.withConverter((input?: any): string => "shadow", value); + } + + private withConverter(String: (value?: any) => string, value: string): string { + return String(value); + } + + shadowedLocal(value: string): string { + const String: (value?: any) => string = (input?: any): string => "local"; + return String(value); + } + + unsupportedObject(): string { + return String({ value: "a" }); + } + + symbolicNumber(value: number): string { + return String(value); + } +}