From ee6ce04f4bb8133eada0243de64710bbfe9826ca Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 19:56:40 +0300 Subject: [PATCH 1/3] Preserve bounded UTF-16 backing and model global Array.isArray --- .../usvm/machine/call/TsBuiltinGlobalType.kt | 5 + .../intrinsic/TsArrayIsArrayIntrinsicModel.kt | 88 +++++++++++ .../kotlin/org/usvm/machine/expr/ReadField.kt | 2 +- .../org/usvm/machine/expr/ReadLength.kt | 28 ++-- .../machine/expr/TsCapturedInstanceCall.kt | 5 + .../org/usvm/machine/expr/TsExprResolver.kt | 2 +- .../usvm/machine/interpreter/TsInterpreter.kt | 17 +- .../usvm/machine/operator/TsBinaryOperator.kt | 7 +- .../kotlin/org/usvm/machine/state/TsState.kt | 16 +- .../org/usvm/machine/state/TsStringBacking.kt | 2 +- .../main/kotlin/org/usvm/util/ArrayStorage.kt | 40 +++++ .../kotlin/org/usvm/util/StringStorage.kt | 97 ++++++++++++ .../call/StringModelBackingBoundaryTest.kt | 81 ++++++++++ .../call/TsArrayIsArrayIntrinsicModelTest.kt | 147 ++++++++++++++++++ .../call/TsUnknownCallModelCatalogTest.kt | 1 + .../kotlin/org/usvm/util/TsTestResolver.kt | 8 +- .../models/ArrayIsArrayIntrinsicModel.ts | 38 +++++ .../models/StringModelBackingBoundary.ts | 16 ++ 18 files changed, 576 insertions(+), 24 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/StringModelBackingBoundaryTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt create mode 100644 usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts create mode 100644 usvm-ts/src/test/resources/models/StringModelBackingBoundary.ts diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt index 288fc23f13..56eda2b05f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt @@ -1,6 +1,7 @@ package org.usvm.machine.call import org.jacodb.ets.model.EtsAnyType +import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsFunctionType import org.jacodb.ets.model.EtsLocal @@ -41,3 +42,7 @@ private fun EtsValue.isLegacyBuiltinGlobal( name == expectedName && type == EtsUnknownType && callee.enclosingClass == EtsClassSignature.UNKNOWN.copy(name = expectedName) + +internal fun EtsType.isBuiltinArrayGlobalType(): Boolean = this is EtsFunctionType && + signature.returnType is EtsArrayType && + signature.enclosingClass.file == EtsClassSignature.UNKNOWN.file diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt new file mode 100644 index 0000000000..c839d92c1e --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt @@ -0,0 +1,88 @@ +package org.usvm.machine.call.intrinsic + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.machine.call.TsUnknownCall +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.state.TsState + +/** Exact `Array.isArray` semantics for the genuine global `Array` built-in. */ +internal object TsArrayIsArrayIntrinsicModel : TsBuiltInUnknownCallModel { + const val MODEL_ID: String = "ts.array.isArray" + + private val anyArrayType = EtsArrayType(elementType = EtsUnknownType, dimensions = 1) + + override val id: String = MODEL_ID + override val target = TsUnknownCallTarget( + methodName = "isArray", + ) + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { + if (!call.hasGlobalArrayOwner()) { + return null + } + + val value = when { + call.arguments.isEmpty() -> return state.normalExecution(state.ctx.falseExpr) + else -> call.arguments.first().resolved ?: return null + } + val result = state.isArray(value) + + return state.normalExecution(result) + } + + private fun TsUnknownCall.hasGlobalArrayOwner(): Boolean { + val owner = receiver?.source as? EtsLocal ?: return false + val ownerType = owner.type as? EtsFunctionType ?: return false + val signatureFile = ownerType.signature.enclosingClass.file + + return owner.name == "Array" && + ownerType.signature.returnType is EtsArrayType && + signatureFile.projectName == UNKNOWN_SIGNATURE_COMPONENT && + signatureFile.fileName == UNKNOWN_SIGNATURE_COMPONENT + } + + private fun TsState.isArray(value: UExpr<*>) = with(ctx) { + when { + value.isFakeObject() -> { + val fakeType = value.getFakeType(memory) + val reference = value.extractRef(memory) + + mkAnd( + fakeType.refTypeExpr, + isNonNullArrayReference(reference), + ) + } + + value.sort == addressSort -> isNonNullArrayReference(value.asExpr(addressSort)) + else -> falseExpr + } + } + + private fun TsState.isNonNullArrayReference(reference: UHeapRef): UBoolExpr = with(ctx) { + val isDefined = mkNot(mkEq(reference, mkUndefinedValue())) + val isNonNull = mkNot(mkEq(reference, mkTsNullValue())) + + mkAnd(isDefined, isNonNull, memory.types.evalIsSubtype(reference, anyArrayType)) + } + + private fun TsState.normalExecution(result: UExpr<*>): TsUnknownCallModelExecution = with(ctx) { + val successor = TsUnknownCallModelSuccessor( + guard = trueExpr, + completion = TsUnknownCallModelCompletion.Normal { result }, + ) + + TsUnknownCallModelExecution(successors = listOf(successor)) + } + + private const val UNKNOWN_SIGNATURE_COMPONENT: String = "%unk" +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index 1bd686f5d5..62e588e7ee 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt @@ -394,7 +394,7 @@ private fun TsContext.materializeTypedStringField( val activeStringConstraints = mkImplies(activeGuard, constraints) scope.assert(activeStringConstraints) ?: return null - scope.doWithState { boundedStringBackingRefs += stringRef } + scope.doWithState { boundedStringBackingRefs += stringRef to maxStringLength } return stringRef } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt index b30f330466..f366f0dcf9 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadLength.kt @@ -17,8 +17,7 @@ import org.usvm.machine.interpreter.TsStepScope import org.usvm.sizeSort import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayLengthLValue -import org.usvm.util.mkStringBackingLValue -import org.usvm.util.mkStringBackingLengthLValue +import org.usvm.util.stringLength // Handles reading the `length` property. fun TsContext.readLengthProperty( @@ -29,6 +28,19 @@ fun TsContext.readLengthProperty( ): UExpr<*>? { // Determine the array type. val storageType = scope.calcOnState { arrayStorageType(instance, instanceLocal.type) } + if (storageType is EtsStringType) { + val length = scope.calcOnState { stringLength(instance) } + val lengthBound = scope.calcOnState { boundedStringBackingRefs[instance] ?: maxArraySize } + ensureLengthBounds(scope, length, lengthBound) ?: return null + + return mkBvToFpExpr( + sort = fp64Sort, + roundingMode = fpRoundingModeSortDefaultValue(), + value = length.asExpr(sizeSort), + signed = true, + ) + } + val arrayType: EtsArrayType = when (val type = storageType) { is EtsArrayType -> type @@ -38,18 +50,6 @@ fun TsContext.readLengthProperty( EtsArrayType(EtsUnknownType, dimensions = 1) } - is EtsStringType -> { - val charsRef = scope.calcOnState { - memory.read(mkStringBackingLValue(instance)) - } - - return readArrayLength( - scope = scope, - lengthLValue = mkStringBackingLengthLValue(charsRef), - maxArraySize = maxArraySize, - ) - } - else -> error("Expected EtsArrayType, EtsAnyType or EtsUnknownType, but got: $type") } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt index 2bb04e4ac7..135a8617ec 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt @@ -19,6 +19,7 @@ import org.usvm.USort import org.usvm.api.allocateConcreteRef import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isTrue +import org.usvm.machine.call.isBuiltinArrayGlobalType import org.usvm.machine.call.isBuiltinGlobalType import org.usvm.machine.state.lastStmt import org.usvm.util.getAllFields @@ -158,6 +159,10 @@ private fun isImplicitModeledGlobal(source: EtsLocal, callee: EtsMethodSignature return true } + if (source.type.isBuiltinArrayGlobalType()) { + return true + } + val modeled = when (source.name) { "Logger" -> true "Number" -> callee.name == "isNaN" 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 283441ffc6..dd7bc6b699 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 @@ -774,7 +774,7 @@ class TsExprResolver( guard = trueExpr, ) memory.write(mkStringBackingLengthLValue(resultChars), resultLength, guard = trueExpr) - boundedStringBackingRefs += result + boundedStringBackingRefs += result to options.maxArraySize memory.memcpy( srcRef = leftChars, 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 0b5757cc7a..5b9e6ab11e 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 @@ -40,6 +40,7 @@ import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UExpr import org.usvm.UInterpreter +import org.usvm.USort import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArray import org.usvm.api.targets.TsTarget @@ -775,7 +776,12 @@ class TsInterpreter( unknownCallDispatcher = unknownCallDispatcher, ) - fun getInitialState(method: EtsMethod, targets: List): TsState = with(ctx) { + fun getInitialState( + method: EtsMethod, + targets: List, + configure: (TsState) -> Unit = {}, + parameterSortOverride: (Int) -> USort? = { null }, + ): TsState = with(ctx) { val state = TsState( ctx = ctx, ownership = MutabilityOwnership(), @@ -803,6 +809,11 @@ class TsInterpreter( method.parameters.forEachIndexed { i, param -> val idx = i + 1 // +1 because 0 is reserved for `this` + val overriddenSort = parameterSortOverride(idx) + if (overriddenSort != null) { + state.saveSortForLocal(idx, overriddenSort) + return@forEachIndexed + } val ref by lazy { val lValue = mkRegisterStackLValue(addressSort, idx) @@ -851,7 +862,7 @@ class TsInterpreter( state.pathConstraints += state.memory.types.evalTypeEquals(ref, EtsStringType) state.pathConstraints += state.symbolicStringBackingConstraint(ref) - state.boundedStringBackingRefs += ref + state.boundedStringBackingRefs += ref to state.maxStringLength } val parameterSort = typeToSort(parameterType) @@ -869,6 +880,8 @@ class TsInterpreter( } } + configure(state) + val solver = solver() val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt index 3a9ef594eb..5b6842bffe 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/operator/TsBinaryOperator.kt @@ -86,7 +86,10 @@ private fun TsContext.stringValueEquals( rhsChars = rhsChars, lhsLength = lhsLength, rhsLength = rhsLength, - maxLength = maxStringLength, + maxLength = maxOf( + boundedStringBackingRefs[lhs] ?: maxStringLength, + boundedStringBackingRefs[rhs] ?: maxStringLength, + ), ) } @@ -119,7 +122,7 @@ private fun TsContext.stringValueEquals( boundedLengths, ) scope.fork(supported, blockOnFalseState = { - terminateAsUnsupported(reason = "String equality requires symbolic string length in 0..$maxStringLength") + terminateAsUnsupported(reason = "String equality requires symbolic string length in 0..${comparison.maxLength}") }) ?: return null // Known literals supply a tighter comparison bound; all other string lengths are constrained above. 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 29056d7dfe..daed206637 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 @@ -1,5 +1,6 @@ package org.usvm.machine.state +import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBlockCfg import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsFile @@ -32,6 +33,7 @@ import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.TsFunction import org.usvm.memory.ULValue import org.usvm.memory.UMemory +import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.model.UModelBase import org.usvm.sizeSort import org.usvm.targets.UTargetsSet @@ -87,11 +89,11 @@ class TsState( */ var stringConstantAllocatedRefs: UPersistentHashMap = persistentHashMapOf(), /** - * References whose string backing and length bound have been modeled. + * Maps references with modeled string backing to their maximum length. * A new symbolic string producer must register its reference here after creating the backing model. * String literals are recognized separately through [TsContext.getStringConstantValue]. */ - var boundedStringBackingRefs: Set = emptySet(), + var boundedStringBackingRefs: Map = emptyMap(), /** Unresolved reference payloads that may acquire string backing after type refinement. */ var symbolicStringCandidates: Set = emptySet(), /** Exception delivered to the current catch block, before its binding is initialized. */ @@ -100,6 +102,7 @@ class TsState( var trackedObjectProperties: Set = emptySet(), var writtenConcreteFields: Set> = emptySet(), var writtenObjectLiteralFieldSorts: UPersistentHashMap, USort> = persistentHashMapOf(), + internal val denseInputArrays: MutableMap = mutableMapOf(), private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( ctx = ctx, @@ -300,6 +303,7 @@ class TsState( ref } stringConstantAllocatedRefs = updated + boundedStringBackingRefs += result to value.length result } @@ -347,6 +351,7 @@ class TsState( trackedObjectProperties = trackedObjectProperties, writtenConcreteFields = writtenConcreteFields, writtenObjectLiteralFieldSorts = writtenObjectLiteralFieldSorts, + denseInputArrays = denseInputArrays.toMutableMap(), activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ) } @@ -354,3 +359,10 @@ class TsState( override val isExceptional: Boolean get() = methodResult is TsMethodResult.TsException } + +/** Snapshot of the storage regions that establish dense input-array contents. */ +data class TsDenseInputArray( + val type: EtsArrayType, + val lengthRegion: UReadOnlyMemoryRegion<*, *>, + val elementRegion: UReadOnlyMemoryRegion<*, *>, +) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt index 55a87920ed..91b181f1b4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsStringBacking.kt @@ -70,7 +70,7 @@ internal fun TsStepScope.prepareRefinedStringBackings(): Unit? { val backingConstraint = calcOnState { symbolicStringBackingConstraint(ref) } assert(backingConstraint) ?: return null doWithState { - boundedStringBackingRefs += ref + boundedStringBackingRefs += ref to maxStringLength symbolicStringCandidates -= ref } } 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..b308634a5e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt @@ -14,11 +14,14 @@ import org.usvm.USort import org.usvm.api.memcpy import org.usvm.collection.array.UArrayRegion import org.usvm.collection.array.UArrayRegionId +import org.usvm.collection.array.length.UArrayLengthsRegionId import org.usvm.machine.TsContext import org.usvm.machine.TsSizeSort import org.usvm.machine.expr.TsUnresolvedSort +import org.usvm.machine.state.TsDenseInputArray import org.usvm.machine.state.TsState import org.usvm.machine.types.TsUnresolvedArrayKind +import org.usvm.sizeSort /** Enumerates payload regions independently of whether an array was allocated or came from the input. */ internal inline fun TsContext.forEachArrayPayloadRegion(arrayType: EtsArrayType, action: (EtsType, USort) -> Unit) { @@ -73,3 +76,40 @@ internal fun TsState.initializeArrayKind( ) memory.setRegion(regionId, initialized) } + +/** Records that every slot below the current input length has an initialized value. */ +fun TsState.markDenseInputArray( + array: UConcreteHeapRef, + type: EtsArrayType, +) = with(ctx) { + val descriptor = arrayDescriptorOf(type) + val elementSort = typeToSort(type.elementType) + require(elementSort !is TsUnresolvedSort) { "A dense input array needs a concrete element sort" } + + val lengthRegionId = UArrayLengthsRegionId(sizeSort, descriptor) + val elementRegionId = UArrayRegionId(descriptor, elementSort) + denseInputArrays[array] = TsDenseInputArray( + type = type, + lengthRegion = memory.getRegion(lengthRegionId), + elementRegion = memory.getRegion(elementRegionId), + ) +} + +/** Returns true only while neither the recorded length nor payload region has changed. */ +internal fun TsState.isUnmodifiedDenseInputArray( + array: UConcreteHeapRef, + type: EtsArrayType, +): Boolean = with(ctx) { + val snapshot = denseInputArrays[array] ?: return false + if (snapshot.type != type) return false + + val descriptor = arrayDescriptorOf(type) + val elementSort = typeToSort(type.elementType) + if (elementSort is TsUnresolvedSort) return false + + val lengthRegionId = UArrayLengthsRegionId(sizeSort, descriptor) + val elementRegionId = UArrayRegionId(descriptor, elementSort) + + memory.getRegion(lengthRegionId) === snapshot.lengthRegion && + memory.getRegion(elementRegionId) === snapshot.elementRegion +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt new file mode 100644 index 0000000000..a07f72f8fe --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt @@ -0,0 +1,97 @@ +package org.usvm.util + +import io.ksmt.sort.KFp64Sort +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStringType +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.api.initializeArrayLength +import org.usvm.api.memcpy +import org.usvm.machine.TsSizeSort +import org.usvm.machine.state.TsState +import org.usvm.sizeSort + +internal val STRING_CHARACTER_ARRAY_TYPE = EtsArrayType(EtsNumberType, dimensions = 1) + +internal fun TsState.stringCharacters(receiver: UHeapRef): UHeapRef = with(ctx) { + memory.read(mkStringBackingLValue(receiver)).asExpr(addressSort) +} + +internal fun TsState.stringLength(receiver: UHeapRef): UExpr { + val characters = stringCharacters(receiver) + return memory.read(mkStringBackingLengthLValue(characters)) +} + +fun TsState.markStringMaxLength( + string: UConcreteHeapRef, + maxLength: Int, +) { + require(maxLength >= 0) { "String maximum length must be non-negative" } + boundedStringBackingRefs += string to maxLength +} + +private fun TsState.trackedStringMaxLength(string: UHeapRef): Int? = + boundedStringBackingRefs[string] + +internal fun TsState.allocateString( + length: UExpr, + maxLength: Int? = null, +): Pair = with(ctx) { + val string = memory.allocConcrete(EtsStringType) + val characters = memory.allocConcrete(STRING_CHARACTER_ARRAY_TYPE.elementType) + memory.initializeArrayLength( + arrayHeapRef = characters, + type = stringBackingArrayDescriptor, + sizeSort = sizeSort, + count = length, + ) + memory.write( + mkStringBackingLValue(string), + characters, + guard = trueExpr, + ) + if (maxLength != null) { + markStringMaxLength(string = string, maxLength = maxLength) + } + + string to characters +} + +internal fun TsState.copyStringRange( + receiver: UHeapRef, + from: UExpr, + length: UExpr, +): UConcreteHeapRef = with(ctx) { + val source = stringCharacters(receiver) + val (result, destination) = allocateString(length, maxLength = trackedStringMaxLength(receiver)) + memory.memcpy( + source, + destination, + stringBackingArrayDescriptor, + bv16Sort, + fromSrc = from, + fromDst = mkBv(0), + length = length, + ) + result +} + +internal fun TsState.stringFromCodeUnit(codeUnit: UExpr): UConcreteHeapRef = with(ctx) { + val (result, characters) = allocateString(mkBv(1), maxLength = 1) + val value = mkFpToBvExpr( + roundingMode = fpRoundingModeSortDefaultValue(), + value = codeUnit, + bvSize = bv16Sort.sizeBits.toInt(), + isSigned = false, + ).asExpr(bv16Sort) + val character = mkStringBackingElementLValue(ref = characters, index = mkBv(0)) + memory.write( + character, + value, + guard = trueExpr, + ) + result +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/StringModelBackingBoundaryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/StringModelBackingBoundaryTest.kt new file mode 100644 index 0000000000..3c97711091 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/StringModelBackingBoundaryTest.kt @@ -0,0 +1,81 @@ +package org.usvm.machine.call + +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.junit.jupiter.api.Test +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.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import kotlin.test.assertTrue + +class StringModelBackingBoundaryTest : TsMethodTestRunner() { + override val scene = EtsScene( + listOf( + loadEtsFileAutoConvert( + getResourcePath("/models/StringModelBackingBoundary.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + + override val runner: (EtsMethod, UMachineOptions) -> List = { method, options -> + TsMachine(scene = scene, options = options, tsOptions = TsOptions(maxArraySize = 12)).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + @Test + fun `derived strings compare their full contents within the configured bound`() { + discoverProperties( + method = getMethod(methodName = "equalDerived", className = "StringModelBackingBoundary"), + { _, result -> result.value }, + invariants = arrayOf({ _, result -> result.value }), + ) + } + + @Test + fun `derived string length uses the configured bound`() { + discoverProperties( + method = getMethod(methodName = "derivedLength", className = "StringModelBackingBoundary"), + { input, result -> result.number == input.value.length + 10.0 }, + invariants = arrayOf({ input, result -> result.number == input.value.length + 10.0 }), + ) + } + + @Test + fun `derived string witnesses retain their full contents`() { + discoverProperties( + method = getMethod(methodName = "returnedDerived", className = "StringModelBackingBoundary"), + { input, result -> result.value == input.value + "0123456789" }, + invariants = arrayOf({ input, result -> result.value == input.value + "0123456789" }), + ) + } + + @Test + fun `concatenation beyond the configured bound remains unsupported`() { + for (methodName in listOf("equalDerived", "derivedLength", "returnedDerived")) { + val method = getMethod(methodName = methodName, className = "StringModelBackingBoundary") + + val analysis = TsMachine( + scene = scene, + options = UMachineOptions(), + tsOptions = TsOptions(maxArraySize = 2), + ).use { machine -> + machine.analyzeWithOutcome(methods = listOf(method)) + } + + assertTrue(analysis.states.isEmpty(), methodName) + assertTrue( + analysis.unsupportedPaths.any { "result exceeds the configured length bound" in it }, + "$methodName: ${analysis.unsupportedPaths}", + ) + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt new file mode 100644 index 0000000000..5357ecd578 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt @@ -0,0 +1,147 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +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.call.intrinsic.TsArrayIsArrayIntrinsicModel +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsArrayIsArrayIntrinsicModelTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/ArrayIsArrayIntrinsicModel.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(projectFiles = listOf(sourceFile)) + + @Test + fun `scalars are not arrays`() { + val result = analyze("scalarValuesAreNotArrays", "missingArgumentIsNotArray") + + assertTrue(result.values.values.all { values -> assertIs(values.single()).value }) + assertEquals( + List(size = 6) { TsArrayIsArrayIntrinsicModel.MODEL_ID }, + result.modelIds, + ) + } + + @Test + fun `ordinary arrays are arrays`() { + val result = analyze("ordinaryArraysAreArrays") + + assertTrue(assertIs(result.values.getValue("ordinaryArraysAreArrays").single()).value) + assertEquals( + List(size = 2) { TsArrayIsArrayIntrinsicModel.MODEL_ID }, + result.modelIds, + ) + } + + @Test + fun `null and undefined parameters are not arrays`() { + val result = analyze("nullParameterIsNotArray", "undefinedParameterIsNotArray") + + result.values.values.forEach { values -> + assertFalse(assertIs(values.single()).value) + } + assertEquals( + List(size = 2) { TsArrayIsArrayIntrinsicModel.MODEL_ID }, + result.modelIds, + ) + } + + @Test + fun `string and nested array parameters are arrays`() { + val result = analyze("stringArrayIsArray", "nestedArrayIsArray") + + result.values.values.forEach { values -> + assertTrue(assertIs(values.single()).value) + } + assertEquals( + List(size = 2) { TsArrayIsArrayIntrinsicModel.MODEL_ID }, + result.modelIds, + ) + } + + @Test + fun `non builtin isArray call is not claimed by the model`() { + val result = analyze("nonBuiltinIsArrayFallsBack") + + assertTrue(result.modelIds.isEmpty()) + assertTrue(result.events.none { event -> event.outcome == TsUnknownCallOutcome.MODEL_APPLIED }) + } + + private fun analyze(vararg methodNames: String): AnalysisResult { + val methods = methodNames.associateWith(::method) + val observer = RecordingUnknownCallObserver() + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(unknownCallFallback = TsResidualCallPolicy.STOP_PATH), + observer = observer, + ).use { machine -> + val states = machine.analyze(methods.values.toList()) + val values = methods.mapValues { (_, method) -> + states.filter { state -> state.entrypoint === method } + .map { state -> TsTestResolver().resolve(method, state).returnValue } + } + + AnalysisResult( + values = values, + events = observer.events.toList(), + ) + } + } + + private fun method(name: String): EtsMethod = scene.projectClasses + .single { clazz -> clazz.name == DEFAULT_ARK_CLASS_NAME && clazz.declaringFile === sourceFile } + .methods + .single { method -> method.name == name } + + private class RecordingUnknownCallObserver : TsInterpreterObserver { + val events = mutableListOf() + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + private data class AnalysisResult( + val values: Map>, + val events: List, + ) { + val modelIds: List = events.mapNotNull { event -> + (event.decision as? TsUnknownCallDecision.ModelApplied)?.modelId + } + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 1_000L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} 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 77d8018b3a..4de5a89b20 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 @@ -152,6 +152,7 @@ class TsUnknownCallModelCatalogTest { val catalog = TsBuiltInUnknownCallModels.catalog() val expectedModelIds = listOf( + "ts.array.isArray", "ts.array.pop", TsArrayShiftIntrinsicModel.MODEL_ID, TsNumericIntrinsicModelFamily.MATH_ABS_ID, 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 9dd242ac27..1fee530dff 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -79,6 +79,7 @@ class TsTestResolver { method, resolvedLValuesToFakeObjects, state.maxStringLength, + stringLengthBounds = state.boundedStringBackingRefs, propertyState = state, ) val afterMemoryScope = MemoryScope( @@ -88,6 +89,7 @@ class TsTestResolver { method, resolvedLValuesToFakeObjects, state.maxStringLength, + stringLengthBounds = state.boundedStringBackingRefs, propertyState = state, ) @@ -193,6 +195,7 @@ class TsTestResolver { method: EtsMethod, resolvedLValuesToFakeObjects: List, UConcreteHeapRef>>, maxStringLength: Int, + stringLengthBounds: Map, propertyState: TsState, ) : TsTestStateResolver( ctx = ctx, @@ -201,6 +204,7 @@ class TsTestResolver { method = method, resolvedLValuesToFakeObjects = resolvedLValuesToFakeObjects, maxStringLength = maxStringLength, + stringLengthBounds = stringLengthBounds, propertyState = propertyState, ) { fun resolveState(): TsParametersState { @@ -219,6 +223,7 @@ open class TsTestStateResolver( val method: EtsMethod, val resolvedLValuesToFakeObjects: List, UConcreteHeapRef>>, val maxStringLength: Int, + private val stringLengthBounds: Map = emptyMap(), private val propertyState: TsState? = null, ) { private val resolvedClasses = hashMapOf() @@ -370,7 +375,8 @@ open class TsTestStateResolver( val lengthLValue = mkStringBackingLengthLValue(charsRef) val length = evaluateInModel(stringMemory.read(lengthLValue)).extractInt() - require(length in 0..maxStringLength) { "Unsupported symbolic string length: $length" } + val lengthBound = stringLengthBounds[heapRef] ?: stringLengthBounds[concreteRef] ?: maxStringLength + require(length in 0..lengthBound) { "Unsupported symbolic string length: $length" } val value = buildString(length) { repeat(length) { index -> diff --git a/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts b/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts new file mode 100644 index 0000000000..22515dc2ed --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts @@ -0,0 +1,38 @@ +export function scalarValuesAreNotArrays(): boolean { + return !Array.isArray(42) + && !Array.isArray(true) + && !Array.isArray('value') + && !Array.isArray(undefined) + && !Array.isArray(null); +} + +export function ordinaryArraysAreArrays(): boolean { + return Array.isArray([]) && Array.isArray([1, 2, 3]); +} + +export function stringArrayIsArray(value: string[]): boolean { + return Array.isArray(value); +} + +export function nestedArrayIsArray(value: number[][]): boolean { + return Array.isArray(value); +} + +export function missingArgumentIsNotArray(): boolean { + // @ts-expect-error Arity test deliberately omits the first argument. + return !Array.isArray(); +} + +export function nullParameterIsNotArray(value: null): boolean { + return Array.isArray(value); +} + +export function undefinedParameterIsNotArray(value: undefined): boolean { + return Array.isArray(value); +} + +declare const FakeArray: any; + +export function nonBuiltinIsArrayFallsBack(): boolean { + return FakeArray.isArray([]); +} diff --git a/usvm-ts/src/test/resources/models/StringModelBackingBoundary.ts b/usvm-ts/src/test/resources/models/StringModelBackingBoundary.ts new file mode 100644 index 0000000000..7f01e2b21c --- /dev/null +++ b/usvm-ts/src/test/resources/models/StringModelBackingBoundary.ts @@ -0,0 +1,16 @@ +export class StringModelBackingBoundary { + equalDerived(value: string): boolean { + const left = value + "0123456789"; + const right = value + "0123456789"; + + return left === right; + } + + derivedLength(value: string): number { + return (value + "0123456789").length; + } + + returnedDerived(value: string): string { + return value + "0123456789"; + } +} From 20e933571b8877948c1b58547df019a39f1f9828 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 20:13:46 +0300 Subject: [PATCH 2/3] Keep standalone backing changes free of unused model prerequisites --- .../usvm/machine/interpreter/TsInterpreter.kt | 15 +--- .../kotlin/org/usvm/machine/state/TsState.kt | 11 --- .../main/kotlin/org/usvm/util/ArrayStorage.kt | 40 --------- .../kotlin/org/usvm/util/StringStorage.kt | 81 ------------------- 4 files changed, 1 insertion(+), 146 deletions(-) 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 5b9e6ab11e..645b098471 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 @@ -40,7 +40,6 @@ import org.usvm.StepResult import org.usvm.StepScope import org.usvm.UExpr import org.usvm.UInterpreter -import org.usvm.USort import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArray import org.usvm.api.targets.TsTarget @@ -776,12 +775,7 @@ class TsInterpreter( unknownCallDispatcher = unknownCallDispatcher, ) - fun getInitialState( - method: EtsMethod, - targets: List, - configure: (TsState) -> Unit = {}, - parameterSortOverride: (Int) -> USort? = { null }, - ): TsState = with(ctx) { + fun getInitialState(method: EtsMethod, targets: List): TsState = with(ctx) { val state = TsState( ctx = ctx, ownership = MutabilityOwnership(), @@ -809,11 +803,6 @@ class TsInterpreter( method.parameters.forEachIndexed { i, param -> val idx = i + 1 // +1 because 0 is reserved for `this` - val overriddenSort = parameterSortOverride(idx) - if (overriddenSort != null) { - state.saveSortForLocal(idx, overriddenSort) - return@forEachIndexed - } val ref by lazy { val lValue = mkRegisterStackLValue(addressSort, idx) @@ -880,8 +869,6 @@ class TsInterpreter( } } - configure(state) - val solver = solver() val model = solver.check(state.pathConstraints).ensureSat().model state.models = listOf(model) 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 daed206637..89e5b4064b 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 @@ -1,6 +1,5 @@ package org.usvm.machine.state -import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBlockCfg import org.jacodb.ets.model.EtsClass import org.jacodb.ets.model.EtsFile @@ -33,7 +32,6 @@ import org.usvm.machine.interpreter.PromiseState import org.usvm.machine.interpreter.TsFunction import org.usvm.memory.ULValue import org.usvm.memory.UMemory -import org.usvm.memory.UReadOnlyMemoryRegion import org.usvm.model.UModelBase import org.usvm.sizeSort import org.usvm.targets.UTargetsSet @@ -102,7 +100,6 @@ class TsState( var trackedObjectProperties: Set = emptySet(), var writtenConcreteFields: Set> = emptySet(), var writtenObjectLiteralFieldSorts: UPersistentHashMap, USort> = persistentHashMapOf(), - internal val denseInputArrays: MutableMap = mutableMapOf(), private val activeUnknownCallModels: MutableList> = mutableListOf(), ) : UState( ctx = ctx, @@ -351,7 +348,6 @@ class TsState( trackedObjectProperties = trackedObjectProperties, writtenConcreteFields = writtenConcreteFields, writtenObjectLiteralFieldSorts = writtenObjectLiteralFieldSorts, - denseInputArrays = denseInputArrays.toMutableMap(), activeUnknownCallModels = activeUnknownCallModels.toMutableList(), ) } @@ -359,10 +355,3 @@ class TsState( override val isExceptional: Boolean get() = methodResult is TsMethodResult.TsException } - -/** Snapshot of the storage regions that establish dense input-array contents. */ -data class TsDenseInputArray( - val type: EtsArrayType, - val lengthRegion: UReadOnlyMemoryRegion<*, *>, - val elementRegion: UReadOnlyMemoryRegion<*, *>, -) 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 b308634a5e..3cd941ce4b 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/ArrayStorage.kt @@ -14,14 +14,11 @@ import org.usvm.USort import org.usvm.api.memcpy import org.usvm.collection.array.UArrayRegion import org.usvm.collection.array.UArrayRegionId -import org.usvm.collection.array.length.UArrayLengthsRegionId import org.usvm.machine.TsContext import org.usvm.machine.TsSizeSort import org.usvm.machine.expr.TsUnresolvedSort -import org.usvm.machine.state.TsDenseInputArray import org.usvm.machine.state.TsState import org.usvm.machine.types.TsUnresolvedArrayKind -import org.usvm.sizeSort /** Enumerates payload regions independently of whether an array was allocated or came from the input. */ internal inline fun TsContext.forEachArrayPayloadRegion(arrayType: EtsArrayType, action: (EtsType, USort) -> Unit) { @@ -76,40 +73,3 @@ internal fun TsState.initializeArrayKind( ) memory.setRegion(regionId, initialized) } - -/** Records that every slot below the current input length has an initialized value. */ -fun TsState.markDenseInputArray( - array: UConcreteHeapRef, - type: EtsArrayType, -) = with(ctx) { - val descriptor = arrayDescriptorOf(type) - val elementSort = typeToSort(type.elementType) - require(elementSort !is TsUnresolvedSort) { "A dense input array needs a concrete element sort" } - - val lengthRegionId = UArrayLengthsRegionId(sizeSort, descriptor) - val elementRegionId = UArrayRegionId(descriptor, elementSort) - denseInputArrays[array] = TsDenseInputArray( - type = type, - lengthRegion = memory.getRegion(lengthRegionId), - elementRegion = memory.getRegion(elementRegionId), - ) -} - -/** Returns true only while neither the recorded length nor payload region has changed. */ -internal fun TsState.isUnmodifiedDenseInputArray( - array: UConcreteHeapRef, - type: EtsArrayType, -): Boolean = with(ctx) { - val snapshot = denseInputArrays[array] ?: return false - if (snapshot.type != type) return false - - val descriptor = arrayDescriptorOf(type) - val elementSort = typeToSort(type.elementType) - if (elementSort is TsUnresolvedSort) return false - - val lengthRegionId = UArrayLengthsRegionId(sizeSort, descriptor) - val elementRegionId = UArrayRegionId(descriptor, elementSort) - - memory.getRegion(lengthRegionId) === snapshot.lengthRegion && - memory.getRegion(elementRegionId) === snapshot.elementRegion -} diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt index a07f72f8fe..85df73a850 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/StringStorage.kt @@ -1,20 +1,10 @@ package org.usvm.util -import io.ksmt.sort.KFp64Sort import io.ksmt.utils.asExpr -import org.jacodb.ets.model.EtsArrayType -import org.jacodb.ets.model.EtsNumberType -import org.jacodb.ets.model.EtsStringType -import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef -import org.usvm.api.initializeArrayLength -import org.usvm.api.memcpy import org.usvm.machine.TsSizeSort import org.usvm.machine.state.TsState -import org.usvm.sizeSort - -internal val STRING_CHARACTER_ARRAY_TYPE = EtsArrayType(EtsNumberType, dimensions = 1) internal fun TsState.stringCharacters(receiver: UHeapRef): UHeapRef = with(ctx) { memory.read(mkStringBackingLValue(receiver)).asExpr(addressSort) @@ -24,74 +14,3 @@ internal fun TsState.stringLength(receiver: UHeapRef): UExpr { val characters = stringCharacters(receiver) return memory.read(mkStringBackingLengthLValue(characters)) } - -fun TsState.markStringMaxLength( - string: UConcreteHeapRef, - maxLength: Int, -) { - require(maxLength >= 0) { "String maximum length must be non-negative" } - boundedStringBackingRefs += string to maxLength -} - -private fun TsState.trackedStringMaxLength(string: UHeapRef): Int? = - boundedStringBackingRefs[string] - -internal fun TsState.allocateString( - length: UExpr, - maxLength: Int? = null, -): Pair = with(ctx) { - val string = memory.allocConcrete(EtsStringType) - val characters = memory.allocConcrete(STRING_CHARACTER_ARRAY_TYPE.elementType) - memory.initializeArrayLength( - arrayHeapRef = characters, - type = stringBackingArrayDescriptor, - sizeSort = sizeSort, - count = length, - ) - memory.write( - mkStringBackingLValue(string), - characters, - guard = trueExpr, - ) - if (maxLength != null) { - markStringMaxLength(string = string, maxLength = maxLength) - } - - string to characters -} - -internal fun TsState.copyStringRange( - receiver: UHeapRef, - from: UExpr, - length: UExpr, -): UConcreteHeapRef = with(ctx) { - val source = stringCharacters(receiver) - val (result, destination) = allocateString(length, maxLength = trackedStringMaxLength(receiver)) - memory.memcpy( - source, - destination, - stringBackingArrayDescriptor, - bv16Sort, - fromSrc = from, - fromDst = mkBv(0), - length = length, - ) - result -} - -internal fun TsState.stringFromCodeUnit(codeUnit: UExpr): UConcreteHeapRef = with(ctx) { - val (result, characters) = allocateString(mkBv(1), maxLength = 1) - val value = mkFpToBvExpr( - roundingMode = fpRoundingModeSortDefaultValue(), - value = codeUnit, - bvSize = bv16Sort.sizeBits.toInt(), - isSigned = false, - ).asExpr(bv16Sort) - val character = mkStringBackingElementLValue(ref = characters, index = mkBv(0)) - memory.write( - character, - value, - guard = trueExpr, - ) - result -} From b05aabcfe28ebabb1b2d7d6f80d4b8f525deab51 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 20:15:22 +0300 Subject: [PATCH 3/3] Handle conditional fake values in Array.isArray --- .../call/intrinsic/TsArrayIsArrayIntrinsicModel.kt | 10 +++++++++- .../machine/call/TsArrayIsArrayIntrinsicModelTest.kt | 12 ++++++++++++ .../resources/models/ArrayIsArrayIntrinsicModel.ts | 4 ++++ 3 files changed, 25 insertions(+), 1 deletion(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt index c839d92c1e..6f431b2382 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt @@ -8,6 +8,7 @@ import org.jacodb.ets.model.EtsUnknownType import org.usvm.UBoolExpr import org.usvm.UExpr import org.usvm.UHeapRef +import org.usvm.UIteExpr import org.usvm.machine.call.TsUnknownCall import org.usvm.machine.call.TsUnknownCallModelCompletion import org.usvm.machine.call.TsUnknownCallModelExecution @@ -51,8 +52,15 @@ internal object TsArrayIsArrayIntrinsicModel : TsBuiltInUnknownCallModel { signatureFile.fileName == UNKNOWN_SIGNATURE_COMPONENT } - private fun TsState.isArray(value: UExpr<*>) = with(ctx) { + private fun TsState.isArray(value: UExpr<*>): UBoolExpr = with(ctx) { when { + value is UIteExpr<*> -> { + val trueResult = isArray(value.trueBranch) + val falseResult = isArray(value.falseBranch) + + mkIte(value.condition, trueResult, falseResult) + } + value.isFakeObject() -> { val fakeType = value.getFakeType(memory) val reference = value.extractRef(memory) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt index 5357ecd578..9420884b8b 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt @@ -78,6 +78,18 @@ class TsArrayIsArrayIntrinsicModelTest { ) } + @Test + fun `conditional any arguments preserve both array and non array outcomes`() { + val result = analyze("nullishAnyArrayFallback") + val outcomes = result.values.getValue("nullishAnyArrayFallback").map { value -> + assertIs(value).value + }.toSet() + + assertEquals(setOf(false, true), outcomes) + assertTrue(result.modelIds.isNotEmpty()) + assertTrue(result.modelIds.all { modelId -> modelId == TsArrayIsArrayIntrinsicModel.MODEL_ID }) + } + @Test fun `non builtin isArray call is not claimed by the model`() { val result = analyze("nonBuiltinIsArrayFallsBack") diff --git a/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts b/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts index 22515dc2ed..577b14f61e 100644 --- a/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts +++ b/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts @@ -36,3 +36,7 @@ declare const FakeArray: any; export function nonBuiltinIsArrayFallsBack(): boolean { return FakeArray.isArray([]); } + +export function nullishAnyArrayFallback(value: any): boolean { + return Array.isArray(value ?? []); +}