diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index ff34417fe5..c651b676ca 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt @@ -1,5 +1,6 @@ package org.usvm.machine.expr +import io.ksmt.expr.KFpRoundingMode import io.ksmt.utils.asExpr import mu.KotlinLogging import org.jacodb.ets.model.EtsArrayType @@ -76,6 +77,13 @@ internal fun TsExprResolver.tryApproximateInstanceCall( } } + // Handle `Math` method calls + if (expr.instance.name == "Math") { + if (expr.callee.name == "floor") { + return from(handleMathFloor(expr)) + } + } + val instance = scope.calcOnState { resolve(expr.instance)?.asExpr(addressSort) } ?: return TsExprApproximationResult.ResolveFailure @@ -255,6 +263,27 @@ private fun TsExprResolver.handlePromiseResolveReject(expr: EtsInstanceCallExpr) promise } +private fun TsExprResolver.handleMathFloor(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) { + check(expr.args.size == 1) { + "Math.floor() should have exactly one argument, but got ${expr.args.size}" + } + val arg = resolve(expr.args.single()) ?: return null + + when (arg.sort) { + fp64Sort -> mkFpRoundToIntegralExpr( + roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardNegative), + value = arg.asExpr(fp64Sort), + ) + + sizeSort -> arg.asExpr(sizeSort) + + else -> { + logger.warn { "Unsupported argument sort for Math.floor(): ${arg.sort}" } + null + } + } +} + /** * Handles the `Array.push(...items)` method call. * Appends the specified `items` to the end of the array. diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/AsyncReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/AsyncReachabilityTest.kt new file mode 100644 index 0000000000..e3a4b97a28 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/AsyncReachabilityTest.kt @@ -0,0 +1,296 @@ +package org.usvm.reachability + +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Disabled +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.api.targets.TsTarget +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertTrue +import kotlin.time.Duration + +/** + * Tests for asynchronous programming reachability scenarios. + * Verifies reachability analysis through async patterns and error handling. + */ +class AsyncReachabilityTest { + + private val scene = run { + val path = "/reachability/AsyncReachability.ts" + val res = getResourcePath(path) + val file = loadEtsFileAutoConvert(res) + EtsScene(listOf(file)) + } + + private val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + private val tsOptions = TsOptions() + + @Test + fun testAsyncAwaitReachable() { + // Test reachability through async function logic: + // const result = delay * 2 -> if (result > 50) -> if (result < 100) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "asyncAwaitReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (result > 50) + val minCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(minCheck)) + + // if (result < 100) + val maxCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(maxCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for async/await reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when delay * 2 is between 50-100" + ) + } + + @Test + fun testPromiseChainReachable() { + // Test reachability through Promise chain: + // const doubled = value * 2 -> if (doubled === 20) -> return Promise.resolve(1) + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "promiseChainReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (doubled === 20) + val doubledCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(doubledCheck)) + + // return Promise.resolve(1) + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for Promise chain reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when input value is 10" + ) + } + + @Disabled("No ::map method") + @Test + fun testPromiseAllReachable() { + // Test reachability through Promise.all pattern: + // const results = values.map(v => v * 2) -> if (results.length === 3) -> if (results[1] === 40) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "promiseAllReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (results.length === 3) + val lengthCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(lengthCheck)) + + // if (results[1] === 40) + val valueCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(valueCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for Promise.all reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when values[1] is 20 (doubled to 40)" + ) + } + + @Disabled("Function types are not supported in EtsHierarchy") + @Test + fun testCallbackReachable() { + // Test reachability through callback pattern: + // const processed = value + 10 -> if (processed > 25) -> callback(processed) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "callbackReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (processed > 25) + val processedCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(processedCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for callback reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when value > 15 (processed > 25)" + ) + } + + @Test + fun testErrorHandlingReachable() { + // Test reachability through try-catch error handling: + // try { if (shouldThrow) throw Error -> return 1 } catch { return -1 } + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "errorHandlingReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (shouldThrow) + val throwCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(throwCheck)) + + // Both return paths should be reachable + val returnStmts = method.cfg.stmts.filterIsInstance() + returnStmts.forEach { returnStmt -> + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + } + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for error handling reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmts.any { it in reachedStatements }, + "Expected at least one return statement to be reached in try-catch" + ) + } + + @Test + fun testConditionalAsyncReachable() { + // Test reachability through conditional async pattern: + // if (useSync) result = value * 2 else result = value + 10 -> if (result === 20) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "conditionalAsyncReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (useSync) + val useSyncCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(useSyncCheck)) + + // if (result === 20) + val resultCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(resultCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for conditional async reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached through conditional branches" + ) + } + + @Test + fun testPromiseCreationReachable() { + // Test reachability through Promise creation logic: + // if (shouldResolve) -> if (value > 5) -> return 1 + // else -> if (value < 0) -> return -1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "promiseCreationReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (shouldResolve) + val shouldResolveCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(shouldResolveCheck)) + + // Multiple return paths + val returnStmts = method.cfg.stmts.filterIsInstance() + returnStmts.forEach { returnStmt -> + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + } + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for Promise creation reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmts.any { it in reachedStatements }, + "Expected at least one return statement to be reached in Promise creation" + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt index a425e4de42..2affb0f943 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt @@ -4,6 +4,7 @@ import org.jacodb.ets.model.EtsIfStmt import org.jacodb.ets.model.EtsReturnStmt import org.jacodb.ets.model.EtsScene import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Disabled import org.usvm.PathSelectionStrategy import org.usvm.SolverType import org.usvm.UMachineOptions @@ -95,7 +96,7 @@ class ComplexReachabilityTest { target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) // return 1 - val returnStmt = method.cfg.stmts.filterIsInstance()[0] + val returnStmt = method.cfg.stmts.filterIsInstance()[1] target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) val results = machine.analyze(listOf(method), listOf(initialTarget)) @@ -147,6 +148,7 @@ class ComplexReachabilityTest { ) } + @Disabled("Multiple methods ::process") @Test fun testConditionalObjectReachable() { // Test reachability with conditional object creation and polymorphic method calls @@ -167,7 +169,7 @@ class ComplexReachabilityTest { target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) // return 1 - val return1 = method.cfg.stmts.filterIsInstance()[0] + val return1 = method.cfg.stmts.filterIsInstance()[2] target.addChild(TsReachabilityTarget.FinalPoint(return1)) // return 2 diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt index 0ad63c6702..837a551e8a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt @@ -161,7 +161,7 @@ class FunctionCallReachabilityTest { target = target.addChild(TsReachabilityTarget.IntermediatePoint(check)) // return 1 - val returnStmt = method.cfg.stmts.filterIsInstance()[0] + val returnStmt = method.cfg.stmts.filterIsInstance()[1] target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) val results = machine.analyze(listOf(method), listOf(initialTarget)) diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/HigherOrderFunctionsReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/HigherOrderFunctionsReachabilityTest.kt new file mode 100644 index 0000000000..151816f119 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/HigherOrderFunctionsReachabilityTest.kt @@ -0,0 +1,319 @@ +package org.usvm.reachability + +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Disabled +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.api.targets.TsTarget +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertTrue +import kotlin.time.Duration + +/** + * Tests for higher-order functions and closures reachability scenarios. + * Verifies reachability analysis through function composition and array processing patterns. + */ +@Disabled("Iterators are not supported") +class HigherOrderFunctionsReachabilityTest { + + private val scene = run { + val path = "/reachability/HigherOrderFunctionsReachability.ts" + val res = getResourcePath(path) + val file = loadEtsFileAutoConvert(res) + EtsScene(listOf(file)) + } + + private val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + private val tsOptions = TsOptions() + + @Test + fun testFunctionFactoryReachable() { + // Test reachability through function factory: + // const factor = 3 -> if (factor > 2) -> const result = value * factor -> if (result === 15) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "functionFactoryReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (factor > 2) + val factorCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(factorCheck)) + + // if (result === 15) + val resultCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(resultCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for function factory reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when value = 5 and factor = 3 (5 * 3 = 15)" + ) + } + + @Test + fun testCallbackReachable() { + // Test reachability through callback-like array processing: + // return this.processWithCallback(numbers, multiplier) -> 30 * 5 = 150 > 100 -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "callbackReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // return statement from processWithCallback + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for callback reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when callback produces value > 100" + ) + } + + @Test + fun testProcessWithCallbackReachable() { + // Test the helper method processWithCallback: + // for (const item of arr) -> const processed = item * multiplier -> if (processed > 100) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "processWithCallback" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (processed > 100) + val processedCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(processedCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for processWithCallback reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when any item * multiplier > 100" + ) + } + + @Test + fun testClosureReachable() { + // Test reachability through closure-like counter: + // counter += 5 -> counter += 10 -> if (counter === 15) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "closureReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (counter === 15) + val counterCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(counterCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for closure reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when accumulated counter equals 15" + ) + } + + @Test + fun testCompositionReachable() { + // Test reachability through function composition: + // const doubled = input * 2 -> const addedTen = doubled + 10 -> if (addedTen === 30) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "compositionReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (addedTen === 30) + val resultCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(resultCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for function composition reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when input = 10: double(10) = 20, addTen(20) = 30" + ) + } + + @Test + fun testArrowFunctionReachable() { + // Test reachability through arrow function: + // const result = input > 5 ? input * 2 : input -> if (result === 14) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "arrowFunctionReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (result === 14) + val resultCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(resultCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for arrow function reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached: 7 > 5, so 7 * 2 = 14" + ) + } + + @Test + fun testMapOperationReachable() { + // Test reachability through map-like operation: + // for (const value of values) -> const transformed = value * 3 -> if (transformed > 50) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "mapOperationReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (transformed > 50) + val transformedCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(transformedCheck)) + + // if (hasLargeValue) + val hasLargeValueCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(hasLargeValueCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for map operation reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when any value * 3 > 50" + ) + } + + @Test + fun testFilterOperationReachable() { + // Test reachability through filter-like operation: + // for (const value of values) -> if (value > 10) filteredCount++ -> if (filteredCount === 2) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "filterOperationReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (value > 10) + val valueCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(valueCheck)) + + // if (filteredCount === 2) + val countCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(countCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for filter operation reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when exactly 2 values are > 10" + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/InheritanceReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/InheritanceReachabilityTest.kt new file mode 100644 index 0000000000..e010dc48cb --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/InheritanceReachabilityTest.kt @@ -0,0 +1,292 @@ +package org.usvm.reachability + +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Disabled +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.api.targets.TsTarget +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertTrue +import kotlin.time.Duration + +/** + * Tests for class inheritance and polymorphism reachability scenarios. + * Verifies reachability analysis through class hierarchies, method overriding, and inheritance patterns. + */ +@Disabled("Inheritance is hard") +class InheritanceReachabilityTest { + + private val scene = run { + val path = "/reachability/InheritanceReachability.ts" + val res = getResourcePath(path) + val file = loadEtsFileAutoConvert(res) + EtsScene(listOf(file)) + } + + private val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + private val tsOptions = TsOptions() + + @Test + fun testPolymorphicCallReachable() { + // Test reachability through polymorphic method calls: + // if (useA) instance = new ConcreteA(value) else instance = new ConcreteB(value, 2) + // const result = instance.process() -> if (result > 0) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "polymorphicCallReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (useA) + val useACheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(useACheck)) + + // if (result > 0) + val resultCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(resultCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for polymorphic call reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached through either polymorphic path" + ) + } + + @Test + fun testInstanceofInheritanceReachable() { + // Test reachability through type-specific method call: + // const obj = new ConcreteA(value) -> const specificResult = obj.specificMethodA() -> if (specificResult === 1) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "instanceofInheritanceReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (specificResult === 1) + val specificResultCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(specificResultCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for instanceof inheritance reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when value is 15" + ) + } + + @Test + fun testMethodOverrideReachable() { + // Test reachability through method overriding: + // objA.commonMethod() vs objB.commonMethod() -> if (resultA === 20 && resultB === 30) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "methodOverrideReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (resultA === 20 && resultB === 30) + val overrideCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(overrideCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for method override reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when base method gives 20 and override gives 30" + ) + } + + @Test + fun testConstructorChainingReachable() { + // Test reachability through constructor chaining: + // const obj = new ConcreteB(15, 4) -> if (obj.process() === 1) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "constructorChainingReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (processResult === 1) + val processCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(processCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for constructor chaining reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when 15 * 4 = 60 > 50" + ) + } + + @Test + fun testSimpleInheritanceReachable() { + // Test reachability through inheritance with protected field access: + // if (obj.value > 10) -> const commonResult = obj.commonMethod() -> if (commonResult === 24) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "simpleInheritanceReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (obj.value > 10) + val valueCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(valueCheck)) + + // if (commonResult === 24) + val commonResultCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(commonResultCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for simple inheritance reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached through inheritance (12 * 2 = 24)" + ) + } + + @Test + fun testFieldInheritanceReachable() { + // Test reachability through field access in inheritance hierarchy: + // if (obj.value < 10) -> const result = obj.process() -> if (result === 0) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "fieldInheritanceReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (obj.value < 10) + val valueCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(valueCheck)) + + // if (result === 0) + val resultCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(resultCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for field inheritance reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when multiplication doesn't exceed threshold" + ) + } + + @Test + fun testAbstractMethodReachable() { + // Test reachability through abstract method implementations in ConcreteA + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + + // Test ConcreteA.process() method directly + val concreteAMethods = scene.projectClasses + .first { it.name.contains("ConcreteA") } + .methods.filter { it.name == "process" } + + val method = concreteAMethods.first() + val target = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + + // if (this.value > 10) + // return this.commonMethod() or similar + val ifStmt = method.cfg.stmts.filterIsInstance()[0] + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target + .addChild(TsReachabilityTarget.IntermediatePoint(ifStmt)) + .addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(target)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for abstract method implementation reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when value > 10" + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/LoopsReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/LoopsReachabilityTest.kt new file mode 100644 index 0000000000..79189c19ec --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/LoopsReachabilityTest.kt @@ -0,0 +1,260 @@ +package org.usvm.reachability + +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Disabled +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.api.targets.TsTarget +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertTrue +import kotlin.time.Duration + +/** + * Tests for loops and iteration reachability scenarios. + * Verifies reachability analysis through for loops, while loops, and loop control statements. + */ +class LoopsReachabilityTest { + + private val scene = run { + val path = "/reachability/LoopsReachability.ts" + val res = getResourcePath(path) + val file = loadEtsFileAutoConvert(res) + EtsScene(listOf(file)) + } + + private val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + private val tsOptions = TsOptions() + + @Test + fun testForLoopReachable() { + // Test reachability through for loop: + // for (let i = 0; i < limit; i++) -> if (i === 5) -> if (limit > 10) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "forLoopReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (i === 5) + val iCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(iCheck)) + + // if (limit > 10) + val limitCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(limitCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for for loop reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when limit > 10" + ) + } + + @Test + fun testWhileLoopBreakReachable() { + // Test reachability through while loop with break: + // while (counter < 100) -> if (counter === 20) break -> if (counter > 50) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "whileLoopBreakReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (counter === 20) + val breakCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(breakCheck)) + + // if (counter > 50) - this should be unreachable due to break + val unreachableCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(unreachableCheck)) + + // return 1 - should be unreachable + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + + // This test verifies that the unreachable path is correctly identified + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + // The return 1 should NOT be reached due to break at counter == 20 + } + + @Test + fun testNestedLoopContinueReachable() { + // Test reachability through nested loops with continue: + // for (i < 5) -> for (j < 5) -> if (i + j === 3) continue -> if (i === 2 && j === 3) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "nestedLoopContinueReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (i + j === 3) + val continueCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(continueCheck)) + + // if (i === 2 && j === 3) + val reachableCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(reachableCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for nested loop reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when i=2, j=3 (2+3=5, not 3)" + ) + } + + @Disabled("Iterators are not yet supported") + @Test + fun testForInLoopReachable() { + // Test reachability through for-in loop: + // for (const key in obj) -> if (key === "b") -> if (obj[key] === 2) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "forInLoopReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (key === "b") + val keyCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(keyCheck)) + + // if (obj[key] === 2) + val valueCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(valueCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[1] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for for-in loop reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when key 'b' has value 2" + ) + } + + @Disabled("Iterators are not yet supported") + @Test + fun testForOfLoopReachable() { + // Test reachability through for-of loop: + // for (const value of arr) -> if (value > 25) -> if (value < 35) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "forOfLoopReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (value > 25) + val minCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(minCheck)) + + // if (value < 35) + val maxCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(maxCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[1] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for for-of loop reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached for value 30 (25 < 30 < 35)" + ) + } + + @Test + fun testDoWhileReachable() { + // Test reachability through do-while loop: + // do { count++; if (count === threshold) -> return 1 } while (count < threshold) + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "doWhileReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (count === threshold) + val thresholdCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(thresholdCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[1] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for do-while loop reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached at least once in do-while" + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/RecursionReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/RecursionReachabilityTest.kt new file mode 100644 index 0000000000..89687e4c4c --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/RecursionReachabilityTest.kt @@ -0,0 +1,401 @@ +package org.usvm.reachability + +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Disabled +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.api.targets.TsTarget +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertTrue +import kotlin.time.Duration + +/** + * Tests for recursion reachability scenarios. + * Verifies reachability analysis through recursive function calls with controlled depth limits. + */ +@Disabled("Recursion is not fully supported yet") +class RecursionReachabilityTest { + + private val scene = run { + val path = "/reachability/RecursionReachability.ts" + val res = getResourcePath(path) + val file = loadEtsFileAutoConvert(res) + EtsScene(listOf(file)) + } + + private val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + private val tsOptions = TsOptions() + + @Test + fun testFactorialReachable() { + // Test reachability through factorial wrapper with depth limits: + // const result = this.factorial(input) -> if (result === 24) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "factorialReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (result === 24) + val resultCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(resultCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for factorial reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when input = 4 (4! = 24)" + ) + } + + @Test + fun testFactorialDirectReachable() { + // Test reachability within factorial method itself with depth limits: + // if (n <= 1) -> return 1 (base case) + // if (n > 5) -> return -1 (depth limit) + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "factorial" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (n <= 1) + val baseCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(baseCheck)) + + // if (n > 5) + val depthCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(depthCheck)) + + // Multiple return paths should be reachable + val returnStmts = method.cfg.stmts.filterIsInstance() + returnStmts.forEach { returnStmt -> + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + } + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for direct factorial reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmts.any { it in reachedStatements }, + "Expected at least one return statement to be reached in factorial" + ) + } + + @Test + fun testCountdownReachable() { + // Test reachability through tail recursion with depth limits: + // this.countdown(n - 1, accumulator + n) -> if (n === 0 && accumulator > 10) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "countdown" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (n === 0) + val baseCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(baseCheck)) + + // if (accumulator > 10) + val accumulatorCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(accumulatorCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for tail recursion reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when initial n leads to accumulator > 10" + ) + } + + @Test + fun testMutualRecursionReachable() { + // Test reachability through mutual recursion with depth limits: + // if (input > 0 && input < 5) -> const evenResult = this.isEven(input) -> if (evenResult && input === 4) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "mutualRecursionReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (input > 0 && input < 5) + val rangeCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(rangeCheck)) + + // if (evenResult && input === 4) + val evenAndFourCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(evenAndFourCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for mutual recursion reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached for even number 4" + ) + } + + @Test + fun testFibonacciIterativeReachable() { + // Test reachability through iterative fibonacci approach: + // if (n <= 1) return n -> for loop calculation -> if (b === 13) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "fibonacciIterative" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (n <= 1) + val baseCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(baseCheck)) + + // if (n > 10) + val limitCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(limitCheck)) + + // if (b === 13) + val specialCheck = method.cfg.stmts.filterIsInstance()[2] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(specialCheck)) + + // return 1 + val specialReturn = method.cfg.stmts.filterIsInstance()[1] // Second return statement + target.addChild(TsReachabilityTarget.FinalPoint(specialReturn)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for fibonacci iterative reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + specialReturn in reachedStatements, + "Expected special return statement to be reached when fib(7) = 13" + ) + } + + @Test + fun testTreeTraversalReachable() { + // Test reachability through simplified tree traversal with parameterized target: + // if (treeNode.value === target) -> return 1 (reachable when target = 10) + // if (treeNode.left.value === target) -> return 2 (reachable when target = 5) + // if (treeNode.right.value === target) -> return 3 (reachable when target = 15) + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "treeTraversalReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + + // Path 1: + // if (treeNode.value === target) + // return 1 + val ifStmt1 = method.cfg.stmts.filterIsInstance()[0] + val returnStmt1 = method.cfg.stmts.filterIsInstance()[0] + + initialTarget + .addChild(TsReachabilityTarget.IntermediatePoint(ifStmt1)) + .addChild(TsReachabilityTarget.FinalPoint(returnStmt1)) + + // Path 2: + // if (treeNode.left.value === target) + // return 2 + val ifStmt2 = method.cfg.stmts.filterIsInstance()[1] + val returnStmt2 = method.cfg.stmts.filterIsInstance()[1] + initialTarget + .addChild(TsReachabilityTarget.IntermediatePoint(ifStmt2)) + .addChild(TsReachabilityTarget.FinalPoint(returnStmt2)) + + // Path 3: + // if (treeNode.right.value === target) + // return 3 + val ifStmt3 = method.cfg.stmts.filterIsInstance()[2] + val returnStmt3 = method.cfg.stmts.filterIsInstance()[2] + initialTarget + .addChild(TsReachabilityTarget.IntermediatePoint(ifStmt3)) + .addChild(TsReachabilityTarget.FinalPoint(returnStmt3)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for tree traversal reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt1 in reachedStatements, + "Expected 'return 1' to be reached when target = 10" + ) + assertTrue( + returnStmt2 in reachedStatements, + "Expected 'return 2' to be reached when target = 5" + ) + assertTrue( + returnStmt3 in reachedStatements, + "Expected 'return 3' to be reached when target = 15" + ) + } + + @Test + fun testSumRecursionReachable() { + // Test reachability through simple recursive sum with depth limits: + // const result = this.sumToN(input) -> if (result === 15) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "sumRecursionReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (result === 15) + val resultCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(resultCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for sum recursion reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when input = 5 (sum(5) = 15)" + ) + } + + @Test + fun testBinarySearchReachable() { + // Test reachability through binary search with depth limits: + // const found = this.binarySearchSimple(sortedArray, 7) -> if (found) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "binarySearchReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (found) + val foundCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(foundCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for binary search reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when target 7 is found" + ) + } + + @Disabled("Infinite") + @Test + fun testIsEvenDirectReachable() { + // Test reachability within isEven method for mutual recursion: + // if (n === 0) return true -> if (n === 1) return false -> if (n > 4) return false -> this.isOdd(n - 1) + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "isEven" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // Multiple conditional checks in isEven + val ifStmts = method.cfg.stmts.filterIsInstance() + ifStmts.forEach { ifStmt -> + target = target.addChild(TsReachabilityTarget.IntermediatePoint(ifStmt)) + } + + // Multiple return paths + val returnStmts = method.cfg.stmts.filterIsInstance() + returnStmts.forEach { returnStmt -> + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + } + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for isEven direct reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmts.any { it in reachedStatements }, + "Expected at least one return statement to be reached in isEven" + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/TypeGuardsReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/TypeGuardsReachabilityTest.kt new file mode 100644 index 0000000000..c8d00c1245 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/TypeGuardsReachabilityTest.kt @@ -0,0 +1,385 @@ +package org.usvm.reachability + +import org.jacodb.ets.model.EtsIfStmt +import org.jacodb.ets.model.EtsReturnStmt +import org.jacodb.ets.model.EtsScene +import org.jacodb.ets.utils.loadEtsFileAutoConvert +import org.junit.jupiter.api.Disabled +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.api.targets.TsTarget +import org.usvm.machine.TsMachine +import org.usvm.machine.TsOptions +import org.usvm.util.getResourcePath +import kotlin.test.Test +import kotlin.test.assertTrue +import kotlin.time.Duration + +/** + * Tests for type guards and assertions reachability scenarios. + * Verifies reachability analysis through typeof checks, instanceof operations, and user-defined type guards. + */ +class TypeGuardsReachabilityTest { + + private val scene = run { + val path = "/reachability/TypeGuardsReachability.ts" + val res = getResourcePath(path) + val file = loadEtsFileAutoConvert(res) + EtsScene(listOf(file)) + } + + private val options = UMachineOptions( + pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED), + exceptionsPropagation = true, + stopOnTargetsReached = true, + timeout = Duration.INFINITE, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + private val tsOptions = TsOptions() + + @Disabled("Typeof is not fully supported") + @Test + fun testTypeofGuardReachable() { + // Test reachability through typeof type guard with constant string comparison: + // if (typeof value === "string") -> if (value === "hello") -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "typeofGuardReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (typeof value === "string") + val typeofCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(typeofCheck)) + + // if (value === "hello") + val stringCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(stringCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for typeof guard reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when value is exactly 'hello'" + ) + } + + @Disabled("Fake type in type constraints") + @Test + fun testInstanceofGuardReachable() { + // Test reachability through instanceof type guard: + // if (obj instanceof Array) -> if (obj.length === 3) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "instanceofGuardReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (obj instanceof Array) + val instanceofCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(instanceofCheck)) + + // if (obj.length === 3) + val lengthCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(lengthCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[1] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for instanceof guard reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when obj is array with length 3" + ) + } + + @Disabled("Typeof is not fully supported") + @Test + fun testUserDefinedGuardReachable() { + // Test reachability through user-defined type guard: + // if (this.isString(input)) -> if (input === "test") -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "userDefinedGuardReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (this.isString(input)) + val guardCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(guardCheck)) + + // if (input === "test") + val testCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(testCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for user-defined guard reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when input is exactly 'test'" + ) + } + + @Test + fun testTypeAssertionReachable() { + // Test reachability through type assertion: + // const str = value as string -> if (str === "A") -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "typeAssertionReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (str === "A") + val assertionCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(assertionCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[1] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for type assertion reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when value is exactly 'A'" + ) + } + + @Disabled("Input string to constant string comparison") + @Test + fun testNonNullAssertionReachable() { + // Test reachability through non-null assertion: + // if (value !== null) -> const definiteString = value! -> if (definiteString === "nonempty") -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "nonNullAssertionReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (value !== null) + val nullCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(nullCheck)) + + // if (definiteString === "nonempty") + val stringCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(stringCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for non-null assertion reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when value is non-null 'nonempty'" + ) + } + + @Disabled("Typeof is not fully supported") + @Test + fun testNumericTypeGuardReachable() { + // Test reachability through numeric type guard: + // if (typeof value === "number") -> if (value > 10) -> if (value < 20) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "numericTypeGuardReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (typeof value === "number") + val typeofCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(typeofCheck)) + + // if (value > 10) + val minCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(minCheck)) + + // if (value < 20) + val maxCheck = method.cfg.stmts.filterIsInstance()[2] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(maxCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for numeric type guard reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached for numbers between 10 and 20" + ) + } + + @Test + fun testBooleanTypeGuardReachable() { + // Test reachability through boolean type guard: + // if (typeof value === "boolean") -> if (value === true) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "booleanTypeGuardReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (typeof value === "boolean") + val typeofCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(typeofCheck)) + + // if (value === true) + val boolCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(boolCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[1] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for boolean type guard reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached when value is boolean true" + ) + } + + @Test + fun testObjectTypeGuardReachable() { + // Test reachability through object type guard: + // if (typeof value === "object" && value !== null) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "objectTypeGuardReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (typeof value === "object" && value !== null) + val objectCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(objectCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for object type guard reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached for non-null objects" + ) + } + + @Disabled("Fake type in type constraints") + @Test + fun testComplexTypeGuardReachable() { + // Test reachability through complex type guard combination: + // if (typeof value === "object" && value !== null) -> if (value instanceof Date) -> if (value.getFullYear() > 2020) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "complexTypeGuardReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (typeof value === "object" && value !== null) + val objectCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(objectCheck)) + + // if (value instanceof Date) + val dateCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(dateCheck)) + + // if (value.getFullYear() > 2020) + val yearCheck = method.cfg.stmts.filterIsInstance()[2] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(yearCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for complex type guard reachability" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached for dates after 2020" + ) + } +} diff --git a/usvm-ts/src/test/resources/reachability/AsyncReachability.ts b/usvm-ts/src/test/resources/reachability/AsyncReachability.ts new file mode 100644 index 0000000000..e674a077a7 --- /dev/null +++ b/usvm-ts/src/test/resources/reachability/AsyncReachability.ts @@ -0,0 +1,93 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +/** + * Asynchronous programming reachability scenarios. + * Tests reachability through async patterns and error handling. + */ +class AsyncReachability { + + // Async function with conditional logic + async asyncAwaitReachable(delay: number): Promise { + const result = delay * 2; + if (result > 50) { + if (result < 100) { + return 1; // Reachable when delay * 2 is between 50-100 + } + } + return 0; + } + + // Promise with conditional return + promiseChainReachable(value: number): Promise { + const doubled = value * 2; + if (doubled === 20) { + return Promise.resolve(1); // Reachable when input value is 10 + } + return Promise.resolve(0); + } + + // Array processing with Promise-like result + async promiseAllReachable(values: number[]): Promise { + const results = values.map(v => v * 2); + + if (results.length === 3) { + if (results[1] === 40) { + return 1; // Reachable when values[1] is 20 + } + } + return 0; + } + + // Callback pattern with threshold check + callbackReachable(value: number, callback: (result: number) => void): number { + const processed = value + 10; + if (processed > 25) { + callback(processed); + return 1; // Reachable when value > 15 + } + return 0; + } + + // Try-catch error handling + errorHandlingReachable(shouldThrow: boolean): number { + try { + if (shouldThrow) { + throw new Error("Test error"); + } + return 1; // Reachable when shouldThrow is false + } catch (error) { + return -1; // Reachable when shouldThrow is true + } + } + + // Conditional branching with different calculations + conditionalAsyncReachable(useSync: boolean, value: number): number { + let result: number; + + if (useSync) { + result = value * 2; + } else { + result = value + 10; + } + + if (result === 20) { + return 1; // Reachable: value=10 with useSync=true, or value=10 with useSync=false + } + return 0; + } + + // Promise creation with conditional logic + promiseCreationReachable(shouldResolve: boolean, value: number): number { + if (shouldResolve) { + if (value > 5) { + return 1; // Reachable when shouldResolve=true and value>5 + } + } else { + if (value < 0) { + return -1; // Reachable when shouldResolve=false and value<0 + } + } + return 0; + } +} diff --git a/usvm-ts/src/test/resources/reachability/HigherOrderFunctionsReachability.ts b/usvm-ts/src/test/resources/reachability/HigherOrderFunctionsReachability.ts new file mode 100644 index 0000000000..9aa7b12cbd --- /dev/null +++ b/usvm-ts/src/test/resources/reachability/HigherOrderFunctionsReachability.ts @@ -0,0 +1,120 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +/** + * Higher-order functions and closures reachability scenarios. + * Tests reachability through function composition and array processing patterns. + */ +class HigherOrderFunctionsReachability { + + // Function factory with conditional return + createMultiplier(factor: number): (x: number) => number { + if (factor > 2) { + return function(x: number): number { + return x * factor; + }; + } else { + return function(x: number): number { + return x; + }; + } + } + + functionFactoryReachable(value: number): number { + const factor = 3; + if (factor > 2) { + const result = value * factor; + if (result === 15) { + return 1; // Reachable when value = 5 and factor = 3 + } + } + return 0; + } + + // Array processing with callback-like behavior + processWithCallback(arr: number[], multiplier: number): number { + for (const item of arr) { + const processed = item * multiplier; + if (processed > 100) { + return 1; // Reachable based on array values and multiplier + } + } + return 0; + } + + callbackReachable(): number { + const numbers = [10, 20, 30]; + const multiplier = 5; + return this.processWithCallback(numbers, multiplier); + // Returns 1 because 30 * 5 = 150 > 100 + } + + // Counter with incremental updates + closureReachable(): number { + let counter = 0; + + counter += 5; + counter += 10; + + if (counter === 15) { + return 1; // Reachable when accumulated counter equals 15 + } + return 0; + } + + // Function composition through sequential operations + compositionReachable(input: number): number { + const doubled = input * 2; + const addedTen = doubled + 10; + + if (addedTen === 30) { + return 1; // Reachable when input = 10: double(10) = 20, addTen(20) = 30 + } + return 0; + } + + // Conditional expression with ternary operator + arrowFunctionReachable(): number { + const input = 7; + const result = input > 5 ? input * 2 : input; + + if (result === 14) { + return 1; // Reachable: 7 > 5, so 7 * 2 = 14 + } + return 0; + } + + // Map-like transformation with early termination + mapOperationReachable(values: number[]): number { + let hasLargeValue = false; + + for (const value of values) { + const transformed = value * 3; + if (transformed > 50) { + hasLargeValue = true; + break; + } + } + + if (hasLargeValue) { + return 1; // Reachable when any value * 3 > 50 + } + return 0; + } + + // Filter-like counting operation + filterOperationReachable(values: number[]): number { + let filteredCount = 0; + + for (const value of values) { + if (value > 10) { + filteredCount++; + } + } + + if (filteredCount === 2) { + return 1; // Reachable when exactly 2 values are > 10 + } + return 0; + } +} diff --git a/usvm-ts/src/test/resources/reachability/InheritanceReachability.ts b/usvm-ts/src/test/resources/reachability/InheritanceReachability.ts new file mode 100644 index 0000000000..4d3d4d0d70 --- /dev/null +++ b/usvm-ts/src/test/resources/reachability/InheritanceReachability.ts @@ -0,0 +1,145 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +/** + * Class inheritance and polymorphism reachability scenarios. + * Tests reachability through class hierarchies, method overriding, and inheritance patterns. + */ + +abstract class BaseClass { + protected value: number = 0; + + abstract process(): number; + + protected commonMethod(): number { + return this.value * 2; + } +} + +class ConcreteA extends BaseClass { + constructor(initialValue: number) { + super(); + this.value = initialValue; + } + + process(): number { + if (this.value > 10) { + return this.commonMethod(); // Call to parent method + } + return 0; + } + + specificMethodA(): number { + if (this.value === 15) { + return 1; // Reachable when value is exactly 15 + } + return 0; + } +} + +class ConcreteB extends BaseClass { + private multiplier: number = 3; + + constructor(initialValue: number, multiplier: number) { + super(); + this.value = initialValue; + this.multiplier = multiplier; + } + + process(): number { + const result = this.value * this.multiplier; + if (result > 50) { + return 1; // Reachable based on value and multiplier + } + return 0; + } + + // Override parent method with different implementation + commonMethod(): number { + return this.value * this.multiplier; + } +} + +class InheritanceReachability { + + // Conditional instantiation with different types + polymorphicCallReachable(useA: boolean, value: number): number { + let result: number; + + if (useA) { + const instanceA = new ConcreteA(value); + result = instanceA.process(); + } else { + const instanceB = new ConcreteB(value, 2); + result = instanceB.process(); + } + + if (result > 0) { + return 1; // Reachable through either path + } + return 0; + } + + // Type-specific method call + instanceofInheritanceReachable(value: number): number { + const obj = new ConcreteA(value); + + const specificResult = obj.specificMethodA(); + if (specificResult === 1) { + return 1; // Reachable when value is 15 + } + return 0; + } + + // Method overriding with different calculations + methodOverrideReachable(): number { + const objA = new ConcreteA(10); + const objB = new ConcreteB(10, 3); + + const resultA = objA.commonMethod(); // Uses base implementation: 10 * 2 = 20 + const resultB = objB.commonMethod(); // Uses overridden implementation: 10 * 3 = 30 + + if (resultA === 20 && resultB === 30) { + return 1; // Reachable with different method implementations + } + return 0; + } + + // Constructor with parameter passing + constructorChainingReachable(): number { + const obj = new ConcreteB(15, 4); + const processResult = obj.process(); // 15 * 4 = 60 > 50, returns 1 + + if (processResult === 1) { + return 1; // Reachable when constructor parameters lead to result > 50 + } + return 0; + } + + // Inheritance with protected field access + simpleInheritanceReachable(): number { + const obj = new ConcreteA(12); + + if (obj.value > 10) { // Access protected field from parent + const commonResult = obj.commonMethod(); // Call inherited method + if (commonResult === 24) { // 12 * 2 = 24 + return 1; // Reachable through inheritance + } + } + return 0; + } + + // Field access through inheritance hierarchy + fieldInheritanceReachable(): number { + const obj = new ConcreteB(8, 5); + + // Access inherited protected field + if (obj.value < 10) { + const result = obj.process(); // 8 * 5 = 40, not > 50 + if (result === 0) { + return 1; // Reachable when multiplication doesn't exceed threshold + } + } + return 0; + } +} diff --git a/usvm-ts/src/test/resources/reachability/LoopsReachability.ts b/usvm-ts/src/test/resources/reachability/LoopsReachability.ts new file mode 100644 index 0000000000..b6adf3435c --- /dev/null +++ b/usvm-ts/src/test/resources/reachability/LoopsReachability.ts @@ -0,0 +1,89 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +/** + * Loops and iteration reachability scenarios. + * Tests reachability through for loops, while loops, and loop control statements. + */ +class LoopsReachability { + + // For loop with reachable condition + forLoopReachable(limit: number): number { + for (let i = 0; i < limit; i++) { + if (i === 5) { + if (limit > 10) { + return 1; // Reachable when limit > 10 + } + } + } + return 0; + } + + // While loop with break condition + whileLoopBreakReachable(start: number): number { + let counter = start; + while (counter < 100) { + counter += 2; + if (counter === 20) { + break; + } + if (counter > 50) { + return 1; // Unreachable due to break at 20 + } + } + return 0; + } + + // Nested loops with continue + nestedLoopContinueReachable(): number { + for (let i = 0; i < 5; i++) { + for (let j = 0; j < 5; j++) { + if (i + j === 3) { + continue; + } + if (i === 2 && j === 3) { + return 1; // Reachable: 2 + 3 = 5, not equal to 3 + } + } + } + return 0; + } + + // For-in loop reachability + forInLoopReachable(): number { + const obj = { a: 1, b: 2, c: 3 }; + for (const key in obj) { + if (key === "b") { + if (obj[key] === 2) { + return 1; // Reachable when iterating over object + } + } + } + return 0; + } + + // For-of loop with array + forOfLoopReachable(): number { + const arr = [10, 20, 30, 40]; + for (const value of arr) { + if (value > 25) { + if (value < 35) { + return 1; // Reachable for value = 30 + } + } + } + return 0; + } + + // Do-while loop reachability + doWhileReachable(threshold: number): number { + let count = 0; + do { + count++; + if (count === threshold) { + return 1; // Always reachable at least once + } + } while (count < threshold); + return 0; + } +} diff --git a/usvm-ts/src/test/resources/reachability/RecursionReachability.ts b/usvm-ts/src/test/resources/reachability/RecursionReachability.ts new file mode 100644 index 0000000000..3259eb9017 --- /dev/null +++ b/usvm-ts/src/test/resources/reachability/RecursionReachability.ts @@ -0,0 +1,167 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +/** + * Recursion reachability scenarios. + * Tests reachability through recursive function calls with controlled depth limits. + */ +class RecursionReachability { + + // Recursive factorial with depth limit + factorial(n: number): number { + if (n <= 1) { + return 1; // Base case reachable + } + + if (n > 5) { + return -1; // Note: depth limit to prevent infinite loops + } + + return n * this.factorial(n - 1); // Recursive case with depth limit + } + + factorialReachable(input: number): number { + const result = this.factorial(input); + if (result === 24) { // 4! = 24 + return 1; // Reachable when input = 4 + } + return 0; + } + + // Tail recursion with accumulator + countdown(n: number, accumulator: number = 0): number { + if (n === 0) { + if (accumulator > 10) { + return 1; // Reachable when initial n leads to accumulator > 10 + } + return 0; + } + + if (n > 5) { + return 0; // Note: depth limit to prevent excessive recursion + } + + return this.countdown(n - 1, accumulator + n); + } + + // Mutual recursion with even/odd check + isEven(n: number): boolean { + if (n === 0) return true; + if (n === 1) return false; + if (n > 4) return false; // Note: depth limit + return this.isOdd(n - 1); + } + + isOdd(n: number): boolean { + if (n === 0) return false; + if (n === 1) return true; + if (n > 4) return true; // Note: depth limit + return this.isEven(n - 1); + } + + mutualRecursionReachable(input: number): number { + if (input > 0 && input < 5) { + const evenResult = this.isEven(input); + if (evenResult && input === 4) { + return 1; // Reachable for even number 4 + } + } + return 0; + } + + // Iterative fibonacci to avoid deep recursion + fibonacciIterative(n: number): number { + if (n <= 1) return n; + if (n > 10) return -1; + + let a = 0, b = 1; + for (let i = 2; i <= n; i++) { + const temp = a + b; + a = b; + b = temp; + } + + if (b === 13) { // fib(7) = 13 + return 1; // Special case + } + + return b; + } + + // Tree traversal using direct property access + treeTraversalReachable(target: number): number { + const treeNode = { + value: 10, + left: { value: 5 }, + right: { value: 15 }, + }; + + // Direct search without recursion + if (treeNode.value === target) { + return 1; // Reachable when root matches target (target = 10) + } + if (treeNode.left.value === target) { + return 2; // Reachable when left child matches target (target = 5) + } + if (treeNode.right.value === target) { + return 3; // Reachable when right child matches target (target = 15) + } + + return 0; + } + + // Simple recursive sum with depth control + sumToN(n: number): number { + if (n <= 0) { + return 0; // Base case + } + if (n > 5) { + return -1; // Note: depth limit + } + + return n + this.sumToN(n - 1); + } + + sumRecursionReachable(input: number): number { + const result = this.sumToN(input); + if (result === 15) { // sum(5) = 5+4+3+2+1 = 15 + return 1; // Reachable when input = 5 + } + return 0; + } + + // Binary search with depth control + binarySearchSimple(arr: number[], target: number, start: number = 0, end: number = -1): boolean { + if (end === -1) end = arr.length - 1; + + if (start > end) { + return false; // Base case: not found + } + + if (end - start > 8) { + return false; // Note: depth limit to prevent excessive recursion + } + + const mid = Math.floor((start + end) / 2); + + if (arr[mid] === target) { + return true; // Found + } + + if (arr[mid] > target) { + return this.binarySearchSimple(arr, target, start, mid - 1); + } else { + return this.binarySearchSimple(arr, target, mid + 1, end); + } + } + + binarySearchReachable(): number { + const sortedArray = [1, 3, 5, 7, 9, 11, 13, 15]; + const found = this.binarySearchSimple(sortedArray, 7); + + if (found) { + return 1; // Reachable when target 7 is found + } + return 0; + } +} diff --git a/usvm-ts/src/test/resources/reachability/TypeGuardsReachability.ts b/usvm-ts/src/test/resources/reachability/TypeGuardsReachability.ts new file mode 100644 index 0000000000..ad3f884a77 --- /dev/null +++ b/usvm-ts/src/test/resources/reachability/TypeGuardsReachability.ts @@ -0,0 +1,106 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +/** + * Type guards and assertions reachability scenarios. + * Tests reachability through typeof checks, instanceof operations, and user-defined type guards. + */ +class TypeGuardsReachability { + + // typeof type guard reachability + typeofGuardReachable(value: any): number { + if (typeof value === "string") { + // Note: string operations are limited to constant comparisons + if (value === "hello") { + return 1; // Reachable when value is exactly "hello" + } + } + return 0; + } + + // instanceof type guard reachability + instanceofGuardReachable(obj: any): number { + if (obj instanceof Array) { + if (obj.length === 3) { + return 1; // Reachable when obj is array with 3 elements + } + } + return 0; + } + + // User-defined type guard + isString(value: any): value is string { + return typeof value === "string"; + } + + userDefinedGuardReachable(input: any): number { + if (this.isString(input)) { + if (input === "test") { + return 1; // Reachable when input is exactly "test" + } + } + return 0; + } + + // Type assertion reachability + typeAssertionReachable(value: any): number { + const str = value as string; + if (str === "A") { + return 1; // Reachable when value is exactly "A" + } + return 0; + } + + // Non-null assertion reachability + nonNullAssertionReachable(value: string | null): number { + if (value !== null) { + const definiteString = value!; + if (definiteString === "nonempty") { + return 1; // Reachable when value is non-null "nonempty" + } + } + return 0; + } + + // Numeric type guard for better symbolic support + numericTypeGuardReachable(value: any): number { + if (typeof value === "number") { + if (value > 10) { + if (value < 20) { + return 1; // Reachable for numbers between 10 and 20 + } + } + } + return 0; + } + + // Boolean type guard reachability + booleanTypeGuardReachable(value: any): number { + if (typeof value === "boolean") { + if (value === true) { + return 1; // Reachable when value is boolean true + } + } + return 0; + } + + // Object type guard without null + objectTypeGuardReachable(value: any): number { + if (typeof value === "object" && value !== null) { + return 1; // Reachable for non-null objects + } + return 0; + } + + // Complex type guard combinations + complexTypeGuardReachable(value: any): number { + if (typeof value === "object" && value !== null) { + if (value instanceof Date) { + if (value.getFullYear() > 2020) { + return 1; // Reachable for dates after 2020 + } + } + } + return 0; + } +}