From 4b2f9aa941dce70004b755826261ea23f0567c6e Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 3 Sep 2025 15:44:25 +0300 Subject: [PATCH 1/8] Bump jacodb and ArkAnalyzer --- .github/workflows/ci.yml | 2 +- buildSrc/src/main/kotlin/Dependencies.kt | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 39bc478697..34faf3df14 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/buildSrc/src/main/kotlin/Dependencies.kt b/buildSrc/src/main/kotlin/Dependencies.kt index ca55b77f83..fe81c5630b 100644 --- a/buildSrc/src/main/kotlin/Dependencies.kt +++ b/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" From e326d19cebec900fce4a240aa9293c8bccc9dd7f Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 3 Sep 2025 15:45:21 +0300 Subject: [PATCH 2/8] Adopt enum changes --- .../main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt b/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt index 9dc13b5cd8..9d135dd210 100644 --- a/usvm-ts-dataflow/src/main/kotlin/org/usvm/dataflow/ts/infer/dto/EtsTypeToDto.kt +++ b/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 { override fun visit(type: EtsEnumValueType): TypeDto { return EnumValueTypeDto( signature = type.signature.toDto(), - constant = type.constant?.toDto(), + name = type.name, ) } From 63647024187ea85bf324e9793ffbd4fd18fc94df Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 10 Sep 2025 13:13:58 +0300 Subject: [PATCH 3/8] Replace plus-assign Currently, ArkIR for field-plus-assign is broken --- .../src/test/resources/reachability/ComplexReachability.ts | 2 +- .../test/resources/reachability/FunctionCallReachability.ts | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/test/resources/reachability/ComplexReachability.ts b/usvm-ts/src/test/resources/reachability/ComplexReachability.ts index 2ef75448c7..e9b04e3126 100644 --- a/usvm-ts/src/test/resources/reachability/ComplexReachability.ts +++ b/usvm-ts/src/test/resources/reachability/ComplexReachability.ts @@ -172,7 +172,7 @@ class Calculator { } add(val: number): void { - this.currentValue += val; + this.currentValue = this.currentValue + val; } } diff --git a/usvm-ts/src/test/resources/reachability/FunctionCallReachability.ts b/usvm-ts/src/test/resources/reachability/FunctionCallReachability.ts index 815d34d8cc..b50b4e575f 100644 --- a/usvm-ts/src/test/resources/reachability/FunctionCallReachability.ts +++ b/usvm-ts/src/test/resources/reachability/FunctionCallReachability.ts @@ -136,12 +136,12 @@ class FunctionCallReachability { } incrementCounter(counter: Counter, amount: number): void { - counter.value += amount; + counter.value = counter.value + amount; } crossIncrement(obj1: SimpleCounter, obj2: SimpleCounter, amount: number): void { - obj1.count += amount; - obj2.count += amount; + obj1.count = obj1.count + amount; + obj2.count = obj2.count + amount; } calculateSum(arr: number[]): number { From 831e31b159906911b328da7fb456e1b0c37d31cd Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 10 Sep 2025 13:14:35 +0300 Subject: [PATCH 4/8] Fix asserts --- .../reachability/ArrayReachabilityTest.kt | 30 ++++---- .../BasicConditionsReachabilityTest.kt | 31 ++++---- .../reachability/ComplexReachabilityTest.kt | 75 ++++++++++++------- .../FieldAccessReachabilityTest.kt | 27 +++---- .../FunctionCallReachabilityTest.kt | 32 ++++---- .../reachability/ComplexReachability.ts | 10 +-- 6 files changed, 107 insertions(+), 98 deletions(-) diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/ArrayReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/ArrayReachabilityTest.kt index 3eeb1192ea..b710f59e8d 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/ArrayReachabilityTest.kt +++ b/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() diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt index b8d949da58..6a42c32e87 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/BasicConditionsReachabilityTest.kt +++ b/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" ) } diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt index 49b0daee96..a425e4de42 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/ComplexReachabilityTest.kt +++ b/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()[0] target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) - // if (processedArr[0] > input) - val secondIf = method.cfg.stmts.filterIsInstance()[1] - target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) - // return 1 val returnStmt = method.cfg.stmts.filterIsInstance()[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()[0] target = target.addChild(TsReachabilityTarget.IntermediatePoint(firstIf)) + // if (calculator.getValue() === 25) + val secondIf = method.cfg.stmts.filterIsInstance()[1] + target = target.addChild(TsReachabilityTarget.IntermediatePoint(secondIf)) + // return 1 val returnStmt = method.cfg.stmts.filterIsInstance()[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" ) } } diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt index 38db366450..49bda77f08 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/FieldAccessReachabilityTest.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 field access reachability scenarios. @@ -36,7 +34,7 @@ class FieldAccessReachabilityTest { 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 FieldAccessReachabilityTest { target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) val results = machine.analyze(listOf(method), listOf(initialTarget)) - assertEquals( - 1, - results.size, - "Expected exactly one result for field access reachable path, but got ${results.size}" + assertTrue( + results.isNotEmpty(), + "Expected at least one result", ) val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() @@ -108,10 +105,9 @@ class FieldAccessReachabilityTest { target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) val results = machine.analyze(listOf(method), listOf(initialTarget)) - assertEquals( - 1, - results.size, - "Expected exactly one result for field modification reachable path, but got ${results.size}" + assertTrue( + results.isNotEmpty(), + "Expected at least one result", ) val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() @@ -176,10 +172,9 @@ class FieldAccessReachabilityTest { target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) val results = machine.analyze(listOf(method), listOf(initialTarget)) - assertEquals( - 1, - results.size, - "Expected exactly one result for object creation reachable path, but got ${results.size}" + assertTrue( + results.isNotEmpty(), + "Expected at least one result", ) val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() @@ -215,7 +210,7 @@ class FieldAccessReachabilityTest { val results = machine.analyze(listOf(method), listOf(initialTarget)) assertTrue( results.isNotEmpty(), - "Expected at least one result for ambiguous field access, but got ${results.size}" + "Expected at least one result", ) val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() diff --git a/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt index 7cdc3a4c63..0ad63c6702 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/reachability/FunctionCallReachabilityTest.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 function call reachability scenarios. @@ -36,7 +34,7 @@ class FunctionCallReachabilityTest { 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 FunctionCallReachabilityTest { target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) val results = machine.analyze(listOf(method), listOf(initialTarget)) - assertEquals( - 1, - results.size, - "Expected exactly one result for simple call reachable path, but got ${results.size}" + assertTrue( + results.isNotEmpty(), + "Expected at least one result", ) val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() @@ -135,10 +132,9 @@ class FunctionCallReachabilityTest { target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) val results = machine.analyze(listOf(method), listOf(initialTarget)) - assertEquals( - 1, - results.size, - "Expected exactly one result for chained calls reachable path, but got ${results.size}" + assertTrue( + results.isNotEmpty(), + "Expected at least one result", ) val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() @@ -169,10 +165,9 @@ class FunctionCallReachabilityTest { target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) val results = machine.analyze(listOf(method), listOf(initialTarget)) - assertEquals( - 1, - results.size, - "Expected exactly one result for recursive call reachable path, but got ${results.size}" + assertTrue( + results.isNotEmpty(), + "Expected at least one result", ) val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() @@ -207,10 +202,9 @@ class FunctionCallReachabilityTest { target.addChild(TsReachabilityTarget.FinalPoint(returnStmt)) val results = machine.analyze(listOf(method), listOf(initialTarget)) - assertEquals( - 1, - results.size, - "Expected exactly one result for state modification reachable path, but got ${results.size}" + assertTrue( + results.isNotEmpty(), + "Expected at least one result", ) val reachedStatements = results.flatMap { it.pathNode.allStatements }.toSet() diff --git a/usvm-ts/src/test/resources/reachability/ComplexReachability.ts b/usvm-ts/src/test/resources/reachability/ComplexReachability.ts index e9b04e3126..71f54af325 100644 --- a/usvm-ts/src/test/resources/reachability/ComplexReachability.ts +++ b/usvm-ts/src/test/resources/reachability/ComplexReachability.ts @@ -29,9 +29,9 @@ class ComplexReachability { const arr = this.createNumberArray(input); const processedArr = this.processArray(arr); - if (processedArr.length > 0) { - if (processedArr[0] > input) { - return 1; // Reachable depending on input value + if (processedArr.length > 1) { + if (processedArr[1] === 3) { + return 1; // Reachable when input >= 2, processedArr = [1,3,5,...] } } return 0; @@ -45,8 +45,8 @@ class ComplexReachability { const doubled = calculator.getDoubled(); if (doubled === 30) { calculator.add(10); - if (calculator.getValue() === 40) { - return 1; // Reachable: 15 * 2 = 30, then 15 + 10 = 25, but getValue() returns current value + if (calculator.getValue() === 25) { + return 1; // Reachable: 15 + 10 = 25 } } return 0; From d926fd73f06520d0ba68d7be00bfd0480d9f5ecf Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 10 Sep 2025 13:14:51 +0300 Subject: [PATCH 5/8] Reuse assignToArrayIndex function --- .../org/usvm/machine/expr/CallApproximations.kt | 13 ++++++------- 1 file changed, 6 insertions(+), 7 deletions(-) diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt index 428267ef50..12145391e1 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt +++ b/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( From 118acc30871dafa44a4bc67c9d6e3c014348fd7e Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 10 Sep 2025 13:15:27 +0300 Subject: [PATCH 6/8] Add test with push-based array creation --- .../org/usvm/samples/arrays/InputArrays.kt | 11 +++++++++ .../resources/samples/arrays/InputArrays.ts | 24 +++++++++++++++++++ 2 files changed, 35 insertions(+) diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt index 9c23e8c085..1df2559bb2 100644 --- a/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt +++ b/usvm-ts/src/test/kotlin/org/usvm/samples/arrays/InputArrays.kt @@ -160,4 +160,15 @@ class InputArrays : TsMethodTestRunner() { }, ) } + + @Test + fun `test conditionalLength`() { + val method = getMethod("conditionalLength") + discoverProperties( + method = method, + { x, r -> + (r eq 1) && (x.number > 0.0) + }, + ) + } } diff --git a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts index 200a4c8814..af04a6f0c9 100644 --- a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts +++ b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts @@ -58,4 +58,28 @@ class InputArrays { return x; } + + conditionalLength(input: number) { + const arr = createNumberArray(input); + const res = processArray(arr); + if (res.length > 0) return 1; + if (input > 0) return -1; // unreachable, since 'input > 0' implies 'res.length > 0' + return 0; + } +} + +function createNumberArray(size: number): number[] { + const arr = []; + for (let i = 0; i < size && i < 5; i++) { + arr.push(i + 1); + } + return arr; +} + +function processArray(arr: number[]): number[] { + const result = []; + for (let i = 0; i < arr.length; i++) { + result.push(arr[i] * 2); + } + return result; } From 53c2ac901f132518cb40b219cb0860a5f7422a69 Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 10 Sep 2025 14:19:32 +0300 Subject: [PATCH 7/8] Fix test --- usvm-ts/src/test/resources/samples/arrays/InputArrays.ts | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts index af04a6f0c9..7de52221cd 100644 --- a/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts +++ b/usvm-ts/src/test/resources/samples/arrays/InputArrays.ts @@ -60,8 +60,8 @@ class InputArrays { } conditionalLength(input: number) { - const arr = createNumberArray(input); - const res = processArray(arr); + const arr: number[] = createNumberArray(input); + const res: number[] = processArray(arr); if (res.length > 0) return 1; if (input > 0) return -1; // unreachable, since 'input > 0' implies 'res.length > 0' return 0; @@ -69,7 +69,7 @@ class InputArrays { } function createNumberArray(size: number): number[] { - const arr = []; + const arr = new Array(); for (let i = 0; i < size && i < 5; i++) { arr.push(i + 1); } @@ -77,7 +77,7 @@ function createNumberArray(size: number): number[] { } function processArray(arr: number[]): number[] { - const result = []; + const result = new Array(); for (let i = 0; i < arr.length; i++) { result.push(arr[i] * 2); } From 4b3107f7d5127e20002007745d1ae61b64b4ecfa Mon Sep 17 00:00:00 2001 From: Konstantin Chukharev Date: Wed, 10 Sep 2025 14:54:20 +0300 Subject: [PATCH 8/8] Fix test [2] --- .../test/resources/reachability/ComplexReachability.ts | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/usvm-ts/src/test/resources/reachability/ComplexReachability.ts b/usvm-ts/src/test/resources/reachability/ComplexReachability.ts index 71f54af325..6693891be9 100644 --- a/usvm-ts/src/test/resources/reachability/ComplexReachability.ts +++ b/usvm-ts/src/test/resources/reachability/ComplexReachability.ts @@ -26,8 +26,8 @@ class ComplexReachability { // Method calls with array manipulation methodArrayManipulationReachable(input: number): number { - const arr = this.createNumberArray(input); - const processedArr = this.processArray(arr); + const arr: number[] = this.createNumberArray(input); + const processedArr: number[] = this.processArray(arr); if (processedArr.length > 1) { if (processedArr[1] === 3) { @@ -127,7 +127,7 @@ class ComplexReachability { // Helper methods createNumberArray(size: number): number[] { - const arr = []; + const arr = new Array(); for (let i = 0; i < size && i < 5; i++) { arr.push(i * 2); } @@ -135,7 +135,7 @@ class ComplexReachability { } processArray(arr: number[]): number[] { - const result = []; + const result = new Array(); for (let i = 0; i < arr.length; i++) { result.push(arr[i] + 1); }