CFL Reachability Components

This page lists the CFL reachability subsystems, their source locations, and the reachability guarantee each one provides.

Classical CFL Reachability

Grammar-driven CFL reachability utilities and solver backends

Location: include/CFL/Classical/, lib/CFL/Classical/. Both trees use Core/, Solvers/Engines/ (including PEARL/, POCR/, SQID/, STG/, Skewed/, EndpointQuotient/, CAT/, IEOCE/, and CERT/), Solvers/Preprocessing/, Clients/Alias/, and Clients/ValueFlow/. The two client implementations consistently use AliasClient.* and ValueFlowClient.* filenames.

Features:

One canonical grammar parser with EBNF expansion and binary normalization
Labeled graph construction for text, DOT, PAG, and PEG-style encodings
Solver backends selected by the classical driver: sparse-set, sparse-bitvector, Graspan epoch/delta, transitive-specialized, POCR/hierarchical-POCR, and fully ordered edge-critical-graph
PEARL multi-derivation, Sqid relation chaining, Stg staged solving, and CERT-CFL cardinality-certified solving
Native POCR grammar/graph input, unidirectional summarization, client graph simplification, and RSM-guided foldability checking
Incremental solver sessions for dynamically discovered terminal edges
Adapters for Lotus AserPTA constraint graphs and Lotus SVFG value flow
End-to-end LLVM bitcode alias analysis with CFL-driven indirect calls
End-to-end context-sensitive LLVM value-flow analysis over Lotus SVFGs
Strong-update-aware CFL preparation for Lotus SVFGs

See PEARL Multi-Derivation, Stg Staged Solving, and Sqid Efficient Relation Chaining for paper references, key ideas, algorithm walkthroughs, and exact source mappings. See CAT and IEOCE Engines for the CAT and IEOCE engines. See CERT-CFL: Cardinality-Certified Exact Solving for the CERT-CFL engine.

Dynamic Bidirected Dyck Reachability

Exact single-language Dyck reachability under insertions and deletions of complementary edge pairs. The POPL 2022 C++ algorithm retains degree-based merging, path compression, linked worklists, and acyclic splitting. Cyclic deletion safely recomputes the remaining graph.

Location: include/CFL/DynamicDyck/, lib/CFL/DynamicDyck/

See Dynamic Bidirected Dyck Reachability for the reusable API, artifact formats, and cycle-correction details.

Interleaved-Dyck Core

Shared typed Label, Edge, Graph, and Pair types plus the DOT parser used by interleaved-Dyck benchmark datasets.

Location: include/CFL/InterleavedDyck/Core/, lib/CFL/InterleavedDyck/Core/

StagedBounds consumes this graph directly, Unary applies unary projection, and MCFL converts it through a typed-to-generic adapter.

Exact Unary Interleaved Dyck

Exact component reachability for bidirected unary D1-interleaved-D1. The module provides adaptive counter flattening and the POPL 2022 fixed-counter exact baseline.

Location: include/CFL/InterleavedDyck/Unary/, lib/CFL/InterleavedDyck/Unary/

See Exact Unary Interleaved Dyck for both algorithms, their exactness boundary, and benchmark eligibility rules.

Interleaved-Dyck Staged Bounds

Staged under- and overapproximation for reachability under two interleaved families of Dyck constraints.

Location: include/CFL/InterleavedDyck/StagedBounds/, lib/CFL/InterleavedDyck/StagedBounds/

This component computes a certified union-Dyck lower bound and progressively tighter projected-CFL upper bounds; it is not an exact solver for the general typed problem.

Features:

DOT parsing for parenthesis, bracket, and neutral edges
Dyck-over-the-union underapproximation
Projected-language intersection and derivation-tracing mutual refinement
Stronger parity grammar and pairwise on-demand refinement
Taint and value-flow benchmark modes

Multiple Context-Free Language Reachability

All-pairs reachability for non-deleting, non-permuting MCFGs and the POPL 2025 typed underapproximation hierarchy.

Location: include/CFL/InterleavedDyck/MCFL/, lib/CFL/InterleavedDyck/MCFL/

Features:

All five normal-form MCFL rule types with structural validation
Indexed worklist saturation and tuple reachability pruning
Concrete path witnesses from retained derivation DAGs
G_d^circ and G_d^+ grammar generation for arbitrary dimensions
Dimension-ordered condensation, DOT input, and command-line tool
Adapter from the shared typed interleaved-Dyck graph

Guarantee Summary

Choosing an interleaved-Dyck implementation
API	Intended use	Guarantee
`interleaved_dyck::mcfl::InterleavedDyckSolver`	Proven typed pairs through `G_d`	Underapproximation
`interleaved_dyck::unary::FixedCounterSolver`	POPL 2022 exact fixed-counter baseline	Exact component partition
`interleaved_dyck::unary::AdaptiveSolver`	Bidirected unary projection	Exact component partition
`interleaved_dyck::staged_bounds::Solver`	Typed lower/upper refinement	Approximation bounds

CSIndex (Context-Sensitive Indexing)

Precomputed summaries and reachability indexes that answer context-sensitive queries without re-running the base solver.

Location: include/CFL/CSIndex/, lib/CFL/CSIndex/

The implementation is split into FLARE and SCS. FLARE owns the extended-Dyck graph and indexing algorithms; SCS builds policy products and then reuses FLARE. See Context-Sensitive Reachability Indexing for the public namespaces and directory layout.

Components:

FLARE path-tree, Grail, and tabulation indexes over an extended-Dyck graph
SCS sanitizer-aware product index with optional witness replay
Point queries, fixed-batch queries, and construction/query statistics

Interleaved-Dyck Graph Reduction

PLDI 2020 interleaved-Dyck graph simplification. This component transforms a DOT graph and does not itself return the final reachability relation.

Location: lib/CFL/InterleavedDyck/GraphReduction/

Features:

Two-color summary construction and degree-based node merging
Iterative Python orchestration until no further edge is removed
Explicit directed versus already-bidirected input mode
Summary representation kept internal to the lib subtree