diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt index 14f5c46d78..0476738c48 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt @@ -1,6 +1,7 @@ package org.usvm.machine.call import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsLocal @@ -26,6 +27,7 @@ internal fun hasBuiltinGlobalOwner( internal fun EtsType.isBuiltinGlobalType(expectedName: String): Boolean = when (expectedName) { "Math" -> this is EtsUnclearRefType && name == expectedName "Number" -> this is EtsFunctionType && isBuiltinNumberType() + "Array" -> this is EtsFunctionType && isBuiltinArrayType() else -> false } @@ -39,6 +41,15 @@ private fun EtsFunctionType.isBuiltinNumberType(): Boolean { !parameter.isRest } +private fun EtsFunctionType.isBuiltinArrayType(): Boolean { + val parameter = signature.parameters.singleOrNull() ?: return false + val arrayType = signature.returnType as? EtsArrayType ?: return false + return signature.enclosingClass == EtsClassSignature.UNKNOWN && + signature.name.isEmpty() && + arrayType.elementType == EtsAnyType && arrayType.dimensions == 1 && + parameter.type == EtsNumberType && parameter.isOptional && !parameter.isRest +} + private fun EtsValue.isLegacyBuiltinGlobal( expectedName: String, callee: EtsMethodSignature, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index 6e54d99301..e349d46462 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -325,6 +325,18 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { inputAdapter = TsDenseArrayModelSupport.reduceAdapter, domainGuard = TsDenseArrayModelSupport.denseReceiverDomain, ), + sourceModel( + id = "ts.array.map", + methodName = "map", + inputAdapter = TsDenseArrayModelSupport.callbackAdapter, + domainGuard = TsArraySlotPrimitives.reverseDomain, + ), + sourceModel( + id = "ts.array.forEach", + methodName = "forEach", + inputAdapter = TsDenseArrayModelSupport.callbackAdapter, + domainGuard = TsArraySlotPrimitives.reverseDomain, + ), sourceModel( id = "ts.array.pop", methodName = "pop", @@ -438,7 +450,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { domainGuard = domainGuard, inputAdapter = inputAdapter, requiredModelIds = buildSet { - if (methodName in setOf("reverse", "unshift")) { + if (methodName in setOf("reverse", "unshift", "map", "forEach")) { add("ts.array.primitive.prepareOwnSlots") add("ts.array.primitive.hasOwnSlot") } @@ -457,6 +469,9 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { if (methodName in setOf("push", "unshift")) { add(PRIMITIVE_GROW_ID) } + if (methodName == "map") { + add(PRIMITIVE_ALLOCATE_ID) + } if (methodName in setOf("slice", "concat")) { add(PRIMITIVE_ALLOCATE_LIKE_ID) } @@ -585,6 +600,8 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { sizeSort = sizeSort, count = length, ) + // Fresh allocations have known holes until the source algorithm writes each own slot. + knownArrayPropertyPresence += result result }, ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsCollectionEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsCollectionEtsIrModelFamily.kt new file mode 100644 index 0000000000..df46b586fb --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsCollectionEtsIrModelFamily.kt @@ -0,0 +1,190 @@ +package org.usvm.machine.call.intrinsic + +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.api.typeStreamOf +import org.usvm.machine.call.TsEtsIrUnknownCallModel +import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact +import org.usvm.machine.call.TsEtsIrUnknownCallModelInputAdapter +import org.usvm.machine.call.TsResidualCallPolicy +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModel +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.call.hasBuiltinGlobalOwner +import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact +import org.usvm.machine.expr.TsCollectionKind +import org.usvm.machine.expr.newModeledCollection +import org.usvm.machine.state.TsState +import org.usvm.types.singleOrNull +import org.usvm.util.arrayStorageType + +/** Iterable construction executes normal source bodies over modeled native storage. */ +internal object TsCollectionEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { + private const val CLASS_NAME = "CollectionModels" + private const val PRIMITIVES_NAME = "CollectionModelPrimitives" + private val baseArtifact by lazy { + loadBundledEtsIrUnknownCallModelArtifact( + resourceName = "/org/usvm/machine/call/models/CollectionModels.ts", + sourceFileName = "CollectionModels.ts", + entryPointClassName = CLASS_NAME, + entryPointMethodName = "arrayFrom", + ) + } + private val sourceModelIds by lazy { models.filterIsInstance().map { it.id }.toSet() } + + override val models: List by lazy { + listOf( + constructor(kind = TsCollectionKind.MAP, name = "Map"), + constructor(kind = TsCollectionKind.SET, name = "Set"), + populate(kind = TsCollectionKind.MAP, name = "Map"), + populate(kind = TsCollectionKind.SET, name = "Set"), + initializer(kind = TsCollectionKind.MAP, name = "initializeMap"), + initializer(kind = TsCollectionKind.SET, name = "initializeSet"), + arrayFromModel(), + ) + } + + private fun arrayFromModel(): TsUnknownCallModel = TsEtsIrUnknownCallModel( + id = "ts.array.fromIterable", + target = TsUnknownCallTarget(methodName = "from"), + artifact = artifact("arrayFrom"), + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val owner = call.receiver?.source ?: return@TsEtsIrUnknownCallModelInputAdapter null + if (!hasBuiltinGlobalOwner(owner, call.callee, expectedName = "Array")) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + val arguments = call.arguments.map { + it.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null + } + val input = arguments.firstOrNull() ?: return@TsEtsIrUnknownCallModelInputAdapter null + val mapping = arguments.getOrNull(1) ?: state.ctx.mkUndefinedValue() + val supportedInput = state.supportsIterable(input, call.arguments[0].source.type) + if (mapping != state.ctx.mkUndefinedValue() || !supportedInput) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + listOf(input) + }, + requiredModelIds = setOf( + "ts.array.push", + "ts.array.primitive.grow", + TsIteratorModelFamily.COLLECTION_ITERATOR_ID, + ), + ) + + + private fun constructor(kind: TsCollectionKind, name: String): TsUnknownCallModel { + val entry = if (kind == TsCollectionKind.MAP) "mapConstructor" else "setConstructor" + val initialize = if (kind == TsCollectionKind.MAP) "initializeMap" else "initializeSet" + val signature = EtsClassSignature.UNKNOWN.copy(name = name) + return TsEtsIrUnknownCallModel( + id = "ts.${name.lowercase()}.constructor", + target = TsUnknownCallTarget(methodName = CONSTRUCTOR_NAME, enclosingClassName = name), + artifact = artifact(entry), + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val receiver = call.receiver?.resolved as? UConcreteHeapRef + ?: return@TsEtsIrUnknownCallModelInputAdapter null + val runtimeType = state.memory.typeStreamOf(receiver).singleOrNull() + if (call.callee.enclosingClass != signature || runtimeType != EtsClassType(signature)) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + val arguments = call.arguments.map { it.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null } + val input = arguments.firstOrNull() ?: state.ctx.mkUndefinedValue() + listOf(receiver, input) + }, + requiredModelIds = setOf("ts.collection.primitive.$initialize"), + ) + } + + // Optional populate helpers keep the original constructor model usable without iterable models. + private fun populate(kind: TsCollectionKind, name: String): TsUnknownCallModel { + val entry = if (kind == TsCollectionKind.MAP) "mapFromIterable" else "setFromIterable" + val helper = if (kind == TsCollectionKind.MAP) "populateMap" else "populateSet" + val initialize = if (kind == TsCollectionKind.MAP) "initializeMap" else "initializeSet" + val operation = if (kind == TsCollectionKind.MAP) "set" else "add" + return TsEtsIrUnknownCallModel( + id = "ts.${name.lowercase()}.fromIterable", + target = TsUnknownCallTarget( + methodName = helper, + enclosingClassName = PRIMITIVES_NAME, + failureReason = TsUnknownCallFailureReason.METHOD_BODY_UNAVAILABLE, + ), + artifact = artifact(entry), + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val sourceFile = baseArtifact.file + val helperSignature = sourceFile.allClasses.single { it.name == PRIMITIVES_NAME }.signature + val caller = call.callSite.location.method + val sourceCaller = caller.signature.enclosingClass + val ownedCall = call.callee.enclosingClass == helperSignature && + sourceCaller == baseArtifact.entryPoint.signature.enclosingClass && + state.isUnknownCallModelActive("ts.${name.lowercase()}.constructor") + if (!ownedCall) return@TsEtsIrUnknownCallModelInputAdapter null + val inputs = call.arguments.map { it.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null } + if (inputs.size != 2) return@TsEtsIrUnknownCallModelInputAdapter null + val supportedInput = state.supportsIterable(inputs[1], call.arguments[1].source.type) + if (!supportedInput) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + inputs + }, + requiredModelIds = setOf( + "ts.collection.primitive.$initialize", + "ts.collection.$operation", + "ts.typeError.constructor", + TsIteratorModelFamily.COLLECTION_ITERATOR_ID, + ), + ) + } + + private fun initializer(kind: TsCollectionKind, name: String): TsUnknownCallModel = TsPrimitiveUnknownCallModel( + idPrefix = "ts.collection.primitive", + methodName = name, + enclosingClassName = PRIMITIVES_NAME, + arity = 1, + helperClassSignature = { baseArtifact.file.allClasses.single { it.name == PRIMITIVES_NAME }.signature }, + sourceClassSignature = { baseArtifact.entryPoint.signature.enclosingClass }, + owningModelIds = { sourceModelIds }, + implementation = { state, inputs -> + val receiver = inputs.single() as? UConcreteHeapRef + if (receiver == null) { + null + } else { + val successor = TsUnknownCallModelSuccessor( + guard = state.ctx.trueExpr, + completion = TsUnknownCallModelCompletion.Normal { + modeledCollections += receiver to newModeledCollection(kind) + ctx.mkUndefinedValue() + }, + ) + TsUnknownCallModelExecution(successors = listOf(successor)) + } + }, + unsupportedCallPolicy = TsResidualCallPolicy.STOP_PATH, + ) + + private fun TsState.supportsIterable(input: UExpr<*>, staticType: EtsType): Boolean { + val reference = input as? UConcreteHeapRef ?: return false + val knownNative = reference in modeledCollections || reference in collectionIterators || + reference in arrayIterators || reference in stringIterators + if (knownNative) return true + val type = arrayStorageType(reference, staticType) + return type is EtsArrayType || type == EtsStringType + } + + private fun artifact(name: String): TsEtsIrUnknownCallModelArtifact { + val artifact = baseArtifact + val method = artifact.file.allClasses + .single { it.name == CLASS_NAME } + .methods + .single { it.name == name } + return artifact.copy(entryPoint = method) + } +} 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 c7a0544335..aaa80f1fcd 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 @@ -1,19 +1,15 @@ package org.usvm.machine.call.intrinsic -import org.jacodb.ets.model.EtsClassSignature -import org.jacodb.ets.model.EtsClassType -import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.usvm.UConcreteHeapRef -import org.usvm.api.typeStreamOf import org.usvm.isFalse import org.usvm.machine.call.TsUnknownCall -import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallModel 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.TsCollectionKind +import org.usvm.machine.expr.collectionClear import org.usvm.machine.expr.collectionGet import org.usvm.machine.expr.collectionInsert import org.usvm.machine.expr.collectionMatches @@ -21,18 +17,14 @@ import org.usvm.machine.expr.collectionPut import org.usvm.machine.expr.collectionRemove import org.usvm.machine.expr.collectionUndefined import org.usvm.machine.expr.collectionValue -import org.usvm.machine.expr.newModeledCollection import org.usvm.machine.state.TsState import org.usvm.machine.types.iteUnresolvedValue -import org.usvm.types.singleOrNull -/** Empty native constructors and a bounded coherent subset of Map/Set operations. */ +/** A bounded coherent subset of native Map/Set operations. */ internal object TsCollectionModelFamily : TsBuiltInUnknownCallModelFamily { private const val MAX_ENTRIES = 16 override val models: List = listOf( - ConstructorModel(kind = TsCollectionKind.MAP, name = "Map"), - ConstructorModel(kind = TsCollectionKind.SET, name = "Set"), OperationModel(operation = "get"), OperationModel(operation = "set"), OperationModel(operation = "add"), @@ -41,35 +33,6 @@ internal object TsCollectionModelFamily : TsBuiltInUnknownCallModelFamily { OperationModel(operation = "clear"), ) - private class ConstructorModel(private val kind: TsCollectionKind, name: String) : TsUnknownCallModel { - private val signature = EtsClassSignature.UNKNOWN.copy(name = name) - override val id = "ts.${name.lowercase()}.constructor" - override val target = TsUnknownCallTarget( - methodName = CONSTRUCTOR_NAME, - enclosingClassName = name, - failureReason = TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, - ) - - override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? = with(state.ctx) { - val receiver = call.receiver?.resolved as? UConcreteHeapRef ?: return null - if (call.callee.enclosingClass != signature) return null - val runtimeType = state.memory.typeStreamOf(receiver).singleOrNull() - val nativeType = EtsClassType(signature) - if (runtimeType != nativeType) return null - val arguments = call.arguments.map { it.resolved ?: return null } - val emptyInput = arguments.isEmpty() || arguments.first() == mkUndefinedValue() || - arguments.first() == mkTsNullValue() - if (!emptyInput) return null - - val successor = TsUnknownCallModelSuccessor( - guard = trueExpr, - completion = TsUnknownCallModelCompletion.Normal { receiver }, - applyStateChanges = { modeledCollections += receiver to newModeledCollection(kind = kind) }, - ) - TsUnknownCallModelExecution(successors = listOf(successor)) - } - } - private class OperationModel(private val operation: String) : TsUnknownCallModel { override val id = "ts.collection.$operation" override val target = TsUnknownCallTarget(methodName = operation) @@ -86,7 +49,7 @@ internal object TsCollectionModelFamily : TsBuiltInUnknownCallModelFamily { guard = trueExpr, completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, applyStateChanges = { - modeledCollections += receiver to newModeledCollection(kind = collection.kind) + collectionClear(receiver, collection) }, ) return TsUnknownCallModelExecution(successors = listOf(successor)) @@ -135,7 +98,9 @@ internal object TsCollectionModelFamily : TsBuiltInUnknownCallModelFamily { TsUnknownCallModelSuccessor( guard = match.guard, completion = TsUnknownCallModelCompletion.Normal { receiver }, - applyStateChanges = { collectionPut(collection, match.key, value) }, + applyStateChanges = { + if (collection.kind == TsCollectionKind.MAP) collectionPut(collection, match.key, value) + }, ) }.toMutableList() val canInsert = collection.keys.size < MAX_ENTRIES diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayModelSupport.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayModelSupport.kt index e8e8de1ccc..915515e302 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayModelSupport.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsDenseArrayModelSupport.kt @@ -54,6 +54,19 @@ internal object TsDenseArrayModelSupport { } } + // A non-undefined thisArg requires the callback invocation machinery to bind `this` explicitly. + val callbackAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val receiver = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null + val arguments = call.arguments.map { it.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null } + val callback = arguments.firstOrNull() as? UConcreteHeapRef + ?: return@TsEtsIrUnknownCallModelInputAdapter null + if (callback !in state.associatedFunction) return@TsEtsIrUnknownCallModelInputAdapter null + val thisArgument = arguments.getOrNull(1) ?: state.ctx.mkUndefinedValue() + if (thisArgument != state.ctx.mkUndefinedValue()) return@TsEtsIrUnknownCallModelInputAdapter null + + listOf(receiver, callback) + } + val reduceAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> val inputs = call.resolvedInstanceInputs(maxArgumentCount = 2) ?: return@TsEtsIrUnknownCallModelInputAdapter null diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsIteratorModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsIteratorModelFamily.kt new file mode 100644 index 0000000000..5172b81742 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsIteratorModelFamily.kt @@ -0,0 +1,77 @@ +package org.usvm.machine.call.intrinsic + +import org.usvm.UConcreteHeapRef +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModel +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.TsArrayIterator +import org.usvm.machine.expr.TsCollectionKind +import org.usvm.machine.expr.TsIteratorKind +import org.usvm.machine.expr.arrayIteratorType +import org.usvm.machine.expr.newCollectionIterator +import org.usvm.machine.state.TsState + +/** Named native iterator methods; arbitrary project receivers do not satisfy the runtime domain. */ +internal object TsIteratorModelFamily : TsBuiltInUnknownCallModelFamily { + const val COLLECTION_ITERATOR_ID = "ts.iterator.collection" + const val COLLECTION_ITERATOR_METHOD = "%collectionIterator" + + override val models: List = + TsIteratorKind.entries.map { kind -> IteratorModel(kind) } + CollectionIteratorModel + + private object CollectionIteratorModel : TsUnknownCallModel { + override val id = COLLECTION_ITERATOR_ID + override val target = TsUnknownCallTarget( + methodName = COLLECTION_ITERATOR_METHOD, + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + ) + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { + val receiver = call.receiver?.resolved as? UConcreteHeapRef ?: return null + val collection = state.modeledCollections[receiver] ?: return null + val kind = if (collection.kind == TsCollectionKind.MAP) TsIteratorKind.ENTRIES else TsIteratorKind.VALUES + val successor = TsUnknownCallModelSuccessor( + guard = state.ctx.trueExpr, + completion = TsUnknownCallModelCompletion.Normal { newCollectionIterator(receiver, kind) }, + ) + return TsUnknownCallModelExecution(successors = listOf(successor)) + } + } + + private class IteratorModel(private val kind: TsIteratorKind) : TsUnknownCallModel { + override val id = "ts.iterator.${kind.name.lowercase()}" + override val target = TsUnknownCallTarget(methodName = kind.name.lowercase()) + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { + val receiver = call.receiver?.resolved as? UConcreteHeapRef ?: return null + val collection = state.modeledCollections[receiver] + val array = if (collection == null) state.concreteArray(call, listOf(receiver)) else null + if (collection == null && array == null) return null + + val successor = TsUnknownCallModelSuccessor( + guard = state.ctx.trueExpr, + completion = TsUnknownCallModelCompletion.Normal { + if (collection != null) { + newCollectionIterator(receiver, kind) + } else { + val arrayType = requireNotNull(array).second + val iterator = memory.allocConcrete(arrayIteratorType) + arrayIterators += iterator to TsArrayIterator( + array = receiver, + arrayType = arrayType, + index = ctx.mkBv(0), + exhausted = ctx.falseExpr, + kind = kind, + ) + iterator + } + }, + ) + return TsUnknownCallModelExecution(successors = listOf(successor)) + } + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt index b66dcd8898..191f238902 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ArrayIterator.kt @@ -1,6 +1,7 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr +import io.ksmt.utils.cast import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType @@ -25,18 +26,28 @@ data class TsArrayIterator( val arrayType: EtsArrayType, val index: UExpr, val exhausted: UBoolExpr, + val kind: TsIteratorKind = TsIteratorKind.VALUES, ) /** The result object's fields are kept separate from the iterator's mutable cursor. */ data class TsIteratorResult(val done: UBoolExpr, val value: UExpr<*>) -private val iteratorType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinArrayIterator")) +internal val arrayIteratorType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinArrayIterator")) internal val iteratorResultType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinIteratorResult")) internal fun TsExprResolver.tryApproximateBuiltinIteratorCall( stmt: TsVirtualMethodCallStmt, ): TsExprApproximationResult = with(ctx) { + val collectionResult = tryApproximateCollectionIteratorCall(stmt) + if (collectionResult !is TsExprApproximationResult.NoApproximation) return collectionResult + if (stmt.call.wellKnownSymbol == EtsWellKnownSymbol.ITERATOR) { + val reference = stmt.instance as? UConcreteHeapRef + val nativeIterator = scope.calcOnState { + arrayIterators[reference] != null || stringIterators[reference] != null + } + if (nativeIterator) return TsExprApproximationResult.from(reference) + val string = tryCreateStringIterator(stmt) if (string !is TsExprApproximationResult.NoApproximation) return string @@ -77,7 +88,7 @@ private fun TsExprResolver.createArrayIterator(stmt: TsVirtualMethodCallStmt): U scope.assert(runtimeArray) ?: return null scope.calcOnState { - val iterator = memory.allocConcrete(iteratorType) + val iterator = memory.allocConcrete(arrayIteratorType) arrayIterators += iterator to TsArrayIterator( array = array, arrayType = arrayType, @@ -135,7 +146,21 @@ private fun TsExprResolver.advanceArrayIterator( val value = if (done.isTrue) { mkUndefinedValue() } else { - val element = readArrayElement(scope, iterator.array, iterator.index, iterator.arrayType) ?: return null + val indexNumber = mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = iterator.index.cast(), + signed = true, + ) + val element = when (iterator.kind) { + TsIteratorKind.KEYS -> indexNumber + TsIteratorKind.VALUES -> readArrayElement(scope, iterator.array, iterator.index, iterator.arrayType) + ?: return null + TsIteratorKind.ENTRIES -> { + val item = readArrayElement(scope, iterator.array, iterator.index, iterator.arrayType) ?: return null + scope.calcOnState { iteratorPair(collectionValue(indexNumber), collectionValue(item)) } + } + } iteWriteIntoFakeObject( scope = scope, condition = done, @@ -168,7 +193,10 @@ internal fun TsExprResolver.readBuiltinIteratorField(reference: UHeapRef, name: } } - val isIterator = scope.calcOnState { arrayIterators[reference] != null || stringIterators[reference] != null } + val isIterator = scope.calcOnState { + arrayIterators[reference] != null || stringIterators[reference] != null || + collectionIterators[reference] != null + } if (isIterator && name == "return") return mkUndefinedValue() null diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCollectionIterator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCollectionIterator.kt new file mode 100644 index 0000000000..2ea9ad7163 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCollectionIterator.kt @@ -0,0 +1,158 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsArrayType +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.EtsUnknownType +import org.jacodb.ets.model.EtsWellKnownSymbol +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.api.initializeArray +import org.usvm.isTrue +import org.usvm.machine.TsSizeSort +import org.usvm.machine.TsVirtualMethodCallStmt +import org.usvm.machine.call.TsBuiltInUnknownCallModels +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.dispatch +import org.usvm.machine.call.intrinsic.TsIteratorModelFamily +import org.usvm.machine.state.TsState +import org.usvm.machine.types.TsUnresolvedArrayKind +import org.usvm.machine.types.TsUnresolvedValue +import org.usvm.machine.types.iteUnresolvedValue +import org.usvm.machine.types.mkFakeValue +import org.usvm.sizeSort +import org.usvm.util.initializeArrayKind +import org.usvm.util.markDenseArrayOwnSlots + +/** Native iterator projection; entries yield fresh key/value pair arrays. */ +enum class TsIteratorKind { KEYS, VALUES, ENTRIES } + +/** Cursor refers to insertion history, so deletions, clear, and later additions remain visible. */ +internal data class TsCollectionIterator( + val receiver: UConcreteHeapRef, + val kind: TsIteratorKind, + val index: UExpr, + val exhausted: UBoolExpr, +) + +private val collectionIteratorType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%BuiltinCollectionIterator")) + +internal fun TsState.newCollectionIterator(receiver: UConcreteHeapRef, kind: TsIteratorKind): UHeapRef = with(ctx) { + val iterator = memory.allocConcrete(collectionIteratorType) + collectionIterators += iterator to TsCollectionIterator( + receiver = receiver, + kind = kind, + index = mkBv(0), + exhausted = falseExpr, + ) + iterator +} + +internal fun TsExprResolver.tryApproximateCollectionIteratorCall( + stmt: TsVirtualMethodCallStmt, +): TsExprApproximationResult = with(ctx) { + val receiver = stmt.instance as? UConcreteHeapRef ?: return TsExprApproximationResult.NoApproximation + val iterator = scope.calcOnState { collectionIterators[receiver] } + val collection = scope.calcOnState { modeledCollections[receiver] } + if (stmt.call.wellKnownSymbol == EtsWellKnownSymbol.ITERATOR) { + if (iterator != null) return TsExprApproximationResult.from(receiver) + if (collection == null) return TsExprApproximationResult.NoApproximation + val selectedModels = TsBuiltInUnknownCallModels.catalog(options.unknownCallModelSelection).modelIds + if (TsIteratorModelFamily.COLLECTION_ITERATOR_ID !in selectedModels) { + return TsExprApproximationResult.NoApproximation + } + unknownCallDispatcher.dispatch( + scope = scope, + call = stmt.call, + callSite = stmt.returnSite, + callee = stmt.call.callee.copy(name = TsIteratorModelFamily.COLLECTION_ITERATOR_METHOD), + failureReason = TsUnknownCallFailureReason.PARTIAL_APPROXIMATION, + resolvedReceiver = receiver, + resolvedArguments = stmt.args, + ) + return TsExprApproximationResult.ResolveFailure + } + if (iterator == null || stmt.call.callee.name != "next") return TsExprApproximationResult.NoApproximation + + TsExprApproximationResult.from(advanceCollectionIterator(receiver, iterator)) +} + +private fun TsExprResolver.advanceCollectionIterator( + reference: UConcreteHeapRef, + iterator: TsCollectionIterator, +): UHeapRef? = with(ctx) { + val collection = scope.calcOnState { modeledCollections[iterator.receiver] } + if (collection == null) { + throw UnsupportedOperationException("Collection iterator backend was invalidated by a residual mutation") + } + var found: UBoolExpr = falseExpr + var nextIndex = iterator.index + var value = scope.calcOnState { collectionUndefined() } + var selectedKey = value + var selectedValue = value + // Reverse construction selects the earliest live insertion at or after the cursor. + for ((index, key) in collection.insertionHistory.withIndex().reversed()) { + val present = scope.calcOnState { collectionPresent(collection, key) } + val inRange = mkBvSignedLessOrEqualExpr(iterator.index, mkBv(index)) + val selected = mkAnd(mkNot(iterator.exhausted), inRange, present) + val keyValue = scope.calcOnState { readCollectionPayload(key) } + val itemValue = scope.calcOnState { collectionGet(collection, key) } + selectedKey = iteUnresolvedValue(selected, keyValue, selectedKey) + selectedValue = iteUnresolvedValue(selected, itemValue, selectedValue) + nextIndex = mkIte(selected, mkBv(index + 1), nextIndex) + found = mkOr(found, selected) + } + val done = mkNot(found) + value = when (iterator.kind) { + TsIteratorKind.KEYS -> selectedKey + TsIteratorKind.VALUES -> selectedValue + TsIteratorKind.ENTRIES -> { + if (done.isTrue) value else scope.calcOnState { collectionValue(iteratorPair(selectedKey, selectedValue)) } + } + } + val resultValue = iteUnresolvedValue(done, scope.calcOnState { collectionUndefined() }, value) + val materialized = scope.calcOnState { mkFakeValue(scope = scope, value = resultValue) } ?: return null + + scope.calcOnState { + collectionIterators += reference to iterator.copy(index = nextIndex, exhausted = done) + val result = memory.allocConcrete(iteratorResultType) + iteratorResults += result to TsIteratorResult(done = done, value = materialized) + result + } +} + +/** A fresh two-slot native array preserves heterogeneous entry payloads and their kind selectors. */ +internal fun TsState.iteratorPair(first: TsUnresolvedValue, second: TsUnresolvedValue): UConcreteHeapRef = with(ctx) { + val values = listOf(first, second) + val type = EtsArrayType(EtsUnknownType, dimensions = 1) + val pair = memory.allocConcrete(type) + memory.initializeArray( + arrayHeapRef = pair, + type = EtsArrayType(EtsBooleanType, dimensions = 1), + sort = boolSort, + sizeSort = sizeSort, + contents = values.asSequence().map { it.boolValue }, + ) + memory.initializeArray( + arrayHeapRef = pair, + type = EtsArrayType(EtsNumberType, dimensions = 1), + sort = fp64Sort, + sizeSort = sizeSort, + contents = values.asSequence().map { it.fpValue }, + ) + memory.initializeArray( + arrayHeapRef = pair, + type = type, + sort = addressSort, + sizeSort = sizeSort, + contents = values.asSequence().map { it.refValue }, + ) + initializeArrayKind(pair, TsUnresolvedArrayKind.BOOLEAN, values.map { it.type.boolTypeExpr }) + initializeArrayKind(pair, TsUnresolvedArrayKind.NUMBER, values.map { it.type.fpTypeExpr }) + markDenseArrayOwnSlots(array = pair, length = mkBv(2), capacity = 2) + pair +} 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 8f8d8b0117..11124cf31b 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 @@ -36,6 +36,7 @@ internal data class TsModeledCollection( val kind: TsCollectionKind, val storage: UConcreteHeapRef, val keys: List = emptyList(), + val insertionHistory: List = emptyList(), ) internal data class TsCollectionMatch(val key: UConcreteHeapRef, val guard: UBoolExpr) @@ -105,8 +106,12 @@ internal fun TsState.collectionInsert( val zero = mkFp64(0.0) val normalizedKey = key.copy(fpValue = mkIte(mkFpEqualExpr(key.fpValue, zero), zero, key.fpValue)) val identity = allocateCollectionPayload(normalizedKey) - collectionPut(collection, identity, value) - modeledCollections += receiver to collection.copy(keys = collection.keys + identity) + val storedValue = if (collection.kind == TsCollectionKind.SET) normalizedKey else value + collectionPut(collection, identity, storedValue) + modeledCollections += receiver to collection.copy( + keys = collection.keys + identity, + insertionHistory = collection.insertionHistory + identity, + ) } internal fun TsState.collectionRemove( @@ -118,6 +123,16 @@ internal fun TsState.collectionRemove( modeledCollections += receiver to collection.copy(keys = collection.keys - key) } +internal fun TsState.collectionClear(receiver: UConcreteHeapRef, collection: TsModeledCollection) { + for (key in collection.keys) { + symbolicObjectMapRemove(collection.storage, key, storageType) + } + modeledCollections += receiver to collection.copy(keys = emptyList()) +} + +internal fun TsState.collectionPresent(collection: TsModeledCollection, key: UConcreteHeapRef): UBoolExpr = + symbolicObjectMapContains(collection.storage, key, storageType) + internal fun TsState.collectionSize(collection: TsModeledCollection): UExpr<*> = with(ctx) { val size = symbolicObjectMapSize(collection.storage, storageType) mkBvToFpExpr( @@ -149,7 +164,7 @@ private fun TsState.allocateCollectionPayload(value: TsUnresolvedValue): UConcre ref } -private fun TsState.readCollectionPayload(ref: UHeapRef): TsUnresolvedValue = with(ctx) { +internal fun TsState.readCollectionPayload(ref: UHeapRef): TsUnresolvedValue = with(ctx) { val boolean = memory.read(UFieldLValue(boolSort, ref, CollectionPayload.BOOLEAN)) val number = memory.read(UFieldLValue(fp64Sort, ref, CollectionPayload.NUMBER)) val reference = memory.read(UFieldLValue(addressSort, ref, CollectionPayload.REFERENCE)) 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 59b86472a7..c6c7642a60 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 @@ -32,6 +32,7 @@ import org.usvm.machine.TsSizeSort import org.usvm.machine.expr.TrackedObjectProperty import org.usvm.machine.expr.TsArrayIterator import org.usvm.machine.expr.TsCapturedInstanceCall +import org.usvm.machine.expr.TsCollectionIterator import org.usvm.machine.expr.TsIteratorResult import org.usvm.machine.expr.TsModeledCollection import org.usvm.machine.expr.TsStringIterator @@ -149,6 +150,8 @@ class TsState( ) { internal var promiseExecutorFunctions: Map = emptyMap() + internal var collectionIterators: Map = emptyMap() + internal var modeledCollections: Map = emptyMap() internal var initialEnvironmentFailure: String? = null internal var initialEnvironmentHeaps: Map = emptyMap() @@ -419,6 +422,7 @@ class TsState( denseInputArrays = denseInputArrays.toMutableMap(), activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ).also { cloned -> + cloned.collectionIterators = collectionIterators cloned.modeledCollections = modeledCollections cloned.promiseExecutorFunctions = promiseExecutorFunctions cloned.initialEnvironmentFailure = initialEnvironmentFailure diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts index ca36a2ce26..b717a4ecb6 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts @@ -70,6 +70,32 @@ export class ArrayModels { return accumulator; } + static map(receiver: any[], callback: (value: any, index: number, array: any[]) => any): any[] { + ArrayModelPrimitives.prepareOwnSlots(receiver); + const length = receiver.length; + const result = ArrayModelPrimitives.allocate(length); + let index = 0; + while (index < length) { + if (ArrayModelPrimitives.hasOwnSlot(receiver, index)) { + result[index] = callback(receiver[index], index, receiver); + } + index++; + } + return result; + } + + static forEach(receiver: any[], callback: (value: any, index: number, array: any[]) => any): void { + ArrayModelPrimitives.prepareOwnSlots(receiver); + const length = receiver.length; + let index = 0; + while (index < length) { + if (ArrayModelPrimitives.hasOwnSlot(receiver, index)) { + callback(receiver[index], index, receiver); + } + index++; + } + } + static fromLength(length: number): any[] { return ArrayModelPrimitives.allocate(length); } diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/CollectionModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/CollectionModels.ts new file mode 100644 index 0000000000..80e2e4d708 --- /dev/null +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/CollectionModels.ts @@ -0,0 +1,44 @@ +declare class CollectionModelPrimitives { + static initializeMap(receiver: any): void; + static initializeSet(receiver: any): void; + static populateMap(receiver: any, input: any): void; + static populateSet(receiver: any, input: any): void; +} + +export class CollectionModels { + static mapConstructor(receiver: any, input: any): any { + if (input === undefined || input === null) CollectionModelPrimitives.initializeMap(receiver); + else CollectionModelPrimitives.populateMap(receiver, input); + return receiver; + } + + static setConstructor(receiver: any, input: any): any { + if (input === undefined || input === null) CollectionModelPrimitives.initializeSet(receiver); + else CollectionModelPrimitives.populateSet(receiver, input); + return receiver; + } + + static mapFromIterable(receiver: any, input: any): any { + CollectionModelPrimitives.initializeMap(receiver); + for (const entry of input) { + if (entry === null || (typeof entry !== 'object' && typeof entry !== 'function')) { + throw new TypeError('Iterator value is not an entry object'); + } + receiver.set(entry[0], entry[1]); + } + return receiver; + } + + static setFromIterable(receiver: any, input: any): any { + CollectionModelPrimitives.initializeSet(receiver); + for (const value of input) receiver.add(value); + return receiver; + } + + static arrayFrom(input: any): any[] { + const result: any[] = []; + for (const value of input) result.push(value); + return result; + } + +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt index e05a73e8f8..2975b7f704 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -183,12 +183,15 @@ class TsUnknownCallModelCatalogTest { val expectedModelIds = listOf( "ts.array.concat", "ts.array.fill", + "ts.array.forEach", + "ts.array.fromIterable", "ts.array.fromLength", "ts.array.includes", "ts.array.indexOf", "ts.array.isArray", "ts.array.join", "ts.array.lastIndexOf", + "ts.array.map", "ts.array.pop", "ts.array.primitive.allocate", "ts.array.primitive.allocateLike", @@ -210,9 +213,16 @@ class TsUnknownCallModelCatalogTest { "ts.collection.delete", "ts.collection.get", "ts.collection.has", + "ts.collection.primitive.initializeMap", + "ts.collection.primitive.initializeSet", "ts.collection.set", TsErrorEtsIrModelFamily.CONSTRUCTOR_ID, + "ts.iterator.collection", + "ts.iterator.entries", + "ts.iterator.keys", + "ts.iterator.values", "ts.map.constructor", + "ts.map.fromIterable", TsNumericIntrinsicModelFamily.MATH_ABS_ID, TsNumericIntrinsicModelFamily.MATH_CEIL_ID, TsNumericIntrinsicModelFamily.MATH_FLOOR_ID, @@ -228,6 +238,7 @@ class TsUnknownCallModelCatalogTest { TsNumericIntrinsicModelFamily.NUMBER_IS_SAFE_INTEGER_ID, "ts.number.parseFloat", "ts.set.constructor", + "ts.set.fromIterable", "ts.string.charAt", "ts.string.charCodeAt", "ts.string.endsWith", diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/CollectionOperationsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/CollectionOperationsTest.kt new file mode 100644 index 0000000000..06ac74f66d --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/CollectionOperationsTest.kt @@ -0,0 +1,211 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsMethod +import org.junit.jupiter.api.io.TempDir +import org.usvm.PathSelectionStrategy +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTest +import org.usvm.api.TsTestValue +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.call.TsBuiltInUnknownCallModels +import org.usvm.machine.call.TsUnknownCallModelSelection +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.Test +import kotlin.test.assertTrue + +class CollectionOperationsTest : TsMethodTestRunner() { + override val scene = loadScene("/models/CollectionOperations.ts") + override val tsOptions = TsOptions(eraseTypeAssertions = true) + + override val runner: (EtsMethod, UMachineOptions) -> List = { method, machineOptions -> + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + @TempDir + lateinit var directory: Path + + init { + options = options.copy( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + } + + private val methods = listOf( + "iterableSet", "iterableMap", "mapInvalidEntry", "copyCollections", "arrayFromKeys", + "liveMapIterator", "clearDuringIteration", "setEntryAndZero", "arrayEntryLiveLength", + "arrayKeysAndHoles", "arrayMap", "arrayMapMutation", "arrayForEachMutation", "callbackThrows", + "callbackWithoutThis", "shadowedArrayFrom", "implicitCollectionIteration", + ) + + @Test + fun `iterableSet preserves native source semantics`() { + assertOne(methodName = "iterableSet") + } + + @Test + fun `iterableMap preserves native source semantics`() { + assertOne(methodName = "iterableMap") + } + + @Test + fun `mapInvalidEntry preserves native source semantics`() { + assertOne(methodName = "mapInvalidEntry") + } + + @Test + fun `copyCollections preserves native source semantics`() { + assertOne(methodName = "copyCollections") + } + + @Test + fun `arrayFromKeys preserves native source semantics`() { + assertOne(methodName = "arrayFromKeys") + } + + @Test + fun `liveMapIterator preserves native source semantics`() { + assertOne(methodName = "liveMapIterator") + } + + @Test + fun `clearDuringIteration preserves native source semantics`() { + assertOne(methodName = "clearDuringIteration") + } + + @Test + fun `setEntryAndZero preserves native source semantics`() { + assertOne(methodName = "setEntryAndZero") + } + + @Test + fun `arrayEntryLiveLength preserves native source semantics`() { + assertOne(methodName = "arrayEntryLiveLength") + } + + @Test + fun `arrayKeysAndHoles preserves native source semantics`() { + assertOne(methodName = "arrayKeysAndHoles") + } + + @Test + fun `arrayMap preserves native source semantics`() { + assertOne(methodName = "arrayMap") + } + + @Test + fun `arrayMapMutation preserves native source semantics`() { + assertOne(methodName = "arrayMapMutation") + } + + @Test + fun `arrayForEachMutation preserves native source semantics`() { + assertOne(methodName = "arrayForEachMutation") + } + + @Test + fun `callbackThrows preserves native source semantics`() { + assertOne(methodName = "callbackThrows") + } + + @Test + fun `live iterator state remains independent across symbolic forks`() { + discoverProperties( + method = getMethod(methodName = "iteratorFork", className = "CollectionOperations"), + { branch, result -> branch.value && result.number == 1.0 }, + { branch, result -> !branch.value && result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 1.0 }), + ) + } + + @Test + fun `Node confirms order mutation holes callbacks and errors`() { + val source = getResourcePath("/models/CollectionOperations.ts").readText() + val assertions = methods.joinToString(separator = "\n") { name -> + "if (CollectionOperations.$name() !== 1) throw Error('$name');" + } + + assertNodeReplay( + source = source + assertions + + "if (CollectionOperations.iteratorFork(true) !== 1 || " + + "CollectionOperations.iteratorFork(false) !== 1) throw Error('fork');", + directory = directory, + name = "native-collection-operations", + timeoutMessage = "Native collection operation regression timed out", + ) + } + + @Test + fun `non-undefined callback thisArg stays an explicit residual boundary`() { + val method = getMethod(methodName = "unsupportedThisArg", className = "CollectionOperations") + + val outcome = TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> + machine.analyzeWithMetadata(methods = listOf(method)) + } + + assertTrue(outcome.unsupportedCall) + assertTrue(outcome.states.isEmpty()) + assertTrue(!outcome.engineFailed) + } + + @Test + fun `callbacks receive undefined this without a thisArg`() { + assertOne(methodName = "callbackWithoutThis") + } + + @Test + fun `shadowed Array from executes the user function`() { + assertOne(methodName = "shadowedArrayFrom") + } + + @Test + fun `implicit Set iteration executes the selected iterator model`() { + assertOne(methodName = "implicitCollectionIteration") + } + + @Test + fun `previous catalog cannot silently execute the new operations`() { + val newIds = setOf( + "ts.array.map", "ts.array.forEach", "ts.array.fromIterable", "ts.map.fromIterable", "ts.set.fromIterable", + "ts.iterator.keys", "ts.iterator.values", "ts.iterator.entries", "ts.iterator.collection", + ) + val baselineIds = TsBuiltInUnknownCallModels.catalog().modelIds.toSet() - newIds + val baselineOptions = tsOptions.copy(unknownCallModelSelection = TsUnknownCallModelSelection.Only(baselineIds)) + val names = listOf( + "iterableSet", + "arrayMap", + "arrayFromKeys", + "arrayEntryLiveLength", + "implicitCollectionIteration", + ) + for (name in names) { + val method = getMethod(methodName = name, className = "CollectionOperations") + + val outcome = TsMachine(scene = scene, options = options, tsOptions = baselineOptions).use { machine -> + machine.analyzeWithMetadata(methods = listOf(method)) + } + + assertTrue(outcome.states.isEmpty(), name) + assertTrue(!outcome.engineFailed, name) + } + } + + private fun assertOne(methodName: String) { + discoverProperties( + method = getMethod(methodName = methodName, className = "CollectionOperations"), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/MapSetModelsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/MapSetModelsTest.kt index a2a0e70496..fb359b2d0c 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/MapSetModelsTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/MapSetModelsTest.kt @@ -172,8 +172,8 @@ class MapSetModelsTest : TsMethodTestRunner() { } @Test - fun `unimplemented iterable input and capacity overflow stay explicit residual paths`() { - for (name in listOf("iterableConstructor", "capacityBoundary")) { + fun `capacity overflow stays an explicit residual path`() { + for (name in listOf("capacityBoundary")) { val method = getMethod(methodName = name, className = "MapSetModels") val outcome = TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> machine.analyzeWithMetadata(methods = listOf(method)) diff --git a/usvm-ts/src/test/resources/models/CollectionOperations.ts b/usvm-ts/src/test/resources/models/CollectionOperations.ts new file mode 100644 index 0000000000..5547c9fa63 --- /dev/null +++ b/usvm-ts/src/test/resources/models/CollectionOperations.ts @@ -0,0 +1,177 @@ +export class CollectionOperations { + static iterableSet(): number { + const set = new Set([7, 7, -0, 0, NaN, NaN]); + const values = [...set]; + return set.size === 3 && values[0] === 7 && 1 / values[1] === Infinity && values[2] !== values[2] ? 1 : 0; + } + + static iterableMap(): number { + const map = new Map([['a', 1], ['b', 2], ['a', 3]]); + const entries = [...map]; + return map.size === 2 && entries[0][0] === 'a' && entries[0][1] === 3 + && entries[1][0] === 'b' && entries[1][1] === 2 ? 1 : 0; + } + + static mapInvalidEntry(): number { + try { + new Map([1] as any); + return 0; + } catch (error) { + return error.name === 'TypeError' ? 1 : 0; + } + } + + static copyCollections(): number { + const source = new Map(); + source.set('a', 3).set('b', 5); + const copy = new Map(source); + source.set('a', 7); + const values = new Set(copy.values()); + return copy.get('a') === 3 && values.size === 2 && values.has(3) && values.has(5) ? 1 : 0; + } + + static arrayFromKeys(): number { + const map = new Map(); + map.set('a', 3).set('b', 5); + const keys = Array.from(map.keys()); + return keys.length === 2 && keys[0] === 'a' && keys[1] === 'b' ? 1 : 0; + } + + static liveMapIterator(): number { + const map = new Map(); + map.set(1, 11).set(2, 22).set(3, 33); + const iterator = map.entries(); + const first = iterator.next().value; + map.delete(2); + map.set(3, 44).set(1, 55).set(2, 66); + const second = iterator.next().value; + const third = iterator.next().value; + const done = iterator.next().done; + map.set(4, 77); + return first[0] === 1 && first[1] === 11 && second[0] === 3 && second[1] === 44 + && third[0] === 2 && third[1] === 66 && done && iterator.next().done ? 1 : 0; + } + + static clearDuringIteration(): number { + const set = new Set(); + set.add(1).add(2); + const iterator = set.values(); + const first = iterator.next().value; + set.clear(); + set.add(3); + const second = iterator.next().value; + return first === 1 && second === 3 && iterator.next().done ? 1 : 0; + } + + static setEntryAndZero(): number { + const set = new Set(); + set.add(-0).add(-0); + const iterator = set.entries(); + const entry = iterator.next().value; + return 1 / entry[0] === Infinity && 1 / entry[1] === Infinity && iterator.next().done ? 1 : 0; + } + + static arrayEntryLiveLength(): number { + const array = [3, 5]; + const iterator = array.entries(); + const first = iterator.next().value; + array[1] = 7; + array.push(9); + const second = iterator.next().value; + const third = iterator.next().value; + const done = iterator.next().done; + array.push(11); + return first[0] === 0 && first[1] === 3 && second[0] === 1 && second[1] === 7 + && third[0] === 2 && third[1] === 9 && done && iterator.next().done ? 1 : 0; + } + + static arrayKeysAndHoles(): number { + const array = [3, 5]; + delete array[0]; + const keys = [...array.keys()]; + const values = [...array.values()]; + return keys.length === 2 && keys[0] === 0 && keys[1] === 1 + && values[0] === undefined && values[1] === 5 ? 1 : 0; + } + + static arrayMap(): number { + const array = [3, 5]; + const result = array.map((value, index, receiver) => value + index + (receiver === array ? 1 : 100)); + return result.length === 2 && result[0] === 4 && result[1] === 7 ? 1 : 0; + } + + static arrayMapMutation(): number { + const array = [3, 5, 7]; + const counter = { value: 0 }; + const result = array.map((value, index) => { + counter.value++; + if (index === 0) { + delete array[1]; + array.push(9); + } + return value * 2; + }); + const observed = { calls: 0 }; + result.forEach(() => { observed.calls++; }); + return counter.value === 2 && result.length === 3 && result[0] === 6 + && result[2] === 14 && observed.calls === 2 ? 1 : 0; + } + + static arrayForEachMutation(): number { + const array = [3, 5, 7]; + const counter = { value: 0 }; + const result = array.forEach((value, index, receiver) => { + counter.value += value + index; + if (index === 0) receiver.length = 1; + }); + return result === undefined && counter.value === 3 ? 1 : 0; + } + + static callbackThrows(): number { + const counter = { value: 0 }; + try { + [3, 5].forEach((value) => { + counter.value += value; + throw 7; + }); + return 0; + } catch (error) { + return error === 7 && counter.value === 3 ? 1 : 0; + } + } + + static iteratorFork(remove: boolean): number { + const set = new Set(); + set.add(3).add(5); + const iterator = set.values(); + const first = iterator.next().value; + if (remove) set.delete(5); + const second = iterator.next(); + return first === 3 && (remove ? second.done : !second.done && second.value === 5) ? 1 : 0; + } + + static implicitCollectionIteration(): number { + const set = new Set(); + set.add(3); + let sum = 0; + for (const value of set) sum += value; + return sum === 3 ? 1 : 0; + } + + static callbackWithoutThis(): number { + const result = [3].map(function (this: void, value) { + return this === undefined ? value + 1 : 100; + }); + return result[0] === 4 ? 1 : 0; + } + + static shadowedArrayFrom(): number { + const Array = { from: (value: any) => 7 }; + return Array.from([]) === 7 ? 1 : 0; + } + + static unsupportedThisArg(): number { + [3].forEach(function () {}, {}); + return 1; + } +}