Classical Grammar-Driven CFL Reachability ========================================== ``CFL/Classical`` is the general grammar-driven part of Lotus's CFL subsystem. It is independent of the specialized interleaved-Dyck and MCFL solver representations. Architecture ------------ The public and implementation trees mirror the same responsibility-based layout: ``Core/`` Canonical grammar, labeled graph, relation storage, and validation. ``Solvers/SolverSession`` Public backend selection, incremental session state, and solver orchestration. ``Solvers/Engines/`` Reusable relation engines. ``TransitiveClosure`` is the generic incremental closure engine. ``Engines/PEARL/``, ``Engines/POCR/``, ``Engines/SQID/``, and ``Engines/STG/`` contain the paper algorithms; ``Engines/POCR/`` also contains its specialized alias/value-flow engines and client grammars. ``Solvers/Preprocessing/`` Graph simplification and RSM-guided foldability analysis. ``Solvers/ConstraintGrounding`` The separate structural constraint-grounding analysis. ``Clients/Alias/`` PAG/PEG encoding, Aser synchronization, and the LLVM alias facade. ``Clients/ValueFlow/`` SVFG preparation, encoding, and context-sensitive value-flow queries. ``Grammar`` Parses declared start, terminal, and nonterminal symbols; normalizes whitespace-delimited ``*`` and ``?`` EBNF; binarizes long productions; and compiles string symbols to stable integer IDs. ``GrammarParseOptions`` instantiates correlated attributed symbols such as ``call_i``/``ret_i`` using variable-specific or per-symbol domains. Graph labels provide domains automatically when the command-line driver is used. Only ```` is reserved for epsilon; ``e`` and ``epsilon`` are ordinary terminals. A configurable expansion limit rejects independent attribute domains whose Cartesian product would grow unexpectedly large. The former independent ``CNFGrammar`` parser/transformer has been removed; this is the only grammar normalization implementation. ``LabeledGraph`` Stores the base problem boundary. Solver sessions keep derived facts in a separate relation; only explicit incremental terminal additions modify the graph. Text, DOT, and JSON readers are available; DOT accepts quoted IDs and JSON has an explicit ``nodes``/``vertices`` section for isolated vertices. Plain, reverse, and bidirectional transformations are explicit. Forward and reverse label indices support direct incoming-edge queries. ``Relation`` Separates terminal and derived facts from the graph frontend. Sparse-set, LLVM sparse-bitvector, and endpoint-quotient implementations provide indexed successor and predecessor lookup and streaming edge enumeration. ``SolverSession`` Retains a relation and worklist across calls. ``addTerminalEdge`` followed by ``solve`` supports clients that discover constraints incrementally. Nullable self-facts are seeded only for newly added nodes. ``Solvers/Engines/POCR/ClientGrammars`` Holds POCR's exact standard and grammar-rewritten production tables for the alias and value-flow engines. These are data selections over the shared solver, not additional clients. Solver backends --------------- ``SparseSet`` Conventional indexed worklist saturation with hash-set relations. ``SparseBitVector`` The same worklist algorithm with per-node, per-symbol LLVM sparse bitvectors. This is a storage choice, not the POCR algorithm. ``Graspan`` Executes POCR's source-ordered epoch/delta evaluation. Each source combines its ``old`` and ``new`` facts in the same four phases as ``GspanAA``/``GspanVFA``, then immediately updates that source's two relations. Old sources are revisited while any middle-node delta remains. ``Pearl`` Implements ASE 2023 multi-derivation with separate non-transitive, partially transitive, and fully transitive propagation. Select it with ``--solver pearl``. ``Sqid`` Implements OOPSLA 2026 adaptive and differential relation chaining with dual old/delta graph views. Select it with ``--solver sqid``. ``TransitiveClosure`` Uses sparse bitvectors generally and a dedicated incremental forward/reverse bitvector closure for every production ``X -> X X``. Inserting ``u -> v`` crosses predecessors of ``u`` with successors of ``v``. It does not retain copied reachability trees or a second hash-set closure. ``Pocr`` Ports POCR's paired predecessor-tree/successor-tree propagation to Lotus containers. Primary arcs and secondary closure facts follow the original FIFO scheduling, and linear-recursive rules use early-pruned tree traversal instead of generic relation joins. Sparse bitvectors expose the complete relation to clients and preserve non-empty-path reflexive pairs introduced by cycles. ``HierarchicalPocr`` Uses the same paired-tree closure as ``Pocr`` and prioritizes facts for transitive symbols ahead of the ordinary grammar worklist. Select it with ``--solver hpocr``. ``FullyOrdered`` Ports FOCR's forward/backward edge-critical-graph maintenance. The critical graph is a reduced reachability skeleton, while the public relation remains the complete exact CFL relation. Select it with ``--solver focr``; add ``--focr-scc`` for POCR's optional critical-graph cycle simplification. ``EndpointQuotient`` Select with ``--solver endpoint-quotient``. Retains exact reachability as cells over grammar-dependent source and target partitions, with nullable diagonals represented separately. Solving and ordinary queries do not materialize the complete concrete relation. Identical partitions, lifts, and bridges are shared; dense identity-lift joins propagate bitmap deltas. Other joins use indexed cell traversal and cache repeated nontrivial lift products. Temporary join indexes and grammar plans are released after solving. The endpoint engine implements ``Relation`` directly. It buffers new input facts and rebuilds its static quotient on the next ``solve()``. Until that solve completes, queries see the previous snapshot (or an empty relation before the first solve). An unchanged solve performs no new solver work. Adding an isolated node also invalidates the snapshot, so nullable facts for that node appear after the next solve. Alias-client grammar extensions rebuild from the encoded input graph; they do not expand and reinsert the previous quotient closure as axioms. All backends return exactly the same grammar-relative relation. Tests compare their complete triples, not only start-symbol answers, against an independent cubic recognizer and exercise incremental additions and non-nullable cycles. ``ConstraintGroundingSolver`` is separate: it computes structural set-variable grounding statistics and does not expose a CFL node-pair relation. Querying compressed results --------------------------- Clients use the same relation interface for every backend: .. code-block:: cpp const auto &relation = session.relation(); const auto symbol = grammar.symbolId("S"); bool reachable = relation.contains(symbol, source, target); relation.forEachSuccessor(symbol, source, [&](NodeId target) { consumeTarget(target); }); // Return false to stop; visitEdges returns false when stopped early. relation.visitEdges(symbol, [&](const RelationEdge &edge) { return consumeEdgeAndContinue(edge); }); ``visitSuccessors`` and ``visitPredecessors`` also support early termination; the ``forEach`` variants take void callbacks. ``visitEdges(visitor)`` visits all symbols, and ``visitEdges(symbol, visitor)`` visits only the selected symbol. Traversal order is unspecified, facts are unique, and callbacks must not mutate or solve the relation. ``edges()`` and ``edges(symbol)`` explicitly collect a vector when the caller needs owned results or sorting. The endpoint backend expands only the queried source row or target column for local enumeration. Full enumeration necessarily takes time proportional to the output, but does not allocate a full result vector. Nullable diagonals are included exactly once, even when a positive-length cycle also reaches the same node. The standalone endpoint ``Solver`` additionally exposes ``forEachPositiveRectangle`` for clients that process whole compressed blocks. ``edgeCount`` reads cached exact counts. Session ``Count`` statistics exclude self-pairs and deduplicate overlapping symbols; the endpoint backend computes this union by grouping equivalent source rows, without storing all concrete pairs. ``relation_payload_bytes_estimate`` measures retained compressed containers and buffered inputs, excluding allocator overhead and temporary peak solve memory. Endpoint statistics expose partition/bridge/lift builds, insertion attempts, duplicate inserts, skipped repeated binary outputs, and bitmap join words. ``binary_joins`` still counts compatible cell pairs even when a bitmap operation handles many of them at once. Core phase timings exclude snapshot replacement and session-level statistics; use the session's ``solve_time_microseconds`` for end-to-end solve timing. POCR support utilities ---------------------- ``GraphSimplification`` ports the client preprocessing passes without SVF: direct-edge SCC elimination, PEG/IVFG folding, common-dereference merging, and FastDyck-style pruning of non-contributing edges. The general driver exposes these through ``--scc-elimination``, ``--graph-folding``, ``--interdyck-pruning``, and ``--simplification-flavor alias|value-flow``. Direct foldable pairs are collected once after SCC elimination; alias common-dereference merging and FastDyck then use their own worklists, preserving the original phase boundaries. ``RecursiveStateMachine`` and ``FoldabilityChecker`` implement POCR's RSM transition semantics and node-pair foldability proof. The ``lotus-cfl-foldability`` tool reads an RSM and a pattern file. ``lotus-cfl-pocr`` runs the four hand-specialized engines directly on POCR ``.peg``/``.vfg`` datasets and the standard, Graspan, grammar-rewritten, and rewritten-Graspan client engines. This is an engine driver; it does not introduce a third analysis client. It also exposes ``--scc``, ``--graph-folding``, ``--interdyck``, ``--simplify-graph``, ``--graph-output``, and ``--focr-scc``. ``SolverOptions::unidirectional`` implements POCR's ``Insert``/``Follow`` summarization discipline. All facts remain available as exact output, while only terminals, nullable seeds, and ``Insert`` symbols are indexed as future join candidates. Use ``--unidirectional`` in the general driver. See :doc:`pocr_migration` for the complete source-to-Lotus mapping and the algorithms intentionally merged with an existing implementation. See :doc:`pearl`, :doc:`stg`, and :doc:`sqid` for the papers, key ideas, published algorithms, Lotus adaptations, and validation boundaries. Adapters -------- Adapter implementations are split by dependency: ``CanaryClassicalCFLAliasClient`` PAG and PEG encodings, ``AliasClient``, and ``solveToFixedPoint`` for alternating client-defined discovery with incremental saturation. PEG loads and stores added after solving are converted through existing or reusable synthetic dereference nodes. ``solveSpecialized(Pocr|Focr)`` selects the hand-specialized engine without creating a generic ``SolverSession``. For PAG input, ``AliasClient`` lowers ``load``/``store`` constraints in one structural pass, using indexed address-taken objects or one reusable synthetic dereference per pointer. Unknown raw terminals remain hard errors rather than being ignored. ``CanaryClassicalCFLValueFlowClient`` SVFG preparation, value-flow encoding, ``ValueFlowClient``, and its grammar-driven and specialized engine integration. ``AserConstraintAdapter.h`` A header-only converter from Lotus's native AserPTA constraint graph to the alias client input. A client-provided offset resolver preserves field GEP attributes, while ``AserAliasSynchronizer`` maps new Aser nodes and constraints into successive ``solveToFixedPoint`` rounds, including when PEG has inserted synthetic nodes. Newly observed GEP attributes are batched per synchronization round so the grammar is extended and parsed once. ``LLVMCFLAliasAnalysis`` / ``lotus-cfl-alias`` Build Aser's constraint/model frontend without running its points-to solver. A lightweight projection from solved CFL value aliases to explicit address-taken function objects resolves indirect and intercepted calls; normal Aser callbacks then create actual/formal, return, heap, and newly reached function constraints. Constant global initializers and pointer-bearing ``memcpy`` operations receive explicit constraints when the Aser frontend does not emit them. Supplemental ``memcpy``/``memmove`` constraints are field/range-aware and are revisited after newly discovered callees add nodes. Unmapped pointers and mapped results of unsupported pointer-producing LLVM instructions are conservatively reported as may-alias; explicit unknown facts propagate through SSA uses and affected memory rather than being converted into a no-alias result. ``AliasClient::pointsTo`` is an object-valued relation derived directly from address, copy, GEP, load, and store constraints. It represents fixed fields with allocation-plus-cumulative-offset objects. Variant GEPs retain a known offset congruence (for example, an array-element stride) when LLVM can provide one and otherwise use an arbitrary-offset field object. Synthetic field objects can be projected to their allocation with ``baseObject``. This full object relation is computed lazily only for ``pointsTo`` or enhanced alias queries; ordinary solving and indirect-call discovery do not run a second pointer-analysis fixed point. ``ValueFlowClient`` / ``lotus-cfl-vf`` Implement SVF's second classical-CFL client, ``CFLVF``. The driver builds Lotus's AserPTA-backed SVFG and MemorySSA, removes dereference inputs and stale strong-update flow, keeps ``direct``, ``indirect``, and ``thread`` terminals distinct, and encodes call/return edges as matched ``call_i``/``ret_i`` terminals, and solves context-sensitive value-flow reachability with any classical backend. ``hasBalancedFlow`` (and the compatibility spelling ``hasFlow``) queries the same-context summary relation ``A``. ``hasRealizableFlow`` queries ``R``, which additionally permits unmatched returns at the beginning and unmatched calls at the end while retaining callsite matching for balanced pairs. General realizable queries require a grammar backend; the specialized vertical-propagation engines expose balanced summaries only. The derived relations are the sound union of the edge categories, not a path-feasibility or memory-object proof. ``solveSpecialized(Pocr|Focr)`` selects the native vertical-propagation engine. SVFG strong-update preparation requires explicit ``isSingleton`` metadata, nonrecursive stack ownership, and evidence that the LLVM store overwrites the whole represented object. Loop/recursive allocations and partial writes retain weak-update input flow. Alias and value-flow relation queries require ``solve()`` first and throw a ``logic_error`` when called on an unsolved client. ``ReachabilityStats`` separates session snapshots (graph/relation sizes and payload estimates) from work performed by the current ``solve()`` call (iterations, duplicates, peak worklist, timing, and transitive propagation). ``solveToFixedPoint`` sums per-call work and retains the final snapshots. The LLVM alias facade additionally reports ``frontend_time_microseconds``, ``client_initialization_microseconds``, and ``client_discovery_microseconds`` so encoding/synchronization costs remain distinguishable from solver time on whole-program workloads. Command line ------------ .. code-block:: console cmake --build build --target lotus-cfl-classical lotus-cfl-alias \ lotus-cfl-vf lotus-cfl-foldability lotus-cfl-pocr build/bin/lotus-cfl-classical \ --grammar grammar.txt --graph graph.txt --solver sparse-bitvector --json-stats build/bin/lotus-cfl-alias --solver sparse-bitvector --encoding pag \ --check-annotations module.bc build/bin/lotus-cfl-alias --engine pocr-aa --encoding peg \ --check-annotations module.bc build/bin/lotus-cfl-vf --solver transitive-closure \ --query main::source,main::sink module.bc build/bin/lotus-cfl-vf --engine focr-vfa \ --query main::source,main::sink module.bc build/bin/lotus-cfl-pocr --engine pocr-aa --graph input.peg \ --query 10,20 --json-stats build/bin/lotus-cfl-pocr --engine grgspan-aa --graph input.peg \ --json-stats build/bin/lotus-cfl-pocr --engine focr-vfa --graph input.vfg \ --simplify-graph --focr-scc --graph-output reduced.vfg build/bin/lotus-cfl-classical \ --grammar grammar.txt --graph graph.txt --solver pocr --json-stats build/bin/lotus-cfl-classical \ --grammar pocr.cfg --graph input.peg --solver graspan \ --unidirectional --simplification-flavor alias --simplify-graph Use ``--graph-mode plain|matrix|pag-matrix`` and ``--direction plain|reverse|bidirectional`` to state input semantics. Attributed domains are inferred from graph labels. ``--attribute-domain`` can override a variable (``var:i=1,2``) or symbol kind (``kind:call=1,2``). ``--relation-output``, ``--graph-output``, ``--stats-output``, ``--start-only``, and ``--validate-only`` support reproducible batch workflows. JSON statistics include grammar/graph sizes, worklist behavior, estimated container payload, timings, transitive-closure propagation, POCR tree, and FOCR critical-graph statistics. Payload estimates are not RSS or allocator measurements and must not be used as real memory totals. Input formats ------------- Text graphs contain one ``source,target,label`` edge per line. POCR/SVF-style tabular ``source target label [attribute]`` files (including ``.peg`` and ``.vfg``) are accepted directly; ``call_i 7`` is normalized to ``call_7``. POCR's singular ``Production:`` grammar syntax and ``Insert:``, ``Follow:``, and ``Count:`` sections are parsed natively. In this legacy syntax an indexed LHS derived from non-indexed symbols receives index zero, and an ``_i`` graph edge without an explicit fourth field is likewise normalized to index zero, matching POCR. The line-oriented DOT subset accepts quoted IDs and ``label=...`` edge attributes; JSON accepts ``nodes`` or ``vertices`` plus labeled ``edges``.