Scope
The second L3 engine of the two-engine design (docs/design/specs/l3-intraprocedural-dataflow-design.md, steps 6–7). The AST engine (the default, source-only) landed in #183; this issue tracks the WALA-based L3 engine behind --l3-engine wala plus the differential gate that cross-checks the two engines.
This is the intended next work item after the AST-engine PR.
Work
--l3-engine wala — currently accepted but rejected with a clear "not yet implemented" error. Implement it.- The WALA→source-statement mapping (B.1) — map each SSA instruction to an L1/AST statement node by line-cover match → content disambiguation → no-source-position handling (phi/pi, compiler temporaries) → innermost fallback.
line:col is adopted from the matched AST node, never synthesized. This is the machinery L4's semantic DDG reuses.
- CFG / CDG / DDG on WALA — CFG from
SSACFG + ISSABasicBlock projected via B.1, normalized to one @exit; CDG from WALA dominators/post-dominators; DDG from WALA SSA def-use, same syntactic prov:["ssa"] contract as the AST engine (no points-to at L3).
- Differential gate — run both engines over the fixtures and assert agreement on the defined subset (CFG node set + reachability,
cdg, ddg where syntactic semantics coincide). Pin the documented divergences: exceptional-edge shape/density and within-line attribution on multi-statement lines. The AST engine is the reference.
Notes / design references
Scope
The second L3 engine of the two-engine design (
docs/design/specs/l3-intraprocedural-dataflow-design.md, steps 6–7). The AST engine (the default, source-only) landed in #183; this issue tracks the WALA-based L3 engine behind--l3-engine walaplus the differential gate that cross-checks the two engines.This is the intended next work item after the AST-engine PR.
Work
--l3-engine wala— currently accepted but rejected with a clear "not yet implemented" error. Implement it.line:colis adopted from the matched AST node, never synthesized. This is the machinery L4's semantic DDG reuses.SSACFG+ISSABasicBlockprojected via B.1, normalized to one@exit; CDG from WALA dominators/post-dominators; DDG from WALA SSA def-use, same syntacticprov:["ssa"]contract as the AST engine (no points-to at L3).cdg,ddgwhere syntactic semantics coincide). Pin the documented divergences: exceptional-edge shape/density and within-line attribution on multi-statement lines. The AST engine is the reference.Notes / design references
rta); it degrades to a clear error leaving L2 intact.finallyparity:javacduplicates the finally in bytecode, but the copies collapse to the same single sourceline:colnode the AST engine produces — so the engines converge there (see §4.4.1 and L3 CFG: revisit precise per-path finally modeling (relax one-node-per-line:col) #193).