Flow-Sensitive Pointer Analysis

Overview

FlowSensitivePTA is a sparse, flow-sensitive, inclusion-based pointer analysis. Conventional inclusion-based (Andersen-style) analyses are flow-insensitive: they compute a single points-to set per pointer, merged over all program points. The flow-sensitive solver instead tracks points-to facts at each program point, and it is sparse because it solves over the Sparse Value-Flow Graph (SVFG) and its MemorySSA rather than re-analyzing every program point.

The solver maintains:

  • top-level points-to sets for pointer-producing SVFG nodes;

  • per-node, per-object MemorySSA IN and OUT points-to state;

  • explicit Addr/Copy/GEP/Phi/Load/Store and parameter-flow transfer;

  • canonical (allocation, normalized byte offset) field objects, with array indices collapsed for field-insensitive updates;

  • field-offset-aware aggregate global initializers and memcpy/memmove;

  • singleton-object strong updates and conservative weak updates;

  • Tarjan SCC decomposition with SCC-local fixed points and successor requeueing;

  • auxiliary-PTA call-graph initialization plus on-the-fly indirect-call connection followed by SCC reconstruction;

  • selectable mutable and hash-consed points-to set storage.

Location

  • include/Alias/InclusionBased/FlowSensitive/Sparse/FlowSensitivePTA.h

  • include/Alias/InclusionBased/FlowSensitive/Versioned/VersionedFlowSensitivePTA.h

  • include/Alias/InclusionBased/FlowSensitive/ValueFlow/ValueFlowPTA.h

  • include/Alias/InclusionBased/FlowSensitive/ValueFlow/ValueFlowGraph.h

  • lib/Alias/InclusionBased/FlowSensitive/

Headers and implementations are grouped into matching Sparse/, Versioned/, and ValueFlow/ subdirectories. The value-flow graph belongs to the direct value-flow variant. All variants are built into the FlowSensitivePTA library.

Components

The module contains three flow-sensitive analyses. The first two are Lotus-native migrations of the corresponding SVF pipelines:

  1. FlowSensitivePTA implements the default exhaustive fspta analysis. It is the thread-independent sparse solver described above.

  2. VersionedFlowSensitivePTA implements the vfspta analysis. Memory facts are keyed by (abstract object, meld version) rather than by (SVFG location, abstract object) as in the conventional solver. It adds object prelabeling and version-keyed consume/yield bookkeeping so that strong and weak updates, statement-level reliance, and on-the-fly delta-edge updates all operate on versioned memory state instead of on the whole object. lib/Alias/InclusionBased/FlowSensitive/README.md lists the remaining mechanisms.

  3. ValueFlowPTA implements the vfpta analysis described in Value-Flow-Based Pointer Analysis. It constructs a field-insensitive value-flow graph directly from LLVM IR and discovers indirect flows in object escape order.

Inputs

The fspta and vfspta solvers operate on the Lotus SVFG built from an ICFG. The driver builds the ICFG with ICFGBuilder and the SVFG with SVFGBuilder, enabling MemorySSA construction and a selectable memory-region partition strategy. Indirect callees are connected from flow-sensitive function-pointer results, bounded by the auxiliary analysis. The versioned driver defaults to auxiliary points-to prelabels; --vfspta-prelabel=builder selects region seeds.

The vfpta solver consumes an LLVM module directly. It builds a separate control graph and value-flow graph, so --dump-svfg and --print-memory do not apply to that mode.

The concurrency layer does not duplicate this solver. FSMPTA runs it over an SVFG augmented with fork/join and ThreadMHPIndirectVF edges, and MSli supplies an optional filtered solve graph.

Usage

The lotus-alias-fspta driver runs either solver on an LLVM bitcode module:

./build/bin/lotus-alias-fspta input.bc
./build/bin/lotus-alias-fspta input.bc --analysis=vfspta --print-pts
./build/bin/lotus-alias-fspta input.bc --analysis=vfpta --print-pts
./build/bin/lotus-alias-fspta input.bc --points-to-sets=hash-consed --dump-stats
./build/bin/lotus-alias-fspta input.bc --dump-svfg=fspta.dot --print-memory

Key options:

  • --analysis=fspta|vfspta|vfpta – Select the conventional sparse flow-sensitive solver (default), object-versioned solver, or direct value-flow solver.

  • --parallel --threads=N – Evaluate fspta transfers concurrently with validated snapshots and reference-order retirement. Zero workers selects hardware concurrency; the worker count includes the calling thread.

  • --verify-parallel – Compare all public pointer and memory queries with sequential solving on the final graph; exit with status 3 on a mismatch.

  • --parallel-block-size=N – Transfers per speculative worker block (default 8). One disables local effect forwarding.

  • --parallel-memo=false and --parallel-share-sets=false – Disable certified unchanged-effect reuse and immutable set sharing for experiments.

  • --points-to-sets=mutable|hash-consed – Points-to set backend for fspta: mutable ordered sets (default) or interned immutable sets with operation caching.

  • --memory-partition=distinct|intra-disjoint|inter-disjoint – MemorySSA region partition strategy for fspta and vfspta (default inter-disjoint).

  • --print-pts – Print top-level points-to results.

  • --print-memory – Print non-empty sparse memory facts (fspta and vfspta only).

  • --dump-stats – Print solver statistics (default on).

  • --dump-svfg=<file> – Write the initialized SVFG as a DOT file (fspta and vfspta only).

  • --validate-annotations – Validate __aser_alias__/__aser_no_alias__ calls against the analysis result.

See also Alias Analysis Tools for the tool reference.