Skip to content

[TS PBT] Map Kotlin property definitions and source coverage to EtsIR #350

Description

@CaelmBleidd

Part of #345. Builds on #349.

Goal

Resolve property predicate/precondition exports and supported source coverage into EtsIR targets used by symbolic execution.

Scope

  • Resolve the explicit module/export references in PropertyManifest. Resolve predicate and optional precondition independently and bind ordered inputs, the interpreter receiver slot and result.
  • Use the native frontend's export/source-origin information. Support direct exports and the already implemented re-export cases; document the exact subset. Do not reimplement the complete Node/TypeScript module resolver.
  • Normalize source identities and TypeScript UTF-16, zero-based, half-open coordinates once. Use standard path and text APIs where they preserve these semantics; keep any necessary language-specific line handling small and named.
  • Map supported statement ranges to EtsIR statements. Several normalized statements can share one source origin without being ambiguous.
  • Distinguish EXACT, AMBIGUOUS, UNMAPPED and UNSUPPORTED; preserve useful candidates and reasons instead of guessing.
  • For binary Istanbul if records with known true/false arms, map to the established CFG successor order. Keep one source of truth for that order.
  • Reuse existing coverage provenance and diagnostic conventions. Keep fixed coordinate/CFG conventions documented, rather than building configuration or version negotiation for hypothetical formats.
  • Simplify duplicated path/coordinate/coverage helpers in the existing [TS PBT] Map property coverage to EtsIR #381 work; reuse standard readers and traversal APIs before adding custom streaming infrastructure.

Real-backend limitation

Pinned c8/V8 currently emits one-location branch records without the original if/arm relationship. These records are UNSUPPORTED here, with statement mappings retained. #382 owns exact c8/V8 branch reconstruction and its real-runtime tests.

This issue can complete without #382. Property entry-point mapping and violation search must work with no coverage. Synthetic binary-if fixtures establish only that supported artifact contract, not end-to-end c8 branch support.

Definition of Done

  • Predicate/precondition references and ordered inputs bind correctly through the real native frontend.
  • Exact/shared-origin, ambiguous, missing and unsupported locations have focused behavior tests.
  • A real fast-check/c8 run retains statement mappings and explicitly reports the branch limitation.
  • A property without coverage still produces usable entry-point bindings.
  • Tests protect relevant UTF-16/line-boundary cases, re-export cycles and multi-input ordering without demanding support for every module-resolution feature.
  • Documentation clearly separates the supported binary-if artifact path from the c8/V8 follow-up.
  • Deliver through the existing dedicated PR [TS PBT] Map property coverage to EtsIR #381.

Symbolic input construction, predicate execution, process-framework expansion and new coverage converters are outside this issue.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions