Skip to content

Commit e93ea57

Browse files
LipenLipen
committed
Fix asserts
1 parent 9f4e4b5 commit e93ea57

6 files changed

Lines changed: 144 additions & 58 deletions

File tree

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

Lines changed: 34 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ import org.usvm.api.targets.TsTarget
1414
import org.usvm.machine.TsMachine
1515
import org.usvm.machine.TsOptions
1616
import org.usvm.util.getResourcePath
17-
import org.usvm.util.getRoot
1817
import kotlin.test.Test
1918
import kotlin.test.assertEquals
2019
import kotlin.test.assertTrue
@@ -68,14 +67,20 @@ class ArrayReachabilityTest {
6867

6968
// return 1
7069
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
71-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
70+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
7271

73-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
72+
val results = machine.analyze(listOf(method), listOf(initialTarget))
7473
assertEquals(
7574
1,
7675
results.size,
7776
"Expected exactly one result for simple array reachable path, but got ${results.size}"
7877
)
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+
)
7984
}
8085

8186
@Disabled("Extra exceptional path is found")
@@ -100,14 +105,20 @@ class ArrayReachabilityTest {
100105

101106
// return 1
102107
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
103-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
108+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
104109

105-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
110+
val results = machine.analyze(listOf(method), listOf(initialTarget))
106111
assertEquals(
107112
1,
108113
results.size,
109114
"Expected exactly one result for array modification reachable path, but got ${results.size}"
110115
)
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+
)
111122
}
112123

113124
@Test
@@ -127,9 +138,9 @@ class ArrayReachabilityTest {
127138

128139
// return -1
129140
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
130-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
141+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
131142

132-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
143+
val results = machine.analyze(listOf(method), listOf(initialTarget))
133144

134145
// In targeted mode, results may be non-empty as machine explores paths toward targets
135146
// But the unreachable return statement should not be reached in any execution path
@@ -161,14 +172,20 @@ class ArrayReachabilityTest {
161172

162173
// return 1
163174
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
164-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
175+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
165176

166-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
177+
val results = machine.analyze(listOf(method), listOf(initialTarget))
167178
assertEquals(
168179
1,
169180
results.size,
170181
"Expected exactly one result for array sum reachable path, but got ${results.size}"
171182
)
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+
)
172189
}
173190

174191
@Disabled("Nested array access becomes field access")
@@ -193,13 +210,19 @@ class ArrayReachabilityTest {
193210

194211
// return 1
195212
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
196-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
213+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
197214

198-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
215+
val results = machine.analyze(listOf(method), listOf(initialTarget))
199216
assertEquals(
200217
1,
201218
results.size,
202219
"Expected exactly one result for nested array reachable path, but got ${results.size}"
203220
)
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+
)
204227
}
205228
}

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

Lines changed: 21 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ import org.usvm.api.targets.TsTarget
1313
import org.usvm.machine.TsMachine
1414
import org.usvm.machine.TsOptions
1515
import org.usvm.util.getResourcePath
16-
import org.usvm.util.getRoot
1716
import kotlin.test.Test
1817
import kotlin.test.assertEquals
1918
import kotlin.test.assertTrue
@@ -69,12 +68,18 @@ class BasicConditionsReachabilityTest {
6968
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
7069
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
7170

72-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
71+
val results = machine.analyze(listOf(method), listOf(initialTarget))
7372
assertEquals(
7473
1,
7574
results.size,
7675
"Expected exactly one result for reachable path, but got ${results.size}"
7776
)
77+
78+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
79+
assertTrue(
80+
returnStmt in reachedStatements,
81+
"Expected return statement to be reached in execution path"
82+
)
7883
}
7984

8085
@Test
@@ -98,12 +103,10 @@ class BasicConditionsReachabilityTest {
98103

99104
// return -1
100105
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
101-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
106+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
102107

103-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
108+
val results = machine.analyze(listOf(method), listOf(initialTarget))
104109

105-
// In targeted mode, results may be non-empty as machine explores paths toward targets
106-
// But the unreachable return statement should not be reached in any execution path
107110
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
108111
assertTrue(
109112
returnStmt !in reachedStatements,
@@ -136,14 +139,20 @@ class BasicConditionsReachabilityTest {
136139

137140
// return 1
138141
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
139-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
142+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
140143

141-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
144+
val results = machine.analyze(listOf(method), listOf(initialTarget))
142145
assertEquals(
143146
1,
144147
results.size,
145148
"Expected exactly one result for multi-variable reachable path, but got ${results.size}"
146149
)
150+
151+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
152+
assertTrue(
153+
returnStmt in reachedStatements,
154+
"Expected return statement to be reached in execution path"
155+
)
147156
}
148157

149158
@Test
@@ -171,9 +180,9 @@ class BasicConditionsReachabilityTest {
171180

172181
// return 1
173182
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
174-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
183+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
175184

176-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
185+
val results = machine.analyze(listOf(method), listOf(initialTarget))
177186
assertEquals(
178187
1,
179188
results.size,
@@ -202,9 +211,9 @@ class BasicConditionsReachabilityTest {
202211

203212
// return -1
204213
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
205-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
214+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
206215

207-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
216+
val results = machine.analyze(listOf(method), listOf(initialTarget))
208217

209218
// In targeted mode, results may be non-empty as machine explores paths toward targets
210219
// But the unreachable return statement should not be reached in any execution path

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

Lines changed: 20 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ import org.usvm.api.targets.TsTarget
1313
import org.usvm.machine.TsMachine
1414
import org.usvm.machine.TsOptions
1515
import org.usvm.util.getResourcePath
16-
import org.usvm.util.getRoot
1716
import kotlin.test.Test
1817
import kotlin.test.assertEquals
1918
import kotlin.test.assertTrue
@@ -67,9 +66,9 @@ class ComplexReachabilityTest {
6766

6867
// return 1
6968
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
70-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
69+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
7170

72-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
71+
val results = machine.analyze(listOf(method), listOf(initialTarget))
7372
assertEquals(
7473
1,
7574
results.size,
@@ -98,9 +97,9 @@ class ComplexReachabilityTest {
9897

9998
// return 1
10099
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
101-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
100+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
102101

103-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
102+
val results = machine.analyze(listOf(method), listOf(initialTarget))
104103
assertEquals(
105104
1,
106105
results.size,
@@ -125,9 +124,9 @@ class ComplexReachabilityTest {
125124

126125
// return 1
127126
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
128-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
127+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
129128

130-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
129+
val results = machine.analyze(listOf(method), listOf(initialTarget))
131130
assertEquals(
132131
1,
133132
results.size,
@@ -155,14 +154,23 @@ class ComplexReachabilityTest {
155154
target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf))
156155

157156
// return 1
158-
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
159-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
157+
val return1 = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
158+
target.addChild(TsReachabilityTarget.FinalPoint(return1))
159+
160+
// return 2
161+
val return2 = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[1]
162+
target.addChild(TsReachabilityTarget.FinalPoint(return2))
160163

161-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
164+
val results = machine.analyze(listOf(method), listOf(initialTarget))
162165
assertTrue(
163166
results.isNotEmpty(),
164167
"Expected at least one result for conditional object reachable path, but got ${results.size}"
165168
)
169+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
170+
assertTrue(
171+
return1 in reachedStatements,
172+
"Expected 'return 1' statement to be reached in conditional object reachable path"
173+
)
166174
}
167175

168176
@Test
@@ -190,9 +198,9 @@ class ComplexReachabilityTest {
190198

191199
// return 1
192200
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
193-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
201+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
194202

195-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
203+
val results = machine.analyze(listOf(method), listOf(initialTarget))
196204
assertEquals(
197205
1,
198206
results.size,

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

Lines changed: 34 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,6 @@ import org.usvm.api.targets.TsTarget
1313
import org.usvm.machine.TsMachine
1414
import org.usvm.machine.TsOptions
1515
import org.usvm.util.getResourcePath
16-
import org.usvm.util.getRoot
1716
import kotlin.test.Test
1817
import kotlin.test.assertEquals
1918
import kotlin.test.assertTrue
@@ -67,14 +66,20 @@ class FieldAccessReachabilityTest {
6766

6867
// return 1
6968
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
70-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
69+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
7170

72-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
71+
val results = machine.analyze(listOf(method), listOf(initialTarget))
7372
assertEquals(
7473
1,
7574
results.size,
7675
"Expected exactly one result for field access reachable path, but got ${results.size}"
7776
)
77+
78+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
79+
assertTrue(
80+
returnStmt in reachedStatements,
81+
"Expected return statement to be reached in execution path"
82+
)
7883
}
7984

8085
@Test
@@ -98,14 +103,20 @@ class FieldAccessReachabilityTest {
98103

99104
// return 1
100105
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
101-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
106+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
102107

103-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
108+
val results = machine.analyze(listOf(method), listOf(initialTarget))
104109
assertEquals(
105110
1,
106111
results.size,
107112
"Expected exactly one result for field modification reachable path, but got ${results.size}"
108113
)
114+
115+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
116+
assertTrue(
117+
returnStmt in reachedStatements,
118+
"Expected return statement to be reached in execution path"
119+
)
109120
}
110121

111122
@Test
@@ -125,9 +136,9 @@ class FieldAccessReachabilityTest {
125136

126137
// return -1
127138
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
128-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
139+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
129140

130-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
141+
val results = machine.analyze(listOf(method), listOf(initialTarget))
131142

132143
// In targeted mode, results may be non-empty as machine explores paths toward targets
133144
// But the unreachable return statement should not be reached in any execution path
@@ -159,14 +170,20 @@ class FieldAccessReachabilityTest {
159170

160171
// return 1
161172
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
162-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
173+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
163174

164-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
175+
val results = machine.analyze(listOf(method), listOf(initialTarget))
165176
assertEquals(
166177
1,
167178
results.size,
168179
"Expected exactly one result for object creation reachable path, but got ${results.size}"
169180
)
181+
182+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
183+
assertTrue(
184+
returnStmt in reachedStatements,
185+
"Expected return statement to be reached in execution path"
186+
)
170187
}
171188

172189
@Test
@@ -190,12 +207,18 @@ class FieldAccessReachabilityTest {
190207

191208
// return 1
192209
val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
193-
target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
210+
target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
194211

195-
val results = machine.analyze(listOf(method), listOf(target.getRoot()))
212+
val results = machine.analyze(listOf(method), listOf(initialTarget))
196213
assertTrue(
197214
results.isNotEmpty(),
198215
"Expected at least one result for ambiguous field access, but got ${results.size}"
199216
)
217+
218+
val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
219+
assertTrue(
220+
returnStmt in reachedStatements,
221+
"Expected return statement to be reached in execution path"
222+
)
200223
}
201224
}

0 commit comments

Comments
 (0)