Skip to content

Commit 7354d9f

Browse files
LipenLipen
authored
[TS] Reachability analysis (#331)
1 parent 5f0b67f commit 7354d9f

File tree

11 files changed

+1852
-1
lines changed

11 files changed

+1852
-1
lines changed

‎usvm-ts/src/test/kotlin/org/usvm/reachability/ArrayReachabilityTest.kt‎

Lines changed: 228 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,228 @@
1+
package org.usvm.reachability
2+
3+
import org.jacodb.ets.model.EtsIfStmt
4+
import org.jacodb.ets.model.EtsReturnStmt
5+
import org.jacodb.ets.model.EtsScene
6+
import org.jacodb.ets.utils.loadEtsFileAutoConvert
7+
import org.junit.jupiter.api.Disabled
8+
import org.usvm.PathSelectionStrategy
9+
import org.usvm.SolverType
10+
import org.usvm.UMachineOptions
11+
import org.usvm.api.targets.ReachabilityObserver
12+
import org.usvm.api.targets.TsReachabilityTarget
13+
import org.usvm.api.targets.TsTarget
14+
import org.usvm.machine.TsMachine
15+
import org.usvm.machine.TsOptions
16+
import org.usvm.util.getResourcePath
17+
import kotlin.test.Test
18+
import kotlin.test.assertEquals
19+
import kotlin.test.assertTrue
20+
import kotlin.time.Duration
21+
import kotlin.time.Duration.Companion.seconds
22+
23+
/**
24+
* Tests for array access reachability scenarios.
25+
* Verifies reachability analysis through array element comparisons and operations.
26+
*/
27+
class ArrayReachabilityTest {
28+
29+
private val scene = run {
30+
val path = "/reachability/ArrayReachability.ts"
31+
val res = getResourcePath(path)
32+
val file = loadEtsFileAutoConvert(res)
33+
EtsScene(listOf(file))
34+
}
35+
36+
private val options = UMachineOptions(
37+
pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
38+
exceptionsPropagation = true,
39+
stopOnTargetsReached = true,
40+
timeout = 15.seconds,
41+
stepsFromLastCovered = 3500L,
42+
solverType = SolverType.YICES,
43+
solverTimeout = Duration.INFINITE,
44+
typeOperationsTimeout = Duration.INFINITE,
45+
)
46+
47+
private val tsOptions = TsOptions()
48+
49+
@Test
50+
fun testSimpleArrayReachable() {
51+
// Test reachability through array access: arr[0] === 10 -> arr[1] > 15 -> return 1
52+
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
53+
val method = scene.projectClasses
54+
.flatMap { it.methods }
55+
.single { it.name == "simpleArrayReachable" }
56+
57+
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
58+
var target: TsTarget = initialTarget
59+
60+
// if (arr[0] === 10)
61+
val firstIf = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
62+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf))
63+
64+
// if (arr[1] > 15)
65+
val secondIf = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
66+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf))
67+
68+
// return 1
69+
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
70+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
71+
72+
val results = machine.analyze(listOf(method), listOf(initialTarget))
73+
assertEquals(
74+
1,
75+
results.size,
76+
"Expected exactly one result for simple array reachable path, but got ${results.size}"
77+
)
78+
79+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
80+
assertTrue(
81+
returnStmt in reachedStatements,
82+
"Expected return statement to be reached in execution path"
83+
)
84+
}
85+
86+
@Disabled("Extra exceptional path is found")
87+
@Test
88+
fun testArrayModificationReachable() {
89+
// Test reachability after array modification: arr[index] = value -> arr[index] > 10 -> return 1
90+
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
91+
val method = scene.projectClasses
92+
.flatMap { it.methods }
93+
.single { it.name == "arrayModificationReachable" }
94+
95+
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
96+
var target: TsTarget = initialTarget
97+
98+
// if (index >= 0 && index < 3)
99+
val boundsCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
100+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(boundsCheck))
101+
102+
// if (arr[index] > 10)
103+
val check = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
104+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(check))
105+
106+
// return 1
107+
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
108+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
109+
110+
val results = machine.analyze(listOf(method), listOf(initialTarget))
111+
assertEquals(
112+
1,
113+
results.size,
114+
"Expected exactly one result for array modification reachable path, but got ${results.size}"
115+
)
116+
117+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
118+
assertTrue(
119+
returnStmt in reachedStatements,
120+
"Expected return statement to be reached in execution path"
121+
)
122+
}
123+
124+
@Test
125+
fun testArrayBoundsUnreachable() {
126+
// Test unreachability due to array element constraints: arr[0] > 20 (when arr[0] = 5)
127+
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
128+
val method = scene.projectClasses
129+
.flatMap { it.methods }
130+
.single { it.name == "arrayBoundsUnreachable" }
131+
132+
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
133+
var target: TsTarget = initialTarget
134+
135+
// if (arr[0] > 20)
136+
val check = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
137+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(check))
138+
139+
// return -1
140+
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
141+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
142+
143+
val results = machine.analyze(listOf(method), listOf(initialTarget))
144+
145+
// In targeted mode, results may be non-empty as machine explores paths toward targets
146+
// But the unreachable return statement should not be reached in any execution path
147+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
148+
assertTrue(
149+
returnStmt !in reachedStatements,
150+
"Unreachable return statement was reached in execution path"
151+
)
152+
}
153+
154+
@Test
155+
fun testArraySumReachable() {
156+
// Test reachability through array sum calculation: sum === 30 -> arr[0] < arr[1] -> return 1
157+
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
158+
val method = scene.projectClasses
159+
.flatMap { it.methods }
160+
.single { it.name == "arraySumReachable" }
161+
162+
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
163+
var target: TsTarget = initialTarget
164+
165+
// if (sum === 30)
166+
val sumCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
167+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(sumCheck))
168+
169+
// if (arr[0] < arr[1])
170+
val comparison = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
171+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(comparison))
172+
173+
// return 1
174+
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
175+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
176+
177+
val results = machine.analyze(listOf(method), listOf(initialTarget))
178+
assertEquals(
179+
1,
180+
results.size,
181+
"Expected exactly one result for array sum reachable path, but got ${results.size}"
182+
)
183+
184+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
185+
assertTrue(
186+
returnStmt in reachedStatements,
187+
"Expected return statement to be reached in execution path"
188+
)
189+
}
190+
191+
@Disabled("Nested array access becomes field access")
192+
@Test
193+
fun testNestedArrayReachable() {
194+
// Test reachability through nested array access: matrix[0][0] === 1 -> matrix[1][1] === 4 -> return 1
195+
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
196+
val method = scene.projectClasses
197+
.flatMap { it.methods }
198+
.single { it.name == "nestedArrayReachable" }
199+
200+
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
201+
var target: TsTarget = initialTarget
202+
203+
// if (matrix[0][0] === 1)
204+
val firstCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
205+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstCheck))
206+
207+
// if (matrix[1][1] === 4)
208+
val secondCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
209+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondCheck))
210+
211+
// return 1
212+
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
213+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
214+
215+
val results = machine.analyze(listOf(method), listOf(initialTarget))
216+
assertEquals(
217+
1,
218+
results.size,
219+
"Expected exactly one result for nested array reachable path, but got ${results.size}"
220+
)
221+
222+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
223+
assertTrue(
224+
returnStmt in reachedStatements,
225+
"Expected return statement to be reached in execution path"
226+
)
227+
}
228+
}

0 commit comments

Comments
 (0)