[TS PBT] Map property coverage to EtsIR

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 = "9ea33879c9"
+    const val jacodb = "aa319129f8"
     const val juliet = "1.3.2"
     const val junit = "5.9.3"
     const val kotlin = "2.1.0"

usvm-ts-pbt/DESIGN.md

@@ -8,6 +8,8 @@ API and CLI examples, see [README.md](README.md).
 - Kotlin owns property definitions, validation, registries, orchestration, and public results.
 - Node is a thin adapter around fast-check and direct TypeScript loading.
 - Per-property source coverage is an optional backend capability collected by Kotlin through an isolated c8 run.
+- A backend-neutral Kotlin mapping layer connects manifests and source coverage to EtsIR without changing the
+  declarative property model.
 - The JSON exchange is one request and one response from the same packaged distribution; it has no persistence or
   compatibility negotiation.
 - Failures are typed without exposing runtime-dependent Node stack traces.
@@ -25,6 +27,7 @@ flowchart LR
         Backend[FastCheckBackend]
         Process[FastCheckProcessClient]
         Projection[FastCheckProjectionClient]
+        Mapping[PropertyEtsMapper]
     end
 
     subgraph Node_adapter[Private Node adapter]
@@ -41,13 +44,17 @@ flowchart LR
     Tsx[tsx]
     C8[c8 and Istanbul JSON]
     UserTS[User TypeScript source]
+    EtsIR[EtsScene and EtsSourceSpan]
 
     CLI --> Registry
     CLI --> Backend
     Caller --> Backend
     Registry --> Model
     Backend --> Model
     Backend --> Process
+    Model --> Mapping
+    Process --> Mapping
+    Mapping --> EtsIR
     Process --> ExecutionCLI
     Process --> C8
     C8 --> ExecutionCLI
@@ -72,6 +79,7 @@ flowchart LR
 | Registry and CLI | Select Kotlin-defined properties and turn user options into a run configuration. |
 | `FastCheckBackend` | Validate examples, resolve source roots, and create the adapter request. |
 | `FastCheckProcessClient` | Supervise Node with coroutines and optionally decode one isolated c8 report. |
+| `PropertyEtsMapper` | Resolve property entry points and backend-neutral coverage to explicit EtsIR targets. |
 | `execution-cli.ts` | Read one JSON request, protect protocol stdout from user logging, and write one response. |
 | `execute-property.ts` | Build the fast-check property, run it, and translate `RunDetails` into the common result. |
 | `project-domain.ts` | Translate domain descriptors into real `fc.Arbitrary` instances. |
@@ -213,11 +221,52 @@ A successful or falsified property exits the bridge normally, allowing c8 to flu
 invalid protocol responses, and hard kills do not produce a completed property result. The workspace is removed
 in all cases, and a new workspace is used for every property.
 
+## Property-to-EtsIR mapping
+
+The mapping layer consumes common Kotlin artifacts only: `PropertyManifest`, optional `PropertyCoverageArtifact`,
+an `EtsScene`, and source roots. It does not depend on `FastCheckBackend` or its private runtime representation.
+The result is a `PropertyEtsMappingArtifact` that keeps the manifest property ID, backend coverage provenance,
+mapping coordinate and branch-order provenance, resolved predicate and precondition targets, coverage targets, and
+stable diagnostic reasons.
+
+Entry-point resolution starts from the manifest module/export pair and follows named or bare-star TypeScript
+re-exports. Direct function exports resolve only in the file-level `%dflt` class. Namespace-star exports are not
+callable methods, bare-star traversal excludes `default`, explicit runtime exports take precedence over bare-star
+exports, and duplicate paths to one EtsIR method are deduplicated. Type-alias exports do not mask bare-star runtime
+exports. The pinned EtsIR model preserves `isTypeOnly` independently of declaration kind, so type-only named and
+star re-exports do not mask a bare-star runtime fallback.
+Module candidates mirror the frontend's `.ts`, `.ets`, `.d.ts`, and directory-index suffix rules.
+Predicate and precondition resolution are independent. A resolved method carries `EtsEntryPointBindings`: receiver
+slot zero, ordered input-to-parameter bindings in subsequent slots, and the result type. A mismatch between
+manifest inputs and EtsIR parameters is unsupported, as is coverage carrying another property ID.
+
+Existing source roots and files are canonicalized with real paths; an unresolvable root makes entry-point mapping
+unsupported. Istanbul lines are converted from one-based to zero-based, columns stay zero-based, and offsets are
+calculated in UTF-16 code units using TypeScript's LF, CRLF, CR, U+2028, and U+2029 line terminators. Statement mapping first looks
+for an exact `EtsSourceSpan`; if normalized EtsIR statements share that span, all remain exact targets. A containing
+coverage range with one distinct origin is also exact, several distinct origins are ambiguous, and no origin match
+is unmapped. Missing source text, invalid coordinates, or an EtsIR file whose statements have no origins are
+unsupported.
+
+Branch mapping currently accepts an Istanbul `if` with exactly two ordered arms and resolves conditions to
+`EtsIfStmt`. The first CFG successor is recorded as true and the second as false. Several EtsIR conditions with one
+shared origin are exact; several distinct condition origins are ambiguous. Other branch types, non-binary arm
+shapes, and EtsIR conditions without two ordered successors are unsupported rather than inferred.
+An invalid arm is reported independently while a successfully resolved condition remains available, and aggregate
+coverage status includes both conditions and arms.
+
+The JVM taint-analysis `PositionResolver` and `ConditionResolver` were reviewed as architectural prior art. Their
+useful separation is preserved: declarative receiver/argument/result positions are distinct from runtime-bound
+values, and condition interpretation is distinct from position resolution. The TypeScript mapper expresses this
+with EtsIR-specific binding and mapping records and has no dependency on `usvm-jvm` or the taint-analysis module.
+
 The execution client starts stdout, stderr, and stdin work concurrently on the coroutine I/O dispatcher. Requests
 and stdout are limited to 4 MiB; stderr is limited to 64 KiB. These are transport safety bounds, not property-policy
-limits. The hard deadline is the property timeout plus two seconds for transport, followed by a 250 ms graceful
-shutdown before force-kill. The only run-control maximum is `2^31 - 1` milliseconds because Node timers use signed
-32-bit delays; runs, examples, and replay paths have no arbitrary count or length caps.
+limits. The hard deadline is the property timeout plus two seconds for transport, followed by up to 250 ms of
+graceful shutdown before force-kill, bounded by the absolute deadline. A private supervisor keeps the adapter in an
+owned process group and retains a stable worker until cleanup, so an adapter that exits before its descendants cannot
+orphan them. The only run-control maximum is `2^31 - 1` milliseconds because Node timers use signed 32-bit delays;
+runs, examples, and replay paths have no arbitrary count or length caps.
 
 ## Runtime packaging
 
@@ -238,12 +287,15 @@ classifier because `tsx` depends on a native esbuild package.
   shrinking, explicit examples, preconditions, async predicates, and timeouts.
 - Coverage golden tests assert literal TypeScript statement and branch outcomes for successful and falsified runs,
   cross-property isolation, scope and glob filtering, and source-map/report diagnostics.
+- Mapping golden tests load stable TypeScript fixtures through the native frontend and cover predicate,
+  precondition, re-export, UTF-16 normalization, shared spans, exact/ambiguous/unmapped branches, unsupported
+  source data, and backend-without-coverage behavior.
 
 ## Non-goals
 
 - Persisting requests or results, or supporting old wire formats.
 - Discovering properties by scanning TypeScript source roots.
 - Compiling user TypeScript as part of the PBT workflow.
 - Reimplementing generation, replay, skip accounting, or shrinking in Kotlin.
-- Mapping Node source locations to EtsIR or constructing symbolic targets from coverage.
-- Combining Node source coverage with future EtsIR replay coverage.
+- Constructing symbolic inputs or executing mapped properties in USVM.
+- Combining backend source coverage with future EtsIR replay coverage.

usvm-ts-pbt/README.md

@@ -137,6 +137,61 @@ Missing or malformed reports use `coverage.report.missing` and `coverage.report.
 remap produces `coverage.source-map.missing` or `coverage.source-map.invalid`; a missing packaged c8 runtime
 produces `coverage.collector.not-found`.
 
+## Property-to-EtsIR mapping
+
+`PropertyEtsMapper` combines a backend-neutral `PropertyManifest`, an `EtsScene`, and optional
+`PropertyCoverageArtifact` into one `PropertyEtsMappingArtifact` per property:
+
+```kotlin
+val mapping = PropertyEtsMapper(
+    scene = etsScene,
+    sourceRoots = sourceRoots,
+).map(
+    manifest = property.toManifest(),
+    coverage = result.coverage,
+)
+```
+
+Predicate and optional precondition exports are resolved independently, including named and bare-star TypeScript
+re-exports and extensionless `.ts`, `.ets`, `.d.ts`, and directory-index module paths. Direct function exports map
+only to file-level EtsIR methods; namespace-star exports are not treated as functions, bare-star exports do not
+forward `default`, explicit runtime exports take precedence over bare-star exports, and duplicate re-export paths
+to the same method collapse to one target. Type-alias exports do not mask bare-star runtime exports. The current
+EtsIR export model preserves `isTypeOnly` independently of the declaration kind, so type-only named and star
+re-exports do not mask a bare-star runtime fallback.
+Every resolved entry point has explicit receiver, ordered input, and result bindings. The receiver uses stack slot
+zero and property inputs follow it in manifest order. A coverage artifact for another property is rejected rather
+than combined with the manifest.
+
+Existing source roots and files are canonicalized through real paths, so symlinked frontend inputs align with
+backend coverage; an unresolvable root is `UNSUPPORTED`. Istanbul's one-based lines and zero-based columns become
+zero-based half-open ranges with UTF-16 offsets, matching TypeScript and EtsIR source spans. CRLF, lone CR, LF,
+U+2028, and U+2029 are recognized as TypeScript line terminators.
+Statement ranges are compared with `EtsSourceSpan` origins. Several normalized EtsIR statements sharing one exact
+origin remain one `EXACT` mapping with several targets; several distinct origins inside a covered range are
+`AMBIGUOUS`.
+
+Binary Istanbul branches map to `EtsIfStmt`. Arm zero is the true CFG successor and arm one is the false successor,
+as recorded by `EtsMappingProvenance`. Other branch shapes are `UNSUPPORTED`; the mapper does not guess switch,
+logical-expression, or backend-specific arm semantics.
+
+| Status | Meaning |
+| --- | --- |
+| `EXACT` | One source identity was established; normalized statements may produce several EtsIR targets with that shared identity. |
+| `AMBIGUOUS` | Several distinct entry points or source origins match, and every candidate is preserved. |
+| `UNMAPPED` | The input is supported, but no EtsIR target matches it. |
+| `UNSUPPORTED` | The input cannot be interpreted safely, for example because coverage, source text, origins, coordinates, bindings, or branch shape are unsupported. |
+
+Stable mapping diagnostics include `mapping.entry-point.unmapped`, `mapping.entry-point.ambiguous`,
+`mapping.entry-point.bindings.unsupported`, `mapping.coverage.unavailable`,
+`mapping.coverage.property-id.mismatch`, `mapping.statement.unmapped`, `mapping.statement.ambiguous`,
+`mapping.branch.unmapped`, `mapping.branch.ambiguous`, `mapping.branch.shape.unsupported`,
+`mapping.branch.cfg.unsupported`,
+`mapping.source.unavailable`, `mapping.source.location.unsupported`, and
+`mapping.source-origins.unsupported`, and `mapping.source-root.unsupported`. Backend provenance is preserved
+separately from mapping provenance and
+backend diagnostics are copied without reinterpretation.
+
 ## Registries and CLI
 
 The CLI loads Kotlin property registries through `ServiceLoader`:

usvm-ts-pbt/fast-check-adapter/package.json

@@ -9,7 +9,7 @@
     "build": "tsc --project tsconfig.json",
     "pretest": "npm run build",
     "test": "npm run test:compiled",
-    "test:compiled": "node --test dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js"
+    "test:compiled": "node --test dist/test/entry-point.test.js dist/test/execute-property.test.js dist/test/execution-cli.test.js dist/test/js-value.test.js dist/test/project-domain.test.js dist/test/projection-cli.test.js dist/test/projection-supervisor.test.js"
   },
   "dependencies": {
     "c8": "10.1.3",

usvm-ts-pbt/fast-check-adapter/src/execute-property.ts

@@ -83,7 +83,7 @@ export async function executeProperty(requestValue: unknown): Promise<FastCheckE
   const property = buildProperty(arbitrary, predicate, precondition);
   const parameters = buildParameters(request);
 
-  const details = await Promise.resolve(fc.check(property, parameters));
+  const details = await checkProperty(property, parameters, request.replayPath);
 
   if (details.errorInstance instanceof ProtocolError) throw details.errorInstance;
 
@@ -106,23 +106,59 @@ function buildProperty(
 
   if (asynchronous) {
     return fc.asyncProperty(arbitrary, async (values: unknown[]): Promise<boolean> => {
-      const argumentsList = values as JsConcreteValue[];
+      if (precondition !== undefined && !(await precondition.invoke(cloneArguments(values)))) fc.pre(false);
 
-      if (precondition !== undefined && !(await precondition.invoke(argumentsList))) fc.pre(false);
-
-      return await predicate.invoke(argumentsList);
+      return await predicate.invoke(cloneArguments(values));
     });
   }
 
   return fc.property(arbitrary, (values: unknown[]): boolean => {
-    const argumentsList = values as JsConcreteValue[];
-
-    if (precondition !== undefined && !precondition.invoke(argumentsList)) fc.pre(false);
+    if (precondition !== undefined && !precondition.invoke(cloneArguments(values))) fc.pre(false);
 
-    return predicate.invoke(argumentsList) as boolean;
+    return predicate.invoke(cloneArguments(values)) as boolean;
   });
 }
 
+async function checkProperty(
+  property: fc.IProperty<[unknown[]]> | fc.IAsyncProperty<[unknown[]]>,
+  parameters: Parameters<[unknown[]]>,
+  replayPath: string | undefined,
+): Promise<RunDetails<[unknown[]]>> {
+  try {
+    return await Promise.resolve(fc.check(property, parameters));
+  } catch (error: unknown) {
+    const replayFailed = replayPath !== undefined
+      && error instanceof Error
+      && error.message.startsWith('Unable to replay,');
+    if (replayFailed) {
+      throw protocolError(
+        adapterDiagnostic.protocolReplayPathInvalid,
+        'Replay path cannot be applied to this property run',
+        'replayPath',
+      );
+    }
+
+    throw error;
+  }
+}
+
+function cloneArguments(values: unknown[]): JsConcreteValue[] {
+  return cloneRecursiveArrays(values, new Map()) as JsConcreteValue[];
+}
+
+function cloneRecursiveArrays(value: unknown, clones: Map<unknown[], unknown[]>): unknown {
+  if (!Array.isArray(value)) return value;
+
+  const existing = clones.get(value);
+  if (existing !== undefined) return existing;
+
+  const clone: unknown[] = [];
+  clones.set(value, clone);
+  value.forEach((element) => clone.push(cloneRecursiveArrays(element, clones)));
+
+  return clone;
+}
+
 function buildParameters(request: FastCheckExecutionRequest): Parameters<[unknown[]]> {
   const decodedExamples = request.examples.map((example, exampleIndex) => {
     if (example.length !== request.manifest.inputs.length) {
@@ -198,12 +234,18 @@ function failureDetails(details: RunDetails<[unknown[]]>): FastCheckFailureDetai
     };
   }
 
+  if (details.counterexample === null) {
+    return {
+      kind: 'property',
+      errorName: 'PropertyFailure',
+      message: 'Property could not satisfy its precondition within the skip limit',
+    };
+  }
+
   return {
     kind: 'property',
-    errorName: 'PropertyFailure',
-    message: details.counterexample === null
-      ? 'Property could not satisfy its precondition within the skip limit'
-      : 'Property predicate returned false',
+    errorName: 'ThrownValue',
+    message: String(error),
   };
 }
 
@@ -248,7 +290,8 @@ function validateRequest(value: unknown): FastCheckExecutionRequest {
     );
   }
 
-  const invalidReplayPath = request.replayPath !== undefined && typeof request.replayPath !== 'string';
+  const invalidReplayPath = request.replayPath !== undefined
+    && (typeof request.replayPath !== 'string' || !REPLAY_PATH_PATTERN.test(request.replayPath));
   if (invalidReplayPath) {
     throw protocolError(
       adapterDiagnostic.protocolReplayPathInvalid,
@@ -389,3 +432,4 @@ function isSignedInt(value: unknown): value is number {
 
 // Node timers use signed 32-bit millisecond delays; larger values are clamped to one millisecond.
 const MAX_TIMER_DELAY_MILLIS = 2 ** 31 - 1;
+const REPLAY_PATH_PATTERN = /^\d+(?::\d+)*$/;