[TS] Preserve Promise executor closures and settlement arguments

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

@@ -13,6 +13,7 @@ import org.jacodb.ets.model.EtsRefType
 import org.jacodb.ets.model.EtsStringType
 import org.jacodb.ets.model.EtsUnclearRefType
 import org.jacodb.ets.model.EtsUnknownType
+import org.jacodb.ets.model.EtsValue
 import org.jacodb.ets.utils.CONSTRUCTOR_NAME
 import org.usvm.UBoolExpr
 import org.usvm.UConcreteHeapRef
@@ -474,6 +475,10 @@ private fun TsExprResolver.handlePromiseConstructor(expr: EtsInstanceCallExpr):
         "Promise constructor should have exactly one argument, but got ${expr.args.size}"
     }
     val executorLocal = expr.args.single()
+    val executorValue = resolve(executorLocal) ?: return null
+    val executorFunction = (executorValue as? UConcreteHeapRef)?.let { ref ->
+        scope.calcOnState { associatedFunction[ref] }
+    }
 
     // Lookup the executor method
     val executors = resolveEtsMethods(
@@ -499,6 +504,9 @@ private fun TsExprResolver.handlePromiseConstructor(expr: EtsInstanceCallExpr):
     // Save the executor for the promise in the state
     scope.doWithState {
         setPromiseExecutor(promise, executor)
+        if (executorFunction != null) {
+            promiseExecutorFunctions += promise to executorFunction
+        }
     }
 
     promise
@@ -510,10 +518,7 @@ private fun TsExprResolver.handlePromiseResolveReject(expr: EtsInstanceCallExpr)
         "reject" -> PromiseState.REJECTED
         else -> error("Unexpected: $expr")
     }
-    check(expr.args.size == 1) {
-        "Promise.${expr.callee.name}() should have exactly one argument, but got ${expr.args.size}"
-    }
-    val value = resolve(expr.args.single()) ?: return null
+    val value = resolvePromiseSettlementArguments(expr.args) ?: return null
 
     if (newState == PromiseState.FULFILLED) {
         val existingPromise = existingPromiseOrEnsureNonThenable(
@@ -1573,3 +1578,14 @@ private fun TsExprResolver.handleArrayReverse(
         array
     }
 }
+
+/** Missing settlement values are undefined; extra arguments are evaluated before being ignored. */
+internal fun TsExprResolver.resolvePromiseSettlementArguments(arguments: List<EtsValue>): UExpr<*>? {
+    var first: UExpr<*> = ctx.mkUndefinedValue()
+    for ((index, argument) in arguments.withIndex()) {
+        val value = resolve(argument) ?: return null
+        if (index == 0) first = value
+    }
+
+    return first
+}

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

@@ -748,14 +748,15 @@ class TsExprResolver(
     ): List<UExpr<*>> = with(ctx) {
         val args: MutableList<UExpr<*>> = mutableListOf()
 
-        // Executor lambda does not have 'this', so we fill it with 'undefined':
-        args += mkUndefinedValue()
+        val function = scope.calcOnState { promiseExecutorFunctions[promise] }
+        args += function?.thisInstance ?: mkUndefinedValue()
 
         val params = executor.parameters.toMutableList()
         if (params.isNotEmpty() && params[0].type is EtsLexicalEnvType) {
             params.removeFirst()
-            // TODO: handle closures
-            args += mkUndefinedValue()
+            val closure = function?.closure
+                ?: throw UnsupportedOperationException("Promise executor closure is unavailable")
+            args += closure
         }
 
         if (params.isNotEmpty()) {
@@ -1372,10 +1373,7 @@ class TsExprResolver(
                 if (isAllocatedConcreteHeapRef(ptr)) {
                     val callback = scope.calcOnState { promiseCallbacks[ptr] }
                     if (callback != null) {
-                        check(expr.args.size == 1) {
-                            "Promise settlement callback should have exactly one argument, but got ${expr.args.size}"
-                        }
-                        val value = resolve(expr.args.single()) ?: return null
+                        val value = resolvePromiseSettlementArguments(expr.args) ?: return null
                         val fakeValue = value.toFakeObject(scope) ?: return null
                         scope.doWithState {
                             if (!isResolved(callback.promise)) {

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

@@ -100,19 +100,15 @@ class TsState(
     internal var initializedArrayIndices: Map<UHeapRef, Map<UExpr<TsSizeSort>, UBoolExpr>> = emptyMap(),
     var boundThis: UPersistentHashMap<UConcreteHeapRef, UHeapRef> = persistentHashMapOf(),
     var dfltObject: UPersistentHashMap<EtsFileSignature, UConcreteHeapRef> = persistentHashMapOf(),
-
     /**
      * Maps (file signature, field name) to the sort used for that field in the dflt object.
      * This tracks sorts for global variables that are represented as fields of dflt objects.
      */
     var dfltObjectFieldSorts: UPersistentHashMap<Pair<EtsFileSignature, String>, USort> = persistentHashMapOf(),
-
     /** True while an auxiliary entry-point guard or one of its callees is executing. */
     var entryPointGuardActive: Boolean = false,
-
     /** Terminal guard outcome; [TsEntryPointGuardOutcome.NONE] also covers predicate execution. */
     var entryPointGuardOutcome: TsEntryPointGuardOutcome = TsEntryPointGuardOutcome.NONE,
-
     /**
      * Maps string values to their corresponding heap references that were allocated for string constants.
      * This tracks which string constants have been initialized in this particular state to avoid
@@ -150,6 +146,8 @@ class TsState(
     forkPoints = forkPoints,
     targets = targets,
 ) {
+    internal var promiseExecutorFunctions: Map<UConcreteHeapRef, TsFunction> = emptyMap()
+
     internal var initialEnvironmentFailure: String? = null
     internal var initialEnvironmentHeaps: Map<EtsClass, TsInitialEnvironmentHeap> = emptyMap()
     internal var initialEnvironmentSlots: Map<Pair<EtsClass, String>, TsInitialEnvironmentSlot> = emptyMap()
@@ -419,6 +417,7 @@ class TsState(
             denseInputArrays = denseInputArrays.toMutableMap(),
             activeUnknownCallModels = activeUnknownCallModels.toMutableList(),
         ).also { cloned ->
+            cloned.promiseExecutorFunctions = promiseExecutorFunctions
             cloned.initialEnvironmentFailure = initialEnvironmentFailure
             cloned.initialEnvironmentHeaps = initialEnvironmentHeaps
             cloned.initialEnvironmentSlots = initialEnvironmentSlots

usvm-ts/src/test/kotlin/org/usvm/machine/expr/PromiseSettlementArityTest.kt

@@ -0,0 +1,133 @@
+package org.usvm.machine.expr
+
+import org.jacodb.ets.model.EtsMethod
+import org.junit.jupiter.api.io.TempDir
+import org.usvm.PathSelectionStrategy
+import org.usvm.StateCollectionStrategy
+import org.usvm.UConcreteHeapRef
+import org.usvm.UMachineOptions
+import org.usvm.api.TsTest
+import org.usvm.api.TsTestValue
+import org.usvm.machine.TsMachine
+import org.usvm.machine.TsOptions
+import org.usvm.machine.interpreter.PromiseState
+import org.usvm.machine.interpreter.getResolvedValue
+import org.usvm.machine.state.TsMethodResult
+import org.usvm.util.TsMethodTestRunner
+import org.usvm.util.TsTestResolver
+import org.usvm.util.assertNodeReplay
+import org.usvm.util.getResourcePath
+import java.nio.file.Path
+import kotlin.io.path.readText
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertIs
+
+class PromiseSettlementArityTest : TsMethodTestRunner() {
+    override val scene = loadScene("/models/PromiseSettlementArity.ts")
+    override val tsOptions = TsOptions(eraseTypeAssertions = true)
+
+    // Entry-point async returns are Promises. Inspect their fulfilled payload, the value observed by await,
+    // rather than asking the ordinary object witness resolver to reconstruct a native Promise instance.
+    override val runner: (EtsMethod, UMachineOptions) -> List<TsTest> = { method, machineOptions ->
+        TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine ->
+            machine.analyze(listOf(method)).map { state ->
+                val completion = assertIs<TsMethodResult.Success>(state.methodResult)
+                val promise = assertIs<UConcreteHeapRef>(completion.value)
+                assertEquals(PromiseState.FULFILLED, state.promiseState[promise])
+
+                val resultState = state.clone()
+                val payload = resultState.getResolvedValue(promise, resultState.ctx.addressSort)
+                resultState.methodResult = TsMethodResult.Success.MockedCall(payload, method.signature)
+                TsTestResolver().resolve(method, resultState)
+            }
+        }
+    }
+
+    @TempDir
+    lateinit var directory: Path
+
+    init {
+        options = options.copy(
+            pathSelectionStrategies = listOf(PathSelectionStrategy.BFS),
+            stateCollectionStrategy = StateCollectionStrategy.ALL,
+            stopOnCoverage = 0,
+            throwExceptionOnStepFailure = true,
+        )
+    }
+
+    @Test
+    fun `resolveMissing follows ordinary Promise semantics`() {
+        assertOne(methodName = "resolveMissing")
+    }
+
+    @Test
+    fun `rejectMissing follows ordinary Promise semantics`() {
+        assertOne(methodName = "rejectMissing")
+    }
+
+    @Test
+    fun `resolveExtra follows ordinary Promise semantics`() {
+        assertOne(methodName = "resolveExtra")
+    }
+
+    @Test
+    fun `rejectExtra follows ordinary Promise semantics`() {
+        assertOne(methodName = "rejectExtra")
+    }
+
+    @Test
+    fun `callbackResolveMissing follows ordinary Promise semantics`() {
+        assertOne(methodName = "callbackResolveMissing")
+    }
+
+    @Test
+    fun `callbackRejectMissing follows ordinary Promise semantics`() {
+        assertOne(methodName = "callbackRejectMissing")
+    }
+
+    @Test
+    fun `firstSettlementWins follows ordinary Promise semantics`() {
+        assertOne(methodName = "firstSettlementWins")
+    }
+
+    @Test
+    fun `callbackExtra follows ordinary Promise semantics`() {
+        assertOne(methodName = "callbackExtra")
+    }
+
+    @Test
+    fun `native Promise confirms missing extra and repeated settlements`() {
+        val source = getResourcePath("/models/PromiseSettlementArity.ts").readText()
+        val methods = listOf(
+            "resolveMissing",
+            "rejectMissing",
+            "resolveExtra",
+            "rejectExtra",
+            "callbackResolveMissing",
+            "callbackRejectMissing",
+            "firstSettlementWins",
+            "callbackExtra",
+        )
+        val calls = methods.joinToString(separator = "\n") { name ->
+            "if (await PromiseSettlementArity.$name() !== 1) throw Error('$name');"
+        }
+
+        val invoke = "\n(async () => { $calls })().catch(error => { console.error(error); process.exitCode = 1; });"
+
+        assertNodeReplay(
+            source = source + invoke,
+            directory = directory,
+            name = "promise-settlement-arity",
+            timeoutMessage = "Native Promise settlement regression timed out",
+        )
+    }
+
+    private fun assertOne(methodName: String) {
+        discoverProperties<TsTestValue.TsNumber>(
+            method = getMethod(methodName = methodName, className = "PromiseSettlementArity"),
+            { result -> result.number == 1.0 },
+            invariants = arrayOf({ result -> result.number == 1.0 }),
+        )
+    }
+}

usvm-ts/src/test/resources/models/PromiseSettlementArity.ts

@@ -0,0 +1,47 @@
+// @ts-nocheck
+export class PromiseSettlementArity {
+    static async resolveMissing(): Promise<number> {
+        const value = await Promise.resolve();
+        return value === undefined ? 1 : 0;
+    }
+
+    static async rejectMissing(): Promise<number> {
+        try { await Promise.reject(); } catch (value) { return value === undefined ? 1 : 0; }
+        return 0;
+    }
+
+    static async resolveExtra(): Promise<number> {
+        let effects = 0;
+        const value = await Promise.resolve(7, ++effects);
+        return value === 7 && effects === 1 ? 1 : 0;
+    }
+
+    static async rejectExtra(): Promise<number> {
+        let effects = 0;
+        try { await Promise.reject(7, ++effects); }
+        catch (value) { return value === 7 && effects === 1 ? 1 : 0; }
+        return 0;
+    }
+
+    static async callbackResolveMissing(): Promise<number> {
+        const value = await new Promise<void>((resolve) => resolve());
+        return value === undefined ? 1 : 0;
+    }
+
+    static async callbackRejectMissing(): Promise<number> {
+        try { await new Promise<void>((resolve, reject) => reject()); }
+        catch (value) { return value === undefined ? 1 : 0; }
+        return 0;
+    }
+
+    static async firstSettlementWins(): Promise<number> {
+        const value = await new Promise<number>((resolve: any) => { resolve(7); resolve(); });
+        return value === 7 ? 1 : 0;
+    }
+
+    static async callbackExtra(): Promise<number> {
+        const counter = { effects: 0 };
+        const value = await new Promise<number>((resolve: any) => resolve(7, ++counter.effects));
+        return value === 7 && counter.effects === 1 ? 1 : 0;
+    }
+}