Skip to content

Commit 831e31b

Browse files
LipenLipen
committed
Fix asserts
1 parent 6364702 commit 831e31b

6 files changed

Lines changed: 107 additions & 98 deletions

File tree

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

Lines changed: 13 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ class ArrayReachabilityTest {
3737
pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
3838
exceptionsPropagation = true,
3939
stopOnTargetsReached = true,
40-
timeout = 15.seconds,
40+
timeout = Duration.INFINITE,
4141
stepsFromLastCovered = 3500L,
4242
solverType = SolverType.YICES,
4343
solverTimeout = Duration.INFINITE,
@@ -70,10 +70,9 @@ class ArrayReachabilityTest {
7070
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
7171

7272
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}"
73+
assertTrue(
74+
results.isNotEmpty(),
75+
"Expected at least one result",
7776
)
7877

7978
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -108,10 +107,9 @@ class ArrayReachabilityTest {
108107
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
109108

110109
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}"
110+
assertTrue(
111+
results.isNotEmpty(),
112+
"Expected at least one result",
115113
)
116114

117115
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -175,10 +173,9 @@ class ArrayReachabilityTest {
175173
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
176174

177175
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}"
176+
assertTrue(
177+
results.isNotEmpty(),
178+
"Expected at least one result",
182179
)
183180

184181
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -213,10 +210,9 @@ class ArrayReachabilityTest {
213210
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
214211

215212
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}"
213+
assertTrue(
214+
results.isNotEmpty(),
215+
"Expected at least one result",
220216
)
221217

222218
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()

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

Lines changed: 16 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,8 @@ import org.usvm.machine.TsMachine
1414
import org.usvm.machine.TsOptions
1515
import org.usvm.util.getResourcePath
1616
import kotlin.test.Test
17-
import kotlin.test.assertEquals
1817
import kotlin.test.assertTrue
1918
import kotlin.time.Duration
20-
import kotlin.time.Duration.Companion.seconds
2119

2220
/**
2321
* Tests for basic conditional reachability scenarios.
@@ -36,7 +34,7 @@ class BasicConditionsReachabilityTest {
3634
pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
3735
exceptionsPropagation = true,
3836
stopOnTargetsReached = true,
39-
timeout = 15.seconds,
37+
timeout = Duration.INFINITE,
4038
stepsFromLastCovered = 3500L,
4139
solverType = SolverType.YICES,
4240
solverTimeout = Duration.INFINITE,
@@ -70,10 +68,9 @@ class BasicConditionsReachabilityTest {
7068
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
7169

7270
val results = machine.analyze(listOf(method), listOf(initialTarget))
73-
assertEquals(
74-
1,
75-
results.size,
76-
"Expected exactly one result for reachable path, but got ${results.size}"
71+
assertTrue(
72+
results.isNotEmpty(),
73+
"Expected at least one result",
7774
)
7875

7976
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -145,10 +142,9 @@ class BasicConditionsReachabilityTest {
145142
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
146143

147144
val results = machine.analyze(listOf(method), listOf(initialTarget))
148-
assertEquals(
149-
1,
150-
results.size,
151-
"Expected exactly one result for multi-variable reachable path, but got ${results.size}"
145+
assertTrue(
146+
results.isNotEmpty(),
147+
"Expected at least one result",
152148
)
153149

154150
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -187,10 +183,15 @@ class BasicConditionsReachabilityTest {
187183
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
188184

189185
val results = machine.analyze(listOf(method), listOf(initialTarget))
190-
assertEquals(
191-
1,
192-
results.size,
193-
"Expected exactly one result for equality-based reachable path, but got ${results.size}"
186+
assertTrue(
187+
results.isNotEmpty(),
188+
"Expected at least one result",
189+
)
190+
191+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
192+
assertTrue(
193+
returnStmt in reachedStatements,
194+
"Expected return statement to be reached in execution path"
194195
)
195196
}
196197

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

Lines changed: 49 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,8 @@ import org.usvm.machine.TsMachine
1414
import org.usvm.machine.TsOptions
1515
import org.usvm.util.getResourcePath
1616
import kotlin.test.Test
17-
import kotlin.test.assertEquals
1817
import kotlin.test.assertTrue
1918
import kotlin.time.Duration
20-
import kotlin.time.Duration.Companion.seconds
2119

2220
/**
2321
* Tests for complex reachability scenarios combining multiple language constructions.
@@ -36,7 +34,7 @@ class ComplexReachabilityTest {
3634
pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
3735
exceptionsPropagation = true,
3836
stopOnTargetsReached = true,
39-
timeout = 15.seconds,
37+
timeout = Duration.INFINITE,
4038
stepsFromLastCovered = 3500L,
4139
solverType = SolverType.YICES,
4240
solverTimeout = Duration.INFINITE,
@@ -69,10 +67,15 @@ class ComplexReachabilityTest {
6967
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
7068

7169
val results = machine.analyze(listOf(method), listOf(initialTarget))
72-
assertEquals(
73-
1,
74-
results.size,
75-
"Expected exactly one result for array-object combined reachable path, but got ${results.size}"
70+
assertTrue(
71+
results.isNotEmpty(),
72+
"Expected at least one result",
73+
)
74+
75+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
76+
assertTrue(
77+
returnStmt in reachedStatements,
78+
"Expected return statement to be reached in execution path"
7679
)
7780
}
7881

@@ -87,23 +90,24 @@ class ComplexReachabilityTest {
8790
val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
8891
var target: TsTarget = initialTarget
8992

90-
// if (processedArr.length > 0)
93+
// if (processedArr.length > 1)
9194
val firstIf = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
9295
target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf))
9396

94-
// if (processedArr[0] > input)
95-
val secondIf = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
96-
target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf))
97-
9897
// return 1
9998
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
10099
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
101100

102101
val results = machine.analyze(listOf(method), listOf(initialTarget))
103-
assertEquals(
104-
1,
105-
results.size,
106-
"Expected exactly one result for method array manipulation reachable path, but got ${results.size}"
102+
assertTrue(
103+
results.isNotEmpty(),
104+
"Expected at least one result",
105+
)
106+
107+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
108+
assertTrue(
109+
returnStmt in reachedStatements,
110+
"Expected return statement to be reached in execution path"
107111
)
108112
}
109113

@@ -122,15 +126,24 @@ class ComplexReachabilityTest {
122126
val firstIf = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
123127
target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf))
124128

129+
// if (calculator.getValue() === 25)
130+
val secondIf = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
131+
target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf))
132+
125133
// return 1
126134
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
127135
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
128136

129137
val results = machine.analyze(listOf(method), listOf(initialTarget))
130-
assertEquals(
131-
1,
132-
results.size,
133-
"Expected exactly one result for object method call reachable path, but got ${results.size}"
138+
assertTrue(
139+
results.isNotEmpty(),
140+
"Expected at least one result",
141+
)
142+
143+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
144+
assertTrue(
145+
returnStmt in reachedStatements,
146+
"Expected return statement to be reached in execution path"
134147
)
135148
}
136149

@@ -164,12 +177,17 @@ class ComplexReachabilityTest {
164177
val results = machine.analyze(listOf(method), listOf(initialTarget))
165178
assertTrue(
166179
results.isNotEmpty(),
167-
"Expected at least one result for conditional object reachable path, but got ${results.size}"
180+
"Expected at least one result",
168181
)
182+
169183
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
170184
assertTrue(
171185
return1 in reachedStatements,
172-
"Expected 'return 1' statement to be reached in conditional object reachable path"
186+
"Expected 'return 1' statement to be reached in execution path"
187+
)
188+
assertTrue(
189+
return2 in reachedStatements,
190+
"Expected 'return 2' statement to be reached in execution path"
173191
)
174192
}
175193

@@ -201,10 +219,15 @@ class ComplexReachabilityTest {
201219
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
202220

203221
val results = machine.analyze(listOf(method), listOf(initialTarget))
204-
assertEquals(
205-
1,
206-
results.size,
207-
"Expected exactly one result for cross-reference reachable path, but got ${results.size}"
222+
assertTrue(
223+
results.isNotEmpty(),
224+
"Expected at least one result",
225+
)
226+
227+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
228+
assertTrue(
229+
returnStmt in reachedStatements,
230+
"Expected return statement to be reached in execution path"
208231
)
209232
}
210233
}

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

Lines changed: 11 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,8 @@ import org.usvm.machine.TsMachine
1414
import org.usvm.machine.TsOptions
1515
import org.usvm.util.getResourcePath
1616
import kotlin.test.Test
17-
import kotlin.test.assertEquals
1817
import kotlin.test.assertTrue
1918
import kotlin.time.Duration
20-
import kotlin.time.Duration.Companion.seconds
2119

2220
/**
2321
* Tests for field access reachability scenarios.
@@ -36,7 +34,7 @@ class FieldAccessReachabilityTest {
3634
pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
3735
exceptionsPropagation = true,
3836
stopOnTargetsReached = true,
39-
timeout = 15.seconds,
37+
timeout = Duration.INFINITE,
4038
stepsFromLastCovered = 3500L,
4139
solverType = SolverType.YICES,
4240
solverTimeout = Duration.INFINITE,
@@ -70,10 +68,9 @@ class FieldAccessReachabilityTest {
7068
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
7169

7270
val results = machine.analyze(listOf(method), listOf(initialTarget))
73-
assertEquals(
74-
1,
75-
results.size,
76-
"Expected exactly one result for field access reachable path, but got ${results.size}"
71+
assertTrue(
72+
results.isNotEmpty(),
73+
"Expected at least one result",
7774
)
7875

7976
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -108,10 +105,9 @@ class FieldAccessReachabilityTest {
108105
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
109106

110107
val results = machine.analyze(listOf(method), listOf(initialTarget))
111-
assertEquals(
112-
1,
113-
results.size,
114-
"Expected exactly one result for field modification reachable path, but got ${results.size}"
108+
assertTrue(
109+
results.isNotEmpty(),
110+
"Expected at least one result",
115111
)
116112

117113
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -176,10 +172,9 @@ class FieldAccessReachabilityTest {
176172
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
177173

178174
val results = machine.analyze(listOf(method), listOf(initialTarget))
179-
assertEquals(
180-
1,
181-
results.size,
182-
"Expected exactly one result for object creation reachable path, but got ${results.size}"
175+
assertTrue(
176+
results.isNotEmpty(),
177+
"Expected at least one result",
183178
)
184179

185180
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -215,7 +210,7 @@ class FieldAccessReachabilityTest {
215210
val results = machine.analyze(listOf(method), listOf(initialTarget))
216211
assertTrue(
217212
results.isNotEmpty(),
218-
"Expected at least one result for ambiguous field access, but got ${results.size}"
213+
"Expected at least one result",
219214
)
220215

221216
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()

0 commit comments

Comments
 (0)