Subcubic PEG Alias Analysis

Paper and scope

Lotus implements Qirun Zhang, Xiao Xiao, Charles Zhang, Hao Yuan, and Zhendong Su, Efficient Subcubic Alias Analysis for C, OOPSLA 2014 (DOI 10.1145/2660193.2660213).

The engine computes all-pairs memory and value aliases on a pointer expression graph (PEG). The implementation covers:

  • Algorithm 1 and the transition machines in Figures 10 and 11;

  • Algorithm 2, which reuses the memory phase’s summaries to derive value aliases;

  • the fast-set differences in Section 3.4; and

  • the connected-component decomposition in Section 3.3.2.

The input language is the paper’s assignment/dereference PEG. This specialized API is independent of the arbitrary-grammar SolverSession contract and has a dedicated command-line tool, lotus-cfl-subcubic-aa. It operates on graphs; it does not construct a PEG directly from C or LLVM bitcode.

Relations and input contract

An a edge goes from an assignment’s right-hand side to its left-hand expression. A d edge goes from an expression e to its dereference *e. The corresponding reverse labels are abar and dbar. With ? denoting an optional path and * denoting repetition, the paper’s grammar is:

M -> dbar V d
V -> (M? abar)* M? (a M?)*

M(u, v) means that the expressions may denote the same memory location; V(u, v) means that they may evaluate to the same pointer value. Both relations are symmetric. V includes every diagonal pair because the empty path is valid. M contains only paths actually derived through dereferences. Neither relation is transitively closed.

Every assignment target must have at least one incoming d edge. This is the PEG property used in the paper’s Lemmas 5 and 6; arbitrary labeled graphs need not satisfy it. The core validates this property and rejects out-of-range vertex IDs. Duplicate edges do not change the result.

The low-level Problem stores only forward assignment and dereference edges, with reverse edges implicit. The LabeledGraph adapter requires explicit matching reverse edges and accepts only a, abar, d, and dbar. The driver can add missing reverses when --bidirectional is explicitly requested. Unknown labels remain errors after this transformation.

Field labels such as f_i, load/store constraints, and the extended Lotus ArrayPath/Memcpy grammar are outside this input language. The existing encodeCflPegGraph helper can supply assignment/dereference edges from Lotus alias constraints, but any resulting field labels or violated assignment-target conditions require a suitable frontend encoding. The existing AliasClient also applies its own graph reductions; the new adapter preserves the vertex IDs and graph structure supplied to it.

Algorithm 1: memory aliases

The engine retains seven summary relations: M, V1, V1Prime, D1, D1Prime, D2, and D2Prime. A worklist stores newly discovered summary facts.

Initialization derives dbar V d paths using nullable V. In a canonical expression graph this inserts the reflexive M pair for each dereferenced expression. Lotus also supports a source with several dereference successors: it seeds every ordered pair of those successors, including the diagonal, to preserve the same grammar semantics.

Phase one extends the right endpoint of an M, V1, or V1Prime summary along the outgoing edges permitted by Figure 10. An encountered dereference creates the pivot summary used by phase two. Phase two extends the left endpoint according to Figure 11, and a matching dereference produces a new M pair. Every new memory-alias fact is inserted in both orientations.

Prime states enforce the nonconsecutive-memory-path restriction. The transition table prevents the propagation from treating M as a transitive relation or returning to a forbidden assignment direction. New memory edges reenter the worklist in both orientations and initiate further two-phase propagation.

Algorithm 2: value aliases

After the memory phase reaches its fixed point, Algorithm 2 closes the existing V1 relation transitively and obtains V1Prime from V1 and M. These summaries represent the forward paths needed by the paper’s Gamma and Upsilon reachability construction.

For each original assignment, the engine constructs the initial V2 seeds using the target’s V1, V1Prime, and M successors. Its final join combines these immutable initial seeds with the completed forward relations. Newly generated output pairs do not become additional V2 join inputs. This preserves the single central assignment required by the Upsilon construction; recursively joining new output would produce false transitive aliases.

The public value relation combines those nontrivial paths with their reverse orientations, the memory-alias paths, and all reflexive paths. Selecting compute_value_aliases = false stops before this phase. Value queries, counts, and visitors then throw std::logic_error rather than returning incomplete information.

Fast sets and components

Each relation has packed rows over the component’s local vertex IDs. With fast sets enabled, propagation subtracts the destination’s known bits from the source row a word at a time and visits only newly discovered elements. The incoming relation is indexed as well, supporting phase two’s reversed endpoint propagation. use_fast_sets = false runs the same algorithm with scalar element-by-element membership checks over the same storage.

By default, the original PEG is split into weakly connected components and each component is solved independently. The result retains the mapping from the original vertex IDs to component-local IDs, so queries use the original IDs. Cross-component queries return false; isolated vertices still have their reflexive value pair. decompose_components = false processes the input as a single graph. The connected_components counter records the number of independently processed graphs and largest_component records the largest processed graph.

The implementation uses 64-bit words. A fast-set difference scans at most ceil(component_size / 64) words plus its output elements. The paper’s O(n^3 / log n) bound assumes a uniform-cost RAM with word size Theta(log n). The implementation provides the corresponding word-parallel operations on fixed-width machine words; its name does not constitute a measured speedup or a reproduction of the paper’s benchmark results. Explicit pair enumeration also costs at least the output size.

Public API

Core header

CFL/Classical/Solvers/Engines/SubcubicAA/SubcubicAA.h

Lotus graph adapter

CFL/Classical/Solvers/Engines/SubcubicAA/SubcubicAAAdapter.h

Implementation and build target

lib/CFL/Classical/Solvers/Engines/SubcubicAA/, compiled into CanaryClassicalCFL.

The namespace is lotus::cfl::classical::engines::subcubic. A minimal core API example is:

#include "CFL/Classical/Solvers/Engines/SubcubicAA/SubcubicAA.h"

namespace aa = lotus::cfl::classical::engines::subcubic;
aa::Problem problem;
problem.nodes = 4; // &x, x, &y, y
problem.dereferences = {{0, 1}, {2, 3}};
problem.assignments = {{1, 3}}; // y = x

aa::Result result = aa::solve(problem);
bool aliases = result.valueAlias(1, 3); // true

For a Lotus graph, use aa::toSubcubicAliasProblem(graph) before calling solve. The returned move-only Result retains packed relations and supports constant-time memoryAlias and valueAlias queries. It also provides counts, per-source successor visitors, and whole-relation visitors. Visitors receive original IDs, enumerate ordered pairs once, and stop when the callback returns false. Counts include diagonal pairs and both orientations. Every query and per-source visitor checks its vertex IDs.

Command line

The driver accepts a positional graph path or --graph FILE. Text/PEG files use Lotus’s source target label format; labeled DOT and Lotus JSON graphs use the existing LabeledGraph parser.

build/bin/lotus-cfl-subcubic-aa \
  tests/regress/CFL/Classical/subcubic-aa-figure4.graph \
  --query 'a,*d' --json-stats

build/bin/lotus-cfl-subcubic-aa \
  tests/regress/CFL/Classical/subcubic-aa-figure4.graph \
  --memory-only --query 'b,*c' --print-aliases

build/bin/lotus-cfl-subcubic-aa --graph physical-edges.peg \
  --bidirectional --no-fast-sets --no-components

--relation memory|value selects the queried and enumerated relation; the default is value. --memory-only selects memory by default, and an explicit --relation value is incompatible with it. --query LHS,RHS uses exact vertex names. --print-aliases lists ordered pairs sorted by source and target names; without JSON it emits M or V followed by the two names, separated by tabs.

--json-stats emits a single JSON object with work counters, options, relation counts, and any requested query or alias-pair array. In memory-only mode, value_aliases is null and value_aliases_computed is false. Vertex names are JSON-escaped. Unknown options, invalid graphs, and unknown query vertices produce a diagnostic on stderr and exit status 1.

The supplied Figure 4 example contains 10 vertices, 7 ordered memory-alias pairs, and 30 ordered value-alias pairs. It demonstrates V(a, *d) and V(*d, e) while V(a, e) is false.

Build and validation

With the normal Lotus LLVM 14 and other build dependencies installed:

cmake -S . -B build -DCMAKE_BUILD_TYPE=Release \
  -DLOTUS_BUILD_ALL_LIBRARIES=OFF -DLOTUS_BUILD_TESTS=ON \
  -DLOTUS_TOOL_FAMILIES=cfl -DLOTUS_TEST_SUBSYSTEMS=cfl
cmake --build build --target lotus-cfl-subcubic-aa cfl_tests -j2
ctest --test-dir build --output-on-failure \
  -R 'SubcubicAA|classical_cfl_cli_subcubic_'

Unit tests compare all M/V pairs with an independent encoding of Figure 7 run by Lotus’s classical SolverSession. They cover the paper example, nontransitivity, nullable initialization with multiple dereference successors, cycles, duplicate edges, generated valid PEGs, disconnected and isolated vertices, word boundaries, visitor cancellation, memory-only results, and malformed inputs. CLI regression cases check the example, fast/scalar and decomposition modes, reverse-edge handling, argument validation, pair enumeration, and JSON escaping.