From 0ab6234672d337d46bde43571ea4df4f439069ad Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Tue, 20 Oct 2026 12:21:36 +0300 Subject: [PATCH] Preserve Promise executor closures and settlement argument semantics --- .../usvm/machine/expr/CallApproximations.kt | 24 +++- .../org/usvm/machine/expr/TsExprResolver.kt | 14 +- .../kotlin/org/usvm/machine/state/TsState.kt | 7 +- .../expr/PromiseSettlementArityTest.kt | 133 ++++++++++++++++++ .../models/PromiseSettlementArity.ts | 47 +++++++ 5 files changed, 209 insertions(+), 16 deletions(-) create mode 100644 usvm-ts/src/test/kotlin/org/usvm/machine/expr/PromiseSettlementArityTest.kt create mode 100644 usvm-ts/src/test/resources/models/PromiseSettlementArity.ts 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 160e341659..15fab96a6e 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 @@ -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): 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 +} diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt index 9da950ce8e..05a2b4314c 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/expr/TsExprResolver.kt @@ -748,14 +748,15 @@ class TsExprResolver( ): List> = with(ctx) { val args: MutableList> = 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)) { diff --git a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt index 9a3e28cba2..a764a51afc 100644 --- a/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt +++ b/usvm-ts/src/main/kotlin/org/usvm/machine/state/TsState.kt @@ -100,19 +100,15 @@ class TsState( internal var initializedArrayIndices: Map, UBoolExpr>> = emptyMap(), var boundThis: UPersistentHashMap = persistentHashMapOf(), var dfltObject: UPersistentHashMap = 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, 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 = emptyMap() + internal var initialEnvironmentFailure: String? = null internal var initialEnvironmentHeaps: Map = emptyMap() internal var initialEnvironmentSlots: Map, 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 diff --git a/usvm-ts/src/test/kotlin/org/usvm/machine/expr/PromiseSettlementArityTest.kt b/usvm-ts/src/test/kotlin/org/usvm/machine/expr/PromiseSettlementArityTest.kt new file mode 100644 index 0000000000..365aad0e96 --- /dev/null +++ b/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 = { method, machineOptions -> + TsMachine(scene = scene, options = machineOptions, tsOptions = tsOptions).use { machine -> + machine.analyze(listOf(method)).map { state -> + val completion = assertIs(state.methodResult) + val promise = assertIs(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( + method = getMethod(methodName = methodName, className = "PromiseSettlementArity"), + { result -> result.number == 1.0 }, + invariants = arrayOf({ result -> result.number == 1.0 }), + ) + } +} diff --git a/usvm-ts/src/test/resources/models/PromiseSettlementArity.ts b/usvm-ts/src/test/resources/models/PromiseSettlementArity.ts new file mode 100644 index 0000000000..71f7a231e1 --- /dev/null +++ b/usvm-ts/src/test/resources/models/PromiseSettlementArity.ts @@ -0,0 +1,47 @@ +// @ts-nocheck +export class PromiseSettlementArity { + static async resolveMissing(): Promise { + const value = await Promise.resolve(); + return value === undefined ? 1 : 0; + } + + static async rejectMissing(): Promise { + try { await Promise.reject(); } catch (value) { return value === undefined ? 1 : 0; } + return 0; + } + + static async resolveExtra(): Promise { + let effects = 0; + const value = await Promise.resolve(7, ++effects); + return value === 7 && effects === 1 ? 1 : 0; + } + + static async rejectExtra(): Promise { + let effects = 0; + try { await Promise.reject(7, ++effects); } + catch (value) { return value === 7 && effects === 1 ? 1 : 0; } + return 0; + } + + static async callbackResolveMissing(): Promise { + const value = await new Promise((resolve) => resolve()); + return value === undefined ? 1 : 0; + } + + static async callbackRejectMissing(): Promise { + try { await new Promise((resolve, reject) => reject()); } + catch (value) { return value === undefined ? 1 : 0; } + return 0; + } + + static async firstSettlementWins(): Promise { + const value = await new Promise((resolve: any) => { resolve(7); resolve(); }); + return value === 7 ? 1 : 0; + } + + static async callbackExtra(): Promise { + const counter = { effects: 0 }; + const value = await new Promise((resolve: any) => resolve(7, ++counter.effects)); + return value === 7 && counter.effects === 1 ? 1 : 0; + } +}