From e861cf4ff4f21a4b737952908fe82ffe05c9c5e8 Mon Sep 17 00:00:00 2001 From: Aleksei Menshutin Date: Mon, 12 Oct 2026 18:51:46 +0300 Subject: [PATCH] Separate captured environments from PBT source arguments --- .../ts/pbt/mapping/EtsEntryPointResolver.kt | 48 ++++++++-- .../usvm/ts/pbt/mapping/EtsMappingModel.kt | 7 ++ .../PropertyEtsExportResolutionTest.kt | 87 ++++++++++++++++++- .../mapping/exports/CapturedBuiltinArrow.ts | 19 ++++ 4 files changed, 154 insertions(+), 7 deletions(-) create mode 100644 usvm-ts-pbt/src/test/resources/mapping/exports/CapturedBuiltinArrow.ts diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsEntryPointResolver.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsEntryPointResolver.kt index 12cc28be18..8787c9e4c9 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsEntryPointResolver.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsEntryPointResolver.kt @@ -7,8 +7,10 @@ import org.jacodb.ets.model.EtsExportInfo import org.jacodb.ets.model.EtsExportType import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsLexicalEnvType import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsMethod +import org.jacodb.ets.model.EtsMethodParameter import org.jacodb.ets.model.EtsMethodSignature import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStaticFieldRef @@ -49,7 +51,11 @@ internal class EtsEntryPointResolver( val hasAmbiguousResolution = hasAmbiguousCandidateResolution || hasAmbiguousSourceResolution val entryPointName = "${entryPoint.module}#${entryPoint.exportName}" - if (methods.any { method -> method.parameters.size != manifest.inputs.size }) { + val methodsWithBindings = methods.map { method -> method to method.bindingParameters() } + val hasUnmatchedSourceParameters = methodsWithBindings.any { (_, parameters) -> + parameters.inputs.size != manifest.inputs.size + } + if (hasUnmatchedSourceParameters) { val diagnostic = EtsMappingDiagnostic( code = PbtDiagnosticCode.MAPPING_ENTRY_POINT_BINDINGS_UNSUPPORTED, message = "Property inputs do not match EtsIR parameters for ${entryPoint.exportName}", @@ -63,10 +69,13 @@ internal class EtsEntryPointResolver( ) } - val targets = methods.map { method -> + val targets = methodsWithBindings.map { (method, parameters) -> EtsEntryPointTarget( method = method, - bindings = method.bindingsFor(manifest), + bindings = method.bindingsFor( + manifest = manifest, + parameters = parameters, + ), ) } @@ -231,16 +240,32 @@ internal class EtsEntryPointResolver( return modulePaths.any(filePaths::contains) } - private fun EtsMethod.bindingsFor(manifest: PropertyManifest): EtsEntryPointBindings { + private fun EtsMethod.bindingParameters(): EtsBindingParameters { + // The frontend lifts arrow-function captures into one leading lexical-environment parameter. + // It is not a source argument; the interpreter recognizes the same parameter by its semantic type. + val hiddenClosure = parameters.firstOrNull()?.takeIf { parameter -> + parameter.type is EtsLexicalEnvType + } + + return EtsBindingParameters( + lexicalEnvironment = hiddenClosure, + inputs = if (hiddenClosure == null) parameters else parameters.drop(1), + ) + } + + private fun EtsMethod.bindingsFor( + manifest: PropertyManifest, + parameters: EtsBindingParameters, + ): EtsEntryPointBindings { val receiverType = EtsClassType( signature = signature.enclosingClass, typeParameters = requireNotNull(enclosingClass).typeParameters, ) - val inputBindings = manifest.inputs.zip(parameters).mapIndexed { index, (input, parameter) -> + val inputBindings = manifest.inputs.zip(parameters.inputs).map { (input, parameter) -> EtsInputBinding( propertyInputName = input.name, parameter = parameter, - stackSlot = index + RECEIVER_STACK_SLOTS, + stackSlot = parameter.index + RECEIVER_STACK_SLOTS, ) } @@ -251,10 +276,21 @@ internal class EtsEntryPointResolver( ), inputs = inputBindings, result = EtsResultBinding(type = returnType), + lexicalEnvironment = parameters.lexicalEnvironment?.let { parameter -> + EtsLexicalEnvironmentBinding( + parameter = parameter, + stackSlot = parameter.index + RECEIVER_STACK_SLOTS, + ) + }, ) } } +private data class EtsBindingParameters( + val lexicalEnvironment: EtsMethodParameter?, + val inputs: List, +) + private data class ExportResolutionStep( val file: EtsFile, val exportName: String, diff --git a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsMappingModel.kt b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsMappingModel.kt index 5d0b3f9310..7fc3a5ca98 100644 --- a/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsMappingModel.kt +++ b/usvm-ts-pbt/src/main/kotlin/org/usvm/ts/pbt/mapping/EtsMappingModel.kt @@ -96,6 +96,12 @@ data class EtsReceiverBinding( val type: EtsType, ) +/** Preserves the frontend's hidden lexical-environment parameter separately from source arguments. */ +data class EtsLexicalEnvironmentBinding( + val parameter: EtsMethodParameter, + val stackSlot: Int, +) + /** Connects one ordered property input to the corresponding EtsIR parameter and stack slot. */ data class EtsInputBinding( val propertyInputName: String, @@ -113,6 +119,7 @@ data class EtsEntryPointBindings( val receiver: EtsReceiverBinding, val inputs: List, val result: EtsResultBinding, + val lexicalEnvironment: EtsLexicalEnvironmentBinding? = null, ) /** Resolved EtsIR method and its property-facing symbolic bindings. */ diff --git a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/mapping/PropertyEtsExportResolutionTest.kt b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/mapping/PropertyEtsExportResolutionTest.kt index 401ce47bec..8afa178bfc 100644 --- a/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/mapping/PropertyEtsExportResolutionTest.kt +++ b/usvm-ts-pbt/src/test/kotlin/org/usvm/ts/pbt/mapping/PropertyEtsExportResolutionTest.kt @@ -3,6 +3,7 @@ package org.usvm.ts.pbt.mapping import org.jacodb.ets.model.EtsAssignStmt import org.jacodb.ets.model.EtsFile import org.jacodb.ets.model.EtsFunctionType +import org.jacodb.ets.model.EtsLexicalEnvType import org.jacodb.ets.model.EtsLocal import org.jacodb.ets.model.EtsScene import org.jacodb.ets.model.EtsStaticFieldRef @@ -18,9 +19,90 @@ import org.usvm.ts.pbt.model.TypeScriptEntryPoint import org.usvm.ts.pbt.testResourcePath import java.nio.file.Path import kotlin.test.assertEquals +import kotlin.test.assertNotNull +import kotlin.test.assertNull import kotlin.test.assertTrue class PropertyEtsExportResolutionTest { + @Test + fun `exported arrow binds source input after its hidden builtin capture`() { + val source = testResourcePath("/mapping/exports/CapturedBuiltinArrow.ts") + val mapper = mapper(source) + + val artifact = mapper.map( + manifest(module = source.fileName.toString(), exportName = "usesCapturedBuiltins"), + ) + + assertEquals(EtsMappingStatus.EXACT, artifact.predicate.status) + val target = artifact.predicate.targets.single() + val lexicalEnvironment = assertNotNull(target.bindings.lexicalEnvironment) + val hiddenCapture = lexicalEnvironment.parameter + val captureType = hiddenCapture.type as EtsLexicalEnvType + val input = target.bindings.inputs.single() + assertEquals(expected = 0, actual = hiddenCapture.index) + assertEquals(expected = 1, actual = lexicalEnvironment.stackSlot) + assertEquals(listOf("Number", "Error"), captureType.closures.map { closure -> closure.name }) + assertEquals(expected = "value", actual = input.parameter.name) + assertEquals(expected = 1, actual = input.parameter.index) + assertEquals(expected = 2, actual = input.stackSlot) + } + + @Test + fun `arbitrary captured runtime value remains explicit in lexical environment binding`() { + val source = testResourcePath("/mapping/exports/CapturedBuiltinArrow.ts") + val mapper = mapper(source) + + val artifact = mapper.map( + manifest(module = source.fileName.toString(), exportName = "capturesModuleValue"), + ) + + assertEquals(EtsMappingStatus.EXACT, artifact.predicate.status) + val bindings = artifact.predicate.targets.single().bindings + val lexicalEnvironment = assertNotNull(bindings.lexicalEnvironment) + val captureType = lexicalEnvironment.parameter.type as EtsLexicalEnvType + assertEquals(listOf("threshold"), captureType.closures.map { closure -> closure.name }) + assertEquals(expected = 1, actual = lexicalEnvironment.stackSlot) + assertEquals(expected = 2, actual = bindings.inputs.single().stackSlot) + } + + @Test + fun `captured expression arrow preserves multiple source inputs in order`() { + val source = testResourcePath("/mapping/exports/CapturedBuiltinArrow.ts") + val mapper = mapper(source) + val manifest = manifest( + module = source.fileName.toString(), + exportName = "capturedBuiltinsWithTwoInputs", + ).copy( + inputs = listOf( + PropertyInput(name = "first", domain = IntegerDomain()), + PropertyInput(name = "second", domain = IntegerDomain()), + ), + ) + + val artifact = mapper.map(manifest) + + assertEquals(EtsMappingStatus.EXACT, artifact.predicate.status) + val bindings = artifact.predicate.targets.single().bindings + assertNotNull(bindings.lexicalEnvironment) + assertEquals(listOf("first", "second"), bindings.inputs.map { input -> input.propertyInputName }) + assertEquals(listOf("left", "right"), bindings.inputs.map { input -> input.parameter.name }) + assertEquals(listOf(2, 3), bindings.inputs.map { input -> input.stackSlot }) + } + + @Test + fun `hidden builtin capture does not conceal unmatched source parameters`() { + val source = testResourcePath("/mapping/exports/CapturedBuiltinArrow.ts") + val mapper = mapper(source) + + val artifact = mapper.map( + manifest(module = source.fileName.toString(), exportName = "capturedBuiltinsWithTwoInputs"), + ) + + assertEquals(EtsMappingStatus.UNSUPPORTED, artifact.predicate.status) + assertEquals(emptyList(), artifact.predicate.targets) + assertEquals("mapping.entry-point.bindings.unsupported", artifact.predicate.diagnostics.single().code) + } + @Test fun `named default declaration resolves only through the default export name`() { val source = testResourcePath("/mapping/exports/NamedDefaultDeclaration.ts") @@ -116,9 +198,12 @@ class PropertyEtsExportResolutionTest { val artifact = mapper.map(manifest(module = source.fileName.toString(), exportName = "arrowPredicate")) assertEquals(EtsMappingStatus.EXACT, artifact.predicate.status) - val method = artifact.predicate.targets.single().method + val target = artifact.predicate.targets.single() + val method = target.method assertTrue(method.name.startsWith("%AM")) assertEquals(listOf("value"), method.parameters.map { parameter -> parameter.name }) + assertNull(target.bindings.lexicalEnvironment) + assertEquals(expected = 1, actual = target.bindings.inputs.single().stackSlot) } @Test diff --git a/usvm-ts-pbt/src/test/resources/mapping/exports/CapturedBuiltinArrow.ts b/usvm-ts-pbt/src/test/resources/mapping/exports/CapturedBuiltinArrow.ts new file mode 100644 index 0000000000..026cd06536 --- /dev/null +++ b/usvm-ts-pbt/src/test/resources/mapping/exports/CapturedBuiltinArrow.ts @@ -0,0 +1,19 @@ +export const usesCapturedBuiltins = (value: number): boolean => { + if (!Number.isInteger(value)) { + throw new Error('expected an integer') + } + + return value % 2 === 0 +} + +export const capturedBuiltinsWithTwoInputs = (left: number, right: number): boolean => + Number.isFinite(left) && left === right + +let capturesModuleValue: (value: number) => boolean + +{ + const threshold = 3 + capturesModuleValue = (value: number): boolean => value > threshold +} + +export { capturesModuleValue }