From 9457bec64707e8fbd3470168f02e88cc3e8e5d3d Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 03:09:14 +0300 Subject: [PATCH 1/6] Compose plain-object Calls inputs with recursive domains and current runtime diagnostics --- .../org/usvm/ts/calls/CallsCoverageReplay.kt | 10 + .../org/usvm/ts/calls/CallsCoverageSearch.kt | 18 +- .../usvm/ts/calls/CallsInputMaterializer.kt | 63 ++- .../org/usvm/ts/calls/CallsInputSnapshot.kt | 11 + .../ts/calls/CallsInputTypeCompatibility.kt | 65 ++- .../org/usvm/ts/calls/CallsObjectShapes.kt | 72 ++++ .../org/usvm/ts/calls/CallsSourceReplay.kt | 3 + .../org/usvm/ts/calls/CallsSymbolicInputs.kt | 12 +- .../ts/calls/CurrentTsCallsSymbolicEngine.kt | 4 +- .../ts/calls/CallsCoverageExperimentTest.kt | 49 +++ .../usvm/ts/calls/CallsObjectInputsTest.kt | 402 ++++++++++++++++++ .../usvm/samples/lang/StoredFunctionCall.kt | 11 + .../samples/lang/StoredFunctionCall.ts | 21 + 13 files changed, 719 insertions(+), 22 deletions(-) create mode 100644 usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsObjectShapes.kt create mode 100644 usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsObjectInputsTest.kt diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageReplay.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageReplay.kt index 8fc9ccef9d..1dadb1eec8 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageReplay.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageReplay.kt @@ -302,6 +302,16 @@ private fun coverageWrapper( return { kind: 'number', value: 'finite', bits }; } if (Array.isArray(value)) return { kind: 'array', elements: value.map(encodeValue) }; + if (value !== null && typeof value === 'object' && + (Object.getPrototypeOf(value) === Object.prototype || Object.getPrototypeOf(value) === null)) { + const fields = Object.fromEntries(Object.entries(value).map(([name, field]) => { + if (['__proto__', 'constructor', 'prototype'].includes(name)) { + throw new Error('Unsupported replay object property name'); + } + return [name, encodeValue(field)]; + })); + return { kind: 'object', fields }; + } throw new Error('Unsupported replay argument type'); } diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt index fea534a64e..2fcec4d4f6 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsCoverageSearch.kt @@ -7,8 +7,10 @@ import org.usvm.SolverType import org.usvm.StateCollectionStrategy import org.usvm.UMachineOptions import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent import org.usvm.machine.call.TsUnknownCallModelSelection import org.usvm.machine.interpreter.TsInitialStateSolverUnknownException import org.usvm.machine.state.TsMethodResult @@ -63,6 +65,7 @@ internal data class CallsCoverageSearchResult( val unsupportedCall: Boolean = false, val engineFailed: Boolean = false, val runtimeLimited: Boolean = false, + val runtimeLimitationReasons: List = emptyList(), val diagnostic: String? = null, ) @@ -111,6 +114,7 @@ internal class CurrentTsCallsCoverageEngine( bindings = preparation.inputBindings, lexicalEnvironment = preparation.lexicalEnvironment, captures = preparation.captures, + sourceScene = preparation.scene, ) val candidates = mutableListOf() val extractionFailures = mutableListOf() @@ -133,16 +137,25 @@ internal class CurrentTsCallsCoverageEngine( } else { TsUnknownCallModelSelection.Only(emptySet()) } + val runtimeLimitationReasons = linkedSetOf() + val interpreterObserver = object : TsInterpreterObserver { + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + runtimeLimitationReasons += event.reason.name + } + } + val inputCapacity = request.function.inputs.maxOfOrNull { it.domain.callsInputCapacity() } ?: 0 val machineOptions = coverageMachineOptions(request) val machineResult = runCatching { TsMachine( - scene = preparation.scene, + scene = symbolicInputs.scene, options = machineOptions, tsOptions = TsOptions( + maxArraySize = maxOf(TsOptions().maxArraySize, inputCapacity), unknownCallModelSelection = modelSelection, unknownCallFallback = request.profile.fallback, ), machineObserver = observer, + observer = interpreterObserver, ).use { machine -> machine.analyzeWithMetadata( methods = listOf(preparation.method), @@ -177,7 +190,8 @@ internal class CurrentTsCallsCoverageEngine( machineTeardownElapsedMillis = machineTeardownElapsedMillis, unsupportedCall = outcome?.unsupportedCall == true, engineFailed = outcome?.engineFailed == true, - runtimeLimited = outcome?.runtimeLimited == true, + runtimeLimited = outcome?.runtimeLimited == true || runtimeLimitationReasons.isNotEmpty(), + runtimeLimitationReasons = runtimeLimitationReasons.toList(), diagnostic = machineResult.exceptionOrNull()?.let { error -> error.message ?: error::class.java.name }, ) } diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt index 868987148f..121953170c 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt @@ -6,6 +6,7 @@ import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStringType @@ -29,14 +30,19 @@ 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 +import org.usvm.ts.pbt.model.ObjectDomain import org.usvm.ts.pbt.model.OptionalDomain import org.usvm.ts.pbt.model.PropertyDomain import org.usvm.ts.pbt.model.StringDomain import org.usvm.util.allocateBoundedString import org.usvm.util.componentType import org.usvm.util.mkArrayIndexLValue +import org.usvm.util.mkFieldLValue -internal fun TsState.materializeCallsInput(domain: PropertyDomain): MaterializedCallsInput = with(ctx) { +internal fun TsState.materializeCallsInput( + domain: PropertyDomain, + objectShapes: CallsObjectShapes, +): MaterializedCallsInput = with(ctx) { when (domain) { BooleanDomain -> { val value = makeSymbolicPrimitive(boolSort) @@ -63,10 +69,13 @@ internal fun TsState.materializeCallsInput(domain: PropertyDomain): Materialized ) } is OptionalDomain -> { - materializeCallsOptional(domain) + materializeCallsOptional(domain = domain, objectShapes = objectShapes) } is ArrayDomain -> { - materializeCallsArray(domain) + materializeCallsArray(domain = domain, objectShapes = objectShapes) + } + is ObjectDomain -> { + materializeCallsObject(domain = domain, objectShapes = objectShapes) } else -> { error("Unsupported Calls input domain: $domain") @@ -74,6 +83,27 @@ internal fun TsState.materializeCallsInput(domain: PropertyDomain): Materialized } } +private fun TsState.materializeCallsObject( + domain: ObjectDomain, + objectShapes: CallsObjectShapes, +): MaterializedCallsInput = with(ctx) { + val runtimeType = objectShapes.typeOf(domain) + val reference = memory.allocConcrete(runtimeType) + val fields = domain.fields.mapValues { (name, fieldDomain) -> + val field = materializeCallsInput(domain = fieldDomain, objectShapes = objectShapes) + val sort = field.value.sort + + memory.write( + mkFieldLValue(sort, reference, name), + field.value.asExpr(sort), + guard = trueExpr, + ) + field.snapshot + } + + MaterializedCallsInput(reference, ObjectInputSnapshot(fields)) +} + private fun TsState.initializeIntegerInput(domain: IntegerDomain): UExpr = with(ctx) { if (domain.min == domain.max) return mkFp64(domain.min.toDouble()) @@ -105,8 +135,11 @@ private fun TsState.materializeCallsConstant(value: JsConcreteValue): UExpr<*> = } } -private fun TsState.materializeCallsOptional(domain: OptionalDomain): MaterializedCallsInput = with(ctx) { - val nested = materializeCallsInput(domain.value) +private fun TsState.materializeCallsOptional( + domain: OptionalDomain, + objectShapes: CallsObjectShapes, +): MaterializedCallsInput = with(ctx) { + val nested = materializeCallsInput(domain = domain.value, objectShapes = objectShapes) val nil = materializeCallsConstant(domain.nil) val chooseValue: UBoolExpr = makeSymbolicPrimitive(boolSort) val nestedBool = extractValue(nested.value, boolSort, ::getIntermediateBoolLValue) @@ -131,7 +164,7 @@ private fun TsState.materializeCallsOptional(domain: OptionalDomain): Materializ MaterializedCallsInput(value, OptionalInputSnapshot(chooseValue, nested.snapshot, domain.nil)) } -private fun PropertyDomain.callsRuntimeType(): EtsType = when (this) { +internal fun PropertyDomain.callsRuntimeType(objectType: (ObjectDomain) -> EtsClassType): EtsType = when (this) { BooleanDomain -> { EtsBooleanType } @@ -142,7 +175,7 @@ private fun PropertyDomain.callsRuntimeType(): EtsType = when (this) { EtsStringType } is ArrayDomain -> { - val nestedType = element.callsRuntimeType() + val nestedType = element.callsRuntimeType(objectType) if (nestedType is EtsArrayType) { nestedType.copy(dimensions = nestedType.dimensions + 1) } else { @@ -150,10 +183,13 @@ private fun PropertyDomain.callsRuntimeType(): EtsType = when (this) { } } is OptionalDomain -> { - val nestedType = value.callsRuntimeType() - val nilType = ConstantDomain(nil).callsRuntimeType() + val nestedType = value.callsRuntimeType(objectType) + val nilType = ConstantDomain(nil).callsRuntimeType(objectType) EtsUnionType(types = listOf(nestedType, nilType)) } + is ObjectDomain -> { + objectType(this) + } is ConstantDomain -> { when (value) { is JsConcreteValue.Boolean -> EtsBooleanType @@ -171,8 +207,11 @@ private fun PropertyDomain.callsRuntimeType(): EtsType = when (this) { } } -private fun TsState.materializeCallsArray(domain: ArrayDomain): MaterializedCallsInput = with(ctx) { - val runtimeType = domain.callsRuntimeType() as EtsArrayType +private fun TsState.materializeCallsArray( + domain: ArrayDomain, + objectShapes: CallsObjectShapes, +): MaterializedCallsInput = with(ctx) { + val runtimeType = domain.callsRuntimeType(objectShapes::typeOf) as EtsArrayType val descriptor = arrayDescriptorOf(runtimeType) val arrayRef = memory.allocConcrete(runtimeType) val length = initializeLength(minLength = domain.minLength, maxLength = domain.maxLength) @@ -184,7 +223,7 @@ private fun TsState.materializeCallsArray(domain: ArrayDomain): MaterializedCall ) val elementSort = typeToSort(runtimeType.componentType) val elements = List(domain.maxLength) { index -> - val element = materializeCallsInput(domain.element) + val element = materializeCallsInput(domain = domain.element, objectShapes = objectShapes) val liveIndex = mkBvSignedLessExpr(mkBv(index), length) when (elementSort) { boolSort -> memory.write( diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputSnapshot.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputSnapshot.kt index 58f65526c9..9b4981f6f7 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputSnapshot.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputSnapshot.kt @@ -82,6 +82,17 @@ internal data class ArrayInputSnapshot( } } +internal data class ObjectInputSnapshot( + val fields: Map, +) : CallsInputSnapshot { + override fun markDenseInputs(state: TsState) { + fields.values.forEach { field -> field.markDenseInputs(state) } + } + + override fun resolve(model: UModelBase): JsConcreteValue = + JsConcreteValue.Object(fields.mapValues { (_, snapshot) -> snapshot.resolve(model) }) +} + internal data class ConstantInputSnapshot(val value: JsConcreteValue) : CallsInputSnapshot { override fun resolve(model: UModelBase): JsConcreteValue = value } diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputTypeCompatibility.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputTypeCompatibility.kt index 5880dfcaed..490ff04e90 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputTypeCompatibility.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputTypeCompatibility.kt @@ -5,15 +5,19 @@ import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanLiteralType import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsGenericType import org.jacodb.ets.model.EtsIntersectionType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNullType import org.jacodb.ets.model.EtsNumberLiteralType import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsRefType +import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStringLiteralType import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType @@ -24,18 +28,23 @@ 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 +import org.usvm.ts.pbt.model.ObjectDomain import org.usvm.ts.pbt.model.OptionalDomain import org.usvm.ts.pbt.model.PropertyDomain import org.usvm.ts.pbt.model.PropertyInput import org.usvm.ts.pbt.model.StringDomain +import org.usvm.util.EtsHierarchy import org.usvm.util.componentType +import org.usvm.util.getAllFields /** Rejects bindings whose frozen domain would replace a source parameter with an incompatible runtime kind. */ internal fun callsInputTypePreflight( inputs: List, bindings: List, method: EtsMethod, + scene: EtsScene, ): String? { + val hierarchy = EtsHierarchy(scene) val domainsByName = inputs.associate { input -> input.name to input.domain } val genericParameters = method.typeParameters.filterIsInstance().associateBy { it.typeName } for (binding in bindings) { @@ -43,6 +52,7 @@ internal fun callsInputTypePreflight( type = binding.parameter.type, genericParameters = genericParameters, path = "inputs.${binding.propertyInputName}", + hierarchy = hierarchy, ) if (limitation != null) { return "$limitation (source parameter ${binding.parameter.name}, stack slot ${binding.stackSlot})" @@ -56,13 +66,14 @@ private fun PropertyDomain.inputTypeLimitation( type: EtsType, genericParameters: Map, path: String, + hierarchy: EtsHierarchy, visitedGenerics: Set = emptySet(), ): String? { if (this is OptionalDomain) { - val valueLimitation = value.inputTypeLimitation(type, genericParameters, path, visitedGenerics) + val valueLimitation = value.inputTypeLimitation(type, genericParameters, path, hierarchy, visitedGenerics) if (valueLimitation != null) return valueLimitation - return ConstantDomain(nil).inputTypeLimitation(type, genericParameters, "$path.nil", visitedGenerics) + return ConstantDomain(nil).inputTypeLimitation(type, genericParameters, "$path.nil", hierarchy, visitedGenerics) } val constant = (this as? ConstantDomain)?.value @@ -106,10 +117,10 @@ private fun PropertyDomain.inputTypeLimitation( } val upperBound = type.constraint ?: genericParameters[type.typeName]?.constraint ?: EtsUnknownType - return inputTypeLimitation(upperBound, genericParameters, path, visitedGenerics + type.typeName) + return inputTypeLimitation(upperBound, genericParameters, path, hierarchy, visitedGenerics + type.typeName) } is EtsAliasType -> { - return inputTypeLimitation(type.originalType, genericParameters, path, visitedGenerics) + return inputTypeLimitation(type.originalType, genericParameters, path, hierarchy, visitedGenerics) } is EtsArrayType -> { val isSupportedArray = this is ArrayDomain && type.dimensions >= 1 @@ -118,17 +129,27 @@ private fun PropertyDomain.inputTypeLimitation( type = type.componentType, genericParameters = genericParameters, path = "$path[]", + hierarchy = hierarchy, visitedGenerics = visitedGenerics, ) } false } + is EtsClassType, is EtsUnclearRefType -> { + return objectFieldTypeLimitation( + type = type as EtsRefType, + genericParameters = genericParameters, + path = path, + hierarchy = hierarchy, + visitedGenerics = visitedGenerics, + ) + } is EtsUnionType -> { - type.types.any { member -> inputTypeLimitation(member, genericParameters, path, visitedGenerics) == null } + type.types.any { member -> inputTypeLimitation(member, genericParameters, path, hierarchy, visitedGenerics) == null } } is EtsIntersectionType -> { for (member in type.types) { - val limitation = inputTypeLimitation(member, genericParameters, path, visitedGenerics) + val limitation = inputTypeLimitation(member, genericParameters, path, hierarchy, visitedGenerics) if (limitation != null) return limitation } true @@ -140,3 +161,35 @@ private fun PropertyDomain.inputTypeLimitation( return if (compatible) null else "$path: frozen domain $this is not supported for declared type $type" } + +private fun PropertyDomain.objectFieldTypeLimitation( + type: EtsRefType, + genericParameters: Map, + path: String, + hierarchy: EtsHierarchy, + visitedGenerics: Set, +): String? { + if (this !is ObjectDomain) { + return "$path: frozen domain $this requires a compatible object domain for declared type $type" + } + + val declaredFields = hierarchy.classesForType(type).flatMap { clazz -> clazz.getAllFields(hierarchy) } + for ((name, domain) in fields) { + val fieldPath = "$path.$name" + val fieldType = declaredFields.filter { field -> field.name == name } + .distinctBy { field -> field.signature } + .singleOrNull() + ?.type + ?: return "$fieldPath: cannot resolve the declared field type in $type" + val limitation = domain.inputTypeLimitation( + type = fieldType, + genericParameters = genericParameters, + path = fieldPath, + hierarchy = hierarchy, + visitedGenerics = visitedGenerics, + ) + if (limitation != null) return limitation + } + + return null +} diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsObjectShapes.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsObjectShapes.kt new file mode 100644 index 0000000000..eacff7ac6d --- /dev/null +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsObjectShapes.kt @@ -0,0 +1,72 @@ +package org.usvm.ts.calls + +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassCategory +import org.jacodb.ets.model.EtsClassImpl +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFieldImpl +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsFileSignature +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsType +import org.usvm.ts.pbt.model.ObjectDomain +import org.usvm.ts.pbt.model.PropertyDomain + +/** Runtime shapes of the own data properties emitted by the concrete input generator. */ +internal class CallsObjectShapes(sourceScene: EtsScene, domains: List) { + private val shapes = linkedMapOf() + private val classes = mutableListOf() + private val occupiedNames = sourceScene.projectAndSdkClasses.mapTo(mutableSetOf()) { it.name } + private val fileSignature: EtsFileSignature + val scene: EtsScene + + init { + val occupiedFiles = (sourceScene.projectFiles + sourceScene.sdkFiles).mapTo(mutableSetOf()) { it.signature } + sourceScene.projectAndSdkClasses.mapTo(occupiedFiles) { it.signature.file } + fileSignature = generateSequence(0) { it + 1 } + .map { index -> EtsFileSignature(projectName = "usvm-calls-inputs", fileName = "shapes-$index.ts") } + .first { it !in occupiedFiles } + domains.forEach(::register) + + scene = if (classes.isEmpty()) { + sourceScene + } else { + val file = EtsFile(signature = fileSignature, classes = classes, namespaces = emptyList()) + EtsScene( + projectFiles = sourceScene.projectFiles + file, + sdkFiles = sourceScene.sdkFiles, + projectName = sourceScene.projectName, + ) + } + } + + fun typeOf(domain: ObjectDomain): EtsClassType = shapes.getValue(domain) + + private fun register(domain: PropertyDomain): EtsType = domain.callsRuntimeType(::registerObject) + + private fun registerObject(domain: ObjectDomain): EtsClassType { + shapes[domain]?.let { return it } + + val name = generateSequence(shapes.size) { it + 1 } + .map { index -> "__usvm_calls_input_$index" } + .first { it !in occupiedNames } + occupiedNames += name + val signature = EtsClassSignature(name = name, file = fileSignature) + val type = EtsClassType(signature) + shapes[domain] = type + val fields = domain.fields.map { (fieldName, fieldDomain) -> + EtsFieldImpl(EtsFieldSignature(enclosingClass = signature, name = fieldName, type = register(fieldDomain))) + } + + // A source annotation supplies field layout, never methods or nominal ancestry. + classes += EtsClassImpl( + signature = signature, + fields = fields, + methods = emptyList(), + category = EtsClassCategory.OBJECT, + ) + return type + } +} diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceReplay.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceReplay.kt index ab1a8a021c..a7b0cd7923 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceReplay.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSourceReplay.kt @@ -14,6 +14,7 @@ import org.usvm.ts.pbt.model.BooleanDomain import org.usvm.ts.pbt.model.ConstantDomain import org.usvm.ts.pbt.model.ExecutionKind import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.ObjectDomain import org.usvm.ts.pbt.model.PropertyDefinition import org.usvm.ts.pbt.model.PropertyDomain import org.usvm.ts.pbt.model.PropertyId @@ -398,6 +399,8 @@ private fun JsConcreteValue.exactReplayDomain(): PropertyDomain = when (this) { TupleDomain(elements.map { element -> element.exactReplayDomain() }) } + is JsConcreteValue.Object -> ObjectDomain(fields.mapValues { (_, value) -> value.exactReplayDomain() }) + else -> ConstantDomain(this) } diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt index 2bb749d0b2..f53970bcd8 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt @@ -1,6 +1,7 @@ package org.usvm.ts.calls import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsScene import org.usvm.machine.state.TsState import org.usvm.ts.pbt.fastcheck.TypeScriptSourceCapture import org.usvm.ts.pbt.mapping.EtsInputBinding @@ -11,6 +12,7 @@ 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 +import org.usvm.ts.pbt.model.ObjectDomain import org.usvm.ts.pbt.model.OptionalDomain import org.usvm.ts.pbt.model.PropertyDomain import org.usvm.ts.pbt.model.PropertyInput @@ -23,6 +25,7 @@ internal fun PropertyDomain.isSupportedCallsSymbolicDomain(): Boolean = when (th is OptionalDomain -> value.isSupportedCallsSymbolicDomain() && (nil == JsConcreteValue.Null || nil == JsConcreteValue.Undefined) is ArrayDomain -> element.isSupportedCallsSymbolicDomain() + is ObjectDomain -> fields.values.all { it.isSupportedCallsSymbolicDomain() } else -> false } @@ -31,6 +34,7 @@ internal fun PropertyDomain.callsInputCapacity(): Int = when (this) { is ConstantDomain -> (value as? JsConcreteValue.String)?.value?.length ?: 0 is OptionalDomain -> value.callsInputCapacity() is ArrayDomain -> maxOf(maxLength, element.callsInputCapacity()) + is ObjectDomain -> fields.values.maxOfOrNull { it.callsInputCapacity() } ?: 0 else -> 0 } @@ -46,7 +50,11 @@ internal class CallsSymbolicInputs( bindings: List, private val lexicalEnvironment: EtsLexicalEnvironmentBinding?, private val captures: List, + sourceScene: EtsScene, ) { + private val objectShapes = CallsObjectShapes(sourceScene, inputs.map(PropertyInput::domain)) + val scene: EtsScene = objectShapes.scene + private val boundInputs: List> private var snapshots: List? = null @@ -69,6 +77,7 @@ internal class CallsSymbolicInputs( state.initializeInput( stackSlot = binding.stackSlot, domain = input.domain, + objectShapes = objectShapes, ) } initializedSnapshots.forEach { snapshot -> snapshot.markDenseInputs(state) } @@ -86,8 +95,9 @@ internal class CallsSymbolicInputs( private fun TsState.initializeInput( stackSlot: Int, domain: PropertyDomain, + objectShapes: CallsObjectShapes, ): CallsInputSnapshot = with(ctx) { - val input = materializeCallsInput(domain) + val input = materializeCallsInput(domain = domain, objectShapes = objectShapes) when (input.value.sort) { boolSort -> memory.write( mkRegisterStackLValue(boolSort, stackSlot), diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt index ceae9dffce..4e5a6d8ab9 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt @@ -193,13 +193,14 @@ internal class CurrentTsCallsSymbolicEngine( bindings = prepared.inputBindings, lexicalEnvironment = prepared.lexicalEnvironment, captures = prepared.captures, + sourceScene = scene, ) val interpreterObserver = UnknownCallEventSinkObserver( sink = request.unknownCallEventSink, runtimeLimitationSink = request.runtimeLimitationEventSink, ) val analysis = TsMachine( - scene = scene, + scene = symbolicInputs.scene, options = machineOptions, tsOptions = tsOptions, machineObserver = targetObserver, @@ -350,6 +351,7 @@ internal class CurrentTsCallsSymbolicEngine( inputs = request.function.inputs, bindings = mappedTarget.bindings.inputs, method = method, + scene = scene, ) if (inputTypeLimitation != null) { return CallsFunctionPreparation.Rejected( diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt index 1f3b4906d7..1ad61e3d10 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt @@ -5,6 +5,7 @@ import org.usvm.ts.pbt.model.ArrayDomain import org.usvm.ts.pbt.model.BooleanDomain import org.usvm.ts.pbt.model.JsConcreteValue import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.ObjectDomain import org.usvm.ts.pbt.model.PropertyInput import org.usvm.ts.pbt.model.StringDomain import org.usvm.ts.pbt.model.TypeScriptEntryPoint @@ -219,6 +220,54 @@ class CallsCoverageExperimentTest { assertTrue(replay.coveredStatementKeys.isNotEmpty()) } + @Test + fun `coverage search reports the concrete runtime limitation reason`() { + val fixture = fixture( + source = """ + export function writesNamedProperty(value: number): boolean { + const values = [1]; + values[0.5] = value; + return true; + } + """.trimIndent(), + exportName = "writesNamedProperty", + inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())), + ) + + val search = CurrentTsCallsCoverageEngine(testSourceEngine()).search( + request = coverageRequest(fixture, onCandidate = {}), + ) + + assertTrue(search.runtimeLimited, search.toString()) + assertTrue("ARRAY_NAMED_PROPERTY_WRITE" in search.runtimeLimitationReasons, search.toString()) + } + + @Test + fun `coverage replay compares the object before the source mutates it`() { + val fixture = fixture( + source = """ + export function increment(input: { score: number }): number { + input.score += 1; + return input.score; + } + """.trimIndent(), + exportName = "increment", + inputs = listOf(PropertyInput( + name = "input", + domain = ObjectDomain(mapOf("score" to NumberDomain())), + )), + ) + val inputs = listOf(JsConcreteValue.Object(mapOf("score" to JsConcreteValue.number(3.0)))) + + val replay = OriginalTypeScriptCoverageReplayer( + sourceRoot = fixture.sourceRoot, + function = fixture.function, + ).use { replayer -> replayer.replay(inputs = inputs, timeoutMillis = 20_000L) } + + assertEquals(CallsCoverageCompletion.RETURNED, replay.completion) + assertTrue(replay.coveredStatementKeys.isNotEmpty()) + } + private fun coverageRequest( fixture: CoverageFixture, onCandidate: (CallsCoverageCandidate) -> Unit, diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsObjectInputsTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsObjectInputsTest.kt new file mode 100644 index 0000000000..2b1c3db218 --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsObjectInputsTest.kt @@ -0,0 +1,402 @@ +package org.usvm.ts.calls + +import org.usvm.machine.call.TsUnknownCallEvent +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.ts.pbt.model.ArrayDomain +import org.usvm.ts.pbt.model.BooleanDomain +import org.usvm.ts.pbt.model.IntegerDomain +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.ObjectDomain +import org.usvm.ts.pbt.model.OptionalDomain +import org.usvm.ts.pbt.model.PropertyDomain +import org.usvm.ts.pbt.model.PropertyInput +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertNotNull +import kotlin.test.assertNull +import kotlin.test.assertTrue + +internal class CallsObjectInputsTest : CurrentTsCallsSymbolicEngineTestSupport() { + @Test + fun `plain object argument has symbolic fields and exact source replay`() { + val fixture = fixture( + source = """ + export interface Input { score: number; enabled: boolean } + + export function accepts(input: Input): boolean { + if (input.score > 5 && input.enabled) return true; + return false; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf(PropertyInput( + name = "input", + domain = ObjectDomain(mapOf( + "score" to NumberDomain(), + "enabled" to BooleanDomain, + )), + )), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + val inputs = assertNotNull(result.inputs, result.toString()) + val input = assertIs(inputs.single()) + + assertTrue(assertIs(input.fields.getValue("score")).toDouble() > 5) + assertEquals(JsConcreteValue.Boolean(true), input.fields.getValue("enabled")) + fixture.assertReplayConfirmed(inputs) + } + + @Test + fun `plain object keeps data fields of a class annotation without becoming that class`() { + val fixture = fixture( + source = """ + class C { + x: number = 0; + f(): number { return 7; } + } + + export function accepts(input: C): boolean { + if (input.x > 5) return true; + return false; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf(PropertyInput(name = "input", domain = ObjectDomain(mapOf("x" to NumberDomain())))), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + val inputs = assertNotNull(result.inputs, result.toString()) + + assertEquals(CallsSymbolicStatus.REACHED, result.status, result.toString()) + fixture.assertReplayConfirmed(inputs) + } + + @Test + fun `plain object does not borrow methods from its class annotation`() { + val fixture = fixture( + source = """ + class C { + x: number = 0; + f(): number { return 7; } + } + + export function accepts(input: C): boolean { + if (input.f() === 7) return true; + return false; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf(PropertyInput(name = "input", domain = ObjectDomain(mapOf("x" to NumberDomain())))), + targetStatement = "return true;", + ) + val unknownCalls = mutableListOf() + + val result = fixture.search(modelIds = emptySet(), unknownCallEventSink = unknownCalls::add) + + assertEquals(CallsSymbolicStatus.UNREACHED, result.status, result.toString()) + assertNull(result.inputs) + assertTrue(unknownCalls.any { it.failureReason == TsUnknownCallFailureReason.NO_SUITABLE_VIRTUAL_TARGET }) + } + + @Test + fun `plain object owns only its supplied fields despite the class annotation`() { + val fixture = fixture( + source = """ + class C { + x: number = 0; + missing: number = 7; + } + + export function accepts(input: C): boolean { + if ('x' in input && !('missing' in input) && input.missing === undefined) return true; + return false; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf(PropertyInput(name = "input", domain = ObjectDomain(mapOf("x" to NumberDomain())))), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + val inputs = assertNotNull(result.inputs, result.toString()) + + assertEquals(CallsSymbolicStatus.REACHED, result.status, result.toString()) + fixture.assertReplayConfirmed(inputs) + } + + @Test + fun `plain object is not an instance of its class annotation`() { + val fixture = fixture( + source = """ + class C { x: number = 0; } + + export function accepts(input: C): boolean { + if (!(input instanceof C)) return true; + return false; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf(PropertyInput(name = "input", domain = ObjectDomain(mapOf("x" to NumberDomain())))), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + val inputs = assertNotNull(result.inputs, result.toString()) + + assertEquals(CallsSymbolicStatus.REACHED, result.status, result.toString()) + fixture.assertReplayConfirmed(inputs) + } + + @Test + fun `plain object constructor lookup cannot invent the annotated constructor`() { + val fixture = fixture( + source = """ + class C { x: number = 0; } + + export function accepts(input: C): boolean { + if (input.constructor === C) return true; + return false; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf(PropertyInput(name = "input", domain = ObjectDomain(mapOf("x" to NumberDomain())))), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + val replay = OriginalTypeScriptTargetReplayer().replay( + sourceRoots = listOf(fixture.sourceRoot), + entryPoint = fixture.function.entryPoint, + inputs = listOf(JsConcreteValue.Object(mapOf("x" to JsConcreteValue.number(1.0)))), + target = fixture.target, + timeoutMillis = 10_000L, + ) + + // Current engine reports unsupported Object.prototype lookup through the search error boundary. + assertEquals(CallsSymbolicStatus.TOOL_ERROR, result.status, result.toString()) + assertTrue(result.diagnostic.orEmpty().contains("unsupported prototype lookup"), result.toString()) + assertNull(result.inputs) + assertEquals(CallsReplayStatus.REJECTED, replay.status, replay.toString()) + } + + @Test + fun `object field primitive storage mismatch is rejected before search`() { + assertUnsupportedObjectField(annotation = "boolean", domain = NumberDomain(), path = "input.value") + } + + @Test + fun `object field array element storage mismatch is rejected before search`() { + assertUnsupportedObjectField( + annotation = "boolean[]", + domain = ArrayDomain(element = NumberDomain(), minLength = 1, maxLength = 2), + path = "input.value[]", + ) + } + + @Test + fun `object domain cannot pretend to be an array field`() { + assertUnsupportedObjectField( + annotation = "number[]", + domain = ObjectDomain(mapOf("length" to NumberDomain())), + path = "input.value", + ) + } + + private fun assertUnsupportedObjectField(annotation: String, domain: PropertyDomain, path: String) { + val fixture = fixture( + source = """ + export function accepts(input: { value: $annotation }): boolean { + return true; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf(PropertyInput(name = "input", domain = ObjectDomain(mapOf("value" to domain)))), + targetStatement = "return true;", + ) + + val preflight = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.UNSUPPORTED, preflight.status, preflight.toString()) + assertEquals(CallsSymbolicPreflightReasonCode.INPUT_DOMAIN_UNSUPPORTED, preflight.reasonCode) + assertTrue(preflight.diagnostic.orEmpty().contains(path), preflight.toString()) + } + + @Test + fun `nested object and array fields have symbolic values and exact source replay`() { + val fixture = fixture( + source = """ + export function accepts(input: { details: { score: number }; scores: number[] }): boolean { + if (input.details.score > 5 && input.scores.length > 0 && input.scores[0] > 3) return true; + return false; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf( + PropertyInput( + name = "input", + domain = ObjectDomain( + fields = mapOf( + "details" to ObjectDomain(fields = mapOf("score" to NumberDomain())), + "scores" to ArrayDomain(element = NumberDomain(), minLength = 1, maxLength = 2), + ), + ), + ), + ), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + val inputs = assertNotNull(result.inputs, result.toString()) + val input = assertIs(inputs.single()) + val details = assertIs(input.fields.getValue("details")) + val scores = assertIs(input.fields.getValue("scores")) + + assertTrue(assertIs(details.fields.getValue("score")).toDouble() > 5) + assertTrue(assertIs(scores.elements.first()).toDouble() > 3) + fixture.assertReplayConfirmed(inputs) + } + + @Test + fun `nested object domain with non-object EtsIR field is rejected before search`() { + val fixture = fixture( + source = """ + export function accepts(input: { details: number }): boolean { + return true; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf( + PropertyInput( + name = "input", + domain = ObjectDomain( + fields = mapOf("details" to ObjectDomain(fields = mapOf("score" to NumberDomain()))), + ), + ), + ), + targetStatement = "return true;", + ) + + val preflight = fixture.preflight() + + assertEquals(CallsSymbolicPreflightStatus.UNSUPPORTED, preflight.status) + assertEquals(CallsSymbolicPreflightReasonCode.INPUT_DOMAIN_UNSUPPORTED, preflight.reasonCode) + assertTrue(preflight.diagnostic.orEmpty().contains("input.details"), preflight.toString()) + } + + @Test + fun `object argument can pass through constructor and stored callback`() { + val fixture = fixture( + source = """ + class Mapper { + private callback: (value: number) => number; + + constructor() { + this.callback = (value: number) => value + 1; + } + + map(value: number): number { + return this.callback(value); + } + } + + export function accepts(input: { score: number }): boolean { + const mapper = new Mapper(); + if (mapper.map(input.score) > 5) return true; + return false; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf(PropertyInput( + name = "input", + domain = ObjectDomain(mapOf("score" to NumberDomain())), + )), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + val inputs = assertNotNull(result.inputs, result.toString()) + val input = assertIs(inputs.single()) + + assertTrue(assertIs(input.fields.getValue("score")).toDouble() > 4) + fixture.assertReplayConfirmed(inputs) + } + + @Test + fun `object domain cannot pretend to be a function field`() { + assertUnsupportedObjectField( + annotation = "() => number", + domain = ObjectDomain(mapOf("score" to NumberDomain())), + path = "input.value", + ) + } + + @Test + fun `object inputs compose with recursive arrays and integer domains`() { + val fixture = fixture( + source = """ + export function accepts(input: { items: { score: number }[] }): boolean { + if (input.items[0].score === 7) return true; + return false; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf(PropertyInput( + name = "input", + domain = ObjectDomain(mapOf( + "items" to ArrayDomain( + element = ObjectDomain(mapOf("score" to IntegerDomain(min = 6, max = 8))), + minLength = 1, + maxLength = 1, + ), + )), + )), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + val inputs = assertNotNull(result.inputs, result.toString()) + + assertEquals(CallsSymbolicStatus.REACHED, result.status, result.toString()) + fixture.assertReplayConfirmed(inputs) + } + + @Test + fun `optional object fields preserve entry values after source mutation`() { + val fixture = fixture( + source = """ + export function accepts(input: { detail: { score: number } | null }): boolean { + if (input.detail === null) return false; + const score = input.detail.score; + input.detail.score = 0; + if (score === 7) return true; + return false; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf(PropertyInput( + name = "input", + domain = ObjectDomain(mapOf( + "detail" to OptionalDomain( + value = ObjectDomain(mapOf("score" to IntegerDomain(min = 6, max = 8))), + nil = JsConcreteValue.Null, + ), + )), + )), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + val inputs = assertNotNull(result.inputs, result.toString()) + val input = assertIs(inputs.single()) + val detail = assertIs(input.fields.getValue("detail")) + + assertEquals(CallsSymbolicStatus.REACHED, result.status, result.toString()) + assertEquals(JsConcreteValue.number(7.0), detail.fields.getValue("score")) + fixture.assertReplayConfirmed(inputs) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StoredFunctionCall.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StoredFunctionCall.kt index 077d0e844a..79b85885f3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StoredFunctionCall.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/lang/StoredFunctionCall.kt @@ -32,4 +32,15 @@ class StoredFunctionCall : TsMethodTestRunner() { invariants = arrayOf({ result -> result eq 5 }), ) } + + @Test + fun `test inherited callback field`() { + val method = getMethod("inheritedField") + + discoverProperties( + method = method, + { result -> result eq 7 }, + invariants = arrayOf({ result -> result eq 7 }), + ) + } } diff --git a/usvm-ts/src/test/resources/samples/lang/StoredFunctionCall.ts b/usvm-ts/src/test/resources/samples/lang/StoredFunctionCall.ts index b1ad133a1b..47d1dfb41c 100644 --- a/usvm-ts/src/test/resources/samples/lang/StoredFunctionCall.ts +++ b/usvm-ts/src/test/resources/samples/lang/StoredFunctionCall.ts @@ -17,6 +17,12 @@ class StoredFunctionCall { return subject.call(1); } + static inheritedField(): number { + const subject = new DerivedStoredFunctionCall(); + subject.callback = () => 7; + return subject.call(); + } + static regularFunction(): number { const subject = new StoredFunctionCall(); subject.callback = function (value: number): number { @@ -25,3 +31,18 @@ class StoredFunctionCall { return subject.call(1); } } + + +class BaseStoredFunctionCall { + callback: () => number; + + constructor() { + this.callback = () => 7; + } +} + +class DerivedStoredFunctionCall extends BaseStoredFunctionCall { + call(): number { + return this.callback(); + } +} From 9d637a746fba791fae5f99f74a58732110dab642 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 03:19:02 +0300 Subject: [PATCH 2/6] Include exact coverage diagnostics in replay regression --- .../kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt index 1ad61e3d10..853d6ddf49 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt @@ -198,7 +198,7 @@ class CallsCoverageExperimentTest { ).use { replayer -> replayer.replay(inputs = inputs, timeoutMillis = 20_000L) } assertEquals(CallsCoverageCompletion.RETURNED, replay.completion) - assertTrue(replay.coveredStatementKeys.isNotEmpty()) + assertTrue(replay.coveredStatementKeys.isNotEmpty(), replay.toString()) } @Test From 0c3d58748ecc1e68c11ebca7c079ad6d1ad279b5 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 04:49:16 +0300 Subject: [PATCH 3/6] Use shared shadow-aware metadata for Calls object fields --- .../ts/calls/CallsInputTypeCompatibility.kt | 8 ++----- .../usvm/ts/calls/CallsObjectInputsTest.kt | 24 +++++++++++++++++++ 2 files changed, 26 insertions(+), 6 deletions(-) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputTypeCompatibility.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputTypeCompatibility.kt index 490ff04e90..1b0a700b23 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputTypeCompatibility.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputTypeCompatibility.kt @@ -35,7 +35,7 @@ import org.usvm.ts.pbt.model.PropertyInput import org.usvm.ts.pbt.model.StringDomain import org.usvm.util.EtsHierarchy import org.usvm.util.componentType -import org.usvm.util.getAllFields +import org.usvm.util.declaredInstanceProperty /** Rejects bindings whose frozen domain would replace a source parameter with an incompatible runtime kind. */ internal fun callsInputTypePreflight( @@ -173,13 +173,9 @@ private fun PropertyDomain.objectFieldTypeLimitation( return "$path: frozen domain $this requires a compatible object domain for declared type $type" } - val declaredFields = hierarchy.classesForType(type).flatMap { clazz -> clazz.getAllFields(hierarchy) } for ((name, domain) in fields) { val fieldPath = "$path.$name" - val fieldType = declaredFields.filter { field -> field.name == name } - .distinctBy { field -> field.signature } - .singleOrNull() - ?.type + val fieldType = declaredInstanceProperty(type, name, hierarchy)?.type ?: return "$fieldPath: cannot resolve the declared field type in $type" val limitation = domain.inputTypeLimitation( type = fieldType, diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsObjectInputsTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsObjectInputsTest.kt index 2b1c3db218..9945bc5dec 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsObjectInputsTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsObjectInputsTest.kt @@ -76,6 +76,30 @@ internal class CallsObjectInputsTest : CurrentTsCallsSymbolicEngineTestSupport() fixture.assertReplayConfirmed(inputs) } + @Test + fun `plain object accepts a field redeclared by the nearest class`() { + val fixture = fixture( + source = """ + class Parent { x: number = 0; } + class Child extends Parent { x: number = 0; } + + export function accepts(input: Child): boolean { + if (input.x === 2) return true; + return false; + } + """.trimIndent(), + exportName = "accepts", + inputs = listOf(PropertyInput(name = "input", domain = ObjectDomain(mapOf("x" to NumberDomain())))), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + val inputs = assertNotNull(result.inputs, result.toString()) + + assertEquals(CallsSymbolicStatus.REACHED, result.status, result.toString()) + fixture.assertReplayConfirmed(inputs) + } + @Test fun `plain object does not borrow methods from its class annotation`() { val fixture = fixture( From f1913343e35954799aa8a40cd138dfb750fe9eb0 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 04:49:16 +0300 Subject: [PATCH 4/6] Use PBT-owned plain-object shapes in Calls inputs --- .../usvm/ts/calls/CallsInputMaterializer.kt | 61 ++-------------- .../org/usvm/ts/calls/CallsObjectShapes.kt | 72 ------------------- .../org/usvm/ts/calls/CallsSymbolicInputs.kt | 5 +- 3 files changed, 9 insertions(+), 129 deletions(-) delete mode 100644 usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsObjectShapes.kt diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt index 121953170c..03d4b20fe8 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputMaterializer.kt @@ -5,14 +5,6 @@ import io.ksmt.sort.KBv16Sort import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsArrayType -import org.jacodb.ets.model.EtsBooleanType -import org.jacodb.ets.model.EtsClassType -import org.jacodb.ets.model.EtsNullType -import org.jacodb.ets.model.EtsNumberType -import org.jacodb.ets.model.EtsStringType -import org.jacodb.ets.model.EtsType -import org.jacodb.ets.model.EtsUndefinedType -import org.jacodb.ets.model.EtsUnionType import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.api.initializeArrayLength @@ -34,6 +26,7 @@ import org.usvm.ts.pbt.model.ObjectDomain import org.usvm.ts.pbt.model.OptionalDomain import org.usvm.ts.pbt.model.PropertyDomain import org.usvm.ts.pbt.model.StringDomain +import org.usvm.ts.pbt.usvm.PlainObjectInputShapes import org.usvm.util.allocateBoundedString import org.usvm.util.componentType import org.usvm.util.mkArrayIndexLValue @@ -41,7 +34,7 @@ import org.usvm.util.mkFieldLValue internal fun TsState.materializeCallsInput( domain: PropertyDomain, - objectShapes: CallsObjectShapes, + objectShapes: PlainObjectInputShapes, ): MaterializedCallsInput = with(ctx) { when (domain) { BooleanDomain -> { @@ -85,7 +78,7 @@ internal fun TsState.materializeCallsInput( private fun TsState.materializeCallsObject( domain: ObjectDomain, - objectShapes: CallsObjectShapes, + objectShapes: PlainObjectInputShapes, ): MaterializedCallsInput = with(ctx) { val runtimeType = objectShapes.typeOf(domain) val reference = memory.allocConcrete(runtimeType) @@ -137,7 +130,7 @@ private fun TsState.materializeCallsConstant(value: JsConcreteValue): UExpr<*> = private fun TsState.materializeCallsOptional( domain: OptionalDomain, - objectShapes: CallsObjectShapes, + objectShapes: PlainObjectInputShapes, ): MaterializedCallsInput = with(ctx) { val nested = materializeCallsInput(domain = domain.value, objectShapes = objectShapes) val nil = materializeCallsConstant(domain.nil) @@ -164,54 +157,12 @@ private fun TsState.materializeCallsOptional( MaterializedCallsInput(value, OptionalInputSnapshot(chooseValue, nested.snapshot, domain.nil)) } -internal fun PropertyDomain.callsRuntimeType(objectType: (ObjectDomain) -> EtsClassType): EtsType = when (this) { - BooleanDomain -> { - EtsBooleanType - } - is IntegerDomain, is NumberDomain -> { - EtsNumberType - } - is StringDomain -> { - EtsStringType - } - is ArrayDomain -> { - val nestedType = element.callsRuntimeType(objectType) - if (nestedType is EtsArrayType) { - nestedType.copy(dimensions = nestedType.dimensions + 1) - } else { - EtsArrayType(elementType = nestedType, dimensions = 1) - } - } - is OptionalDomain -> { - val nestedType = value.callsRuntimeType(objectType) - val nilType = ConstantDomain(nil).callsRuntimeType(objectType) - EtsUnionType(types = listOf(nestedType, nilType)) - } - is ObjectDomain -> { - objectType(this) - } - is ConstantDomain -> { - when (value) { - is JsConcreteValue.Boolean -> EtsBooleanType - is JsConcreteValue.Number -> EtsNumberType - is JsConcreteValue.String -> EtsStringType - JsConcreteValue.Null -> EtsNullType - JsConcreteValue.Undefined -> EtsUndefinedType - is JsConcreteValue.Array, is JsConcreteValue.Object -> error( - "Structured constants are not primitive domains", - ) - } - } - else -> { - error("Unsupported array element domain: $this") - } -} private fun TsState.materializeCallsArray( domain: ArrayDomain, - objectShapes: CallsObjectShapes, + objectShapes: PlainObjectInputShapes, ): MaterializedCallsInput = with(ctx) { - val runtimeType = domain.callsRuntimeType(objectShapes::typeOf) as EtsArrayType + val runtimeType = objectShapes.runtimeTypeOf(domain) as EtsArrayType val descriptor = arrayDescriptorOf(runtimeType) val arrayRef = memory.allocConcrete(runtimeType) val length = initializeLength(minLength = domain.minLength, maxLength = domain.maxLength) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsObjectShapes.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsObjectShapes.kt deleted file mode 100644 index eacff7ac6d..0000000000 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsObjectShapes.kt +++ /dev/null @@ -1,72 +0,0 @@ -package org.usvm.ts.calls - -import org.jacodb.ets.model.EtsClass -import org.jacodb.ets.model.EtsClassCategory -import org.jacodb.ets.model.EtsClassImpl -import org.jacodb.ets.model.EtsClassSignature -import org.jacodb.ets.model.EtsClassType -import org.jacodb.ets.model.EtsFieldImpl -import org.jacodb.ets.model.EtsFieldSignature -import org.jacodb.ets.model.EtsFile -import org.jacodb.ets.model.EtsFileSignature -import org.jacodb.ets.model.EtsScene -import org.jacodb.ets.model.EtsType -import org.usvm.ts.pbt.model.ObjectDomain -import org.usvm.ts.pbt.model.PropertyDomain - -/** Runtime shapes of the own data properties emitted by the concrete input generator. */ -internal class CallsObjectShapes(sourceScene: EtsScene, domains: List) { - private val shapes = linkedMapOf() - private val classes = mutableListOf() - private val occupiedNames = sourceScene.projectAndSdkClasses.mapTo(mutableSetOf()) { it.name } - private val fileSignature: EtsFileSignature - val scene: EtsScene - - init { - val occupiedFiles = (sourceScene.projectFiles + sourceScene.sdkFiles).mapTo(mutableSetOf()) { it.signature } - sourceScene.projectAndSdkClasses.mapTo(occupiedFiles) { it.signature.file } - fileSignature = generateSequence(0) { it + 1 } - .map { index -> EtsFileSignature(projectName = "usvm-calls-inputs", fileName = "shapes-$index.ts") } - .first { it !in occupiedFiles } - domains.forEach(::register) - - scene = if (classes.isEmpty()) { - sourceScene - } else { - val file = EtsFile(signature = fileSignature, classes = classes, namespaces = emptyList()) - EtsScene( - projectFiles = sourceScene.projectFiles + file, - sdkFiles = sourceScene.sdkFiles, - projectName = sourceScene.projectName, - ) - } - } - - fun typeOf(domain: ObjectDomain): EtsClassType = shapes.getValue(domain) - - private fun register(domain: PropertyDomain): EtsType = domain.callsRuntimeType(::registerObject) - - private fun registerObject(domain: ObjectDomain): EtsClassType { - shapes[domain]?.let { return it } - - val name = generateSequence(shapes.size) { it + 1 } - .map { index -> "__usvm_calls_input_$index" } - .first { it !in occupiedNames } - occupiedNames += name - val signature = EtsClassSignature(name = name, file = fileSignature) - val type = EtsClassType(signature) - shapes[domain] = type - val fields = domain.fields.map { (fieldName, fieldDomain) -> - EtsFieldImpl(EtsFieldSignature(enclosingClass = signature, name = fieldName, type = register(fieldDomain))) - } - - // A source annotation supplies field layout, never methods or nominal ancestry. - classes += EtsClassImpl( - signature = signature, - fields = fields, - methods = emptyList(), - category = EtsClassCategory.OBJECT, - ) - return type - } -} diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt index f53970bcd8..a4f314ff79 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsSymbolicInputs.kt @@ -17,6 +17,7 @@ import org.usvm.ts.pbt.model.OptionalDomain import org.usvm.ts.pbt.model.PropertyDomain import org.usvm.ts.pbt.model.PropertyInput import org.usvm.ts.pbt.model.StringDomain +import org.usvm.ts.pbt.usvm.PlainObjectInputShapes import org.usvm.util.mkRegisterStackLValue internal fun PropertyDomain.isSupportedCallsSymbolicDomain(): Boolean = when (this) { @@ -52,7 +53,7 @@ internal class CallsSymbolicInputs( private val captures: List, sourceScene: EtsScene, ) { - private val objectShapes = CallsObjectShapes(sourceScene, inputs.map(PropertyInput::domain)) + private val objectShapes = PlainObjectInputShapes(sourceScene, inputs.map(PropertyInput::domain)) val scene: EtsScene = objectShapes.scene private val boundInputs: List> @@ -95,7 +96,7 @@ internal class CallsSymbolicInputs( private fun TsState.initializeInput( stackSlot: Int, domain: PropertyDomain, - objectShapes: CallsObjectShapes, + objectShapes: PlainObjectInputShapes, ): CallsInputSnapshot = with(ctx) { val input = materializeCallsInput(domain = domain, objectShapes = objectShapes) when (input.value.sort) { From 85e87f7715d2dab14b5250233dda5ff1489e358d Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 00:21:02 +0300 Subject: [PATCH 5/6] Verify Calls object support after the PBT boundary integration --- .../ts/calls/CurrentTsCallsInputDomainsTest.kt | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsInputDomainsTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsInputDomainsTest.kt index 97d0e87356..3346b2ce18 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsInputDomainsTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsInputDomainsTest.kt @@ -16,11 +16,13 @@ import kotlin.test.assertTrue internal class CurrentTsCallsInputDomainsTest : CurrentTsCallsSymbolicEngineTestSupport() { @Test - fun `object input domains are rejected before symbolic materialization`() { + fun `object input domains produce field witnesses after symbolic materialization`() { val fixture = fixture( source = """ - export function objectInput(value: any): boolean { - if (typeof value === "object") { + export interface ObjectInput { count: number } + + export function objectInput(value: ObjectInput): boolean { + if (value.count === 1) { return true; } return false; @@ -39,9 +41,13 @@ internal class CurrentTsCallsInputDomainsTest : CurrentTsCallsSymbolicEngineTest val preflight = fixture.preflight() val result = fixture.search(modelIds = emptySet()) - assertEquals(CallsSymbolicPreflightStatus.UNSUPPORTED, preflight.status, preflight.toString()) - assertEquals(CallsSymbolicPreflightReasonCode.INPUT_DOMAIN_UNSUPPORTED, preflight.reasonCode) - assertEquals(CallsSymbolicStatus.UNSUPPORTED, result.status, result.toString()) + assertEquals(CallsSymbolicPreflightStatus.ELIGIBLE, preflight.status, preflight.toString()) + assertEquals(CallsSymbolicStatus.REACHED, result.status, result.toString()) + + val inputs = assertNotNull(result.inputs, result.toString()) + val value = assertIs(inputs.single()) + assertEquals(JsConcreteValue.number(1.0), value.fields.getValue("count")) + fixture.assertReplayConfirmed(inputs) } @Test From 32eadcb7125540be57d7312c11a26bef8630960e Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Wed, 14 Oct 2026 01:33:23 +0300 Subject: [PATCH 6/6] Fix Detekt formatting in Calls object input changes Wrap union compatibility arguments and multiline object input fixtures. Sort imports and fix the remaining fixture wrapping in the affected coverage test. Detekt main/test reports contain no findings in the three changed files. Calls source and test compilation and git diff --check passed. --- .../ts/calls/CallsInputTypeCompatibility.kt | 10 ++- .../ts/calls/CallsCoverageExperimentTest.kt | 10 +-- .../usvm/ts/calls/CallsObjectInputsTest.kt | 70 +++++++++++-------- 3 files changed, 57 insertions(+), 33 deletions(-) diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputTypeCompatibility.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputTypeCompatibility.kt index 1b0a700b23..efb979aea2 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputTypeCompatibility.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CallsInputTypeCompatibility.kt @@ -145,7 +145,15 @@ private fun PropertyDomain.inputTypeLimitation( ) } is EtsUnionType -> { - type.types.any { member -> inputTypeLimitation(member, genericParameters, path, hierarchy, visitedGenerics) == null } + type.types.any { member -> + inputTypeLimitation( + type = member, + genericParameters = genericParameters, + path = path, + hierarchy = hierarchy, + visitedGenerics = visitedGenerics, + ) == null + } } is EtsIntersectionType -> { for (member in type.types) { diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt index 853d6ddf49..426a85e9ba 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsCoverageExperimentTest.kt @@ -252,10 +252,12 @@ class CallsCoverageExperimentTest { } """.trimIndent(), exportName = "increment", - inputs = listOf(PropertyInput( - name = "input", - domain = ObjectDomain(mapOf("score" to NumberDomain())), - )), + inputs = listOf( + PropertyInput( + name = "input", + domain = ObjectDomain(mapOf("score" to NumberDomain())), + ), + ), ) val inputs = listOf(JsConcreteValue.Object(mapOf("score" to JsConcreteValue.number(3.0)))) diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsObjectInputsTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsObjectInputsTest.kt index 9945bc5dec..077e66ee0d 100644 --- a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsObjectInputsTest.kt +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CallsObjectInputsTest.kt @@ -31,13 +31,17 @@ internal class CallsObjectInputsTest : CurrentTsCallsSymbolicEngineTestSupport() } """.trimIndent(), exportName = "accepts", - inputs = listOf(PropertyInput( - name = "input", - domain = ObjectDomain(mapOf( - "score" to NumberDomain(), - "enabled" to BooleanDomain, - )), - )), + inputs = listOf( + PropertyInput( + name = "input", + domain = ObjectDomain( + mapOf( + "score" to NumberDomain(), + "enabled" to BooleanDomain, + ), + ), + ), + ), targetStatement = "return true;", ) @@ -335,10 +339,12 @@ internal class CallsObjectInputsTest : CurrentTsCallsSymbolicEngineTestSupport() } """.trimIndent(), exportName = "accepts", - inputs = listOf(PropertyInput( - name = "input", - domain = ObjectDomain(mapOf("score" to NumberDomain())), - )), + inputs = listOf( + PropertyInput( + name = "input", + domain = ObjectDomain(mapOf("score" to NumberDomain())), + ), + ), targetStatement = "return true;", ) @@ -369,16 +375,20 @@ internal class CallsObjectInputsTest : CurrentTsCallsSymbolicEngineTestSupport() } """.trimIndent(), exportName = "accepts", - inputs = listOf(PropertyInput( - name = "input", - domain = ObjectDomain(mapOf( - "items" to ArrayDomain( - element = ObjectDomain(mapOf("score" to IntegerDomain(min = 6, max = 8))), - minLength = 1, - maxLength = 1, + inputs = listOf( + PropertyInput( + name = "input", + domain = ObjectDomain( + mapOf( + "items" to ArrayDomain( + element = ObjectDomain(mapOf("score" to IntegerDomain(min = 6, max = 8))), + minLength = 1, + maxLength = 1, + ), + ), ), - )), - )), + ), + ), targetStatement = "return true;", ) @@ -402,15 +412,19 @@ internal class CallsObjectInputsTest : CurrentTsCallsSymbolicEngineTestSupport() } """.trimIndent(), exportName = "accepts", - inputs = listOf(PropertyInput( - name = "input", - domain = ObjectDomain(mapOf( - "detail" to OptionalDomain( - value = ObjectDomain(mapOf("score" to IntegerDomain(min = 6, max = 8))), - nil = JsConcreteValue.Null, + inputs = listOf( + PropertyInput( + name = "input", + domain = ObjectDomain( + mapOf( + "detail" to OptionalDomain( + value = ObjectDomain(mapOf("score" to IntegerDomain(min = 6, max = 8))), + nil = JsConcreteValue.Null, + ), + ), ), - )), - )), + ), + ), targetStatement = "return true;", )