[TS] Support PtrCall (#311)

Author: Lipen

.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-06-24"
+          BRANCH="neo/2025-07-18"
 
           for ((i=1; i<=MAX_RETRIES; i++)); do
               git clone --depth=1 --branch $BRANCH $REPO_URL $DEST_DIR && break
@@ -177,6 +177,9 @@ jobs:
       - name: Setup Gradle
         uses: gradle/actions/setup-gradle@v4
 
+      - name: Show project list
+        run: ./gradlew projects
+
       - name: Validate Project List
         run: ./gradlew validateProjectList
 

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 = "081adc271e"
+    const val jacodb = "5acbadfed0"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

settings.gradle.kts

@@ -12,7 +12,7 @@ pluginManagement {
 
 plugins {
     // https://plugins.gradle.org/plugin/com.gradle.develocity
-    id("com.gradle.develocity") version("4.0.2")
+    id("com.gradle.develocity") version "4.0.2"
 }
 
 develocity {
@@ -55,4 +55,18 @@ findProject(":usvm-python:usvm-python-commons")?.name = "usvm-python-commons"
 // Actually, `includeBuild("../jacodb")` is enough, but there is a bug in IDEA when path is a symlink.
 // As a workaround, we convert it to a real absolute path.
 // See IDEA bug: https://youtrack.jetbrains.com/issue/IDEA-329756
-// includeBuild(file("../jacodb").toPath().toRealPath().toAbsolutePath())
+// val jacodbPath = file("jacodb").takeIf { it.exists() }
+//     ?: file("../jacodb").takeIf { it.exists() }
+//     ?: error("Local JacoDB directory not found")
+// includeBuild(jacodbPath.toPath().toRealPath().toAbsolutePath()) {
+//     dependencySubstitution {
+//         all {
+//             val requested = requested
+//             if (requested is ModuleComponentSelector && requested.group == "com.github.UnitTestBot.jacodb") {
+//                 val targetProject = ":${requested.module}"
+//                 useTarget(project(targetProject))
+//                 logger.info("Substituting ${requested.group}:${requested.module} with $targetProject")
+//             }
+//         }
+//     }
+// }

usvm-core/src/main/kotlin/org/usvm/Context.kt

@@ -94,7 +94,7 @@ open class UContext<USizeSort : USort>(
     val addressSort: UAddressSort = mkUninterpretedSort("Address")
     val nullRef: UNullRef = UNullRef(this)
 
-    fun mkNullRef(): USymbolicHeapRef {
+    open fun mkNullRef(): USymbolicHeapRef {
         return nullRef
     }
 

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

@@ -25,6 +25,7 @@ import org.jacodb.ets.dto.EnumValueTypeDto
 import org.jacodb.ets.dto.FunctionTypeDto
 import org.jacodb.ets.dto.GenericTypeDto
 import org.jacodb.ets.dto.IntersectionTypeDto
+import org.jacodb.ets.dto.LexicalEnvTypeDto
 import org.jacodb.ets.dto.LiteralTypeDto
 import org.jacodb.ets.dto.LocalSignatureDto
 import org.jacodb.ets.dto.NeverTypeDto
@@ -48,6 +49,7 @@ import org.jacodb.ets.model.EtsEnumValueType
 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
@@ -104,6 +106,14 @@ private object EtsTypeToDto : EtsType.Visitor<TypeDto> {
         )
     }
 
+    override fun visit(type: EtsLexicalEnvType): TypeDto {
+        @Suppress("DEPRECATION")
+        return LexicalEnvTypeDto(
+            method = type.nestedMethod.toDto(),
+            closures = type.closures.map { it.toDto() },
+        )
+    }
+
     override fun visit(type: EtsEnumValueType): TypeDto {
         return EnumValueTypeDto(
             signature = type.signature.toDto(),

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

@@ -17,7 +17,10 @@
 package org.usvm.dataflow.ts.infer.dto
 
 import org.jacodb.ets.dto.ArrayRefDto
+import org.jacodb.ets.dto.CaughtExceptionRefDto
+import org.jacodb.ets.dto.ClosureFieldRefDto
 import org.jacodb.ets.dto.ConstantDto
+import org.jacodb.ets.dto.GlobalRefDto
 import org.jacodb.ets.dto.InstanceFieldRefDto
 import org.jacodb.ets.dto.LocalDto
 import org.jacodb.ets.dto.ParameterRefDto
@@ -26,7 +29,10 @@ import org.jacodb.ets.dto.ThisRefDto
 import org.jacodb.ets.dto.ValueDto
 import org.jacodb.ets.model.EtsArrayAccess
 import org.jacodb.ets.model.EtsBooleanConstant
+import org.jacodb.ets.model.EtsCaughtExceptionRef
+import org.jacodb.ets.model.EtsClosureFieldRef
 import org.jacodb.ets.model.EtsConstant
+import org.jacodb.ets.model.EtsGlobalRef
 import org.jacodb.ets.model.EtsInstanceFieldRef
 import org.jacodb.ets.model.EtsLocal
 import org.jacodb.ets.model.EtsNullConstant
@@ -112,4 +118,25 @@ private object EtsValueToDto : EtsValue.Visitor<ValueDto> {
             field = value.field.toDto(),
         )
     }
+
+    override fun visit(value: EtsCaughtExceptionRef): ValueDto {
+        return CaughtExceptionRefDto(
+            type = value.type.toDto(),
+        )
+    }
+
+    override fun visit(value: EtsGlobalRef): ValueDto {
+        return GlobalRefDto(
+            name = value.name,
+            ref = value.ref?.toDto(),
+        )
+    }
+
+    override fun visit(value: EtsClosureFieldRef): ValueDto {
+        return ClosureFieldRefDto(
+            base = value.base.toDto(),
+            fieldName = value.fieldName,
+            type = value.type.toDto(),
+        )
+    }
 }

usvm-ts/src/main/kotlin/org/usvm/api/TsMock.kt

@@ -0,0 +1,38 @@
+package org.usvm.api
+
+import org.jacodb.ets.model.EtsMethodSignature
+import org.jacodb.ets.model.EtsVoidType
+import org.usvm.UAddressSort
+import org.usvm.UExpr
+import org.usvm.machine.expr.TsUnresolvedSort
+import org.usvm.machine.interpreter.TsStepScope
+import org.usvm.machine.state.TsMethodResult
+import org.usvm.machine.types.mkFakeValue
+
+fun mockMethodCall(
+    scope: TsStepScope,
+    method: EtsMethodSignature,
+) {
+    scope.doWithState {
+        val result: UExpr<*>
+        if (method.returnType is EtsVoidType) {
+            result = ctx.mkUndefinedValue()
+        } else {
+            val sort = ctx.typeToSort(method.returnType)
+            result = when (sort) {
+                is UAddressSort -> makeSymbolicRefUntyped()
+
+                is TsUnresolvedSort -> ctx.mkFakeValue(
+                    scope,
+                    makeSymbolicPrimitive(ctx.boolSort),
+                    makeSymbolicPrimitive(ctx.fp64Sort),
+                    makeSymbolicRefUntyped()
+                )
+
+                else -> makeSymbolicPrimitive(sort)
+            }
+        }
+
+        methodResult = TsMethodResult.Success.MockedCall(result, method)
+    }
+}

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

@@ -58,11 +58,16 @@ class TsContext(
     val voidSort: TsVoidSort by lazy { TsVoidSort(this) }
     val voidValue: TsVoidValue by lazy { TsVoidValue(this) }
 
+    @Deprecated("Use mkUndefinedValue() or mkTsNullValue() instead")
+    override fun mkNullRef(): Nothing {
+        error("Use mkUndefinedValue() or mkTsNullValue() instead of mkNullRef() in TS context")
+    }
+
     /**
      * In TS we treat undefined value as a null reference in other objects.
      * For real null represented in the language we create another reference.
      */
-    private val undefinedValue: UHeapRef = mkNullRef()
+    private val undefinedValue: UHeapRef = nullRef
     fun mkUndefinedValue(): UHeapRef = undefinedValue
 
     private val nullValue: UConcreteHeapRef = mkConcreteHeapRef(addressCounter.freshStaticAddress())
@@ -181,7 +186,7 @@ class TsContext(
     }
 
     fun createFakeObjectRef(): UConcreteHeapRef {
-        val address = mkAddressCounter().freshAllocatedAddress() + MAGIC_OFFSET
+        val address = addressCounter.freshAllocatedAddress() + MAGIC_OFFSET
         return mkConcreteHeapRef(address)
     }
 
@@ -263,6 +268,14 @@ class TsContext(
             ref
         }
     }
+
+    // This is an identifier for a special function representing the 'resolve' function used in promises.
+    // It is not a real function in the code, but we need it to handle promise resolution.
+    val resolveFunctionRef: UConcreteHeapRef = allocateConcreteRef()
+
+    // This is an identifier for a special function representing the 'reject' function used in promises.
+    // It is not a real function in the code, but we need it to handle promise rejection.
+    val rejectFunctionRef: UConcreteHeapRef = allocateConcreteRef()
 }
 
 class Constants {

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

@@ -7,7 +7,7 @@ import org.jacodb.ets.model.EtsStmtLocation
 import org.usvm.UExpr
 
 sealed interface TsMethodCall : EtsStmt {
-    val instance: UExpr<*>?
+    val instance: UExpr<*>
     val args: List<UExpr<*>>
     val returnSite: EtsStmt
 
@@ -21,7 +21,7 @@ sealed interface TsMethodCall : EtsStmt {
 
 class TsVirtualMethodCallStmt(
     val callee: EtsMethodSignature,
-    override val instance: UExpr<*>?,
+    override val instance: UExpr<*>,
     override val args: List<UExpr<*>>,
     override val returnSite: EtsStmt,
 ) : TsMethodCall {
@@ -38,7 +38,7 @@ class TsVirtualMethodCallStmt(
 //  and not wrapped in array (if calling a vararg method)
 class TsConcreteMethodCallStmt(
     val callee: EtsMethod,
-    override val instance: UExpr<*>?,
+    override val instance: UExpr<*>,
     override val args: List<UExpr<*>>,
     override val returnSite: EtsStmt,
 ) : TsMethodCall {