Skip to content

Commit 3ad7a15

Browse files
committed
Fix test with tree structure traversal
1 parent 9e69ace commit 3ad7a15

File tree

2 files changed

+52
-21
lines changed

2 files changed

+52
-21
lines changed

usvm-ts/src/test/kotlin/org/usvm/reachability/RecursionReachabilityTest.kt

Lines changed: 41 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -234,19 +234,44 @@ class RecursionReachabilityTest {
234234

235235
@Test
236236
fun testTreeTraversalReachable() {
237-
// Test reachability through simplified tree traversal (no actual recursion):
238-
// direct property access -> if (found target 15) -> return 1
237+
// Test reachability through simplified tree traversal with parameterized target:
238+
// if (treeNode.value === target) -> return 1 (reachable when target = 10)
239+
// if (treeNode.left.value === target) -> return 2 (reachable when target = 5)
240+
// if (treeNode.right.value === target) -> return 3 (reachable when target = 15)
239241
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
240242
val method = scene.projectClasses
241243
.flatMap { it.methods }
242244
.single { it.name == "treeTraversalReachable" }
243245

244246
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
245-
var target: TsTarget = initialTarget
246247

247-
// The method uses direct property access, so focus on final return
248-
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
249-
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
248+
// Path 1:
249+
// if (treeNode.value === target)
250+
// return 1
251+
val ifStmt1 = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
252+
val returnStmt1 = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
253+
254+
initialTarget
255+
.addChild(TsReachabilityTarget.IntermediatePoint(ifStmt1))
256+
.addChild(TsReachabilityTarget.FinalPoint(returnStmt1))
257+
258+
// Path 2:
259+
// if (treeNode.left.value === target)
260+
// return 2
261+
val ifStmt2 = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
262+
val returnStmt2 = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[1]
263+
initialTarget
264+
.addChild(TsReachabilityTarget.IntermediatePoint(ifStmt2))
265+
.addChild(TsReachabilityTarget.FinalPoint(returnStmt2))
266+
267+
// Path 3:
268+
// if (treeNode.right.value === target)
269+
// return 3
270+
val ifStmt3 = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[2]
271+
val returnStmt3 = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[2]
272+
initialTarget
273+
.addChild(TsReachabilityTarget.IntermediatePoint(ifStmt3))
274+
.addChild(TsReachabilityTarget.FinalPoint(returnStmt3))
250275

251276
val results = machine.analyze(listOf(method), listOf(initialTarget))
252277
assertTrue(
@@ -256,8 +281,16 @@ class RecursionReachabilityTest {
256281

257282
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
258283
assertTrue(
259-
returnStmt in reachedStatements,
260-
"Expected return statement to be reached when value 15 exists in tree"
284+
returnStmt1 in reachedStatements,
285+
"Expected 'return 1' to be reached when target = 10"
286+
)
287+
assertTrue(
288+
returnStmt2 in reachedStatements,
289+
"Expected 'return 2' to be reached when target = 5"
290+
)
291+
assertTrue(
292+
returnStmt3 in reachedStatements,
293+
"Expected 'return 3' to be reached when target = 15"
261294
)
262295
}
263296

usvm-ts/src/test/resources/reachability/RecursionReachability.ts

Lines changed: 11 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -12,11 +12,11 @@ class RecursionReachability {
1212
if (n <= 1) {
1313
return 1; // Base case reachable
1414
}
15-
15+
1616
if (n > 5) {
1717
return -1; // Note: depth limit to prevent infinite loops
1818
}
19-
19+
2020
return n * this.factorial(n - 1); // Recursive case with depth limit
2121
}
2222

@@ -36,7 +36,7 @@ class RecursionReachability {
3636
}
3737
return 0;
3838
}
39-
39+
4040
if (n > 5) {
4141
return 0; // Note: depth limit to prevent excessive recursion
4242
}
@@ -84,29 +84,27 @@ class RecursionReachability {
8484
if (b === 13) { // fib(7) = 13
8585
return 1; // Special case
8686
}
87-
87+
8888
return b;
8989
}
9090

9191
// Tree traversal using direct property access
92-
treeTraversalReachable(): number {
92+
treeTraversalReachable(target: number): number {
9393
const treeNode = {
9494
value: 10,
9595
left: { value: 5 },
96-
right: { value: 15 }
96+
right: { value: 15 },
9797
};
9898

99-
const target = 15;
100-
10199
// Direct search without recursion
102100
if (treeNode.value === target) {
103-
return 1;
101+
return 1; // Reachable when root matches target (target = 10)
104102
}
105-
if (treeNode.left && treeNode.left.value === target) {
106-
return 1;
103+
if (treeNode.left.value === target) {
104+
return 2; // Reachable when left child matches target (target = 5)
107105
}
108-
if (treeNode.right && treeNode.right.value === target) {
109-
return 1; // Reachable: 15 exists in the tree
106+
if (treeNode.right.value === target) {
107+
return 3; // Reachable when right child matches target (target = 15)
110108
}
111109

112110
return 0;

0 commit comments

Comments
 (0)