You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
Part of #345. Builds on #349.
Goal
Resolve property predicate/precondition exports and supported source coverage into EtsIR targets used by symbolic execution.
Scope
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
Symbolic input construction, predicate execution, process-framework expansion and new coverage converters are outside this issue.