Skip to content

Commit 407b68a

Browse files
LipenLipen
authored
[TS] Bump jacodb and adopt enums (#332)
1 parent 7354d9f commit 407b68a

File tree

13 files changed

+159
-117
lines changed

13 files changed

+159
-117
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@ jobs:
130130
DEST_DIR="arkanalyzer"
131131
MAX_RETRIES=10
132132
RETRY_DELAY=3 # Delay between retries in seconds
133-
BRANCH="neo/2025-08-12"
133+
BRANCH="neo/2025-09-03"
134134
135135
for ((i=1; i<=MAX_RETRIES; i++)); do
136136
git clone --depth=1 --branch $BRANCH $REPO_URL $DEST_DIR && break

‎buildSrc/src/main/kotlin/Dependencies.kt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ object Versions {
66
const val clikt = "5.0.0"
77
const val detekt = "1.23.7"
88
const val ini4j = "0.5.4"
9-
const val jacodb = "bb51484fb4"
9+
const val jacodb = "b17013382a"
1010
const val juliet = "1.3.2"
1111
const val junit = "5.9.3"
1212
const val kotlin = "2.1.0"

‎usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,6 @@ import org.jacodb.ets.model.EtsFunctionType
5151
import org.jacodb.ets.model.EtsGenericType
5252
import org.jacodb.ets.model.EtsIntersectionType
5353
import org.jacodb.ets.model.EtsLexicalEnvType
54-
import org.jacodb.ets.model.EtsLiteralType
5554
import org.jacodb.ets.model.EtsNeverType
5655
import org.jacodb.ets.model.EtsNullType
5756
import org.jacodb.ets.model.EtsNumberLiteralType
@@ -120,7 +119,7 @@ private object EtsTypeToDto : EtsType.Visitor<TypeDto> {
120119
override fun visit(type: EtsEnumValueType): TypeDto {
121120
return EnumValueTypeDto(
122121
signature = type.signature.toDto(),
123-
constant = type.constant?.toDto(),
122+
name = type.name,
124123
)
125124
}
126125

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

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -294,14 +294,13 @@ private fun TsExprResolver.handleArrayPush(
294294
memory.write(lengthLValue, newLength, guard = trueExpr)
295295

296296
// Write the new element to the end of the array
297-
// TODO check sorts compatibility https://github.com/UnitTestBot/usvm/issues/300
298-
val newIndexLValue = mkArrayIndexLValue(
299-
sort = elementSort,
300-
ref = array,
297+
assignToArrayIndex(
298+
scope = scope,
299+
array = array,
301300
index = length,
302-
type = arrayType,
303-
)
304-
memory.write(newIndexLValue, arg.asExpr(elementSort), guard = trueExpr)
301+
expr = arg,
302+
arrayType = arrayType,
303+
) ?: return@calcOnState null
305304

306305
// Return the new length of the array (as per ECMAScript spec for Array.push)
307306
mkBvToFpExpr(

‎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
}

0 commit comments

Comments
 (0)