Skip to content

Commit 71cd0e1

Browse files
LipenLipen
authored
[TS] Extend reachability analysis test suite (#334)
1 parent 3eb7178 commit 71cd0e1

15 files changed

+2707
-3
lines changed

‎usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
package org.usvm.machine.expr
22

3+
import io.ksmt.expr.KFpRoundingMode
34
import io.ksmt.utils.asExpr
45
import mu.KotlinLogging
56
import org.jacodb.ets.model.EtsArrayType
@@ -76,6 +77,13 @@ internal fun TsExprResolver.tryApproximateInstanceCall(
7677
}
7778
}
7879

80+
// Handle `Math` method calls
81+
if (expr.instance.name == "Math") {
82+
if (expr.callee.name == "floor") {
83+
return from(handleMathFloor(expr))
84+
}
85+
}
86+
7987
val instance = scope.calcOnState { resolve(expr.instance)?.asExpr(addressSort) }
8088
?: return TsExprApproximationResult.ResolveFailure
8189

@@ -255,6 +263,27 @@ private fun TsExprResolver.handlePromiseResolveReject(expr: EtsInstanceCallExpr)
255263
promise
256264
}
257265

266+
private fun TsExprResolver.handleMathFloor(expr: EtsInstanceCallExpr): UExpr<*>? = with(ctx) {
267+
check(expr.args.size == 1) {
268+
"Math.floor() should have exactly one argument, but got ${expr.args.size}"
269+
}
270+
val arg = resolve(expr.args.single()) ?: return null
271+
272+
when (arg.sort) {
273+
fp64Sort -> mkFpRoundToIntegralExpr(
274+
roundingMode = mkFpRoundingModeExpr(KFpRoundingMode.RoundTowardNegative),
275+
value = arg.asExpr(fp64Sort),
276+
)
277+
278+
sizeSort -> arg.asExpr(sizeSort)
279+
280+
else -> {
281+
logger.warn { "Unsupported argument sort for Math.floor(): ${arg.sort}" }
282+
null
283+
}
284+
}
285+
}
286+
258287
/**
259288
* Handles the `Array.push(...items)` method call.
260289
* Appends the specified `items` to the end of the array.

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

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

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ import org.jacodb.ets.model.EtsIfStmt
44
import org.jacodb.ets.model.EtsReturnStmt
55
import org.jacodb.ets.model.EtsScene
66
import org.jacodb.ets.utils.loadEtsFileAutoConvert
7+
import org.junit.jupiter.api.Disabled
78
import org.usvm.PathSelectionStrategy
89
import org.usvm.SolverType
910
import org.usvm.UMachineOptions
@@ -95,7 +96,7 @@ class ComplexReachabilityTest {
9596
target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf))
9697

9798
// return 1
98-
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
99+
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[1]
99100
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
100101

101102
val results = machine.analyze(listOf(method), listOf(initialTarget))
@@ -147,6 +148,7 @@ class ComplexReachabilityTest {
147148
)
148149
}
149150

151+
@Disabled("Multiple methods ::process")
150152
@Test
151153
fun testConditionalObjectReachable() {
152154
// Test reachability with conditional object creation and polymorphic method calls
@@ -167,7 +169,7 @@ class ComplexReachabilityTest {
167169
target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf))
168170

169171
// return 1
170-
val return1 = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
172+
val return1 = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[2]
171173
target.addChild(TsReachabilityTarget.FinalPoint(return1))
172174

173175
// return 2

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -161,7 +161,7 @@ class FunctionCallReachabilityTest {
161161
target = target.addChild(TsReachabilityTarget.IntermediatePoint(check))
162162

163163
// return 1
164-
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
164+
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[1]
165165
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
166166

167167
val results = machine.analyze(listOf(method), listOf(initialTarget))

0 commit comments

Comments
 (0)