[TS] Bump jacodb and adopt enums

.github/workflows/ci.yml

@@ -130,7 +130,7 @@ jobs:
           DEST_DIR="arkanalyzer"
           MAX_RETRIES=10
           RETRY_DELAY=3  # Delay between retries in seconds  
-          BRANCH="neo/2025-08-12"
+          BRANCH="neo/2025-09-03"
 
           for ((i=1; i<=MAX_RETRIES; i++)); do
               git clone --depth=1 --branch $BRANCH $REPO_URL $DEST_DIR && break

buildSrc/src/main/kotlin/Dependencies.kt

@@ -6,7 +6,7 @@ object Versions {
     const val clikt = "5.0.0"
     const val detekt = "1.23.7"
     const val ini4j = "0.5.4"
-    const val jacodb = "bb51484fb4"
+    const val jacodb = "b17013382a"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

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

@@ -51,7 +51,6 @@ import org.jacodb.ets.model.EtsFunctionType
 import org.jacodb.ets.model.EtsGenericType
 import org.jacodb.ets.model.EtsIntersectionType
 import org.jacodb.ets.model.EtsLexicalEnvType
-import org.jacodb.ets.model.EtsLiteralType
 import org.jacodb.ets.model.EtsNeverType
 import org.jacodb.ets.model.EtsNullType
 import org.jacodb.ets.model.EtsNumberLiteralType
@@ -120,7 +119,7 @@ private object EtsTypeToDto : EtsType.Visitor<TypeDto> {
     override fun visit(type: EtsEnumValueType): TypeDto {
         return EnumValueTypeDto(
             signature = type.signature.toDto(),
-            constant = type.constant?.toDto(),
+            name = type.name,
         )
     }
 

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

@@ -294,14 +294,13 @@ private fun TsExprResolver.handleArrayPush(
         memory.write(lengthLValue, newLength, guard = trueExpr)
 
         // Write the new element to the end of the array
-        // TODO check sorts compatibility https://github.com/UnitTestBot/usvm/issues/300
-        val newIndexLValue = mkArrayIndexLValue(
-            sort = elementSort,
-            ref = array,
+        assignToArrayIndex(
+            scope = scope,
+            array = array,
             index = length,
-            type = arrayType,
-        )
-        memory.write(newIndexLValue, arg.asExpr(elementSort), guard = trueExpr)
+            expr = arg,
+            arrayType = arrayType,
+        ) ?: return@calcOnState null
 
         // Return the new length of the array (as per ECMAScript spec for Array.push)
         mkBvToFpExpr(

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

@@ -37,7 +37,7 @@ class ArrayReachabilityTest {
         pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
         exceptionsPropagation = true,
         stopOnTargetsReached = true,
-        timeout = 15.seconds,
+        timeout = Duration.INFINITE,
         stepsFromLastCovered = 3500L,
         solverType = SolverType.YICES,
         solverTimeout = Duration.INFINITE,
@@ -70,10 +70,9 @@ class ArrayReachabilityTest {
         target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))
-        assertEquals(
-            1,
-            results.size,
-            "Expected exactly one result for simple array reachable path, but got ${results.size}"
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result",
         )
 
         val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -108,10 +107,9 @@ class ArrayReachabilityTest {
         target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))
-        assertEquals(
-            1,
-            results.size,
-            "Expected exactly one result for array modification reachable path, but got ${results.size}"
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result",
         )
 
         val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -175,10 +173,9 @@ class ArrayReachabilityTest {
         target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))
-        assertEquals(
-            1,
-            results.size,
-            "Expected exactly one result for array sum reachable path, but got ${results.size}"
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result",
         )
 
         val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -213,10 +210,9 @@ class ArrayReachabilityTest {
         target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))
-        assertEquals(
-            1,
-            results.size,
-            "Expected exactly one result for nested array reachable path, but got ${results.size}"
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result",
         )
 
         val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()

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

@@ -14,10 +14,8 @@ import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.util.getResourcePath
 import kotlin.test.Test
-import kotlin.test.assertEquals
 import kotlin.test.assertTrue
 import kotlin.time.Duration
-import kotlin.time.Duration.Companion.seconds
 
 /**
  * Tests for basic conditional reachability scenarios.
@@ -36,7 +34,7 @@ class BasicConditionsReachabilityTest {
         pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
         exceptionsPropagation = true,
         stopOnTargetsReached = true,
-        timeout = 15.seconds,
+        timeout = Duration.INFINITE,
         stepsFromLastCovered = 3500L,
         solverType = SolverType.YICES,
         solverTimeout = Duration.INFINITE,
@@ -70,10 +68,9 @@ class BasicConditionsReachabilityTest {
         target = target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))
-        assertEquals(
-            1,
-            results.size,
-            "Expected exactly one result for reachable path, but got ${results.size}"
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result",
         )
 
         val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -145,10 +142,9 @@ class BasicConditionsReachabilityTest {
         target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))
-        assertEquals(
-            1,
-            results.size,
-            "Expected exactly one result for multi-variable reachable path, but got ${results.size}"
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result",
         )
 
         val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
@@ -187,10 +183,15 @@ class BasicConditionsReachabilityTest {
         target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))
-        assertEquals(
-            1,
-            results.size,
-            "Expected exactly one result for equality-based reachable path, but got ${results.size}"
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result",
+        )
+
+        val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
+        assertTrue(
+            returnStmt in reachedStatements,
+            "Expected return statement to be reached in execution path"
         )
     }
 

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

@@ -14,10 +14,8 @@ import org.usvm.machine.TsMachine
 import org.usvm.machine.TsOptions
 import org.usvm.util.getResourcePath
 import kotlin.test.Test
-import kotlin.test.assertEquals
 import kotlin.test.assertTrue
 import kotlin.time.Duration
-import kotlin.time.Duration.Companion.seconds
 
 /**
  * Tests for complex reachability scenarios combining multiple language constructions.
@@ -36,7 +34,7 @@ class ComplexReachabilityTest {
         pathSelectionStrategies = listOf(PathSelectionStrategy.TARGETED),
         exceptionsPropagation = true,
         stopOnTargetsReached = true,
-        timeout = 15.seconds,
+        timeout = Duration.INFINITE,
         stepsFromLastCovered = 3500L,
         solverType = SolverType.YICES,
         solverTimeout = Duration.INFINITE,
@@ -69,10 +67,15 @@ class ComplexReachabilityTest {
         target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))
-        assertEquals(
-            1,
-            results.size,
-            "Expected exactly one result for array-object combined reachable path, but got ${results.size}"
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result",
+        )
+
+        val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
+        assertTrue(
+            returnStmt in reachedStatements,
+            "Expected return statement to be reached in execution path"
         )
     }
 
@@ -87,23 +90,24 @@ class ComplexReachabilityTest {
         val initialTarget = TsReachabilityTarget.InitialPoint(method.cfg.stmts.first())
         var target: TsTarget = initialTarget
 
-        // if (processedArr.length > 0)
+        // if (processedArr.length > 1)
         val firstIf = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
         target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf))
 
-        // if (processedArr[0] > input)
-        val secondIf = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
-        target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf))
-
         // return 1
         val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
         target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))
-        assertEquals(
-            1,
-            results.size,
-            "Expected exactly one result for method array manipulation reachable path, but got ${results.size}"
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result",
+        )
+
+        val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
+        assertTrue(
+            returnStmt in reachedStatements,
+            "Expected return statement to be reached in execution path"
         )
     }
 
@@ -122,15 +126,24 @@ class ComplexReachabilityTest {
         val firstIf = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[0]
         target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf))
 
+        // if (calculator.getValue() === 25)
+        val secondIf = method.cfg.stmts.filterIsInstance<EtsIfStmt>()[1]
+        target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf))
+
         // return 1
         val returnStmt = method.cfg.stmts.filterIsInstance<EtsReturnStmt>()[0]
         target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))
-        assertEquals(
-            1,
-            results.size,
-            "Expected exactly one result for object method call reachable path, but got ${results.size}"
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result",
+        )
+
+        val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
+        assertTrue(
+            returnStmt in reachedStatements,
+            "Expected return statement to be reached in execution path"
         )
     }
 
@@ -164,12 +177,17 @@ class ComplexReachabilityTest {
         val results = machine.analyze(listOf(method), listOf(initialTarget))
         assertTrue(
             results.isNotEmpty(),
-            "Expected at least one result for conditional object reachable path, but got ${results.size}"
+            "Expected at least one result",
         )
+
         val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
         assertTrue(
             return1 in reachedStatements,
-            "Expected 'return 1' statement to be reached in conditional object reachable path"
+            "Expected 'return 1' statement to be reached in execution path"
+        )
+        assertTrue(
+            return2 in reachedStatements,
+            "Expected 'return 2' statement to be reached in execution path"
         )
     }
 
@@ -201,10 +219,15 @@ class ComplexReachabilityTest {
         target.addChild(TsReachabilityTarget.FinalPoint(returnStmt))
 
         val results = machine.analyze(listOf(method), listOf(initialTarget))
-        assertEquals(
-            1,
-            results.size,
-            "Expected exactly one result for cross-reference reachable path, but got ${results.size}"
+        assertTrue(
+            results.isNotEmpty(),
+            "Expected at least one result",
+        )
+
+        val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet()
+        assertTrue(
+            returnStmt in reachedStatements,
+            "Expected return statement to be reached in execution path"
         )
     }
 }