diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt index 288fc23f13..436e5fad9e 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/TsBuiltinGlobalType.kt @@ -10,6 +10,10 @@ import org.jacodb.ets.model.EtsType import org.jacodb.ets.model.EtsUnclearRefType import org.jacodb.ets.model.EtsUnknownType import org.jacodb.ets.model.EtsValue +import org.usvm.UConcreteHeapRef +import org.usvm.UExpr +import org.usvm.machine.TsContext +import org.usvm.util.EtsHierarchy internal fun hasBuiltinGlobalOwner( owner: EtsValue, @@ -41,3 +45,10 @@ private fun EtsValue.isLegacyBuiltinGlobal( name == expectedName && type == EtsUnknownType && callee.enclosingClass == EtsClassSignature.UNKNOWN.copy(name = expectedName) + +internal fun TsContext.isBuiltinArrayConstructor(value: UExpr<*>): Boolean { + val reference = value as? UConcreteHeapRef ?: return false + val signature = classConstructorSignature(reference) ?: return false + + return signature.name == "Array" && signature.file == EtsHierarchy.OBJECT_CLASS.signature.file +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt new file mode 100644 index 0000000000..423774424d --- /dev/null +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/call/intrinsic/TsArrayIsArrayIntrinsicModel.kt @@ -0,0 +1,84 @@ +package org.usvm.machine.call.intrinsic + +import io.ksmt.utils.asExpr +import org.jacodb.ets.model.EtsArrayType +import org.jacodb.ets.model.EtsUnknownType +import org.usvm.UBoolExpr +import org.usvm.UExpr +import org.usvm.UHeapRef +import org.usvm.UIteExpr +import org.usvm.machine.call.TsUnknownCall +import org.usvm.machine.call.TsUnknownCallModelCompletion +import org.usvm.machine.call.TsUnknownCallModelExecution +import org.usvm.machine.call.TsUnknownCallModelSuccessor +import org.usvm.machine.call.TsUnknownCallTarget +import org.usvm.machine.call.isBuiltinArrayConstructor +import org.usvm.machine.state.TsState + +/** Exact `Array.isArray` semantics for the genuine global `Array` built-in. */ +internal object TsArrayIsArrayIntrinsicModel : TsBuiltInUnknownCallModel { + const val MODEL_ID: String = "ts.array.isArray" + + private val anyArrayType = EtsArrayType(elementType = EtsUnknownType, dimensions = 1) + + override val id: String = MODEL_ID + override val target = TsUnknownCallTarget( + methodName = "isArray", + ) + + override fun apply(state: TsState, call: TsUnknownCall): TsUnknownCallModelExecution? { + val owner = call.receiver?.resolved ?: return null + if (!state.ctx.isBuiltinArrayConstructor(owner)) { + return null + } + + if (call.arguments.isEmpty()) { + return state.normalExecution(state.ctx.falseExpr) + } + + val value = call.arguments.first().resolved ?: return null + val result = state.isArray(value) + + return state.normalExecution(result) + } + + private fun TsState.isArray(value: UExpr<*>): UBoolExpr = with(ctx) { + when { + value is UIteExpr<*> -> { + val trueResult = isArray(value.trueBranch) + val falseResult = isArray(value.falseBranch) + + mkIte(value.condition, trueResult, falseResult) + } + + value.isFakeObject() -> { + val fakeType = value.getFakeType(memory) + val reference = value.extractRef(memory) + + mkAnd( + fakeType.refTypeExpr, + isNonNullArrayReference(reference), + ) + } + + value.sort == addressSort -> isNonNullArrayReference(value.asExpr(addressSort)) + else -> falseExpr + } + } + + private fun TsState.isNonNullArrayReference(reference: UHeapRef): UBoolExpr = with(ctx) { + val isDefined = mkNot(mkEq(reference, mkUndefinedValue())) + val isNonNull = mkNot(mkEq(reference, mkTsNullValue())) + + mkAnd(isDefined, isNonNull, memory.types.evalIsSubtype(reference, anyArrayType)) + } + + private fun TsState.normalExecution(result: UExpr<*>): TsUnknownCallModelExecution = with(ctx) { + val successor = TsUnknownCallModelSuccessor( + guard = trueExpr, + completion = TsUnknownCallModelCompletion.Normal { result }, + ) + + TsUnknownCallModelExecution(successors = listOf(successor)) + } +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt index 2bb04e4ac7..00f06d3f79 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsCapturedInstanceCall.kt @@ -19,6 +19,7 @@ import org.usvm.USort import org.usvm.api.allocateConcreteRef import org.usvm.isAllocatedConcreteHeapRef import org.usvm.isTrue +import org.usvm.machine.call.isBuiltinArrayConstructor import org.usvm.machine.call.isBuiltinGlobalType import org.usvm.machine.state.lastStmt import org.usvm.util.getAllFields @@ -53,8 +54,8 @@ internal fun TsExprResolver.tryCaptureInstanceCall( val priorAssignments = method.cfg.stmts.takeWhile { it !== assignment }.filterIsInstance() val source = originalReceiver(requireNotNull(call.receiver), priorAssignments) - val implicitGlobal = isImplicitModeledGlobal(source, call.callee, method) val receiver = resolve(field.instance) ?: return TsExprApproximationResult.ResolveFailure + val implicitGlobal = isBuiltinArrayConstructor(receiver) || isImplicitModeledGlobal(source, call.callee, method) val reference = when { implicitGlobal -> null receiver.isFakeObject() -> receiver.extractRef(scope) 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 5484d7d03e..419d1aeaf2 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 @@ -92,6 +92,7 @@ import org.jacodb.ets.model.EtsValue import org.jacodb.ets.model.EtsVoidExpr import org.jacodb.ets.model.EtsYieldExpr import org.jacodb.ets.utils.ANONYMOUS_METHOD_PREFIX +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME import org.jacodb.ets.utils.DEFAULT_ARK_METHOD_NAME import org.jacodb.ets.utils.NAMED_FUNCTION_REFERENCE_PREFIX import org.jacodb.ets.utils.getDeclaredLocals @@ -1799,17 +1800,21 @@ class TsSimpleValueResolver( } val currentMethod = scope.calcOnState { lastEnteredMethod } - if (local !in currentMethod.getDeclaredLocals()) { + if (local !in currentMethod.getDeclaredLocals() && local.type is EtsFunctionType) { + val currentFile = currentMethod.enclosingClass?.declaringFile + val defaultClass = currentFile?.classes?.firstOrNull { it.name == DEFAULT_ARK_CLASS_NAME } + val defaultMethod = defaultClass?.methods?.firstOrNull { it.name == DEFAULT_ARK_METHOD_NAME } 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) - } + val isGlobal = defaultMethod?.getDeclaredLocals()?.any { it.name == local.name } == true + val isImported = currentFile?.importInfos?.any { it.name == local.name } == true + val hasSourceBinding = isParameter || isGlobal || isImported + if (hasSourceBinding) return resolveLocal(local) - if (local.type is EtsFunctionType) { - // TODO: function pointers should be "singletons" - return scope.calcOnState { memory.allocConcrete(local.type) } - } + val sdkConstructor = ctx.scene.sdkConstructorForGlobal(local) + if (sdkConstructor != null) return ctx.classConstructorRef(sdkConstructor.signature) + + // TODO: function pointers should be "singletons" + return scope.calcOnState { memory.allocConcrete(local.type) } } return resolveLocal(local) diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt new file mode 100644 index 0000000000..8c4535176c --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsArrayIsArrayIntrinsicModelTest.kt @@ -0,0 +1,202 @@ +package org.usvm.machine.call + +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.DEFAULT_ARK_CLASS_NAME +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.StateCollectionStrategy +import org.usvm.UMachineOptions +import org.usvm.api.TsTestValue +import org.usvm.machine.TsInterpreterObserver +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.machine.call.intrinsic.TsArrayIsArrayIntrinsicModel +import org.usvm.util.TsTestResolver +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertEquals +import kotlin.test.assertFalse +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class TsArrayIsArrayIntrinsicModelTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/models/ArrayIsArrayIntrinsicModel.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val shadowFile = loadEtsFileAutoConvert( + getResourcePath("/models/ArrayIsArraySourceShadow.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val scene = EtsScene(projectFiles = listOf(sourceFile, shadowFile)) + + @Test + fun `scalars are not arrays`() { + val result = analyze("scalarValuesAreNotArrays", "missingArgumentIsNotArray") + + assertTrue(result.values.values.all { values -> assertIs(values.single()).value }) + assertEquals( + List(size = 6) { TsArrayIsArrayIntrinsicModel.MODEL_ID }, + result.modelIds, + ) + } + + @Test + fun `ordinary arrays are arrays`() { + val result = analyze("ordinaryArraysAreArrays") + + assertTrue(assertIs(result.values.getValue("ordinaryArraysAreArrays").single()).value) + assertEquals( + List(size = 2) { TsArrayIsArrayIntrinsicModel.MODEL_ID }, + result.modelIds, + ) + } + + @Test + fun `null and undefined parameters are not arrays`() { + val result = analyze("nullParameterIsNotArray", "undefinedParameterIsNotArray") + + result.values.values.forEach { values -> + assertFalse(assertIs(values.single()).value) + } + assertEquals( + List(size = 2) { TsArrayIsArrayIntrinsicModel.MODEL_ID }, + result.modelIds, + ) + } + + @Test + fun `string and nested array parameters are arrays`() { + val result = analyze("stringArrayIsArray", "nestedArrayIsArray") + + result.values.values.forEach { values -> + assertTrue(assertIs(values.single()).value) + } + assertEquals( + List(size = 2) { TsArrayIsArrayIntrinsicModel.MODEL_ID }, + result.modelIds, + ) + } + + @Test + fun `conditional any arguments preserve both array and non array outcomes`() { + val result = analyze("nullishAnyArrayFallback") + val outcomes = result.values.getValue("nullishAnyArrayFallback").map { value -> + assertIs(value).value + }.toSet() + + assertEquals(setOf(false, true), outcomes) + assertTrue(result.modelIds.isNotEmpty()) + assertTrue(result.modelIds.all { modelId -> modelId == TsArrayIsArrayIntrinsicModel.MODEL_ID }) + } + + @Test + fun `non builtin isArray call is not claimed by the model`() { + val result = analyze("nonBuiltinIsArrayFallsBack") + + assertTrue(result.modelIds.isEmpty()) + assertTrue(result.events.none { event -> event.outcome == TsUnknownCallOutcome.MODEL_APPLIED }) + } + + @Test + fun `source Array shadow keeps its ordinary implementation`() { + val result = analyze("sourceShadowKeepsItsImplementation") + + val value = result.values.getValue("sourceShadowKeepsItsImplementation").single() + assertFalse(assertIs(value).value) + assertTrue(result.modelIds.isEmpty()) + } + + @Test + fun `aliases keep the genuine builtin identity`() { + val result = analyze("arrayAliasKeepsBuiltinIdentity", "builtinAliasSurvivesLocalShadow") + + result.values.values.forEach { values -> + assertTrue(assertIs(values.single()).value) + } + assertEquals(List(size = 3) { TsArrayIsArrayIntrinsicModel.MODEL_ID }, result.modelIds) + } + + @Test + fun `constructor typed source shadows and reassigned aliases preserve their implementation`() { + val result = analyze("typedSourceShadowKeepsItsImplementation", "reassignedAliasKeepsItsImplementation") + + result.values.values.forEach { values -> + assertFalse(assertIs(values.single()).value) + } + assertTrue(result.modelIds.isEmpty()) + } + + @Test + fun `a file global source shadow does not acquire an SDK constructor identity`() { + val result = analyze("globalShadowKeepsItsImplementation", source = shadowFile) + + val value = result.values.getValue("globalShadowKeepsItsImplementation").single() + assertFalse(assertIs(value).value) + assertTrue(result.modelIds.isEmpty()) + } + + private fun analyze(vararg methodNames: String, source: EtsFile = sourceFile): AnalysisResult { + val methods = methodNames.associateWith { name -> method(name, source) } + val observer = RecordingUnknownCallObserver() + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = TsOptions(unknownCallFallback = TsResidualCallPolicy.STOP_PATH), + observer = observer, + ).use { machine -> + val states = machine.analyze(methods.values.toList()) + val values = methods.mapValues { (_, method) -> + states.filter { state -> state.entrypoint === method } + .map { state -> TsTestResolver().resolve(method, state).returnValue } + } + + AnalysisResult( + values = values, + events = observer.events.toList(), + ) + } + } + + private fun method(name: String, source: EtsFile): EtsMethod = scene.projectClasses + .single { clazz -> clazz.name == DEFAULT_ARK_CLASS_NAME && clazz.declaringFile === source } + .methods + .single { method -> method.name == name } + + private class RecordingUnknownCallObserver : TsInterpreterObserver { + val events = mutableListOf() + + override fun onUnknownCall(event: TsUnknownCallEvent) { + events += event + } + } + + private data class AnalysisResult( + val values: Map>, + val events: List, + ) { + val modelIds: List = events.mapNotNull { event -> + (event.decision as? TsUnknownCallDecision.ModelApplied)?.modelId + } + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.BFS), + stateCollectionStrategy = StateCollectionStrategy.ALL, + exceptionsPropagation = true, + throwExceptionOnStepFailure = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 1_000L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt index 77d8018b3a..4de5a89b20 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/machine/call/TsUnknownCallModelCatalogTest.kt @@ -152,6 +152,7 @@ class TsUnknownCallModelCatalogTest { val catalog = TsBuiltInUnknownCallModels.catalog() val expectedModelIds = listOf( + "ts.array.isArray", "ts.array.pop", TsArrayShiftIntrinsicModel.MODEL_ID, TsNumericIntrinsicModelFamily.MATH_ABS_ID, diff --git a/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts b/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts new file mode 100644 index 0000000000..901060192b --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayIsArrayIntrinsicModel.ts @@ -0,0 +1,77 @@ +export function scalarValuesAreNotArrays(): boolean { + return !Array.isArray(42) + && !Array.isArray(true) + && !Array.isArray('value') + && !Array.isArray(undefined) + && !Array.isArray(null); +} + +export function ordinaryArraysAreArrays(): boolean { + return Array.isArray([]) && Array.isArray([1, 2, 3]); +} + +export function stringArrayIsArray(value: string[]): boolean { + return Array.isArray(value); +} + +export function nestedArrayIsArray(value: number[][]): boolean { + return Array.isArray(value); +} + +export function missingArgumentIsNotArray(): boolean { + // @ts-expect-error Arity test deliberately omits the first argument. + return !Array.isArray(); +} + +export function nullParameterIsNotArray(value: null): boolean { + return Array.isArray(value); +} + +export function undefinedParameterIsNotArray(value: undefined): boolean { + return Array.isArray(value); +} + +declare const FakeArray: any; + +export function nonBuiltinIsArrayFallsBack(): boolean { + return FakeArray.isArray([]); +} + +export function nullishAnyArrayFallback(value: any): boolean { + return Array.isArray(value ?? []); +} + +export function sourceShadowKeepsItsImplementation(): boolean { + const Array = { isArray: (_value: unknown): boolean => false }; + return Array.isArray([]); +} + +export function arrayAliasKeepsBuiltinIdentity(): boolean { + const Alias = Array; + const SecondAlias = Alias; + return Alias.isArray([]) && SecondAlias.isArray([1]); +} + +type GlobalArrayConstructor = typeof Array; + +export function typedSourceShadowKeepsItsImplementation(): boolean { + // @ts-expect-error A type annotation must not replace this incomplete source object with the SDK constructor. + const Array: GlobalArrayConstructor = { isArray: (_value: unknown): boolean => false }; + return Array.isArray([]); +} + +export function reassignedAliasKeepsItsImplementation(): boolean { + let Alias = Array; + // @ts-expect-error Deliberately replace the constructor with an object exposing the same method. + Alias = { isArray: (_value: unknown): boolean => false }; + return Alias.isArray([]); +} + +export function builtinAliasSurvivesLocalShadow(): boolean { + const Alias = Array; + { + // @ts-expect-error A local annotation does not change the already captured builtin. + const Array: GlobalArrayConstructor = { isArray: (_value: unknown): boolean => false }; + return Alias.isArray([]) && !Array.isArray([]); + } +} diff --git a/usvm-ts/src/test/resources/models/ArrayIsArraySourceShadow.ts b/usvm-ts/src/test/resources/models/ArrayIsArraySourceShadow.ts new file mode 100644 index 0000000000..4d84928925 --- /dev/null +++ b/usvm-ts/src/test/resources/models/ArrayIsArraySourceShadow.ts @@ -0,0 +1,6 @@ +// @ts-expect-error A source binding may expose only the method used by this program. +const Array: typeof globalThis.Array = { isArray: (_value: unknown): boolean => false }; + +export function globalShadowKeepsItsImplementation(): boolean { + return Array.isArray([]); +}