diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt index 5255f494d8..1dce219a9e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsUnknownCallModelDispatcher.kt @@ -6,6 +6,7 @@ import org.usvm.api.makeFreshUnknownCallResult import org.usvm.api.setMockMethodCallResult import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.call.intrinsic.TsDateEtsIrModelFamily +import org.usvm.machine.expr.invalidateCollectionAfterResidual import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState @@ -76,6 +77,7 @@ class TsModelUnknownCallDispatcher( TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN -> { val result = makeFreshUnknownCallResult(scope, call) ?: return TsUnknownCallOutcome.PATH_STOPPED scope.doWithState { + invalidateCollectionAfterResidual(call) setMockMethodCallResult(call.callee, result) newStmt(call.callSite) } @@ -134,6 +136,7 @@ class TsModelUnknownCallDispatcher( if (residualGuard != null && residualPolicy == TsResidualCallPolicy.FRESH_SYMBOLIC_RETURN) { guardedStateChanges += residualGuard to { + invalidateCollectionAfterResidual(call) setMockMethodCallResult(call.callee, requireNotNull(freshResidualResult)) newStmt(call.callSite) freshResidualApplied = true 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 new file mode 100644 index 0000000000..c7a0544335 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsCollectionModelFamily.kt @@ -0,0 +1,159 @@ +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.collectionGet +import org.usvm.machine.expr.collectionInsert +import org.usvm.machine.expr.collectionMatches +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. */ +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"), + OperationModel(operation = "has"), + OperationModel(operation = "delete"), + 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) + + 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 mapOnly = operation == "get" || operation == "set" + if (mapOnly && collection.kind != TsCollectionKind.MAP) return null + if (operation == "add" && collection.kind != TsCollectionKind.SET) return null + val arguments = call.arguments.map { it.resolved ?: return null } + if (operation == "clear") { + val successor = TsUnknownCallModelSuccessor( + guard = trueExpr, + completion = TsUnknownCallModelCompletion.Normal { ctx.mkUndefinedValue() }, + applyStateChanges = { + modeledCollections += receiver to newModeledCollection(kind = collection.kind) + }, + ) + return TsUnknownCallModelExecution(successors = listOf(successor)) + } + val key = state.collectionValue(arguments.firstOrNull() ?: mkUndefinedValue()) + val matches = state.collectionMatches(collection, key) ?: return null + val found = mkOr(matches.map { it.guard }) + val missing = mkNot(found) + when (operation) { + "has" -> { + val successor = TsUnknownCallModelSuccessor( + guard = trueExpr, + completion = TsUnknownCallModelCompletion.Normal { found }, + ) + TsUnknownCallModelExecution(successors = listOf(successor)) + } + "get" -> { + var result = state.collectionUndefined() + for (match in matches) { + result = iteUnresolvedValue(match.guard, state.collectionGet(collection, match.key), result) + } + val completion = TsUnknownCallModelCompletion.Unresolved(result) + val successor = TsUnknownCallModelSuccessor(guard = trueExpr, completion = completion) + TsUnknownCallModelExecution(successors = listOf(successor)) + } + "delete" -> { + val successors = matches.map { match -> + TsUnknownCallModelSuccessor( + guard = match.guard, + completion = TsUnknownCallModelCompletion.Normal { ctx.trueExpr }, + applyStateChanges = { collectionRemove(receiver, collection, match.key) }, + ) + } + TsUnknownCallModelSuccessor( + guard = missing, + completion = TsUnknownCallModelCompletion.Normal { ctx.falseExpr }, + ) + TsUnknownCallModelExecution(successors) + } + "set", "add" -> { + val value = if (operation == "add") { + key + } else { + state.collectionValue(arguments.getOrNull(1) ?: mkUndefinedValue()) + } + val successors = matches.map { match -> + TsUnknownCallModelSuccessor( + guard = match.guard, + completion = TsUnknownCallModelCompletion.Normal { receiver }, + applyStateChanges = { collectionPut(collection, match.key, value) }, + ) + }.toMutableList() + val canInsert = collection.keys.size < MAX_ENTRIES + if (canInsert) { + successors += TsUnknownCallModelSuccessor( + guard = missing, + completion = TsUnknownCallModelCompletion.Normal { receiver }, + applyStateChanges = { collectionInsert(receiver, collection, key, value) }, + ) + } + if (successors.isEmpty()) return null + TsUnknownCallModelExecution( + successors = successors, + residualGuard = if (canInsert || missing.isFalse) null else missing, + ) + } + else -> error("Unexpected collection operation: $operation") + } + } + } +} 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 new file mode 100644 index 0000000000..8f8d8b0117 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCollectionStorage.kt @@ -0,0 +1,219 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import io.ksmt.utils.cast +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsStringType +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.UIteExpr +import org.usvm.api.collection.ObjectMapCollectionApi.mkSymbolicObjectMap +import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapContains +import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapGet +import org.usvm.api.collection.ObjectMapCollectionApi.symbolicObjectMapPut +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.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.util.mkStringBackingElementLValue +import org.usvm.util.mkStringBackingLValue +import org.usvm.util.mkStringBackingLengthLValue + +internal enum class TsCollectionKind { MAP, SET } + +/** Native object identity and symbolic backend are shared by all aliases and cloned with the state. */ +internal data class TsModeledCollection( + val kind: TsCollectionKind, + val storage: UConcreteHeapRef, + val keys: List = emptyList(), +) + +internal data class TsCollectionMatch(val key: UConcreteHeapRef, val guard: UBoolExpr) + +private enum class CollectionPayload { BOOLEAN, NUMBER, REFERENCE, IS_BOOLEAN, IS_NUMBER, IS_REFERENCE } +private val storageType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%CollectionStorage")) +private val payloadType = EtsClassType(EtsClassSignature.UNKNOWN.copy(name = "%CollectionPayload")) + +internal fun TsState.newModeledCollection(kind: TsCollectionKind) = TsModeledCollection( + kind = kind, + storage = mkSymbolicObjectMap(mapType = storageType).asExpr(ctx.addressSort) as UConcreteHeapRef, +) + +internal fun TsState.collectionValue(value: UExpr<*>): TsUnresolvedValue = with(ctx) { + val (boolean, isBoolean) = extractValue(value, boolSort, ::getIntermediateBoolLValue) + val (number, isNumber) = extractValue(value, fp64Sort, ::getIntermediateFpLValue) + val (reference, isReference) = extractValue(value, addressSort, ::getIntermediateRefLValue) + TsUnresolvedValue( + boolValue = boolean ?: falseExpr, + fpValue = number ?: mkFp64(0.0), + refValue = reference ?: mkUndefinedValue(), + type = EtsFakeType(isBoolean, isNumber, isReference), + ) +} + +internal fun TsState.collectionUndefined(): TsUnresolvedValue = collectionValue(ctx.mkUndefinedValue()) + +internal fun TsState.collectionMatches( + collection: TsModeledCollection, + value: TsUnresolvedValue, +): List? = with(ctx) { + val matches = mutableListOf() + var unmatched: UBoolExpr = trueExpr + for (key in collection.keys) { + val present = symbolicObjectMapContains(collection.storage, key, storageType) + if (present.isFalse) continue + + val equal = collectionKeyEquals(readCollectionPayload(key), value) ?: return null + val selected = mkAnd(unmatched, present, equal) + if (!selected.isFalse) matches += TsCollectionMatch(key = key, guard = selected) + unmatched = mkAnd(unmatched, mkNot(mkAnd(present, equal))) + } + matches +} + +internal fun TsState.collectionGet(collection: TsModeledCollection, key: UConcreteHeapRef): TsUnresolvedValue { + val value = symbolicObjectMapGet(collection.storage, key, storageType, ctx.addressSort) + return readCollectionPayload(value) +} + +internal fun TsState.collectionPut( + collection: TsModeledCollection, + key: UConcreteHeapRef, + value: TsUnresolvedValue, +) { + val payload = allocateCollectionPayload(value) + symbolicObjectMapPut(collection.storage, key, payload, storageType, ctx.addressSort) +} + +internal fun TsState.collectionInsert( + receiver: UConcreteHeapRef, + collection: TsModeledCollection, + key: TsUnresolvedValue, + value: TsUnresolvedValue, +) = with(ctx) { + // SameValueZero stores either sign of numeric zero as positive zero. + 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) +} + +internal fun TsState.collectionRemove( + receiver: UConcreteHeapRef, + collection: TsModeledCollection, + key: UConcreteHeapRef, +) { + symbolicObjectMapRemove(collection.storage, key, storageType) + modeledCollections += receiver to collection.copy(keys = collection.keys - key) +} + +internal fun TsState.collectionSize(collection: TsModeledCollection): UExpr<*> = with(ctx) { + val size = symbolicObjectMapSize(collection.storage, storageType) + mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = size.cast(), + signed = true, + ) +} + +/** A residual mutation must not leave later precise model calls observing an obsolete backend. */ +internal fun TsState.invalidateCollectionAfterResidual(call: TsUnknownCall) { + val receiver = call.receiver?.resolved as? UConcreteHeapRef ?: return + if (receiver !in modeledCollections) return + val readonlyOperation = call.callee.name in setOf("get", "has", "keys", "values", "entries") + if (readonlyOperation) return + + modeledCollections -= receiver +} + +private fun TsState.allocateCollectionPayload(value: TsUnresolvedValue): UConcreteHeapRef = with(ctx) { + val ref = memory.allocConcrete(payloadType) + memory.write(UFieldLValue(boolSort, ref, CollectionPayload.BOOLEAN), value.boolValue, trueExpr) + memory.write(UFieldLValue(fp64Sort, ref, CollectionPayload.NUMBER), value.fpValue, trueExpr) + memory.write(UFieldLValue(addressSort, ref, CollectionPayload.REFERENCE), value.refValue, trueExpr) + memory.write(UFieldLValue(boolSort, ref, CollectionPayload.IS_BOOLEAN), value.type.boolTypeExpr, trueExpr) + memory.write(UFieldLValue(boolSort, ref, CollectionPayload.IS_NUMBER), value.type.fpTypeExpr, trueExpr) + memory.write(UFieldLValue(boolSort, ref, CollectionPayload.IS_REFERENCE), value.type.refTypeExpr, trueExpr) + ref +} + +private 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)) + val isBoolean = memory.read(UFieldLValue(boolSort, ref, CollectionPayload.IS_BOOLEAN)) + val isNumber = memory.read(UFieldLValue(boolSort, ref, CollectionPayload.IS_NUMBER)) + val isReference = memory.read(UFieldLValue(boolSort, ref, CollectionPayload.IS_REFERENCE)) + val type = EtsFakeType(boolTypeExpr = isBoolean, fpTypeExpr = isNumber, refTypeExpr = isReference) + + TsUnresolvedValue(boolValue = boolean, fpValue = number, refValue = reference, type = type) +} + +private 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) + val bothNaN = mkAnd(leftIsNaN, rightIsNaN) + val sameNumber = mkFpEqualExpr(left.fpValue, right.fpValue) + val sameNumberKey = mkOr(sameNumber, bothNaN) + val numberEqual = mkAnd( + left.type.fpTypeExpr, + right.type.fpTypeExpr, + sameNumberKey, + ) + val bothReferences = mkAnd(left.type.refTypeExpr, right.type.refTypeExpr) + val referenceEqual = if (bothReferences.isFalse) { + falseExpr + } else { + referenceOrStringKeyEquals(left.refValue, right.refValue) ?: return null + } + val referencesEqual = mkAnd(bothReferences, referenceEqual) + mkOr(booleanEqual, numberEqual, referencesEqual) +} + +private fun TsState.referenceOrStringKeyEquals(left: UHeapRef, right: UHeapRef): UBoolExpr? = with(ctx) { + val sameReference = mkHeapRefEq(left, right) + if (sameReference.isTrue) return trueExpr + val leftIsString = memory.types.evalTypeEquals(left, EtsStringType) + val rightIsString = memory.types.evalTypeEquals(right, EtsStringType) + if (leftIsString.isFalse || rightIsString.isFalse) return sameReference + + val leftConstant = (left as? UConcreteHeapRef)?.let(::getStringConstantValue) + val rightConstant = (right as? UConcreteHeapRef)?.let(::getStringConstantValue) + if (leftConstant != null && rightConstant != null) return mkBool(leftConstant == rightConstant) + val leftBound = modeledStringBound(left) ?: return null + val rightBound = modeledStringBound(right) ?: return null + val leftChars = memory.read(mkStringBackingLValue(left)) + val rightChars = memory.read(mkStringBackingLValue(right)) + val leftLength = memory.read(mkStringBackingLengthLValue(leftChars)) + val rightLength = memory.read(mkStringBackingLengthLValue(rightChars)) + val charactersEqual = (0 until maxOf(leftBound, rightBound)).map { index -> + val position = mkBv(index) + val leftCharacter = memory.read(mkStringBackingElementLValue(leftChars, position)) + val rightCharacter = memory.read(mkStringBackingElementLValue(rightChars, position)) + mkImplies(mkBvSignedLessExpr(position, leftLength), mkEq(leftCharacter, rightCharacter)) + } + val stringsEqual = mkAnd(leftIsString, rightIsString, mkEq(leftLength, rightLength), mkAnd(charactersEqual)) + mkOr(sameReference, stringsEqual) +} + +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 UIteExpr<*>) return null + val trueBound = modeledStringBound(ref.trueBranch.asExpr(addressSort)) ?: return null + val falseBound = modeledStringBound(ref.falseBranch.asExpr(addressSort)) ?: return null + maxOf(trueBound, falseBound) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsIntrinsicFieldResult.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsIntrinsicFieldResult.kt index 47f9581a6c..6c7b0f51f4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsIntrinsicFieldResult.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsIntrinsicFieldResult.kt @@ -27,6 +27,14 @@ internal fun TsContext.tryReadIntrinsicField( instance: UHeapRef, field: EtsFieldSignature, ): TsIntrinsicFieldResult> { + val collection = (instance as? UConcreteHeapRef)?.let { ref -> + scope.calcOnState { modeledCollections[ref] } + } + if (collection != null && field.name == "size") { + val size = scope.calcOnState { collectionSize(collection) } + return TsIntrinsicFieldResult.Handled(size) + } + val regularExpression = intrinsicRegExpReference(scope, instance) if (regularExpression != null) { return TsIntrinsicFieldResult.from(readRegExpField(scope, regularExpression, field.name)) @@ -51,6 +59,14 @@ internal fun TsContext.tryWriteIntrinsicField( field: EtsFieldSignature, value: UExpr<*>, ): TsIntrinsicFieldResult { + val collection = (instance as? UConcreteHeapRef)?.let { ref -> + scope.calcOnState { modeledCollections[ref] } + } + if (collection != null && field.name == "size") { + scope.doWithState { terminateAsUnsupported(reason = "Writing native collection size is not modeled") } + return TsIntrinsicFieldResult.Stopped + } + val nativeMathConstant = scope.calcOnState { isNativeMathConstant(instance, field.name) } if (nativeMathConstant) { scope.doWithState { 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 a764a51afc..59b86472a7 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 @@ -33,6 +33,7 @@ import org.usvm.machine.expr.TrackedObjectProperty import org.usvm.machine.expr.TsArrayIterator import org.usvm.machine.expr.TsCapturedInstanceCall import org.usvm.machine.expr.TsIteratorResult +import org.usvm.machine.expr.TsModeledCollection import org.usvm.machine.expr.TsStringIterator import org.usvm.machine.interpreter.PromiseCallback import org.usvm.machine.interpreter.PromiseState @@ -148,6 +149,7 @@ class TsState( ) { internal var promiseExecutorFunctions: Map = emptyMap() + internal var modeledCollections: Map = emptyMap() internal var initialEnvironmentFailure: String? = null internal var initialEnvironmentHeaps: Map = emptyMap() internal var initialEnvironmentSlots: Map, TsInitialEnvironmentSlot> = emptyMap() @@ -417,6 +419,7 @@ class TsState( denseInputArrays = denseInputArrays.toMutableMap(), activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ).also { cloned -> + cloned.modeledCollections = modeledCollections cloned.promiseExecutorFunctions = promiseExecutorFunctions cloned.initialEnvironmentFailure = initialEnvironmentFailure cloned.initialEnvironmentHeaps = initialEnvironmentHeaps 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 17253ef33e..e05a73e8f8 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 @@ -205,7 +205,14 @@ class TsUnknownCallModelCatalogTest { TsArrayShiftIntrinsicModel.MODEL_ID, "ts.array.slice", "ts.array.unshift", + "ts.collection.add", + "ts.collection.clear", + "ts.collection.delete", + "ts.collection.get", + "ts.collection.has", + "ts.collection.set", TsErrorEtsIrModelFamily.CONSTRUCTOR_ID, + "ts.map.constructor", TsNumericIntrinsicModelFamily.MATH_ABS_ID, TsNumericIntrinsicModelFamily.MATH_CEIL_ID, TsNumericIntrinsicModelFamily.MATH_FLOOR_ID, @@ -220,6 +227,7 @@ class TsUnknownCallModelCatalogTest { TsNumericIntrinsicModelFamily.NUMBER_IS_NAN_ID, TsNumericIntrinsicModelFamily.NUMBER_IS_SAFE_INTEGER_ID, "ts.number.parseFloat", + "ts.set.constructor", "ts.string.charAt", "ts.string.charCodeAt", "ts.string.endsWith", 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 new file mode 100644 index 0000000000..a2a0e70496 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/MapSetModelsTest.kt @@ -0,0 +1,225 @@ +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 MapSetModelsTest : TsMethodTestRunner() { + override val scene = loadScene("/models/MapSetModels.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, + ) + } + + @Test + fun `mapOverwrite agrees with native collection semantics`() { + assertOne(methodName = "mapOverwrite") + } + + @Test + fun `mapMissingAndUndefined agrees with native collection semantics`() { + assertOne(methodName = "mapMissingAndUndefined") + } + + @Test + fun `mapSameValueZero agrees with native collection semantics`() { + assertOne(methodName = "mapSameValueZero") + } + + @Test + fun `mapObjectIdentity agrees with native collection semantics`() { + assertOne(methodName = "mapObjectIdentity") + } + + @Test + fun `mapDeleteAndReinsert agrees with native collection semantics`() { + assertOne(methodName = "mapDeleteAndReinsert") + } + + @Test + fun `mapClear agrees with native collection semantics`() { + assertOne(methodName = "mapClear") + } + + @Test + fun `mapKindsRemainDistinct agrees with native collection semantics`() { + assertOne(methodName = "mapKindsRemainDistinct") + } + + @Test + fun `setSameValueZero agrees with native collection semantics`() { + assertOne(methodName = "setSameValueZero") + } + + @Test + fun `setMissing agrees with native collection semantics`() { + assertOne(methodName = "setMissing") + } + + @Test + fun `setDeleteAndClear agrees with native collection semantics`() { + assertOne(methodName = "setDeleteAndClear") + } + + @Test + fun `nullishConstructors agrees with native collection semantics`() { + assertOne(methodName = "nullishConstructors") + } + + @Test + fun `symbolic number keys preserve conditional equality and state forks`() { + for (name in listOf("mapSymbolicKeys", "setSymbolicKeys")) { + discoverProperties( + method = getMethod(methodName = name, className = "MapSetModels"), + { left, right, result -> left.number == right.number && result.number == 1.0 }, + { left, right, result -> left.number != right.number && result.number == 1.0 }, + invariants = arrayOf({ _, _, result -> result.number == 1.0 }), + ) + } + } + + @Test + fun `symbolic string keys compare contents instead of heap identity`() { + discoverProperties( + method = getMethod(methodName = "mapStringContents", className = "MapSetModels"), + { left, right, result -> left.value == right.value && result.number == 1.0 }, + { left, right, result -> left.value != right.value && result.number == 1.0 }, + invariants = arrayOf({ _, _, result -> result.number == 1.0 }), + ) + } + + @Test + fun `conditional deletion does not leak between state forks`() { + discoverProperties( + method = getMethod(methodName = "mapConditional", className = "MapSetModels"), + { 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 `native collections confirm concrete boundary and symbolic representatives`() { + val source = getResourcePath("/models/MapSetModels.ts").readText() + val methods = listOf( + "mapOverwrite", + "mapMissingAndUndefined", + "mapSameValueZero", + "mapObjectIdentity", + "mapDeleteAndReinsert", + "mapClear", + "mapKindsRemainDistinct", + "setSameValueZero", + "setMissing", + "setDeleteAndClear", + "nullishConstructors", + ) + val concrete = methods.joinToString(separator = "\n") { name -> + "if (MapSetModels.$name() !== 1) throw Error('$name');" + } + val representatives = """ + for (const left of [0, -0, NaN, 7, 19]) { + for (const right of [0, -0, NaN, 7, 19]) { + if (MapSetModels.mapSymbolicKeys(left, right) !== 1) throw Error('map keys'); + if (MapSetModels.setSymbolicKeys(left, right) !== 1) throw Error('set keys'); + } + } + for (const left of ['', 'a', 'ab']) for (const right of ['', 'a', 'ab']) { + if (MapSetModels.mapStringContents(left, right) !== 1) throw Error('string keys'); + } + if (MapSetModels.mapConditional(true) !== 1 || MapSetModels.mapConditional(false) !== 1) { + throw Error('state fork'); + } + """.trimIndent() + + assertNodeReplay( + source = source + concrete + representatives, + directory = directory, + name = "native-map-set-models", + timeoutMessage = "Native collection regression timed out", + ) + } + + @Test + fun `unimplemented iterable input and capacity overflow stay explicit residual paths`() { + for (name in listOf("iterableConstructor", "capacityBoundary")) { + val method = getMethod(methodName = name, className = "MapSetModels") + val outcome = TsMachine(scene = scene, options = options, tsOptions = tsOptions).use { machine -> + machine.analyzeWithMetadata(methods = listOf(method)) + } + + assertTrue(outcome.unsupportedCall, name) + assertTrue(outcome.states.isEmpty(), name) + assertTrue(!outcome.engineFailed, name) + } + } + + @Test + fun `explicit old catalog excludes collection semantics`() { + val oldIds = TsBuiltInUnknownCallModels.catalog().modelIds.filterNot { id -> + id.startsWith("ts.collection.") || id == "ts.map.constructor" || id == "ts.set.constructor" + }.toSet() + val baselineOptions = tsOptions.copy(unknownCallModelSelection = TsUnknownCallModelSelection.Only(oldIds)) + val method = getMethod(methodName = "mapOverwrite", className = "MapSetModels") + + val outcome = TsMachine(scene = scene, options = options, tsOptions = baselineOptions).use { machine -> + machine.analyzeWithMetadata(methods = listOf(method)) + } + + assertTrue(outcome.unsupportedCall) + assertTrue(outcome.states.isEmpty()) + assertTrue(!outcome.engineFailed) + } + + @Test + fun `source generator yield delegation is unsupported rather than an engine error`() { + val method = getMethod(methodName = "delegatedYield", className = "MapSetModels") + val collectingOptions = options.copy(throwExceptionOnStepFailure = false) + val outcome = TsMachine(scene = scene, options = collectingOptions, tsOptions = tsOptions).use { machine -> + machine.analyzeWithMetadata(methods = listOf(method)) + } + + assertTrue(!outcome.engineFailed) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.unsupportedPaths.any { it.contains("Not supported") }) + } + + private fun assertOne(methodName: String) { + discoverProperties( + method = getMethod(methodName = methodName, className = "MapSetModels"), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } +} diff --git a/usvm-ts/src/test/resources/models/MapSetModels.ts b/usvm-ts/src/test/resources/models/MapSetModels.ts new file mode 100644 index 0000000000..62efe820f7 --- /dev/null +++ b/usvm-ts/src/test/resources/models/MapSetModels.ts @@ -0,0 +1,137 @@ +export class MapSetModels { + static mapOverwrite(): number { + const map = new Map(); + const alias = map; + const chained = map.set('key', 7); + alias.set('key', 19); + return chained === map && map.size === 1 && map.get('key') === 19 ? 1 : 0; + } + + static mapMissingAndUndefined(): number { + const map = new Map(); + (map as any).set(); + return map.size === 1 && (map as any).has() && (map as any).get() === undefined + && !map.has('missing') && map.get('missing') === undefined ? 1 : 0; + } + + static mapSameValueZero(): number { + const map = new Map(); + map.set(NaN, 7); + map.set(0 / 0, 19); + map.set(-0, 23); + map.set(0, 29); + return map.size === 2 && map.get(NaN) === 19 && map.get(-0) === 29 ? 1 : 0; + } + + static mapObjectIdentity(): number { + const first = { value: 1 }; + const second = { value: 1 }; + const map = new Map(); + map.set(first, 17); + map.set(second, 19); + return map.size === 2 && map.get(first) === 17 && map.get(second) === 19 ? 1 : 0; + } + + static mapStringContents(left: string, right: string): number { + const map = new Map(); + map.set(left, 17); + map.set(right, 19); + return map.get(left) === (left === right ? 19 : 17) ? 1 : 0; + } + + static mapSymbolicKeys(left: number, right: number): number { + const map = new Map(); + map.set(left, 17); + map.set(right, 19); + const same = left === right || (left !== left && right !== right); + return map.get(left) === (same ? 19 : 17) ? 1 : 0; + } + + static mapDeleteAndReinsert(): number { + const map = new Map(); + map.set(7, 17); + const first = map.delete(7); + const second = map.delete(7); + map.set(7, 19); + return first && !second && map.size === 1 && map.get(7) === 19 ? 1 : 0; + } + + static mapClear(): number { + const map = new Map(); + const alias = map; + map.set('key', 17); + const result = alias.clear(); + return result === undefined && map.size === 0 && !map.has('key') ? 1 : 0; + } + + static mapConditional(branch: boolean): number { + const map = new Map(); + map.set('key', 17); + if (branch) map.delete('key'); + else map.set('key', 19); + if (branch) return !map.has('key') && map.size === 0 ? 1 : 0; + return map.get('key') === 19 && map.size === 1 ? 1 : 0; + } + + static mapKindsRemainDistinct(): number { + const map = new Map(); + map.set(0, 17); + map.set(false, 19); + map.set('0', 23); + map.set(null, 29); + map.set(undefined, 31); + return map.size === 5 && map.get(0) === 17 && map.get(false) === 19 + && map.get('0') === 23 && map.get(null) === 29 && map.get(undefined) === 31 ? 1 : 0; + } + + static setSameValueZero(): number { + const set = new Set(); + const chained = set.add(NaN).add(0 / 0).add(-0).add(0); + return chained === set && set.size === 2 && set.has(NaN) && set.has(0) ? 1 : 0; + } + + static setMissing(): number { + const set = new Set(); + (set as any).add(); + return set.size === 1 && set.has(undefined) && !set.has(null) ? 1 : 0; + } + + static setDeleteAndClear(): number { + const set = new Set(); + const alias = set; + set.add('first').add('second'); + const first = alias.delete('first'); + const second = alias.delete('first'); + alias.clear(); + set.add('third'); + return first && !second && set.size === 1 && set.has('third') && !set.has('second') ? 1 : 0; + } + + static setSymbolicKeys(left: number, right: number): number { + const set = new Set(); + set.add(left).add(right); + const same = left === right || (left !== left && right !== right); + return set.has(left) && set.has(right) && set.size === (same ? 1 : 2) ? 1 : 0; + } + + static nullishConstructors(): number { + const map = new Map(null as any); + const set = new Set(undefined); + return map.size === 0 && set.size === 0 ? 1 : 0; + } + static iterableConstructor(): number { + const set = new Set([7, 19]); + return set.size; + } + + static capacityBoundary(): number { + const set = new Set(); + for (let key = 0; key < 17; key++) set.add(key); + return set.size; + } + + static *delegatedYield(): IterableIterator { + yield* [1]; + } + +}