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 668bbd0388..950a3d5af6 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,19 @@ 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 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. 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/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/call/intrinsic/TsArrayEtsIrModelFamily.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayEtsIrModelFamily.kt index cfe30da81a..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 @@ -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(arrayType) + 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..ea1b1d6896 --- /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 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 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.machine.expr.builtInErrorSignature +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..cbddae1432 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ErrorModelStorage.kt @@ -0,0 +1,163 @@ +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.EtsFieldSignature +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 +import org.usvm.machine.interpreter.TsStepScope +import org.usvm.types.singleOrNull +import org.usvm.util.boxArrayValue + +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" + +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 + } +} + +/** Only unresolved SDK Error fields need the unqualified declaration lookup. */ +internal fun EtsFieldSignature.runtimeFieldSignature(): EtsFieldSignature = + if (isUnresolvedErrorField()) copy(enclosingClass = EtsClassSignature.UNKNOWN) else this + +private fun TsContext.resolveErrorStorageField( + scope: TsStepScope, + instance: UHeapRef, + field: EtsFieldSignature, +): ErrorStorageField? { + val definitionStorageField = field.errorModelDefinitionStorageField().takeIf { + applicationAndSdkClasses.none { owner -> owner.signature == field.enclosingClass } && + TsErrorEtsIrModelFamily.ownsStorageDefinitionField(field) + } + 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)) + } +} + +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, + ) + memory.write(deletedFieldLValue(instance, field), falseExpr, guard = trueExpr) + writtenConcreteFields += instance to field.name + } + return true +} + +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/ReadField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/ReadField.kt index e7fd221fa9..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 @@ -148,6 +148,11 @@ private fun TsContext.resolveDeclaredField( val deleted = scope.calcOnState { memory.read(deletedFieldLValue(instance, field)) } if (deleted.isTrue) return mkUndefinedValue() + 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) val wasWritten = scope.calcOnState { (instance to field.name) in writtenConcreteFields } @@ -157,10 +162,9 @@ 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( + val storageSort = writtenSort ?: declaredLiteralSort ?: resolvedFieldSort( scope = scope, instance = instance, field = field, @@ -173,15 +177,20 @@ private fun TsContext.resolveDeclaredField( (resolvedField as? TsResolutionResult.Unique)?.property?.type } - if (!wasWritten) { + val requiresDeclaredPresence = !wasWritten + 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) + 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. @@ -336,7 +345,7 @@ private fun TsContext.readField( sort: USort, ): UExpr<*> { if (sort !is TsUnresolvedSort) { - val lValue = mkFieldLValue(sort, instance, field) + 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/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 8eff962178..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 @@ -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,50 +431,11 @@ 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 - } - } + override fun visit(expr: EtsCastExpr): UExpr<*>? { + val value = resolve(expr.arg) ?: return null + if (options.eraseTypeAssertions) return value - else -> { - error("Unsupported cast from ${expr.arg} to ${expr.type}") - } - } + return ctx.applyCastConstraints(scope = scope, value = value, type = expr.type) } override fun visit(expr: EtsTypeOfExpr): UExpr? = with(ctx) { @@ -1360,12 +1322,10 @@ class TsExprResolver( val callee = scope.calcOnState { associatedFunction[ptr] } if (callee == null) { - unknownCallDispatcher.dispatch( - scope = scope, - call = expr, - callSite = scope.calcOnState { lastStmt }, - failureReason = TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, - resolvedReceiver = ptr, + dispatchUnresolvedPointer( + expr = expr, + pointer = ptr, + fallbackReason = TsUnknownCallFailureReason.POINTER_TARGET_NOT_FOUND, ) return null } @@ -1380,24 +1340,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 { - unknownCallDispatcher.dispatch( - scope = scope, - call = expr, - callSite = scope.calcOnState { lastStmt }, - failureReason = TsUnknownCallFailureReason.NON_REFERENCE_POINTER, - resolvedReceiver = ptr, + dispatchUnresolvedPointer( + expr = expr, + pointer = ptr, + fallbackReason = TsUnknownCallFailureReason.NON_REFERENCE_POINTER, ) } @@ -1406,6 +1373,54 @@ 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 + } + + 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/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/main/kotlin/org/usvm/machine/expr/WriteField.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/WriteField.kt index 82f8d2d61c..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 @@ -200,6 +200,14 @@ fun TsContext.assignToInstanceField( return Unit } + val wroteModeledErrorField = writeModeledErrorField( + scope = scope, + instance = unwrappedInstance, + field = field, + value = expr, + ) + if (wroteModeledErrorField) return Unit + 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/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt index e6e1cdd8f3..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 @@ -71,7 +69,9 @@ import org.usvm.machine.expr.handleAssignToStaticField import org.usvm.machine.expr.handleDefineDataProperty 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.thrownValueType import org.usvm.machine.expr.tryApproximateInstanceCall import org.usvm.machine.expr.writeGlobal import org.usvm.machine.state.TsMethodResult @@ -727,13 +727,9 @@ class TsInterpreter( observer?.onThrowStatement(exprResolver.simpleValueResolver, stmt, scope) - val exception = exprResolver.resolve(stmt.exception) ?: return - val exceptionType: EtsType = when (exception.sort) { - ctx.addressSort -> EtsStringType // TODO: improve object type detection - ctx.fp64Sort -> EtsNumberType - ctx.boolSort -> EtsBooleanType - else -> EtsStringType - } + val resolvedException = exprResolver.resolve(stmt.exception) ?: return + val exception = ctx.normalizeThrownValue(scope, resolvedException) ?: return + val exceptionType = ctx.thrownValueType(scope, exception) scope.doWithState { methodResult = TsMethodResult.TsException(exception, exceptionType) 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/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/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..fbecd4baa9 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayConstructorEtsIrModelTest.kt @@ -0,0 +1,173 @@ +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 { + assertEquals(1, values.size, "Unknown call events: $events") + return 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..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) } @@ -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..196bb728a0 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorEtsIrModelTest.kt @@ -0,0 +1,159 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsClassType +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.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( + 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) + 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 -> + 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(eraseTypeAssertions = true), + 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..b0526612ab --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsErrorSourceSemanticsTest.kt @@ -0,0 +1,143 @@ +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 `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( + 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 `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( + 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/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/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..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 @@ -127,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/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..8baad3a7b0 --- /dev/null +++ b/usvm-ts/src/test/resources/models/ErrorEtsIr.ts @@ -0,0 +1,111 @@ +class ForeignFields { + name: number = 17; + message: boolean = true; +} + +export class ErrorEtsIr { + static 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"; + } + + static overwrittenReferenceKinds(): boolean { + const error: any = new Error("original"); + error.message = null; + error.name = undefined; + return error.message === null && error.name === undefined; + } + + static overwrittenObjectAlias(): boolean { + const error: any = new Error("original"); + const payload = { marker: 7 }; + error.message = payload; + 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"; + return error.message === message && typeof error.message === "string" && error.name === "Error"; + } + + static name(): string { + return new Error("expected message").name; + } + + static message(): string { + 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"); + } + + 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..a59a1beaa9 100644 --- a/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts +++ b/usvm-ts/src/test/resources/models/NumericBoundarySemantics.ts @@ -56,6 +56,13 @@ export class NumericBoundarySemantics { return alias[0] === null ? 2 : -1; } + typedArrayCannotStoreMissingValue(): number { + const source = [11]; + const destination = [22]; + destination[0] = source[2]; + return destination[0]; + } + bitwiseNaN(): number { return (0 / 0) >> 1; } 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/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; + } +} 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"; + } +}