[TS] Integrate computed class members with distinct symbol identity

buildSrc/src/main/kotlin/Dependencies.kt

@@ -6,7 +6,7 @@ object Versions {
     const val clikt = "5.0.0"
     const val detekt = "1.23.7"
     const val ini4j = "0.5.4"
-    const val jacodb = "4251d2023d"
+    const val jacodb = "0fac32c8c5"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt

@@ -4,6 +4,7 @@ import org.junit.jupiter.api.io.TempDir
 import org.usvm.SolverType
 import org.usvm.ts.pbt.model.ArrayDomain
 import org.usvm.ts.pbt.model.BooleanDomain
+import org.usvm.ts.pbt.model.ConstantDomain
 import org.usvm.ts.pbt.model.IntegerDomain
 import org.usvm.ts.pbt.model.JsConcreteValue
 import org.usvm.ts.pbt.model.NumberDomain
@@ -219,28 +220,41 @@ class CallsClassDataRegistryOracleTest {
             constructorInputs = listOf(PropertyInput(name = "flag", domain = BooleanDomain)),
         )
 
-        val result = CurrentTsCallsClassCoverageEngine().search(
-            CallsClassSearchRequest(
-                harness = harness,
-                profile = CallsExperimentProfile.EMPTY_STOP,
-                frozenModelIds = emptySet(),
-                expectedNativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision,
-                seed = 1,
-                budget = 3.seconds,
-                timeQuantum = 100.milliseconds,
-                solverQueryLimit = 1.seconds,
-                solverType = SolverType.YICES,
-                candidateCap = 20,
-                requireEntryPointWitness = true,
-            ),
-        )
+        // Coverage-directed search need not enumerate every input model for each entry point.
+        val branchInputs = listOf(JsConcreteValue.Boolean(true), JsConcreteValue.Boolean(false))
+        val candidates = branchInputs.flatMap { flag ->
+            val inputs = listOf(PropertyInput(name = "flag", domain = ConstantDomain(flag)))
+            val branchHarness = harness.copy(
+                surface = harness.surface.copy(constructorInputs = inputs),
+                functions = harness.functions.map { it.copy(inputs = inputs) },
+            )
+            val result = CurrentTsCallsClassCoverageEngine().search(
+                CallsClassSearchRequest(
+                    harness = branchHarness,
+                    profile = CallsExperimentProfile.EMPTY_STOP,
+                    frozenModelIds = emptySet(),
+                    expectedNativeFrontendRevision = CallsBuildIdentity.nativeFrontendRevision,
+                    seed = 1,
+                    budget = 3.seconds,
+                    timeQuantum = 100.milliseconds,
+                    solverQueryLimit = 1.seconds,
+                    solverType = SolverType.YICES,
+                    candidateCap = 20,
+                    requireEntryPointWitness = true,
+                ),
+            )
+
+            val scenarioIds = result.search.candidates.map { it.entryPointId }.toSet()
+            assertEquals(harness.scenarios.map { it.id }.toSet(), scenarioIds, "flag=$flag")
+            result.search.candidates.forEach { assertEquals(listOf(flag), it.inputs) }
+            result.search.candidates
+        }
 
         val constructorScenarioId = harness.scenarios.first().id
-        val constructorBranches = result.search.candidates.filter { it.entryPointId == constructorScenarioId }
+        val constructorBranches = candidates.filter { it.entryPointId == constructorScenarioId }
             .map { it.inputs.single() }.toSet()
         assertEquals(setOf(JsConcreteValue.Boolean(true), JsConcreteValue.Boolean(false)), constructorBranches)
-        assertEquals(harness.scenarios.map { it.id }.toSet(), result.search.candidates.map { it.entryPointId }.toSet())
-        for (candidate in result.search.candidates) {
+        for (candidate in candidates) {
             val index = harness.scenarios.indexOfFirst { it.id == candidate.entryPointId }
             val original = OriginalTypeScriptClassReplayer(
                 directory,

usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt

@@ -26,6 +26,10 @@ private val logger = KotlinLogging.logger {}
 internal fun TsExprResolver.handleStaticCall(
     expr: EtsStaticCallExpr,
 ): UExpr<*>? = with(ctx) {
+    if (expr.callee.wellKnownSymbol != null) {
+        throw UnsupportedOperationException("Symbol-keyed static method dispatch is not supported")
+    }
+
     // Check if the method was already called and returned a value.
     when (val result = scope.calcOnState { methodResult }) {
         is TsMethodResult.Success -> {
@@ -121,7 +125,7 @@ private fun TsExprResolver.resolveStaticMethod(
 
 private fun EtsMethod.isStaticCallTarget(methodName: String): Boolean {
     val isTopLevelFunction = enclosingClass?.name == DEFAULT_ARK_CLASS_NAME
-    return name == methodName && (isStatic || isTopLevelFunction)
+    return signature.wellKnownSymbol == null && name == methodName && (isStatic || isTopLevelFunction)
 }
 
 private fun TsExprResolver.processAmbiguousStaticMethod(

usvm-ts/src/main/kotlin/org/usvm/machine/expr/InputObjectProperties.kt

@@ -25,6 +25,7 @@ import org.usvm.util.EtsHierarchy
 import org.usvm.util.InputPropertyDeclaration
 import org.usvm.util.declaredInstanceProperty
 import org.usvm.util.getAllMethods
+import org.usvm.util.hasStringName
 import org.usvm.util.mkFieldLValue
 
 private enum class PropertySlot {
@@ -96,7 +97,7 @@ private fun inputPropertyUnsupportedReason(local: EtsLocal?, name: String, hiera
     if (type !is EtsClassType && type !is EtsUnclearRefType) return null
 
     val inheritedMethod = hierarchy.classesForType(type).flatMap { it.getAllMethods(hierarchy) }
-        .any { !it.isStatic && it.name == name }
+        .any { !it.isStatic && it.hasStringName(name) }
     return if (inheritedMethod) "Input property '$name' requires unsupported class prototype lookup" else null
 }
 

usvm-ts/src/main/kotlin/org/usvm/machine/expr/ObjectPropertyUtil.kt

@@ -12,6 +12,7 @@ import org.usvm.machine.TsContext
 import org.usvm.machine.interpreter.TsStepScope
 import org.usvm.types.singleOrNull
 import org.usvm.util.EtsHierarchy
+import org.usvm.util.hasStringName
 
 internal const val PROTOTYPE_PROPERTY_NAME = "__proto__"
 
@@ -44,7 +45,7 @@ internal fun TsContext.objectLiteralClass(
 }
 
 internal fun EtsClass.hasOwnProperty(name: String): Boolean =
-    fields.any { it.name == name } || methods.any { it.name == name }
+    fields.any { it.hasStringName(name) } || methods.any { it.hasStringName(name) }
 
 private fun TsStepScope.hasPrototypeMutation(instance: UHeapRef, clazz: EtsClass): Boolean = calcOnState {
     clazz.fields.any { it.name == PROTOTYPE_PROPERTY_NAME } ||

usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt

@@ -47,10 +47,12 @@ import org.usvm.util.InputPropertyDeclaration
 import org.usvm.util.TsResolutionResult
 import org.usvm.util.arrayStorageType
 import org.usvm.util.createFakeField
+import org.usvm.util.hasStringName
 import org.usvm.util.mkFieldLValue
 import org.usvm.util.mkStringBackingElementLValue
 import org.usvm.util.mkStringBackingLValue
 import org.usvm.util.mkStringBackingLengthLValue
+import org.usvm.util.requireStringKey
 import org.usvm.util.resolveEtsField
 import org.usvm.util.boxArrayValue as boxRuntimeValue
 
@@ -59,6 +61,8 @@ private val logger = KotlinLogging.logger {}
 internal fun TsExprResolver.handleInstanceFieldRef(
     value: EtsInstanceFieldRef,
 ): UExpr<*>? = with(ctx) {
+    value.field.requireStringKey()
+
     when (val captured = tryCaptureInstanceCall(value)) {
         is TsExprApproximationResult.SuccessfulApproximation -> return captured.expr
         TsExprApproximationResult.ResolveFailure -> return null
@@ -166,7 +170,7 @@ private fun TsContext.resolveDeclaredField(
         return mkUndefinedValue()
     }
 
-    val declaredLiteralField = objectClass?.fields?.singleOrNull { it.name == field.name }
+    val declaredLiteralField = objectClass?.fields?.singleOrNull { it.hasStringName(field.name) }
     val writtenSort = scope.calcOnState { writtenObjectLiteralFieldSorts[instance to field.name] }
     val declaredLiteralSort = declaredLiteralField?.let { typeToSort(it.type) }
     val storageSort = writtenSort ?: declaredLiteralSort ?: resolvedFieldSort(
@@ -440,6 +444,8 @@ private fun TsContext.materializeTypedStringField(
 internal fun TsExprResolver.handleStaticFieldRef(
     value: EtsStaticFieldRef,
 ): UExpr<*>? = with(ctx) {
+    value.field.requireStringKey()
+
     if (value.field.name == "prototype") {
         val constructor = classConstructorRef(value.field.enclosingClass)
         if (!ensureSupportedArrayPrototypeAccess(constructor, value.field.name)) return null
@@ -454,6 +460,8 @@ fun TsContext.readStaticField(
     field: EtsFieldSignature,
     hierarchy: EtsHierarchy,
 ): UExpr<*>? {
+    field.requireStringKey()
+
     // TODO: handle unresolved class, or multiple classes
     val clazz = scene.projectAndSdkClasses.singleOrNull {
         it.signature == field.enclosingClass

usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt

@@ -24,12 +24,14 @@ import org.usvm.machine.call.isBuiltinDateGlobalType
 import org.usvm.machine.call.isBuiltinGlobalType
 import org.usvm.machine.state.lastStmt
 import org.usvm.util.getAllFields
+import org.usvm.util.hasStringName
 import org.usvm.util.mkFieldLValue
 
 /** A method property selected before evaluating call arguments. */
 class TsCapturedInstanceCall(
     val receiver: UExpr<*>,
     val sourceReceiver: EtsLocal,
+    val callee: EtsMethodSignature,
 )
 
 internal fun TsExprResolver.tryCaptureInstanceCall(
@@ -40,13 +42,16 @@ internal fun TsExprResolver.tryCaptureInstanceCall(
         ?: return TsExprApproximationResult.NoApproximation
     val target = assignment.lhv as? EtsLocal ?: return TsExprApproximationResult.NoApproximation
     val call = method.cfg.stmts.asSequence().mapNotNull { it.callExpr as? EtsPtrCallExpr }
-        .firstOrNull { it.ptr == target && it.receiver == field.instance && it.callee.name == field.field.name }
+        .firstOrNull {
+            val matchesNamedOrComputedKey = it.callee.name == field.field.name || it.callee.name == "%call"
+            it.ptr == target && it.receiver == field.instance && matchesNamedOrComputedKey
+        }
         ?: return TsExprApproximationResult.NoApproximation
 
     // Actual callback fields keep their value, including non-callable values.
     val owners = hierarchy.classesForType(EtsClassType(field.field.enclosingClass))
     val hasDeclaredField = owners.any { owner ->
-        owner.getAllFields(hierarchy).any { it.name == field.field.name }
+        owner.getAllFields(hierarchy).any { it.hasStringName(field.field.name) }
     }
 
     if (hasDeclaredField) {
@@ -89,14 +94,17 @@ internal fun TsExprResolver.tryCaptureInstanceCall(
 
     // Logger's compatibility approximation deliberately matches the source variable name.
     val approximationReceiver = if (implicitGlobal || source.name == "Logger") source else field.instance
+    val callee = call.callee.copy(name = field.field.name)
+    val captured = TsCapturedInstanceCall(
+        receiver = receiver,
+        sourceReceiver = approximationReceiver,
+        callee = callee,
+    )
     val pointer = allocateConcreteRef()
     scope.doWithState {
         capturedInstanceCalls = capturedInstanceCalls.put(
             pointer,
-            TsCapturedInstanceCall(
-                receiver = receiver,
-                sourceReceiver = approximationReceiver,
-            ),
+            captured,
             ownership,
         )
     }
@@ -110,7 +118,7 @@ internal fun TsExprResolver.handleCapturedInstanceCall(
     val receiver = requireNotNull(call.receiver)
     val instanceCall = EtsInstanceCallExpr(
         instance = receiver,
-        callee = call.callee,
+        callee = captured.callee,
         args = call.args,
         type = call.type,
     )

usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt

@@ -606,7 +606,7 @@ class TsExprResolver(
             .asSequence()
             .filter { clazz -> clazz.category != EtsClassCategory.OBJECT }
             .flatMap { clazz -> clazz.getAllMethods(hierarchy).asSequence() }
-            .any { method -> !method.isStatic && method.name == name }
+            .any { method -> !method.isStatic && method.signature.wellKnownSymbol == null && method.name == name }
         return if (inheritedMethod) "Deleting '$name' requires unsupported class prototype method lookup" else null
     }
 

usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt

@@ -24,8 +24,10 @@ import org.usvm.sizeSort
 import org.usvm.util.EtsHierarchy
 import org.usvm.util.TsResolutionResult
 import org.usvm.util.arrayStorageType
+import org.usvm.util.hasStringName
 import org.usvm.util.mkArrayLengthLValue
 import org.usvm.util.mkFieldLValue
+import org.usvm.util.requireStringKey
 import org.usvm.util.resolveEtsField
 import org.usvm.util.truncateKnownArrayIndices
 import org.usvm.util.boxArrayValue as boxRuntimeValue
@@ -209,6 +211,8 @@ fun TsContext.assignToInstanceField(
     expr: UExpr<*>,
     hierarchy: EtsHierarchy,
 ): Unit? {
+    field.requireStringKey()
+
     // Unwrap to get non-fake reference.
     val unwrappedInstance = resolveHeapRef(scope, instance.unwrapRef(scope)) ?: return null
 
@@ -352,6 +356,8 @@ fun TsContext.assignToStaticField(
     field: EtsFieldSignature,
     expr: UExpr<*>,
 ): Unit? {
+    field.requireStringKey()
+
     val clazz = scene.projectAndSdkClasses.singleOrNull {
         it.signature == field.enclosingClass
     } ?: return null
@@ -363,7 +369,7 @@ fun TsContext.assignToStaticField(
     val instance = scope.calcOnState { getStaticInstance(clazz) }
 
     val sort = run {
-        val fields = clazz.fields.filter { it.name == field.name }
+        val fields = clazz.fields.filter { it.hasStringName(field.name) }
         if (fields.size == 1) {
             val field = fields.single()
             val sort = typeToSort(field.type)

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt

@@ -231,6 +231,9 @@ class TsInterpreter(
 
         val instance = stmt.instance
         val callee = stmt.call.callee
+        if (callee.wellKnownSymbol != null) {
+            throw UnsupportedOperationException("Symbol-keyed method dispatch is not supported")
+        }
 
         fun selectedMethod(receiverClass: EtsClass): EtsMethod? = if (stmt.call.isSuperCall) {
             graph.hierarchy.explicitSuperMethod(receiverClass, callee)
@@ -256,6 +259,10 @@ class TsInterpreter(
             TsExprApproximationResult.NoApproximation -> {}
         }
 
+        if (stmt.call.wellKnownSymbol != null) {
+            throw UnsupportedOperationException("Symbol-keyed method dispatch requires a supported intrinsic receiver")
+        }
+
         if (instance.sort != addressSort) {
             unknownCallDispatcher.dispatch(scope, stmt, Reason.NON_REFERENCE_RECEIVER, instance)
             return

usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt

@@ -31,7 +31,9 @@ fun TsContext.resolveEtsField(
             error("Multiple classes with name ${field.enclosingClass.name}")
         }
         val clazz = classes.single()
-        val fields = clazz.getAllFields(hierarchy).filter { it.name == field.name }
+        val fields = clazz.getAllFields(hierarchy).filter {
+            it.name == field.name && it.signature.wellKnownSymbol == field.wellKnownSymbol
+        }
         if (fields.size == 1) {
             return TsResolutionResult.create(fields.single())
         }
@@ -41,19 +43,21 @@ fun TsContext.resolveEtsField(
     if (instance != null) {
         when (val instanceType = instance.type) {
             is EtsClassType -> {
-                val field = tryGetSingleField(scene, instanceType.signature.name, field.name, hierarchy)
+                val field = tryGetSingleField(scene, instanceType.signature.name, field, hierarchy)
                 if (field != null) return TsResolutionResult.create(field)
             }
 
             is EtsUnclearRefType -> {
-                val field = tryGetSingleField(scene, instanceType.typeName, field.name, hierarchy)
+                val field = tryGetSingleField(scene, instanceType.typeName, field, hierarchy)
                 if (field != null) return TsResolutionResult.create(field)
             }
         }
     }
 
     val fields = scene.projectAndSdkClasses.flatMap { cls ->
-        cls.getAllFields(hierarchy).filter { it.name == field.name }
+        cls.getAllFields(hierarchy).filter {
+            it.name == field.name && it.signature.wellKnownSymbol == field.wellKnownSymbol
+        }
     }
 
     return TsResolutionResult.create(fields)
@@ -62,27 +66,28 @@ fun TsContext.resolveEtsField(
 private fun tryGetSingleField(
     scene: EtsScene,
     className: String,
-    fieldName: String,
+    field: EtsFieldSignature,
     hierarchy: EtsHierarchy,
 ): EtsField? {
     val classes = scene.projectAndSdkClasses.filter { cls ->
         cls.name == className
     }
     if (classes.size == 1) {
         val clazz = classes.single()
-        val fields = clazz.getAllFields(hierarchy).filter { it.name == fieldName }
+        val fields = clazz.getAllFields(hierarchy).filter {
+            it.name == field.name && it.signature.wellKnownSymbol == field.wellKnownSymbol
+        }
         if (fields.isEmpty()) {
-            // logger.warn { "No field with name '$fieldName' in class '${clazz.name}'" }
             return null
         }
         if (fields.size > 1) {
-            logger.warn { "Multiple fields with name '$fieldName' in class '${clazz.name}': $fields" }
+            logger.warn { "Multiple fields with name '${field.name}' in class '${clazz.name}': $fields" }
             return null
         }
         return fields.single()
     }
     val fields = classes.flatMap { cls ->
-        cls.fields.filter { it.name == fieldName }
+        cls.fields.filter { it.name == field.name && it.signature.wellKnownSymbol == field.wellKnownSymbol }
     }
     if (fields.size == 1) {
         return fields.single()
@@ -110,10 +115,13 @@ fun EtsClass.getAllProperties(hierarchy: EtsHierarchy): Pair<Set<EtsFieldName>,
     val classes = hierarchy.getAncestors(this)
 
     classes.forEach {
-        val fieldNames = it.fields.map<EtsField, EtsFieldName> { it.name }
+        val fieldNames = it.fields.filter { field -> field.signature.wellKnownSymbol == null }
+            .map<EtsField, EtsFieldName> { it.name }
         allFields.addAll(fieldNames)
 
-        val methods = it.methods.filter { it.name != CONSTRUCTOR_NAME }
+        val methods = it.methods.filter { method ->
+            method.signature.wellKnownSymbol == null && method.name != CONSTRUCTOR_NAME
+        }
         val methodNames = methods.map<EtsMethod, EtsFieldName> { it.name }
         allMethods.addAll(methodNames)
     }