diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index 0bfe3bfa03..316b213b70 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -121,7 +121,9 @@ class TsMachine( ) } ?: scene - private val runtimeScene = analysisScene.withCoreRuntimeSdk() + private val runtimeScene = analysisScene.withCoreRuntimeSdk().let { runtime -> + if (tsOptions.maxInputCollectionSize == null) runtime else runtime.withInputCollectionSdk() + } private val applicationAndSdkClasses = scene.projectClasses + runtimeScene.sdkClasses private val graph = TsGraph(runtimeScene) private val typeSystem = TsTypeSystem( diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt index 6334667b8e..b98bbbadfa 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -3,6 +3,7 @@ package org.usvm.machine import org.jacodb.ets.model.EtsClassSignature import org.usvm.machine.call.TsResidualCallPolicy import org.usvm.machine.call.TsUnknownCallModelSelection +import org.usvm.machine.expr.MAX_MODELED_COLLECTION_ENTRIES /** Initial own-property assumptions for symbolic input objects; writes and deletes always take precedence. */ enum class TsInputPropertyPresence { @@ -23,6 +24,8 @@ data class TsOptions( val interproceduralAnalysis: Boolean = true, val enableVisualization: Boolean = false, val maxArraySize: Int = 1_000, + /** Bounded native Map/Set input domain; null retains unsupported symbolic collection inputs. */ + val maxInputCollectionSize: Int? = null, val inputPropertyPresence: TsInputPropertyPresence = TsInputPropertyPresence.DECLARED_FIELDS, val unknownCallModelSelection: TsUnknownCallModelSelection = TsUnknownCallModelSelection.All, val unknownCallFallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH, @@ -34,6 +37,10 @@ data class TsOptions( val classCoverageTargets: Set? = null, ) { init { + require(maxInputCollectionSize == null || maxInputCollectionSize in 1..MAX_MODELED_COLLECTION_ENTRIES) { + "Input collection capacity must be between 1 and 16, or disabled" + } + val hasCoverageTargets = classCoverageTargets == null || classCoverageTargets.isNotEmpty() require(hasCoverageTargets) { "Explicit class coverage targets must not be empty" } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt index 01cf76b348..a3754ecb61 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt @@ -3,6 +3,8 @@ package org.usvm.machine import org.jacodb.ets.dto.EtsFileDto import org.jacodb.ets.dto.toEtsFile import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassImpl +import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsLocal @@ -78,3 +80,20 @@ internal fun EtsScene.runtimeFunctionType(): EtsClassType { ?: throw UnsupportedOperationException("SDK Function identity is ambiguous or unavailable") return EtsClassType(functionClass.signature) } + +/** Native collection input types need real identities in the solver's finite runtime-type universe. */ +internal fun EtsScene.withInputCollectionSdk(): EtsScene { + val names = setOf("Map", "Set") - projectAndSdkClasses.map { it.name }.toSet() + if (names.isEmpty()) return this + + val classes = names.map { name -> + EtsClassImpl( + signature = EtsClassSignature.UNKNOWN.copy(name = name), + fields = emptyList(), + methods = emptyList(), + superClass = EtsHierarchy.OBJECT_CLASS.signature, + ) + } + val file = EtsFile(signature = EtsClassSignature.UNKNOWN.file, classes = classes, namespaces = emptyList()) + return EtsScene(projectFiles = projectFiles, sdkFiles = sdkFiles + file, projectName = projectName) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsCollectionModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsCollectionModelFamily.kt index aaa80f1fcd..c74bfe6388 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsCollectionModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsCollectionModelFamily.kt @@ -8,6 +8,7 @@ import org.usvm.machine.call.TsUnknownCallModelCompletion import org.usvm.machine.call.TsUnknownCallModelExecution import org.usvm.machine.call.TsUnknownCallModelSuccessor import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.expr.MAX_MODELED_COLLECTION_ENTRIES import org.usvm.machine.expr.TsCollectionKind import org.usvm.machine.expr.collectionClear import org.usvm.machine.expr.collectionGet @@ -22,7 +23,6 @@ import org.usvm.machine.types.iteUnresolvedValue /** A bounded coherent subset of native Map/Set operations. */ internal object TsCollectionModelFamily : TsBuiltInUnknownCallModelFamily { - private const val MAX_ENTRIES = 16 override val models: List = listOf( OperationModel(operation = "get"), @@ -40,6 +40,7 @@ internal object TsCollectionModelFamily : TsBuiltInUnknownCallModelFamily { override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? = with(state.ctx) { val receiver = call.receiver?.resolved as? UConcreteHeapRef ?: return null val collection = state.modeledCollections[receiver] ?: return null + val originalReceiver = state.collectionOriginalReceivers[receiver] ?: receiver val mapOnly = operation == "get" || operation == "set" if (mapOnly && collection.kind != TsCollectionKind.MAP) return null if (operation == "add" && collection.kind != TsCollectionKind.SET) return null @@ -97,17 +98,17 @@ internal object TsCollectionModelFamily : TsBuiltInUnknownCallModelFamily { val successors = matches.map { match -> TsUnknownCallModelSuccessor( guard = match.guard, - completion = TsUnknownCallModelCompletion.Normal { receiver }, + completion = TsUnknownCallModelCompletion.Normal { originalReceiver }, applyStateChanges = { if (collection.kind == TsCollectionKind.MAP) collectionPut(collection, match.key, value) }, ) }.toMutableList() - val canInsert = collection.keys.size < MAX_ENTRIES + val canInsert = collection.keys.size < MAX_MODELED_COLLECTION_ENTRIES if (canInsert) { successors += TsUnknownCallModelSuccessor( guard = missing, - completion = TsUnknownCallModelCompletion.Normal { receiver }, + completion = TsUnknownCallModelCompletion.Normal { originalReceiver }, applyStateChanges = { collectionInsert(receiver, collection, key, value) }, ) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 15fab96a6e..1146a63674 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -154,6 +154,9 @@ internal fun TsExprResolver.tryApproximateInstanceCall( val instance = stmt.instance if (!ensureSupportedObjectMutation(stmt)) return TsExprApproximationResult.ResolveFailure + val inputCollection = tryApproximateInputCollectionCall(stmt) + if (inputCollection !is TsExprApproximationResult.NoApproximation) return inputCollection + val regularExpression = tryApproximateRegExpCall(stmt) if (regularExpression !is TsExprApproximationResult.NoApproximation) return regularExpression 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 3f46417f9a..9e6e34a04f 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 @@ -116,6 +116,21 @@ internal fun TsExprResolver.handleInstanceFieldRef( } } + if (value.field.name == "size") { + when (val inputCollection = inputCollectionReference(instance, instanceLocal.type)) { + is TsIntrinsicFieldResult.Handled -> { + val collection = scope.calcOnState { modeledCollections[inputCollection.value] } + if (collection == null) { + scope.doWithState { terminateAsUnsupported(reason = "Input collection backend was invalidated") } + return null + } + return scope.calcOnState { collectionSize(collection) } + } + TsIntrinsicFieldResult.Stopped -> return null + TsIntrinsicFieldResult.NotApplicable -> {} + } + } + // Read the field. return resolveField(scope, instanceLocal, instance, value.field, hierarchy) } @@ -334,9 +349,29 @@ private fun TsContext.initialReferenceConstraint( hierarchy: EtsHierarchy, ): UBoolExpr = when (type) { is EtsClassType -> scope.calcOnState { - val auxiliary = type.toAuxiliaryType(hierarchy) - val classConstraint = auxiliary?.let { memory.types.evalIsSubtype(ref, it) } ?: trueExpr - mkAnd(mkNotNullOrUndefined(ref), classConstraint) + val nativeCollection = type.nativeCollectionKind() != null && + hierarchy.classesForType(type).any { it.signature.file == EtsClassSignature.UNKNOWN.file } + if (nativeCollection) { + inputCollectionTypes += ref to type + val nativeType = memory.types.evalTypeEquals(ref, type) + mkAnd(mkNotNullOrUndefined(ref), nativeType) + } else { + val auxiliary = type.toAuxiliaryType(hierarchy) + val classConstraint = auxiliary?.let { memory.types.evalIsSubtype(ref, it) } ?: trueExpr + mkAnd(mkNotNullOrUndefined(ref), classConstraint) + } + } + is EtsUnclearRefType -> { + val nativeCollection = type.name in setOf("Map", "Set") && + hierarchy.classesForType(type).any { it.signature.file == EtsClassSignature.UNKNOWN.file } + if (nativeCollection) { + scope.doWithState { inputCollectionTypes += ref to type } + val nativeType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = type.name)) + val runtimeType = scope.calcOnState { memory.types.evalTypeEquals(ref, nativeType) } + mkAnd(mkNotNullOrUndefined(ref), runtimeType) + } else { + trueExpr + } } is EtsNullType -> mkHeapRefEq(ref, mkTsNullValue()) is EtsUndefinedType -> mkHeapRefEq(ref, mkUndefinedValue()) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCollectionStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCollectionStorage.kt index 11124cf31b..39498c3b2d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCollectionStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCollectionStorage.kt @@ -18,6 +18,8 @@ import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapRemove import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapSize import org.usvm.api.evalTypeEquals import org.usvm.collection.field.UFieldLValue +import org.usvm.collection.map.length.UMapLengthLValue +import org.usvm.collection.set.ref.URefSetEntryLValue import org.usvm.isFalse import org.usvm.isTrue import org.usvm.machine.call.TsUnknownCall @@ -25,10 +27,13 @@ import org.usvm.machine.state.TsState import org.usvm.machine.types.EtsFakeType import org.usvm.machine.types.TsUnresolvedValue import org.usvm.machine.types.extractValue +import org.usvm.sizeSort import org.usvm.util.mkStringBackingElementLValue import org.usvm.util.mkStringBackingLValue import org.usvm.util.mkStringBackingLengthLValue +internal const val MAX_MODELED_COLLECTION_ENTRIES = 16 + internal enum class TsCollectionKind { MAP, SET } /** Native object identity and symbolic backend are shared by all aliases and cloned with the state. */ @@ -130,6 +135,20 @@ internal fun TsState.collectionClear(receiver: UConcreteHeapRef, collection: TsM modeledCollections += receiver to collection.copy(keys = emptyList()) } +/** Initial bounded slots have symbolic presence; cardinality changes under the identical guard. */ +internal fun TsState.guardInitialCollectionEntry( + collection: TsModeledCollection, + key: UConcreteHeapRef, + present: UBoolExpr, +) = with(ctx) { + val membership = URefSetEntryLValue(collection.storage, key, storageType) + val length = UMapLengthLValue(collection.storage, storageType, sizeSort) + val currentSize = memory.read(length) + val absent = mkNot(present) + memory.write(membership, falseExpr, guard = absent) + memory.write(length, mkBvSubExpr(currentSize, mkBv(1)), guard = absent) +} + internal fun TsState.collectionPresent(collection: TsModeledCollection, key: UConcreteHeapRef): UBoolExpr = symbolicObjectMapContains(collection.storage, key, storageType) @@ -176,7 +195,7 @@ internal fun TsState.readCollectionPayload(ref: UHeapRef): TsUnresolvedValue = w TsUnresolvedValue(boolValue = boolean, fpValue = number, refValue = reference, type = type) } -private fun TsState.collectionKeyEquals(left: TsUnresolvedValue, right: TsUnresolvedValue): UBoolExpr? = with(ctx) { +internal fun TsState.collectionKeyEquals(left: TsUnresolvedValue, right: TsUnresolvedValue): UBoolExpr? = with(ctx) { val booleanEqual = mkAnd(left.type.boolTypeExpr, right.type.boolTypeExpr, mkEq(left.boolValue, right.boolValue)) val leftIsNaN = mkFpIsNaNExpr(left.fpValue) val rightIsNaN = mkFpIsNaNExpr(right.fpValue) @@ -226,7 +245,12 @@ private fun TsState.referenceOrStringKeyEquals(left: UHeapRef, right: UHeapRef): private fun TsState.modeledStringBound(ref: UHeapRef): Int? = with(ctx) { boundedStringBackingRefs[ref]?.let { return it } - if (ref is UConcreteHeapRef) return getStringConstantValue(ref)?.length + if (ref is UConcreteHeapRef) { + val constant = getStringConstantValue(ref) + if (constant != null) return constant.length + if (memory.types.evalTypeEquals(ref, EtsStringType).isFalse) return 0 + return null + } if (ref !is UIteExpr<*>) return null val trueBound = modeledStringBound(ref.trueBranch.asExpr(addressSort)) ?: return null val falseBound = modeledStringBound(ref.falseBranch.asExpr(addressSort)) ?: return null diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index d6cacc0ea5..0a79b373bd 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 @@ -530,6 +530,13 @@ class TsExprResolver( checkUndefinedOrNullPropertyRead(scope, rawInstance, operand.field.name) ?: return null val instance = resolveHeapRef(scope, rawInstance) ?: return null + val supportedMutation = ensureSupportedInputCollectionMutation( + reference = instance, + declaredType = operand.instance.type, + property = operand.field.name, + ) + if (!supportedMutation) return null + val nativeMathConstant = scope.calcOnState { isNativeMathConstant(instance, operand.field.name) } if (nativeMathConstant) { scope.doWithState { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsInputCollections.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsInputCollections.kt new file mode 100644 index 0000000000..763ea758c4 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsInputCollections.kt @@ -0,0 +1,220 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsBooleanType +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnclearRefType +import org.jacodb.ets.model.EtsWellKnownSymbol +import org.usvm.UConcreteHeapRef +import org.usvm.UHeapRef +import org.usvm.USymbolicHeapRef +import org.usvm.api.evalTypeEquals +import org.usvm.api.makeSymbolicPrimitive +import org.usvm.api.makeSymbolicRefUntyped +import org.usvm.api.typeStreamOf +import org.usvm.isTrue +import org.usvm.machine.TsVirtualMethodCallStmt +import org.usvm.machine.call.TsBuiltInUnknownCallModels +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModelDispatcher +import org.usvm.machine.call.dispatch +import org.usvm.machine.state.TsState +import org.usvm.machine.state.symbolicStringBackingConstraint +import org.usvm.machine.types.EtsFakeType +import org.usvm.machine.types.TsUnresolvedValue +import org.usvm.sizeSort +import org.usvm.types.singleOrNull + +internal fun EtsType.nativeCollectionKind(): TsCollectionKind? { + val name = when (this) { + is EtsClassType -> { + if (signature.file != EtsClassSignature.UNKNOWN.file) return null + signature.name + } + is EtsUnclearRefType -> name + else -> return null + } + return when (name) { + "Map" -> TsCollectionKind.MAP + "Set" -> TsCollectionKind.SET + else -> null + } +} + +/** + * Finite input domain, including every cardinality from zero to the configured capacity. + * Symbolic receivers are partitioned by heap equality before a state-owned native backend is selected. + * The allocated handle is private: set/add return the original receiver and object identity is unchanged. + */ +internal fun TsExprResolver.inputCollectionReference( + reference: UHeapRef, + declaredType: EtsType, +): TsIntrinsicFieldResult = with(ctx) { + val capacity = options.maxInputCollectionSize ?: return TsIntrinsicFieldResult.NotApplicable + if (unknownCallDispatcher !is TsUnknownCallModelDispatcher) return TsIntrinsicFieldResult.NotApplicable + val selected = TsBuiltInUnknownCallModels.catalog(options.unknownCallModelSelection).modelIds + if ("ts.collection.has" !in selected) return TsIntrinsicFieldResult.NotApplicable + if (reference !is USymbolicHeapRef) return TsIntrinsicFieldResult.NotApplicable + + val sourceType = if (declaredType.nativeCollectionKind() != null) { + declaredType + } else { + scope.calcOnState { inputCollectionTypes[reference] ?: memory.typeStreamOf(reference).singleOrNull() } + ?: return TsIntrinsicFieldResult.NotApplicable + } + val elementTypes = when (sourceType) { + is EtsClassType -> sourceType.typeParameters + is EtsUnclearRefType -> sourceType.typeParameters + else -> emptyList() + } + val kind = sourceType.nativeCollectionKind() ?: return TsIntrinsicFieldResult.NotApplicable + val nativeName = if (kind == TsCollectionKind.MAP) "Map" else "Set" + // A project class named Map/Set must keep ordinary method/field semantics. + val shadowed = scene.projectClasses.any { it.name == nativeName } + if (shadowed) return TsIntrinsicFieldResult.NotApplicable + + val nativeType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = nativeName)) + val nativeConstraint = scope.calcOnState { memory.types.evalTypeEquals(reference, nativeType) } + scope.assert(nativeConstraint) ?: return TsIntrinsicFieldResult.Stopped + + val known = scope.calcOnState { inputCollectionReferences.toList() } + for ((original, handle) in known) { + val equal = mkHeapRefEq(original, reference) + val aliases = scope.calcOnState { models.first().eval(equal).isTrue } + val condition = if (aliases) equal else mkNot(equal) + scope.fork(condition) ?: return TsIntrinsicFieldResult.Stopped + if (aliases) return TsIntrinsicFieldResult.Handled(handle) + } + + val handle = scope.calcOnState { + val handle = memory.allocConcrete(nativeType) + val collection = newModeledCollection(kind) + modeledCollections += handle to collection + inputCollectionReferences += reference to handle + collectionOriginalReceivers += handle to reference + initializeInputCollection(handle, capacity, elementTypes) + handle + } + // Refresh models after introducing cardinality, payload-kind and distinct-key constraints. + scope.assert(trueExpr) ?: return TsIntrinsicFieldResult.Stopped + TsIntrinsicFieldResult.Handled(handle) +} + +internal fun TsExprResolver.tryApproximateInputCollectionCall( + stmt: TsVirtualMethodCallStmt, +): TsExprApproximationResult = with(ctx) { + if (stmt.instance.sort != addressSort) return TsExprApproximationResult.NoApproximation + val collection = inputCollectionReference(stmt.instance.asExpr(addressSort), stmt.call.instance.type) + val handle = when (collection) { + is TsIntrinsicFieldResult.Handled -> collection.value + TsIntrinsicFieldResult.Stopped -> return TsExprApproximationResult.ResolveFailure + TsIntrinsicFieldResult.NotApplicable -> return TsExprApproximationResult.NoApproximation + } + val normalized = TsVirtualMethodCallStmt( + call = stmt.call, + instance = handle, + args = stmt.args, + returnSite = stmt.returnSite, + originalCall = stmt.originalCall, + targetCaptured = stmt.targetCaptured, + ) + if (stmt.call.wellKnownSymbol == EtsWellKnownSymbol.ITERATOR) { + return tryApproximateCollectionIteratorCall(normalized) + } + + unknownCallDispatcher.dispatch( + scope = scope, + call = normalized, + failureReason = TsUnknownCallFailureReason.VIRTUAL_METHOD_NOT_FOUND, + resolvedReceiver = handle, + ) + TsExprApproximationResult.ResolveFailure +} + +/** Keep readonly native size outside ordinary property storage for symbolic receivers too. */ +internal fun TsExprResolver.ensureSupportedInputCollectionMutation( + reference: UHeapRef, + declaredType: EtsType, + property: String, +): Boolean { + if (property != "size") return true + return when (inputCollectionReference(reference, declaredType)) { + is TsIntrinsicFieldResult.Handled -> { + scope.doWithState { terminateAsUnsupported(reason = "Mutating native collection size is not modeled") } + false + } + TsIntrinsicFieldResult.Stopped -> false + TsIntrinsicFieldResult.NotApplicable -> true + } +} + +private fun TsState.initializeInputCollection( + handle: UConcreteHeapRef, + capacity: Int, + elementTypes: List, +) = with(ctx) { + val count = makeSymbolicPrimitive(sizeSort) + pathConstraints += mkBvSignedGreaterOrEqualExpr(count, mkBv(0)) + pathConstraints += mkBvSignedLessOrEqualExpr(count, mkBv(capacity)) + val previousKeys = mutableListOf() + for (index in 0 until capacity) { + val present = mkBvSignedLessExpr(mkBv(index), count) + val key = newInputCollectionValue(elementTypes.getOrNull(0)) + val collection = modeledCollections.getValue(handle) + for (previous in previousKeys) { + val equal = requireNotNull(collectionKeyEquals(previous, key)) + pathConstraints += mkImplies(present, mkNot(equal)) + } + val value = if (collection.kind == TsCollectionKind.SET) { + key + } else { + newInputCollectionValue(elementTypes.getOrNull(1)) + } + collectionInsert(handle, collection, key, value) + val updated = modeledCollections.getValue(handle) + val identity = updated.keys.last() + // Build a dense symbolic prefix in insertion order; backend size stays coherent with membership. + guardInitialCollectionEntry(updated, identity, present) + previousKeys += key + } +} + +private fun TsState.newInputCollectionValue(declaredType: EtsType?): TsUnresolvedValue = with(ctx) { + if (declaredType == EtsNumberType) return collectionValue(makeSymbolicPrimitive(fp64Sort)) + if (declaredType == EtsBooleanType) return collectionValue(makeSymbolicPrimitive(boolSort)) + + val type = EtsFakeType( + boolTypeExpr = makeSymbolicPrimitive(boolSort), + fpTypeExpr = makeSymbolicPrimitive(boolSort), + refTypeExpr = makeSymbolicPrimitive(boolSort), + ) + pathConstraints += type.mkExactlyOneTypeConstraint(ctx) + val kindConstraint = when (declaredType) { + EtsBooleanType -> type.boolTypeExpr + EtsNumberType -> type.fpTypeExpr + EtsStringType, is EtsClassType, is EtsUnclearRefType -> type.refTypeExpr + else -> trueExpr + } + pathConstraints += kindConstraint + val reference = makeSymbolicRefUntyped() + if (declaredType == EtsStringType) { + pathConstraints += mkNotNullOrUndefined(reference) + pathConstraints += memory.types.evalTypeEquals(reference, EtsStringType) + } + val isString = memory.types.evalTypeEquals(reference, EtsStringType) + val isDefined = mkNotNullOrUndefined(reference) + val string = mkAnd(type.refTypeExpr, isString, isDefined) + pathConstraints += mkImplies(string, symbolicStringBackingConstraint(reference)) + boundedStringBackingRefs += reference to maxStringLength + + TsUnresolvedValue( + boolValue = makeSymbolicPrimitive(boolSort), + fpValue = makeSymbolicPrimitive(fp64Sort), + refValue = reference, + type = type, + ) +} 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 947b391258..780c72de54 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 @@ -114,6 +114,9 @@ internal fun TsExprResolver.handleAssignToInstanceField( if (!ensureSupportedArrayPrototypeAccess(instance, field.name)) return null ensureSupportedDatePrototypeAccess(instance, field.name) + val supportedMutation = ensureSupportedInputCollectionMutation(instance, instanceLocal.type, field.name) + if (!supportedMutation) return null + val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } if (storageType == EtsStringType) { return handleStringPropertyWrite() diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInitialState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInitialState.kt index 6c965334e0..0bdcad0091 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInitialState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInitialState.kt @@ -3,6 +3,8 @@ package org.usvm.machine.interpreter import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsGenericType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNullType @@ -12,14 +14,17 @@ import org.jacodb.ets.model.EtsTupleType import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType +import org.usvm.UHeapRef import org.usvm.api.evalTypeEquals import org.usvm.api.targets.TsTarget import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.machine.TsContext import org.usvm.machine.TsGraph import org.usvm.machine.TsOptions +import org.usvm.machine.expr.TsCollectionKind import org.usvm.machine.expr.TsUnresolvedSort import org.usvm.machine.expr.mkNotNullOrUndefined +import org.usvm.machine.expr.nativeCollectionKind import org.usvm.machine.state.TsState import org.usvm.machine.state.localsCount import org.usvm.machine.state.newStmt @@ -83,6 +88,11 @@ internal fun createInitialStateOrNull( } val parameterType = param.type.initialInputType(genericParameters) + val nativeCollectionInput = options.maxInputCollectionSize != null && + parameterType.nativeCollectionKind() != null + if (nativeCollectionInput) { + state.constrainNativeCollectionInput(ref, parameterType, graph) + } if (parameterType is EtsRefType) { run { state.pathConstraints += mkNotNullOrUndefined(ref) @@ -159,6 +169,18 @@ internal fun createInitialStateOrNull( state } +private fun TsState.constrainNativeCollectionInput(reference: UHeapRef, parameterType: EtsType, graph: TsGraph) { + val kind = parameterType.nativeCollectionKind() ?: return + val declaredClasses = if (parameterType is EtsRefType) graph.hierarchy.classesForType(parameterType) else emptySet() + val hasProjectDeclaration = declaredClasses.any { it.signature.file != EtsClassSignature.UNKNOWN.file } + if (hasProjectDeclaration) return + + val nativeName = if (kind == TsCollectionKind.MAP) "Map" else "Set" + val nativeType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = nativeName)) + pathConstraints += memory.types.evalTypeEquals(reference, nativeType) + inputCollectionTypes += reference to parameterType +} + private fun TsState.initializeModel(method: EtsMethod): Boolean { val solver = ctx.solver() val solverResult = solver.check(pathConstraints) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index c6c7642a60..72fd52a611 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -152,6 +152,10 @@ class TsState( internal var collectionIterators: Map = emptyMap() + internal var inputCollectionTypes: Map = emptyMap() + internal var inputCollectionReferences: Map = emptyMap() + internal var collectionOriginalReceivers: Map = emptyMap() + internal var modeledCollections: Map = emptyMap() internal var initialEnvironmentFailure: String? = null internal var initialEnvironmentHeaps: Map = emptyMap() @@ -424,6 +428,9 @@ class TsState( ).also { cloned -> cloned.collectionIterators = collectionIterators cloned.modeledCollections = modeledCollections + cloned.inputCollectionTypes = inputCollectionTypes + cloned.inputCollectionReferences = inputCollectionReferences + cloned.collectionOriginalReceivers = collectionOriginalReceivers cloned.promiseExecutorFunctions = promiseExecutorFunctions cloned.initialEnvironmentFailure = initialEnvironmentFailure cloned.initialEnvironmentHeaps = initialEnvironmentHeaps diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt index 587caa961f..f73fb040e4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/TsTestResolver.kt @@ -371,6 +371,13 @@ open class TsTestStateResolver( return TsTestValue.TsNull } + val inputCollection = propertyState?.inputCollectionReferences?.keys?.any { reference -> + evaluateInModel(reference) == concreteRef + } == true + if (inputCollection) { + throw TsUnsupportedWitnessException("Native input collection witness reconstruction is not modeled") + } + val type = if (concreteRef.isAllocated) { resolutionMemory.typeStreamOf(concreteRef).first() } else { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/InputCollectionsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/InputCollectionsTest.kt new file mode 100644 index 0000000000..895abadf00 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/InputCollectionsTest.kt @@ -0,0 +1,114 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import org.usvm.PathSelectionStrategy +import org.usvm.StateCollectionStrategy +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsMethodTestRunner +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +/** Normal source entries; inspect scalar returns because native input witnesses are not serializable yet. */ +class InputCollectionsTest : TsMethodTestRunner() { + override val scene = loadScene("/models/InputCollections.ts") + override val tsOptions = TsOptions(eraseTypeAssertions = true, maxInputCollectionSize = 2, maxArraySize = 4) + + init { + options = options.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + collectedStatesLimit = null, + throwExceptionOnStepFailure = true, + ) + } + + @Test + fun `input map includes empty and nonempty cardinalities`() = assertReturns("mapPresence", setOf(1.0, 2.0, 3.0)) + + @Test + fun `input map membership values size and mutations agree`() = assertReturns("mapMutation", setOf(1.0, 2.0)) + + @Test + fun `symbolically equal receivers share a backend and distinct receivers remain separate`() = + assertReturns("aliases", setOf(1.0, 2.0)) + + @Test + fun `typed input field and local alias share mutations`() = assertReturns("field", setOf(1.0)) + + @Test + fun `input set includes present and absent elements with coherent size`() = + assertReturns("setPresence", setOf(1.0, 2.0)) + + @Test + fun `input insertion order enumerates every live entry exactly once`() = + assertReturns("iteration", setOf(1.0, 2.0)) + + @Test + fun `input iterator observes clear and reinsert with sticky exhaustion`() = + assertReturns("liveIteration", setOf(1.0)) + + @Test + fun `input string keys preserve SameValueZero content equality`() = assertReturns("stringKeys", setOf(1.0)) + + @Test + fun `input mutation does not leak between forks`() = assertReturns("stateFork", setOf(1.0, 2.0)) + + @Test + fun `initial lookup is stable and membership distinguishes missing values`() = + assertReturns("initialLookup", setOf(1.0, 2.0, 3.0)) + + @Test + fun `erased aliases retain native collection state`() = assertReturns("erasedAlias", setOf(1.0)) + + @Test + fun `native size writes and deletes stay explicit unsupported boundaries`() { + for (name in listOf("invalidSizeWrite", "invalidSizeDelete")) { + val method = getMethod(methodName = name, className = "InputCollections") + + val outcome = TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> + machine.analyzeWithMetadata(methods = listOf(method)) + } + + assertFalse(outcome.engineFailed, name) + assertTrue(outcome.unsupportedPaths.any { it.contains("native collection size") }, name) + assertTrue(outcome.states.isEmpty(), name) + } + } + + @Test + fun `disabled input domain retains explicit unsupported outcome`() { + val disabled = tsOptions.copy(maxInputCollectionSize = null) + for (name in listOf("mapMutation", "field")) { + val method = getMethod(methodName = name, className = "InputCollections") + + val outcome = TsMachine(scene = scene, options = options, tsOptions = disabled).use { machine -> + machine.analyzeWithMetadata(methods = listOf(method)) + } + + assertTrue(outcome.unsupportedCall, name) + val completed = outcome.states.any { it.methodResult is TsMethodResult.Success } + assertFalse(completed, name) + assertFalse(outcome.engineFailed, name) + } + } + + private fun assertReturns(name: String, expected: Set) { + val method = getMethod(methodName = name, className = "InputCollections") + val outcome = TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> + machine.analyzeWithMetadata(methods = listOf(method)) + } + + assertFalse(outcome.engineFailed, name) + assertFalse(outcome.unsupportedCall, outcome.unsupportedPaths.toString()) + val actual = outcome.states.map { state -> + val result = state.methodResult as TsMethodResult.Success + state.models.first().eval(result.value.asExpr(state.ctx.fp64Sort)).extractDouble() + }.toSet() + assertEquals(expected = expected, actual = actual, message = name) + } +} diff --git a/usvm-ts/src/test/resources/models/InputCollections.ts b/usvm-ts/src/test/resources/models/InputCollections.ts new file mode 100644 index 0000000000..cf8b16f896 --- /dev/null +++ b/usvm-ts/src/test/resources/models/InputCollections.ts @@ -0,0 +1,109 @@ +export class InputCollections { + values: Map; + + mapPresence(map: Map): number { + const before = map.size; + if (before === 0) { + if (map.has(7) || map.get(7) !== undefined) return -1; + return 1; + } + if (before === 2) return 2; + return 3; + } + + initialLookup(map: Map): number { + const has = map.has(7); + const first = map.get(7); + const second = map.get(7); + if (!has) return first === undefined && second === undefined ? 1 : -1; + if (first !== second && !(first !== first && second !== second)) return -2; + return first === 19 ? 2 : 3; + } + + erasedAlias(map: Map): number { + const alias: any = map; + alias.set('key', 19); + return alias.get('key') === 19 && alias.size === map.size ? 1 : -1; + } + + invalidSizeWrite(map: Map): void { + (map as any).size = 7; + } + + invalidSizeDelete(map: Map): void { + delete (map as any).size; + } + + mapMutation(map: Map): number { + const before = map.size; + const had = map.has(7); + if (map.set(7, 19) !== map) return -1; + if (!map.has(7) || map.get(7) !== 19) return -2; + if (map.size !== before + (had ? 0 : 1)) return -3; + if (!map.delete(7) || map.has(7) || map.get(7) !== undefined) return -4; + map.clear(); + if (map.size !== 0) return -5; + return had ? 1 : 2; + } + + aliases(left: Map, right: Map): number { + left.clear(); + right.clear(); + left.set(7, 19); + if (left === right) { + if (!right.has(7) || right.get(7) !== 19 || right.size !== 1) return -1; + right.delete(7); + return left.size === 0 ? 1 : -2; + } + return right.has(7) ? -3 : 2; + } + + field(): number { + const alias = this.values; + alias.clear(); + this.values.set(7, 19); + return alias.get(7) === 19 && alias.size === 1 ? 1 : -1; + } + + setPresence(set: Set): number { + const before = set.size; + const had = set.has(7); + if (set.add(7) !== set || !set.has(7)) return -1; + if (set.size !== before + (had ? 0 : 1)) return -2; + if (!set.delete(7) || set.has(7)) return -3; + set.clear(); + return set.size === 0 ? (had ? 1 : 2) : -4; + } + + iteration(map: Map): number { + let count = 0; + for (const key of map.keys()) { + if (!map.has(key)) return -1; + count++; + } + return count === map.size ? (count === 0 ? 1 : 2) : -2; + } + + liveIteration(set: Set): number { + const iterator = set.values(); + set.clear(); + set.add(19); + const first = iterator.next(); + if (first.done || first.value !== 19) return -1; + if (!iterator.next().done) return -2; + set.add(23); + return iterator.next().done ? 1 : -3; + } + + stringKeys(map: Map): number { + map.set('key', 19); + return map.get('k' + 'ey') === 19 && map.has('key') ? 1 : -1; + } + + stateFork(map: Map, clear: boolean): number { + map.set(7, 19); + if (clear) map.clear(); + if (clear) return map.has(7) ? -1 : 1; + return map.get(7) === 19 ? 2 : -2; + } +}