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/, Engines/STG/, Engines/Skewed/, Engines/EndpointQuotient/, Engines/CAT/, and Engines/IEOCE/ contain the paper algorithms; Engines/CERT/ is the Lotus-native cardinality-certified engine. Engines/POCR/ also contains the client grammars. Engines/SubcubicAA/ provides the specialized OOPSLA 2014 PEG memory/value alias algorithms through a separate graph-analysis API.

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. This is the only grammar normalization implementation in the classical solver.

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.

Skewed

Implements the PLDI 2024 skewed-tabulation worklist with separate indexed (E) and propagating (PE) facts. Select it with --solver skewed. The general SolverSession backend preserves Lotus’s complete-relation contract and safely rebuilds after terminal-edge or isolated-node updates, because old PE facts are not indexed as future join candidates. The engine API also exposes the supplied conservative target-only static rewrite; it is intentionally not enabled by the complete-relation backend.

Cat

Implements ICSE 2026 context-aware tabulation with per-symbol usage contexts and guarded transitivity rewrites. Select it with --solver cat.

Iea

Implements OOPSLA 2024 iterative-epoch online cycle elimination. Select it with --solver iea.

IeaOcr

IEA with online cycle reduction and minimum-equivalent graphs. Select it with --solver iea-ocr.

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 builds refined partitions on the next solve(). The previous compressed closure is migrated into those partitions as already-processed cells, so saturation visits only facts induced by the delta. 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.

CertCFL

Select with --solver cert. Cardinality-certified exact all-symbol solving: universal-degree certificates and a finite threshold domain promote dense blocks to exactness, with symbolic nullable identity. observed must remain unset and unidirectional is rejected. The kernel is available directly for selected-symbol observation contracts. See CERT-CFL: Cardinality-Certified Exact Solving for the promotion rules, resource limits, and the completed-snapshot adapter contract.

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. These utilities remain available through their C++ APIs and unit tests.

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. See CAT and IEOCE Engines for the CAT and IEOCE engines. See Subcubic PEG Alias Analysis for the specialized PEG memory/value alias engine and its lotus-cfl-subcubic-aa driver.

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. 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 client 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. The derived relations are the sound union of the edge categories, not a path-feasibility or memory-object proof.

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-solve lotus-cfl-alias lotus-cfl-vf
build/bin/lotus-cfl-solve \
  --grammar grammar.txt --graph graph.txt --solver sparse-bitvector --json-stats

build/bin/lotus-cfl-alias --solver sparse-bitvector --encoding cfl-peg \
  --check-annotations module.bc

build/bin/lotus-cfl-vf --solver transitive-closure \
  --query main::source,main::sink module.bc

The LLVM frontends can also export their normalized CFL instance for replay by any graph-level backend:

build/bin/lotus-cfl-alias --encoding cfl-peg \
  --dump-cfl-graph module.peg --dump-cfl-grammar alias.grammar module.bc

build/bin/lotus-cfl-vf --encoding classical-cfl \
  --dump-cfl-graph module.vfg --dump-cfl-grammar value-flow.grammar module.bc

build/bin/lotus-cfl-solve --graph module.vfg \
  --grammar value-flow.grammar --solver pocr --result-scope count

The native value-flow encoding remains the default. classical-cfl projects all ordinary SVFG edges to a and preserves context with call_i and ret_i. The exported graph records isolated nodes, and the exported grammar preserves Insert, Follow, and Count metadata, so replay retains the same nullable and target-relation semantics.

Alias encodings are intentionally distinct. cfl-peg is the recommended default and the interchange-compatible a/d/f_i analysis. pag keeps the constraint-level formulation for diagnostics and comparisons. peg is the Lotus extended grammar with ArrayPath and Memcpy summaries. Removing the latter two would discard different analysis semantics rather than merely remove duplicate serializations.

build/bin/lotus-cfl-solve \
  --grammar grammar.txt --graph graph.txt --solver pocr --json-stats

build/bin/lotus-cfl-solve \
  --grammar pocr.cfg --graph input.peg --solver graspan \
  --unidirectional --simplification-flavor alias --simplify-graph

External graph/grammar datasets can select their declared Count relation without going through an LLVM frontend. Backends that support target-projected evaluation use that scope during solving; other backends compute their full relation and filter the reported output:

build/bin/lotus-cfl-solve \
  --grammar benchmarks/real-world/CFL/Classical/grammars/aa.ecfg \
  --graph benchmarks/real-world/CFL/Classical/spec2017/pegs/lbm.g \
  --graph-mode plain \
  --solver skewed --result-scope count --json-stats

When a target-projected backend consumes a transformed grammar, its Follow set supplies the exact propagating nonterminals. Default solver sessions remain all-symbol and therefore preserve the complete Relation contract used by the LLVM clients. Dataset-specific batch policy is kept outside the binary in scripts/cfl/run_cfl_classical.py.

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.