[TS] Support explicitly bounded symbolic Map and Set inputs

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(

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<EtsClassSignature>? = 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" }
 

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)
+}

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<TsUnknownCallModel> = 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) },
                         )
                     }

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
 

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())

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

@@ -18,17 +18,22 @@ 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
 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

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 {