L3 CFG: revisit precise per-path finally modeling (relax one-node-per-line:col)

[sinha108]

Context

L3's AST CFG engine (#183) models a finally block as a single body node keyed by its source line:col, whose completion fans out to the union of every exit's continuation — normal completion, each catch, return/break/continue, and uncaught throw. This is a sound over-approximation: it never omits a real edge, and it makes the finally post-dominate the try body (so CDG is correct).

It is forced by the schema invariant that every body node has exactly one line:col id. The textbook fix — duplicating/inlining the finally per exit path, as javac does in bytecode — would produce copies that share the same source line:col and therefore collide under that identity.

See docs/design/specs/l3-intraprocedural-dataflow-design.md §4.4.1.

The imprecision

Because the single finally node's successors are the union of all continuations, the CFG admits infeasible paths: after the finally, control appears able to reach every exit target regardless of how the finally was entered.

int f(int x) {
    int r = 0;
    for (int i = 0; i < x; i++) {
        try {
            if (p(i)) break;   // break  -> finally -> loop exit
            r = g(i);          // normal -> finally -> loop back
        } finally {
            cleanup();         // C: fans out to BOTH the loop exit and the loop back
        }
    }
    return r;
}

cleanup() (C) fans out to both the loop-exit and the loop-back edge; the model cannot tell which continuation applies to which entry, so both are always present. Downstream control- and data-dependence around finally inherit this over-approximation.

JavaParser / WALA parity

WALA analyzes bytecode, where javac duplicates the finally body along each exit path (plus a synthetic catch-all handler that runs it and rethrows), so WALA's bytecode CFG is precise (per-copy, single successors). But the planned WALA L3 engine (#183/#184) projects instructions back to source line:col; the duplicated copies share source positions and collapse to one node, merging their edges — reproducing the same single-node fan-out the AST engine produces.

So the two engines converge on finally rather than diverge, and the differential gate can require they agree on the finally node and its reachability. The one expected divergence is exception-edge density: WALA's catch-all lets any instruction throw into the finally, whereas the AST engine edges only from statements that syntactically contain a call/allocation.

Proposed future work

Recover per-path precision by relaxing the one-node-per-line:col invariant for finally copies — e.g. suffixed ids such as @<line:col>#normal, @<line:col>#return, @<line:col>#break:<label> — one copy per exit path, each with a single successor.

Costs to weigh:

• complicates DDG/CDG and every consumer that joins on body-node ids (a line:col no longer uniquely identifies a node);
• the WALA engine would need to keep the bytecode copies distinct rather than collapsing them, and map each to a suffixed id;
• the schema localId pattern would need to admit the suffix.

Decide based on whether a downstream need (precise slicing/taint through finally) outweighs the identity simplicity. Until then the sound over-approximation stands.

References

• Design: docs/design/specs/l3-intraprocedural-dataflow-design.md §4.4.1, §5.2, §7.2
• L3: codeanalyzer-java: L3 intraprocedural dataflow (CFG/CDG/DDG) #183 · epic: Epic: codeanalyzer-java → canonical schema v2 + L3/L4 dataflow (analyzer + SDK) .github#42