Skip to content

Commit 36c11f1

Browse files
LipenLipen
committed
Add more test samples for reachability analysis
1 parent 99fa6cd commit 36c11f1

12 files changed

Lines changed: 2627 additions & 0 deletions

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

Lines changed: 293 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,293 @@
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.usvm.PathSelectionStrategy
8+
import org.usvm.SolverType
9+
import org.usvm.UMachineOptions
10+
import org.usvm.api.targets.ReachabilityObserver
11+
import org.usvm.api.targets.TsReachabilityTarget
12+
import org.usvm.api.targets.TsTarget
13+
import org.usvm.machine.TsMachine
14+
import org.usvm.machine.TsOptions
15+
import org.usvm.util.getResourcePath
16+
import kotlin.test.Test
17+
import kotlin.test.assertTrue
18+
import kotlin.time.Duration
19+
20+
/**
21+
* Tests for asynchronous programming reachability scenarios.
22+
* Verifies reachability analysis through async patterns and error handling.
23+
*/
24+
class AsyncReachabilityTest {
25+
26+
private val scene = run {
27+
val path = "/reachability/AsyncReachability.ts"
28+
val res = getResourcePath(path)
29+
val file = loadEtsFileAutoConvert(res)
30+
EtsScene(listOf(file))
31+
}
32+
33+
private val options = UMachineOptions(
34+
pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
35+
exceptionsPropagation = true,
36+
stopOnTargetsReached = true,
37+
timeout = Duration.INFINITE,
38+
stepsFromLastCovered = 3500L,
39+
solverType = SolverType.YICES,
40+
solverTimeout = Duration.INFINITE,
41+
typeOperationsTimeout = Duration.INFINITE,
42+
)
43+
44+
private val tsOptions = TsOptions()
45+
46+
@Test
47+
fun testAsyncAwaitReachable() {
48+
// Test reachability through async function logic:
49+
// const result = delay * 2 -> if (result > 50) -> if (result < 100) -> return 1
50+
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
51+
val method = scene.projectClasses
52+
.flatMap { it.methods }
53+
.single { it.name == "asyncAwaitReachable" }
54+
55+
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
56+
var target: TsTarget = initialTarget
57+
58+
// if (result > 50)
59+
val minCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
60+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(minCheck))
61+
62+
// if (result < 100)
63+
val maxCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
64+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(maxCheck))
65+
66+
// return 1
67+
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
68+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
69+
70+
val results = machine.analyze(listOf(method), listOf(initialTarget))
71+
assertTrue(
72+
results.isNotEmpty(),
73+
"Expected at least one result for async/await reachability"
74+
)
75+
76+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
77+
assertTrue(
78+
returnStmt in reachedStatements,
79+
"Expected return statement to be reached when delay * 2 is between 50-100"
80+
)
81+
}
82+
83+
@Test
84+
fun testPromiseChainReachable() {
85+
// Test reachability through Promise chain:
86+
// const doubled = value * 2 -> if (doubled === 20) -> return Promise.resolve(1)
87+
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
88+
val method = scene.projectClasses
89+
.flatMap { it.methods }
90+
.single { it.name == "promiseChainReachable" }
91+
92+
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
93+
var target: TsTarget = initialTarget
94+
95+
// if (doubled === 20)
96+
val doubledCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
97+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(doubledCheck))
98+
99+
// return Promise.resolve(1)
100+
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
101+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
102+
103+
val results = machine.analyze(listOf(method), listOf(initialTarget))
104+
assertTrue(
105+
results.isNotEmpty(),
106+
"Expected at least one result for Promise chain reachability"
107+
)
108+
109+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
110+
assertTrue(
111+
returnStmt in reachedStatements,
112+
"Expected return statement to be reached when input value is 10"
113+
)
114+
}
115+
116+
@Test
117+
fun testPromiseAllReachable() {
118+
// Test reachability through Promise.all pattern:
119+
// const results = values.map(v => v * 2) -> if (results.length === 3) -> if (results[1] === 40) -> return 1
120+
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
121+
val method = scene.projectClasses
122+
.flatMap { it.methods }
123+
.single { it.name == "promiseAllReachable" }
124+
125+
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
126+
var target: TsTarget = initialTarget
127+
128+
// if (results.length === 3)
129+
val lengthCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
130+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(lengthCheck))
131+
132+
// if (results[1] === 40)
133+
val valueCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
134+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(valueCheck))
135+
136+
// return 1
137+
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
138+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
139+
140+
val results = machine.analyze(listOf(method), listOf(initialTarget))
141+
assertTrue(
142+
results.isNotEmpty(),
143+
"Expected at least one result for Promise.all reachability"
144+
)
145+
146+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
147+
assertTrue(
148+
returnStmt in reachedStatements,
149+
"Expected return statement to be reached when values[1] is 20 (doubled to 40)"
150+
)
151+
}
152+
153+
@Test
154+
fun testCallbackReachable() {
155+
// Test reachability through callback pattern:
156+
// const processed = value + 10 -> if (processed > 25) -> callback(processed) -> return 1
157+
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
158+
val method = scene.projectClasses
159+
.flatMap { it.methods }
160+
.single { it.name == "callbackReachable" }
161+
162+
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
163+
var target: TsTarget = initialTarget
164+
165+
// if (processed > 25)
166+
val processedCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
167+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(processedCheck))
168+
169+
// return 1
170+
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
171+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
172+
173+
val results = machine.analyze(listOf(method), listOf(initialTarget))
174+
assertTrue(
175+
results.isNotEmpty(),
176+
"Expected at least one result for callback reachability"
177+
)
178+
179+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
180+
assertTrue(
181+
returnStmt in reachedStatements,
182+
"Expected return statement to be reached when value > 15 (processed > 25)"
183+
)
184+
}
185+
186+
@Test
187+
fun testErrorHandlingReachable() {
188+
// Test reachability through try-catch error handling:
189+
// try { if (shouldThrow) throw Error -> return 1 } catch { return -1 }
190+
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
191+
val method = scene.projectClasses
192+
.flatMap { it.methods }
193+
.single { it.name == "errorHandlingReachable" }
194+
195+
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
196+
var target: TsTarget = initialTarget
197+
198+
// if (shouldThrow)
199+
val throwCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
200+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(throwCheck))
201+
202+
// Both return paths should be reachable
203+
val returnStmts = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()
204+
returnStmts.forEach { returnStmt ->
205+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
206+
}
207+
208+
val results = machine.analyze(listOf(method), listOf(initialTarget))
209+
assertTrue(
210+
results.isNotEmpty(),
211+
"Expected at least one result for error handling reachability"
212+
)
213+
214+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
215+
assertTrue(
216+
returnStmts.any { it in reachedStatements },
217+
"Expected at least one return statement to be reached in try-catch"
218+
)
219+
}
220+
221+
@Test
222+
fun testConditionalAsyncReachable() {
223+
// Test reachability through conditional async pattern:
224+
// if (useSync) result = value * 2 else result = value + 10 -> if (result === 20) -> return 1
225+
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
226+
val method = scene.projectClasses
227+
.flatMap { it.methods }
228+
.single { it.name == "conditionalAsyncReachable" }
229+
230+
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
231+
var target: TsTarget = initialTarget
232+
233+
// if (useSync)
234+
val useSyncCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
235+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(useSyncCheck))
236+
237+
// if (result === 20)
238+
val resultCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
239+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(resultCheck))
240+
241+
// return 1
242+
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
243+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
244+
245+
val results = machine.analyze(listOf(method), listOf(initialTarget))
246+
assertTrue(
247+
results.isNotEmpty(),
248+
"Expected at least one result for conditional async reachability"
249+
)
250+
251+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
252+
assertTrue(
253+
returnStmt in reachedStatements,
254+
"Expected return statement to be reached through conditional branches"
255+
)
256+
}
257+
258+
@Test
259+
fun testPromiseCreationReachable() {
260+
// Test reachability through Promise creation logic:
261+
// if (shouldResolve) -> if (value > 5) -> return 1
262+
// else -> if (value < 0) -> return -1
263+
val machine = TsMachine(scene, options, tsOptions, machineObserver = ReachabilityObserver())
264+
val method = scene.projectClasses
265+
.flatMap { it.methods }
266+
.single { it.name == "promiseCreationReachable" }
267+
268+
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
269+
var target: TsTarget = initialTarget
270+
271+
// if (shouldResolve)
272+
val shouldResolveCheck = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
273+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(shouldResolveCheck))
274+
275+
// Multiple return paths
276+
val returnStmts = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()
277+
returnStmts.forEach { returnStmt ->
278+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
279+
}
280+
281+
val results = machine.analyze(listOf(method), listOf(initialTarget))
282+
assertTrue(
283+
results.isNotEmpty(),
284+
"Expected at least one result for Promise creation reachability"
285+
)
286+
287+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
288+
assertTrue(
289+
returnStmts.any { it in reachedStatements },
290+
"Expected at least one return statement to be reached in Promise creation"
291+
)
292+
}
293+
}

0 commit comments

Comments
 (0)