From 22b546968d9405100fee386d6d1fcceaa266e98a Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 01:06:06 +0300 Subject: [PATCH 1/9] Preserve Error field runtime values and symbolic string messages --- usvm-ts/UNKNOWN_CALL_MODELS.md | 14 +- .../org/usvm/machine/TsInterpreterObserver.kt | 1 + .../call/intrinsic/TsArrayEtsIrModelFamily.kt | 120 ++++++++++++- .../call/intrinsic/TsErrorEtsIrModelFamily.kt | 103 +++++++++++ .../intrinsic/TsStringEtsIrModelFamily.kt | 23 ++- .../usvm/machine/expr/ErrorModelStorage.kt | 105 +++++++++++ .../kotlin/org/usvm/machine/expr/ReadField.kt | 40 +++-- .../org/usvm/machine/expr/TsExprResolver.kt | 75 ++++---- .../org/usvm/machine/expr/WriteField.kt | 21 +++ .../usvm/machine/call/models/ArrayModels.ts | 5 + .../usvm/machine/call/models/ErrorModels.ts | 13 ++ .../usvm/machine/call/models/StringModels.ts | 60 +++++++ .../call/ErrorModelBackingBoundaryTest.kt | 81 +++++++++ .../call/ErrorModelOwnerBoundaryTest.kt | 54 ++++++ .../call/TsArrayConstructorEtsIrModelTest.kt | 170 ++++++++++++++++++ .../machine/call/TsArrayShiftReplayTest.kt | 56 ++++++ .../machine/call/TsErrorEtsIrModelTest.kt | 147 +++++++++++++++ .../call/TsErrorSourceSemanticsTest.kt | 114 ++++++++++++ .../call/TsStringReplaceAllEtsIrModelTest.kt | 103 +++++++++++ .../call/TsUnknownCallModelCatalogTest.kt | 5 + .../expr/NumericBoundarySemanticsTest.kt | 1 + .../resources/models/ArrayConstructorEtsIr.ts | 64 +++++++ .../src/test/resources/models/ErrorEtsIr.ts | 77 ++++++++ .../models/ErrorModelBackingBoundary.ts | 12 ++ .../models/NumericBoundarySemantics.ts | 5 + .../resources/models/StringReplaceAllEtsIr.ts | 42 +++++ .../resources/models/UserDefinedErrorEtsIr.ts | 14 ++ .../array-constructor-shadow/exported.ts | 3 + .../models/array-constructor-shadow/main.ts | 10 ++ .../models/error-storage-owner/ErrorModels.ts | 16 ++ 30 files changed, 1490 insertions(+), 64 deletions(-) create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt create mode 100644 usvm-ts/src/main/resources/org/usvm/machine/call/models/ErrorModels.ts create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/ErrorModelBackingBoundaryTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/ErrorModelOwnerBoundaryTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayConstructorEtsIrModelTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsStringReplaceAllEtsIrModelTest.kt create mode 100644 usvm-ts/src/test/resources/models/ArrayConstructorEtsIr.ts create mode 100644 usvm-ts/src/test/resources/models/ErrorEtsIr.ts create mode 100644 usvm-ts/src/test/resources/models/ErrorModelBackingBoundary.ts create mode 100644 usvm-ts/src/test/resources/models/StringReplaceAllEtsIr.ts create mode 100644 usvm-ts/src/test/resources/models/UserDefinedErrorEtsIr.ts create mode 100644 usvm-ts/src/test/resources/models/array-constructor-shadow/exported.ts create mode 100644 usvm-ts/src/test/resources/models/array-constructor-shadow/main.ts create mode 100644 usvm-ts/src/test/resources/models/error-storage-owner/ErrorModels.ts diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index 668bbd0388..a5938078ae 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -67,14 +67,17 @@ The built-in catalog includes the following public APIs and their internal stora | --- | --- | --- | | `ts.array.shift` | Kotlin intrinsic using symbolic-memory `memcpy` | Zero-argument `shift` on a definitely one-dimensional array. | | `ts.array.isArray` | Kotlin runtime-type primitive | The genuine global Array predicate, including null, undefined and fake-value wrappers. | +| `ts.array.fromLength` | TypeScript/EtsIR body with a heap-allocation primitive | Genuine callable `Array(length)` with one numeric argument. Valid lengths up to 16 allocate holes that read as `undefined`; larger valid lengths use fallback. | | `ts.array.pop` | TypeScript/EtsIR body | Zero-argument `pop` on a definitely one-dimensional array that also satisfies the symbolic runtime type guard. | | `ts.array.includes`, `ts.array.indexOf`, `ts.array.lastIndexOf` | TypeScript/EtsIR bodies | One-dimensional arrays and numeric positions, with the missing-slot exclusions below. | -| `ts.array.push`, `ts.array.fill`, `ts.array.reverse`, `ts.array.unshift`, `ts.array.slice`, `ts.array.concat` | TypeScript/EtsIR bodies with storage growth/allocation primitives | One-dimensional arrays with length/result at most 16. Push/unshift accept up to three arguments; resolved-sort arrays require matching element sorts, while mixed arrays retain runtime value kinds. Concat accepts one same-type array. Except push, these operations require a current dense-array proof. | +| `ts.array.push`, `ts.array.fill`, `ts.array.reverse`, `ts.array.unshift`, `ts.array.slice`, `ts.array.concat` | TypeScript/EtsIR bodies with storage growth/allocation primitives | One-dimensional arrays with length/result at most 16. Push/unshift accept up to three arguments; resolved-sort arrays require matching element sorts, while mixed arrays retain runtime value kinds. Concat accepts one same-type array. Except push and full-range `fill(value)`, these operations require a current dense-array proof. | | `ts.string.charAt`, `ts.string.charCodeAt`, `ts.string.includes`, `ts.string.indexOf`, `ts.string.lastIndexOf`, `ts.string.startsWith`, `ts.string.endsWith` | TypeScript/EtsIR bodies | Strings in initialized UTF-16 storage, including symbolic code units and numeric positions. | | `ts.string.slice`, `ts.string.substring`, `ts.string.trim`, `ts.string.trimStart`, `ts.string.trimEnd` | TypeScript/EtsIR bodies | UTF-16 range copying; substring clamps/swaps bounds, and trim uses the ECMAScript whitespace set. | +| `ts.string.replaceAll` | TypeScript/EtsIR body | String receiver, string search and string replacement; non-overlapping UTF-16 matches, empty search and ECMAScript dollar substitutions for a dollar sign, the match, its prefix and its suffix. RegExp, callbacks and argument coercions use fallback. | | `ts.string.toLowerCase`, `ts.string.toUpperCase` | TypeScript/EtsIR bodies | ASCII strings of at most 16 code units; other strings use residual fallback. | | `ts.math.abs`, `ts.math.ceil`, `ts.math.floor`, `ts.math.max`, `ts.math.min`, `ts.math.round`, `ts.math.sqrt`, `ts.math.trunc` | Kotlin FP primitives | Numeric arguments; dynamic coercions use fallback. | | `ts.number.isFinite`, `ts.number.isInteger`, `ts.number.isNaN`, `ts.number.isSafeInteger` | Kotlin FP/type primitives | Non-coercing Number predicates, including runtime-kind guards. | +| `ts.error.constructor` | TypeScript/EtsIR body | Genuine `new Error(message)` with one string argument; initializes `name` and `message`. Other arities, coercions, subclasses, `cause` and stack inspection are outside this model. | | `ts.date.*` (38 IDs) | TypeScript/EtsIR bodies | Numeric Date construction, `UTC`, fixed-clock `now`, getters, setters, `valueOf`, and source `toISOString`; see the Date boundary below. | Matching standard calls are assumed to refer to genuine builtins. Monkey patching and prototype replacement are @@ -105,10 +108,17 @@ modeled array methods can still use fallback after its first mutation or copy. named-property writes or unsupported length growth. These events are separate from unknown-call model decisions. Exhaustion after a runtime limitation does not establish that a source target is unreachable; a reached target still requires original-source replay. +named-property access, unsupported length growth, or assigning a runtime kind absent from a typed array's storage. +Reads may return an element or `undefined`; subsequent numeric operations and typed writes preserve that runtime-kind +guard. TypeScript `as` and angle-bracket assertions are erased and never change a value or constrain its runtime kind. +These events are separate from unknown-call model decisions. +The Calls runner writes them synchronously and reports `RUNTIME_LIMITATION` when search exhausts after such a stop +without reaching the target. An actual timeout remains `TIMEOUT`; a reached target still requires original-source replay. Calls preflight checks input binding and source/IR target mapping before choosing a model/fallback profile. Excluded functions remain in the corpus support ledger. Comparative runs use a frozen common target set; failures discovered after that freeze remain scheduled failures. The analysis budget is 30 seconds per -target and seed; JVM/frontend startup and original-source replay have separate recorded limits. +target, profile and seed; JVM/frontend startup and original-source replay have separate recorded limits. Readiness +traverses reachable same-file callees and the initializers triggered by their static-field accesses. ### `unknownCallFallback` diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt index d115df1717..d6cf60c6ee 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsInterpreterObserver.kt @@ -98,6 +98,7 @@ enum class TsRuntimeFeatureLimitationReason { ARRAY_NAMED_PROPERTY_WRITE, ARRAY_INDEX_GROWTH, ARRAY_ITERATOR_UNSUPPORTED, + ARRAY_ELEMENT_KIND_WRITE, ARRAY_LENGTH_CAPACITY, ARRAY_LENGTH_GROWTH, STRING_ITERATOR_UNSUPPORTED, diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index cfe30da81a..a54874b36e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -2,11 +2,16 @@ package org.usvm.machine.call.intrinsic import io.ksmt.utils.asExpr import io.ksmt.utils.cast +import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsUnknownType import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef import org.usvm.UExpr +import org.usvm.api.initializeArray import org.usvm.api.initializeArrayLength import org.usvm.machine.call.TsEtsIrUnknownCallModel import org.usvm.machine.call.TsEtsIrUnknownCallModelArtifact @@ -21,10 +26,14 @@ import org.usvm.machine.call.TsUnknownCallModelSuccessor import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact import org.usvm.machine.call.resolvedInstanceInputs +import org.usvm.machine.expr.mkFpToUint32AfterValidation +import org.usvm.machine.expr.mkValidArrayLength import org.usvm.machine.state.TsState +import org.usvm.machine.types.TsUnresolvedArrayKind import org.usvm.sizeSort import org.usvm.util.arrayStorageType import org.usvm.util.componentType +import org.usvm.util.initializeArrayKind import org.usvm.util.isUnmodifiedDenseInputArray import org.usvm.util.mkArrayLengthLValue @@ -122,8 +131,9 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { private val fillDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> val (array, arrayType) = state.concreteArray(call, inputs) ?: return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr - val isDenseInput = state.isUnmodifiedDenseInputArray(array, arrayType) - if (!isDenseInput) { + val fillsWholeArray = call.arguments.size == 1 + val hasKnownSlotValues = fillsWholeArray || state.isUnmodifiedDenseInputArray(array, arrayType) + if (!hasKnownSlotValues) { return@TsEtsIrUnknownCallModelDomainGuard state.ctx.falseExpr } @@ -295,8 +305,31 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { if (call.arguments.isEmpty()) call.resolvedInstanceInputs(maxArgumentCount = call.arguments.size) else null } + private val arrayConstructorAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + if (!call.hasGlobalArrayConstructorShape() || call.arguments.size != 1) { + return@TsEtsIrUnknownCallModelInputAdapter null + } + + val length = call.arguments.single().resolved + ?.takeIf { value -> value.sort == state.ctx.fp64Sort } + ?: return@TsEtsIrUnknownCallModelInputAdapter null + listOf(length) + } + override val models: List by lazy { + val arrayConstructorModel = TsEtsIrUnknownCallModel( + id = ARRAY_FROM_LENGTH_ID, + target = TsUnknownCallTarget( + methodName = "Array", + failureReason = TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, + ), + artifact = artifact("fromLength"), + inputAdapter = arrayConstructorAdapter, + requiredModelIds = setOf(PRIMITIVE_ALLOCATE_ID), + ) + listOf( + arrayConstructorModel, sourceModel( id = "ts.array.pop", methodName = "pop", @@ -357,6 +390,11 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { arity = 2, implementation = ::growArray, ), + primitiveModel( + methodName = "allocate", + arity = 1, + implementation = ::allocateArray, + ), primitiveModel( methodName = "allocateLike", arity = 2, @@ -500,6 +538,60 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } + private fun allocateArray( + state: TsState, + inputs: List>, + ): TsUnknownCallModelExecution? = with(state.ctx) { + val fpLength = inputs.singleOrNull() + ?.takeIf { value -> value.sort == fp64Sort } + ?.asExpr(fp64Sort) + ?: return null + val validLength = mkValidArrayLength(fpLength) + val maximumLength = mkFp64(MAX_SOURCE_ARRAY_LENGTH.toDouble()) + val withinModelCapacity = mkFpLessOrEqualExpr( + fpLength, + maximumLength, + ) + val supportedLength = mkAnd(validLength, withinModelCapacity) + val length = mkFpToUint32AfterValidation(fpLength, validLength).asExpr(sizeSort) + val arrayType = EtsArrayType(EtsUnknownType, dimensions = 1) + + // The model covers only valid, bounded one-number lengths. All other inputs remain residual. + val validSuccessor = TsUnknownCallModelSuccessor( + guard = supportedLength, + completion = TsUnknownCallModelCompletion.Normal { + val descriptor = arrayDescriptorOf(arrayType) + val result = memory.allocConcrete(descriptor) + val undefinedSlots = List(MAX_SOURCE_ARRAY_LENGTH) { mkUndefinedValue() } + memory.initializeArray( + arrayHeapRef = result, + type = descriptor, + sort = addressSort, + sizeSort = sizeSort, + contents = undefinedSlots.asSequence(), + ) + TsUnresolvedArrayKind.entries.forEach { kind -> + initializeArrayKind( + array = result, + kind = kind, + values = List(MAX_SOURCE_ARRAY_LENGTH) { falseExpr }, + ) + } + memory.initializeArrayLength( + arrayHeapRef = result, + type = descriptor, + sizeSort = sizeSort, + count = length, + ) + result + }, + ) + TsUnknownCallModelExecution( + successors = listOf(validSuccessor), + residualGuard = mkNot(supportedLength), + ) + } + private fun allocateArrayLike( state: TsState, inputs: List>, @@ -545,7 +637,31 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { ) } + private fun TsUnknownCall.hasGlobalArrayConstructorShape(): Boolean { + val owner = receiver?.source as? EtsLocal ?: return false + val ownerSignature = (owner.type as? EtsFunctionType)?.signature ?: return false + val ownerParameter = ownerSignature.parameters.singleOrNull() ?: return false + val ownerReturnType = ownerSignature.returnType as? EtsArrayType ?: return false + val callReturnType = resultType as? EtsArrayType ?: return false + val signatureFile = ownerSignature.enclosingClass.file + + return owner.name == "Array" && + signatureFile.projectName == UNKNOWN_SIGNATURE_COMPONENT && + signatureFile.fileName == UNKNOWN_SIGNATURE_COMPONENT && + ownerSignature.name.isEmpty() && + ownerParameter.type == EtsNumberType && + ownerParameter.isOptional && + !ownerParameter.isRest && + ownerReturnType.elementType == EtsAnyType && + ownerReturnType.dimensions == 1 && + callReturnType.elementType == EtsAnyType && + callReturnType.dimensions == 1 + } + private const val MATH_FLOOR_MODEL_ID = "ts.math.floor" + private const val ARRAY_FROM_LENGTH_ID = "ts.array.fromLength" private const val PRIMITIVE_GROW_ID = "ts.array.primitive.grow" + private const val PRIMITIVE_ALLOCATE_ID = "ts.array.primitive.allocate" private const val PRIMITIVE_ALLOCATE_LIKE_ID = "ts.array.primitive.allocateLike" + private const val UNKNOWN_SIGNATURE_COMPONENT = "%unk" } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt new file mode 100644 index 0000000000..3b449964aa --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt @@ -0,0 +1,103 @@ +package org.usvm.machine.call.intrinsic + +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsStringType +import org.jacodb.ets.utils.CONSTRUCTOR_NAME +import org.usvm.UConcreteHeapRef +import io.ksmt.utils.asExpr +import org.usvm.machine.expr.builtInErrorSignature +import org.usvm.api.evalTypeEquals +import org.usvm.api.typeStreamOf +import org.usvm.machine.call.TsEtsIrUnknownCallModel +import org.usvm.machine.call.TsEtsIrUnknownCallModelDomainGuard +import org.usvm.machine.call.TsEtsIrUnknownCallModelInputAdapter +import org.usvm.machine.call.TsUnknownCallFailureReason +import org.usvm.machine.call.TsUnknownCallModel +import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact +import org.usvm.types.single + +/** Narrow built-in `Error(message: string)` constructor model. */ +internal object TsErrorEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { + const val CONSTRUCTOR_ID: String = "ts.error.constructor" + + private const val ERROR_CLASS = "Error" + private const val RESOURCE = "/org/usvm/machine/call/models/ErrorModels.ts" + + private val artifact by lazy { + loadBundledEtsIrUnknownCallModelArtifact( + resourceName = RESOURCE, + sourceFileName = "ErrorModels.ts", + entryPointClassName = "ErrorModels", + entryPointMethodName = "construct", + ) + } + + internal fun ownsStorageDefinitionField(field: EtsFieldSignature): Boolean = + field.enclosingClass.name == "ErrorValue" && field.enclosingClass.file == artifact.file.signature + + override val models: List by lazy { + listOf(constructorModel()) + } + + private fun constructorModel(): TsUnknownCallModel { + val target = TsUnknownCallTarget( + methodName = CONSTRUCTOR_NAME, + enclosingClassName = ERROR_CLASS, + failureReason = TsUnknownCallFailureReason.RECEIVER_CLASS_NOT_FOUND, + ) + + return TsEtsIrUnknownCallModel( + id = CONSTRUCTOR_ID, + target = target, + artifact = artifact, + domainGuard = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> + with(state.ctx) { + val receiver = inputs.getOrNull(0) as? UConcreteHeapRef + ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr + val messageValue = inputs.getOrNull(1) + ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr + if (messageValue.sort != addressSort) return@TsEtsIrUnknownCallModelDomainGuard falseExpr + val message = messageValue.asExpr(addressSort) + val builtinSignature = builtInErrorSignature + val builtinErrorType = EtsClassType(signature = builtinSignature) + val receiverRuntimeType = state.memory.typeStreamOf(receiver).single() + + if (call.callee.enclosingClass != builtinSignature) { + return@TsEtsIrUnknownCallModelDomainGuard falseExpr + } + if (receiver.hasFakeValueBranch() || receiverRuntimeType != builtinErrorType) { + return@TsEtsIrUnknownCallModelDomainGuard falseExpr + } + val knownFunction = (message as? UConcreteHeapRef)?.let { ref -> + state.associatedFunction.containsKey(ref) + } == true + if (message.hasFakeValueBranch() || knownFunction) { + return@TsEtsIrUnknownCallModelDomainGuard falseExpr + } + + val originalMessage = call.arguments.single().resolved + ?: return@TsEtsIrUnknownCallModelDomainGuard falseExpr + val referenceKindGuard = if (originalMessage.isFakeObject()) { + originalMessage.getFakeType(state.memory).refTypeExpr + } else { + trueExpr + } + mkAnd(referenceKindGuard, state.memory.types.evalTypeEquals(message, EtsStringType)) + } + }, + inputAdapter = TsEtsIrUnknownCallModelInputAdapter { state, call -> + val receiver = call.receiver?.resolved ?: return@TsEtsIrUnknownCallModelInputAdapter null + val message = call.arguments.singleOrNull()?.resolved + ?: return@TsEtsIrUnknownCallModelInputAdapter null + + with(state.ctx) { + if (message.sort != addressSort) return@TsEtsIrUnknownCallModelInputAdapter null + val payload = if (message.isFakeObject()) message.extractRef(state.memory) else message + listOf(receiver, payload) + } + }, + ) + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt index b170cb6ebb..e351445103 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsStringEtsIrModelFamily.kt @@ -30,6 +30,7 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { private const val CLASS_NAME = "StringModels" private const val PRIMITIVES_CLASS_NAME = "StringModelPrimitives" private const val RESOURCE_NAME = "/org/usvm/machine/call/models/StringModels.ts" + private const val REPLACE_ALL_INPUT_COUNT = 3 private val baseArtifact by lazy { loadBundledEtsIrUnknownCallModelArtifact( @@ -151,6 +152,19 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { state.ctx.mkAnd(receiverGuard, searchGuard) } + private val replaceAllAdapter = TsEtsIrUnknownCallModelInputAdapter { _, call -> + if (call.arguments.size == 2) call.resolvedInstanceInputs(maxArgumentCount = 2) else null + } + + private val replaceAllDomain = TsEtsIrUnknownCallModelDomainGuard { state, _, inputs -> + if (inputs.size != REPLACE_ALL_INPUT_COUNT) { + state.ctx.falseExpr + } else { + val guards = inputs.map { value -> stringDomain(state = state, input = value) } + state.ctx.mkAnd(guards) + } + } + private val asciiReceiverDomain = TsEtsIrUnknownCallModelDomainGuard { state, call, inputs -> with(state.ctx) { val receiverGuard = receiverDomain.evaluate(state, call, inputs) @@ -242,6 +256,12 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { inputAdapter = sliceAdapter, domainGuard = receiverDomain, ), + sourceModel( + id = "ts.string.replaceAll", + methodName = "replaceAll", + inputAdapter = replaceAllAdapter, + domainGuard = replaceAllDomain, + ), sourceModel( id = "ts.string.trim", methodName = "trim", @@ -311,9 +331,10 @@ internal object TsStringEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { add(PRIMITIVE_CODE_UNIT_AT_ID) } } - if (methodName in setOf("trim", "trimStart", "trimEnd")) { + if (methodName in setOf("trim", "trimStart", "trimEnd", "replaceAll")) { add(PRIMITIVE_CODE_UNIT_AT_ID) } + if (methodName == "replaceAll") add(PRIMITIVE_FROM_CODE_UNIT_ID) }, ) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt new file mode 100644 index 0000000000..c718d3a592 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt @@ -0,0 +1,105 @@ +package org.usvm.machine.expr + +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsField +import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsLocal +import org.usvm.UConcreteHeapRef +import org.usvm.UHeapRef +import org.usvm.USort +import org.usvm.api.typeStreamOf +import org.usvm.collection.field.UFieldLValue +import org.usvm.machine.TsContext +import org.usvm.machine.call.intrinsic.TsErrorEtsIrModelFamily +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.types.singleOrNull +import org.usvm.util.EtsHierarchy +import org.usvm.util.TsResolutionResult +import org.usvm.util.resolveEtsField + +internal val builtInErrorSignature = EtsClassSignature.UNKNOWN.copy(name = "Error") + +internal const val ERROR_NAME_STORAGE_FIELD = "__usvmErrorName" +internal const val ERROR_MESSAGE_STORAGE_FIELD = "__usvmErrorMessage" + +internal fun EtsFieldSignature.isErrorModelStorageDefinitionField(): Boolean = + enclosingClass.name == "ErrorValue" && + enclosingClass.file.fileName == "ErrorModels.ts" && + (name == ERROR_NAME_STORAGE_FIELD || name == ERROR_MESSAGE_STORAGE_FIELD) + +internal fun EtsFieldSignature.isUnresolvedErrorField(): Boolean = + enclosingClass == builtInErrorSignature && (name == "name" || name == "message") + +internal enum class ErrorStorageField { NAME, MESSAGE } + +internal fun mkErrorModelStorageLValue( + sort: Sort, + ref: UHeapRef, + key: ErrorStorageField, +): UFieldLValue = UFieldLValue(sort, ref, key) + +private fun EtsFieldSignature.errorModelDefinitionStorageField(): ErrorStorageField? { + if (!isErrorModelStorageDefinitionField()) return null + + return when (name) { + ERROR_NAME_STORAGE_FIELD -> ErrorStorageField.NAME + ERROR_MESSAGE_STORAGE_FIELD -> ErrorStorageField.MESSAGE + else -> null + } +} + +internal fun EtsFieldSignature.errorModelStorageField(): ErrorStorageField? { + if (enclosingClass != builtInErrorSignature && enclosingClass != EtsClassSignature.UNKNOWN) { + return null + } + + return when (name) { + "name" -> ErrorStorageField.NAME + "message" -> ErrorStorageField.MESSAGE + else -> null + } +} + +internal data class ModelStorageFieldResolution( + val storageField: ErrorStorageField?, + val etsField: TsResolutionResult, + val isModelStorageField: Boolean, +) + +internal fun TsContext.resolveModelStorageField( + scope: TsStepScope, + instanceLocal: EtsLocal?, + instance: UHeapRef, + field: EtsFieldSignature, + hierarchy: EtsHierarchy, +): ModelStorageFieldResolution { + val definitionStorageField = field.errorModelDefinitionStorageField().takeIf { + applicationAndSdkClasses.none { owner -> owner.signature == field.enclosingClass } && + TsErrorEtsIrModelFamily.ownsStorageDefinitionField(field) + } + val candidateStorageField = definitionStorageField ?: field.errorModelStorageField() + val runtimeType = (instance as? UConcreteHeapRef) + ?.takeIf { candidateStorageField != null } + ?.let { concreteInstance -> + scope.calcOnState { memory.typeStreamOf(concreteInstance).singleOrNull() } + } + val storageField = candidateStorageField.takeIf { + runtimeType == EtsClassType(signature = builtInErrorSignature) + } + val etsField = when { + storageField != null -> TsResolutionResult.Empty + field.isUnresolvedErrorField() -> resolveEtsField( + instance = instanceLocal, + field = field.copy(enclosingClass = EtsClassSignature.UNKNOWN), + hierarchy = hierarchy, + ) + else -> resolveEtsField(instanceLocal, field, hierarchy) + } + + return ModelStorageFieldResolution( + storageField = storageField, + etsField = etsField, + isModelStorageField = storageField != null, + ) +} 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 e7fd221fa9..25c4214bcc 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 @@ -50,7 +50,6 @@ import org.usvm.util.mkFieldLValue import org.usvm.util.mkStringBackingElementLValue import org.usvm.util.mkStringBackingLValue import org.usvm.util.mkStringBackingLengthLValue -import org.usvm.util.resolveEtsField private val logger = KotlinLogging.logger {} @@ -148,6 +147,14 @@ private fun TsContext.resolveDeclaredField( val deleted = scope.calcOnState { memory.read(deletedFieldLValue(instance, field)) } if (deleted.isTrue) return mkUndefinedValue() + val (errorStorageField, resolvedField, isModelStorageField) = resolveModelStorageField( + scope = scope, + instanceLocal = local, + instance = instance, + field = field, + hierarchy = hierarchy, + ) + // A literal's own declarations, rather than scene-wide same-name fields, determine its initial storage. val objectClass = objectLiteralClass(scope, instance, hierarchy) val wasWritten = scope.calcOnState { (instance to field.name) in writtenConcreteFields } @@ -157,31 +164,31 @@ private fun TsContext.resolveDeclaredField( } val declaredLiteralField = objectClass?.fields?.singleOrNull { it.name == field.name } - val resolvedField = resolveEtsField(local, field, hierarchy) val writtenSort = scope.calcOnState { writtenObjectLiteralFieldSorts[instance to field.name] } val declaredLiteralSort = declaredLiteralField?.let { typeToSort(it.type) } - val sort = writtenSort ?: declaredLiteralSort ?: resolvedFieldSort( - scope = scope, - instance = instance, - field = field, - resolved = resolvedField, - hierarchy = hierarchy, - ) - val declaredType = if (objectClass != null) { + val storageSort = if (errorStorageField != null) { + addressSort + } else { + writtenSort ?: declaredLiteralSort ?: resolvedFieldSort(scope, instance, field, resolvedField, hierarchy) + } + val declaredType = if (errorStorageField != null) { + null + } else if (objectClass != null) { declaredLiteralField?.type } else { (resolvedField as? TsResolutionResult.Unique)?.property?.type } - if (!wasWritten) { + val requiresDeclaredPresence = !wasWritten && !isModelStorageField + if (requiresDeclaredPresence) { val fieldExists = scope.calcOnState { memory.types.evalIsSubtype(instance, EtsAuxiliaryType(properties = setOf(field.name))) } scope.assert(fieldExists) ?: return null } - val storedValue = readField(scope, instance, field, sort) - val value = materializeFieldValue(scope, storedValue, sort, declaredType) ?: return null + val storedValue = readField(scope, instance, field, storageSort, errorStorageField) + val value = materializeFieldValue(scope, storedValue, storageSort, declaredType) ?: return null if (deleted.isFalse) return value // Conditional deletion yields undefined on the deleted branch, while preserving the stored runtime kind. @@ -334,9 +341,14 @@ private fun TsContext.readField( instance: UHeapRef, field: EtsFieldSignature, sort: USort, + errorStorageField: ErrorStorageField?, ): UExpr<*> { if (sort !is TsUnresolvedSort) { - val lValue = mkFieldLValue(sort, instance, field) + val lValue = if (errorStorageField == null) { + mkFieldLValue(sort, instance, field.name) + } else { + mkErrorModelStorageLValue(sort, instance, errorStorageField) + } return scope.calcOnState { memory.read(lValue) } } 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 8eff962178..d037a07c09 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 @@ -168,6 +168,7 @@ private const val ECMASCRIPT_BITWISE_INTEGER_SIZE = 32 * and `x << 37` is equivalent to `x << 5`. */ private const val ECMASCRIPT_BITWISE_SHIFT_MASK = 0b11111 +private const val UNKNOWN_SIGNATURE_COMPONENT = "%unk" private enum class UpdateOperator { INCREMENT, @@ -430,51 +431,8 @@ class TsExprResolver( ) } - override fun visit(expr: EtsCastExpr): UExpr<*>? = with(ctx) { - val resolvedExpr = resolve(expr.arg) ?: return@with null - if (resolvedExpr is UConcreteHeapRef && classConstructorSignature(resolvedExpr) != null) { - // TypeScript assertions do not change the identity of a constructor at runtime. - return@with resolvedExpr - } - - return when (resolvedExpr.sort) { - fp64Sort -> { - logger.error("Unsupported cast from fp ${expr.arg} to ${expr.type}") - TODO("Not yet implemented https://github.com/UnitTestBot/usvm/issues/299") - } - - boolSort -> { - logger.error("Unsupported cast from boolean ${expr.arg} to ${expr.type}") - TODO("Not yet implemented https://github.com/UnitTestBot/usvm/issues/299") - } - - addressSort -> { - scope.calcOnState { - val instance = resolvedExpr.asExpr(addressSort) - - if (instance.isFakeObject()) { - val fakeType = instance.getFakeType(scope) - pathConstraints += fakeType.refTypeExpr - val refValue = instance.extractRef(scope) - pathConstraints += memory.types.evalIsSubtype(refValue, expr.type) - return@calcOnState instance - } - - if (expr.type !is EtsRefType) { - logger.error("Unsupported cast from non-ref ${expr.arg} to ${expr.type}") - TODO("Not supported yet https://github.com/UnitTestBot/usvm/issues/299") - } - - pathConstraints += memory.types.evalIsSubtype(instance, expr.type) - instance - } - } - - else -> { - error("Unsupported cast from ${expr.arg} to ${expr.type}") - } - } - } + // TypeScript assertions are erased; they neither convert nor constrain the runtime value. + override fun visit(expr: EtsCastExpr): UExpr<*>? = resolve(expr.arg) override fun visit(expr: EtsTypeOfExpr): UExpr? = with(ctx) { val arg = resolve(expr.arg) ?: return null @@ -1360,12 +1318,19 @@ class TsExprResolver( val callee = scope.calcOnState { associatedFunction[ptr] } if (callee == null) { + val resolvedArguments = if (expr.isBuiltInArrayConstructor()) { + val argument = resolve(expr.args.single()) ?: return null + listOf(argument) + } else { + List(expr.args.size) { null } + } unknownCallDispatcher.dispatch( scope = scope, call = expr, callSite = scope.calcOnState { lastStmt }, failureReason = TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, resolvedReceiver = ptr, + resolvedArguments = resolvedArguments, ) return null } @@ -1406,6 +1371,26 @@ class TsExprResolver( } } + private fun EtsPtrCallExpr.isBuiltInArrayConstructor(): Boolean { + if (callee.name != "Array" || ptr.name != "Array" || args.size != 1) { + return false + } + + val signature = (ptr.type as? EtsFunctionType)?.signature ?: return false + val parameter = signature.parameters.singleOrNull() ?: return false + val returnType = signature.returnType as? EtsArrayType ?: return false + val signatureFile = signature.enclosingClass.file + + return signatureFile.projectName == UNKNOWN_SIGNATURE_COMPONENT && + signatureFile.fileName == UNKNOWN_SIGNATURE_COMPONENT && + signature.name.isEmpty() && + parameter.type == EtsNumberType && + parameter.isOptional && + !parameter.isRest && + returnType.elementType == EtsAnyType && + returnType.dimensions == 1 + } + private fun EtsPtrCallExpr.isBuiltInNumberConverter(): Boolean { val hasBuiltInCallSite = callee.name == "Number" && callee.enclosingClass == EtsClassSignature.UNKNOWN && 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 82f8d2d61c..f33ae325f3 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 @@ -25,6 +25,7 @@ import org.usvm.util.TsResolutionResult import org.usvm.util.arrayStorageType import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue +import org.usvm.util.boxArrayValue import org.usvm.util.resolveEtsField import org.usvm.util.truncateKnownArrayIndices @@ -200,6 +201,26 @@ fun TsContext.assignToInstanceField( return Unit } + val errorStorageField = resolveModelStorageField( + scope = scope, + instanceLocal = instanceLocal, + instance = unwrappedInstance, + field = field, + hierarchy = hierarchy, + ).storageField + if (errorStorageField != null) { + val payload = boxArrayValue(scope, expr) + return scope.doWithState { + memory.write( + mkErrorModelStorageLValue(addressSort, unwrappedInstance, errorStorageField), + payload.asExpr(addressSort), + guard = trueExpr, + ) + memory.write(deletedFieldLValue(unwrappedInstance, field), falseExpr, guard = trueExpr) + writtenConcreteFields += unwrappedInstance to field.name + } + } + val objectLiteralClass = objectLiteralClass(scope, unwrappedInstance, hierarchy) val declaredObjectLiteralField = objectLiteralClass?.fields?.singleOrNull { it.name == field.name } val newObjectLiteralField = objectLiteralClass != null && declaredObjectLiteralField == null diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts index 14754943f9..db3b8b86c7 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ArrayModels.ts @@ -1,9 +1,14 @@ declare class ArrayModelPrimitives { static grow(receiver: any[], length: number): void; + static allocate(length: number): any[]; static allocateLike(receiver: any[], length: number): any[]; } export class ArrayModels { + static fromLength(length: number): any[] { + return ArrayModelPrimitives.allocate(length); + } + static pop(receiver: any[]): any { const length = receiver.length; if (length === 0) { diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/ErrorModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ErrorModels.ts new file mode 100644 index 0000000000..ca847a6ea2 --- /dev/null +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/ErrorModels.ts @@ -0,0 +1,13 @@ +export class ErrorValue { + // Keep model storage out of unresolved user-property lookup. + __usvmErrorName: string; + __usvmErrorMessage: string; +} + +export class ErrorModels { + static construct(receiver: ErrorValue, message: string): ErrorValue { + receiver.__usvmErrorName = "Error"; + receiver.__usvmErrorMessage = message; + return receiver; + } +} diff --git a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts index 5210921e6c..f475de2afc 100644 --- a/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts +++ b/usvm-ts/src/main/resources/org/usvm/machine/call/models/StringModels.ts @@ -115,6 +115,66 @@ export class StringModels { return StringModels.slice(receiver, 0, end); } + static replaceAll(receiver: string, search: string, replacement: string): string { + const length = receiver.length; + const searchLength = search.length; + let result = ""; + let endOfLastMatch = 0; + let position = 0; + while (position + searchLength <= length) { + let offset = 0; + while (offset < searchLength && + StringModelPrimitives.codeUnitAt(receiver, position + offset) === + StringModelPrimitives.codeUnitAt(search, offset)) { + offset++; + } + if (offset === searchLength) { + result += StringModels.slice(receiver, endOfLastMatch, position); + result += StringModels.substitution(receiver, search, replacement, position); + endOfLastMatch = position + searchLength; + position = endOfLastMatch + (searchLength === 0 ? 1 : 0); + } else { + position++; + } + } + return result + StringModels.slice(receiver, endOfLastMatch, length); + } + private static substitution(receiver: string, search: string, replacement: string, position: number): string { + const replacementLength = replacement.length; + let result = ""; + let index = 0; + while (index < replacementLength) { + const code = StringModelPrimitives.codeUnitAt(replacement, index); + if (code === 36 && index + 1 < replacementLength) { + const next = StringModelPrimitives.codeUnitAt(replacement, index + 1); + if (next === 36) { + result += "$"; + index += 2; + continue; + } + if (next === 38) { + result += search; + index += 2; + continue; + } + if (next === 96) { + result += StringModels.slice(receiver, 0, position); + index += 2; + continue; + } + if (next === 39) { + const matchEnd = position + search.length; + result += StringModels.slice(receiver, matchEnd, receiver.length); + index += 2; + continue; + } + } + result += StringModelPrimitives.fromCodeUnit(code); + index++; + } + return result; + } + private static isWhitespace(codeUnit: number): boolean { return (codeUnit >= 0x09 && codeUnit <= 0x0d) || codeUnit === 0x20 || codeUnit === 0xa0 || codeUnit === 0x1680 diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/ErrorModelBackingBoundaryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/ErrorModelBackingBoundaryTest.kt new file mode 100644 index 0000000000..e06ee3b519 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/ErrorModelBackingBoundaryTest.kt @@ -0,0 +1,81 @@ +package org.usvm.machine.call + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStringType +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.machine.expr.ERROR_MESSAGE_STORAGE_FIELD +import org.usvm.machine.expr.ERROR_NAME_STORAGE_FIELD +import org.usvm.machine.expr.ErrorStorageField +import org.usvm.machine.expr.mkErrorModelStorageLValue +import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import org.usvm.util.mkFieldLValue +import kotlin.test.assertEquals +import kotlin.test.assertIs + +class ErrorModelBackingBoundaryTest : TsMethodTestRunner() { + override val scene = EtsScene( + listOf( + loadEtsFileAutoConvert( + getResourcePath("/models/ErrorModelBackingBoundary.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + + override val runner: (EtsMethod, UMachineOptions) -> List = { method, options -> + TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + @Test + fun `modeled Error retains supported public name and message semantics`() { + discoverProperties( + method = getMethod(methodName = "publicFields", className = "ErrorModelBackingBoundary"), + { result -> result.value == "CustomError|after" }, + invariants = arrayOf({ result -> result.value == "CustomError|after" }), + ) + } + + @Test + fun `ordinary property named like Error message storage stays separate in memory`() { + checkStorageIsolation(key = ErrorStorageField.MESSAGE, sourceName = ERROR_MESSAGE_STORAGE_FIELD) + } + + @Test + fun `ordinary property named like Error name storage stays separate in memory`() { + checkStorageIsolation(key = ErrorStorageField.NAME, sourceName = ERROR_NAME_STORAGE_FIELD) + } + + // This deliberately tests field-region isolation after source-created Error initialization. + // It does not claim support for adding arbitrary own properties through the TypeScript interpreter. + private fun checkStorageIsolation(key: ErrorStorageField, sourceName: String) { + val method = getMethod(methodName = "allocatedError", className = "ErrorModelBackingBoundary") + TsMachine(scene = scene, options = UMachineOptions(), tsOptions = TsOptions()).use { machine -> + val state = machine.analyze(listOf(method)).single() + val result = assertIs(state.methodResult) + val reference = result.value.asExpr(state.ctx.addressSort) + val modelSlot = mkErrorModelStorageLValue(state.ctx.addressSort, reference, key) + val ordinarySlot = mkFieldLValue(state.ctx.addressSort, reference, sourceName) + val original = state.memory.read(modelSlot) + val userValue = state.memory.allocConcrete(EtsStringType) + + state.memory.write(ordinarySlot, userValue, guard = state.ctx.trueExpr) + + assertEquals(original, state.memory.read(modelSlot)) + assertEquals(userValue, state.memory.read(ordinarySlot)) + } + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/ErrorModelOwnerBoundaryTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/ErrorModelOwnerBoundaryTest.kt new file mode 100644 index 0000000000..253cfc9278 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/ErrorModelOwnerBoundaryTest.kt @@ -0,0 +1,54 @@ +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 + +class ErrorModelOwnerBoundaryTest : TsMethodTestRunner() { + override val scene = EtsScene( + listOf( + loadEtsFileAutoConvert( + getResourcePath("/models/error-storage-owner/ErrorModels.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + + override val runner: (EtsMethod, UMachineOptions) -> List = { method, options -> + TsMachine( + scene = scene, + options = options, + tsOptions = TsOptions(unknownCallModelSelection = TsUnknownCallModelSelection.Only(emptySet())), + ).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + @Test + fun `source ErrorValue in ErrorModels keeps ordinary self field storage`() { + discoverProperties( + method = getMethod(methodName = "ordinarySelfFields", className = "ErrorValue"), + { result -> result.value == "user name|user message" }, + invariants = arrayOf({ result -> result.value == "user name|user message" }), + ) + } + + @Test + fun `source ErrorValue fields remain visible through any alias`() { + discoverProperties( + method = getMethod(methodName = "ordinarySelfFieldsThroughAny", className = "ErrorValue"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayConstructorEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayConstructorEtsIrModelTest.kt new file mode 100644 index 0000000000..893ab8b2e7 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayConstructorEtsIrModelTest.kt @@ -0,0 +1,170 @@ +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.jacodb.ets.utils.loadEtsProjectAutoConvert +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.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 TsArrayConstructorEtsIrModelTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/ArrayConstructorEtsIr.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + private val importedShadowScene = loadEtsProjectAutoConvert( + getResourcePath("/models/array-constructor-shadow"), + useArkAnalyzerTypeInference = null, + ) + + @Test + fun `callable Array creates holes and accepts in bounds writes`() { + val result = analyze(methodName = "callableArrayCreatesHolesAndAcceptsWrites") + + assertEquals(13_456.0, result.singleNumber()) + assertEquals( + listOf("ts.array.fromLength", "ts.array.primitive.allocate"), + result.modelIds, + ) + } + + @Test + fun `callable Array result can be assigned to a nested array type`() { + val result = analyze(methodName = "callableArraySupportsNestedAssignment") + + assertEquals(256.0, result.singleNumber()) + assertEquals( + listOf("ts.array.fromLength", "ts.array.primitive.allocate"), + result.modelIds, + ) + } + + @Test + fun `invalid callable Array lengths remain residual`() { + for (methodName in listOf("negativeLength", "fractionalLength", "nanLength", "infiniteLength")) { + val result = analyze(methodName = methodName) + + assertTrue(result.values.isEmpty(), methodName) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome, methodName) + } + } + + @Test + fun `valid length above model capacity remains residual`() { + val result = analyze(methodName = "oversizedLength") + + assertTrue(result.values.isEmpty()) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, result.events.last().outcome) + } + + @Test + fun `full fill initializes every slot of a sparse array`() { + val expectedResults = mapOf( + "fullFillInitializesSparseNumberArray" to 3_777.0, + "fullFillInitializesSparseBooleanArray" to 3_111.0, + ) + + for ((methodName, expected) in expectedResults) { + val result = analyze(methodName = methodName) + + assertEquals(expected, result.singleNumber(), methodName) + assertEquals(listOf("ts.array.fill", "ts.math.floor"), result.modelIds, methodName) + } + } + + @Test + fun `shadowed Array function is not modeled as the global constructor`() { + val result = analyze(methodName = "shadowedArrayIsNotModeled") + + assertEquals(2.0, result.singleNumber()) + assertTrue(result.events.isEmpty()) + } + + @Test + fun `imported Array function is not modeled as the global constructor`() { + val result = analyze( + methodName = "callImportedArray", + className = "ImportedArrayShadow", + scene = importedShadowScene, + ) + + assertEquals(99.0, result.singleNumber()) + assertTrue(result.events.isEmpty()) + } + + private fun analyze( + methodName: String, + className: String = "ArrayConstructorEtsIr", + scene: EtsScene = this.scene, + ): AnalysisResult { + val method = method(scene, className, methodName) + val observer = RecordingUnknownCallObserver() + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> + val states = machine.analyze(listOf(method)) + AnalysisResult( + values = states.map { state -> TsTestResolver().resolve(method, state).returnValue }, + events = observer.events.toList(), + ) + } + } + + private fun method(scene: EtsScene, className: String, methodName: String): EtsMethod = scene.projectClasses + .single { it.name == className } + .methods + .single { it.name == methodName } + + private class RecordingUnknownCallObserver : TsInterpreterObserver { + val events = mutableListOf() + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + private data class AnalysisResult( + val values: List, + val events: List, + ) { + fun singleNumber(): Double = assertIs(values.single()).number + + val modelIds: List + get() = 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 = 20_000L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} 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 571f88e566..8bf30815be 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 @@ -158,11 +158,67 @@ class TsArrayShiftReplayTest { """.trimIndent(), ) ) + addAll(assertionAndWriteCases()) addAll(storageOperationCases()) addAll(pairCases()) addAll(typedCases()) } + private fun assertionAndWriteCases(): List = buildList { + add( + ReplayCase( + name = "number type assertions preserve runtime values", + parameters = "value: number", + maxResult = 1, + body = """ + if (value !== 42) return 0; + const asserted = value as unknown as string; + return typeof asserted === 'number' && asserted === 42 ? 1 : -1; + """.trimIndent(), + ) + ) + add( + ReplayCase( + name = "boolean type assertions do not convert to numbers", + parameters = "value: boolean", + maxResult = 1, + body = """ + if (!value) return 0; + const asserted = value as unknown as number; + return typeof asserted === 'boolean' && asserted === true ? 1 : -1; + """.trimIndent(), + ) + ) + add( + ReplayCase( + name = "truthy wrapped number retains its runtime kind through assertion and write", + parameters = "values: number[]", + maxResult = 2, + body = """ + if (values.length !== 1) return 0; + const item = values[0]; + if (!item) return 1; + const asserted = item as unknown as number; + const output = [0]; + output[0] = asserted; + return output[0] === item ? 2 : -1; + """.trimIndent(), + ) + ) + add( + ReplayCase( + name = "typed array copies preserve wrapped numbers including NaN", + parameters = "values: number[]", + maxResult = 1, + body = """ + if (values.length !== 2) return 0; + values[0] = values[1]; + return values[0] === values[1] || values[0] !== values[0] ? 1 : -1; + """.trimIndent(), + ) + ) + } + 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) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt new file mode 100644 index 0000000000..edc3a7ae09 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.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.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.TsErrorEtsIrModelFamily +import org.usvm.machine.state.TsMethodResult +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 TsErrorEtsIrModelTest { + private val builtInSourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/ErrorEtsIr.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val shadowSourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/UserDefinedErrorEtsIr.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val builtInScene = EtsScene(projectFiles = listOf(builtInSourceFile)) + private val shadowScene = EtsScene(projectFiles = listOf(shadowSourceFile)) + + @Test + fun `Error constructor and public field accesses record constructor model`() { + val methodNames = listOf("name", "message", "overwrittenName", "overwrittenMessage", "anyErrorMessage") + + methodNames.forEach { methodName -> + val result = analyze(scene = builtInScene, className = "ErrorEtsIr", methodName = methodName) + + assertEquals(listOf(TsErrorEtsIrModelFamily.CONSTRUCTOR_ID), result.modelIds) + } + } + + @Test + fun `modeled Error receiver remains the thrown exception`() { + val result = analyze(scene = builtInScene, className = "ErrorEtsIr", methodName = "throwError") + + assertEquals(1, result.states.size) + assertIs(result.states.single().methodResult) + assertEquals(listOf(TsErrorEtsIrModelFamily.CONSTRUCTOR_ID), result.modelIds) + assertTrue(result.values.single() is TsTestValue.TsException) + } + + @Test + fun `Error model storage does not affect ordinary any field resolution`() { + listOf("anyForeignNameComparison", "anyForeignMessageComparison").forEach { methodName -> + val result = analyze(scene = builtInScene, className = "ErrorEtsIr", methodName = methodName) + val actual = result.values.map { value -> assertIs(value).number } + + // An `any` read may retain an extra symbolic branch, but the concrete path must remain reachable. + assertTrue(1.0 in actual, methodName) + assertTrue(result.modelIds.isEmpty(), methodName) + } + } + + @Test + fun `callback Error message remains residual`() { + val result = analyze(scene = builtInScene, className = "ErrorEtsIr", methodName = "callbackMessage") + + assertTrue(result.states.isEmpty()) + assertEquals( + listOf(TsResidualCallPolicy.STOP_PATH), + result.events.mapNotNull { event -> + (event.decision as? TsUnknownCallDecision.ResidualFallback)?.policy + }, + ) + assertTrue(result.modelIds.isEmpty()) + } + + @Test + fun `user defined Error constructor does not use builtin model`() { + val result = analyze(scene = shadowScene, className = "UserDefinedErrorEtsIr", methodName = "name") + val actual = assertIs(result.values.single()).value + + assertEquals("ShadowError", actual) + assertTrue(result.modelIds.isEmpty()) + } + + private fun analyze(scene: EtsScene, className: String, methodName: String): AnalysisResult { + val method = method(scene = scene, className = className, methodName = methodName) + val observer = RecordingUnknownCallObserver() + val states = TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(), + observer = observer, + ).use { machine -> machine.analyze(listOf(method)) } + val values = states.map { state -> TsTestResolver().resolve(method, state).returnValue } + + return AnalysisResult( + states = states, + values = values, + events = observer.events.toList(), + ) + } + + private fun method(scene: EtsScene, className: String, methodName: String): EtsMethod = scene.projectClasses + .single { clazz -> clazz.name == className } + .methods + .single { method -> method.name == methodName } + + private class RecordingUnknownCallObserver : TsInterpreterObserver { + val events = mutableListOf() + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + private data class AnalysisResult( + val states: List, + val values: List, + 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 = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt new file mode 100644 index 0000000000..3e659593a6 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt @@ -0,0 +1,114 @@ +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 + +class TsErrorSourceSemanticsTest : TsMethodTestRunner() { + override val scene = EtsScene( + listOf( + loadEtsFileAutoConvert( + getResourcePath("/models/ErrorEtsIr.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + + override val runner: (EtsMethod, UMachineOptions) -> List = { method, options -> + TsMachine(scene = scene, options = options, tsOptions = TsOptions()).use { machine -> + machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } + } + } + + @Test + fun `source primitive name and message writes preserve actual runtime kinds`() { + discoverProperties( + method = getMethod(methodName = "overwrittenPrimitiveKinds", className = "ErrorEtsIr"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `source nullish name and message writes preserve values`() { + discoverProperties( + method = getMethod(methodName = "overwrittenReferenceKinds", className = "ErrorEtsIr"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `source object message write preserves alias identity`() { + discoverProperties( + method = getMethod(methodName = "overwrittenObjectAlias", className = "ErrorEtsIr"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `ordinary symbolic string message remains eligible and retains identity`() { + discoverProperties( + method = getMethod(methodName = "symbolicMessage", className = "ErrorEtsIr"), + { message, result -> message.value.isEmpty() && result.value }, + { message, result -> message.value.isNotEmpty() && result.value }, + invariants = arrayOf({ _, result -> result.value }), + ) + } + + @Test + fun `source name preserves Error string semantics`() { + discoverProperties( + method = getMethod(methodName = "name", className = "ErrorEtsIr"), + { result -> result.value == "Error" }, + invariants = arrayOf({ result -> result.value == "Error" }), + ) + } + + @Test + fun `source message preserves Error string semantics`() { + discoverProperties( + method = getMethod(methodName = "message", className = "ErrorEtsIr"), + { result -> result.value == "expected message" }, + invariants = arrayOf({ result -> result.value == "expected message" }), + ) + } + + @Test + fun `source overwrittenName preserves Error string semantics`() { + discoverProperties( + method = getMethod(methodName = "overwrittenName", className = "ErrorEtsIr"), + { result -> result.value == "CustomError" }, + invariants = arrayOf({ result -> result.value == "CustomError" }), + ) + } + + @Test + fun `source overwrittenMessage preserves Error string semantics`() { + discoverProperties( + method = getMethod(methodName = "overwrittenMessage", className = "ErrorEtsIr"), + { result -> result.value == "after" }, + invariants = arrayOf({ result -> result.value == "after" }), + ) + } + + @Test + fun `source anyErrorMessage preserves Error string semantics`() { + discoverProperties( + method = getMethod(methodName = "anyErrorMessage", className = "ErrorEtsIr"), + { result -> result.value == "aliased message" }, + invariants = arrayOf({ result -> result.value == "aliased message" }), + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsStringReplaceAllEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsStringReplaceAllEtsIrModelTest.kt new file mode 100644 index 0000000000..f0f6df7652 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsStringReplaceAllEtsIrModelTest.kt @@ -0,0 +1,103 @@ +package org.usvm.machine.call + +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.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 TsStringReplaceAllEtsIrModelTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/StringReplaceAllEtsIr.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(listOf(sourceFile)) + + @Test + fun `literal string replacement implements substitution and UTF16 boundaries`() { + val cases = mapOf( + "literalMatches" to "XX/aba", + "emptySearch" to "-A-\uD83D-\uDE00-", + "substitutions" to "\$:a::ba:\$1b\$:a:ab::\$1", + "noMatches" to "abc", + "emptyReceiver" to "\$", + "replacementIsNotSearchedAgain" to "aaaa", + ) + + cases.forEach { (methodName, expected) -> + val (values, events) = analyze(methodName) + + assertEquals(expected, assertIs(values.single()).value, methodName) + assertTrue(events.any { (it.decision as? TsUnknownCallDecision.ModelApplied)?.modelId == MODEL_ID }) + assertTrue(events.all { it.outcome == TsUnknownCallOutcome.MODEL_APPLIED }) + } + } + + @Test + fun `non string arguments remain explicit residual calls`() { + val cases = listOf( + "numericSearchIsResidual", + "numericReplacementIsResidual", + "callbackReplacementIsResidual", + "callableSearchIsResidual", + ) + + for (methodName in cases) { + val (values, events) = analyze(methodName) + + assertTrue(values.isEmpty(), methodName) + assertEquals(TsUnknownCallOutcome.PATH_STOPPED, events.single().outcome, methodName) + } + } + + private fun analyze(methodName: String): Pair, List> { + val method = scene.projectClasses.single { it.name == "StringReplaceAllEtsIr" }.methods + .single { it.name == methodName } + val events = mutableListOf() + val observer = object : TsInterpreterObserver { + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(unknownCallModelSelection = TsUnknownCallModelSelection.Only(setOf(MODEL_ID))), + observer = observer, + ).use { machine -> + val values = machine.analyze(listOf(method)).map { state -> + TsTestResolver().resolve(method, state).returnValue + } + values to events.toList() + } + } + + private companion object { + const val MODEL_ID = "ts.string.replaceAll" + 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/call/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt index 0ed730f6f9..8c3ec5deff 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 @@ -12,6 +12,7 @@ import org.usvm.UMachineOptions import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.call.intrinsic.TsArrayShiftIntrinsicModel +import org.usvm.machine.call.intrinsic.TsErrorEtsIrModelFamily import org.usvm.machine.call.intrinsic.TsNumericIntrinsicModelFamily import org.usvm.machine.state.TsState import kotlin.test.Test @@ -180,11 +181,13 @@ class TsUnknownCallModelCatalogTest { val expectedModelIds = listOf( "ts.array.concat", "ts.array.fill", + "ts.array.fromLength", "ts.array.includes", "ts.array.indexOf", "ts.array.isArray", "ts.array.lastIndexOf", "ts.array.pop", + "ts.array.primitive.allocate", "ts.array.primitive.allocateLike", "ts.array.primitive.grow", "ts.array.push", @@ -192,6 +195,7 @@ class TsUnknownCallModelCatalogTest { TsArrayShiftIntrinsicModel.MODEL_ID, "ts.array.slice", "ts.array.unshift", + TsErrorEtsIrModelFamily.CONSTRUCTOR_ID, TsNumericIntrinsicModelFamily.MATH_ABS_ID, TsNumericIntrinsicModelFamily.MATH_CEIL_ID, TsNumericIntrinsicModelFamily.MATH_FLOOR_ID, @@ -212,6 +216,7 @@ class TsUnknownCallModelCatalogTest { "ts.string.lastIndexOf", "ts.string.primitive.codeUnitAt", "ts.string.primitive.fromCodeUnit", + "ts.string.replaceAll", "ts.string.slice", "ts.string.startsWith", "ts.string.substring", 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 index d830ea95c3..33e6914d67 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumericBoundarySemanticsTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumericBoundarySemanticsTest.kt @@ -118,6 +118,7 @@ class NumericBoundarySemanticsTest : TsMethodTestRunner() { "negativeArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, "outOfRangeArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_INDEX_GROWTH, "chainedMissingArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, + "typedArrayCannotStoreMissingValue" to TsRuntimeFeatureLimitationReason.ARRAY_ELEMENT_KIND_WRITE, ) unsupportedMethods.forEach { (methodName, reason) -> diff --git a/usvm-ts/src/test/resources/models/ArrayConstructorEtsIr.ts b/usvm-ts/src/test/resources/models/ArrayConstructorEtsIr.ts new file mode 100644 index 0000000000..8fe9120e3b --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayConstructorEtsIr.ts @@ -0,0 +1,64 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +export class ArrayConstructorEtsIr { + callableArrayCreatesHolesAndAcceptsWrites(): number { + const values = Array(3); + const startsWithUndefined = values[0] === undefined; + values[0] = 4; + values[1] = 5; + values[2] = 6; + + return (startsWithUndefined ? 1 : 0) * 10000 + + values.length * 1000 + + values[0] * 100 + + values[1] * 10 + + values[2]; + } + + callableArraySupportsNestedAssignment(): number { + const result: number[][] = Array(2); + result[0] = [4, 5]; + result[1] = [6]; + + return result.length * 100 + result[0][1] * 10 + result[1][0]; + } + + negativeLength(): any[] { + return Array(-1); + } + + fractionalLength(): any[] { + return Array(1.5); + } + + nanLength(): any[] { + return Array(NaN); + } + + infiniteLength(): any[] { + return Array(Infinity); + } + + oversizedLength(): any[] { + return Array(17); + } + + fullFillInitializesSparseNumberArray(): number { + const values = new Array(3).fill(7); + return values.length * 1000 + values[0] * 100 + values[1] * 10 + values[2]; + } + + fullFillInitializesSparseBooleanArray(): number { + const values = new Array(3).fill(true); + return values.length * 1000 + + (values[0] ? 1 : 0) * 100 + + (values[1] ? 1 : 0) * 10 + + (values[2] ? 1 : 0); + } + + shadowedArrayIsNotModeled(): number { + const Array = (arrayLength?: number): any[] => [arrayLength]; + return Array(2)[0]; + } +} diff --git a/usvm-ts/src/test/resources/models/ErrorEtsIr.ts b/usvm-ts/src/test/resources/models/ErrorEtsIr.ts new file mode 100644 index 0000000000..f8b326a65f --- /dev/null +++ b/usvm-ts/src/test/resources/models/ErrorEtsIr.ts @@ -0,0 +1,77 @@ +class ForeignFields { + overwrittenPrimitiveKinds(): boolean { + const error: any = new Error("original"); + error.message = 7; + error.name = false; + return error.message === 7 && typeof error.message === "number" + && error.name === false && typeof error.name === "boolean"; + } + + overwrittenReferenceKinds(): boolean { + const error: any = new Error("original"); + error.message = null; + error.name = undefined; + return error.message === null && error.name === undefined; + } + + overwrittenObjectAlias(): boolean { + const error: any = new Error("original"); + const payload = { marker: 7 }; + error.message = payload; + return error.message === payload && error.message.marker === 7; + } + + symbolicMessage(message: string): boolean { + const error = new Error(message); + if (message.length === 0) return error.message === message && error.name === "Error"; + return error.message === message && typeof error.message === "string" && error.name === "Error"; + } + + name: number = 17; + message: boolean = true; +} + +export class ErrorEtsIr { + static name(): string { + return new Error("expected message").name; + } + + static message(): string { + return new Error("expected message").message; + } + + static throwError(): number { + throw new Error("expected message"); + } + + static overwrittenName(): string { + const error = new Error("expected message"); + error.name = "CustomError"; + return error.name; + } + + static overwrittenMessage(): string { + const error = new Error("before"); + error.message = "after"; + return error.message; + } + + static anyErrorMessage(): string { + const error: any = new Error("aliased message"); + return error.message; + } + + static anyForeignNameComparison(): number { + const value: any = new ForeignFields(); + return value.name === 17 ? 1 : -1; + } + + static anyForeignMessageComparison(): number { + const value: any = new ForeignFields(); + return value.message === true ? 1 : -1; + } + + static callbackMessage(): string { + return new Error((() => "x") as any).message; + } +} diff --git a/usvm-ts/src/test/resources/models/ErrorModelBackingBoundary.ts b/usvm-ts/src/test/resources/models/ErrorModelBackingBoundary.ts new file mode 100644 index 0000000000..74a68e97fd --- /dev/null +++ b/usvm-ts/src/test/resources/models/ErrorModelBackingBoundary.ts @@ -0,0 +1,12 @@ +export class ErrorModelBackingBoundary { + publicFields(): string { + const error = new Error("before"); + error.name = "CustomError"; + error.message = "after"; + return error.name + "|" + error.message; + } + + allocatedError(): Error { + return new Error("original"); + } +} diff --git a/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts b/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts index 50b9808d09..cc7de8e98f 100644 --- a/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts +++ b/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts @@ -54,6 +54,11 @@ export class NumericBoundarySemantics { const observed = secondAlias[0]; if (values === other) return observed === null ? 1 : -1; return alias[0] === null ? 2 : -1; + typedArrayCannotStoreMissingValue(): number { + const source = [11]; + const destination = [22]; + destination[0] = source[2]; + return destination[0]; } bitwiseNaN(): number { diff --git a/usvm-ts/src/test/resources/models/StringReplaceAllEtsIr.ts b/usvm-ts/src/test/resources/models/StringReplaceAllEtsIr.ts new file mode 100644 index 0000000000..685f56c3a4 --- /dev/null +++ b/usvm-ts/src/test/resources/models/StringReplaceAllEtsIr.ts @@ -0,0 +1,42 @@ +// @ts-nocheck +export class StringReplaceAllEtsIr { + literalMatches(): string { + return "aaaa/aba".replaceAll("aa", "X"); + } + + emptySearch(): string { + return "A😀".replaceAll("", "-"); + } + + substitutions(): string { + return "aba".replaceAll("a", "$$:$&:$`:$':$1"); + } + + noMatches(): string { + return "abc".replaceAll("x", "$&"); + } + + emptyReceiver(): string { + return "".replaceAll("", "$$"); + } + + replacementIsNotSearchedAgain(): string { + return "aa".replaceAll("a", "aa"); + } + + numericSearchIsResidual(): string { + return "123".replaceAll(1, "x"); + } + + numericReplacementIsResidual(): string { + return "abc".replaceAll("a", 1); + } + + callbackReplacementIsResidual(): string { + return "aa".replaceAll("a", (match: string) => match); + } + + callableSearchIsResidual(): string { + return "aa".replaceAll((match: string) => match, "x"); + } +} diff --git a/usvm-ts/src/test/resources/models/UserDefinedErrorEtsIr.ts b/usvm-ts/src/test/resources/models/UserDefinedErrorEtsIr.ts new file mode 100644 index 0000000000..6745cccdae --- /dev/null +++ b/usvm-ts/src/test/resources/models/UserDefinedErrorEtsIr.ts @@ -0,0 +1,14 @@ +class Error { + name: string = "ShadowError"; + message: string; + + constructor(message: string) { + this.message = message; + } +} + +export class UserDefinedErrorEtsIr { + static name(): string { + return new Error("shadow message").name; + } +} diff --git a/usvm-ts/src/test/resources/models/array-constructor-shadow/exported.ts b/usvm-ts/src/test/resources/models/array-constructor-shadow/exported.ts new file mode 100644 index 0000000000..8c3ccc4691 --- /dev/null +++ b/usvm-ts/src/test/resources/models/array-constructor-shadow/exported.ts @@ -0,0 +1,3 @@ +// @ts-nocheck + +export const Array = (length?: number): any[] => [99]; diff --git a/usvm-ts/src/test/resources/models/array-constructor-shadow/main.ts b/usvm-ts/src/test/resources/models/array-constructor-shadow/main.ts new file mode 100644 index 0000000000..524567379e --- /dev/null +++ b/usvm-ts/src/test/resources/models/array-constructor-shadow/main.ts @@ -0,0 +1,10 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +import { Array } from "./exported"; + +export class ImportedArrayShadow { + callImportedArray(): number { + return Array(2)[0]; + } +} diff --git a/usvm-ts/src/test/resources/models/error-storage-owner/ErrorModels.ts b/usvm-ts/src/test/resources/models/error-storage-owner/ErrorModels.ts new file mode 100644 index 0000000000..4eb2d271b8 --- /dev/null +++ b/usvm-ts/src/test/resources/models/error-storage-owner/ErrorModels.ts @@ -0,0 +1,16 @@ +export class ErrorValue { + __usvmErrorName: string = "initial name"; + __usvmErrorMessage: string = "initial message"; + + ordinarySelfFields(): string { + this.__usvmErrorName = "user name"; + this.__usvmErrorMessage = "user message"; + return this.__usvmErrorName + "|" + this.__usvmErrorMessage; + } + ordinarySelfFieldsThroughAny(): boolean { + this.__usvmErrorName = "user name"; + this.__usvmErrorMessage = "user message"; + const alias: any = this; + return alias.__usvmErrorName === "user name" && alias.__usvmErrorMessage === "user message"; + } +} From 21a832eb50c97ef90d8c3a2981d629e552e59ee1 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 01:34:44 +0300 Subject: [PATCH 2/9] Place source semantics regressions in their intended classes --- .../expr/NumericBoundarySemanticsTest.kt | 6 +++++- .../src/test/resources/models/ErrorEtsIr.ts | 18 +++++++++--------- .../models/NumericBoundarySemantics.ts | 2 ++ 3 files changed, 16 insertions(+), 10 deletions(-) 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 index 33e6914d67..94a08f7651 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumericBoundarySemanticsTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/NumericBoundarySemanticsTest.kt @@ -118,7 +118,6 @@ class NumericBoundarySemanticsTest : TsMethodTestRunner() { "negativeArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, "outOfRangeArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_INDEX_GROWTH, "chainedMissingArrayWrite" to TsRuntimeFeatureLimitationReason.ARRAY_NAMED_PROPERTY_WRITE, - "typedArrayCannotStoreMissingValue" to TsRuntimeFeatureLimitationReason.ARRAY_ELEMENT_KIND_WRITE, ) unsupportedMethods.forEach { (methodName, reason) -> @@ -128,6 +127,11 @@ class NumericBoundarySemanticsTest : TsMethodTestRunner() { assertEquals(reason, observer.limitations.single().reason, methodName) } discoverNumber("negativeZeroArrayWrite", expected = 7.0) + discoverProperties( + method = method("typedArrayCannotStoreMissingValue"), + { result -> result == TsTestValue.TsUndefined }, + invariants = arrayOf({ result -> result == TsTestValue.TsUndefined }), + ) } @Test diff --git a/usvm-ts/src/test/resources/models/ErrorEtsIr.ts b/usvm-ts/src/test/resources/models/ErrorEtsIr.ts index f8b326a65f..108947f653 100644 --- a/usvm-ts/src/test/resources/models/ErrorEtsIr.ts +++ b/usvm-ts/src/test/resources/models/ErrorEtsIr.ts @@ -1,5 +1,10 @@ class ForeignFields { - overwrittenPrimitiveKinds(): boolean { + name: number = 17; + message: boolean = true; +} + +export class ErrorEtsIr { + static overwrittenPrimitiveKinds(): boolean { const error: any = new Error("original"); error.message = 7; error.name = false; @@ -7,31 +12,26 @@ class ForeignFields { && error.name === false && typeof error.name === "boolean"; } - overwrittenReferenceKinds(): boolean { + static overwrittenReferenceKinds(): boolean { const error: any = new Error("original"); error.message = null; error.name = undefined; return error.message === null && error.name === undefined; } - overwrittenObjectAlias(): boolean { + static overwrittenObjectAlias(): boolean { const error: any = new Error("original"); const payload = { marker: 7 }; error.message = payload; return error.message === payload && error.message.marker === 7; } - symbolicMessage(message: string): boolean { + static symbolicMessage(message: string): boolean { const error = new Error(message); if (message.length === 0) return error.message === message && error.name === "Error"; return error.message === message && typeof error.message === "string" && error.name === "Error"; } - name: number = 17; - message: boolean = true; -} - -export class ErrorEtsIr { static name(): string { return new Error("expected message").name; } diff --git a/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts b/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts index cc7de8e98f..a59a1beaa9 100644 --- a/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts +++ b/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts @@ -54,6 +54,8 @@ export class NumericBoundarySemantics { const observed = secondAlias[0]; if (values === other) return observed === null ? 1 : -1; return alias[0] === null ? 2 : -1; + } + typedArrayCannotStoreMissingValue(): number { const source = [11]; const destination = [22]; From 91e7b0adf7dd79db71a26074e7fbca485d661000 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 01:36:06 +0300 Subject: [PATCH 3/9] Dispatch callable builtin Array without a heap function pointer --- .../call/intrinsic/TsArrayEtsIrModelFamily.kt | 2 +- .../org/usvm/machine/expr/TsExprResolver.kt | 16 +++++++++++++++- .../call/TsArrayConstructorEtsIrModelTest.kt | 5 ++++- 3 files changed, 20 insertions(+), 3 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index a54874b36e..ac1874c52a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -561,7 +561,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { guard = supportedLength, completion = TsUnknownCallModelCompletion.Normal { val descriptor = arrayDescriptorOf(arrayType) - val result = memory.allocConcrete(descriptor) + val result = memory.allocConcrete(arrayType) val undefinedSlots = List(MAX_SOURCE_ARRAY_LENGTH) { mkUndefinedValue() } memory.initializeArray( arrayHeapRef = result, 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 d037a07c09..8b45d78b56 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 @@ -1357,12 +1357,26 @@ class TsExprResolver( ) scope.doWithState { newStmt(concreteCall) } } else { + val builtinArrayConstructor = expr.isBuiltInArrayConstructor() + val failureReason = if (builtinArrayConstructor) { + TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND + } else { + TsUnknownCallFailureReason.NON_REFERENCE_POINTER + } + val resolvedArguments = if (builtinArrayConstructor) { + val argument = resolve(expr.args.single()) ?: return null + listOf(argument) + } else { + List(expr.args.size) { null } + } + unknownCallDispatcher.dispatch( scope = scope, call = expr, callSite = scope.calcOnState { lastStmt }, - failureReason = TsUnknownCallFailureReason.NON_REFERENCE_POINTER, + failureReason = failureReason, resolvedReceiver = ptr, + resolvedArguments = resolvedArguments, ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayConstructorEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayConstructorEtsIrModelTest.kt index 893ab8b2e7..fbecd4baa9 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayConstructorEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayConstructorEtsIrModelTest.kt @@ -146,7 +146,10 @@ class TsArrayConstructorEtsIrModelTest { val values: List, val events: List, ) { - fun singleNumber(): Double = assertIs(values.single()).number + fun singleNumber(): Double { + assertEquals(1, values.size, "Unknown call events: $events") + return assertIs(values.single()).number + } val modelIds: List get() = events.mapNotNull { event -> From 3c78ecd1bfa3f5c3eae3892c154bf0de43c4fc46 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 01:48:57 +0300 Subject: [PATCH 4/9] Extract runtime dispatch and field storage helpers --- .../call/intrinsic/TsErrorEtsIrModelFamily.kt | 4 +- .../org/usvm/machine/expr/TsExprResolver.kt | 84 +++++++++++-------- .../org/usvm/machine/expr/WriteField.kt | 38 ++++++--- 3 files changed, 77 insertions(+), 49 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt index 3b449964aa..ea1b1d6896 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsErrorEtsIrModelFamily.kt @@ -1,12 +1,11 @@ package org.usvm.machine.call.intrinsic +import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.utils.CONSTRUCTOR_NAME import org.usvm.UConcreteHeapRef -import io.ksmt.utils.asExpr -import org.usvm.machine.expr.builtInErrorSignature import org.usvm.api.evalTypeEquals import org.usvm.api.typeStreamOf import org.usvm.machine.call.TsEtsIrUnknownCallModel @@ -16,6 +15,7 @@ import org.usvm.machine.call.TsUnknownCallFailureReason import org.usvm.machine.call.TsUnknownCallModel import org.usvm.machine.call.TsUnknownCallTarget import org.usvm.machine.call.loadBundledEtsIrUnknownCallModelArtifact +import org.usvm.machine.expr.builtInErrorSignature import org.usvm.types.single /** Narrow built-in `Error(message: string)` constructor model. */ 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 8b45d78b56..f2a9895d3b 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 @@ -1318,19 +1318,10 @@ class TsExprResolver( val callee = scope.calcOnState { associatedFunction[ptr] } if (callee == null) { - val resolvedArguments = if (expr.isBuiltInArrayConstructor()) { - val argument = resolve(expr.args.single()) ?: return null - listOf(argument) - } else { - List(expr.args.size) { null } - } - unknownCallDispatcher.dispatch( - scope = scope, - call = expr, - callSite = scope.calcOnState { lastStmt }, - failureReason = TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, - resolvedReceiver = ptr, - resolvedArguments = resolvedArguments, + dispatchUnresolvedPointer( + expr = expr, + pointer = ptr, + fallbackReason = TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, ) return null } @@ -1345,38 +1336,31 @@ class TsExprResolver( TsExprApproximationResult.NoApproximation -> {} } + val explicitReceiver = expr.receiver + val boundInstance = callee.thisInstance + val instance = if (boundInstance != null) { + boundInstance + } else if (explicitReceiver != null) { + val resolvedReceiver = resolve(explicitReceiver) ?: return null + resolvedReceiver.asExpr(addressSort) + } else { + ctx.mkUndefinedValue() + } + val concreteCall = TsConcreteMethodCallStmt( callee = callee.method, call = expr, resolvedReceiver = ptr, - instance = callee.thisInstance - ?: expr.receiver?.let { resolve(it)?.asExpr(addressSort) ?: return null } - ?: ctx.mkUndefinedValue(), + instance = instance, args = resolvedArgs, returnSite = scope.calcOnState { lastStmt }, ) scope.doWithState { newStmt(concreteCall) } } else { - val builtinArrayConstructor = expr.isBuiltInArrayConstructor() - val failureReason = if (builtinArrayConstructor) { - TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND - } else { - TsUnknownCallFailureReason.NON_REFERENCE_POINTER - } - val resolvedArguments = if (builtinArrayConstructor) { - val argument = resolve(expr.args.single()) ?: return null - listOf(argument) - } else { - List(expr.args.size) { null } - } - - unknownCallDispatcher.dispatch( - scope = scope, - call = expr, - callSite = scope.calcOnState { lastStmt }, - failureReason = failureReason, - resolvedReceiver = ptr, - resolvedArguments = resolvedArguments, + dispatchUnresolvedPointer( + expr = expr, + pointer = ptr, + fallbackReason = TsUnknownCallFailureReason.NON_REFERENCE_POINTER, ) } @@ -1385,6 +1369,34 @@ class TsExprResolver( } } + private fun dispatchUnresolvedPointer( + expr: EtsPtrCallExpr, + pointer: UExpr<*>, + fallbackReason: TsUnknownCallFailureReason, + ) { + val builtinArrayConstructor = expr.isBuiltInArrayConstructor() + val failureReason = if (builtinArrayConstructor) { + TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND + } else { + fallbackReason + } + val resolvedArguments = if (builtinArrayConstructor) { + val argument = resolve(expr.args.single()) ?: return + listOf(argument) + } else { + List(expr.args.size) { null } + } + + unknownCallDispatcher.dispatch( + scope = scope, + call = expr, + callSite = scope.calcOnState { lastStmt }, + failureReason = failureReason, + resolvedReceiver = pointer, + resolvedArguments = resolvedArguments, + ) + } + private fun EtsPtrCallExpr.isBuiltInArrayConstructor(): Boolean { if (callee.name != "Array" || ptr.name != "Array" || args.size != 1) { return false 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 f33ae325f3..b7434ba715 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 @@ -23,9 +23,9 @@ import org.usvm.sizeSort import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult import org.usvm.util.arrayStorageType +import org.usvm.util.boxArrayValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue -import org.usvm.util.boxArrayValue import org.usvm.util.resolveEtsField import org.usvm.util.truncateKnownArrayIndices @@ -178,6 +178,25 @@ private fun TsContext.assignToArrayLength( } } +private fun TsContext.writeErrorModelStorageField( + scope: TsStepScope, + instance: UHeapRef, + field: EtsFieldSignature, + storageField: ErrorStorageField, + value: UExpr<*>, +) { + val payload = boxArrayValue(scope, value) + scope.doWithState { + memory.write( + mkErrorModelStorageLValue(addressSort, instance, storageField), + payload.asExpr(addressSort), + guard = trueExpr, + ) + memory.write(deletedFieldLValue(instance, field), falseExpr, guard = trueExpr) + writtenConcreteFields += instance to field.name + } +} + fun TsContext.assignToInstanceField( scope: TsStepScope, instanceLocal: EtsLocal, @@ -209,16 +228,13 @@ fun TsContext.assignToInstanceField( hierarchy = hierarchy, ).storageField if (errorStorageField != null) { - val payload = boxArrayValue(scope, expr) - return scope.doWithState { - memory.write( - mkErrorModelStorageLValue(addressSort, unwrappedInstance, errorStorageField), - payload.asExpr(addressSort), - guard = trueExpr, - ) - memory.write(deletedFieldLValue(unwrappedInstance, field), falseExpr, guard = trueExpr) - writtenConcreteFields += unwrappedInstance to field.name - } + return writeErrorModelStorageField( + scope = scope, + instance = unwrappedInstance, + field = field, + storageField = errorStorageField, + value = expr, + ) } val objectLiteralClass = objectLiteralClass(scope, unwrappedInstance, hierarchy) From 4826d79358eac8de71b67a1adfe69d7722442511 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 02:02:39 +0300 Subject: [PATCH 5/9] Preserve modeled Error runtime identity through thrown value packets --- .../usvm/machine/expr/ErrorModelStorage.kt | 8 ++++ .../usvm/machine/interpreter/TsInterpreter.kt | 40 ++++++++++++++++++- .../machine/call/TsErrorEtsIrModelTest.kt | 24 ++++++++--- .../call/TsErrorSourceSemanticsTest.kt | 19 +++++++++ .../call/TsModeledErrorIdentityTest.kt | 32 +++++++++++++++ .../src/test/resources/models/ErrorEtsIr.ts | 24 +++++++++++ 6 files changed, 139 insertions(+), 8 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/call/TsModeledErrorIdentityTest.kt diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt index c718d3a592..0d29aef4cc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt @@ -5,11 +5,13 @@ import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsField import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsType import org.usvm.UConcreteHeapRef import org.usvm.UHeapRef import org.usvm.USort import org.usvm.api.typeStreamOf import org.usvm.collection.field.UFieldLValue +import org.usvm.machine.TS_TYPE_ERROR_TYPE import org.usvm.machine.TsContext import org.usvm.machine.call.intrinsic.TsErrorEtsIrModelFamily import org.usvm.machine.interpreter.TsStepScope @@ -20,6 +22,12 @@ import org.usvm.util.resolveEtsField internal val builtInErrorSignature = EtsClassSignature.UNKNOWN.copy(name = "Error") +/** Matches exact SDK identities and the interpreter's own TypeError, excluding source class shadows. */ +internal fun EtsType.isModeledErrorType(): Boolean = + this == EtsClassType(signature = builtInErrorSignature) || + this == EtsClassType(signature = EtsClassSignature.UNKNOWN.copy(name = "TypeError")) || + this == TS_TYPE_ERROR_TYPE + internal const val ERROR_NAME_STORAGE_FIELD = "__usvmErrorName" internal const val ERROR_MESSAGE_STORAGE_FIELD = "__usvmErrorMessage" 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 e6e1cdd8f3..5bf7c0fd4d 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 @@ -38,6 +38,7 @@ import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.callExpr import org.usvm.StepResult import org.usvm.StepScope +import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UInterpreter import org.usvm.api.evalTypeEquals @@ -47,6 +48,7 @@ import org.usvm.api.typeStreamOf import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.forkblacklists.UForkBlackList import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.isTrue import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext import org.usvm.machine.TsGraph @@ -69,9 +71,11 @@ import org.usvm.machine.expr.handleAssignToLocal import org.usvm.machine.expr.handleAssignToProperty import org.usvm.machine.expr.handleAssignToStaticField import org.usvm.machine.expr.handleDefineDataProperty +import org.usvm.machine.expr.isModeledErrorType import org.usvm.machine.expr.mkNotNullOrUndefined import org.usvm.machine.expr.mkTruthyExpr import org.usvm.machine.expr.readGlobal +import org.usvm.machine.expr.resolveHeapRef import org.usvm.machine.expr.tryApproximateInstanceCall import org.usvm.machine.expr.writeGlobal import org.usvm.machine.state.TsMethodResult @@ -91,6 +95,7 @@ import org.usvm.solver.UUnknownResult import org.usvm.targets.UTargetsSet import org.usvm.types.TypesResult import org.usvm.types.single +import org.usvm.types.singleOrNull import org.usvm.util.executableOverloadImplementation import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue @@ -727,9 +732,16 @@ class TsInterpreter( observer?.onThrowStatement(exprResolver.simpleValueResolver, stmt, scope) - val exception = exprResolver.resolve(stmt.exception) ?: return + val resolvedException = exprResolver.resolve(stmt.exception) ?: return + val exception = normalizeThrownValue(scope, resolvedException) ?: return val exceptionType: EtsType = when (exception.sort) { - ctx.addressSort -> EtsStringType // TODO: improve object type detection + ctx.addressSort -> { + val reference = exception as? UConcreteHeapRef + val runtimeType = reference?.let { ref -> + scope.calcOnState { memory.typeStreamOf(ref).singleOrNull() } + } + runtimeType?.takeIf { type -> type.isModeledErrorType() } ?: EtsStringType + } ctx.fp64Sort -> EtsNumberType ctx.boolSort -> EtsBooleanType else -> EtsStringType @@ -740,6 +752,30 @@ class TsInterpreter( } } + private fun normalizeThrownValue(scope: TsStepScope, exception: UExpr<*>): UExpr<*>? = with(ctx) { + var value = exception + while (value.sort == addressSort) { + val reference = resolveHeapRef(scope, value.asExpr(addressSort)) ?: return null + if (!reference.isFakeObject()) return reference + + val type = reference.getFakeType(scope) + val booleanKind = scope.calcOnState { models.first().eval(type.boolTypeExpr).isTrue } + val numberKind = scope.calcOnState { models.first().eval(type.fpTypeExpr).isTrue } + val selectedKind = when { + booleanKind -> type.boolTypeExpr + numberKind -> type.fpTypeExpr + else -> type.refTypeExpr + } + scope.fork(selectedKind) ?: return null + value = when { + booleanKind -> reference.extractBool(scope) + numberKind -> reference.extractFp(scope) + else -> reference.extractRef(scope) + } + } + value + } + private fun visitNopStmt(scope: TsStepScope, stmt: EtsNopStmt) { val successors = graph.successors(stmt).toList() when (successors.size) { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt index edc3a7ae09..b182cccdc5 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt @@ -1,5 +1,11 @@ package org.usvm.machine.call +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration +import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.EtsIrProvider @@ -13,14 +19,10 @@ import org.usvm.machine.TsInterpreterObserver import org.usvm.machine.TsMachine import org.usvm.machine.TsOptions import org.usvm.machine.call.intrinsic.TsErrorEtsIrModelFamily +import org.usvm.machine.expr.builtInErrorSignature import org.usvm.machine.state.TsMethodResult 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 TsErrorEtsIrModelTest { private val builtInSourceFile = loadEtsFileAutoConvert( @@ -50,11 +52,21 @@ class TsErrorEtsIrModelTest { val result = analyze(scene = builtInScene, className = "ErrorEtsIr", methodName = "throwError") assertEquals(1, result.states.size) - assertIs(result.states.single().methodResult) + val exception = assertIs(result.states.single().methodResult) + assertEquals(EtsClassType(signature = builtInErrorSignature), exception.type) assertEquals(listOf(TsErrorEtsIrModelFamily.CONSTRUCTOR_ID), result.modelIds) assertTrue(result.values.single() is TsTestValue.TsException) } + @Test + fun `any field Error throw retains actual builtin exception type`() { + val result = analyze(scene = builtInScene, className = "ErrorEtsIr", methodName = "throwAnyFieldError") + + val exception = assertIs(result.states.single().methodResult) + assertEquals(EtsClassType(signature = builtInErrorSignature), exception.type) + assertEquals(listOf(TsErrorEtsIrModelFamily.CONSTRUCTOR_ID), result.modelIds) + } + @Test fun `Error model storage does not affect ordinary any field resolution`() { listOf("anyForeignNameComparison", "anyForeignMessageComparison").forEach { methodName -> diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt index 3e659593a6..7a48cfa000 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt @@ -67,6 +67,25 @@ class TsErrorSourceSemanticsTest : TsMethodTestRunner() { ) } + @Test + fun `throwing an Error through an any field preserves caught identity and payload`() { + discoverProperties( + method = getMethod(methodName = "catchAnyFieldError", className = "ErrorEtsIr"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `conditional any thrown values preserve both Error and numeric kinds`() { + discoverProperties( + method = getMethod(methodName = "catchConditionalErrorOrNumber", className = "ErrorEtsIr"), + { flag, result -> flag.value && result.number == 2.0 }, + { flag, result -> !flag.value && result.number == 1.0 }, + invariants = arrayOf({ flag, result -> result.number == if (flag.value) 2.0 else 1.0 }), + ) + } + @Test fun `source name preserves Error string semantics`() { discoverProperties( diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsModeledErrorIdentityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsModeledErrorIdentityTest.kt new file mode 100644 index 0000000000..ec26eab5f2 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsModeledErrorIdentityTest.kt @@ -0,0 +1,32 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFileSignature +import org.junit.jupiter.api.Test +import org.usvm.machine.TS_TYPE_ERROR_TYPE +import org.usvm.machine.expr.isModeledErrorType +import kotlin.test.assertFalse +import kotlin.test.assertTrue + +class TsModeledErrorIdentityTest { + @Test + fun `native SDK and interpreter Error identities are recognized`() { + val sdkError = EtsClassType(signature = EtsClassSignature.UNKNOWN.copy(name = "Error")) + val sdkTypeError = EtsClassType(signature = EtsClassSignature.UNKNOWN.copy(name = "TypeError")) + + assertTrue(sdkError.isModeledErrorType()) + assertTrue(sdkTypeError.isModeledErrorType()) + assertTrue(TS_TYPE_ERROR_TYPE.isModeledErrorType()) + } + + @Test + fun `same named application classes do not become builtin Error identities`() { + val sourceFile = EtsFileSignature(projectName = "application", fileName = "ShadowErrors.ts") + val sourceError = EtsClassType(signature = EtsClassSignature(name = "Error", file = sourceFile)) + val sourceTypeError = EtsClassType(signature = EtsClassSignature(name = "TypeError", file = sourceFile)) + + assertFalse(sourceError.isModeledErrorType()) + assertFalse(sourceTypeError.isModeledErrorType()) + } +} diff --git a/usvm-ts/src/test/resources/models/ErrorEtsIr.ts b/usvm-ts/src/test/resources/models/ErrorEtsIr.ts index 108947f653..daece894c6 100644 --- a/usvm-ts/src/test/resources/models/ErrorEtsIr.ts +++ b/usvm-ts/src/test/resources/models/ErrorEtsIr.ts @@ -40,6 +40,30 @@ export class ErrorEtsIr { return new Error("expected message").message; } + static throwAnyFieldError(): number { + const container: any = { value: new Error("field error") }; + throw container.value; + } + + static catchAnyFieldError(): boolean { + const container: any = { value: new Error("field error") }; + try { + throw container.value; + } catch (error) { + return error === container.value && error.message === "field error" && error.name === "Error"; + } + } + + static catchConditionalErrorOrNumber(flag: boolean): number { + const container: any = { value: flag ? new Error("conditional error") : 7 }; + try { + throw container.value; + } catch (error) { + if (typeof error === "number") return error === 7 ? 1 : -1; + return error.message === "conditional error" && error.name === "Error" ? 2 : -2; + } + } + static throwError(): number { throw new Error("expected message"); } From eda33404fa69c15242914bc93e5c8c61406bb8e5 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 02:12:30 +0300 Subject: [PATCH 6/9] Order modeled error test imports consistently --- .../machine/call/intrinsic/TsArrayEtsIrModelFamily.kt | 2 +- .../org/usvm/machine/call/TsErrorEtsIrModelTest.kt | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index ac1874c52a..86d00d3ee4 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -82,7 +82,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { if (hasUnsupportedArrayShape) { falseExpr } else { - val elementSort = typeToSort(receiverType.componentType) + val elementSort = typeToSort(receiverType.elementType) val hasNoMissingSlots = array is UConcreteHeapRef && state.isUnmodifiedDenseInputArray(array, receiverType) val excludesMissingSlot = when { diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt index b182cccdc5..6608fb1aef 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt @@ -1,10 +1,5 @@ package org.usvm.machine.call -import kotlin.test.Test -import kotlin.test.assertEquals -import kotlin.test.assertIs -import kotlin.test.assertTrue -import kotlin.time.Duration import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsScene @@ -23,6 +18,11 @@ import org.usvm.machine.expr.builtInErrorSignature import org.usvm.machine.state.TsMethodResult 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 TsErrorEtsIrModelTest { private val builtInSourceFile = loadEtsFileAutoConvert( From e6dd1452cd4b8ccad4cdd97ad97f6b04d5874dac Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 23:29:24 +0300 Subject: [PATCH 7/9] Extract modeled Error helpers after rebasing on main --- .../call/intrinsic/TsArrayEtsIrModelFamily.kt | 2 +- .../usvm/machine/expr/ErrorModelStorage.kt | 44 +++++++++++++++++ .../org/usvm/machine/expr/WriteField.kt | 41 +++++++++++----- .../usvm/machine/interpreter/TsInterpreter.kt | 48 ++----------------- 4 files changed, 79 insertions(+), 56 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index 86d00d3ee4..ac1874c52a 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt @@ -82,7 +82,7 @@ internal object TsArrayEtsIrModelFamily : TsBuiltInUnknownCallModelFamily { if (hasUnsupportedArrayShape) { falseExpr } else { - val elementSort = typeToSort(receiverType.elementType) + val elementSort = typeToSort(receiverType.componentType) val hasNoMissingSlots = array is UConcreteHeapRef && state.isUnmodifiedDenseInputArray(array, receiverType) val excludesMissingSlot = when { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt index 0d29aef4cc..89de6b8ed2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt @@ -1,16 +1,22 @@ package org.usvm.machine.expr +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsField import org.jacodb.ets.model.EtsFieldSignature import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsNumberType +import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType import org.usvm.UConcreteHeapRef +import org.usvm.UExpr import org.usvm.UHeapRef import org.usvm.USort import org.usvm.api.typeStreamOf import org.usvm.collection.field.UFieldLValue +import org.usvm.isTrue import org.usvm.machine.TS_TYPE_ERROR_TYPE import org.usvm.machine.TsContext import org.usvm.machine.call.intrinsic.TsErrorEtsIrModelFamily @@ -111,3 +117,41 @@ internal fun TsContext.resolveModelStorageField( isModelStorageField = storageField != null, ) } + +internal fun TsContext.normalizeThrownValue(scope: TsStepScope, exception: UExpr<*>): UExpr<*>? { + var value = exception + while (value.sort == addressSort) { + val reference = resolveHeapRef(scope, value.asExpr(addressSort)) ?: return null + if (!reference.isFakeObject()) return reference + + val type = reference.getFakeType(scope) + val booleanKind = scope.calcOnState { models.first().eval(type.boolTypeExpr).isTrue } + val numberKind = scope.calcOnState { models.first().eval(type.fpTypeExpr).isTrue } + val selectedKind = when { + booleanKind -> type.boolTypeExpr + numberKind -> type.fpTypeExpr + else -> type.refTypeExpr + } + scope.fork(selectedKind) ?: return null + value = when { + booleanKind -> reference.extractBool(scope) + numberKind -> reference.extractFp(scope) + else -> reference.extractRef(scope) + } + } + return value +} + +internal fun TsContext.thrownValueType(scope: TsStepScope, exception: UExpr<*>): EtsType = + when (exception.sort) { + addressSort -> { + val reference = exception as? UConcreteHeapRef + val runtimeType = reference?.let { ref -> + scope.calcOnState { memory.typeStreamOf(ref).singleOrNull() } + } + runtimeType?.takeIf { type -> type.isModeledErrorType() } ?: EtsStringType + } + fp64Sort -> EtsNumberType + boolSort -> EtsBooleanType + else -> EtsStringType + } 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 b7434ba715..f82e48758a 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 @@ -197,6 +197,32 @@ private fun TsContext.writeErrorModelStorageField( } } +private fun TsContext.writeModeledErrorField( + scope: TsStepScope, + instanceLocal: EtsLocal, + instance: UHeapRef, + field: EtsFieldSignature, + value: UExpr<*>, + hierarchy: EtsHierarchy, +): Boolean { + val storageField = resolveModelStorageField( + scope = scope, + instanceLocal = instanceLocal, + instance = instance, + field = field, + hierarchy = hierarchy, + ).storageField ?: return false + + writeErrorModelStorageField( + scope = scope, + instance = instance, + field = field, + storageField = storageField, + value = value, + ) + return true +} + fun TsContext.assignToInstanceField( scope: TsStepScope, instanceLocal: EtsLocal, @@ -220,22 +246,15 @@ fun TsContext.assignToInstanceField( return Unit } - val errorStorageField = resolveModelStorageField( + val wroteModeledErrorField = writeModeledErrorField( scope = scope, instanceLocal = instanceLocal, instance = unwrappedInstance, field = field, + value = expr, hierarchy = hierarchy, - ).storageField - if (errorStorageField != null) { - return writeErrorModelStorageField( - scope = scope, - instance = unwrappedInstance, - field = field, - storageField = errorStorageField, - value = expr, - ) - } + ) + if (wroteModeledErrorField) return Unit val objectLiteralClass = objectLiteralClass(scope, unwrappedInstance, hierarchy) val declaredObjectLiteralField = objectLiteralClass?.fields?.singleOrNull { it.name == field.name } 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 5bf7c0fd4d..7716244634 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 @@ -6,7 +6,6 @@ import org.jacodb.ets.model.EtsAnyType import org.jacodb.ets.model.EtsArrayAccess import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsAssignStmt -import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsCallStmt import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsClosureFieldRef @@ -21,7 +20,6 @@ import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod import org.jacodb.ets.model.EtsNopStmt import org.jacodb.ets.model.EtsNullType -import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsPropertyRef import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsReturnStmt @@ -38,7 +36,6 @@ import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.callExpr import org.usvm.StepResult import org.usvm.StepScope -import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UInterpreter import org.usvm.api.evalTypeEquals @@ -48,7 +45,6 @@ import org.usvm.api.typeStreamOf import org.usvm.collections.immutable.internal.MutabilityOwnership import org.usvm.forkblacklists.UForkBlackList import org.usvm.isAllocatedConcreteHeapRef -import org.usvm.isTrue import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext import org.usvm.machine.TsGraph @@ -71,11 +67,11 @@ import org.usvm.machine.expr.handleAssignToLocal import org.usvm.machine.expr.handleAssignToProperty import org.usvm.machine.expr.handleAssignToStaticField import org.usvm.machine.expr.handleDefineDataProperty -import org.usvm.machine.expr.isModeledErrorType import org.usvm.machine.expr.mkNotNullOrUndefined import org.usvm.machine.expr.mkTruthyExpr +import org.usvm.machine.expr.normalizeThrownValue import org.usvm.machine.expr.readGlobal -import org.usvm.machine.expr.resolveHeapRef +import org.usvm.machine.expr.thrownValueType import org.usvm.machine.expr.tryApproximateInstanceCall import org.usvm.machine.expr.writeGlobal import org.usvm.machine.state.TsMethodResult @@ -95,7 +91,6 @@ import org.usvm.solver.UUnknownResult import org.usvm.targets.UTargetsSet import org.usvm.types.TypesResult import org.usvm.types.single -import org.usvm.types.singleOrNull import org.usvm.util.executableOverloadImplementation import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue @@ -733,49 +728,14 @@ class TsInterpreter( observer?.onThrowStatement(exprResolver.simpleValueResolver, stmt, scope) val resolvedException = exprResolver.resolve(stmt.exception) ?: return - val exception = normalizeThrownValue(scope, resolvedException) ?: return - val exceptionType: EtsType = when (exception.sort) { - ctx.addressSort -> { - val reference = exception as? UConcreteHeapRef - val runtimeType = reference?.let { ref -> - scope.calcOnState { memory.typeStreamOf(ref).singleOrNull() } - } - runtimeType?.takeIf { type -> type.isModeledErrorType() } ?: EtsStringType - } - ctx.fp64Sort -> EtsNumberType - ctx.boolSort -> EtsBooleanType - else -> EtsStringType - } + val exception = ctx.normalizeThrownValue(scope, resolvedException) ?: return + val exceptionType = ctx.thrownValueType(scope, exception) scope.doWithState { methodResult = TsMethodResult.TsException(exception, exceptionType) } } - private fun normalizeThrownValue(scope: TsStepScope, exception: UExpr<*>): UExpr<*>? = with(ctx) { - var value = exception - while (value.sort == addressSort) { - val reference = resolveHeapRef(scope, value.asExpr(addressSort)) ?: return null - if (!reference.isFakeObject()) return reference - - val type = reference.getFakeType(scope) - val booleanKind = scope.calcOnState { models.first().eval(type.boolTypeExpr).isTrue } - val numberKind = scope.calcOnState { models.first().eval(type.fpTypeExpr).isTrue } - val selectedKind = when { - booleanKind -> type.boolTypeExpr - numberKind -> type.fpTypeExpr - else -> type.refTypeExpr - } - scope.fork(selectedKind) ?: return null - value = when { - booleanKind -> reference.extractBool(scope) - numberKind -> reference.extractFp(scope) - else -> reference.extractRef(scope) - } - } - value - } - private fun visitNopStmt(scope: TsStepScope, stmt: EtsNopStmt) { val successors = graph.successors(stmt).toList() when (successors.size) { From 9f245b3727f7fe7a961fa015892551b48d1a2134 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 23:50:26 +0300 Subject: [PATCH 8/9] Keep modeled Error storage at field access boundaries --- .../usvm/machine/expr/ErrorModelStorage.kt | 76 ++++++++++--------- .../kotlin/org/usvm/machine/expr/ReadField.kt | 43 +++++------ .../org/usvm/machine/expr/WriteField.kt | 48 ------------ .../call/TsErrorSourceSemanticsTest.kt | 10 +++ .../src/test/resources/models/ErrorEtsIr.ts | 10 +++ 5 files changed, 81 insertions(+), 106 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt index 89de6b8ed2..cbddae1432 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt @@ -4,9 +4,7 @@ import io.ksmt.utils.asExpr import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType -import org.jacodb.ets.model.EtsField import org.jacodb.ets.model.EtsFieldSignature -import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsNumberType import org.jacodb.ets.model.EtsStringType import org.jacodb.ets.model.EtsType @@ -22,9 +20,7 @@ import org.usvm.machine.TsContext import org.usvm.machine.call.intrinsic.TsErrorEtsIrModelFamily import org.usvm.machine.interpreter.TsStepScope import org.usvm.types.singleOrNull -import org.usvm.util.EtsHierarchy -import org.usvm.util.TsResolutionResult -import org.usvm.util.resolveEtsField +import org.usvm.util.boxArrayValue internal val builtInErrorSignature = EtsClassSignature.UNKNOWN.copy(name = "Error") @@ -75,47 +71,57 @@ internal fun EtsFieldSignature.errorModelStorageField(): ErrorStorageField? { } } -internal data class ModelStorageFieldResolution( - val storageField: ErrorStorageField?, - val etsField: TsResolutionResult, - val isModelStorageField: Boolean, -) +/** Only unresolved SDK Error fields need the unqualified declaration lookup. */ +internal fun EtsFieldSignature.runtimeFieldSignature(): EtsFieldSignature = + if (isUnresolvedErrorField()) copy(enclosingClass = EtsClassSignature.UNKNOWN) else this -internal fun TsContext.resolveModelStorageField( +private fun TsContext.resolveErrorStorageField( scope: TsStepScope, - instanceLocal: EtsLocal?, instance: UHeapRef, field: EtsFieldSignature, - hierarchy: EtsHierarchy, -): ModelStorageFieldResolution { +): ErrorStorageField? { val definitionStorageField = field.errorModelDefinitionStorageField().takeIf { applicationAndSdkClasses.none { owner -> owner.signature == field.enclosingClass } && TsErrorEtsIrModelFamily.ownsStorageDefinitionField(field) } - val candidateStorageField = definitionStorageField ?: field.errorModelStorageField() - val runtimeType = (instance as? UConcreteHeapRef) - ?.takeIf { candidateStorageField != null } - ?.let { concreteInstance -> - scope.calcOnState { memory.typeStreamOf(concreteInstance).singleOrNull() } - } - val storageField = candidateStorageField.takeIf { - runtimeType == EtsClassType(signature = builtInErrorSignature) + val candidateStorageField = definitionStorageField ?: field.errorModelStorageField() ?: return null + val concreteInstance = instance as? UConcreteHeapRef ?: return null + val runtimeType = scope.calcOnState { memory.typeStreamOf(concreteInstance).singleOrNull() } + + return candidateStorageField.takeIf { runtimeType == EtsClassType(signature = builtInErrorSignature) } +} + +internal fun TsContext.readModeledErrorField( + scope: TsStepScope, + instance: UHeapRef, + field: EtsFieldSignature, +): UExpr<*>? { + val storageField = resolveErrorStorageField(scope, instance, field) ?: return null + + return scope.calcOnState { + memory.read(mkErrorModelStorageLValue(addressSort, instance, storageField)) } - val etsField = when { - storageField != null -> TsResolutionResult.Empty - field.isUnresolvedErrorField() -> resolveEtsField( - instance = instanceLocal, - field = field.copy(enclosingClass = EtsClassSignature.UNKNOWN), - hierarchy = hierarchy, +} + +internal fun TsContext.writeModeledErrorField( + scope: TsStepScope, + instance: UHeapRef, + field: EtsFieldSignature, + value: UExpr<*>, +): Boolean { + val storageField = resolveErrorStorageField(scope, instance, field) ?: return false + val payload = boxArrayValue(scope, value) + + scope.doWithState { + memory.write( + mkErrorModelStorageLValue(addressSort, instance, storageField), + payload.asExpr(addressSort), + guard = trueExpr, ) - else -> resolveEtsField(instanceLocal, field, hierarchy) + memory.write(deletedFieldLValue(instance, field), falseExpr, guard = trueExpr) + writtenConcreteFields += instance to field.name } - - return ModelStorageFieldResolution( - storageField = storageField, - etsField = etsField, - isModelStorageField = storageField != null, - ) + return true } internal fun TsContext.normalizeThrownValue(scope: TsStepScope, exception: UExpr<*>): UExpr<*>? { 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 25c4214bcc..b6b34f38b0 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 @@ -50,6 +50,7 @@ import org.usvm.util.mkFieldLValue import org.usvm.util.mkStringBackingElementLValue import org.usvm.util.mkStringBackingLValue import org.usvm.util.mkStringBackingLengthLValue +import org.usvm.util.resolveEtsField private val logger = KotlinLogging.logger {} @@ -147,13 +148,10 @@ private fun TsContext.resolveDeclaredField( val deleted = scope.calcOnState { memory.read(deletedFieldLValue(instance, field)) } if (deleted.isTrue) return mkUndefinedValue() - val (errorStorageField, resolvedField, isModelStorageField) = resolveModelStorageField( - scope = scope, - instanceLocal = local, - instance = instance, - field = field, - hierarchy = hierarchy, - ) + val modeledValue = readModeledErrorField(scope, instance, field) + if (modeledValue != null) return applyFieldDeletion(scope, deleted, modeledValue) + + val resolvedField = resolveEtsField(local, field.runtimeFieldSignature(), hierarchy) // A literal's own declarations, rather than scene-wide same-name fields, determine its initial storage. val objectClass = objectLiteralClass(scope, instance, hierarchy) @@ -166,20 +164,20 @@ private fun TsContext.resolveDeclaredField( val declaredLiteralField = objectClass?.fields?.singleOrNull { it.name == field.name } val writtenSort = scope.calcOnState { writtenObjectLiteralFieldSorts[instance to field.name] } val declaredLiteralSort = declaredLiteralField?.let { typeToSort(it.type) } - val storageSort = if (errorStorageField != null) { - addressSort - } else { - writtenSort ?: declaredLiteralSort ?: resolvedFieldSort(scope, instance, field, resolvedField, hierarchy) - } - val declaredType = if (errorStorageField != null) { - null - } else if (objectClass != null) { + val storageSort = writtenSort ?: declaredLiteralSort ?: resolvedFieldSort( + scope = scope, + instance = instance, + field = field, + resolved = resolvedField, + hierarchy = hierarchy, + ) + val declaredType = if (objectClass != null) { declaredLiteralField?.type } else { (resolvedField as? TsResolutionResult.Unique)?.property?.type } - val requiresDeclaredPresence = !wasWritten && !isModelStorageField + val requiresDeclaredPresence = !wasWritten if (requiresDeclaredPresence) { val fieldExists = scope.calcOnState { memory.types.evalIsSubtype(instance, EtsAuxiliaryType(properties = setOf(field.name))) @@ -187,8 +185,12 @@ private fun TsContext.resolveDeclaredField( scope.assert(fieldExists) ?: return null } - val storedValue = readField(scope, instance, field, storageSort, errorStorageField) + val storedValue = readField(scope, instance, field, storageSort) val value = materializeFieldValue(scope, storedValue, storageSort, declaredType) ?: return null + return applyFieldDeletion(scope, deleted, value) +} + +private fun TsContext.applyFieldDeletion(scope: TsStepScope, deleted: UBoolExpr, value: UExpr<*>): UExpr<*> { if (deleted.isFalse) return value // Conditional deletion yields undefined on the deleted branch, while preserving the stored runtime kind. @@ -341,14 +343,9 @@ private fun TsContext.readField( instance: UHeapRef, field: EtsFieldSignature, sort: USort, - errorStorageField: ErrorStorageField?, ): UExpr<*> { if (sort !is TsUnresolvedSort) { - val lValue = if (errorStorageField == null) { - mkFieldLValue(sort, instance, field.name) - } else { - mkErrorModelStorageLValue(sort, instance, errorStorageField) - } + val lValue = mkFieldLValue(sort, instance, field.name) return scope.calcOnState { memory.read(lValue) } } 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 f82e48758a..61acf67a0d 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 @@ -23,7 +23,6 @@ import org.usvm.sizeSort import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult import org.usvm.util.arrayStorageType -import org.usvm.util.boxArrayValue import org.usvm.util.mkArrayLengthLValue import org.usvm.util.mkFieldLValue import org.usvm.util.resolveEtsField @@ -178,51 +177,6 @@ private fun TsContext.assignToArrayLength( } } -private fun TsContext.writeErrorModelStorageField( - scope: TsStepScope, - instance: UHeapRef, - field: EtsFieldSignature, - storageField: ErrorStorageField, - value: UExpr<*>, -) { - val payload = boxArrayValue(scope, value) - scope.doWithState { - memory.write( - mkErrorModelStorageLValue(addressSort, instance, storageField), - payload.asExpr(addressSort), - guard = trueExpr, - ) - memory.write(deletedFieldLValue(instance, field), falseExpr, guard = trueExpr) - writtenConcreteFields += instance to field.name - } -} - -private fun TsContext.writeModeledErrorField( - scope: TsStepScope, - instanceLocal: EtsLocal, - instance: UHeapRef, - field: EtsFieldSignature, - value: UExpr<*>, - hierarchy: EtsHierarchy, -): Boolean { - val storageField = resolveModelStorageField( - scope = scope, - instanceLocal = instanceLocal, - instance = instance, - field = field, - hierarchy = hierarchy, - ).storageField ?: return false - - writeErrorModelStorageField( - scope = scope, - instance = instance, - field = field, - storageField = storageField, - value = value, - ) - return true -} - fun TsContext.assignToInstanceField( scope: TsStepScope, instanceLocal: EtsLocal, @@ -248,11 +202,9 @@ fun TsContext.assignToInstanceField( val wroteModeledErrorField = writeModeledErrorField( scope = scope, - instanceLocal = instanceLocal, instance = unwrappedInstance, field = field, value = expr, - hierarchy = hierarchy, ) if (wroteModeledErrorField) return Unit diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt index 7a48cfa000..b0526612ab 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt @@ -57,6 +57,16 @@ class TsErrorSourceSemanticsTest : TsMethodTestRunner() { ) } + @Test + fun `deletion and reassignment preserve modeled message storage on both branches`() { + discoverProperties( + method = getMethod(methodName = "deletedAndReassignedMessage", className = "ErrorEtsIr"), + { flag, result -> flag.value && result.value }, + { flag, result -> !flag.value && result.value }, + invariants = arrayOf({ _, result -> result.value }), + ) + } + @Test fun `ordinary symbolic string message remains eligible and retains identity`() { discoverProperties( diff --git a/usvm-ts/src/test/resources/models/ErrorEtsIr.ts b/usvm-ts/src/test/resources/models/ErrorEtsIr.ts index daece894c6..8baad3a7b0 100644 --- a/usvm-ts/src/test/resources/models/ErrorEtsIr.ts +++ b/usvm-ts/src/test/resources/models/ErrorEtsIr.ts @@ -26,6 +26,16 @@ export class ErrorEtsIr { return error.message === payload && error.message.marker === 7; } + static deletedAndReassignedMessage(flag: boolean): boolean { + const error: any = new Error("initial"); + if (flag) delete error.message; + const afterDelete = error.message; + const deletionMatches = flag ? afterDelete === undefined : afterDelete === "initial"; + + error.message = 7; + return deletionMatches && error.message === 7 && typeof error.message === "number"; + } + static symbolicMessage(message: string): boolean { const error = new Error(message); if (message.length === 0) return error.message === message && error.name === "Error"; From 6be44b9a31a4b3b1e702a35268edcb6298ffbfa1 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 13 Oct 2026 23:50:26 +0300 Subject: [PATCH 9/9] Preserve ETS casts by default and opt into TypeScript assertion erasure --- .../ts/calls/CurrentTsCallsSymbolicEngine.kt | 1 + .../calls/CurrentTsCallsTypeAssertionTest.kt | 36 ++++++++++ usvm-ts/UNKNOWN_CALL_MODELS.md | 4 +- .../main/kotlin/org/usvm/machine/TsOptions.kt | 2 + .../org/usvm/machine/expr/TsExprResolver.kt | 8 ++- .../org/usvm/machine/expr/TypeAssertions.kt | 37 ++++++++++ .../machine/TsTypeAssertionOptionsTest.kt | 71 +++++++++++++++++++ .../machine/call/TsArrayShiftReplayTest.kt | 2 +- .../machine/call/TsErrorEtsIrModelTest.kt | 2 +- .../resources/models/TypeAssertionOptions.ts | 27 +++++++ 10 files changed, 185 insertions(+), 5 deletions(-) create mode 100644 usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsTypeAssertionTest.kt create mode 100644 usvm-ts/src/main/kotlin/org/usvm/machine/expr/TypeAssertions.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/TsTypeAssertionOptionsTest.kt create mode 100644 usvm-ts/src/test/resources/models/TypeAssertionOptions.ts diff --git a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt index 3235a2eb7e..6bb8b72162 100644 --- a/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt +++ b/usvm-ts-calls/src/main/kotlin/org/usvm/ts/calls/CurrentTsCallsSymbolicEngine.kt @@ -163,6 +163,7 @@ internal class CurrentTsCallsSymbolicEngine( maxArraySize = maxOf(TsOptions().maxArraySize, inputCapacity), unknownCallModelSelection = modelSelection, unknownCallFallback = request.profile.fallback, + eraseTypeAssertions = true, ) val symbolicInputs = CallsSymbolicInputs( inputs = request.function.inputs, diff --git a/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsTypeAssertionTest.kt b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsTypeAssertionTest.kt new file mode 100644 index 0000000000..4622d2266a --- /dev/null +++ b/usvm-ts-calls/src/test/kotlin/org/usvm/ts/calls/CurrentTsCallsTypeAssertionTest.kt @@ -0,0 +1,36 @@ +package org.usvm.ts.calls + +import org.usvm.ts.pbt.model.JsConcreteValue +import org.usvm.ts.pbt.model.NumberDomain +import org.usvm.ts.pbt.model.PropertyInput +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertNotNull + +internal class CurrentTsCallsTypeAssertionTest : CurrentTsCallsSymbolicEngineTestSupport() { + @Test + fun `Calls erases type assertions and replays the original runtime number`() { + val fixture = fixture( + source = """ + export function assertedNumber(value: number): boolean { + const asserted = value as unknown as string; + if (typeof asserted === "number" && asserted === 42) { + return true; + } + return false; + } + """.trimIndent(), + exportName = "assertedNumber", + inputs = listOf(PropertyInput(name = "value", domain = NumberDomain())), + targetStatement = "return true;", + ) + + val result = fixture.search(modelIds = emptySet()) + + val inputs = assertNotNull(result.inputs, result.toString()) + val value = assertIs(inputs.single()).toDouble() + assertEquals(42.0, value) + fixture.assertReplayConfirmed(inputs) + } +} diff --git a/usvm-ts/UNKNOWN_CALL_MODELS.md b/usvm-ts/UNKNOWN_CALL_MODELS.md index a5938078ae..950a3d5af6 100644 --- a/usvm-ts/UNKNOWN_CALL_MODELS.md +++ b/usvm-ts/UNKNOWN_CALL_MODELS.md @@ -110,7 +110,9 @@ Exhaustion after a runtime limitation does not establish that a source target is still requires original-source replay. named-property access, unsupported length growth, or assigning a runtime kind absent from a typed array's storage. Reads may return an element or `undefined`; subsequent numeric operations and typed writes preserve that runtime-kind -guard. TypeScript `as` and angle-bracket assertions are erased and never change a value or constrain its runtime kind. +guard. TypeScript `as` and angle-bracket assertions are erased only with `TsOptions(eraseTypeAssertions = true)` +and never change a value or constrain its runtime kind in that mode. The default retains the existing ETS cast +constraints and unsupported-cast behavior. The TypeScript Calls engine explicitly enables erasure. These events are separate from unknown-call model decisions. The Calls runner writes them synchronously and reports `RUNTIME_LIMITATION` when search exhausts after such a stop without reaching the target. An actual timeout remains `TIMEOUT`; a reached target still requires original-source replay. diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt index 43223856ff..7075187b1f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsOptions.kt @@ -27,6 +27,8 @@ data class TsOptions( val unknownCallFallback: TsResidualCallPolicy = TsResidualCallPolicy.STOP_PATH, /** Fixed experiment clock used by `Date.now()` and `new Date()`; `null` leaves those calls unsupported. */ val dateNowMilliseconds: Double? = null, + /** Erase TypeScript assertions; false retains the existing ETS cast constraints and unsupported casts. */ + val eraseTypeAssertions: Boolean = false, ) { init { val isValidDateNow = dateNowMilliseconds == null || 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 f2a9895d3b..4b5166e925 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 @@ -431,8 +431,12 @@ class TsExprResolver( ) } - // TypeScript assertions are erased; they neither convert nor constrain the runtime value. - override fun visit(expr: EtsCastExpr): UExpr<*>? = resolve(expr.arg) + override fun visit(expr: EtsCastExpr): UExpr<*>? { + val value = resolve(expr.arg) ?: return null + if (options.eraseTypeAssertions) return value + + return ctx.applyCastConstraints(scope = scope, value = value, type = expr.type) + } override fun visit(expr: EtsTypeOfExpr): UExpr? = with(ctx) { val arg = resolve(expr.arg) ?: return null diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TypeAssertions.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TypeAssertions.kt new file mode 100644 index 0000000000..a14e20257f --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TypeAssertions.kt @@ -0,0 +1,37 @@ +package org.usvm.machine.expr + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsRefType +import org.jacodb.ets.model.EtsType +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.machine.TsContext +import org.usvm.machine.interpreter.TsStepScope + +/** Retains the cast semantics used by ETS analysis unless assertion erasure is explicitly enabled. */ +internal fun TsContext.applyCastConstraints(scope: TsStepScope, value: UExpr<*>, type: EtsType): UExpr<*> { + if (value is UConcreteHeapRef && classConstructorSignature(value) != null) return value + + return when (value.sort) { + fp64Sort -> TODO("Not yet implemented https://github.com/UnitTestBot/usvm/issues/299") + boolSort -> TODO("Not yet implemented https://github.com/UnitTestBot/usvm/issues/299") + addressSort -> scope.calcOnState { + val instance = value.asExpr(addressSort) + if (instance.isFakeObject()) { + val fakeType = instance.getFakeType(scope) + pathConstraints += fakeType.refTypeExpr + val refValue = instance.extractRef(scope) + pathConstraints += memory.types.evalIsSubtype(refValue, type) + return@calcOnState instance + } + + if (type !is EtsRefType) { + TODO("Not supported yet https://github.com/UnitTestBot/usvm/issues/299") + } + + pathConstraints += memory.types.evalIsSubtype(instance, type) + instance + } + else -> error("Unsupported cast to $type from sort ${value.sort}") + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/TsTypeAssertionOptionsTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/TsTypeAssertionOptionsTest.kt new file mode 100644 index 0000000000..f14e204154 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/TsTypeAssertionOptionsTest.kt @@ -0,0 +1,71 @@ +package org.usvm.machine + +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.StateCollectionStrategy +import org.usvm.api.TsTestValue +import org.usvm.test.util.checkers.noResultsExpected +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.getResourcePath + +open class TsTypeAssertionOptionsTestBase : TsMethodTestRunner() { + override val scene = EtsScene( + listOf( + loadEtsFileAutoConvert( + getResourcePath("/models/TypeAssertionOptions.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ), + ), + ) + + init { + options = options.copy( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + throwExceptionOnStepFailure = true, + ) + } +} + +class TsTypeAssertionDefaultTest : TsTypeAssertionOptionsTestBase() { + @Test + fun `default casts reject an incompatible allocated reference type`() { + checkMatches( + method = getMethod(methodName = "incompatibleReference", className = "TypeAssertionOptions"), + analysisResultNumberMatches = noResultsExpected, + ) + } +} + +class TsTypeAssertionErasureTest : TsTypeAssertionOptionsTestBase() { + override val tsOptions = TsOptions(eraseTypeAssertions = true) + + @Test + fun `erased assertions preserve the original reference despite incompatible annotation`() { + discoverProperties( + method = getMethod(methodName = "incompatibleReference", className = "TypeAssertionOptions"), + { result -> result.number == 7.0 }, + invariants = arrayOf({ result -> result.number == 7.0 }), + ) + } + + @Test + fun `erased as assertions preserve numeric runtime values`() { + discoverProperties( + method = getMethod(methodName = "numericAssertion", className = "TypeAssertionOptions"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } + + @Test + fun `erased angle bracket assertions preserve boolean runtime values`() { + discoverProperties( + method = getMethod(methodName = "booleanAssertion", className = "TypeAssertionOptions"), + { result -> result.value }, + invariants = arrayOf({ result -> result.value }), + ) + } +} 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 8bf30815be..867e20712a 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 @@ -43,7 +43,7 @@ class TsArrayShiftReplayTest { val tests = TsMachine( scene = scene, options = machineOptions, - tsOptions = TsOptions(), + tsOptions = TsOptions(eraseTypeAssertions = true), unknownCallDispatcher = dispatcher, ).use { machine -> machine.analyze(listOf(method)).map { state -> TsTestResolver().resolve(method, state) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt index 6608fb1aef..196bb728a0 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt @@ -108,7 +108,7 @@ class TsErrorEtsIrModelTest { val states = TsMachine( scene = scene, options = machineOptions, - tsOptions = TsOptions(), + tsOptions = TsOptions(eraseTypeAssertions = true), observer = observer, ).use { machine -> machine.analyze(listOf(method)) } val values = states.map { state -> TsTestResolver().resolve(method, state).returnValue } diff --git a/usvm-ts/src/test/resources/models/TypeAssertionOptions.ts b/usvm-ts/src/test/resources/models/TypeAssertionOptions.ts new file mode 100644 index 0000000000..940d883f11 --- /dev/null +++ b/usvm-ts/src/test/resources/models/TypeAssertionOptions.ts @@ -0,0 +1,27 @@ +class OriginalAssertionValue { + original: number = 1; +} + +class OtherAssertionValue { + other: number = 2; +} + +export class TypeAssertionOptions { + static incompatibleReference(): number { + const value = new OriginalAssertionValue(); + const asserted = value as OtherAssertionValue; + return asserted ? 7 : 8; + } + + static numericAssertion(): boolean { + const value = 42; + const asserted = value as unknown as string; + return typeof asserted === "number" && asserted === 42; + } + + static booleanAssertion(): boolean { + const value = true; + const asserted = value; + return typeof asserted === "boolean" && asserted === true; + } +}