Strict Relations Alias Analysis — Algorithm

Overview

Strict Relations Alias Analysis (SRAA) is a pointer-alias analysis that proves pointers cannot alias by establishing strict (<, ≤) relations between symbolic numeric expressions that describe memory objects. The technique combines:

  • An SSI/e-SSA-style live-range–splitting transformation,

  • A symbolic Range Analysis pass, and

  • A constraint solver for strict inequalities.

  • Location: lib/Alias/SRAA

Highlights

  • Proves NoAlias results by reasoning about strict inequalities on pointer offsets

  • Uses InterProceduralRA to infer value ranges and propagate constraints

  • Tracks primitive layouts of aggregate types to compare sub-field accesses

Usage

Register the StrictRelations pass (-sraa) inside an LLVM pass pipeline or via the Lotus AA wrapper.

This document focuses solely on the algorithmic workflow of SRAA as implemented in the artifact.

Inputs / Outputs / Invariants

  • Inputs: LLVM IR in SSA form, size metadata for abstract memory objects, target ABI layout rules.

  • Outputs: Pairs of pointers classified as NoAlias (strictly proven) or MayAlias.

  • Invariants: symbolic expressions remain affine, constraints are monotone, and transformations preserve IR semantics.

Algorithmic Pipeline (High-Level View)

The analysis is structured as a pipeline:

  1. Live-Range Splitting (vSSA)

  2. Range Analysis (RA)

  3. Strict-Inequality Generation

  4. Constraint Propagation

  5. Alias Disambiguation

  6. (Optional) PDG node reduction

Data products exchanged between stages:

  • vSSA emits per-version def-use chains and symbolic expressions.

  • RA outputs symbolic lower/upper bounds per versioned value.

  • Inequality construction synthesizes strict constraints in canonical form.

  • The solver produces disjointness facts and contradiction reports for diagnostics.

Each stage is described in detail below.

1. vSSA / SSI Transformation

SRAA requires precise symbolic information per program point. Therefore, the implementation first transforms the IR into a variant of SSI (Sparse Static Single Information) called vSSA.

The vSSA transformation performs:

  1. Splitting at control-flow joins Insert φ-like nodes for variables whose value-flow merges.

  2. Splitting at control-flow forks Insert σ-like nodes to preserve flow sensitivity of interval constraints.

  3. Splitting at uses of pointer-index expressions Ensures every symbolic expression has a single definition site.

Formally:

For each variable x:

  • Insert φ where x_in(B1) ≠ x_in(B2)

  • Insert σ at outgoing edges when range(x) changes on different successors

  • Create a unique version x_i for each definition/merge/split

Implementation notes:

  • vSSA runs after mem2reg and before alias analysis passes that expect canonical pointers.

  • Synthetic definitions are tagged so later passes can ignore them when materializing code.

  • The transformation keeps debug metadata and dominance info in sync, ensuring downstream passes receive well-formed IR.

This results in a def-use graph suitable for sparse constraint propagation.

2. Symbolic Range Analysis

The Range Analysis pass computes symbolic ranges of the form:

x ∈ [L(x), U(x)]

where L(x), U(x) are symbolic linear expressions derived from:

  • loop induction variables

  • pointer arithmetic (GEP)

  • branch conditions

  • integer arithmetic

  • comparisons

Example symbolic constraints inferred:

i_3 = i_2 + 1 ⇒ L(i_3) = L(i_2)+1, U(i_3) = U(i_2)+1 if (i < n) ⇒ U(i) ≤ U(n)-1

Propagation strategy:

  1. Seed bounds using constants, known loop trip counts, and structure layout info.

  2. Push constraints along vSSA def-use edges in topological order.

  3. Relax bounds when a tighter symbolic expression is discovered.

  4. Iterate until no bound changes (typically a small number of rounds because the graph is sparse).

The RA solver is linear, sparse, and propagates constraints until fixed point. It records justification edges so later stages can reconstruct the proof chain that produced every bound.

3. Strict-Inequality Construction

Given pointer expressions:

p = base + offset_p q = base + offset_q

SRAA constructs strict inequalities such as:

offset_p + size_p ≤ offset_q offset_q + size_q ≤ offset_p offset_p < offset_q

These are derived from:

  • value ranges from RA

  • control-flow–guarded conditions

  • loop bounds

  • comparisons in the IR (e.g., if (i < j) introduces i < j constraint)

Each inequality is represented in canonical form:

ax + by + … < k

Canonicalization steps:

  • Normalize coefficients so gcd is 1, making syntactic deduplication easier.

  • Replace non-strict constraints generated by RA (≤) with equivalent strict forms when object sizes allow.

  • Attach provenance (IR instruction, dominance frontier) for auditing and debugging.

The system contains only affine expressions.

4. Constraint Propagation Solver

SRAA maintains a strict-inequality constraint graph:

  • Nodes: symbolic variables (offsets, indices, derived expressions)

  • Edges: inequalities of form x < y + c

Algorithm:

  1. Initialize graph with inequalities from Range Analysis.

  2. For every edge (x → y) labeled +c, propagate: L(y) ≥ L(x) + c and U(x) ≤ U(y) - c

  3. When two expressions conflict: If offset_p + size_p ≤ offset_q is provably true, register a disjointness fact.

  4. Detect contradictory cycles (negative-weight cycles in the negated system) and mark the originating constraints as infeasible for diagnostics.

  5. Continue propagation until a fixed point.

Practical considerations:

  • The solver caches shortest paths for repeated queries in interprocedural contexts.

  • Worklists are partitioned per strongly connected component to reduce redundant relaxations.

This is a Bellman–Ford–like relaxation over a directed constraint graph, but runs sparsely due to vSSA def-use structure.

5. Alias Disambiguation (Final Decision)

For two memory objects with computed offsets:

Let:

  • P ranges over [Lp, Up]

  • Q ranges over [Lq, Uq]

  • And their sizes: size(P) and size(Q)

SRAA proves NoAlias if any of the following hold:

  1. ::

    Up + size(P) ≤ Lq

  2. ::

    Uq + size(Q) ≤ Lp

  3. Strict relation holds::

    Up < Lq OR Uq < Lp

Example:

  • p = base + i * 4, 0 ≤ i < n

  • q = base + (n + j) * 4, 0 ≤ j < m

  • size(p) = size(q) = 4

RA yields Up = 4(n-1) and Lq = 4n. Therefore Up + size(p) = 4n ≤ Lq, and SRAA reports NoAlias.

If none of the strict inequalities are provable, SRAA returns MayAlias.

Notes:

  • Proofs use purely symbolic comparisons.

  • No heap-shape or points-to analysis is required.

  • SRAA is context-insensitive but interprocedural: formal-actual parameters are connected via synthetic φ-like merges.

6. PDG Memory-Node Reduction (Applicability)

For dependence-graph construction (as used in the paper’s applicability study):

If two memory objects are proven disjoint, the PDG pass merges or eliminates corresponding memory nodes.

Optimization details:

  • Proven NoAlias edges are annotated so later passes can skip building memory dependences entirely.

  • When only one direction is proven (e.g., p before q), the PDG records a directed reduction, shrinking the transitive closure.

The result is fewer nodes and fewer dependence edges, which improves precision in downstream analyses.

Summary of Properties

  • Sparse due to vSSA/SSI transformation.

  • Linear constraint solving on affine strict inequalities.

  • Provably sound for proving disjointness (NoAlias).

  • Flow-sensitive but context-insensitive.

  • Explainable: every NoAlias result carries a justification chain for debugging.

  • Produces strict (<, ≤) disjointness proofs, not approximate heuristics.

  • Complements and composes with LLVM’s baseline alias analyses.

End of document.