diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index fa3a6c9aca..4e94f7b95a 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/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" diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt index f575a1071f..f4b5a58a94 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsClassDataRegistryOracleTest.kt +++ b/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, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt index f54fbddef6..042517c2ee 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallStatic.kt +++ b/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( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/InputObjectProperties.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/InputObjectProperties.kt index c08b86af09..f43fdcd3a9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/InputObjectProperties.kt +++ b/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 } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ObjectPropertyUtil.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ObjectPropertyUtil.kt index c10cef332a..941a2570a6 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ObjectPropertyUtil.kt +++ b/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 } || diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index 0d952dade4..1a94e3d6b8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/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 diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt index c7da5d879a..9766897a0d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt +++ b/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, ) 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 4483abd36e..45d01dc4ce 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 @@ -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 } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index f1e29d64aa..76c60cdea2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/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) 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 81aa89a000..22865401ac 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 @@ -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 diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt index 2fbbe2fa8a..9df7526cf8 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsFieldResolver.kt +++ b/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,7 +66,7 @@ fun TsContext.resolveEtsField( private fun tryGetSingleField( scene: EtsScene, className: String, - fieldName: String, + field: EtsFieldSignature, hierarchy: EtsHierarchy, ): EtsField? { val classes = scene.projectAndSdkClasses.filter { cls -> @@ -70,19 +74,20 @@ private fun tryGetSingleField( } 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, val classes = hierarchy.getAncestors(this) classes.forEach { - val fieldNames = it.fields.map { it.name } + val fieldNames = it.fields.filter { field -> field.signature.wellKnownSymbol == null } + .map { 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 { it.name } allMethods.addAll(methodNames) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index 79db08ffa4..2255d25c52 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -117,7 +117,7 @@ class EtsHierarchy(private val scene: EtsScene) { while (classes.isNotEmpty()) { val current = classes.removeFirst() - val method = current.methods.firstOrNull { !it.isStatic && it.name == methodName } + val method = current.methods.firstOrNull { !it.isStatic && it.hasStringName(methodName) } if (method != null) return method val superClasses = current.superClass?.let(::resolveClassesBySignature).orEmpty() @@ -131,14 +131,14 @@ class EtsHierarchy(private val scene: EtsScene) { .filter { it.name == "Object" } .sortedBy { it.signature.toString() } .mapNotNull { sdkObject -> - sdkObject.methods.firstOrNull { !it.isStatic && it.name == methodName } + sdkObject.methods.firstOrNull { !it.isStatic && it.hasStringName(methodName) } } .firstOrNull() if (objectMethod != null) return objectMethod while (interfaces.isNotEmpty()) { val current = interfaces.removeFirst() - val method = current.methods.firstOrNull { !it.isStatic && it.name == methodName } + val method = current.methods.firstOrNull { !it.isStatic && it.hasStringName(methodName) } if (method != null) return method val parents = current.implementedInterfaces.flatMap(::resolveClassesBySignature) @@ -150,6 +150,8 @@ class EtsHierarchy(private val scene: EtsScene) { /** Explicit `super.m()` starts lookup at the declared superclass, not the receiver's override. */ fun explicitSuperMethod(receiverClass: EtsClass, callee: EtsMethodSignature): EtsMethod? { + if (callee.wellKnownSymbol != null) return null + val ancestors = getAncestors(receiverClass) - receiverClass val declaredSuperclasses = classesForType(EtsClassType(callee.enclosingClass)) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsMemberNames.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsMemberNames.kt new file mode 100644 index 0000000000..6fd799531f --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsMemberNames.kt @@ -0,0 +1,17 @@ +package org.usvm.util + +import org.jacodb.ets.model.EtsField +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsMethod + +internal fun EtsField.hasStringName(name: String): Boolean = + signature.wellKnownSymbol == null && this.name == name + +internal fun EtsMethod.hasStringName(name: String): Boolean = + signature.wellKnownSymbol == null && this.name == name + +internal fun EtsFieldSignature.requireStringKey() { + if (wellKnownSymbol != null) { + throw UnsupportedOperationException("Symbol-keyed field storage is not supported: $wellKnownSymbol") + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsMethodOverloads.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsMethodOverloads.kt index f1e4a4d1df..cd67880b53 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsMethodOverloads.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsMethodOverloads.kt @@ -9,6 +9,7 @@ internal fun EtsMethod.executableOverloadImplementation(): EtsMethod { ?.methods ?.filter { candidate -> candidate.name == name && + candidate.signature.wellKnownSymbol == signature.wellKnownSymbol && candidate.isStatic == isStatic && candidate.cfg.stmts.isNotEmpty() } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/InputPropertyDeclaration.kt b/usvm-ts/src/main/kotlin/org/usvm/util/InputPropertyDeclaration.kt index f4734cb435..723e303845 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/InputPropertyDeclaration.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/InputPropertyDeclaration.kt @@ -30,7 +30,7 @@ fun resolveInstanceProperty( val declarations = hierarchy.classesForType(type).map { receiver -> val fieldOwners = hierarchy.getAncestors(receiver).filter { owner -> - owner.fields.any { !it.isStatic && it.name == name } + owner.fields.any { !it.isStatic && it.hasStringName(name) } } // A class field defines the value even when an implemented interface has a weaker contract. val classOwners = fieldOwners.filter { it.category != EtsClassCategory.INTERFACE } @@ -41,7 +41,7 @@ fun resolveInstanceProperty( owners.none { descendant -> owner != descendant && owner in hierarchy.getAncestors(descendant) } } val nearestFields = nearestOwners.flatMap { owner -> - owner.fields.filter { field -> !field.isStatic && field.name == name } + owner.fields.filter { field -> !field.isStatic && field.hasStringName(name) } } val nearestDeclarations = nearestFields .map { field -> 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 8821bd93c4..b2b5e3ad74 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/LValueUtil.kt @@ -56,7 +56,10 @@ fun mkFieldLValue( sort: Sort, ref: UHeapRef, field: EtsFieldSignature, -): UFieldLValue = mkFieldLValue(sort, ref, field.name) +): UFieldLValue { + field.requireStringKey() + return mkFieldLValue(sort, ref, field.name) +} fun mkFieldLValue( sort: Sort, diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/MethodResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/MethodResolver.kt index c2e36fecc0..f1ef1f1994 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/MethodResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/MethodResolver.kt @@ -24,7 +24,7 @@ fun TsContext.resolveEtsMethods( val methods = classes.flatMap { it.methods }.filter { - it.name == method.name + it.name == method.name && it.signature.wellKnownSymbol == method.wellKnownSymbol } return methods } @@ -39,7 +39,7 @@ fun TsContext.resolveEtsMethods( val methods = classes.flatMap { it.methods }.filter { - it.name == method.name + it.name == method.name && it.signature.wellKnownSymbol == method.wellKnownSymbol } return methods } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/TypeCoercion.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/TypeCoercion.kt index aab7e5c3b6..5733b4e92f 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/TypeCoercion.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/TypeCoercion.kt @@ -3,18 +3,31 @@ package org.usvm.samples.lang import org.jacodb.ets.model.EtsScene import org.junit.jupiter.api.Disabled import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.StateCollectionStrategy import org.usvm.api.TsTestValue import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath import org.usvm.util.isTruthy +import java.nio.file.Path +import kotlin.io.path.readText private val TsTestValue.TsBoolean.number: Double get() = if (value) 1.0 else 0.0 class TypeCoercion : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + private val tsPath = "/samples/lang/TypeCoercion.ts" override val scene: EtsScene = loadScene(tsPath) + init { + options = options.copy(stopOnCoverage = 0, stateCollectionStrategy = StateCollectionStrategy.ALL) + } + @Test fun `test argWithConst`() { val method = getMethod("argWithConst") @@ -90,12 +103,62 @@ class TypeCoercion : TsMethodTestRunner() { } @Test - fun `test transitiveCoercionNoTypes`() { - val method = getMethod("transitiveCoercionNoTypes") + fun `untyped transitive coercion retains every numeric branch`() { + val method = getMethod("transitiveCoercionNumbers") + + discoverProperties( + method = method, + { _, _, _, result -> result.number == 1.0 }, + { _, _, _, result -> result.number == 2.0 }, + { _, _, _, result -> result.number == 3.0 }, + { _, _, _, result -> result.number == 4.0 }, + invariants = arrayOf({ a, b, c, result -> + result.number == transitiveResult(a.number, b.number, c.number) + }), + ) + } + + @Test + fun `untyped transitive coercion converts boolean inputs to numbers`() { + val method = getMethod("transitiveCoercionBoolean") - discoverProperties( - method, - // Too complicated to write property matchers, examine run log to verify the test. + discoverProperties( + method = method, + { _, _, _, result -> result.number == 2.0 }, + { _, _, _, result -> result.number == 3.0 }, + { _, _, _, result -> result.number == 4.0 }, + invariants = arrayOf({ a, b, c, result -> + result.number == transitiveResult(a.number, b.number, c.number) + }), ) } + + @Test + fun `native coercion agrees with numeric and boolean branch expectations`() { + assertNodeReplay( + source = getResourcePath(tsPath).readText() + "\n" + """ + const subject = new TypeCoercion(); + const numeric = [ + [2, 2, 2, 1], [2, 2, 3, 2], [1, 2, 3, 3], [0, 0, 0, 4], + [NaN, NaN, 2, 3], [Infinity, Infinity, Infinity, 1], [-0, 0, -0, 4], + ]; + for (const [a, b, c, expected] of numeric) { + if (subject.transitiveCoercionNumbers(a, b, c) !== expected) throw Error('numeric coercion'); + } + for (const [a, b, c, expected] of [[0, false, 2, 2], [1, false, 2, 3], [0, false, 0, 4]]) { + if (subject.transitiveCoercionBoolean(a, b, c) !== expected) throw Error('boolean coercion'); + } + """.trimIndent(), + directory = directory, + name = "transitive-coercion", + timeoutMessage = "Native transitive coercion replay timed out", + ) + } + + private fun transitiveResult(a: Double, b: Double, c: Double): Double = when { + a != b -> 3.0 + c == 0.0 || c == 1.0 -> 4.0 + !c.isNaN() && a == c -> 1.0 + else -> 2.0 + } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/ComputedClassMembersTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/ComputedClassMembersTest.kt new file mode 100644 index 0000000000..2a01f5d98c --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/ComputedClassMembersTest.kt @@ -0,0 +1,117 @@ +package org.usvm.samples.types + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertFalse +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class ComputedClassMembersTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val sourcePath = "/samples/types/ComputedClassMembers.ts" + + override val scene: EtsScene = loadScene(sourcePath) + + @Test + fun `ordinary methods execute in plain literal and iterator classes`() { + for (name in listOf("plainCounter", "literalCounter", "iteratorCounter")) { + discoverConstant(name, expected = 7.0) + } + discoverConstant("literalStatic", expected = 11.0) + + replay( + """ + const subject = new ComputedClassMembers(); + for (const name of ['plainCounter', 'literalCounter', 'iteratorCounter']) { + if (subject[name]() !== 7) throw Error(name); + } + if (subject.literalStatic() !== 11) throw Error('literal static'); + """.trimIndent(), + ) + } + + @Test + fun `string lookalike calls select their ordinary declarations`() { + discoverConstant("stringMethod", expected = 29.0) + assertUnsupported("stringStaticMethod", reason = "Property access needs a modeled object") + + replay( + """ + const subject = new ComputedClassMembers(); + if (subject.stringMethod() !== 29) throw Error('string method'); + if (subject.stringStaticMethod() !== 43) throw Error('string static'); + if (subject.symbolMethod() !== 17) throw Error('symbol identity'); + """.trimIndent(), + ) + } + + @Test + fun `unsupported symbol initialization retains its cause and returns no string result`() { + assertUnsupported("symbolFieldInitialization", reason = "Symbol-keyed field storage") + } + + @Test + fun `symbol access is explicit unsupported instead of returning the string method result`() { + assertUnsupported("symbolMethod", reason = null) + } + + @Test + fun `shadowed and dynamic keys keep frontend barriers`() { + assertUnsupported("shadowedSymbol", reason = "Unsupported frontend") + assertUnsupported("dynamicKey", reason = "Unsupported frontend") + } + + private fun discoverConstant(methodName: String, expected: Double) { + discoverProperties( + method = getMethod(methodName, className = "ComputedClassMembers"), + { result -> result.number == expected }, + invariants = arrayOf({ result -> result.number == expected }), + ) + } + + private fun assertUnsupported(methodName: String, reason: String?) { + val method = getMethod(methodName, className = "ComputedClassMembers") + val result = TsMachine( + scene = scene, + options = UMachineOptions( + solverType = SolverType.YICES, + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = 20.seconds, + ), + tsOptions = TsOptions(), + ).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) } + + assertTrue(result.stopReason == TsAnalysisStopReason.EXHAUSTED, "$methodName: ${result.stopReason}") + assertTrue(result.states.isEmpty(), methodName) + assertFalse(result.engineFailed, methodName) + assertTrue(result.unsupportedPaths.isNotEmpty(), "$methodName: $result") + if (reason != null) { + assertTrue(result.unsupportedPaths.any { reason in it }, "$methodName: ${result.unsupportedPaths}") + } + } + + private fun replay(assertions: String) { + assertNodeReplay( + source = getResourcePath(sourcePath).readText() + "\n" + assertions, + directory = directory, + name = "computed-class-members", + timeoutMessage = "Computed class member native replay timed out", + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/EtsMemberIdentityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/util/EtsMemberIdentityTest.kt new file mode 100644 index 0000000000..a4475783ad --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/util/EtsMemberIdentityTest.kt @@ -0,0 +1,73 @@ +package org.usvm.util + +import io.mockk.mockk +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsWellKnownSymbol +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.machine.TsContext +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertNull + +class EtsMemberIdentityTest { + private val file = loadEtsFileAutoConvert(getResourcePath("/samples/types/ComputedClassMembers.ts")) + private val scene = EtsScene(projectFiles = listOf(file)) + private val hierarchy = EtsHierarchy(scene) + + @Test + fun `method resolution and inherited string lookup distinguish symbol declarations`() { + val ctx = TsContext(scene = scene, components = mockk()) + val owner = scene.projectClasses.single { it.name == "IteratorCounter" } + val stringMethods = owner.methods.filter { it.hasStringName("Symbol.iterator") } + val symbolMethods = owner.methods.filter { it.signature.wellKnownSymbol == EtsWellKnownSymbol.ITERATOR } + val stringMethod = stringMethods.single { !it.isStatic } + + assertEquals(stringMethods, ctx.resolveEtsMethods(stringMethod.signature)) + assertEquals(symbolMethods, ctx.resolveEtsMethods(symbolMethods.first().signature)) + assertEquals(stringMethod, hierarchy.nearestInstanceMethod(owner, methodName = "Symbol.iterator")) + } + + @Test + fun `field resolution keeps identity through exact inferred and fallback owner lookup`() { + val ctx = TsContext(scene = scene, components = mockk()) + val owner = scene.projectClasses.single { it.name == "SymbolFieldCounter" } + + for (field in owner.fields) { + val exact = ctx.resolveEtsField(instance = null, field = field.signature, hierarchy = hierarchy) + val unknownOwner = field.signature.copy(enclosingClass = EtsClassSignature.UNKNOWN) + val receiverTypes = listOf( + EtsClassType(owner.signature), + EtsUnclearRefType(name = owner.name, typeParameters = emptyList()), + ) + + assertEquals(TsResolutionResult.Unique(field), exact) + for (type in receiverTypes) { + val inferred = ctx.resolveEtsField( + instance = EtsLocal(name = "receiver", type = type), + field = unknownOwner, + hierarchy = hierarchy, + ) + + assertEquals(TsResolutionResult.Unique(field), inferred) + } + assertEquals( + TsResolutionResult.Unique(field), + ctx.resolveEtsField(instance = null, field = unknownOwner, hierarchy = hierarchy), + ) + } + } + + @Test + fun `symbol-only members do not imply ordinary string properties`() { + val owner = scene.projectClasses.single { it.name == "SymbolOnlyCounter" } + val properties = owner.getAllPropertiesCombined(hierarchy) + + assertFalse("Symbol.iterator" in properties) + assertNull(hierarchy.nearestInstanceMethod(owner, methodName = "Symbol.iterator")) + } +} 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 ecc3a2f44a..516185393e 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -563,7 +563,9 @@ open class TsTestStateResolver( val tracked = propertyState?.trackedObjectProperties.orEmpty() .filter { evaluateInModel(it.instance) == concreteRef } .groupBy { it.name } - val declaredFields = clazz.fields.filterNot { (it as EtsFieldImpl).modifiers.isStatic } + val declaredFields = clazz.fields.filter { + !it.isStatic && it.signature.wellKnownSymbol == null + } declaredFields.forEach { field -> if (field.name in tracked) return@forEach if ((field as EtsFieldImpl).isOptional && !concreteRef.isAllocated) return@forEach diff --git a/usvm-ts/src/test/resources/samples/lang/TypeCoercion.ts b/usvm-ts/src/test/resources/samples/lang/TypeCoercion.ts index 79deb9040a..ba01c77b53 100644 --- a/usvm-ts/src/test/resources/samples/lang/TypeCoercion.ts +++ b/usvm-ts/src/test/resources/samples/lang/TypeCoercion.ts @@ -79,6 +79,14 @@ class TypeCoercion { return 3; } + transitiveCoercionNumbers(a: number, b: number, c: number): number { + return this.transitiveCoercionNoTypes(a, b, c); + } + + transitiveCoercionBoolean(a: number, b: boolean, c: number): number { + return this.transitiveCoercionNoTypes(a, b, c); + } + transitiveCoercionNoTypes(a, b, c): number { if (a == b) { if (c != 0 && c != 1) { diff --git a/usvm-ts/src/test/resources/samples/types/ComputedClassMembers.ts b/usvm-ts/src/test/resources/samples/types/ComputedClassMembers.ts new file mode 100644 index 0000000000..39879cd6d0 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/ComputedClassMembers.ts @@ -0,0 +1,52 @@ +class PlainCounter { + value = 3; + increment(value: number): number { return this.value + value; } +} + +class LiteralCounter { + ['value'] = 3; + ['increment'](value: number): number { return this.value + value; } + static ['answer'](): number { return 11; } +} + +class IteratorCounter { + value = 3; + [Symbol.iterator](): number { return 17; } + ['Symbol.iterator'](): number { return 29; } + increment(value: number): number { return this.value + value; } + static [Symbol.iterator](): number { return 31; } + static ['Symbol.iterator'](): number { return 43; } +} + +class SymbolFieldCounter { + [Symbol.iterator] = 17; + ['Symbol.iterator'] = 29; + increment(value: number): number { return value + 1; } +} + +class SymbolOnlyCounter { + [Symbol.iterator](): number { return 17; } +} + +export class ComputedClassMembers { + plainCounter(): number { return new PlainCounter().increment(4); } + literalCounter(): number { return new LiteralCounter().increment(4); } + iteratorCounter(): number { return new IteratorCounter().increment(4); } + literalStatic(): number { return LiteralCounter.answer(); } + stringMethod(): number { return new IteratorCounter()['Symbol.iterator'](); } + stringStaticMethod(): number { return IteratorCounter['Symbol.iterator'](); } + symbolMethod(): number { return new IteratorCounter()[Symbol.iterator](); } + symbolFieldInitialization(): number { return new SymbolFieldCounter().increment(4); } + + shadowedSymbol(): number { + const Symbol = { iterator: 'increment' }; + const Counter = class { [Symbol.iterator](): number { return 19; } }; + return new Counter().increment(); + } + + dynamicKey(): number { + const key = () => 'increment'; + const Counter = class { [key()](): number { return 23; } }; + return new Counter().increment(); + } +}