diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt index e060ff41f8..738278bbe9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayShiftIntrinsicModel.kt @@ -5,6 +5,7 @@ import org.jacodb.ets.model.EtsArrayType import org.usvm.UAddressSort import org.usvm.UExpr import org.usvm.USort +import org.usvm.isFalse import org.usvm.machine.TsSizeSort import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.call.TsUnknownCallFailureReason @@ -17,8 +18,8 @@ import org.usvm.machine.state.TsState import org.usvm.machine.types.readUnresolvedArrayElement import org.usvm.util.arrayStorageType import org.usvm.util.copyArrayElements -import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.readTypedArrayElement /** Engine intrinsic for `Array.shift`, whose bulk move is implemented by symbolic-memory `memcpy`. */ internal object TsArrayShiftIntrinsicModel : TsBuiltInUnknownCallModel { @@ -91,15 +92,12 @@ internal object TsArrayShiftIntrinsicModel : TsBuiltInUnknownCallModel { index: UExpr, ): TsUnknownCallModelCompletion = with(ctx) { if (input.elementSort !is TsUnresolvedSort) { - val firstElementLValue = mkArrayIndexLValue( - sort = input.elementSort, - ref = input.array, - index = index, - type = input.arrayType, - ) - val firstElement = memory.read(firstElementLValue) - - return@with TsUnknownCallModelCompletion.Normal { firstElement } + val element = readTypedArrayElement(input.array, index, input.arrayType) + return@with if (element.hasBoxedValue.isFalse) { + TsUnknownCallModelCompletion.Normal { element.nativeValue } + } else { + TsUnknownCallModelCompletion.Unresolved(element.unresolvedValue) + } } val firstElement = readUnresolvedArrayElement(memory, input.array, index) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumericIntrinsicModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumericIntrinsicModelFamily.kt index 948493f52d..af17e12e8a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumericIntrinsicModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsNumericIntrinsicModelFamily.kt @@ -209,6 +209,13 @@ private fun unaryMathCall( } val argument = call.arguments.firstOrNull()?.resolved ?: return state.normalExecution(state.ctx.mkFp(Double.NaN, state.ctx.fp64Sort)) + with(state.ctx) { + if (argument.isFakeObject()) { + val numberGuard = argument.getFakeType(state.memory).fpTypeExpr + val result = operation(argument.extractFp(state.memory)) + return state.normalExecution(result, guard = numberGuard) + } + } if (argument.sort != state.ctx.fp64Sort) { return null } @@ -244,13 +251,19 @@ private fun TsUnknownCall.hasGlobalOwner(expectedName: String): Boolean { return hasBuiltinGlobalOwner(owner = owner, callee = callee, expectedName = expectedName) } -private fun TsState.normalExecution(result: UExpr<*>): TsUnknownCallModelExecution = with(ctx) { +private fun TsState.normalExecution( + result: UExpr<*>, + guard: UBoolExpr = ctx.trueExpr, +): TsUnknownCallModelExecution = with(ctx) { val successor = TsUnknownCallModelSuccessor( - guard = trueExpr, + guard = guard, completion = TsUnknownCallModelCompletion.Normal { result }, ) - TsUnknownCallModelExecution(successors = listOf(successor)) + TsUnknownCallModelExecution( + successors = listOf(successor), + residualGuard = guard.takeUnless { it == trueExpr }?.let(::mkNot), + ) } private fun TsState.isInteger(value: UExpr) = with(ctx) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index c5bc2d329c..41d028beb7 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -21,6 +21,7 @@ import org.usvm.api.memcpy import org.usvm.api.readArrayIndex import org.usvm.getIntValue import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.isFalse import org.usvm.machine.TsSizeSort import org.usvm.machine.TsVirtualMethodCallStmt import org.usvm.machine.call.TsUnknownCallFailureReason @@ -43,12 +44,29 @@ import org.usvm.util.arrayStorageType import org.usvm.util.copyArrayElements import org.usvm.util.forEachArrayPayloadRegion import org.usvm.util.initializeArrayKind -import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.readTypedArrayElement import org.usvm.util.resolveEtsMethods private val logger = KotlinLogging.logger {} +private val modeledStringMethods = setOf( + "substring", + "trim", + "trimStart", + "trimEnd", + "charAt", + "charCodeAt", + "endsWith", + "includes", + "indexOf", + "lastIndexOf", + "slice", + "startsWith", + "toLowerCase", + "toUpperCase", +) + internal fun TsExprResolver.tryApproximateGlobalInstanceCall( expr: EtsInstanceCallExpr, ): TsExprApproximationResult = with(ctx) { @@ -168,7 +186,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `Array.pop() method calls if (expr.callee.name == "pop") { - return handleArrayPopCall(stmt, instanceType, elementSort) + return handleArrayPopCall(stmt, instanceType) } // Handle `Array.fill() method calls @@ -183,7 +201,7 @@ internal fun TsExprResolver.tryApproximateInstanceCall( // Handle `Array.shift() method calls if (expr.callee.name == "shift") { - return handleArrayShiftCall(stmt, instanceType, elementSort) + return handleArrayShiftCall(stmt, instanceType) } // Handle `Array.join() method calls @@ -217,18 +235,6 @@ internal fun TsExprResolver.tryApproximateInstanceCall( } } - val modeledStringMethods = setOf( - "charAt", - "charCodeAt", - "endsWith", - "includes", - "indexOf", - "lastIndexOf", - "slice", - "startsWith", - "toLowerCase", - "toUpperCase", - ) if (instanceType is EtsStringType && expr.callee.name in modeledStringMethods) { val dispatcher = unknownCallDispatcher if (dispatcher !is TsUnknownCallModelDispatcher) { @@ -300,11 +306,10 @@ private fun EtsMethodSignature.withEnclosingClassName(name: String): EtsMethodSi private fun TsExprResolver.handleArrayPopCall( stmt: TsVirtualMethodCallStmt, instanceType: EtsArrayType, - elementSort: USort, ): TsExprApproximationResult { val dispatcher = unknownCallDispatcher if (dispatcher !is TsUnknownCallModelDispatcher) { - return from(handleArrayPop(stmt, instanceType, elementSort, stmt.instance.asExpr(ctx.addressSort))) + return from(handleArrayPop(stmt, instanceType, stmt.instance.asExpr(ctx.addressSort))) } dispatcher.dispatch( @@ -320,11 +325,10 @@ private fun TsExprResolver.handleArrayPopCall( private fun TsExprResolver.handleArrayShiftCall( stmt: TsVirtualMethodCallStmt, instanceType: EtsArrayType, - elementSort: USort, ): TsExprApproximationResult { val dispatcher = unknownCallDispatcher if (dispatcher !is TsUnknownCallModelDispatcher) { - return from(handleArrayShift(stmt, instanceType, elementSort, stmt.instance.asExpr(ctx.addressSort))) + return from(handleArrayShift(stmt, instanceType, stmt.instance.asExpr(ctx.addressSort))) } dispatcher.dispatch( @@ -546,23 +550,22 @@ private fun TsExprResolver.handleArrayPush( private fun TsExprResolver.handleArrayPop( stmt: TsVirtualMethodCallStmt, arrayType: EtsArrayType, - elementSort: USort, array: UHeapRef, ): UExpr<*>? = with(ctx) { check(stmt.args.isEmpty()) { "Array.pop() should have no arguments, but got ${stmt.args.size}" } - removeArrayElement(stmt, array, arrayType, elementSort, first = false) + removeArrayElement(stmt, array, arrayType, first = false) } private fun TsExprResolver.removeArrayElement( stmt: TsVirtualMethodCallStmt, array: UHeapRef, arrayType: EtsArrayType, - elementSort: USort, first: Boolean, ): UExpr<*>? = with(ctx) { + val storageSort = typeToSort(arrayType.elementType) val lengthLValue = mkArrayLengthLValue(array, arrayType) val length = scope.calcOnState { memory.read(lengthLValue) } val nonEmpty = mkNot(mkEq(length, mkBv(0))) @@ -577,10 +580,15 @@ private fun TsExprResolver.removeArrayElement( scope.calcOnState { val newLength = mkBvSubExpr(length, mkBv(1)) val index = if (first) mkBv(0) else newLength - val removed = if (typeToSort(arrayType.elementType) is TsUnresolvedSort) { + val removed = if (storageSort is TsUnresolvedSort) { mkFakeValue(scope, readUnresolvedArrayElement(memory, array, index)) } else { - memory.read(mkArrayIndexLValue(elementSort, array, index, arrayType)) + val element = readTypedArrayElement(array, index, arrayType) + if (element.hasBoxedValue.isFalse) { + element.nativeValue + } else { + mkFakeValue(scope, element.unresolvedValue) + } } if (first) { @@ -742,14 +750,13 @@ private const val ARRAY_FILL_MAX_SIZE = 10_000 private fun TsExprResolver.handleArrayShift( stmt: TsVirtualMethodCallStmt, arrayType: EtsArrayType, - elementSort: USort, array: UHeapRef, ): UExpr<*>? = with(ctx) { check(stmt.args.isEmpty()) { "Array.shift() should have no arguments, but got ${stmt.args.size}" } - removeArrayElement(stmt, array, arrayType, elementSort, first = true) + removeArrayElement(stmt, array, arrayType, first = true) } /** diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/EcmaScriptNumericConversions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/EcmaScriptNumericConversions.kt new file mode 100644 index 0000000000..0e29d51406 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/EcmaScriptNumericConversions.kt @@ -0,0 +1,163 @@ +package org.usvm.machine.expr + +import io.ksmt.expr.KFpRoundingMode +import io.ksmt.sort.KBvSort +import io.ksmt.sort.KFp64Sort +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.USort +import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.types.extractValue + +private const val UINT32_MODULUS = 4_294_967_296.0 +private const val UINT32_MAX_VALUE = 4_294_967_295.0 + +internal data class TsNumericArrayIndex( + val value: UExpr, + val isNumeric: UBoolExpr, + val hasUnsupportedReadKey: UBoolExpr, +) + +/** Classifies an index that may be wrapped with another runtime type. */ +internal fun TsContext.extractNumericArrayIndex( + scope: TsStepScope, + index: UExpr, +): TsNumericArrayIndex { + val runtimeValues = scope.calcOnState { + with(ctx) { + val (_, boolGuard) = extractValue(index, boolSort, ::getIntermediateBoolLValue) + val (fpValue, fpGuard) = extractValue(index, fp64Sort, ::getIntermediateFpLValue) + val (reference, refGuard) = extractValue(index, addressSort, ::getIntermediateRefLValue) + + IndexRuntimeValues( + boolTypeGuard = boolGuard, + numericValue = fpValue, + numericTypeGuard = fpGuard, + refValue = reference, + refTypeGuard = refGuard, + ) + } + } + val refIsKnownMissingKey = if (runtimeValues.refValue == null) { + falseExpr + } else { + val refIsNull = mkHeapRefEq(runtimeValues.refValue, mkTsNullValue()) + val refIsUndefined = mkHeapRefEq(runtimeValues.refValue, mkUndefinedValue()) + val refIsNullish = mkOr(refIsNull, refIsUndefined) + + mkAnd( + runtimeValues.refTypeGuard, + refIsNullish, + ) + } + val hasSupportedRuntimeType = mkOr( + runtimeValues.boolTypeGuard, + runtimeValues.numericTypeGuard, + refIsKnownMissingKey, + ) + + return TsNumericArrayIndex( + value = runtimeValues.numericValue ?: mkFp64(0.0), + isNumeric = runtimeValues.numericTypeGuard, + hasUnsupportedReadKey = mkNot(hasSupportedRuntimeType), + ) +} + +private data class IndexRuntimeValues( + val boolTypeGuard: UBoolExpr, + val numericValue: UExpr?, + val numericTypeGuard: UBoolExpr, + val refValue: UHeapRef?, + val refTypeGuard: UBoolExpr, +) + +/** ECMAScript ToUint32, represented as the common 32-bit bit pattern used by ToInt32. */ +internal fun TsContext.mkEcmaScriptToUint32(value: UExpr): UExpr = with(this) { + val zero = mkFp64(0.0) + val isFinite = mkAnd( + mkFpIsNaNExpr(value).not(), + mkFpIsInfiniteExpr(value).not(), + ) + val finiteValue = mkIte(isFinite, value, zero) + val towardZero = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardZero) + val integer = mkFpRoundToIntegralExpr( + roundingMode = towardZero, + value = finiteValue, + ) + val modulus = mkFp64(UINT32_MODULUS) + val remainder = mkFpRemExpr(integer, modulus) + val remainderIsNegative = mkFpLessExpr(remainder, zero) + val positiveRemainder = mkFpAddExpr(fpRoundingModeSortDefaultValue(), remainder, modulus) + val normalizedRemainder = mkIte( + condition = remainderIsNegative, + trueBranch = positiveRemainder, + falseBranch = remainder, + ) + + mkFpToBvExpr( + roundingMode = towardZero, + value = normalizedRemainder, + bvSize = bv32Sort.sizeBits.toInt(), + isSigned = false, + ) +} + +internal fun TsContext.mkValidArrayIndexProperty( + value: UExpr, +): UBoolExpr = mkFiniteIntegerInRange( + value = value, + minimum = 0.0, + maximum = UINT32_MAX_VALUE - 1.0, +) + +internal fun TsContext.mkValidArrayLength(value: UExpr): UBoolExpr = mkFiniteIntegerInRange( + value = value, + minimum = 0.0, + maximum = UINT32_MAX_VALUE, +) + +internal fun TsContext.mkFpToUint32AfterValidation( + value: UExpr, + validity: UBoolExpr, +): UExpr = with(this) { + val safeValue = mkIte( + condition = validity, + trueBranch = value, + falseBranch = mkFp64(0.0), + ) + mkFpToBvExpr( + roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardZero), + value = safeValue, + bvSize = bv32Sort.sizeBits.toInt(), + isSigned = false, + ) +} + +private fun TsContext.mkFiniteIntegerInRange( + value: UExpr, + minimum: Double, + maximum: Double, +): UBoolExpr = with(this) { + val towardZero = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardZero) + val integer = mkFpRoundToIntegralExpr( + roundingMode = towardZero, + value = value, + ) + val isNotNaN = mkFpIsNaNExpr(value).not() + val isNotInfinite = mkFpIsInfiniteExpr(value).not() + val isInteger = mkFpEqualExpr(value, integer) + val minimumValue = mkFp64(minimum) + val maximumValue = mkFp64(maximum) + val isAtLeastMinimum = mkFpLessOrEqualExpr(minimumValue, value) + val isAtMostMaximum = mkFpLessOrEqualExpr(value, maximumValue) + + mkAnd( + isNotNaN, + isNotInfinite, + isInteger, + isAtLeastMinimum, + isAtMostMaximum, + ) +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Property.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Property.kt index 1f26ff0cb7..b4bd5d567b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Property.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/Property.kt @@ -16,12 +16,11 @@ import org.jacodb.ets.model.EtsStringConstant import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUnknownType -import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.util.arrayStorageType internal fun TsExprResolver.handlePropertyRef(value: EtsPropertyRef): UExpr<*>? { - val normalized = normalizePropertyRef(value) ?: return null + val normalized = normalizePropertyRef(value, isRead = true) ?: return null return when (normalized) { is EtsArrayAccess -> handleArrayAccess(normalized) @@ -31,7 +30,7 @@ internal fun TsExprResolver.handlePropertyRef(value: EtsPropertyRef): UExpr<*>? } internal fun TsExprResolver.handleAssignToProperty(value: EtsPropertyRef, expr: UExpr<*>): Unit? { - val normalized = normalizePropertyRef(value) ?: return null + val normalized = normalizePropertyRef(value, isRead = false) ?: return null return when (normalized) { is EtsArrayAccess -> handleAssignToArrayIndex(normalized, expr) @@ -41,7 +40,7 @@ internal fun TsExprResolver.handleAssignToProperty(value: EtsPropertyRef, expr: } /** Reuses the existing model for concrete data-property names and array indices. */ -internal fun TsExprResolver.normalizePropertyRef(value: EtsPropertyRef): EtsLValue? = with(ctx) { +internal fun TsExprResolver.normalizePropertyRef(value: EtsPropertyRef, isRead: Boolean): EtsLValue? = with(ctx) { var key = resolve(value.key) ?: return null if (key.isFakeObject()) { key = key.extractSingleValueFromFakeObjectOrNull(scope) @@ -59,11 +58,17 @@ internal fun TsExprResolver.normalizePropertyRef(value: EtsPropertyRef): EtsLVal // Storage selection must inspect each feasible reference produced by a guarded property write. val reference = resolveHeapRef(scope, rawReference) ?: return null val storageType = scope.calcOnState { arrayStorageType(reference, value.instance.type) } - if (storageType == EtsStringType && key.sort == fp64Sort) { + val isStringWrite = storageType == EtsStringType && !isRead + if (isStringWrite) { + throw UnsupportedOperationException("String property writes are unsupported: ${value.key}") + } + + val isIndexedNumericKey = (storageType is EtsArrayType || storageType == EtsStringType) && key.sort == fp64Sort + if (isIndexedNumericKey) { return EtsArrayAccess(array = value.instance, index = value.key, type = value.type) } - val name = (key as? UConcreteHeapRef)?.let(::getStringConstantValue) + val name = concreteStringValue(key) ?: throw UnsupportedOperationException("Property access needs a constant converted key: ${value.key}") if (storageType == EtsStringType && name != "length") { val number = name.toDoubleOrNull() @@ -76,7 +81,7 @@ internal fun TsExprResolver.normalizePropertyRef(value: EtsPropertyRef): EtsLVal if (storageType is EtsArrayType) { val index = name.toIntOrNull()?.takeIf { it >= 0 && it.toString() == name } - ?: throw UnsupportedOperationException("Unsupported array property: $name") + ?: throw UnsupportedOperationException("Unsupported indexed property: $name") return EtsArrayAccess(array = value.instance, index = EtsNumberConstant(index.toDouble()), type = value.type) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt index 89c117138e..0225867606 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadArray.kt @@ -8,18 +8,23 @@ import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsUnknownType +import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.isFalse +import org.usvm.isTrue import org.usvm.machine.TsContext import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.machine.types.mkFakeValue import org.usvm.machine.types.readUnresolvedArrayElement import org.usvm.sizeSort import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.readTypedArrayElement private val logger = KotlinLogging.logger {} @@ -49,13 +54,13 @@ internal fun TsExprResolver.handleArrayAccess( // Resolve the index. val resolvedIndex = resolve(value.index) ?: return null - val receiverType = scope.calcOnState { arrayStorageType(array, value.array.type) } - if (receiverType == EtsStringType) { + val storageType = scope.calcOnState { arrayStorageType(array, value.array.type) } + if (storageType == EtsStringType) { return readStringIndex(receiver = array, index = resolvedIndex) } val propertyName = concreteStringValue(resolvedIndex) - if (propertyName != null && receiverType !is EtsArrayType) { + if (propertyName != null && storageType !is EtsArrayType) { val field = EtsFieldSignature( name = propertyName, enclosingClass = EtsClassSignature.UNKNOWN, @@ -63,35 +68,41 @@ internal fun TsExprResolver.handleArrayAccess( ) return resolveField(scope, value.array, array, field, hierarchy) } - if (receiverType !is EtsArrayType) { + + if (storageType !is EtsArrayType) { stopRuntimeFeatureLimitation( reason = TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE, - detail = "Indexed access requires supported storage: static=${value.array.type}, storage=$receiverType", + detail = "Indexed access requires supported storage: static=${value.array.type}, storage=$storageType", ) return null } - check(resolvedIndex.sort == fp64Sort) { - "Expected fp64 sort for index, got: ${resolvedIndex.sort}" + val index = extractNumericArrayIndex(scope, resolvedIndex) + val unsupportedKeyIsFeasible = scope.checkSat(index.hasUnsupportedReadKey) != null + if (unsupportedKeyIsFeasible) { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_READ, + detail = "property key requires unsupported ToPropertyKey conversion: $resolvedIndex", + ) } - val index = resolvedIndex.asExpr(fp64Sort) - - // Convert the index to a bit-vector. - val bvIndex = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = index, - bvSize = sizeSort.sizeBits.toInt(), - isSigned = true, - ).asExpr(sizeSort) - - // Read the array element. - readArray(scope, array, bvIndex, receiverType) + scope.assert(mkNot(index.hasUnsupportedReadKey)) ?: return null + + val indexIsSupported = mkAnd( + index.isNumeric, + mkValidArrayIndexProperty( + value = index.value, + ), + ) + val bvIndex = mkFpToUint32AfterValidation(index.value, indexIsSupported).asExpr(sizeSort) + + readArrayProperty(scope, array, bvIndex, indexIsSupported, storageType) } -fun TsContext.readArray( +private fun TsContext.readArrayProperty( scope: TsStepScope, array: UHeapRef, index: UExpr, + indexIsSupported: UBoolExpr, arrayType: EtsArrayType, ): UExpr<*>? { checkNotFake(array) @@ -102,22 +113,48 @@ fun TsContext.readArray( memory.read(lengthLValue) } - // Check for out-of-bounds access. - checkNegativeIndexRead(scope, index) ?: return null - checkReadingInRange(scope, index, length) ?: return null + val zero = mkBv(0) + val elementExists = mkAnd( + indexIsSupported, + mkBvSignedGreaterOrEqualExpr(index, zero), + mkBvSignedLessExpr(index, length), + ) + if (elementExists.isFalse) { + return mkUndefinedValue() + } + + val element = readArrayElement(scope, array, index, arrayType) + if (elementExists.isTrue) { + return element + } + + return iteWriteIntoFakeObject( + scope = scope, + condition = elementExists, + trueBranchValue = element, + falseBranchValue = mkUndefinedValue(), + ) +} +private fun TsContext.readArrayElement( + scope: TsStepScope, + array: UHeapRef, + index: UExpr, + arrayType: EtsArrayType, +): UExpr<*> { // Determine the element sort. val sort = typeToSort(arrayType.elementType) // If the element type is known, we can read it directly. if (sort !is TsUnresolvedSort) { - val lValue = mkArrayIndexLValue( - sort = sort, - ref = array, - index = index, - type = arrayType, - ) - return scope.calcOnState { memory.read(lValue) } + return scope.calcOnState { + val element = readTypedArrayElement(array, index, arrayType) + if (element.hasBoxedValue.isFalse) { + element.nativeValue + } else { + mkFakeValue(scope = scope, value = element.unresolvedValue) + } + } } return scope.calcOnState { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 5b60f64c3e..224f294426 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -342,11 +342,8 @@ class TsExprResolver( else -> throw UnsupportedOperationException("Symbolic property key conversion: ${expr.arg}") } } - // Keep a symbolic numeric key in numeric form until the property read. String indexing can then - // test canonical integer positions directly; object properties still require a concrete string key. - if (value.sort == fp64Sort && value !is KFp64Value) { - return value - } + // Indexed properties retain evaluated numeric keys; object receivers convert concrete keys below. + if (value.sort == fp64Sort) return value val key = concreteStringValue(value) ?: throw UnsupportedOperationException("Unmodeled property key conversion: ${expr.arg}") @@ -421,13 +418,8 @@ class TsExprResolver( val arg = resolve(expr.arg) ?: return null val numericArg = mkNumericExpr(arg, scope) - // Convert to 32-bit integer, perform bitwise NOT, then convert back to number - val bvArg = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = numericArg.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true - ) + // Convert to the total ECMAScript 32-bit pattern, perform bitwise NOT, then convert back to number. + val bvArg = mkEcmaScriptToUint32(numericArg.asExpr(fp64Sort)) val notResult = mkBvNotExpr(bvArg) return mkBvToFpExpr( @@ -579,7 +571,7 @@ class TsExprResolver( } is EtsPropertyRef -> { - val normalized = normalizePropertyRef(operand) ?: return null + val normalized = normalizePropertyRef(operand, isRead = false) ?: return null visit(EtsDeleteExpr(arg = normalized)) } @@ -940,18 +932,8 @@ class TsExprResolver( val rightNum = mkNumericExpr(right, scope) // Convert to 32-bit integers, perform bitwise AND, then convert back - val leftBv = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = leftNum.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true, - ) - val rightBv = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = rightNum.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true, - ) + val leftBv = mkEcmaScriptToUint32(leftNum.asExpr(fp64Sort)) + val rightBv = mkEcmaScriptToUint32(rightNum.asExpr(fp64Sort)) val result = mkBvAndExpr(leftBv, rightBv) return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), result, signed = true) @@ -965,18 +947,8 @@ class TsExprResolver( val rightNum = mkNumericExpr(right, scope) // Convert to 32-bit integers, perform bitwise OR, then convert back - val leftBv = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = leftNum.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true, - ) - val rightBv = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = rightNum.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true, - ) + val leftBv = mkEcmaScriptToUint32(leftNum.asExpr(fp64Sort)) + val rightBv = mkEcmaScriptToUint32(rightNum.asExpr(fp64Sort)) val result = mkBvOrExpr(leftBv, rightBv) return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), result, signed = true) @@ -990,18 +962,8 @@ class TsExprResolver( val rightNum = mkNumericExpr(right, scope) // Convert to 32-bit integers, perform bitwise XOR, then convert back - val leftBv = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = leftNum.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true, - ) - val rightBv = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = rightNum.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true, - ) + val leftBv = mkEcmaScriptToUint32(leftNum.asExpr(fp64Sort)) + val rightBv = mkEcmaScriptToUint32(rightNum.asExpr(fp64Sort)) val result = mkBvXorExpr(leftBv, rightBv) return mkBvToFpExpr(fp64Sort, fpRoundingModeSortDefaultValue(), result, signed = true) @@ -1015,18 +977,8 @@ class TsExprResolver( val rightNum = mkNumericExpr(right, scope) // Convert to 32-bit integers and perform left shift - val leftBv = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = leftNum.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true, - ) - val rightBv = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = rightNum.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true, - ) + val leftBv = mkEcmaScriptToUint32(leftNum.asExpr(fp64Sort)) + val rightBv = mkEcmaScriptToUint32(rightNum.asExpr(fp64Sort)) // Mask the shift amount to 5 bits (0-31) as per JavaScript spec val shiftAmount = mkBvAndExpr( @@ -1046,18 +998,8 @@ class TsExprResolver( val rightNum = mkNumericExpr(right, scope) // Convert to 32-bit integers and perform signed right shift - val leftBv = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = leftNum.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true, - ) - val rightBv = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = rightNum.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true, - ) + val leftBv = mkEcmaScriptToUint32(leftNum.asExpr(fp64Sort)) + val rightBv = mkEcmaScriptToUint32(rightNum.asExpr(fp64Sort)) // Mask the shift amount to 5 bits (0-31) val shiftAmount = mkBvAndExpr( @@ -1082,18 +1024,8 @@ class TsExprResolver( val rightNum = mkNumericExpr(right, scope) // Convert to 32-bit integers and perform unsigned right shift - val leftBv = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = leftNum.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true, - ) - val rightBv = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = rightNum.asExpr(fp64Sort), - bvSize = ECMASCRIPT_BITWISE_INTEGER_SIZE, - isSigned = true, - ) + val leftBv = mkEcmaScriptToUint32(leftNum.asExpr(fp64Sort)) + val rightBv = mkEcmaScriptToUint32(rightNum.asExpr(fp64Sort)) // Mask the shift amount to 5 bits (0-31) val shiftAmount = mkBvAndExpr( @@ -1593,33 +1525,25 @@ class TsExprResolver( TODO() } - val bvSize = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = size.asExpr(fp64Sort), - bvSize = 32, - isSigned = true, - ) + val fpSize = size.asExpr(fp64Sort) + val validLength = mkValidArrayLength(fpSize) + + scope.fork( + validLength, + blockOnFalseState = { throwException("RangeError: Invalid array length: $fpSize") }, + ) ?: return@calcOnState null - val condition = mkAnd( - mkEq( - mkBvToFpExpr( - sort = fp64Sort, - roundingMode = fpRoundingModeSortDefaultValue(), - value = bvSize, - signed = true, - ), - size.asExpr(fp64Sort) - ), - mkAnd( - mkBvSignedLessOrEqualExpr(mkBv(0), bvSize.asExpr(bv32Sort)), - mkBvSignedLessOrEqualExpr(bvSize.asExpr(bv32Sort), mkBv(Int.MAX_VALUE)) + val maximumSupportedLength = mkFp64(options.maxArraySize.toDouble()) + val withinModelCapacity = mkFpLessOrEqualExpr(fpSize, maximumSupportedLength) + if (scope.checkSat(mkNot(withinModelCapacity)) != null) { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_LENGTH_CAPACITY, + detail = "new Array length exceeds model capacity: $fpSize", ) - ) + } + scope.assert(withinModelCapacity) ?: return@calcOnState null - scope.fork( - condition, - blockOnFalseState = { throwException("Invalid array size: ${size.asExpr(fp64Sort)}") } - ) + val bvSize = mkFpToUint32AfterValidation(fpSize, validLength) if (arrayType.elementType is EtsArrayType) { TODO("Multidimensional arrays are not supported yet, https://github.com/UnitTestBot/usvm/issues/287") @@ -1627,7 +1551,7 @@ class TsExprResolver( val descriptor = arrayDescriptorOf(arrayType) val address = memory.allocConcrete(descriptor) - memory.initializeArrayLength(address, descriptor, sizeSort, bvSize) + memory.initializeArrayLength(address, descriptor, sizeSort, bvSize.asExpr(sizeSort)) address } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt index e963032393..7305401f41 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteArray.kt @@ -1,6 +1,7 @@ package org.usvm.machine.expr import io.ksmt.utils.asExpr +import mu.KotlinLogging import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsClassSignature @@ -15,8 +16,14 @@ import org.usvm.machine.TsSizeSort import org.usvm.machine.interpreter.TsStepScope import org.usvm.sizeSort import org.usvm.util.arrayStorageType +import org.usvm.util.boxArrayValue +import org.usvm.util.initializeTypedArrayOverrides import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue +import org.usvm.util.typedArrayBoxedLValue +import org.usvm.util.typedArrayOverrideLValue + +private val logger = KotlinLogging.logger {} internal fun TsExprResolver.handleAssignToArrayIndex( lhv: EtsArrayAccess, @@ -33,20 +40,29 @@ internal fun TsExprResolver.handleAssignToArrayIndex( } else { resolvedArray.asExpr(addressSort) } - - // Check for undefined or null array access. checkUndefinedOrNullPropertyRead(scope, rawArray, propertyName = "[]") ?: return null val array = resolveHeapRef(scope, rawArray) ?: return null + handleAssignToArrayIndex(lhv = lhv, expr = expr, array = array) +} + +internal fun TsExprResolver.handleAssignToArrayIndex( + lhv: EtsArrayAccess, + expr: UExpr<*>, + array: UHeapRef, +): Unit? = with(ctx) { + // Check for undefined or null array access. + checkUndefinedOrNullPropertyRead(scope, array, propertyName = "[]") ?: return null + // Resolve the index. val resolvedIndex = resolve(lhv.index) ?: return null - val receiverType = scope.calcOnState { arrayStorageType(array, lhv.array.type) } - if (receiverType == EtsStringType) { + val storageType = scope.calcOnState { arrayStorageType(array, lhv.array.type) } + if (storageType == EtsStringType) { throw UnsupportedOperationException("Writes to string indexes are not modeled") } val propertyName = concreteStringValue(resolvedIndex) - if (propertyName != null && receiverType !is EtsArrayType) { + if (propertyName != null && storageType !is EtsArrayType) { val field = EtsFieldSignature( name = propertyName, enclosingClass = EtsClassSignature.UNKNOWN, @@ -54,28 +70,48 @@ internal fun TsExprResolver.handleAssignToArrayIndex( ) return assignToInstanceField(scope, lhv.array, array, field, expr, hierarchy) } - if (receiverType !is EtsArrayType) { + + if (storageType !is EtsArrayType) { stopRuntimeFeatureLimitation( reason = TsRuntimeFeatureLimitationReason.ARRAY_STORAGE_TYPE, - detail = "Indexed access requires supported storage: static=${lhv.array.type}, storage=$receiverType", + detail = "Indexed access requires supported storage: static=${lhv.array.type}, storage=$storageType", ) return null } - check(resolvedIndex.sort == fp64Sort) { - "Expected fp64 sort for index, got: ${resolvedIndex.sort}" + val index = extractNumericArrayIndex(scope, resolvedIndex) + + val indexIsSupported = mkAnd( + index.isNumeric, + mkValidArrayIndexProperty( + value = index.value, + ), + ) + val unsupportedIndexIsFeasible = scope.checkSat(mkNot(indexIsSupported)) != null + if (unsupportedIndexIsFeasible) { + logger.warn { "Unsupported named array property write for key: $resolvedIndex" } + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, + detail = "property key is not a supported numeric array index: $resolvedIndex", + ) } - val index = resolvedIndex.asExpr(fp64Sort) + scope.assert(indexIsSupported) ?: return null - // Convert the index to a bit-vector. - val bvIndex = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = index, - bvSize = 32, - isSigned = true, - ).asExpr(sizeSort) + val bvIndex = mkFpToUint32AfterValidation(index.value, indexIsSupported).asExpr(sizeSort) - return assignToArrayIndex(scope, array, bvIndex, expr, receiverType) + return assignToArrayIndex( + scope = scope, + array = array, + index = bvIndex, + expr = expr, + arrayType = storageType, + onUnsupportedGrowth = { + reportRuntimeFeatureLimitation( + reason = TsRuntimeFeatureLimitationReason.ARRAY_INDEX_GROWTH, + detail = "array index write would grow beyond the current length", + ) + }, + ) } fun TsContext.assignToArrayIndex( @@ -84,6 +120,7 @@ fun TsContext.assignToArrayIndex( index: UExpr, expr: UExpr<*>, arrayType: EtsArrayType, + onUnsupportedGrowth: (() -> Unit)? = null, ): Unit? { checkNotFake(array) @@ -97,14 +134,44 @@ fun TsContext.assignToArrayIndex( // However, we decided to forbid this behavior in our model for simplicity. // Instead, we only allow writing to existing indices. - // Check for out-of-bounds access. - checkNegativeIndexRead(scope, index) ?: return null - checkReadingInRange(scope, index, length) ?: return null + val indexIsNonNegative = mkBvSignedGreaterOrEqualExpr(index, mkBv(0)) + val indexIsBelowLength = mkBvSignedLessExpr(index, length) + val indexIsInRange = mkAnd(indexIsNonNegative, indexIsBelowLength) + if (scope.checkSat(mkNot(indexIsInRange)) != null) { + logger.warn { "Unsupported array growth through index write: index=$index, length=$length" } + onUnsupportedGrowth?.invoke() + } + scope.assert(indexIsInRange) ?: return null val elementSort = typeToSort(arrayType.elementType) // If the element sort is known, write directly. if (elementSort !is TsUnresolvedSort) { + val containsFakeValue = expr.sort == addressSort && expr.asExpr(addressSort).hasFakeValueBranch() + val directPayload = expr.sort == elementSort && !containsFakeValue + if (directPayload) { + val lValue = mkArrayIndexLValue(elementSort, array, index, arrayType) + return scope.doWithState { + memory.write(lValue, expr.asExpr(elementSort), guard = trueExpr) + initializeTypedArrayOverrides(array) + memory.write(typedArrayOverrideLValue(array, index), falseExpr, guard = trueExpr) + } + } + + val fake = boxArrayValue(scope, expr) + val kind = fake.getFakeType(scope) + val compatibleKind = when (elementSort) { + boolSort -> kind.boolTypeExpr + fp64Sort -> kind.fpTypeExpr + addressSort -> kind.refTypeExpr + else -> error("Unsupported typed array element sort: $elementSort") + } + val payload = when (elementSort) { + boolSort -> fake.extractBool(scope) + fp64Sort -> fake.extractFp(scope) + addressSort -> fake.extractRef(scope) + else -> error("Unsupported typed array element sort: $elementSort") + } val lValue = mkArrayIndexLValue( sort = elementSort, ref = array, @@ -112,7 +179,10 @@ fun TsContext.assignToArrayIndex( type = arrayType, ) return scope.doWithState { - memory.write(lValue, expr.asExpr(elementSort), guard = trueExpr) + memory.write(lValue, payload.asExpr(elementSort), guard = compatibleKind) + initializeTypedArrayOverrides(array) + memory.write(typedArrayBoxedLValue(array, index), fake, guard = trueExpr) + memory.write(typedArrayOverrideLValue(array, index), mkNot(compatibleKind), guard = trueExpr) } } @@ -123,7 +193,7 @@ fun TsContext.assignToArrayIndex( index = index.asExpr(sizeSort), type = arrayType, ) - val fakeExpr = expr.toFakeObject(scope) + val fakeExpr = boxArrayValue(scope, expr) return scope.doWithState { memory.write(lValue, fakeExpr, guard = trueExpr) } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index 35734c96d2..c53578a18e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt @@ -13,6 +13,7 @@ import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.isAllocatedConcreteHeapRef import org.usvm.machine.TsContext +import org.usvm.machine.TsRuntimeFeatureLimitationReason import org.usvm.machine.interpreter.TsStepScope import org.usvm.machine.interpreter.ensureStaticsInitialized import org.usvm.machine.types.EtsAuxiliaryType @@ -93,6 +94,7 @@ internal fun TsExprResolver.handleAssignToInstanceField( arrayType = arrayType, value = expr, maxArraySize = options.maxArraySize, + onFeatureLimitation = ::reportRuntimeFeatureLimitation, ) } @@ -106,6 +108,7 @@ private fun TsContext.assignToArrayLength( arrayType: EtsArrayType, value: UExpr<*>, maxArraySize: Int, + onFeatureLimitation: (TsRuntimeFeatureLimitationReason, String) -> Unit, ): Unit? = with(this) { val (fpLength, numericTypeGuard) = scope.calcOnState { with(ctx) { @@ -121,37 +124,41 @@ private fun TsContext.assignToArrayLength( return null } - val convertedLength = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = fpLength, - bvSize = 32, - isSigned = true, - ) - val roundTrip = mkBvToFpExpr( - sort = fp64Sort, - roundingMode = fpRoundingModeSortDefaultValue(), - value = convertedLength, - signed = true, - ) - val length = convertedLength.asExpr(sizeSort) + val validJsLength = mkValidArrayLength(fpLength) + scope.fork( + validJsLength, + blockOnFalseState = { throwException("RangeError: Invalid array length: $fpLength") }, + ) ?: return null + + val maximumSupportedLength = mkFp64(maxArraySize.toDouble()) + val withinModelCapacity = mkFpLessOrEqualExpr(fpLength, maximumSupportedLength) + if (scope.checkSat(mkNot(withinModelCapacity)) != null) { + onFeatureLimitation( + TsRuntimeFeatureLimitationReason.ARRAY_LENGTH_CAPACITY, + "assigned array length exceeds model capacity: $fpLength", + ) + } + scope.assert(withinModelCapacity) ?: run { + logger.warn { "Unsupported array length assignment beyond model capacity: $fpLength" } + return null + } + + val length = mkFpToUint32AfterValidation(fpLength, validJsLength).asExpr(sizeSort) val lengthLValue = mkArrayLengthLValue(array, arrayType) val currentLength = scope.calcOnState { memory.read(lengthLValue) } - val lengthIsIntegral = mkFpEqualExpr(roundTrip, fpLength) - val lengthIsNonNegative = mkBvSignedGreaterOrEqualExpr(length, mkBv(0)) - val lengthIsWithinLimit = mkBvSignedLessOrEqualExpr(length, mkBv(maxArraySize)) val lengthIsNotGrowing = mkBvSignedLessOrEqualExpr(length, currentLength) - val validLength = mkAnd( - lengthIsIntegral, - lengthIsNonNegative, - lengthIsWithinLimit, - lengthIsNotGrowing, - ) - scope.assert(validLength) ?: run { + if (scope.checkSat(mkNot(lengthIsNotGrowing)) != null) { + onFeatureLimitation( + TsRuntimeFeatureLimitationReason.ARRAY_LENGTH_GROWTH, + "assigned array length would grow beyond the current length", + ) + } + scope.assert(lengthIsNotGrowing) ?: run { logger.warn { - "Unsupported array length assignment: expected an integral length in [0, current length], " + - "but the constraint is UNSAT: $validLength" + "Unsupported array length growth: expected length at most the current length, " + + "but the constraint is UNSAT: $lengthIsNotGrowing" } return null } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index 858ec044a3..1f07f0062e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt @@ -1,7 +1,6 @@ package org.usvm.machine.interpreter import io.ksmt.utils.asExpr -import io.ksmt.utils.cast import mu.KotlinLogging import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayAccess @@ -88,10 +87,8 @@ import org.usvm.machine.types.toAuxiliaryType import org.usvm.sizeSort import org.usvm.targets.UTargetsSet import org.usvm.types.TypesResult -import org.usvm.types.first import org.usvm.types.single import org.usvm.util.executableOverloadImplementation -import org.usvm.util.mkArrayIndexLValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.mkRegisterStackLValue @@ -605,32 +602,8 @@ class TsInterpreter( "Expected address sort for the array, got: ${array.sort}" } val arrayRef = array.asExpr(addressSort) - val resolvedIndex = exprResolver.resolve(lhv.index) ?: return null - val index = resolvedIndex.asExpr(fp64Sort) - val bvIndex = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = index, - bvSize = 32, - isSigned = true, - ).asExpr(sizeSort) - val arrayType = if (isAllocatedConcreteHeapRef(array)) { - scope.calcOnState { memory.typeStreamOf(array).first() } - } else { - lhv.array.type - } - check(arrayType is EtsArrayType) { - "Expected EtsArrayType, got: ${lhv.array.type}" - } - val elementSort = typeToSort(arrayType.elementType) - val elementLValue = mkArrayIndexLValue( - sort = elementSort, - ref = arrayRef, - index = bvIndex.asExpr(sizeSort), - type = arrayType, - ) - scope.doWithState { - memory.write(elementLValue, expr.cast(), guard = trueExpr) - } + + exprResolver.handleAssignToArrayIndex(lhv, expr, arrayRef) } } 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 89e5b4064b..25d56aac73 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 @@ -99,6 +99,7 @@ class TsState( var unsupportedReason: String? = null, var trackedObjectProperties: Set = emptySet(), var writtenConcreteFields: Set> = emptySet(), + var initializedTypedArrayOverrides: Set = emptySet(), var writtenObjectLiteralFieldSorts: UPersistentHashMap, USort> = persistentHashMapOf(), private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( @@ -347,6 +348,7 @@ class TsState( unsupportedReason = unsupportedReason, trackedObjectProperties = trackedObjectProperties, writtenConcreteFields = writtenConcreteFields, + initializedTypedArrayOverrides = initializedTypedArrayOverrides, writtenObjectLiteralFieldSorts = writtenObjectLiteralFieldSorts, activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt index 3cd941ce4b..3496177c9f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt @@ -44,6 +44,14 @@ internal fun TsState.copyArrayElements( ctx.forEachArrayPayloadRegion(arrayType) { region, sort -> memory.memcpy(srcRef, dstRef, region, sort, fromSrc, fromDst, length) } + with(ctx) { + if (typeToSort(arrayType.elementType) !is TsUnresolvedSort) { + initializeTypedArrayOverrides(srcRef) + initializeTypedArrayOverrides(dstRef) + memory.memcpy(srcRef, dstRef, TsTypedArrayStorage.HAS_BOXED_VALUE, boolSort, fromSrc, fromDst, length) + memory.memcpy(srcRef, dstRef, TsTypedArrayStorage.BOXED_VALUE, addressSort, fromSrc, fromDst, length) + } + } if (ctx.typeToSort(arrayType.elementType) is TsUnresolvedSort) { TsUnresolvedArrayKind.entries.forEach { kind -> memory.memcpy(srcRef, dstRef, kind, ctx.boolSort, fromSrc, fromDst, length) diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/TypedArrayStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/TypedArrayStorage.kt new file mode 100644 index 0000000000..add8b146a7 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/TypedArrayStorage.kt @@ -0,0 +1,111 @@ +package org.usvm.util + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.usvm.UBoolExpr +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.api.allocateConcreteRef +import org.usvm.api.memcpy +import org.usvm.api.readArrayIndex +import org.usvm.collection.array.UArrayIndexLValue +import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.machine.TsContext +import org.usvm.machine.TsSizeSort +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.machine.state.TsState +import org.usvm.machine.types.EtsFakeType +import org.usvm.machine.types.TsUnresolvedValue +import org.usvm.machine.types.iteUnresolvedValue +import org.usvm.machine.types.mkFakeValue + +/** Extra cells preserve values whose runtime kind differs from an allocated array's inferred element type. */ +internal enum class TsTypedArrayStorage { + HAS_BOXED_VALUE, + BOXED_VALUE, +} + +internal fun TsContext.typedArrayOverrideLValue(array: UHeapRef, index: UExpr) = + UArrayIndexLValue(boolSort, array, index, TsTypedArrayStorage.HAS_BOXED_VALUE) + +internal fun TsContext.typedArrayBoxedLValue(array: UHeapRef, index: UExpr) = + UArrayIndexLValue(addressSort, array, index, TsTypedArrayStorage.BOXED_VALUE) + +internal data class TsTypedArrayElement( + val nativeValue: UExpr<*>, + val hasBoxedValue: UBoolExpr, + val unresolvedValue: TsUnresolvedValue, +) + +/** Captures both representations before a model shifts or copies the underlying storage. */ +internal fun TsState.readTypedArrayElement( + array: UHeapRef, + index: UExpr, + arrayType: EtsArrayType, +): TsTypedArrayElement = with(ctx) { + initializeTypedArrayOverrides(array) + val sort = typeToSort(arrayType.elementType) + val nativeValue = memory.read(mkArrayIndexLValue(sort, array, index, arrayType)) + val native = TsUnresolvedValue( + boolValue = if (sort == boolSort) nativeValue.asExpr(boolSort) else falseExpr, + fpValue = if (sort == fp64Sort) nativeValue.asExpr(fp64Sort) else mkFp64(0.0), + refValue = if (sort == addressSort) nativeValue.asExpr(addressSort) else mkUndefinedValue(), + type = when (sort) { + boolSort -> EtsFakeType.mkBool(ctx) + fp64Sort -> EtsFakeType.mkFp(ctx) + addressSort -> EtsFakeType.mkRef(ctx) + else -> error("Typed array has unresolved element sort") + }, + ) + val hasBoxed = memory.readArrayIndex(array, index, TsTypedArrayStorage.HAS_BOXED_VALUE, boolSort) + val boxed = TsUnresolvedValue( + boolValue = falseExpr, + fpValue = mkFp64(0.0), + refValue = memory.readArrayIndex(array, index, TsTypedArrayStorage.BOXED_VALUE, addressSort), + type = EtsFakeType.mkRef(ctx), + ) + + TsTypedArrayElement( + nativeValue = nativeValue, + hasBoxedValue = hasBoxed, + unresolvedValue = iteUnresolvedValue(hasBoxed, boxed, native), + ) +} + +/** Initializes private engine metadata, with alias guards so an existing array's overrides survive. */ +internal fun TsState.initializeTypedArrayOverrides(array: UHeapRef) = with(ctx) { + if (array in initializedTypedArrayOverrides) return@with + + if (!isAllocatedConcreteHeapRef(array)) { + val distinctFromInitialized = initializedTypedArrayOverrides.map { prior -> mkNot(mkHeapRefEq(array, prior)) } + val initializeGuard = mkAnd(distinctFromInitialized) + val empty = allocateConcreteRef() + memory.memcpy( + srcRef = empty, + dstRef = array, + type = TsTypedArrayStorage.HAS_BOXED_VALUE, + elementSort = boolSort, + fromSrcIdx = mkBv(0), + fromDstIdx = mkBv(0), + toDstIdx = mkBv(Int.MAX_VALUE), + guard = initializeGuard, + ) + } + initializedTypedArrayOverrides += array +} + +internal fun TsContext.boxArrayValue(scope: TsStepScope, value: UExpr<*>): UConcreteHeapRef { + val containsFakeValue = value.sort == addressSort && value.asExpr(addressSort).hasFakeValueBranch() + if (!containsFakeValue) return value.toFakeObject(scope) + + return scope.calcOnState { + val packet = TsUnresolvedValue( + boolValue = falseExpr, + fpValue = mkFp64(0.0), + refValue = value.asExpr(addressSort), + type = EtsFakeType.mkRef(ctx), + ) + mkFakeValue(scope = scope, value = packet) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt index 793a1d98ff..571f88e566 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayShiftReplayTest.kt @@ -39,7 +39,13 @@ class TsArrayShiftReplayTest { DynamicTest.dynamicTest(case.name) { val method = methods.getValue("case$index") - val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> + val dispatcher = TsCompatibilityUnknownCallDispatcher.takeIf { case.compatibility } + val tests = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + unknownCallDispatcher = dispatcher, + ).use { machine -> machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } } @@ -159,7 +165,7 @@ class TsArrayShiftReplayTest { private fun storageOperationCases(): List = listOf("any", "unknown").flatMap { type -> copyCases(type) + mutationCases(type) + concatCases(type) - } + }.map { case -> case.copy(name = "compatibility storage: ${case.name}", compatibility = true) } private fun copyCases(type: String): List = listOf( ReplayCase( @@ -446,6 +452,7 @@ class TsArrayShiftReplayTest { val parameters: String, val maxResult: Int, val body: String, + val compatibility: Boolean = false, ) private companion object { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt index 72293e5b07..1820e2bd14 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsInstanceCallReceiverTest.kt @@ -36,7 +36,8 @@ class TsInstanceCallReceiverTest { val methods = scene.projectClasses.single { it.name == "InstanceCallReceiver" }.methods.associateBy { it.name } return cases.map { case -> - DynamicTest.dynamicTest(case.method) { + val label = if (case.compatibility) "compatibility receiver: ${case.method}" else case.method + DynamicTest.dynamicTest(label) { val method = methods.getValue(case.method) val events = mutableListOf() val observer = object : TsInterpreterObserver { @@ -45,7 +46,13 @@ class TsInstanceCallReceiverTest { } } - val tests = TsMachine(scene, options = machineOptions, tsOptions = TsOptions(), observer = observer) + val tests = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + observer = observer, + unknownCallDispatcher = TsCompatibilityUnknownCallDispatcher.takeIf { case.compatibility }, + ) .use { machine -> machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } } @@ -107,30 +114,31 @@ class TsInstanceCallReceiverTest { val method: String, val results: Set, val throws: Boolean = false, + val compatibility: Boolean = false, ) private companion object { val cases = listOf( Case(method = "wrappedShift", results = setOf(1.0)), Case(method = "wrappedPop", results = setOf(1.0)), - Case(method = "wrappedPush", results = setOf(1.0)), - Case(method = "wrappedReverse", results = setOf(1.0)), - Case(method = "wrappedFill", results = setOf(1.0)), - Case(method = "wrappedUnshift", results = setOf(1.0)), - Case(method = "wrappedSlice", results = setOf(1.0)), - Case(method = "wrappedSliceReversed", results = setOf(1.0)), - Case(method = "wrappedSlicePastEnd", results = setOf(1.0)), - Case(method = "wrappedSlicePastStart", results = setOf(1.0)), - Case(method = "wrappedSliceNegative", results = setOf(1.0)), - Case(method = "wrappedSliceEmpty", results = setOf(1.0)), - Case(method = "wrappedConcat", results = setOf(1.0)), + Case(method = "wrappedPush", results = setOf(1.0), compatibility = true), + Case(method = "wrappedReverse", results = setOf(1.0), compatibility = true), + Case(method = "wrappedFill", results = setOf(1.0), compatibility = true), + Case(method = "wrappedUnshift", results = setOf(1.0), compatibility = true), + Case(method = "wrappedSlice", results = setOf(1.0), compatibility = true), + Case(method = "wrappedSliceReversed", results = setOf(1.0), compatibility = true), + Case(method = "wrappedSlicePastEnd", results = setOf(1.0), compatibility = true), + Case(method = "wrappedSlicePastStart", results = setOf(1.0), compatibility = true), + Case(method = "wrappedSliceNegative", results = setOf(1.0), compatibility = true), + Case(method = "wrappedSliceEmpty", results = setOf(1.0), compatibility = true), + Case(method = "wrappedConcat", results = setOf(1.0), compatibility = true), Case(method = "wrappedUserMethod", results = setOf(1.0)), Case(method = "customShift", results = setOf(1.0)), Case(method = "conditionalArrays", results = setOf(0.0, 1.0)), Case(method = "conditionalEmptyArray", results = setOf(0.0, 1.0)), Case(method = "arrayOrUserMethod", results = setOf(0.0, 1.0)), Case(method = "primitiveValueOf", results = setOf(0.0, 1.0)), - Case(method = "primitiveToString", results = setOf(0.0, 1.0)), + Case(method = "primitiveToString", results = setOf(0.0, 1.0), compatibility = true), Case(method = "constrainedFake", results = setOf(0.0, 1.0, 2.0)), Case(method = "nullableReceiver", results = setOf(0.0, 1.0), throws = true), Case(method = "undefinedReceiver", results = setOf(0.0, 1.0), throws = true), diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/GlobalArrayAssignmentBoundaryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/GlobalArrayAssignmentBoundaryTest.kt new file mode 100644 index 0000000000..667ba69652 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/GlobalArrayAssignmentBoundaryTest.kt @@ -0,0 +1,72 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertTrue +import kotlin.time.Duration + +class GlobalArrayAssignmentBoundaryTest { + @Test + fun `fractional global array assignment stops as a named property limitation`() { + val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/GlobalArrayAssignmentBoundary.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + val scene = EtsScene(listOf(sourceFile)) + val method = scene.projectClasses + .single { it.name == "GlobalArrayAssignmentBoundary" } + .methods + .single { it.name == "readSecondValue" } + val observer = RecordingObserver() + + val states = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(maxArraySize = 16), + observer = observer, + ).use { machine -> + machine.analyze(listOf(method)) + } + + assertTrue(states.isEmpty()) + assertEquals( + TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, + observer.limitations.single().reason, + ) + } + + private class RecordingObserver : TsInterpreterObserver { + val limitations = mutableListOf() + + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event + } + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 20_000L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumericBoundarySemanticsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumericBoundarySemanticsTest.kt new file mode 100644 index 0000000000..d830ea95c3 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumericBoundarySemanticsTest.kt @@ -0,0 +1,268 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.machine.state.TsMethodResult +import org.usvm.machine.state.TsState +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class NumericBoundarySemanticsTest : TsMethodTestRunner() { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/NumericBoundarySemantics.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + override val scene = EtsScene(listOf(sourceFile)) + + @Test + fun `allocated arrays preserve mixed runtime kinds and aliases`() { + discoverNumber("mixedNumericUndefinedLiteral", expected = 1.0) + discoverNumber("mixedBooleanNullLiteral", expected = 1.0) + discoverNumber("mixedAliasWrites", expected = 3.0) + discoverNumber("mixedArrayShift", expected = 1.0) + discoverProperties( + method = method("mixedFakeNumberWrite"), + { flag, result -> flag.value && result.number == 1.0 }, + { flag, result -> !flag.value && result.number == 2.0 }, + invariants = arrayOf({ flag, result -> result.number == if (flag.value) 1.0 else 2.0 }), + ) + } + + @Test + fun `symbolic typed input writes preserve mixed values through aliases`() { + discoverProperties, TsTestValue.TsNumber>( + method = method("symbolicTypedInputWrites"), + { values, result -> values.values.size < 2 && result.number == 0.0 }, + { values, result -> values.values.size >= 2 && result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number in setOf(0.0, 1.0) }), + ) + discoverProperties, TsTestValue.TsArray<*>, TsTestValue.TsNumber>( + method = method("symbolicTypedAliases"), + { _, _, result -> result.number == 0.0 }, + { _, _, result -> result.number == 1.0 }, + { _, _, result -> result.number == 2.0 }, + invariants = arrayOf({ _, _, result -> result.number in setOf(0.0, 1.0, 2.0) }), + ) + } + + @Test + fun `materialized input snapshots show mixed writes only after execution`() { + val target = method("symbolicTypedInputWrites") + val tests = analyze(target).map { state -> TsTestResolver().resolve(target, state) } + val mutated = tests.filter { test -> + val result = test.returnValue as? TsTestValue.TsNumber + result?.number == 1.0 + } + + assertTrue(mutated.isNotEmpty()) + for (test in mutated) { + val before = assertIs>(test.before.parameters.single()) + val after = assertIs>(test.after.parameters.single()) + + assertTrue(before.values.all { value -> value is TsTestValue.TsNumber }) + assertEquals(TsTestValue.TsNull, after.values[0]) + assertEquals(TsTestValue.TsBoolean(true), after.values[1]) + } + } + + @Test + fun `bitwise operators use total ECMAScript int32 conversion`() { + val expectedResults = mapOf( + "bitwiseNaN" to 0.0, + "bitwiseInfinity" to 0.0, + "bitwiseUint32Wrap" to 1.0, + "bitwiseFraction" to 1.0, + "bitwiseNegativeFraction" to -1.0, + "bitwiseNotNaN" to -1.0, + "bitwiseAndInfinity" to 0.0, + "bitwiseXorInfinity" to 7.0, + "leftShiftMasksCount" to 2.0, + "rightShiftTruncates" to -2.0, + "unsignedRightShift" to 4_294_967_295.0, + "bitwiseNegativeZero" to 0.0, + ) + + expectedResults.forEach { (methodName, expected) -> + discoverNumber(methodName, expected) + } + } + + @Test + fun `missing numeric array properties return undefined without integer coercion`() { + discoverNumber("missingNumericArrayProperties", expected = 63.0) + discoverNumber("negativeZeroArrayIndex", expected = 11.0) + } + + @Test + fun `unsupported named property and growth writes stop their paths`() { + val unsupportedMethods = mapOf( + "fractionalArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, + "negativeArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, + "outOfRangeArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_INDEX_GROWTH, + "chainedMissingArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, + ) + + unsupportedMethods.forEach { (methodName, reason) -> + val observer = RecordingObserver() + + assertTrue(analyze(methodName, observer).isEmpty(), methodName) + assertEquals(reason, observer.limitations.single().reason, methodName) + } + discoverNumber("negativeZeroArrayWrite", expected = 7.0) + } + + @Test + fun `chained array indexes preserve numeric and undefined branches`() { + discoverNumber("chainedArrayRead", expected = 22.0) + discoverProperties( + method = method("chainedMissingArrayRead"), + { result -> result == TsTestValue.TsUndefined }, + ) + } + + @Test + fun `reference property keys remain explicit read limitations`() { + val unsupportedMethods = listOf( + "stringArrayIndexRead", + "objectArrayIndexRead", + ) + + unsupportedMethods.forEach { methodName -> + val observer = RecordingObserver() + + assertTrue(analyze(methodName, observer).isEmpty(), methodName) + assertEquals( + TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_READ, + observer.limitations.single().reason, + methodName, + ) + } + } + + @Test + fun `numeric string indexes address UTF16 code units without coercion`() { + discoverString("stringZeroIndex", expected = "A") + discoverString("stringNegativeZeroIndex", expected = "A") + discoverString("stringHighSurrogateIndex", expected = "\uD83D") + discoverString("stringLowSurrogateIndex", expected = "\uDE00") + discoverNumber("missingNumericStringProperties", expected = 31.0) + } + + @Test + fun `invalid array lengths throw before conversion`() { + val invalidMethods = listOf( + "newArrayInfinity", + "newArrayUint32Overflow", + "newArrayFraction", + "assignInvalidLength", + ) + + invalidMethods.forEach { methodName -> + val state = analyze(methodName).single() + assertIs(state.methodResult, methodName) + } + } + + @Test + fun `valid but unsupported lengths remain residual`() { + val unsupportedMethods = listOf( + "newArrayBeyondModelCapacity", + "assignLengthBeyondModelCapacity", + ) + + unsupportedMethods.forEach { methodName -> + val observer = RecordingObserver() + + assertTrue(analyze(methodName, observer).isEmpty(), methodName) + assertEquals( + TsRuntimeFeatureLimitationReason.ARRAY_LENGTH_CAPACITY, + observer.limitations.single().reason, + methodName, + ) + } + } + + @Test + fun `negative zero is a valid array length`() { + discoverNumber("newArrayNegativeZero", expected = 0.0) + discoverNumber("assignNegativeZeroLength", expected = 0.0) + } + + private fun discoverNumber(methodName: String, expected: Double) { + discoverProperties( + method = method(methodName), + { result -> result.number == expected }, + invariants = arrayOf({ result -> result.number == expected }), + ) + } + + private fun discoverString(methodName: String, expected: String) { + discoverProperties( + method = method(methodName), + { result -> result.value == expected }, + invariants = arrayOf({ result -> result.value == expected }), + ) + } + + private fun analyze( + methodName: String, + observer: TsInterpreterObserver? = null, + ): List = analyze(method(methodName), observer) + + private fun analyze( + method: EtsMethod, + observer: TsInterpreterObserver? = null, + ): List = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(maxArraySize = 16), + observer = observer, + ).use { machine -> + machine.analyze(listOf(method)) + } + + private fun method(name: String): EtsMethod = scene.projectClasses + .single { it.name == "NumericBoundarySemantics" } + .methods + .single { it.name == name } + + private class RecordingObserver : TsInterpreterObserver { + val limitations = mutableListOf() + + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event + } + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 20_000L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt index 3c9c3feeea..1619f5233e 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/AllocatedArrays.kt @@ -2,11 +2,20 @@ package org.usvm.samples.arrays import org.jacodb.ets.model.EtsScene import org.junit.jupiter.api.Test +import org.usvm.UMachineOptions import org.usvm.api.TsTestValue +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.TsRuntimeFeatureLimitationEvent +import org.usvm.machine.TsRuntimeFeatureLimitationReason +import org.usvm.test.util.checkers.eq as exactly import org.usvm.test.util.checkers.noResultsExpected import org.usvm.util.TsMethodTestRunner import org.usvm.util.eq import org.usvm.util.neq +import kotlin.test.assertEquals +import kotlin.test.assertTrue class AllocatedArrays : TsMethodTestRunner() { private val tsPath = "/samples/arrays/AllocatedArrays.ts" @@ -87,27 +96,48 @@ class AllocatedArrays : TsMethodTestRunner() { @Test fun `test createArrayOfNumbersAndPutDifferentTypes`() { val method = getMethod("createArrayOfNumbersAndPutDifferentTypes") + val expected = listOf(TsTestValue.TsNull, TsTestValue.TsBoolean(value = true), TsTestValue.TsUndefined) + checkMatches>( method = method, - noResultsExpected + analysisResultNumberMatches = exactly(1), + { result -> result.values == expected }, ) } @Test fun `test allocatedArrayLengthExpansion`() { - val method = getMethod("allocatedArrayLengthExpansion") - discoverProperties( - method = method, - { r -> r is TsTestValue.TsException } - ) + assertArrayIndexGrowthLimitation("allocatedArrayLengthExpansion") } @Test fun `test writeInTheIndexEqualToLength`() { - val method = getMethod("writeInTheIndexEqualToLength") - discoverProperties( - method = method, - { r -> r is TsTestValue.TsException }, + assertArrayIndexGrowthLimitation("writeInTheIndexEqualToLength") + } + + private fun assertArrayIndexGrowthLimitation(methodName: String) { + val observer = RecordingObserver() + val states = TsMachine( + scene = scene, + options = UMachineOptions(), + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> + machine.analyze(listOf(getMethod(methodName))) + } + + assertTrue(states.isEmpty()) + assertEquals( + TsRuntimeFeatureLimitationReason.ARRAY_INDEX_GROWTH, + observer.limitations.single().reason, ) } + + private class RecordingObserver : TsInterpreterObserver { + val limitations = mutableListOf() + + override fun onRuntimeFeatureLimitation(event: TsRuntimeFeatureLimitationEvent) { + limitations += event + } + } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt index 31b1d18b6c..486ec151b3 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt @@ -18,22 +18,22 @@ class InputArrays : TsMethodTestRunner() { val method = getMethod("inputArrayOfNumbers") discoverProperties, TsTestValue>( method = method, - { _, r -> r is TsTestValue.TsException }, { x, r -> r as TsTestValue.TsNumber - val x0 = x.values[0] as TsTestValue.TsNumber - (r eq 1) && (x0 eq 1) + val firstElement = x.values.firstOrNull() + (r eq 1) && firstElement is TsTestValue.TsNumber && (firstElement eq 1) }, { x, r -> r as TsTestValue.TsNumber - val x0 = x.values[0] as TsTestValue.TsNumber - (r eq 2) && (x0 neq 1) + val firstElement = x.values.firstOrNull() + val firstElementIsUndefined = firstElement == null || firstElement is TsTestValue.TsUndefined + (r eq -1) && firstElementIsUndefined + }, + { x, r -> + r as TsTestValue.TsNumber + val firstElement = x.values.firstOrNull() + (r eq 2) && firstElement is TsTestValue.TsNumber && (firstElement neq 1) }, - invariants = arrayOf( - { _, r -> - r !is TsTestValue.TsNumber || (r neq -1) - } - ) ) } @@ -62,7 +62,7 @@ class InputArrays : TsMethodTestRunner() { discoverProperties, TsTestValue.TsNumber>( method = method, { x, r -> (r eq 1) && x.values[0].value }, - { x, r -> (r eq -1) && !x.values[0].value }, + { x, r -> (r eq -1) && x.values.firstOrNull()?.value != true }, ) } @@ -73,29 +73,33 @@ class InputArrays : TsMethodTestRunner() { method = method, // TODO exception { x, r -> - val firstElement = x.values[0] + val firstElement = x.values.firstOrNull() (r.values == x.values) && firstElement is TsTestValue.TsNumber && (firstElement eq 1.1) }, { x, r -> - val firstElement = x.values[0] + val firstElement = x.values.firstOrNull() val firstElementCondition = firstElement !is TsTestValue.TsNumber || (firstElement neq 1.1) - val secondElement = x.values[1] + val secondElement = x.values.getOrNull(1) val secondElementCondition = secondElement is TsTestValue.TsBoolean && secondElement.value (r.values == x.values) && firstElementCondition && secondElementCondition }, { x, r -> - val firstElement = x.values[0] + val firstElement = x.values.firstOrNull() val firstElementCondition = firstElement !is TsTestValue.TsNumber || (firstElement neq 1.1) - val secondElement = x.values[1] + val secondElement = x.values.getOrNull(1) val secondElementCondition = secondElement !is TsTestValue.TsBoolean || !secondElement.value - val thirdElement = x.values[2] - val thirdElementCondition = thirdElement is TsTestValue.TsUndefined + val thirdElement = x.values.getOrNull(2) + val thirdElementCondition = thirdElement == null || thirdElement is TsTestValue.TsUndefined + val resultMatches = r.values.size == x.values.size && r.values.zip(x.values).all { (actual, expected) -> + actual == expected || + actual is TsTestValue.TsClass && expected is TsTestValue.TsClass && actual.name == expected.name + } - (r.values == x.values) && firstElementCondition && secondElementCondition && thirdElementCondition + resultMatches && firstElementCondition && secondElementCondition && thirdElementCondition } ) } @@ -127,8 +131,11 @@ class InputArrays : TsMethodTestRunner() { r is TsTestValue.TsNull && value is TsTestValue.TsNumber && (value eq 1) }, { x, r -> - val value = x.values[0] - (r == value) && (value !is TsTestValue.TsNumber || (value neq 1)) + val value = x.values.firstOrNull() + val valueIsNotOne = value !is TsTestValue.TsNumber || (value neq 1) + val resultMatches = if (value == null) r is TsTestValue.TsUndefined else r == value + + valueIsNotOne && resultMatches }, ) } @@ -155,7 +162,7 @@ class InputArrays : TsMethodTestRunner() { resultCondition && fstCondition && sndCondition }, { x, y, r -> - val fst = x.values[0] + val fst = x.values.firstOrNull() val condition = fst !is TsTestValue.TsNumber || (fst neq 1) condition && r is TsTestValue.TsArray<*> && r.values == x.values }, diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 1fee530dff..25f4746236 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -341,6 +341,16 @@ open class TsTestStateResolver( "Other sorts must be resolved above, but got: $sort" } + val hasTypedOverrides = propertyState?.initializedTypedArrayOverrides?.any { candidate -> + model.eval(mkHeapRefEq(candidate, heapRef)).isTrue + } == true + if (resolveMode == ResolveMode.CURRENT && hasTypedOverrides) { + val hasBoxedValue = memory.read(typedArrayOverrideLValue(heapRef, index)) + if (model.eval(hasBoxedValue).isTrue) { + return@map resolveExpr(memory.read(typedArrayBoxedLValue(heapRef, index))) + } + } + val lValue = mkArrayIndexLValue(sort, heapRef, index, type) val value = memory.read(lValue) diff --git a/usvm-ts/src/test/resources/models/GlobalArrayAssignmentBoundary.ts b/usvm-ts/src/test/resources/models/GlobalArrayAssignmentBoundary.ts new file mode 100644 index 0000000000..6dbbbce8f4 --- /dev/null +++ b/usvm-ts/src/test/resources/models/GlobalArrayAssignmentBoundary.ts @@ -0,0 +1,11 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +const globalValues = [11, 22]; +globalValues[0.9] = 7; + +export class GlobalArrayAssignmentBoundary { + readSecondValue(): number { + return globalValues[1]; + } +} diff --git a/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts b/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts new file mode 100644 index 0000000000..a69494c314 --- /dev/null +++ b/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts @@ -0,0 +1,241 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +export class NumericBoundarySemantics { + mixedNumericUndefinedLiteral(): number { + const values: any[] = [123, undefined]; + return values[0] === 123 && values[1] === undefined ? 1 : 0; + } + + mixedBooleanNullLiteral(): number { + const values: any[] = [true, null]; + return values[0] === true && values[1] === null ? 1 : 0; + } + + mixedAliasWrites(): number { + const values = [123, 456]; + const alias: any[] = values; + alias[0] = null; + alias[1] = true; + let result = alias[0] === null && alias[1] === true ? 1 : 0; + alias[0] = 7; + result += alias[0] === 7 ? 2 : 0; + return result; + } + + mixedArrayShift(): number { + const values: any[] = [123, undefined]; + const first = values.shift(); + const second = values.shift(); + return first === 123 && second === undefined && values.length === 0 ? 1 : 0; + } + + mixedFakeNumberWrite(flag: boolean): number { + const values = [123]; + const alias: any[] = values; + const value: any = flag ? 7 : undefined; + alias[0] = value; + return flag ? (alias[0] === 7 ? 1 : 0) : (alias[0] === undefined ? 2 : 0); + } + + symbolicTypedInputWrites(values: number[]): number { + if (values.length < 2) return 0; + const alias: any[] = values; + alias[0] = null; + alias[1] = true; + return alias[0] === null && alias[1] === true ? 1 : -1; + } + + symbolicTypedAliases(values: number[], other: number[]): number { + if (values.length < 1 || other.length < 1) return 0; + const alias: any[] = values; + alias[0] = null; + const secondAlias: any[] = other; + const observed = secondAlias[0]; + if (values === other) return observed === null ? 1 : -1; + return alias[0] === null ? 2 : -1; + } + + bitwiseNaN(): number { + return (0 / 0) >> 1; + } + + bitwiseInfinity(): number { + return (1 / 0) >> 1; + } + + bitwiseUint32Wrap(): number { + return 4294967297 | 0; + } + + bitwiseFraction(): number { + return 1.9 | 0; + } + + bitwiseNegativeFraction(): number { + return -1.9 | 0; + } + + bitwiseNotNaN(): number { + return ~(0 / 0); + } + + bitwiseAndInfinity(): number { + return (1 / 0) & 7; + } + + bitwiseXorInfinity(): number { + return (1 / 0) ^ 7; + } + + leftShiftMasksCount(): number { + return 1 << 33; + } + + rightShiftTruncates(): number { + return -3.9 >> 1; + } + + unsignedRightShift(): number { + return -1.9 >>> 0; + } + + bitwiseNegativeZero(): number { + return -0 | 0; + } + + missingNumericArrayProperties(): number { + const values = [11, 22]; + let result = 0; + if (values[0 / 0] === undefined) result += 1; + if (values[1 / 0] === undefined) result += 2; + if (values[0.9] === undefined) result += 4; + if (values[-1] === undefined) result += 8; + if (values[2] === undefined) result += 16; + if (values[4294967297] === undefined) result += 32; + return result; + } + + negativeZeroArrayIndex(): number { + const values = [11, 22]; + return values[-0]; + } + + fractionalArrayWrite(): number { + const values = [11, 22]; + values[0.9] = 7; + return values[1]; + } + + negativeArrayWrite(): number { + const values = [11, 22]; + values[-1] = 7; + return values[1]; + } + + outOfRangeArrayWrite(): number { + const values = [11, 22]; + values[2] = 7; + return values[1]; + } + + negativeZeroArrayWrite(): number { + const values = [11, 22]; + values[-0] = 7; + return values[0]; + } + + chainedArrayRead(): number { + const values = [11, 22]; + const indices = [0, 1]; + return values[indices[1]]; + } + + chainedMissingArrayRead() { + const values = [11, 22]; + const indices = [0, 1]; + return values[indices[2]]; + } + + chainedMissingArrayWrite(): number { + const values = [11, 22]; + const indices = [0, 1]; + values[indices[2]] = 7; + return values[0]; + } + + stringArrayIndexRead(): number { + const values = [11, 22]; + return values["1"]; + } + + objectArrayIndexRead() { + const values = [11, 22]; + return values[{}]; + } + + stringZeroIndex(): string { + return "A😀B"[0]; + } + + stringNegativeZeroIndex(): string { + return "A😀B"[-0]; + } + + stringHighSurrogateIndex(): string { + return "A😀B"[1]; + } + + stringLowSurrogateIndex(): string { + return "A😀B"[2]; + } + + missingNumericStringProperties(): number { + const value = "abc"; + let result = 0; + if (value[0.9] === undefined) result += 1; + if (value[0 / 0] === undefined) result += 2; + if (value[1 / 0] === undefined) result += 4; + if (value[4294967297] === undefined) result += 8; + if (value[3] === undefined) result += 16; + return result; + } + + newArrayInfinity(): number { + return new Array(1 / 0).length; + } + + newArrayUint32Overflow(): number { + return new Array(4294967296).length; + } + + newArrayFraction(): number { + return new Array(1.9).length; + } + + newArrayBeyondModelCapacity(): number { + return new Array(17).length; + } + + newArrayNegativeZero(): number { + return new Array(-0).length; + } + + assignInvalidLength(): number { + const values = [11, 22]; + values.length = 1 / 0; + return values.length; + } + + assignLengthBeyondModelCapacity(): number { + const values = [11, 22]; + values.length = 17; + return values.length; + } + + assignNegativeZeroLength(): number { + const values = [11, 22]; + values.length = -0; + return values.length; + } +}