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 <epsilon> 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:

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 POCR Migration Matrix for the complete source-to-Lotus mapping and the algorithms intentionally merged with an existing implementation. See PEARL Multi-Derivation, Stg Staged Solving, and Sqid Efficient Relation Chaining 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

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.