[TS] Arrays methods #304

CaelmBleidd · 2025-07-09T13:29:43Z

This PR adds approximations for some Array methods: push, pop, fill, shift, unshift, join, slice, concat, indexOf, includes, reverse.

In most cases, only single-argument (and non-array) calls (where it is applicable) are supported for now. For example, Array.unshift(...items) prepends items to the left, but we currently assume unshift receives a single value.

In all methods that receive start/end indices (e.g. slice or fill), negative indices are not yet supported.

In Array.fill and Array.reverse, only relatively small arrays are supported (of size at most 10000 and 5000, respectively), since it is (yet) impossible to create a symbolic array of symbolic length.

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

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt

usvm-ts/src/test/resources/samples/arrays/ArraysMethods.ts

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

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt

Lipen

🚀

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

+ */
+private fun TsExprResolver.handleArrayJoin(
+    expr: EtsInstanceCallExpr,
+    arrayType: EtsArrayType,


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

+private fun TsExprResolver.handleArrayJoin(
+    expr: EtsInstanceCallExpr,
+    arrayType: EtsArrayType,
+    elementSort: USort,


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

+private fun TsExprResolver.handleArrayIndexOf(
+    expr: EtsInstanceCallExpr,
+    arrayType: EtsArrayType,
+    elementSort: USort,


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

+ */
+private fun TsExprResolver.handleArrayIncludes(
+    expr: EtsInstanceCallExpr,
+    arrayType: EtsArrayType,


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

+private fun TsExprResolver.handleArrayIncludes(
+    expr: EtsInstanceCallExpr,
+    arrayType: EtsArrayType,
+    elementSort: USort,


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

usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt

+
+    /**


Copilot

Pull Request Overview

This PR adds approximations for several TypeScript array methods (push, pop, fill, shift, unshift) to enable symbolic execution. The implementation focuses on single-argument calls and includes test cases to verify the behavior of these array operations.

Implements array method approximations with proper memory management and length tracking
Refactors string constant handling to improve state management
Adds comprehensive test coverage for the new array methods

Reviewed Changes

Copilot reviewed 9 out of 9 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
`usvm-ts/src/test/resources/samples/arrays/ArrayMethods.ts`	TypeScript test samples for array methods including push, pop, fill, shift, unshift, join, slice, concat, indexOf, includes, and reverse
`usvm-ts/src/test/kotlin/org/usvm/util/TsTestResolver.kt`	Minor refactor to extract string constant value retrieval logic
`usvm-ts/src/test/kotlin/org/usvm/samples/arrays/ArrayMethods.kt`	Test implementations verifying array method behavior through symbolic execution
`usvm-ts/src/test/kotlin/org/usvm/project/DemoCalc.kt`	Updates test configuration for demo calculator project
`usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt`	Adds string constant tracking and initialization methods to state management
`usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt`	Fixes array type resolution for allocated heap references
`usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt`	Refactors expression resolution by extracting call approximations
`usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt`	New file implementing array method approximations and call handling logic
`usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt`	Refactors string constant management for better separation of concerns

Comments suppressed due to low confidence (1)

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

The documentation is incorrect. According to the ECMAScript specification, Array.concat() returns a new array and does not modify the original array in place.

 * https://tc39.es/ecma262/multipage/indexed-collections.html#sec-array.prototype.concat

usvm-ts/src/test/resources/samples/arrays/ArrayMethods.ts

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

usvm-ts/src/test/kotlin/org/usvm/samples/arrays/ArrayMethods.kt

CaelmBleidd · 2025-08-05T10:00:54Z

@Lipen please, take a look at the comments

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

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt

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

+    elementSort: USort,
+): UExpr<*>? = with(ctx) {
+    val array = resolve(expr.instance)?.asExpr(addressSort) ?: return null
+    check(expr.args.size >= 1 && expr.args.size <= 3) {


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

+    } else {
+        mkBv(0)
+    }
+    val startBv: UExpr<TsSizeSort> = when (start.sort) {


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

+        val lengthLValue = mkArrayLengthLValue(array, arrayType)
+        scope.calcOnState { memory.read(lengthLValue) }
+    }
+    val endBv: UExpr<TsSizeSort> = when (end.sort) {


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

+    check(expr.args.size == 1) {
+        "Array.indexOf() should have exactly one argument, but got ${expr.args.size}"
+    }
+    val searchElement = resolve(expr.args.single()) ?: return null


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

+    check(expr.args.size == 1) {
+        "Array.includes() should have exactly one argument, but got ${expr.args.size}"
+    }
+    val searchElement = resolve(expr.args.single()) ?: return null


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

+            }
+        )
+
+        //! Note: `reversedArray` is a temporary object not used outside this function,


CaelmBleidd requested a review from Lipen July 9, 2025 13:29

CaelmBleidd changed the title ~~Caelmbleidd/shift method~~ [TS] Arrays methods Jul 9, 2025

Lipen reviewed Jul 9, 2025

View reviewed changes

usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt Outdated Show resolved Hide resolved

Lipen reviewed Jul 9, 2025

View reviewed changes

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt Outdated Show resolved Hide resolved

usvm-ts/src/test/resources/samples/arrays/ArraysMethods.ts Outdated Show resolved Hide resolved

CaelmBleidd requested a review from Lipen July 10, 2025 09:34

CaelmBleidd force-pushed the caelmbleidd/lt branch from 3cada77 to dd67fdc Compare July 11, 2025 13:25

CaelmBleidd force-pushed the caelmbleidd/shift_method branch from 9187a68 to b71e504 Compare July 11, 2025 13:25

Lipen force-pushed the caelmbleidd/lt branch from 1223b18 to d5c85fa Compare July 11, 2025 15:05

Base automatically changed from caelmbleidd/lt to main July 11, 2025 17:32

Lipen force-pushed the caelmbleidd/shift_method branch from b71e504 to 1209ec8 Compare August 1, 2025 12:38

github-advanced-security bot found potential problems Aug 1, 2025

View reviewed changes

usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt Fixed Show fixed Hide fixed

usvm-ts/src/main/kotlin/org/usvm/machine/interpreter/TsInterpreter.kt Fixed Show fixed Hide fixed

Lipen approved these changes Aug 1, 2025

View reviewed changes

Lipen force-pushed the caelmbleidd/shift_method branch from bdc0374 to 6d4b763 Compare August 1, 2025 13:20

github-advanced-security bot found potential problems Aug 4, 2025

View reviewed changes

Lipen requested a review from Copilot August 4, 2025 12:17

Copilot AI reviewed Aug 4, 2025

View reviewed changes

UnitTestBot deleted a comment from Copilot AI Aug 5, 2025

CaelmBleidd commented Aug 5, 2025

View reviewed changes

github-advanced-security bot found potential problems Aug 5, 2025

View reviewed changes

CaelmBleidd commented Aug 5, 2025

View reviewed changes

usvm-ts/src/main/kotlin/org/usvm/machine/expr/CallApproximations.kt Outdated Show resolved Hide resolved

Lipen force-pushed the caelmbleidd/shift_method branch from e0488d3 to da024c5 Compare August 5, 2025 15:21

github-advanced-security bot found potential problems Aug 5, 2025

View reviewed changes

usvm-ts/src/main/kotlin/org/usvm/machine/TsContext.kt Dismissed Show dismissed Hide dismissed

Array methods approximations

7a5a1ce

CaelmBleidd force-pushed the caelmbleidd/shift_method branch from 41bb8a0 to 7a5a1ce Compare August 6, 2025 09:05

CaelmBleidd commented Aug 7, 2025

View reviewed changes

Lipen added 4 commits August 7, 2025 12:29

Add warnings for symbolically approximated methods

1a22b89

Support start/end in Array.fill. Use mkBv

fff54be

Comment

a8c1e6c

Add examples

dd1e57c

github-advanced-security bot found potential problems Aug 7, 2025

View reviewed changes

Lipen merged commit 419eb50 into main Aug 7, 2025
6 checks passed

Lipen deleted the caelmbleidd/shift_method branch August 7, 2025 10:31

[TS] Arrays methods #304

[TS] Arrays methods #304

Uh oh!

Conversation

CaelmBleidd commented Jul 9, 2025 • edited by Lipen Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Lipen left a comment

Choose a reason for hiding this comment

Uh oh!

Check warning

Check warning

Uh oh!

Uh oh!

Check warning

Uh oh!

Check warning

Check warning

Uh oh!

Check warning

Copilot AI left a comment

Choose a reason for hiding this comment

Pull Request Overview

Reviewed Changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

CaelmBleidd commented Aug 5, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Check warning

Check warning

Check warning

Check warning

Check warning

Check warning

Uh oh!

Uh oh!

CaelmBleidd commented Jul 9, 2025 •

edited by Lipen

Loading