From b7f4877d828e0136137bf45cb23974d5fbc020e5 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Sat, 22 Aug 2026 22:07:26 +0300 Subject: [PATCH] [TS Calls] Establish a clean integration baseline --- .../usvm/baseline/CallFallbackBaselineTest.kt | 228 ++++++++++++++++++ .../baseline/CallFallbackBaseline.ts | 165 +++++++++++++ 2 files changed, 393 insertions(+) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/baseline/CallFallbackBaselineTest.kt create mode 100644 usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts diff --git a/usvm-ts/src/test/kotlin/org/usvm/baseline/CallFallbackBaselineTest.kt b/usvm-ts/src/test/kotlin/org/usvm/baseline/CallFallbackBaselineTest.kt new file mode 100644 index 000000000..67dedf94f --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/baseline/CallFallbackBaselineTest.kt @@ -0,0 +1,228 @@ +package org.usvm.baseline + +import org.jacodb.ets.model.EtsCallExpr +import org.jacodb.ets.model.EtsFile +import org.jacodb.ets.model.EtsInstanceCallExpr +import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsPtrCallExpr +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.model.EtsStaticCallExpr +import org.jacodb.ets.model.EtsStmt +import org.jacodb.ets.utils.EtsIrProvider +import org.jacodb.ets.utils.callExpr +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Test +import org.usvm.PathSelectionStrategy +import org.usvm.SolverType +import org.usvm.UMachineOptions +import org.usvm.api.targets.ReachabilityObserver +import org.usvm.api.targets.TsReachabilityTarget +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.getResourcePath +import kotlin.test.assertFalse +import kotlin.test.assertIs +import kotlin.test.assertTrue +import kotlin.time.Duration + +class CallFallbackBaselineTest { + private val sourceFile = loadEtsFileAutoConvert( + getResourcePath("/baseline/CallFallbackBaseline.ts"), + provider = EtsIrProvider.TS_FRONTEND, + ) + private val fullScene = EtsScene(listOf(sourceFile)) + + @Test + fun `a declared method without a body is mocked and execution continues`() { + assertTrue(reachesReturn("declaredMethodWithoutBodyContinues")) + } + + @Test + fun `an any receiver with a known method name is mocked and execution continues`() { + assertTrue(reachesReturn("anyReceiverWithKnownMethodContinues")) + } + + @Test + fun `an allocated receiver without a suitable method is mocked and execution continues`() { + assertTrue(reachesReturn("allocatedReceiverWithoutMethodContinues")) + } + + @Test + fun `an unresolved static call prunes the state`() { + val scene = sceneWithout("ExternalStatic") + assertFalse(reachesReturn("unresolvedStaticCallPrunes", scene)) + } + + @Test + fun `an unresolved virtual call prunes the state`() { + val scene = sceneWithout("ExternalReceiver") + assertFalse(reachesReturn("unresolvedVirtualCallPrunes", scene)) + } + + @Test + fun `an unresolved call on an allocated receiver prunes the state`() { + val scene = sceneWithout("ExternalReceiver") + assertFalse(reachesReturn("unresolvedAllocatedReceiverCallPrunes", scene)) + } + + @Test + fun `an instance call on a non-reference value prunes the state`() { + assertIs(callExpression("nonReferenceInstanceCallPrunes")) + assertFalse(reachesReturn("nonReferenceInstanceCallPrunes")) + } + + @Test + fun `an unresolved constructor is mocked and execution continues`() { + val scene = sceneWithout("ExternalReceiver") + assertTrue(reachesReturn("unresolvedConstructorContinues", scene)) + } + + @Test + fun `an unresolved any pointer without an associated function prunes the state`() { + assertPointerCall("unresolvedAnyPointerCallPrunes") + assertFalse(reachesReturn("unresolvedAnyPointerCallPrunes")) + } + + @Test + fun `a non-reference pointer call is mocked and execution continues`() { + assertPointerCall("nonReferencePointerCallContinues") + assertTrue(reachesReturn("nonReferencePointerCallContinues")) + } + + @Test + fun `an intraprocedural assignment call is mocked and execution continues`() { + assertTrue( + reachesReturn( + "intraproceduralAssignmentCallContinues", + tsOptions = TsOptions(interproceduralAnalysis = false), + ) + ) + } + + @Test + fun `an intraprocedural call statement is mocked and execution continues`() { + assertTrue( + reachesReturn( + "intraproceduralCallStatementContinues", + tsOptions = TsOptions(interproceduralAnalysis = false), + ) + ) + } + + @Test + fun `a call to Log is mocked without entering its body`() { + val statements = reachedStatements("logCallSkipsBody") + val logReturn = method(fullScene, "record", className = "Log") + .cfg.stmts.filterIsInstance().single() + + assertTrue(returnStatement(fullScene, "logCallSkipsBody") in statements) + assertFalse(logReturn in statements) + } + + @Test + fun `a call through a receiver named Logger skips its body`() { + assertTrue(reachesReturn("loggerCallSkipsBody")) + } + + @Test + fun `toString returns the current placeholder`() { + assertTrue(reachesReturn("toStringUsesPlaceholder")) + } + + @Test + fun `valueOf returns its receiver`() { + assertTrue(reachesReturn("valueOfReturnsReceiver")) + } + + @Test + fun `native Boolean conversion is an unresolved pointer call that prunes the state`() { + assertPointerCall("booleanConverterPrunes") + assertFalse(reachesReturn("booleanConverterPrunes")) + } + + @Test + fun `Boolean construction without an SDK class prunes before its approximation`() { + assertFalse(reachesReturn("booleanConstructorUsesTruthiness")) + } + + @Test + fun `Math floor rounds toward negative infinity`() { + assertTrue(reachesReturn("mathFloorRoundsTowardNegativeInfinity")) + } + + @Test + fun `resource lookup is approximated before entering its body`() { + assertIs(callExpression("resourceLookupSkipsBody")) + assertTrue(reachesReturn("resourceLookupSkipsBody")) + } + + private fun reachesReturn( + methodName: String, + scene: EtsScene = fullScene, + tsOptions: TsOptions = TsOptions(), + ): Boolean = returnStatement(scene, methodName) in reachedStatements(methodName, scene, tsOptions) + + private fun reachedStatements( + methodName: String, + scene: EtsScene = fullScene, + tsOptions: TsOptions = TsOptions(), + ): Set { + val method = method(scene, methodName) + val returnStatement = returnStatement(scene, methodName) + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + initialTarget.addChild(TsReachabilityTarget.FinalPoint(returnStatement)) + + return TsMachine( + scene = scene, + options = machineOptions, + tsOptions = tsOptions, + machineObserver = ReachabilityObserver(), + ).use { machine -> + machine.analyze(listOf(method), listOf(initialTarget)) + .flatMapTo(mutableSetOf()) { state -> state.pathNode.allStatements } + } + } + + private fun returnStatement(scene: EtsScene, methodName: String): EtsReturnStmt = + method(scene, methodName).cfg.stmts.filterIsInstance().single() + + private fun assertPointerCall(methodName: String) { + assertIs(callExpression(methodName)) + } + + private fun callExpression(methodName: String): EtsCallExpr = method(fullScene, methodName) + .cfg.stmts.mapNotNull { it.callExpr }.single() + + private fun method( + scene: EtsScene, + methodName: String, + className: String = "CallFallbackBaseline", + ): EtsMethod = scene.projectClasses + .single { it.name == className } + .methods.single { it.name == methodName } + + private fun sceneWithout(className: String): EtsScene { + val filteredFile = EtsFile( + signature = sourceFile.signature, + classes = sourceFile.classes.filterNot { it.name == className }, + namespaces = sourceFile.namespaces, + importInfos = sourceFile.importInfos, + exportInfos = sourceFile.exportInfos, + ) + return EtsScene(listOf(filteredFile)) + } + + private companion object { + val machineOptions = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3_500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + } +} diff --git a/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts new file mode 100644 index 000000000..d0a4c13e3 --- /dev/null +++ b/usvm-ts/src/test/resources/baseline/CallFallbackBaseline.ts @@ -0,0 +1,165 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +declare class ExternalReceiver { + external(): void; +} + +declare class ExternalStatic { + static external(): void; +} + +class KnownReceiver { + known(): number { + return 1; + } + + toString(): string { + throw "KnownReceiver.toString must be approximated"; + } + + valueOf(): KnownReceiver { + throw "KnownReceiver.valueOf must be approximated"; + } +} + +class EmptyReceiver { +} + +class Log { + static record(): number { + return 999; + } +} + +class LoggerFacade { + info(): void { + throw "Logger calls must be approximated"; + } +} + +function $r(resource: string): any { + throw "resource lookup must be approximated"; +} + +class CallFallbackBaseline { + declaredMethodWithoutBodyContinues(): number { + const receiver = new ExternalReceiver(); + receiver.external(); + return 101; + } + + anyReceiverWithKnownMethodContinues(receiver: any): number { + receiver.known(); + return 102; + } + + allocatedReceiverWithoutMethodContinues(): number { + const receiver = new EmptyReceiver(); + receiver.missing(); + return 103; + } + + unresolvedStaticCallPrunes(): number { + ExternalStatic.external(); + return 104; + } + + unresolvedVirtualCallPrunes(receiver: ExternalReceiver): number { + receiver.external(); + return 105; + } + + unresolvedAllocatedReceiverCallPrunes(): number { + const receiver = new ExternalReceiver(); + receiver.external(); + return 119; + } + + nonReferenceInstanceCallPrunes(receiver: number): number { + receiver.missing(); + return 120; + } + + unresolvedConstructorContinues(): number { + new ExternalReceiver(); + return 106; + } + + unresolvedAnyPointerCallPrunes(callback: any): number { + callback(42); + return 107; + } + + nonReferencePointerCallContinues(callback: number): number { + callback(42); + return 108; + } + + intraproceduralAssignmentCallContinues(): number { + const value = this.known(); + return value + 108; + } + + intraproceduralCallStatementContinues(): number { + this.known(); + return 110; + } + + logCallSkipsBody(): number { + Log.record(); + return 111; + } + + loggerCallSkipsBody(): number { + const Logger = new LoggerFacade(); + Logger.info(); + return 112; + } + + toStringUsesPlaceholder(): number { + const receiver = new KnownReceiver(); + if (receiver.toString() === "I am a string") { + return 113; + } + throw "unexpected toString approximation"; + } + + valueOfReturnsReceiver(): number { + const receiver = new KnownReceiver(); + if (receiver.valueOf() === receiver) { + return 114; + } + throw "unexpected valueOf approximation"; + } + + booleanConverterPrunes(): number { + if (Boolean(1)) { + return 115; + } + throw "unexpected Boolean approximation"; + } + + booleanConstructorUsesTruthiness(): number { + if (new Boolean(0)) { + throw "unexpected Boolean constructor approximation"; + } + return 118; + } + + mathFloorRoundsTowardNegativeInfinity(): number { + if (Math.floor(-1.75) === -2) { + return 116; + } + throw "unexpected Math.floor approximation"; + } + + resourceLookupSkipsBody(): number { + $r("app.string.name"); + return 117; + } + + known(): number { + return 1; + } +}