From a98730d5223750b3bc33e6db80a298c51b9a3bf4 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Thu, 4 Sep 2025 17:18:48 +0300 Subject: [PATCH 1/3] Add tests for targeted mode reachability analysis --- .../reachability/ArrayReachabilityTest.kt | 228 ++++++++++++++++++ .../BasicConditionsReachabilityTest.kt | 226 +++++++++++++++++ .../reachability/ComplexReachabilityTest.kt | 210 ++++++++++++++++ .../FieldAccessReachabilityTest.kt | 224 +++++++++++++++++ .../FunctionCallReachabilityTest.kt | 217 +++++++++++++++++ usvm-ts/src/test/kotlin/org/usvm/util/Util.kt | 12 +- .../reachability/ArrayReachability.ts | 128 ++++++++++ .../resources/reachability/BasicConditions.ts | 87 +++++++ .../reachability/ComplexReachability.ts | 217 +++++++++++++++++ .../reachability/FieldAccessReachability.ts | 118 +++++++++ .../reachability/FunctionCallReachability.ts | 173 +++++++++++++ 11 files changed, 1839 insertions(+), 1 deletion(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/reachability/ArrayReachabilityTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt create mode 100644 usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt create mode 100644 usvm-ts/src/test/resources/reachability/ArrayReachability.ts create mode 100644 usvm-ts/src/test/resources/reachability/BasicConditions.ts create mode 100644 usvm-ts/src/test/resources/reachability/ComplexReachability.ts create mode 100644 usvm-ts/src/test/resources/reachability/FieldAccessReachability.ts create mode 100644 usvm-ts/src/test/resources/reachability/FunctionCallReachability.ts diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/ArrayReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/ArrayReachabilityTest.kt new file mode 100644 index 0000000000..3eeb1192ea --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/ArrayReachabilityTest.kt @@ -0,0 +1,228 @@ +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.assertEquals +import kotlin.test.assertTrue +import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds + +/** + * Tests for array access reachability scenarios. + * Verifies reachability analysis through array element comparisons and operations. + */ +class ArrayReachabilityTest { + + private val scene = run { + val path = "/reachability/ArrayReachability.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 = 15.seconds, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + private val tsOptions = TsOptions() + + @Test + fun testSimpleArrayReachable() { + // Test reachability through array access: arr[0] === 10 -> arr[1] > 15 -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "simpleArrayReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (arr[0] === 10) + val firstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + + // if (arr[1] > 15) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for simple array reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } + + @Disabled("Extra exceptional path is found") + @Test + fun testArrayModificationReachable() { + // Test reachability after array modification: arr[index] = value -> arr[index] > 10 -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "arrayModificationReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (index >= 0 && index < 3) + val boundsCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(boundsCheck)) + + // if (arr[index] > 10) + val check = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(check)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for array modification reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } + + @Test + fun testArrayBoundsUnreachable() { + // Test unreachability due to array element constraints: arr[0] > 20 (when arr[0] = 5) + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "arrayBoundsUnreachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (arr[0] > 20) + val check = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(check)) + + // return -1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + + // In targeted mode, results may be non-empty as machine explores paths toward targets + // But the unreachable return statement should not be reached in any execution path + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt !in reachedStatements, + "Unreachable return statement was reached in execution path" + ) + } + + @Test + fun testArraySumReachable() { + // Test reachability through array sum calculation: sum === 30 -> arr[0] < arr[1] -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "arraySumReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (sum === 30) + val sumCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(sumCheck)) + + // if (arr[0] < arr[1]) + val comparison = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(comparison)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for array sum reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } + + @Disabled("Nested array access becomes field access") + @Test + fun testNestedArrayReachable() { + // Test reachability through nested array access: matrix[0][0] === 1 -> matrix[1][1] === 4 -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "nestedArrayReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (matrix[0][0] === 1) + val firstCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstCheck)) + + // if (matrix[1][1] === 4) + val secondCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for nested array reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt new file mode 100644 index 0000000000..4e76283f75 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt @@ -0,0 +1,226 @@ +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.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.assertEquals +import kotlin.test.assertTrue +import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds + +/** + * Tests for basic conditional reachability scenarios. + * Verifies reachability analysis for simple variable comparisons and branching. + */ +class BasicConditionsReachabilityTest { + + private val scene = run { + val path = "/reachability/BasicConditions.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 = 15.seconds, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + private val tsOptions = TsOptions() + + @Test + fun testSimpleReachablePath() { + // Test reachability of path: if (x > 10) -> if (x < 20) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "simpleReachablePath" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (x > 10) + val firstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + + // if (x < 20) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } + + @Test + fun testSimpleUnreachablePath() { + // Test unreachability of contradicting conditions: if (x > 15) -> if (x < 10) -> return -1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "simpleUnreachablePath" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (x > 15) + val firstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + + // if (x < 10) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + + // return -1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt !in reachedStatements, + "Unreachable return statement was reached in execution path" + ) + } + + @Test + fun testMultiVariableReachable() { + // Test reachability with multiple variables: if (x > 0) -> if (y > 5) -> if (x + y > 10) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "multiVariableReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (x > 0) + val firstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + + // if (y > 5) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + + // if (x + y > 10) + val thirdIf = method.cfg.stmts.filterIsInstance()[2] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(thirdIf)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for multi-variable reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } + + @Test + fun testEqualityBasedReachability() { + // Test reachability with equality: if (value === 42) -> if (value > 40) -> if (value < 50) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "equalityBasedReachability" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (value === 42) + val firstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + + // if (value > 40) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + + // if (value < 50) + val thirdIf = method.cfg.stmts.filterIsInstance()[2] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(thirdIf)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for equality-based reachable path, but got ${results.size}" + ) + } + + @Test + fun testBooleanUnreachable() { + // Test unreachability with contradicting boolean conditions: if (flag) -> if (!flag) -> return -1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "booleanUnreachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (flag) + val firstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + + // if (!flag) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + + // return -1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + + // In targeted mode, results may be non-empty as machine explores paths toward targets + // But the unreachable return statement should not be reached in any execution path + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt !in reachedStatements, + "Unreachable return statement was reached in execution path" + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt new file mode 100644 index 0000000000..49b0daee96 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt @@ -0,0 +1,210 @@ +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.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.assertEquals +import kotlin.test.assertTrue +import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds + +/** + * Tests for complex reachability scenarios combining multiple language constructions. + * Verifies reachability analysis through combinations of arrays, objects, method calls, and conditional logic. + */ +class ComplexReachabilityTest { + + private val scene = run { + val path = "/reachability/ComplexReachability.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 = 15.seconds, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + private val tsOptions = TsOptions() + + @Test + fun testArrayObjectCombinedReachable() { + // Test reachability combining array and object operations + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "arrayObjectCombinedReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (objects[0].value < objects[1].value) + val firstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + + // if (objects[2].value === 30) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for array-object combined reachable path, but got ${results.size}" + ) + } + + @Test + fun testMethodArrayManipulationReachable() { + // Test reachability through method calls with array manipulation + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "methodArrayManipulationReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (processedArr.length > 0) + val firstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + + // if (processedArr[0] > input) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for method array manipulation reachable path, but got ${results.size}" + ) + } + + @Test + fun testObjectMethodCallReachable() { + // Test reachability through object method calls affecting state + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "objectMethodCallReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (doubled === 30) + val firstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for object method call reachable path, but got ${results.size}" + ) + } + + @Test + fun testConditionalObjectReachable() { + // Test reachability with conditional object creation and polymorphic method calls + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "conditionalObjectReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (createExpensive) + val ifStatement = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(ifStatement)) + + // if (createExpensive && result > 200) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + + // return 1 + val return1 = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(return1)) + + // return 2 + val return2 = method.cfg.stmts.filterIsInstance()[1] + target.addChild(TsReachabilityTarget.FinalPoint(return2)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertTrue( + results.isNotEmpty(), + "Expected at least one result for conditional object reachable path, but got ${results.size}" + ) + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + return1 in reachedStatements, + "Expected 'return 1' statement to be reached in conditional object reachable path" + ) + } + + @Test + fun testCrossReferenceReachable() { + // Test reachability with cross-referenced objects forming a graph + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "crossReferenceReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (nodeA.connections.length === 1) + val lengthCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(lengthCheck)) + + // if (nodeA.connections[0].value === 2) + val connectionValueCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(connectionValueCheck)) + + // if (nodeA.connections[0].connections[0].value === 3) + val chainCheck = method.cfg.stmts.filterIsInstance()[2] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(chainCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for cross-reference reachable path, but got ${results.size}" + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt new file mode 100644 index 0000000000..bb6d9d5502 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt @@ -0,0 +1,224 @@ +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.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.assertEquals +import kotlin.test.assertTrue +import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds + +/** + * Tests for field access reachability scenarios. + * Verifies reachability analysis through object field comparisons and modifications. + */ +class FieldAccessReachabilityTest { + + private val scene = run { + val path = "/reachability/FieldAccessReachability.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 = 15.seconds, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + private val tsOptions = TsOptions() + + @Test + fun testSimpleFieldReachable() { + // Test reachability through field access: if (this.x > 0) -> if (this.y < 10) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "simpleFieldReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (this.x > 0) + val firstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + + // if (this.y < 10) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for field access reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } + + @Test + fun testFieldModificationReachable() { + // Test reachability after field modification: this.x = value -> if (this.x > 15) -> if (this.x < 25) -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "fieldModificationReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (this.x > 15) + val firstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + + // if (this.x < 25) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for field modification reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } + + @Test + fun testFieldConstraintUnreachable() { + // Test unreachability due to field constraints: this.x = 10 -> if (this.x > 20) -> return -1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "fieldConstraintUnreachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (this.x > 20) + val ifStmt = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(ifStmt)) + + // return -1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + + // In targeted mode, results may be non-empty as machine explores paths toward targets + // But the unreachable return statement should not be reached in any execution path + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt !in reachedStatements, + "Unreachable return statement was reached in execution path" + ) + } + + @Test + fun testObjectCreationReachable() { + // Test reachability through object creation and field access + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "objectCreationReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (obj.value === 42) + val firstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + + // if (obj.flag) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for object creation reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } + + @Test + fun testAmbiguousFieldAccess() { + // Test reachability with ambiguous field access (multiple classes with same field name) + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "ambiguousFieldAccess" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (useFirst) + val useFirstIf = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(useFirstIf)) + + // if (obj.commonField > 20) + val fieldCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(fieldCheck)) + + // 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 ambiguous field access, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt new file mode 100644 index 0000000000..3d27811de2 --- /dev/null +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt @@ -0,0 +1,217 @@ +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.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.assertEquals +import kotlin.test.assertTrue +import kotlin.time.Duration +import kotlin.time.Duration.Companion.seconds + +/** + * Tests for function call reachability scenarios. + * Verifies reachability analysis through method calls, return values, and call chains. + */ +class FunctionCallReachabilityTest { + + private val scene = run { + val path = "/reachability/FunctionCallReachability.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 = 15.seconds, + stepsFromLastCovered = 3500L, + solverType = SolverType.YICES, + solverTimeout = Duration.INFINITE, + typeOperationsTimeout = Duration.INFINITE, + ) + + private val tsOptions = TsOptions() + + @Test + fun testSimpleCallReachable() { + // Test reachability through method call: this.doubleValue(x) -> result > 20 -> result < 40 -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "simpleCallReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (result > 20) + val firstCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstCheck)) + + // if (result < 40) + val secondCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for simple call reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } + + @Test + fun testCallUnreachable() { + // Test unreachability due to method return constraints: constantValue() returns 42, check result > 100 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "callUnreachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (result > 100) + val check = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(check)) + + // return -1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + + // In targeted mode, results may be non-empty as machine explores paths toward targets + // But the unreachable return statement should not be reached in any execution path + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt !in reachedStatements, + "Unreachable return statement was reached in execution path" + ) + } + + @Test + fun testChainedCallsReachable() { + // Test reachability through chained method calls: addTen(doubleValue(x)) -> result === 30 -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "chainedCallsReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (result === 30) + val check = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(check)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for chained calls reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } + + @Test + fun testRecursiveCallReachable() { + // Test reachability through recursive call: factorial(n) -> result === 24 -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "recursiveCallReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (result === 24) + val check = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(check)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for recursive call reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } + + @Test + fun testStateModificationReachable() { + // Test reachability through state modification: incrementCounter(counter, 5) -> counter.value === 5 -> counter.value > 3 -> return 1 + val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) + val method = scene.projectClasses + .flatMap { it.methods } + .single { it.name == "stateModificationReachable" } + + val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first()) + var target: TsTarget = initialTarget + + // if (counter.value === 5) + val firstCheck = method.cfg.stmts.filterIsInstance()[0] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstCheck)) + + // if (counter.value > 3) + val secondCheck = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondCheck)) + + // return 1 + val returnStmt = method.cfg.stmts.filterIsInstance()[0] + target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) + + val results = machine.analyze(listOf(method), listOf(initialTarget)) + assertEquals( + 1, + results.size, + "Expected exactly one result for state modification reachable path, but got ${results.size}" + ) + + val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() + assertTrue( + returnStmt in reachedStatements, + "Expected return statement to be reached in execution path" + ) + } +} diff --git a/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt index a8b6b12321..cc6824b75a 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/util/Util.kt @@ -1,8 +1,9 @@ package org.usvm.util +import org.usvm.api.TsTestValue.TsBoolean import org.usvm.api.TsTestValue.TsNumber import org.usvm.api.TsTestValue.TsString -import org.usvm.api.TsTestValue.TsBoolean +import org.usvm.targets.UTarget import kotlin.math.absoluteValue fun Boolean.toDouble() = if (this) 1.0 else 0.0 @@ -74,3 +75,12 @@ infix fun TsBoolean.eq(other: TsBoolean): Boolean { infix fun TsBoolean.neq(other: TsBoolean): Boolean { return neq(other.value) } + +fun UTarget<*, T>.getRoot(): T where T : UTarget<*, T> { + var current = this + while (true) { + @Suppress("UNCHECKED_CAST") + val parent = current.parent ?: return current as T + current = parent + } +} diff --git a/usvm-ts/src/test/resources/reachability/ArrayReachability.ts b/usvm-ts/src/test/resources/reachability/ArrayReachability.ts new file mode 100644 index 0000000000..ebef992ab8 --- /dev/null +++ b/usvm-ts/src/test/resources/reachability/ArrayReachability.ts @@ -0,0 +1,128 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +/** + * Array access and manipulation reachability scenarios. + * Tests reachability through array element comparisons and operations. + */ +class ArrayReachability { + + // Simple array element access reachability + simpleArrayReachable(): number { + const arr = [10, 20, 30]; + if (arr[0] === 10) { + if (arr[1] > 15) { + return 1; // Reachable: arr[0] is 10 and arr[1] is 20 > 15 + } + } + return 0; + } + + // Array modification reachability + arrayModificationReachable(index: number, value: number): number { + const arr = [1, 2, 3]; + if (index >= 0 && index < 3) { + arr[index] = value; + if (arr[index] > 10) { + return 1; // Reachable when value > 10 + } + } + return 0; + } + + // Unreachable due to array bounds + arrayBoundsUnreachable(): number { + const arr = [5, 10, 15]; + if (arr[0] > 20) { + return -1; // Unreachable: arr[0] is 5, cannot be > 20 + } + return 0; + } + + // Dynamic array creation and access + dynamicArrayReachable(size: number): number { + if (size > 0 && size < 10) { + const arr = new Array(size); + arr[0] = 42; + if (arr[0] === 42) { + if (arr.length === size) { + return 1; // Reachable when 0 < size < 10 + } + } + } + return 0; + } + + // Array element comparison reachability + arrayComparisonReachable(): number { + const arr1 = [10, 20]; + const arr2 = [15, 25]; + + if (arr1[0] < arr2[0]) { + if (arr1[1] < arr2[1]) { + return 1; // Reachable: 10 < 15 and 20 < 25 + } + } + return 0; + } + + // Array sum condition reachability + arraySumReachable(): number { + const arr = [5, 10, 15]; + const sum = arr[0] + arr[1] + arr[2]; + + if (sum === 30) { + if (arr[0] < arr[1]) { + return 1; // Reachable: sum is 30 and 5 < 10 + } + } + return 0; + } + + // Nested array access + nestedArrayReachable(): number { + const matrix = [[1, 2], [3, 4]]; + if (matrix[0][0] === 1) { + if (matrix[1][1] === 4) { + return 1; // Reachable: matrix[0][0] is 1 and matrix[1][1] is 4 + } + } + return 0; + } + + // Array with object elements + arrayObjectReachable(): number { + const objects = [ + new ArrayElement(10), + new ArrayElement(20), + ]; + + if (objects[0].value < objects[1].value) { + if (objects[0].value + objects[1].value === 30) { + return 1; // Reachable: 10 < 20 and 10 + 20 = 30 + } + } + return 0; + } + + // Array length-based conditions + arrayLengthReachable(arr: number[]): number { + if (arr.length > 2) { + if (arr[0] > 0) { + if (arr[arr.length - 1] > arr[0]) { + return 1; // Reachable with appropriate array + } + } + } + return 0; + } +} + +// Helper class for array tests +class ArrayElement { + value: number; + + constructor(val: number) { + this.value = val; + } +} diff --git a/usvm-ts/src/test/resources/reachability/BasicConditions.ts b/usvm-ts/src/test/resources/reachability/BasicConditions.ts new file mode 100644 index 0000000000..fa81653ab9 --- /dev/null +++ b/usvm-ts/src/test/resources/reachability/BasicConditions.ts @@ -0,0 +1,87 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +/** + * Basic conditional reachability samples covering simple variable comparisons + * and branching scenarios for reachability analysis. + */ +class BasicConditions { + + // Simple reachable path: condition can be satisfied + simpleReachablePath(x: number): number { + if (x > 10) { + if (x < 20) { + return 1; // Reachable when 10 < x < 20 + } + } + return 0; + } + + // Simple unreachable path: contradicting conditions + simpleUnreachablePath(x: number): number { + if (x > 15) { + if (x < 10) { + return -1; // Unreachable: x cannot be both > 15 and < 10 + } + } + return 0; + } + + // Multiple variables with reachable path + multiVariableReachable(x: number, y: number): number { + if (x > 0) { + if (y > 5) { + if (x + y > 10) { + return 1; // Reachable with appropriate x, y values + } + } + } + return 0; + } + + // Multiple variables with unreachable path + multiVariableUnreachable(x: number, y: number): number { + if (x > 0) { + if (y > 0) { + if (x + y < 0) { + return -1; // Unreachable: x > 0 and y > 0 means x + y > 0 + } + } + } + return 0; + } + + // Nested conditions with equality checks + equalityBasedReachability(value: number): number { + if (value === 42) { + if (value > 40) { + if (value < 50) { + return 1; // Reachable when value is exactly 42 + } + } + } + return 0; + } + + // Boolean variable conditions + booleanConditions(flag1: boolean, flag2: boolean): number { + if (flag1) { + if (!flag2) { + if (flag1 && !flag2) { + return 1; // Reachable when flag1 is true and flag2 is false + } + } + } + return 0; + } + + // Complex boolean unreachable condition + booleanUnreachable(flag: boolean): number { + if (flag) { + if (!flag) { + return -1; // Unreachable: flag cannot be both true and false + } + } + return 0; + } +} diff --git a/usvm-ts/src/test/resources/reachability/ComplexReachability.ts b/usvm-ts/src/test/resources/reachability/ComplexReachability.ts new file mode 100644 index 0000000000..2ef75448c7 --- /dev/null +++ b/usvm-ts/src/test/resources/reachability/ComplexReachability.ts @@ -0,0 +1,217 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +/** + * Complex reachability scenarios combining multiple language constructions: + * arrays, objects, method calls, and conditional logic. + */ +class ComplexReachability { + + // Combined array and object field access + arrayObjectCombinedReachable(): number { + const objects = [ + new DataHolder(10), + new DataHolder(20), + new DataHolder(30), + ]; + + if (objects[0].value < objects[1].value) { + objects[2].value = objects[0].value + objects[1].value; + if (objects[2].value === 30) { + return 1; // Reachable: 10 < 20, then objects[2].value = 10 + 20 = 30 + } + } + return 0; + } + + // Method calls with array manipulation + methodArrayManipulationReachable(input: number): number { + const arr = this.createNumberArray(input); + const processedArr = this.processArray(arr); + + if (processedArr.length > 0) { + if (processedArr[0] > input) { + return 1; // Reachable depending on input value + } + } + return 0; + } + + // Object method calls affecting reachability + objectMethodCallReachable(): number { + const calculator = new Calculator(); + calculator.setValue(15); + + const doubled = calculator.getDoubled(); + if (doubled === 30) { + calculator.add(10); + if (calculator.getValue() === 40) { + return 1; // Reachable: 15 * 2 = 30, then 15 + 10 = 25, but getValue() returns current value + } + } + return 0; + } + + // Nested object and array access with method calls + nestedComplexReachable(): number { + const container = new ArrayContainer(); + container.numbers = [5, 10, 15]; + container.processor = new NumberProcessor(); + + const result = container.processor.processNumbers(container.numbers); + if (result > 25) { + if (container.numbers[1] === 10) { + return 1; // Reachable: sum of [5,10,15] is 30 > 25, and numbers[1] is 10 + } + } + return 0; + } + + // Loop-based reachability with early termination + loopBasedReachable(limit: number): number { + const results = []; + for (let i = 0; i < limit && i < 10; i++) { + const computed = this.computeValue(i); + results.push(computed); + + if (computed > 50) { + if (results.length > 2) { + return 1; // Reachable when we find a value > 50 after at least 2 iterations + } + } + } + return 0; + } + + // Conditional object creation and method chaining + conditionalObjectReachable(createExpensive: boolean): number { + let processor: any; + + if (createExpensive) { + processor = new ExpensiveProcessor(); + } else { + processor = new SimpleProcessor(); + } + + const result = processor.process(100); + if (createExpensive && result === 200) { + return 1; // Reachable when createExpensive is true and ExpensiveProcessor doubles the input + } + + if (!createExpensive && result === 100) { + return 2; // Reachable when createExpensive is false and SimpleProcessor returns input unchanged + } + + return 0; + } + + // Array of objects with cross-references + crossReferenceReachable(): number { + const nodeA = new GraphNode(1); + const nodeB = new GraphNode(2); + const nodeC = new GraphNode(3); + + nodeA.addConnection(nodeB); + nodeB.addConnection(nodeC); + nodeC.addConnection(nodeA); + + if (nodeA.connections.length === 1) { + if (nodeA.connections[0].value === 2) { + if (nodeA.connections[0].connections[0].value === 3) { + return 1; // Reachable: A->B, B->C, verify the chain + } + } + } + return 0; + } + + // Helper methods + createNumberArray(size: number): number[] { + const arr = []; + for (let i = 0; i < size && i < 5; i++) { + arr.push(i * 2); + } + return arr; + } + + processArray(arr: number[]): number[] { + const result = []; + for (let i = 0; i < arr.length; i++) { + result.push(arr[i] + 1); + } + return result; + } + + computeValue(input: number): number { + return input * input + input * 10; + } +} + +// Helper classes for complex tests +class DataHolder { + value: number; + + constructor(val: number) { + this.value = val; + } +} + +class Calculator { + private currentValue: number = 0; + + setValue(val: number): void { + this.currentValue = val; + } + + getValue(): number { + return this.currentValue; + } + + getDoubled(): number { + return this.currentValue * 2; + } + + add(val: number): void { + this.currentValue += val; + } +} + +class ArrayContainer { + numbers: number[]; + processor: NumberProcessor; +} + +class NumberProcessor { + processNumbers(arr: number[]): number { + let sum = 0; + for (let i = 0; i < arr.length; i++) { + sum += arr[i]; + } + return sum; + } +} + +class SimpleProcessor { + process(input: number): number { + return input; + } +} + +class ExpensiveProcessor { + process(input: number): number { + return input * 2; + } +} + +class GraphNode { + value: number; + connections: GraphNode[] = []; + + constructor(val: number) { + this.value = val; + } + + addConnection(node: GraphNode): void { + this.connections.push(node); + } +} diff --git a/usvm-ts/src/test/resources/reachability/FieldAccessReachability.ts b/usvm-ts/src/test/resources/reachability/FieldAccessReachability.ts new file mode 100644 index 0000000000..3e2574e901 --- /dev/null +++ b/usvm-ts/src/test/resources/reachability/FieldAccessReachability.ts @@ -0,0 +1,118 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +/** + * Field access and object-based reachability scenarios. + * Tests reachability through object field comparisons and modifications. + */ +class FieldAccessReachability { + x: number = 0; + y: number = 5; + + // Simple field access reachability + simpleFieldReachable(): number { + if (this.x > 0) { + if (this.y < 10) { + return 1; // Reachable when x > 0 and y < 10 + } + } + return 0; + } + + // Field modification affecting reachability + fieldModificationReachable(value: number): number { + this.x = value; + if (this.x > 15) { + if (this.x < 25) { + return 1; // Reachable when 15 < value < 25 + } + } + return 0; + } + + // Unreachable due to field constraints + fieldConstraintUnreachable(): number { + this.x = 10; + if (this.x > 20) { + return -1; // Unreachable: x is set to 10, cannot be > 20 + } + return 0; + } + + // Object creation and field access + objectCreationReachable(): number { + const obj = new SimpleDataClass(); + obj.value = 42; + if (obj.value === 42) { + if (obj.flag) { + return 1; // Reachable if flag is true + } + } + return 0; + } + + // Multiple object field access + multipleObjectFields(): number { + const obj1 = new SimpleDataClass(); + const obj2 = new SimpleDataClass(); + obj1.value = 10; + obj2.value = 20; + + if (obj1.value < obj2.value) { + if (obj1.value + obj2.value === 30) { + return 1; // Reachable: 10 < 20 and 10 + 20 = 30 + } + } + return 0; + } + + // Field access chain reachability + fieldChainReachable(): number { + const container = new ContainerClass(); + container.data = new SimpleDataClass(); + container.data.value = 100; + + if (container.data.value > 50) { + if (container.data.value < 150) { + return 1; // Reachable when 50 < value < 150 + } + } + return 0; + } + + // Ambiguous field access (multiple classes with same field name) + ambiguousFieldAccess(useFirst: boolean): number { + let obj: any; + if (useFirst) { + obj = new ClassA(); + } else { + obj = new ClassB(); + } + + obj.commonField = 25; + if (obj.commonField > 20) { + return 1; // Reachable in both branches + } + return 0; + } +} + +// Helper classes for field access tests +class SimpleDataClass { + value: number = 0; + flag: boolean = true; +} + +class ContainerClass { + data: SimpleDataClass; +} + +class ClassA { + commonField: number = 0; + uniqueA: number = 1; +} + +class ClassB { + commonField: number = 0; + uniqueB: number = 2; +} diff --git a/usvm-ts/src/test/resources/reachability/FunctionCallReachability.ts b/usvm-ts/src/test/resources/reachability/FunctionCallReachability.ts new file mode 100644 index 0000000000..815d34d8cc --- /dev/null +++ b/usvm-ts/src/test/resources/reachability/FunctionCallReachability.ts @@ -0,0 +1,173 @@ +// @ts-nocheck +// noinspection JSUnusedGlobalSymbols + +/** + * Function call reachability scenarios. + * Tests reachability through method calls, return values, and call chains. + */ +class FunctionCallReachability { + + // Simple method call reachability + simpleCallReachable(x: number): number { + const result = this.doubleValue(x); + if (result > 20) { + if (result < 40) { + return 1; // Reachable when 10 < x < 20 (since result = 2*x) + } + } + return 0; + } + + // Method call with unreachable path + callUnreachable(): number { + const result = this.constantValue(); + if (result > 100) { + return -1; // Unreachable: constantValue() returns 42, not > 100 + } + return 0; + } + + // Chained method calls + chainedCallsReachable(x: number): number { + const result = this.addTen(this.doubleValue(x)); + if (result === 30) { + return 1; // Reachable when x = 10: double(10) = 20, addTen(20) = 30 + } + return 0; + } + + // Conditional method calls + conditionalCallReachable(useFirst: boolean, x: number): number { + let result: number; + if (useFirst) { + result = this.doubleValue(x); + } else { + result = this.tripleValue(x); + } + + if (result === 30) { + return 1; // Reachable: x=15 with useFirst=true, or x=10 with useFirst=false + } + return 0; + } + + // Recursive call reachability + recursiveCallReachable(n: number): number { + const result = this.factorial(n); + if (result === 24) { + return 1; // Reachable when n = 4 (4! = 24) + } + return 0; + } + + // Method call affecting object state + stateModificationReachable(): number { + const counter = new Counter(); + this.incrementCounter(counter, 5); + + if (counter.value === 5) { + if (counter.value > 3) { + return 1; // Reachable: counter starts at 0, incremented by 5 + } + } + return 0; + } + + // Method with side effects on multiple objects + multiObjectCallReachable(): number { + const obj1 = new SimpleCounter(); + const obj2 = new SimpleCounter(); + + this.crossIncrement(obj1, obj2, 10); + + if (obj1.count === 10) { + if (obj2.count === 10) { + return 1; // Reachable: both objects get incremented by 10 + } + } + return 0; + } + + // Static method call reachability + staticCallReachable(x: number, y: number): number { + const result = MathUtils.add(x, y); + if (result > 50) { + if (result < 100) { + return 1; // Reachable with appropriate x, y values + } + } + return 0; + } + + // Method call with array parameter + arrayParameterCallReachable(): number { + const arr = [1, 2, 3, 4, 5]; + const sum = this.calculateSum(arr); + + if (sum === 15) { + if (arr.length === 5) { + return 1; // Reachable: sum of [1,2,3,4,5] is 15 + } + } + return 0; + } + + // Helper methods for testing + doubleValue(x: number): number { + return x * 2; + } + + tripleValue(x: number): number { + return x * 3; + } + + constantValue(): number { + return 42; + } + + addTen(x: number): number { + return x + 10; + } + + factorial(n: number): number { + if (n <= 1) return 1; + if (n > 10) return -1; // Prevent infinite recursion in tests + return n * this.factorial(n - 1); + } + + incrementCounter(counter: Counter, amount: number): void { + counter.value += amount; + } + + crossIncrement(obj1: SimpleCounter, obj2: SimpleCounter, amount: number): void { + obj1.count += amount; + obj2.count += amount; + } + + calculateSum(arr: number[]): number { + let sum = 0; + for (let i = 0; i < arr.length; i++) { + sum += arr[i]; + } + return sum; + } +} + +// Helper classes for function call tests +class Counter { + value: number = 0; +} + +class SimpleCounter { + count: number = 0; +} + +class MathUtils { + static add(a: number, b: number): number { + return a + b; + } + + static multiply(a: number, b: number): number { + return a * b; + } +} From 4395c14a58309c9e20e7e4e9fcc94be79d452e6b Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 8 Sep 2025 16:42:39 +0300 Subject: [PATCH 2/3] Wrap long lines --- .../reachability/FunctionCallReachabilityTest.kt | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) 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 3d27811de2..7cdc3a4c63 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt @@ -47,7 +47,8 @@ class FunctionCallReachabilityTest { @Test fun testSimpleCallReachable() { - // Test reachability through method call: this.doubleValue(x) -> result > 20 -> result < 40 -> return 1 + // Test reachability through method call: + // this.doubleValue(x) -> result > 20 -> result < 40 -> return 1 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } @@ -84,7 +85,8 @@ class FunctionCallReachabilityTest { @Test fun testCallUnreachable() { - // Test unreachability due to method return constraints: constantValue() returns 42, check result > 100 + // Test unreachability due to method return constraints: + // constantValue() returns 42 -> result > 100 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } @@ -114,7 +116,8 @@ class FunctionCallReachabilityTest { @Test fun testChainedCallsReachable() { - // Test reachability through chained method calls: addTen(doubleValue(x)) -> result === 30 -> return 1 + // Test reachability through chained method calls: + // addTen(doubleValue(x)) -> result === 30 -> return 1 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } @@ -147,7 +150,8 @@ class FunctionCallReachabilityTest { @Test fun testRecursiveCallReachable() { - // Test reachability through recursive call: factorial(n) -> result === 24 -> return 1 + // Test reachability through recursive call: + // factorial(n) -> result === 24 -> return 1 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } @@ -180,7 +184,8 @@ class FunctionCallReachabilityTest { @Test fun testStateModificationReachable() { - // Test reachability through state modification: incrementCounter(counter, 5) -> counter.value === 5 -> counter.value > 3 -> return 1 + // Test reachability through state modification: + // incrementCounter(counter, 5) -> counter.value === 5 -> counter.value > 3 -> return 1 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } From 994a7454568336078bb12c976f77e853b91d081e Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Mon, 8 Sep 2025 17:35:20 +0300 Subject: [PATCH 3/3] Wrap long lines --- .../BasicConditionsReachabilityTest.kt | 15 ++++++++++----- .../reachability/FieldAccessReachabilityTest.kt | 9 ++++++--- 2 files changed, 16 insertions(+), 8 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt index 4e76283f75..b8d949da58 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt @@ -47,7 +47,8 @@ class BasicConditionsReachabilityTest { @Test fun testSimpleReachablePath() { - // Test reachability of path: if (x > 10) -> if (x < 20) -> return 1 + // Test reachability of path: + // if (x > 10) -> if (x < 20) -> return 1 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } @@ -84,7 +85,8 @@ class BasicConditionsReachabilityTest { @Test fun testSimpleUnreachablePath() { - // Test unreachability of contradicting conditions: if (x > 15) -> if (x < 10) -> return -1 + // Test unreachability of contradicting conditions: + // if (x > 15) -> if (x < 10) -> return -1 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } @@ -116,7 +118,8 @@ class BasicConditionsReachabilityTest { @Test fun testMultiVariableReachable() { - // Test reachability with multiple variables: if (x > 0) -> if (y > 5) -> if (x + y > 10) -> return 1 + // Test reachability with multiple variables: + // if (x > 0) -> if (y > 5) -> if (x + y > 10) -> return 1 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } @@ -157,7 +160,8 @@ class BasicConditionsReachabilityTest { @Test fun testEqualityBasedReachability() { - // Test reachability with equality: if (value === 42) -> if (value > 40) -> if (value < 50) -> return 1 + // Test reachability with equality: + // if (value === 42) -> if (value > 40) -> if (value < 50) -> return 1 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } @@ -192,7 +196,8 @@ class BasicConditionsReachabilityTest { @Test fun testBooleanUnreachable() { - // Test unreachability with contradicting boolean conditions: if (flag) -> if (!flag) -> return -1 + // Test unreachability with contradicting boolean conditions: + // if (flag) -> if (!flag) -> return -1 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt index bb6d9d5502..38db366450 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt @@ -47,7 +47,8 @@ class FieldAccessReachabilityTest { @Test fun testSimpleFieldReachable() { - // Test reachability through field access: if (this.x > 0) -> if (this.y < 10) -> return 1 + // Test reachability through field access: + // if (this.x > 0) -> if (this.y < 10) -> return 1 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } @@ -84,7 +85,8 @@ class FieldAccessReachabilityTest { @Test fun testFieldModificationReachable() { - // Test reachability after field modification: this.x = value -> if (this.x > 15) -> if (this.x < 25) -> return 1 + // Test reachability after field modification: + // this.x = value -> if (this.x > 15) -> if (this.x < 25) -> return 1 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods } @@ -121,7 +123,8 @@ class FieldAccessReachabilityTest { @Test fun testFieldConstraintUnreachable() { - // Test unreachability due to field constraints: this.x = 10 -> if (this.x > 20) -> return -1 + // Test unreachability due to field constraints: + // this.x = 10 -> if (this.x > 20) -> return -1 val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver()) val method = scene.projectClasses .flatMap { it.methods }