diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt index 9a939c7e06..fa079747fe 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt @@ -8,6 +8,7 @@ import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsBooleanLiteralType import org.jacodb.ets.model.EtsBooleanType import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsEnumValueType import org.jacodb.ets.model.EtsGenericType import org.jacodb.ets.model.EtsLexicalEnvType @@ -91,6 +92,16 @@ class TsContext( // String constant caching at context level private val stringConstants: MutableMap = mutableMapOf() + private val classConstructorRefs: MutableMap = mutableMapOf() + private val constructorSignatures: MutableMap = mutableMapOf() + + fun classConstructorRef(signature: EtsClassSignature): UConcreteHeapRef = + classConstructorRefs.getOrPut(signature) { + allocateStaticRef().also { constructorSignatures[it] = signature } + } + + fun classConstructorSignature(ref: UConcreteHeapRef): EtsClassSignature? = constructorSignatures[ref] + /** * Reverse mapping from heap references to their original string constant values. * This is used during test resolution to retrieve the actual string content when diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt index ca75767d69..405ce95895 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsMachine.kt @@ -17,6 +17,7 @@ import org.usvm.machine.call.deduplicateEtsFilesBySignature import org.usvm.machine.interpreter.TsInterpreter import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.TsState +import org.usvm.machine.types.TsConstructorInputGuard import org.usvm.machine.types.TsTypeSystem import org.usvm.ps.createPathSelector import org.usvm.statistics.CompositeUMachineObserver @@ -80,13 +81,15 @@ class TsMachine( ) } ?: scene - private val graph = TsGraph(analysisScene) - private val typeSystem = TsTypeSystem(analysisScene, typeOperationsTimeout = 1.seconds, graph.hierarchy) + private val runtimeScene = analysisScene.withCoreRuntimeSdk() + private val graph = TsGraph(runtimeScene) + private val typeSystem = TsTypeSystem(runtimeScene, typeOperationsTimeout = 1.seconds, graph.hierarchy) private val components = TsComponents(typeSystem, options) private val ctx = TsContext( - scene = analysisScene, + scene = runtimeScene, components = components, - applicationAndSdkClasses = scene.projectAndSdkClasses, + // Model bodies are reachable only through their dispatcher and its domain guards. + applicationAndSdkClasses = scene.projectClasses + runtimeScene.sdkClasses, ) private val resolvedUnknownCallDispatcher = unknownCallDispatcher ?: TsModelUnknownCallDispatcher( models = requireNotNull(resolvedUnknownCallModels), @@ -113,12 +116,15 @@ class TsMachine( methods: List, targets: List = emptyList(), ): TsAnalysisResult { - val initialStates = mutableMapOf() - methods.forEach { initialStates[it] = interpreter.getInitialState(it, targets) } + val (initialStates, unsupportedPaths) = createInitialStates(methods, targets) + + if (initialStates.isEmpty()) { + return TsAnalysisResult(emptyList(), TsAnalysisStopReason.EXHAUSTED, unsupportedPaths.toList()) + } val methodsToTrackCoverage = when (options.coverageZone) { - CoverageZone.METHOD, CoverageZone.TRANSITIVE -> methods.toHashSet() + CoverageZone.METHOD, CoverageZone.TRANSITIVE -> initialStates.keys.toHashSet() CoverageZone.CLASS -> TODO("Unsupported yet") } @@ -157,8 +163,6 @@ class TsMachine( val observers = mutableListOf>(coverageStatistics) observers.add(statesCollector) - val unsupportedPaths = mutableSetOf() - if (tsOptions.enableVisualization) { observers += TsStateVisualizer() } @@ -196,7 +200,7 @@ class TsMachine( if (logger.isInfoEnabled) { observers.add( StatisticsByMethodPrinter( - getMethods = { methods }, + getMethods = { initialStates.keys.toList() }, print = logger::info, getMethodSignature = { it.humanReadableSignature }, coverageStatistics = coverageStatistics, @@ -242,6 +246,26 @@ class TsMachine( ) } + private fun createInitialStates( + methods: List, + targets: List, + ): Pair, MutableSet> { + val initialStates = mutableMapOf() + val unsupportedPaths = mutableSetOf() + val constructorInputs = TsConstructorInputGuard() + + methods.forEach { method -> + val unsupportedReason = constructorInputs.unsupportedReason(method) + if (unsupportedReason != null) { + unsupportedPaths += unsupportedReason + } else { + initialStates[method] = interpreter.getInitialState(method, targets) + } + } + + return initialStates to unsupportedPaths + } + override fun close() { components.close() } diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt new file mode 100644 index 0000000000..9a6d36d630 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeError.kt @@ -0,0 +1,17 @@ +package org.usvm.machine + +import org.jacodb.ets.model.EtsClassSignature +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFileSignature + +private val runtimeFile = EtsFileSignature( + projectName = "usvm.ts.runtime", + fileName = "TypeError", +) +private val typeErrorSignature = EtsClassSignature( + name = "TypeError", + file = runtimeFile, +) + +/** Type identity of terminal JavaScript TypeError exceptions produced by the interpreter. */ +internal val TS_TYPE_ERROR_TYPE = EtsClassType(typeErrorSignature) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt new file mode 100644 index 0000000000..966ce27b7d --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/TsRuntimeSdk.kt @@ -0,0 +1,65 @@ +package org.usvm.machine + +import org.jacodb.ets.dto.EtsFileDto +import org.jacodb.ets.dto.toEtsFile +import org.jacodb.ets.model.EtsClass +import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsLocal +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.etsIrSerializerScript +import org.jacodb.ets.utils.generateEtsIR +import org.usvm.util.EtsHierarchy +import kotlin.io.path.deleteIfExists +import kotlin.io.path.inputStream + +private val coreRuntimeClassNames = setOf("Object", "Function", "Array") + +// JacoDB ships the matching TypeScript lib*.d.ts next to its frontend. Single-file conversion supports +// declarations, while project mode deliberately skips them. Cache the DTO, not mutable scene-owned classes. +private val coreRuntimeSdk: EtsFileDto by lazy { + val library = etsIrSerializerScript(EtsIrProvider.TS_FRONTEND).resolveSibling("lib.es5.d.ts") + val ir = generateEtsIR(library, loadEntrypoints = false, provider = EtsIrProvider.TS_FRONTEND) + try { + val file = ir.inputStream().use { EtsFileDto.loadFromJson(it) } + file.copy( + classes = file.classes.filter { it.signature.name in coreRuntimeClassNames }, + namespaces = emptyList(), + ) + } finally { + ir.deleteIfExists() + } +} + +/** Standard Function and Array declarations use dedicated values, not ordinary class-instance witnesses. */ +internal fun EtsClassType.isCoreRuntimePrototypeIdentity(): Boolean = + signature.file == EtsHierarchy.OBJECT_CLASS.signature.file && + signature.name in setOf("Function", "Array") + +/** + * Load Object, Function and Array from the standard declarations bundled in the pinned JacoDB dependency. + * Keep their signatures and members and preserve SDK declarations supplied by the caller. Declaration files + * describe prototypes and APIs; executing an SDK API still requires an interpreter implementation or model. + */ +internal fun EtsScene.withCoreRuntimeSdk(): EtsScene { + val missingNames = coreRuntimeClassNames - sdkClasses.map { it.name }.toSet() + if (missingNames.isEmpty()) return this + + val library = coreRuntimeSdk.toEtsFile() + val classes = library.classes.filter { it.name in missingNames } + check(classes.map { it.name }.toSet() == missingNames) { "Core TypeScript SDK declarations are missing" } + val file = EtsFile(signature = library.signature, classes = classes, namespaces = emptyList()) + + return EtsScene(projectFiles = projectFiles, sdkFiles = sdkFiles + file, projectName = projectName) +} + +/** An undeclared frontend local denotes a standard-library constructor, rather than a project binding. */ +internal fun EtsScene.sdkConstructorForGlobal(local: EtsLocal): EtsClass? = + sdkClasses.singleOrNull { it.name == local.name } + +internal fun EtsScene.runtimeFunctionType(): EtsClassType { + val functionClass = sdkClasses.singleOrNull { it.name == "Function" } + ?: throw UnsupportedOperationException("SDK Function identity is ambiguous or unavailable") + return EtsClassType(functionClass.signature) +} 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 bb6aa77b95..5eb05dfa69 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 @@ -6,6 +6,7 @@ import org.jacodb.ets.model.EtsArrayType import org.jacodb.ets.model.EtsClassType import org.jacodb.ets.model.EtsField import org.jacodb.ets.model.EtsFieldSignature +import org.jacodb.ets.model.EtsGenericType import org.jacodb.ets.model.EtsInstanceFieldRef import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsNullType @@ -36,6 +37,7 @@ import org.usvm.machine.types.TsUnresolvedValue import org.usvm.machine.types.iteUnresolvedValue import org.usvm.machine.types.iteWriteIntoFakeObject import org.usvm.machine.types.mkFakeValue +import org.usvm.machine.types.requiresConstructorWitness import org.usvm.machine.types.toAuxiliaryType import org.usvm.util.EtsHierarchy import org.usvm.util.TsResolutionResult @@ -225,6 +227,20 @@ private fun TsContext.prepareInitialInputField( activeInitial: UBoolExpr, hierarchy: EtsHierarchy, ): TsUnresolvedValue? { + // A write, deletion or absent property can make the declared initial value irrelevant. + // Do not reject the entire input object just because another field needs a constructor witness. + val unsupportedInitial = when { + declaration?.type?.requiresConstructorWitness() == true -> "Constructor-typed input field" + declaration?.type is EtsGenericType -> "Unresolved generic input field" + else -> null + } + if (unsupportedInitial != null) { + scope.fork(mkNot(activeInitial), blockOnFalseState = { + terminateAsUnsupported(reason = "$unsupportedInitial is not modeled") + }) ?: return null + return value + } + val optional = declaration?.optional == true val sort = declaration?.let { typeToSort(it.type) } ?: unresolvedSort val expectedKind = when (sort) { 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 f0e08bd301..894acb3c6a 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 @@ -21,6 +21,7 @@ import org.jacodb.ets.model.EtsCaughtExceptionRef import org.jacodb.ets.model.EtsClassCategory import org.jacodb.ets.model.EtsClassSignature import org.jacodb.ets.model.EtsClassType +import org.jacodb.ets.model.EtsClassValueRef import org.jacodb.ets.model.EtsClosureFieldRef import org.jacodb.ets.model.EtsConstant import org.jacodb.ets.model.EtsDeleteExpr @@ -92,6 +93,7 @@ import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.NAMED_FUNCTION_REFERENCE_PREFIX import org.jacodb.ets.utils.getDeclaredLocals +import org.usvm.UBoolExpr import org.usvm.UConcreteHeapRef import org.usvm.UExpr import org.usvm.UHeapRef @@ -101,10 +103,12 @@ import org.usvm.api.allocateConcreteRef import org.usvm.api.evalTypeEquals import org.usvm.api.initializeArrayLength import org.usvm.api.memcpy +import org.usvm.api.typeStreamOf import org.usvm.dataflow.ts.infer.tryGetKnownType import org.usvm.dataflow.ts.util.type import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isTrue +import org.usvm.machine.TS_TYPE_ERROR_TYPE import org.usvm.machine.TsConcreteMethodCallStmt import org.usvm.machine.TsContext import org.usvm.machine.TsOptions @@ -120,6 +124,8 @@ import org.usvm.machine.interpreter.markResolved import org.usvm.machine.interpreter.setResolvedValue import org.usvm.machine.operator.TsBinaryOperator import org.usvm.machine.operator.TsUnaryOperator +import org.usvm.machine.runtimeFunctionType +import org.usvm.machine.sdkConstructorForGlobal import org.usvm.machine.state.TsMethodResult import org.usvm.machine.state.lastStmt import org.usvm.machine.state.localsCount @@ -234,6 +240,8 @@ class TsExprResolver( return simpleValueResolver.visit(value) } + override fun visit(value: EtsClassValueRef): UExpr = ctx.classConstructorRef(value.signature) + override fun visit(value: EtsParameterRef): UExpr? { return simpleValueResolver.visit(value) } @@ -396,6 +404,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}") @@ -474,6 +487,9 @@ class TsExprResolver( } val functionValue = mkStringConstant("function", scope) + val isClassConstructor = ref is UConcreteHeapRef && classConstructorSignature(ref) != null + if (isClassConstructor) return functionValue + val isKnownFunction = scope.calcOnState { ref is UConcreteHeapRef && ( associatedFunction[ref] != null || @@ -1151,12 +1167,146 @@ class TsExprResolver( } override fun visit(expr: EtsInstanceOfExpr): UExpr? = with(ctx) { - val arg = resolve(expr.arg)?.asExpr(addressSort) ?: return null - val checkType = expr.checkType as? EtsRefType ?: return falseExpr + val arg = resolve(expr.arg) ?: return null + val checkValue = expr.checkValue - scope.calcOnState { - memory.types.evalIsSubtype(arg, EtsNominalType(checkType)) + val checkType = if (checkValue == null) { + // Legacy EtsIR contains only a static target. New frontend IR always evaluates the RHS. + expr.checkType as? EtsRefType + ?: return falseExpr + } else { + resolveRuntimeConstructor(checkValue, operation = RuntimeConstructorOperation.INSTANCEOF) ?: return null } + + if (arg.sort != addressSort || arg == mkUndefinedValue() || arg == mkTsNullValue()) return falseExpr + if (arg.isFakeObject()) { + val fakeType = arg.getFakeType(scope) + val refValue = arg.extractRef(scope) + val isInstance = referenceInstanceof(refValue, checkType) + + return mkAnd(fakeType.refTypeExpr, isInstance) + } + + referenceInstanceof(arg.asExpr(addressSort), checkType) + } + + private fun referenceInstanceof(ref: UHeapRef, checkType: EtsRefType): UBoolExpr = with(ctx) { + if (ref == mkUndefinedValue() || ref == mkTsNullValue()) return falseExpr + if (ref is UIteExpr<*>) { + val trueValue = referenceInstanceof(ref.trueBranch.asExpr(addressSort), checkType) + val falseValue = referenceInstanceof(ref.falseBranch.asExpr(addressSort), checkType) + return mkIte(ref.condition, trueValue, falseValue) + } + + // Wrappers and conditional values retain the represented function's identity. + val isFunctionObject = ref is UConcreteHeapRef && ( + classConstructorSignature(ref) != null || scope.calcOnState { associatedFunction[ref] != null } + ) + if (isFunctionObject) return runtimeInstanceof(scene.runtimeFunctionType(), checkType) + + if (isAllocatedConcreteHeapRef(ref) && checkType is EtsClassType) { + // allocConcrete records one runtime type, even when the frontend local has a union type. + // The stream utility keeps absent, ambiguous or timed-out identities unresolved instead of choosing one. + val objectType = scope.calcOnState { memory.typeStreamOf(ref).singleOrNull() } as? EtsClassType + if (objectType != null) return runtimeInstanceof(objectType, checkType) + } + + val isInstance = scope.calcOnState { memory.types.evalIsSubtype(ref, EtsNominalType(checkType)) } + mkAnd(mkNotNullOrUndefined(ref), isInstance) + } + + private fun runtimeInstanceof(objectType: EtsRefType, checkType: EtsRefType): UBoolExpr = with(ctx) { + val objectClass = hierarchy.classesForType(objectType).singleOrNull() + ?: throw UnsupportedOperationException("Unknown instanceof receiver class: $objectType") + val constructorClass = hierarchy.classesForType(checkType).singleOrNull() + ?: throw UnsupportedOperationException("Unknown instanceof constructor class: $checkType") + mkBool(constructorClass in hierarchy.getAncestors(objectClass)) + } + + /** + * Resolve the evaluated identity once. `instanceof` can invoke a custom Symbol.hasInstance on its RHS, + * whereas `new` requires [[Construct]]; an ordinary object with that symbol is still not constructable. + */ + private fun resolveRuntimeConstructor( + value: EtsEntity, + operation: RuntimeConstructorOperation, + ): EtsClassType? = with(ctx) { + val constructor = resolve(value) ?: return null + if (constructor.sort == fp64Sort || constructor.sort == boolSort) return throwTypeError() + if (constructor == mkTsNullValue() || constructor == mkUndefinedValue()) return throwTypeError() + + if (constructor.sort != addressSort || constructor.isFakeObject()) { + val target = if (operation == RuntimeConstructorOperation.INSTANCEOF) { + "instanceof RHS" + } else { + "new constructor" + } + throw UnsupportedOperationException("Unresolved $target callability is not modeled") + } + + val constructorRef = constructor as? UConcreteHeapRef + ?: throw UnsupportedOperationException("Symbolic ${operation.operator} constructor identity is not modeled") + if (getStringConstantValue(constructorRef) != null) return throwTypeError() + + val signature = classConstructorSignature(constructorRef) + ?: return rejectNonConstructorValue(constructorRef, operation) + val clazz = hierarchy.classesForType(EtsClassType(signature)).singleOrNull() + ?: throw UnsupportedOperationException("Unknown or ambiguous ${operation.operator} class: $signature") + val hasPotentialCustomHasInstance = hierarchy.getAncestors(clazz).any { ancestor -> + ancestor.methods.any { method -> + method.modifiers.isStatic && (method.name == "%computed" || method.name == "Symbol.hasInstance") + } || ancestor.fields.any { field -> + field.modifiers.isStatic && (field.name == "%computed" || field.name == "Symbol.hasInstance") + } + } + val hasUnsupportedInstanceOverride = operation == RuntimeConstructorOperation.INSTANCEOF && + hasPotentialCustomHasInstance + if (hasUnsupportedInstanceOverride) { + throw UnsupportedOperationException("Custom Symbol.hasInstance may override instanceof for $signature") + } + + EtsClassType(clazz.signature) + } + + private fun rejectNonConstructorValue( + ref: UConcreteHeapRef, + operation: RuntimeConstructorOperation, + ): Nothing? = with(ctx) { + val objectType = if (isAllocatedConcreteHeapRef(ref)) { + scope.calcOnState { memory.typeStreamOf(ref).singleOrNull() } + } else { + null + } + if (objectType == EtsStringType) return throwTypeError() + + val objectClass = (objectType as? EtsClassType)?.let { type -> + hierarchy.classesForType(type).singleOrNull() + } + if (objectClass != null) { + // Computed members may include Symbol.hasInstance, so their instances need a separate model. + val ordinaryObject = objectClass.category == EtsClassCategory.CLASS || + objectClass.category == EtsClassCategory.OBJECT + val hasComputedMember = hierarchy.getAncestors(objectClass).any { ancestor -> + ancestor.methods.any { it.name == "%computed" || it.name == "Symbol.hasInstance" } || + ancestor.fields.any { it.name == "%computed" || it.name == "Symbol.hasInstance" } + } + val isFunction = scope.calcOnState { associatedFunction[ref] != null } + + val mayHandleInstanceof = operation == RuntimeConstructorOperation.INSTANCEOF && hasComputedMember + val isKnownNonConstructor = ordinaryObject && !mayHandleInstanceof && !isFunction + if (isKnownNonConstructor) return throwTypeError() + } + + throw UnsupportedOperationException("Unknown ${operation.operator} constructor value: $ref") + } + + private fun throwTypeError(): Nothing? { + scope.doWithState { + val exception = memory.allocConcrete(TS_TYPE_ERROR_TYPE) + methodResult = TsMethodResult.TsException(exception, TS_TYPE_ERROR_TYPE) + } + + return null } // endregion @@ -1582,6 +1732,12 @@ class TsSimpleValueResolver( val currentMethod = scope.calcOnState { lastEnteredMethod } if (local !in currentMethod.getDeclaredLocals()) { + val isParameter = currentMethod.parameters.any { it.name == local.name } + if (!isParameter && local.type is EtsFunctionType) { + val sdkConstructor = ctx.scene.sdkConstructorForGlobal(local) + if (sdkConstructor != null) return ctx.classConstructorRef(sdkConstructor.signature) + } + if (local.type is EtsFunctionType) { // TODO: function pointers should be "singletons" return scope.calcOnState { memory.allocConcrete(local.type) } @@ -1599,6 +1755,8 @@ class TsSimpleValueResolver( return resolveLocal(value) } + override fun visit(value: EtsClassValueRef): UExpr = ctx.classConstructorRef(value.signature) + override fun visit(value: EtsConstant): UExpr = with(ctx) { logger.warn { "visit(${value::class.simpleName}) is not implemented yet" } error("Not supported $value") @@ -1648,3 +1806,9 @@ class TsSimpleValueResolver( error("Should not be called") } } + +/** The RHS protocols differ: instanceof uses @@hasInstance, while new requires [[Construct]]. */ +private enum class RuntimeConstructorOperation(val operator: String) { + INSTANCEOF(operator = "instanceof"), + NEW(operator = "new"), +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsNominalType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsNominalType.kt index 22505c64b7..7d52ee868f 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsNominalType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/EtsNominalType.kt @@ -3,6 +3,11 @@ package org.usvm.machine.types import org.jacodb.ets.model.EtsRefType import org.jacodb.ets.model.EtsType +/** + * Runtime membership in the declared class hierarchy, rather than TypeScript structural assignability. + * For example, unrelated classes A and B can have identical fields but `new A() instanceof B` is false. + * This wrapper prevents field-shape constraints from being used as JavaScript prototype-chain checks. + */ internal data class EtsNominalType(val type: EtsRefType) : EtsType { override val typeName: String get() = "NominalType $type" diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsConstructorInputGuard.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsConstructorInputGuard.kt new file mode 100644 index 0000000000..0ee059c218 --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsConstructorInputGuard.kt @@ -0,0 +1,52 @@ +package org.usvm.machine.types + +import org.jacodb.ets.model.EtsAliasType +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsClassValueType +import org.jacodb.ets.model.EtsGenericType +import org.jacodb.ets.model.EtsIntersectionType +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsTupleType +import org.jacodb.ets.model.EtsType +import org.jacodb.ets.model.EtsUnionType +import org.usvm.util.humanReadableSignature + +/** + * Bounds inputs that themselves require a callable constructor witness, rather than an ordinary object. + * Instance inputs are structural field maps: neither their class declarations nor generic arguments imply + * that every declared field is used. Check those fields only when their initial values are actually read. + */ +internal class TsConstructorInputGuard { + fun unsupportedReason(method: EtsMethod): String? { + val genericParameters = method.typeParameters.filterIsInstance().associateBy { it.typeName } + val parameter = method.parameters.firstOrNull { + it.type.requiresConstructorWitness(genericParameters) + } ?: return null + + return "Constructor-typed parameter '${parameter.name}' in ${method.humanReadableSignature} is not modeled" + } +} + +/** Inspect the value's own type, without traversing instance declarations or their type arguments. */ +internal fun EtsType.requiresConstructorWitness( + genericParameters: Map = emptyMap(), + visitedGenerics: Set = emptySet(), +): Boolean = when (this) { + is EtsClassValueType -> true + is EtsUnionType -> types.any { it.requiresConstructorWitness(genericParameters, visitedGenerics) } + is EtsIntersectionType -> types.any { it.requiresConstructorWitness(genericParameters, visitedGenerics) } + is EtsTupleType -> types.any { it.requiresConstructorWitness(genericParameters, visitedGenerics) } + is EtsArrayType -> elementType.requiresConstructorWitness(genericParameters, visitedGenerics) + is EtsAliasType -> originalType.requiresConstructorWitness(genericParameters, visitedGenerics) + is EtsGenericType -> { + if (typeName in visitedGenerics) { + false + } else { + val declaration = genericParameters[typeName] + listOfNotNull(constraint, defaultType, declaration?.constraint, declaration?.defaultType).any { + it.requiresConstructorWitness(genericParameters, visitedGenerics + typeName) + } + } + } + else -> false +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt index b167374f86..e63b31039d 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/types/TsTypeSystem.kt @@ -25,6 +25,7 @@ import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnionType import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsVoidType +import org.usvm.machine.isCoreRuntimePrototypeIdentity import org.usvm.types.USupportTypeStream import org.usvm.types.UTypeStream import org.usvm.types.UTypeSystem @@ -271,7 +272,7 @@ class TsTypeSystem( is EtsArrayType -> isInstantiable(t.elementType) // array if elements instantiable is EtsTupleType -> t.types.all { isInstantiable(it) } // tuple if each element instantiable is EtsFunctionType -> true // function literals always possible - is EtsClassType -> true // class instantiation possible + is EtsClassType -> !t.isCoreRuntimePrototypeIdentity() else -> false } } diff --git a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt index 813957d1aa..4de206a4f2 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/util/EtsHierarchy.kt @@ -45,7 +45,7 @@ class EtsHierarchy(private val scene: EtsScene) { } result.takeIf { it.isNotEmpty() } - }.flatten().toMutableSet() + classesForType(OBJECT_CLASS) + }.flatten().toMutableSet() + scene.sdkClasses.filter { it.name == "Object" } } } @@ -118,11 +118,13 @@ class EtsHierarchy(private val scene: EtsScene) { } companion object { - // TODO use real one + private val objectFile = EtsFileSignature(projectName = "", fileName = "lib.es5.d.ts") + + // The Object declaration in the TypeScript library bundled by JacoDB. val OBJECT_CLASS = EtsClassType( signature = EtsClassSignature( name = "Object", - file = EtsFileSignature(projectName = "ES2015", fileName = "BuiltinClass") + file = objectFile ), ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt index af2cb291a0..7db0ac6cd7 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/types/TsTypeSystemTest.kt @@ -17,6 +17,8 @@ import org.jacodb.ets.model.EtsTupleType import org.jacodb.ets.model.EtsUndefinedType import org.jacodb.ets.model.EtsUnknownType import org.junit.jupiter.api.Test +import org.usvm.machine.withCoreRuntimeSdk +import org.usvm.types.TypesResult import org.usvm.util.EtsHierarchy import org.usvm.util.type import kotlin.test.assertFalse @@ -47,6 +49,48 @@ class TsTypeSystemTest { nonObjects.forEach { assertFalse(typeSystem.isSupertype(EtsObjectType, it), it.typeName) } } + @Test + fun `core SDK prototype identities are not ordinary object witnesses`() { + val scene = EtsScene(projectFiles = emptyList()).withCoreRuntimeSdk() + val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, hierarchy = EtsHierarchy(scene)) + val prototypes = scene.sdkClasses.filter { it.name == "Function" || it.name == "Array" } + + assertTrue(typeSystem.isInstantiable(EtsHierarchy.OBJECT_CLASS)) + prototypes.forEach { assertFalse(typeSystem.isInstantiable(it.type), it.name) } + val result = typeSystem.topTypeStream().take(n = 20) as TypesResult.SuccessfulTypesResult + prototypes.forEach { assertFalse(it.type in result.types, it.name) } + } + + @Test + fun `core SDK uses bundled TypeScript declarations with their members`() { + val scene = EtsScene(projectFiles = emptyList()).withCoreRuntimeSdk() + val objectClass = scene.sdkClasses.single { it.name == "Object" } + val functionClass = scene.sdkClasses.single { it.name == "Function" } + val arrayClass = scene.sdkClasses.single { it.name == "Array" } + + assertTrue(objectClass.signature == EtsHierarchy.OBJECT_CLASS.signature) + assertTrue(objectClass.methods.any { it.name == "hasOwnProperty" }) + assertTrue(functionClass.methods.any { it.name == "apply" }) + assertTrue(arrayClass.methods.any { it.name == "slice" }) + assertTrue(scene.sdkClasses.all { it.signature.file.fileName == "lib.es5.d.ts" }) + } + + @Test + fun `core SDK bootstrap preserves explicitly loaded SDK declarations`() { + val fileSignature = EtsFileSignature(projectName = "sdk", fileName = "function.ts") + val functionClass = EtsClassImpl( + signature = EtsClassSignature(name = "Function", file = fileSignature), + fields = emptyList(), + methods = emptyList(), + ) + val file = EtsFile(signature = fileSignature, classes = listOf(functionClass), namespaces = emptyList()) + val scene = EtsScene(projectFiles = emptyList(), sdkFiles = listOf(file)).withCoreRuntimeSdk() + val typeSystem = TsTypeSystem(scene, typeOperationsTimeout = 1.seconds, hierarchy = EtsHierarchy(scene)) + + assertTrue(scene.sdkClasses.single { it.name == "Function" } === functionClass) + assertTrue(typeSystem.isInstantiable(functionClass.type)) + } + @Test fun `auxiliary type is a subtype of a class containing its properties`() { val fileSignature = EtsFileSignature(projectName = "test", fileName = "types.ts") diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeBuiltinInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeBuiltinInstanceofTest.kt new file mode 100644 index 0000000000..41f3c26fc4 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeBuiltinInstanceofTest.kt @@ -0,0 +1,104 @@ +package org.usvm.samples.types + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText + +class RuntimeBuiltinInstanceofTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val tsPath = "/samples/types/RuntimeBuiltinInstanceof.ts" + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `core SDK prototype identities match JavaScript membership`() { + val expected = mapOf( + "constructorObject" to 1.0, + "constructorFunction" to 1.0, + "constructorArray" to 0.0, + "sdkConstructorFunction" to 1.0, + "sdkConstructorObject" to 1.0, + "sdkConstructorArray" to 0.0, + "functionObject" to 1.0, + "functionFunction" to 1.0, + "functionProjectClass" to 0.0, + "boxedConstructorFunction" to 1.0, + "boxedFunctionFunction" to 1.0, + "instanceObject" to 1.0, + "instanceFunction" to 0.0, + "arrayObject" to 1.0, + "arrayArray" to 1.0, + "primitiveObject" to 0.0, + "nullObject" to 0.0, + "stringObject" to 0.0, + "localShadow" to 0.0, + "callParameterShadow" to 0.0, + ) + + expected.forEach { (methodName, result) -> + discoverProperties( + method = getMethod(methodName = methodName, className = "RuntimeBuiltinInstanceof"), + { value -> value.number == result }, + invariants = arrayOf({ value -> value.number == result }), + ) + } + + replay(expected.map { (methodName, result) -> + "if (new RuntimeBuiltinInstanceof().$methodName() !== ${result.toInt()}) throw Error('$methodName');" + }) + } + + @Test + fun `conditional SDK constructor preserves both selected identities`() { + discoverProperties( + method = getMethod(methodName = "conditionalBuiltin", className = "RuntimeBuiltinInstanceof"), + { input, result -> input.value && result.number == 1.0 }, + { input, result -> !input.value && result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 1.0 }), + ) + + replay(listOf( + "if (new RuntimeBuiltinInstanceof().conditionalBuiltin(true) !== 1) throw Error('Function alias');", + "if (new RuntimeBuiltinInstanceof().conditionalBuiltin(false) !== 1) throw Error('Object alias');" + )) + } + + @Test + fun `boxed conditional functions preserve runtime membership`() { + val methods = listOf("boxedConstructorChoice", "boxedFunctionChoice") + + methods.forEach { methodName -> + discoverProperties( + method = getMethod(methodName = methodName, className = "RuntimeBuiltinInstanceof"), + { input, result -> input.value && result.number == 1.0 }, + { input, result -> !input.value && result.number == 0.0 }, + invariants = arrayOf({ input, result -> result.number == if (input.value) 1.0 else 0.0 }), + ) + } + + replay(methods.flatMap { methodName -> + listOf( + "if (new RuntimeBuiltinInstanceof().$methodName(true) !== 1) throw Error('$methodName(true)');", + "if (new RuntimeBuiltinInstanceof().$methodName(false) !== 0) throw Error('$methodName(false)');", + ) + }) + } + + private fun replay(assertions: List) { + val source = getResourcePath(tsPath).readText() + "\n" + assertions.joinToString(separator = "\n") + + assertNodeReplay( + source = source, + directory = directory, + name = "runtime-builtin-instanceof", + timeoutMessage = "Core SDK Node replay timed out", + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt new file mode 100644 index 0000000000..f5f7639590 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeInstanceofTest.kt @@ -0,0 +1,658 @@ +package org.usvm.samples.types + +import org.jacodb.ets.model.EtsScene +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.isAllocatedConcreteHeapRef +import org.usvm.machine.TsAnalysisStopReason +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.state.TsMethodResult +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.TsTestResolver +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText +import kotlin.test.assertEquals +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration.Companion.seconds + +class RuntimeInstanceofTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val tsPath = "/samples/types/RuntimeInstanceof.ts" + + override val scene: EtsScene = loadScene(tsPath) + + @Test + fun `dynamic constructor value selects both outcomes`() { + val method = getMethod(methodName = "dynamicConstructor", className = "RuntimeInstanceof") + + discoverProperties( + method = method, + { input, result -> input.value && result.number == 1.0 }, + { input, result -> !input.value && result.number == 0.0 }, + invariants = arrayOf({ input, result -> result.number == (if (input.value) 1.0 else 0.0) }), + ) + + val outcome = analyze("dynamicConstructor") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + val cases = outcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + val input = assertIs(test.before.parameters.single()).value + val actual = assertIs(test.returnValue).number + assertEquals(if (input) 1.0 else 0.0, actual) + input to actual + } + assertEquals(setOf(false, true), cases.map { it.first }.toSet()) + + replay(cases.map { (input, actual) -> + "if (new RuntimeInstanceof().dynamicConstructor($input) !== ${actual.toInt()}) throw Error('dynamic $input');" + }) + } + + @Test + fun `returned class value keeps constructor identity`() { + val method = getMethod(methodName = "returnedConstructor", className = "RuntimeInstanceof") + + discoverConstant("returnedConstructor", expected = 1.0) + + val outcome = analyze("returnedConstructor") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + outcome.states.forEach { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + assertEquals(1.0, assertIs(test.returnValue).number) + } + + replay(listOf( + "if (new RuntimeInstanceof().returnedConstructor() !== 1) throw Error('returned constructor');" + )) + } + + @Test + fun `typeof recognizes constructor values stored in a local`() { + val method = getMethod(methodName = "aliasedClassTypeof", className = "RuntimeInstanceof") + + discoverProperties( + method = method, + { input, result -> input.value && result.number == 1.0 }, + { input, result -> !input.value && result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 1.0 }), + ) + + val outcome = analyze("aliasedClassTypeof") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + val inputs = outcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + assertEquals(1.0, assertIs(test.returnValue).number) + assertIs(test.before.parameters.single()).value + } + assertEquals(setOf(false, true), inputs.toSet()) + + replay(inputs.map { input -> + "if (new RuntimeInstanceof().aliasedClassTypeof($input) !== 1) throw Error('typeof $input');" + }) + } + + @Test + fun `direct and inherited checks use declared class identity`() { + val expected = mapOf( + "directConstructor" to 1.0, + "castConstructor" to 1.0, + "nonNullConstructor" to 1.0, + "anyConstructor" to 1.0, + "unknownConstructor" to 1.0, + "objectConstructor" to 1.0, + "unrelatedConstructor" to 0.0, + "classTypeof" to 1.0, + "primitiveLeft" to 0.0, + ) + + expected.forEach { (methodName, expectedResult) -> + val method = getMethod(methodName = methodName, className = "RuntimeInstanceof") + + discoverConstant(methodName, expected = expectedResult) + + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty(), "$methodName: ${outcome.unsupportedPaths}") + outcome.states.forEach { state -> + assertIs(state.methodResult, methodName) + val test = TsTestResolver().resolve(method, state) + assertEquals(expectedResult, assertIs(test.returnValue).number, methodName) + } + } + + replay(expected.map { (methodName, expectedResult) -> + "if (new RuntimeInstanceof().$methodName() !== ${expectedResult.toInt()}) throw Error('$methodName');" + }) + } + + @Test + fun `nullish left operands are not class instances`() { + val methods = listOf("undefinedLeft", "nullLeft") + + methods.forEach { methodName -> + val method = getMethod(methodName = methodName, className = "RuntimeInstanceof") + + discoverConstant(methodName, expected = 0.0) + + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty(), methodName) + outcome.states.forEach { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + assertEquals(0.0, assertIs(test.returnValue).number, methodName) + } + } + + replay(methods.map { methodName -> + "if (new RuntimeInstanceof().$methodName() !== 0) throw Error('$methodName');" + }) + } + + @Test + fun `any receiver can contain an instance of the checked class`() { + val method = getMethod(methodName = "anyLeft", className = "RuntimeInstanceof") + + discoverProperties( + method = method, + { _, result -> result.number == 0.0 }, + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 0.0 || result.number == 1.0 }), + ) + + val outcome = analyze("anyLeft") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + val cases = outcome.states.map { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + val input = test.before.parameters.single() + val actual = assertIs(test.returnValue).number + input to actual + } + assertEquals(setOf(0.0, 1.0), cases.map { it.second }.toSet(), "$cases") + + val generatedAssertions = cases.mapIndexed { index, (input, actual) -> + val argument = when (input) { + is TsTestValue.TsClass -> "new ${input.name}()" + is TsTestValue.TsBoolean -> input.value.toString() + is TsTestValue.TsNumber -> input.number.toString() + TsTestValue.TsNull -> "null" + TsTestValue.TsUndefined -> "undefined" + else -> error("Cannot replay generated instanceof input: $input") + } + + "if (new RuntimeInstanceof().anyLeft($argument) !== ${actual.toInt()}) " + + "throw Error('generated instanceof case $index');" + } + replay(generatedAssertions + listOf( + "if (new RuntimeInstanceof().anyLeft(new InstanceA()) !== 1) throw Error('A instance');", + "if (new RuntimeInstanceof().anyLeft(new InstanceB()) !== 0) throw Error('B instance');", + "if (new RuntimeInstanceof().anyLeft(42) !== 0) throw Error('primitive');", + )) + } + + @Test + fun `class constructor values are not instances of project classes`() { + val methods = listOf("constructorLeft", "constructorAliasLeft", "anyConstructorLeft") + + methods.forEach { methodName -> + val method = getMethod(methodName = methodName, className = "RuntimeInstanceof") + if (methodName == "constructorAliasLeft") { + discoverProperties( + method = method, + { input, result -> input.value && result.number == 0.0 }, + { input, result -> !input.value && result.number == 0.0 }, + invariants = arrayOf({ _, result -> result.number == 0.0 }), + ) + } else { + discoverConstant(methodName, expected = 0.0) + } + + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty(), methodName) + + val tests = outcome.states.map { state -> + assertIs(state.methodResult, methodName) + val test = TsTestResolver().resolve(method, state) + assertEquals(0.0, assertIs(test.returnValue).number, methodName) + test + } + + if (methodName == "constructorAliasLeft") { + val inputs = tests.map { test -> + assertIs(test.before.parameters.single()).value + } + assertEquals(setOf(false, true), inputs.toSet()) + } + } + + replay(listOf( + "if (new RuntimeInstanceof().constructorLeft() !== 0) throw Error('direct ctor LHS');", + "if (new RuntimeInstanceof().constructorAliasLeft(true) !== 0) throw Error('A ctor LHS');", + "if (new RuntimeInstanceof().constructorAliasLeft(false) !== 0) throw Error('B ctor LHS');", + "if (new RuntimeInstanceof().anyConstructorLeft() !== 0) throw Error('any ctor LHS');", + )) + } + + @Test + fun `subclass instance belongs to declared parent constructor`() { + val method = getMethod(methodName = "inheritedConstructor", className = "RuntimeInstanceof") + + discoverProperties( + method = method, + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 1.0 }), + ) + + val outcome = analyze("inheritedConstructor") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + outcome.states.forEach { state -> + assertIs(state.methodResult) + val test = TsTestResolver().resolve(method, state) + assertEquals(1.0, assertIs(test.returnValue).number) + } + + replay(listOf( + "if (new RuntimeInstanceof().inheritedConstructor(new InstanceChild()) !== 1) throw Error('parent');" + )) + } + + @Test + fun `non callable RHS throws a TypeError object`() { + val methods = listOf( + "nonCallableRight", + "booleanRight", + "stringRight", + "nullRight", + "undefinedRight", + "objectRight", + "classInstanceRight", + ) + + methods.forEach { methodName -> + val method = getMethod(methodName = methodName, className = "RuntimeInstanceof") + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.unsupportedPaths.isEmpty(), "$methodName: ${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty(), methodName) + outcome.states.forEach { state -> + val exception = assertIs(state.methodResult) + assertEquals("TypeError", exception.type.typeName) + assertTrue(isAllocatedConcreteHeapRef(exception.value)) + + val test = TsTestResolver().resolve(method, state) + val objectException = assertIs(test.returnValue) + assertEquals("TypeError", assertIs(objectException.value).name) + } + } + + replay(methods.map { methodName -> + "let caught$methodName = false; try { new RuntimeInstanceof().$methodName(); } " + + "catch (error) { caught$methodName = error instanceof TypeError; } " + + "if (!caught$methodName) throw Error('$methodName TypeError');" + }) + } + + @Test + fun `non callable RHS TypeError reaches the catch block`() { + discoverConstant(methodName = "caughtNonCallableRight", expected = 1.0) + + replay(listOf( + "if (new RuntimeInstanceof().caughtNonCallableRight() !== 1) throw Error('caught TypeError');" + )) + } + + @Test + fun `custom hasInstance is explicitly unsupported`() { + val custom = analyze("customHasInstance") + val inherited = analyze("inheritedHasInstance") + val customField = analyze(methodName = "customHasInstanceField") + val inheritedField = analyze(methodName = "inheritedHasInstanceField") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, custom.stopReason) + assertTrue(custom.states.isEmpty()) + assertTrue(custom.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${custom.unsupportedPaths}") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, inherited.stopReason) + assertTrue(inherited.states.isEmpty()) + assertTrue(inherited.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${inherited.unsupportedPaths}") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, customField.stopReason) + assertTrue(customField.states.isEmpty()) + assertTrue(customField.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${customField.unsupportedPaths}") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, inheritedField.stopReason) + assertTrue(inheritedField.states.isEmpty()) + assertTrue(inheritedField.unsupportedPaths.any { "Symbol.hasInstance" in it }, "${inheritedField.unsupportedPaths}") + + replay(listOf( + "if (new RuntimeInstanceof().customHasInstance() !== false) throw Error('custom hasInstance');", + "if (new RuntimeInstanceof().inheritedHasInstance(new InstanceHasInstanceChild()) !== false) " + + "throw Error('inherited hasInstance');", + "if (new RuntimeInstanceof().customHasInstanceField() !== false) " + + "throw Error('field hasInstance');", + "if (new RuntimeInstanceof().inheritedHasInstanceField(new InstanceHasInstanceFieldChild()) !== false) " + + "throw Error('inherited field hasInstance');", + )) + } + + @Test + fun `symbolic RHS stays explicitly unsupported until callability is modeled`() { + val outcome = analyze("unresolvedRight") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.unsupportedPaths.any { "Unresolved instanceof RHS callability" in it }, + "${outcome.unsupportedPaths}") + + replay(listOf( + "if (new RuntimeInstanceof().unresolvedRight(InstanceA) !== true) throw Error('callable RHS');", + "let threwTypeError = false; try { new RuntimeInstanceof().unresolvedRight(42); } " + + "catch (error) { threwTypeError = error instanceof TypeError; } " + + "if (!threwTypeError) throw Error('non-callable RHS');", + )) + } + + @Test + fun `unused constructor fields do not exclude structural input objects`() { + val methods = listOf( + "unreadConstructorField", + "unreadNestedConstructorField", + "unreadGenericConstructorField", + "unreadInheritedGenericConstructorField", + ) + + methods.forEach { methodName -> + discoverProperties( + method = getMethod(methodName = methodName, className = "RuntimeInstanceof"), + { _, result -> result.number == 1.0 }, + { _, result -> result.number == 0.0 }, + invariants = arrayOf({ input, result -> + val marker = input.properties["marker"] as? TsTestValue.TsNumber + result.number == if (marker?.number == 7.0) 1.0 else 0.0 + }), + ) + } + + replay(methods.flatMap { methodName -> + listOf( + "if (new RuntimeInstanceof().$methodName({ marker: 7 } as any) !== 1) throw Error('$methodName 7');", + "if (new RuntimeInstanceof().$methodName({ marker: 3 } as any) !== 0) throw Error('$methodName 3');", + ) + }) + } + + @Test + fun `writing a constructor field before reading it needs no callable input witness`() { + discoverProperties( + method = getMethod(methodName = "overwrittenConstructorField", className = "RuntimeInstanceof"), + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 1.0 }), + ) + + replay(listOf( + "if (new RuntimeInstanceof().overwrittenConstructorField({} as any) !== 1) throw Error('overwritten ctor');" + )) + } + + @Test + fun `unsupported field read preserves paths that do not read the constructor`() { + val method = getMethod(methodName = "conditionalConstructorField", className = "RuntimeInstanceof") + + discoverProperties( + method = method, + { _, read, result -> !read.value && result.number == 1.0 }, + { _, read, result -> !read.value && result.number == 0.0 }, + invariants = arrayOf({ input, read, result -> + val marker = input.properties["marker"] as? TsTestValue.TsNumber + val expected = if (marker?.number == 7.0) 1.0 else 0.0 + + read.value == false && result.number == expected + }), + ) + + val outcome = analyze("conditionalConstructorField") + + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed input field" in it }, + "${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + } + + @Test + fun `constructor typed input has an explicit unsupported outcome`() { + val outcome = analyze("constructorParameter") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + "${outcome.unsupportedPaths}") + + replay(listOf( + "if (new RuntimeInstanceof().constructorParameter(InstanceA) !== true) throw Error('A input');", + "if (new RuntimeInstanceof().constructorParameter(InstanceB) !== false) throw Error('B input');", + )) + } + + @Test + fun `constructor containing input types have explicit unsupported outcomes`() { + val methods = listOf( + "constructorUnionParameter", + "nullableConstructorParameter", + "constructorAliasParameter", + "constructorIntersectionParameter", + "genericConstructorParameter", + ) + + methods.forEach { methodName -> + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}") + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + "$methodName: ${outcome.unsupportedPaths}") + } + + replay(listOf( + "if (new RuntimeInstanceof().constructorUnionParameter(InstanceA) !== true) throw Error('union A');", + "if (new RuntimeInstanceof().constructorUnionParameter(InstanceB) !== true) throw Error('union B');", + "if (new RuntimeInstanceof().nullableConstructorParameter(null) !== true) throw Error('nullable null');", + "if (new RuntimeInstanceof().nullableConstructorParameter(InstanceA) !== true) throw Error('nullable A');", + "if (new RuntimeInstanceof().constructorAliasParameter(InstanceA) !== true) throw Error('alias');", + "if (new RuntimeInstanceof().constructorIntersectionParameter(InstanceA) !== true) throw Error('intersection');", + "if (new RuntimeInstanceof().genericConstructorParameter(InstanceA) !== true) throw Error('generic');", + )) + } + + @Test + fun `constructor arrays have an explicit unsupported outcome`() { + val methods = listOf("constructorArrayParameter", "constructorNestedArrayParameter") + + methods.forEach { methodName -> + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}") + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + "$methodName: ${outcome.unsupportedPaths}") + } + + replay(listOf( + "if (new RuntimeInstanceof().constructorArrayParameter([InstanceA]) !== true) throw Error('array');", + "if (new RuntimeInstanceof().constructorNestedArrayParameter([[InstanceA]]) !== true) " + + "throw Error('nested array');", + )) + } + + @Test + fun `constructor tuple has an explicit unsupported outcome`() { + val outcome = analyze("constructorTupleParameter") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty()) + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed parameter" in it }, + "${outcome.unsupportedPaths}") + + replay(listOf( + "if (new RuntimeInstanceof().constructorTupleParameter([InstanceA]) !== true) throw Error('tuple');" + )) + } + + @Test + fun `reading an unresolved generic field has an explicit unsupported outcome`() { + val outcome = analyze("constructorBoxParameter") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.states.isEmpty(), "${outcome.states}") + assertTrue(outcome.unsupportedPaths.any { "Unresolved generic input field" in it }, + "${outcome.unsupportedPaths}") + + replay(listOf( + "const box = new InstanceConstructorBox(); box.value = InstanceA; " + + "if (new RuntimeInstanceof().constructorBoxParameter(box) !== true) throw Error('box');", + )) + } + + @Test + fun `constructor values in object fields have explicit unsupported outcomes`() { + val methods = listOf( + "structuralConstructorParameter", + "recursiveConstructorParameter", + "inheritedConstructorParameter", + ) + + methods.forEach { methodName -> + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}") + assertTrue(outcome.unsupportedPaths.any { "Constructor-typed input field" in it }, + "$methodName: ${outcome.unsupportedPaths}") + } + + replay(listOf( + "if (new RuntimeInstanceof().structuralConstructorParameter({ ctor: InstanceA }) !== true) " + + "throw Error('structural');", + "const holder = new InstanceRecursiveHolder(); holder.ctor = InstanceA; " + + "if (new RuntimeInstanceof().recursiveConstructorParameter(holder) !== true) throw Error('recursive');", + "const inherited = new InstanceInheritedHolder(); inherited.ctor = InstanceA; " + + "if (new RuntimeInstanceof().inheritedConstructorParameter(inherited) !== true) throw Error('inherited');", + )) + } + + @Test + fun `reading inherited generic fields has explicit unsupported outcomes`() { + val methods = listOf("inheritedGenericConstructorParameter", "inheritedGenericNumberParameter") + + methods.forEach { methodName -> + val outcome = analyze(methodName) + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason, methodName) + assertTrue(outcome.states.isEmpty(), "$methodName: ${outcome.states}") + assertTrue(outcome.unsupportedPaths.any { "Unresolved generic input field" in it }, + "$methodName: ${outcome.unsupportedPaths}") + } + + replay(listOf( + "const holder = new InstanceInheritedGenericConstructor(); holder.ctor = InstanceA; " + + "if (new RuntimeInstanceof().inheritedGenericConstructorParameter(holder) !== true) " + + "throw Error('inherited generic');", + "const numberHolder = new InstanceInheritedGenericNumber(); numberHolder.ctor = 1; " + + "if (new RuntimeInstanceof().inheritedGenericNumberParameter(numberHolder) !== true) " + + "throw Error('inherited generic number');", + )) + } + + @Test + fun `concrete inherited number input is not excluded by the constructor guard`() { + val outcome = analyze("inheritedConcreteNumberParameter") + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.isEmpty(), "${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + + replay(listOf( + "const holder = new InstanceInheritedConcreteNumber(); holder.value = 1; " + + "if (new RuntimeInstanceof().inheritedConcreteNumberParameter(holder) !== true) " + + "throw Error('inherited concrete number');", + )) + } + + @Test + fun `unsupported constructor input does not hide another entrypoint`() { + val methods = listOf("constructorParameter", "directConstructor") + .map { getMethod(methodName = it, className = "RuntimeInstanceof") } + val outcome = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> + machine.analyzeWithOutcome(methods = methods) + } + + assertEquals(TsAnalysisStopReason.EXHAUSTED, outcome.stopReason) + assertTrue(outcome.unsupportedPaths.any { "constructorParameter" in it }, "${outcome.unsupportedPaths}") + assertTrue(outcome.states.isNotEmpty()) + outcome.states.forEach { state -> assertIs(state.methodResult) } + } + + private fun discoverConstant(methodName: String, expected: Double) { + discoverProperties( + method = getMethod(methodName = methodName, className = "RuntimeInstanceof"), + { result -> result.number == expected }, + invariants = arrayOf({ result -> result.number == expected }), + ) + } + + private fun analyze(methodName: String) = TsMachine(scene, options = machineOptions, tsOptions = TsOptions()).use { machine -> + machine.analyzeWithOutcome(methods = listOf(getMethod(methodName = methodName, className = "RuntimeInstanceof"))) + } + + private fun replay(assertions: List) { + val source = buildString { + appendLine(getResourcePath(tsPath).readText()) + assertions.forEach(::appendLine) + } + + assertNodeReplay( + source = source, + directory = directory, + name = "runtime-instanceof", + timeoutMessage = "Node replay timed out", + ) + } + + private val machineOptions = UMachineOptions( + stateCollectionStrategy = StateCollectionStrategy.ALL, + stopOnCoverage = 0, + timeout = 30.seconds, + ) +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeSdkInstanceofTest.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeSdkInstanceofTest.kt new file mode 100644 index 0000000000..e149afad44 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/types/RuntimeSdkInstanceofTest.kt @@ -0,0 +1,57 @@ +package org.usvm.samples.types + +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.junit.jupiter.api.io.TempDir +import org.usvm.api.TsTestValue +import org.usvm.util.TsMethodTestRunner +import org.usvm.util.assertNodeReplay +import org.usvm.util.getResourcePath +import java.nio.file.Path +import kotlin.io.path.readText + +class RuntimeSdkInstanceofTest : TsMethodTestRunner() { + @TempDir + lateinit var directory: Path + + private val tsPath = "/samples/types/RuntimeSdkInstanceof.ts" + private val sdkPath = "/samples/types/RuntimeSdkClasses.ts" + override val scene: EtsScene = EtsScene( + projectFiles = listOf(loadEtsFileAutoConvert(getResourcePath(tsPath))), + sdkFiles = listOf(loadEtsFileAutoConvert(getResourcePath(sdkPath))), + ) + + @Test + fun `explicit SDK classes retain constructor and inherited instance identities`() { + val expected = mapOf("constructorObject" to 1.0, "constructorFunction" to 1.0, "constructorParent" to 0.0) + + expected.forEach { (methodName, result) -> + discoverProperties( + method = getMethod(methodName = methodName, className = "RuntimeSdkInstanceof"), + { value -> value.number == result }, + invariants = arrayOf({ value -> value.number == result }), + ) + } + + discoverProperties( + method = getMethod(methodName = "inherited", className = "RuntimeSdkInstanceof"), + { _, result -> result.number == 1.0 }, + invariants = arrayOf({ _, result -> result.number == 1.0 }), + ) + + val sdkSource = getResourcePath(sdkPath).readText().replace("export class", "class") + val source = sdkSource + "\n" + getResourcePath(tsPath).readText().lineSequence() + .filterNot { it.startsWith("import ") }.joinToString(separator = "\n") + val assertions = expected.map { (methodName, result) -> + "if (new RuntimeSdkInstanceof().$methodName() !== ${result.toInt()}) throw Error('$methodName');" + } + "if (new RuntimeSdkInstanceof().inherited(new RuntimeSdkChild()) !== 1) throw Error('SDK inheritance');" + + assertNodeReplay( + source = source + "\n" + assertions.joinToString(separator = "\n"), + directory = directory, + name = "runtime-sdk-instanceof", + timeoutMessage = "Explicit SDK Node replay timed out", + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt index 3ddbe5bc3c..9dd242ac27 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt @@ -39,6 +39,7 @@ import org.usvm.collection.field.UFieldLValue import org.usvm.isAllocated import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isTrue +import org.usvm.machine.TS_TYPE_ERROR_TYPE import org.usvm.machine.TsContext import org.usvm.machine.expr.TrackedObjectProperty import org.usvm.machine.expr.TsUnresolvedSort @@ -149,6 +150,15 @@ class TsTestResolver { try { // Dispatch based on the exception type, similar to string const resolution when (res.type) { + TS_TYPE_ERROR_TYPE -> { + val concreteRef = evaluateInModel(res.value) as? UConcreteHeapRef + check(concreteRef != null && isAllocatedConcreteHeapRef(concreteRef)) + + TsTestValue.TsException.ObjectException( + TsTestValue.TsClass(name = "TypeError", properties = emptyMap()) + ) + } + is EtsStringType -> { val concreteRef = evaluateInModel(res.value) as? UConcreteHeapRef if (concreteRef != null && isAllocatedConcreteHeapRef(concreteRef)) { diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeBuiltinInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeBuiltinInstanceof.ts new file mode 100644 index 0000000000..bb45ee1ee7 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/RuntimeBuiltinInstanceof.ts @@ -0,0 +1,58 @@ +class BuiltinProjectClass {} + +class RuntimeBuiltinInstanceof { + constructorObject(): number { return BuiltinProjectClass instanceof Object ? 1 : 0; } + constructorFunction(): number { return BuiltinProjectClass instanceof Function ? 1 : 0; } + constructorArray(): number { return BuiltinProjectClass instanceof Array ? 1 : 0; } + sdkConstructorFunction(): number { return Array instanceof Function ? 1 : 0; } + sdkConstructorObject(): number { return Function instanceof Object ? 1 : 0; } + sdkConstructorArray(): number { return Object instanceof Array ? 1 : 0; } + functionObject(): number { const fn = () => 1; return fn instanceof Object ? 1 : 0; } + functionFunction(): number { const fn = () => 1; return fn instanceof Function ? 1 : 0; } + functionProjectClass(): number { const fn = () => 1; return fn instanceof BuiltinProjectClass ? 1 : 0; } + boxedConstructorFunction(): number { + const box: any = { value: BuiltinProjectClass }; + return box.value instanceof Function ? 1 : 0; + } + + boxedFunctionFunction(): number { + const box: any = { value: () => 1 }; + return box.value instanceof Function ? 1 : 0; + } + + instanceObject(): number { return new BuiltinProjectClass() instanceof Object ? 1 : 0; } + instanceFunction(): number { return new BuiltinProjectClass() instanceof Function ? 1 : 0; } + arrayObject(): number { return [] instanceof Object ? 1 : 0; } + arrayArray(): number { return [] instanceof Array ? 1 : 0; } + primitiveObject(): number { return 42 instanceof Object ? 1 : 0; } + nullObject(): number { return null instanceof Object ? 1 : 0; } + stringObject(): number { return "text" instanceof Object ? 1 : 0; } + + conditionalBuiltin(useFunction: boolean): number { + const ctor = useFunction ? Function : Object; + return BuiltinProjectClass instanceof ctor ? 1 : 0; + } + + boxedConstructorChoice(useFunction: boolean): number { + const box: any = { value: useFunction ? BuiltinProjectClass : 42 }; + return box.value instanceof Function ? 1 : 0; + } + + boxedFunctionChoice(useFunction: boolean): number { + const box: any = { value: useFunction ? (() => 1) : 42 }; + return box.value instanceof Function ? 1 : 0; + } + + localShadow(): number { + const Object = BuiltinProjectClass; + return BuiltinProjectClass instanceof Object ? 1 : 0; + } + + parameterShadow(Object: any): number { + return BuiltinProjectClass instanceof Object ? 1 : 0; + } + + callParameterShadow(): number { + return this.parameterShadow(BuiltinProjectClass); + } +} diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts new file mode 100644 index 0000000000..a701d1e5e0 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/RuntimeInstanceof.ts @@ -0,0 +1,285 @@ +// @ts-nocheck + +class RuntimeInstanceof { + dynamicConstructor(useA: boolean): number { + const ctor = useA ? InstanceA : InstanceB; + return new InstanceA() instanceof ctor ? 1 : 0; + } + + constructorValue(): typeof InstanceA { + return InstanceA; + } + + returnedConstructor(): number { + const ctor = this.constructorValue(); + return new InstanceA() instanceof ctor && typeof ctor === "function" ? 1 : 0; + } + + directConstructor(): number { + return new InstanceA() instanceof InstanceA ? 1 : 0; + } + + castConstructor(): number { + return new InstanceA() instanceof (InstanceA as typeof InstanceA) ? 1 : 0; + } + + nonNullConstructor(): number { + return new InstanceA() instanceof InstanceA! ? 1 : 0; + } + + anyConstructor(): number { + return new InstanceA() instanceof (InstanceA as any) ? 1 : 0; + } + + unknownConstructor(): number { + return new InstanceA() instanceof (InstanceA as unknown as typeof InstanceA) ? 1 : 0; + } + + objectConstructor(): number { + return new InstanceA() instanceof (InstanceA as object as typeof InstanceA) ? 1 : 0; + } + + inheritedConstructor(instance: InstanceChild): number { + return instance instanceof InstanceParent ? 1 : 0; + } + + unrelatedConstructor(): number { + return new InstanceA() instanceof InstanceB ? 1 : 0; + } + + classTypeof(): number { + return typeof InstanceA === "function" ? 1 : 0; + } + + aliasedClassTypeof(useA: boolean): number { + const ctor = useA ? InstanceA : InstanceB; + return typeof ctor === "function" ? 1 : 0; + } + + primitiveLeft(): number { + return 42 instanceof InstanceA ? 1 : 0; + } + + anyLeft(value: any): number { + return value instanceof InstanceA ? 1 : 0; + } + + constructorLeft(): number { + return InstanceA instanceof InstanceA ? 1 : 0; + } + + constructorAliasLeft(useA: boolean): number { + const ctor = useA ? InstanceA : InstanceB; + return ctor instanceof InstanceA ? 1 : 0; + } + + anyConstructorLeft(): number { + const value: any = InstanceA; + return value instanceof InstanceA ? 1 : 0; + } + + undefinedLeft(): number { + const value: any = undefined; + return value instanceof InstanceA ? 1 : 0; + } + + nullLeft(): number { + const value: any = null; + return value instanceof InstanceA ? 1 : 0; + } + + nonCallableRight(): boolean { + const ctor: any = 42; + return new InstanceA() instanceof ctor; + } + + caughtNonCallableRight(): number { + try { + const ctor: any = 42; + new InstanceA() instanceof ctor; + return 0; + } catch { + return 1; + } + } + + booleanRight(): boolean { + const ctor: any = true; + return new InstanceA() instanceof ctor; + } + + stringRight(): boolean { + const ctor: any = "not a constructor"; + return new InstanceA() instanceof ctor; + } + + nullRight(): boolean { + const ctor: any = null; + return new InstanceA() instanceof ctor; + } + + undefinedRight(): boolean { + const ctor: any = undefined; + return new InstanceA() instanceof ctor; + } + + objectRight(): boolean { + const ctor: any = {}; + return new InstanceA() instanceof ctor; + } + + classInstanceRight(): boolean { + const ctor: any = new InstanceB(); + return new InstanceA() instanceof ctor; + } + + unresolvedRight(ctor: any): boolean { + return new InstanceA() instanceof ctor; + } + + customHasInstance(): boolean { + return new InstanceCustom() instanceof InstanceCustom; + } + + inheritedHasInstance(instance: InstanceHasInstanceChild): boolean { + return instance instanceof InstanceHasInstanceChild; + } + + customHasInstanceField(): boolean { + return new InstanceCustomField() instanceof InstanceCustomField; + } + + inheritedHasInstanceField(instance: InstanceHasInstanceFieldChild): boolean { + return instance instanceof InstanceHasInstanceFieldChild; + } + + unreadConstructorField(holder: { marker: number; ctor: typeof InstanceA }): number { + return holder.marker === 7 ? 1 : 0; + } + + unreadNestedConstructorField(holder: { marker: number; nested: { ctor: typeof InstanceA } }): number { + return holder.marker === 7 ? 1 : 0; + } + + unreadGenericConstructorField(holder: InstancePayload): number { + return holder.marker === 7 ? 1 : 0; + } + + unreadInheritedGenericConstructorField(holder: InstanceInheritedPayload): number { + return holder.marker === 7 ? 1 : 0; + } + + overwrittenConstructorField(holder: { ctor: typeof InstanceA }): number { + holder.ctor = InstanceA; + return typeof holder.ctor === "function" ? 1 : 0; + } + + conditionalConstructorField(holder: { marker: number; ctor: typeof InstanceA }, read: boolean): number { + if (read) return typeof holder.ctor === "function" ? 1 : 0; + return holder.marker === 7 ? 1 : 0; + } + + constructorParameter(ctor: typeof InstanceA): boolean { + return new InstanceA() instanceof ctor; + } + + constructorUnionParameter(ctor: typeof InstanceA | typeof InstanceB): boolean { + return typeof ctor === "function"; + } + + nullableConstructorParameter(ctor: typeof InstanceA | null): boolean { + return ctor === null || typeof ctor === "function"; + } + + constructorAliasParameter(ctor: InstanceConstructorAlias): boolean { + return typeof ctor === "function"; + } + + constructorIntersectionParameter(ctor: typeof InstanceA & { marker?: number }): boolean { + return typeof ctor === "function"; + } + + genericConstructorParameter(ctor: T): boolean { + return typeof ctor === "function"; + } + + constructorTupleParameter(ctors: [typeof InstanceA]): boolean { + return new InstanceA() instanceof ctors[0]; + } + + constructorArrayParameter(ctors: (typeof InstanceA)[]): boolean { + return ctors.length === 1 && new InstanceA() instanceof ctors[0]; + } + + constructorNestedArrayParameter(ctors: (typeof InstanceA)[][]): boolean { + return new InstanceA() instanceof ctors[0][0]; + } + + constructorBoxParameter(box: InstanceConstructorBox): boolean { + return typeof box.value === "function"; + } + + structuralConstructorParameter(holder: { ctor: typeof InstanceA }): boolean { + return typeof holder.ctor === "function"; + } + + recursiveConstructorParameter(holder: InstanceRecursiveHolder): boolean { + return typeof holder.ctor === "function"; + } + + inheritedConstructorParameter(holder: InstanceInheritedHolder): boolean { + return typeof holder.ctor === "function"; + } + + inheritedGenericConstructorParameter(holder: InstanceInheritedGenericConstructor): boolean { + return typeof holder.ctor === "function"; + } + + inheritedGenericNumberParameter(holder: InstanceInheritedGenericNumber): boolean { + return typeof holder.ctor === "number"; + } + + inheritedConcreteNumberParameter(holder: InstanceInheritedConcreteNumber): boolean { + return holder.value === 1; + } +} + +type InstanceConstructorAlias = typeof InstanceA | typeof InstanceB; + +class InstanceA {} +class InstanceB {} +class InstanceConstructorBox { value!: T; } +class InstanceRecursiveHolder { + next?: InstanceRecursiveHolder; + ctor!: typeof InstanceA; +} +class InstanceConstructorBase { ctor!: typeof InstanceA; } +class InstanceInheritedHolder extends InstanceConstructorBase {} +class InstanceGenericConstructorBase { ctor!: T; } +class InstanceInheritedGenericConstructor extends InstanceGenericConstructorBase {} +class InstanceInheritedGenericNumber extends InstanceGenericConstructorBase {} +class InstanceConcreteNumberBase { value!: number; } +class InstanceInheritedConcreteNumber extends InstanceConcreteNumberBase {} +class InstanceParent {} +class InstanceChild extends InstanceParent { childMarker: number = 1; } +class InstanceCustom { + static [Symbol.hasInstance](_value: unknown): boolean { + return false; + } +} +class InstanceHasInstanceParent { + static [Symbol.hasInstance](_value: unknown): boolean { + return false; + } +} +class InstanceHasInstanceChild extends InstanceHasInstanceParent { hasInstanceChildMarker: number = 1; } +class InstanceCustomField { + static [Symbol.hasInstance] = (_value: unknown): boolean => false; +} +class InstanceHasInstanceFieldParent { + static [Symbol.hasInstance] = (_value: unknown): boolean => false; +} +class InstanceHasInstanceFieldChild extends InstanceHasInstanceFieldParent { hasInstanceFieldChildMarker: number = 1; } + +class InstancePayload { marker!: number; value!: T; } +class InstanceInheritedPayload extends InstancePayload {} diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeSdkClasses.ts b/usvm-ts/src/test/resources/samples/types/RuntimeSdkClasses.ts new file mode 100644 index 0000000000..48cb61d653 --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/RuntimeSdkClasses.ts @@ -0,0 +1,4 @@ +export class RuntimeSdkParent {} +export class RuntimeSdkChild extends RuntimeSdkParent { + sdkMarker: number = 1; +} diff --git a/usvm-ts/src/test/resources/samples/types/RuntimeSdkInstanceof.ts b/usvm-ts/src/test/resources/samples/types/RuntimeSdkInstanceof.ts new file mode 100644 index 0000000000..a013459edd --- /dev/null +++ b/usvm-ts/src/test/resources/samples/types/RuntimeSdkInstanceof.ts @@ -0,0 +1,8 @@ +import { RuntimeSdkParent, RuntimeSdkChild } from "./RuntimeSdkClasses"; + +class RuntimeSdkInstanceof { + constructorObject(): number { return RuntimeSdkChild instanceof Object ? 1 : 0; } + constructorFunction(): number { return RuntimeSdkChild instanceof Function ? 1 : 0; } + constructorParent(): number { return RuntimeSdkChild instanceof RuntimeSdkParent ? 1 : 0; } + inherited(value: RuntimeSdkChild): number { return value instanceof RuntimeSdkParent ? 1 : 0; } +}