[TS] Resolve exported TypeScript entry points

usvm-ts-fast-check/fast-check-adapter/src/source-inspector-cli.ts

@@ -0,0 +1,50 @@
+import { readFileSync } from 'node:fs'
+import ts from 'typescript'
+
+function fail(message: string): never {
+  process.stderr.write(`${message}\n`)
+  process.exit(2)
+}
+
+const [sourcePath, exportName, startText, endText] = process.argv.slice(2)
+if (sourcePath === undefined || exportName === undefined || startText === undefined || endText === undefined) {
+  fail('Expected source path, export name, start offset, and end offset')
+}
+
+const startOffset = Number(startText)
+const endOffset = Number(endText)
+if (!Number.isSafeInteger(startOffset) || !Number.isSafeInteger(endOffset)) {
+  fail('Source offsets must be safe integers')
+}
+
+const source = readFileSync(sourcePath, 'utf8')
+const diagnostics = ts.transpileModule(source, {
+  compilerOptions: { target: ts.ScriptTarget.Latest },
+  fileName: sourcePath,
+  reportDiagnostics: true,
+}).diagnostics?.filter((diagnostic) => diagnostic.category === ts.DiagnosticCategory.Error) ?? []
+if (diagnostics.length > 0) {
+  fail(`Cannot parse TypeScript source: ${ts.flattenDiagnosticMessageText(diagnostics[0]?.messageText ?? '', '\n')}`)
+}
+
+const sourceFile = ts.createSourceFile(sourcePath, source, ts.ScriptTarget.Latest, true, ts.ScriptKind.TS)
+
+const bodies: ts.ConciseBody[] = []
+for (const statement of sourceFile.statements) {
+  if (!ts.isVariableStatement(statement)) continue
+  const exported = statement.modifiers?.some((modifier) => modifier.kind === ts.SyntaxKind.ExportKeyword) === true
+  if (!exported) continue
+
+  for (const declaration of statement.declarationList.declarations) {
+    if (!ts.isIdentifier(declaration.name) || declaration.name.text !== exportName) continue
+    if (!declaration.initializer || !ts.isArrowFunction(declaration.initializer)) continue
+    if (ts.isBlock(declaration.initializer.body)) continue
+
+    bodies.push(declaration.initializer.body)
+  }
+}
+
+const matchingBodies = bodies.filter((body) =>
+  body.getStart(sourceFile, false) === startOffset && body.getEnd() === endOffset,
+)
+process.stdout.write(matchingBodies.length === 1 ? 'true' : 'false')

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/FastCheckRuntime.kt

@@ -12,6 +12,8 @@ internal object FastCheckRuntime {
 
     fun processSupervisorEntryPoint(): Path = locateEntryPoint(PROCESS_SUPERVISOR)
 
+    fun sourceInspectorEntryPoint(): Path = locateEntryPoint(SOURCE_INSPECTOR_CLI)
+
     private fun locateEntryPoint(fileName: String): Path {
         val candidates = runtimeDirectories().map { runtimeDirectory ->
             runtimeDirectory.resolve(ENTRY_POINT_DIRECTORY).resolve(fileName)
@@ -49,5 +51,6 @@ internal object FastCheckRuntime {
     private const val EXECUTION_CLI = "execution-cli.js"
     private const val PROJECTION_CLI = "projection-cli.js"
     private const val PROCESS_SUPERVISOR = "process-supervisor.js"
+    private const val SOURCE_INSPECTOR_CLI = "source-inspector-cli.js"
     private const val INSTALLED_RUNTIME_DIRECTORY = "fast-check-adapter"
 }

usvm-ts-fast-check/src/main/kotlin/org/usvm/ts/pbt/fastcheck/TypeScriptSourceInspector.kt

@@ -0,0 +1,40 @@
+package org.usvm.ts.pbt.fastcheck
+
+import java.nio.file.Path
+import java.util.concurrent.TimeUnit
+
+/** Exact TypeScript-AST validation used when EtsIR omits an expression-bodied arrow's source origin. */
+object TypeScriptSourceInspector {
+    fun isExportedExpressionArrowBody(
+        source: Path,
+        exportName: String,
+        startOffset: Int,
+        endOffset: Int,
+        nodeExecutable: String = "node",
+    ): Boolean {
+        val process = ProcessBuilder(
+            nodeExecutable,
+            FastCheckRuntime.sourceInspectorEntryPoint().toString(),
+            source.toString(),
+            exportName,
+            startOffset.toString(),
+            endOffset.toString(),
+        ).redirectErrorStream(true).start()
+        if (!process.waitFor(SOURCE_INSPECTION_TIMEOUT_SECONDS, TimeUnit.SECONDS)) {
+            process.destroyForcibly()
+            error("TypeScript source inspection timed out")
+        }
+
+        val output = process.inputStream.bufferedReader().use { reader -> reader.readText() }.trim()
+        require(process.exitValue() == 0) {
+            "TypeScript source inspection failed with exit ${process.exitValue()}: $output"
+        }
+        return when (output) {
+            "true" -> true
+            "false" -> false
+            else -> error("TypeScript source inspection returned an invalid response: $output")
+        }
+    }
+
+    private const val SOURCE_INSPECTION_TIMEOUT_SECONDS: Long = 10
+}

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,8 @@ 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() }
+        if (methodsWithBindings.any { (_, parameters) -> parameters.inputs.size != manifest.inputs.size }) {
             val diagnostic = EtsMappingDiagnostic(
                 code = PbtDiagnosticCode.MAPPING_ENTRY_POINT_BINDINGS_UNSUPPORTED,
                 message = "Property inputs do not match EtsIR parameters for ${entryPoint.exportName}",
@@ -63,10 +66,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 +237,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 +273,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<EtsMethodParameter>,
+)
+
 private data class ExportResolutionStep(
     val file: EtsFile,
     val exportName: String,

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<EtsInputBinding>,
     val result: EtsResultBinding,
+    val lexicalEnvironment: EtsLexicalEnvironmentBinding? = null,
 )
 
 /** Resolved EtsIR method and its property-facing symbolic bindings. */

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,65 @@ 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.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(0, hiddenCapture.index)
+        assertEquals(1, lexicalEnvironment.stackSlot)
+        assertEquals(listOf("Number", "Error"), captureType.closures.map { closure -> closure.name })
+        assertEquals("value", input.parameter.name)
+        assertEquals(1, input.parameter.index)
+        assertEquals(2, 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(1, lexicalEnvironment.stackSlot)
+        assertEquals(2, bindings.inputs.single().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")

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 }