POCR Migration Matrix

The POCR implementation is represented in Lotus without an SVF dependency. This page records every algorithm-bearing POCR source group and whether Lotus ports it directly or merges it into an equivalent existing component.

General solvers

StdCFL: SolverBackend::SparseSet and SparseBitVector implement the indexed classical worklist algorithm.
PocrCFL: SolverBackend::Pocr uses paired predecessor and successor reachability trees. Primary transitive arcs are registered before tree traversal; closure pairs are then queued as secondary facts. The X -> X A and X -> A X cases traverse the appropriate tree and prune a subtree when its summary edge already exists, as in checkStree/checkPtree (the pruning helpers of the upstream POCR implementation). Structural identity is kept separate from semantic epsilon, so non-nullable cycles correctly derive reflexive pairs.
HPocrCFL: SolverBackend::HierarchicalPocr adds POCR’s separate FIFO primary list, drains it before the ordinary FIFO worklist, and repeats when ordinary processing produces new primary facts.
FocrCFL and TRFocrCFL: Merged as SolverBackend::FullyOrdered. Its edge-critical graph is the reduced storage, while its public relation exposes the exact closure. The TR variant’s separate secondary container is subsumed by this relation abstraction rather than exposed as a second selector; ECG insertion, redundant-critical-edge removal, and primary/secondary scheduling remain.
TRCFL: Merged into SolverBackend::TransitiveClosure. Lotus’s per-symbol incremental closure already separates transitive pairs from the ordinary relation and omits the literal X -> X X worklist join. POCR’s version has unresolved secondary-edge TODOs, so it is not retained as a duplicate mode.
GspanAA and GspanVFA: Generalized as SolverBackend::Graspan while retaining POCR’s two relations and source-ordered epoch update. For every source it evaluates old + new, unary new, new + old, and new + new, then moves that source’s delta into old and installs its next delta. Sources with no local delta are still revisited for old + new joins through a middle node, matching the artifact implementation.
GRAA, GRVFA, GRGspanAA, and GRGspanVFA: These classes differ only by hard-coded production tables. buildPocrClientGrammar owns exact standard and rewritten alias/value-flow tables; gr-aa/gr-vfa pair them with the worklist and grgspan-aa/grgspan-vfa pair them with Graspan. The larger artifact aanew.cfg/vfnew.cfg grammars also load through the canonical Grammar frontend. Both forms have regression coverage. No duplicate solver class is needed.

Clients and preprocessing

StdAA/PocrAA/FocrAA: The grammar-driven path covers all three. PocrAA and FocrAA are expressed by SolverBackend::Pocr and SolverBackend::FullyOrdered running the standard alias client grammar, which preserves POCR’s horizontal propagation, symmetric V/M facts, dereference matching, and attributed field matching. AliasClient is the sole alias client and selects backends through solve/solveToFixedPoint. The LLVM alias adapter defaults every backend to the CFL-oriented PEG encoding and runs direct SCC elimination plus PEG folding. Subsequent indirect-call constraints are projected through the retained representative map and solved incrementally without an unsound re-fold.
StdVFA/PocrVFA/FocrVFA: The grammar-driven path covers all three. PocrVFA and FocrVFA are expressed by SolverBackend::Pocr and SolverBackend::FullyOrdered running the standard value-flow client grammar, which preserves online reachability insertion and vertical call_i A ret_i matching. ValueFlowClient is the sole value-flow client and selects backends through solve.
SCCElimination, PEGFold, and IVFGFold: Ported by GraphSimplification using Lotus’s non-recursive Tarjan utility, representative maps, source-node preservation, and client-specific folding. Foldable direct pairs are detected once on the post-SCC graph and merged before the separate dynamic common-dereference phase, matching POCR’s phase order rather than repeatedly redetecting direct pairs. POCR d is mapped to the physical Lotus PEG addrbar orientation; vgep and Lotus indirect/thread flow edges participate in their corresponding direct-edge reductions.
PEGInterDyck and IVFGInterDyck: Ported as the prune_interdyck graph-simplification phase. Lotus’s separate lib/CFL/InterleavedDyck/GraphReduction implementation remains the single implementation of the stronger PLDI’20 reduction pipeline; it is not copied into Classical.
RSM and GFPattern: Ported as RecursiveStateMachine, NodePairPattern, and FoldabilityChecker. The port implements the intended false-state and two-box enumeration guards instead of preserving the inverted/accumulating conditions in the artifact source.

Formats, relations, and controls

CFG and CFLGraph/PEG/IVFG: Merged into Grammar and LabeledGraph. Both modern Lotus formats and POCR’s tabular attributed formats are accepted directly. Standard and rewritten alias engines complete abar/dbar/fbar_i exactly as POCR’s PEG initializer does, so physical-only and already-bidirectional PEG files have the same result. Legacy attributed productions retain POCR’s runtime rule that an indexed head gets index zero when neither RHS symbol is indexed; omitted graph-edge indices also default to zero.
CFLData and HybridData: Replaced by Lotus Relation backends and PocrTransitiveClosure.
ECG and BSECG: Merged into FullyOrderedTransitiveClosure. The pointer and bitset ECG variants do not warrant separate public algorithms. POCR’s optional ecgscc path is controlled by SolverOptions::simplify_focr_cycles or --focr-scc and is off by default, matching POCR.
CFLOpt::ucfl: Ported through SolverOptions::unidirectional and the grammar’s Insert/Follow/Count metadata.
CFLStat, AAStat, VFAStat, and output options: Merged into ReachabilityStats and the existing structured command-line reporting. --relation-output, --graph-output, --start-only, and --json-stats cover relation pairs, normalized/preprocessed graphs, count symbols, and reproducible algorithm counters without process-global SVF options.

Statistics and graph/relation output use Lotus’s existing structured CLI reporting. Tests compare all exact solver relations with an independent cubic recognizer over 1,000 generated problems, cover incremental updates, ECG cycle simplification, primary/secondary scheduling, and tree-join execution, and run POCR-format and rewritten client grammars through their applicable backends.