Model built-in String conversion for primitive TypeScript values

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,

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<EtsAssignStmt>()
+    val visited = mutableSetOf<EtsLocal>()
+    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<EtsValue>): 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
+}

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 }

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<TsTest> = { method, machineOptions ->
+        val events = mutableListOf<TsUnknownCallEvent>()
+        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<TsTestValue.TsString, TsTestValue.TsString>(
+                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<TsTestValue.TsBoolean, TsTestValue.TsString>(
+            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<TsTestValue.TsString>(
+                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<TsTestValue.TsString, TsTestValue.TsString>(
+                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<TsRuntimeFeatureLimitationEvent>()
+            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<TsTest>) {
+        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<TsTestValue.TsString>(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",
+        )
+    }
+}

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<K>(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);
+    }
+}