Chapter 5.1. Path Analysis

Path analysis extracts finite, acyclic execution paths from a function's control-flow graph (CFG). It is a foundational module — the alias analysis, SafeDrop dangling pointer detection, range analysis, and the verification pipeline all depend on the path enumeration and reachability checking infrastructure provided by this module. The implementation lives at rapx/src/analysis/path_analysis/.

5.1.1 Motivation: Meet-Over-Paths Analysis

Traditional dataflow analysis frameworks typically use chaotic iteration — a MOP (Merge Over Paths) approach that iteratively propagates abstract states across all CFG edges until convergence. For languages with simple branch conditions (e.g., integer comparisons), this works well because the state space is compact and every edge is reachable under some input.

Rust presents a fundamentally different challenge: enum types produce correlated branch conditions that make many structurally possible paths mutually exclusive. Consider a function that pattern-matches the same Option<T> or Result<T,E> twice:

#![allow(unused)]
fn main() {
fn example(x: Option<i32>) -> i32 {
    let a = match x {
        Some(_) => 1,
        None => -1,
    };
    match x {
        Some(_) => a + 1,
        None => a - 1,
    }
}
}

Structurally, the CFG has 2 × 2 = 4 paths through the two match statements. But only 2 are actually reachable: if x was Some at the first match, it must also be Some at the second. The possible return values are 1 + 1 = 2 and -1 - 1 = -2. A chaotic-iteration analysis treats all edges as independent and would merge abstract states from all four routes at every join point, losing the correlation that both match statements depend on the same x. This over-approximation produces spurious state combinations — for instance, the crossed paths would suggest return values of 1 - 1 = 0 and -1 + 1 = 0, making 0 a false positive that compounds with each additional match or if let in the function.

Path analysis addresses this by explicitly enumerating CFG paths and then filtering them with discriminant-constraint checking. Each surviving path carries a consistent set of branch decisions, and downstream analyses process each path independently without merging incompatible states. This is the essence of the meet-over-paths approach: the meet (merge) operation is applied over a set of validated paths rather than over all structurally possible edges.

5.1.2 Path Extraction

Given a MIR function body, the path extraction module answers: what are all the structurally possible CFG paths from function entry to each exit point? The key challenge is loops: each strongly connected component (SCC) in the CFG introduces cyclic back-edges that make a naive enumeration unbounded. RAPx solves this by decomposing SCCs into a hierarchical tree (Section 5.1.2.1) and applying controlled unrolling (Section 5.1.2.2). Structurally valid but semantically impossible paths are then filtered out through discriminant tracking, constant propagation, and SCC context deduplication (Section 5.1.2.3).

5.1.2.1 Natural Loops and SCC Trees

The key insight enabling finite path enumeration is that every loop in Rust MIR is a natural loop. A natural loop has a single dominator (entry block) through which all paths into the loop must pass. This property enables constructing a hierarchical SCC tree:

1. SCC Detection: The CFG is decomposed into strongly connected components (SCCs). Each SCC corresponds to a loop region.
2. Dominator Identification: For each SCC, the block that dominates all SCC members is the loop's entry.
3. SCC Tree Construction: Nested SCCs form a tree — the outermost SCC is the root, children are nested sub-SCCs, and further nesting continues recursively.

         ┌──────────────────────────────────┐
         │  Outer SCC (root)                │
         │  dominator: bb1                  │
         │  ┌──────────────────────────┐    │
         │  │ Inner SCC A (child)      │    │
         │  │ dominator: bb7           │    │
         │  └──────────────────────────┘    │
         │  ┌──────────────────────────┐    │
         │  │ Inner SCC B (child)      │    │
         │  │ dominator: bb12          │    │
         │  └──────────────────────────┘    │
         └──────────────────────────────────┘

The SCC tree enables top-down recursive unfolding: starting from the outermost SCC, the analysis descends into child SCCs and splices their enumerated internal paths as atomic segments into parent paths. This top-down approach also propagates accumulated path constraints from outer contexts into inner SCCs, so inner path enumeration only explores paths consistent with the outer context.

5.1.2.2 Controlled Loop Unrolling

To keep enumeration finite, the check_postfix_segment mechanism tracks path segments between successive visits to the same SCC dominator:

• A postfix segment is the block sequence from one visit to the SCC dominator until the next visit to that same dominator.
• Each distinct postfix segment is counted. The first occurrence is always allowed; subsequent occurrences are limited to postfix_repeat times. Beyond that, the branch is pruned.
• postfix_repeat = 0 (default): each distinct segment appears at most once (the initial occurrence), producing the minimum set of structurally distinct paths.
• postfix_repeat = N: allows N extra repetitions of the same segment, useful for analyses that need multi-iteration loop coverage.

A segment is only worth further exploration if its most recent traversal introduces at least one previously unvisited node. Traversals that merely repeat an already-seen sequence without new blocks are pruned immediately.

5.1.2.3 Pruning Infeasible Paths

Structural enumeration produces many paths that are semantically impossible — for example, taking the Some branch after having already taken the None branch on the same Option. RAPx employs three complementary pruning layers to filter out infeasible paths:

1. Discriminant-based filtering (check_transition): As the DFS traverses CFG edges, each transition through a SwitchInt terminator records the discriminant's concrete value in a constraint map. When the same discriminant is tested again later in the path, the existing constraint is checked — any transition that contradicts the known value is immediately pruned. This handles correlated match/if let branches on enum types and immutable booleans without requiring full SMT solving.

2. Constant propagation: Each block's BlockConstantInfo records which locals received constant assignments (from const rvalues or ADT constructors). As constraints flow through check_transition, copy chains are forwarded and unknown assignments invalidate relevant entries. This extends discriminant tracking to cases where the value propagates through temporary locals and copy operations.

3. SCC context deduplication (visited_sccs): When a nested SCC is reached via multiple parent paths, re-enumerating its internal sub-paths is redundant if the accumulated constraint state is identical. constraint_context hashes all (local → constant_value) bindings accumulated along the path prefix into a ConstraintHash. Before expanding a child SCC, dfs_scc_tree checks whether this hash has been seen before — if so, the expansion is skipped, avoiding combinatorial blowup. The hash naturally distinguishes genuinely different contexts (e.g., inner loop executed vs. skipped) while collapsing identical ones.

Together, these three layers dramatically reduce the number of paths that survive into the PathTree. The first two layers eliminate provably infeasible transitions; the third trades soundness for scalability by assuming that identical constraint fingerprints imply identical sub-path behavior. Example 2 (Section 5.1.3.2) demonstrates discriminant + constant filtering, while Example 3 (Section 5.1.3.3) illustrates the trade-off introduced by SCC context deduplication.

5.1.3 Examples

5.1.3.1 Example 1: Correlated Enum Branches (path_1)

Recall the example(x: Option<i32>) function from Section 5.1.1. Its MIR (cargo rapx analyze mir) contains two SwitchInt terminators on the same discriminant _1:

bb0:  _3 = discriminant(_1); switchInt(_3) -> [0: bb2, 1: bb3, otherwise: bb1]
bb1:  unreachable
bb2:  _2 = const -1_i32; goto bb4          // a = -1 (None)
bb3:  _2 = const 1_i32;  goto bb4          // a = 1  (Some)
bb4:  _4 = discriminant(_1); switchInt(_4) -> [0: bb5, 1: bb6, otherwise: bb1]
bb5:  _0 = Sub(_2, 1); goto bb9            // return a - 1
bb6:  _0 = Add(_2, 1); goto bb9            // return a + 1
bb9:  return

No loops — the CFG is a DAG. Path analysis (cargo rapx analyze paths) produces 2 paths:

Function: "example":
  Path [0, 3, 4, 6, 7, 9]    // Some → Some, returns 2
  Path [0, 2, 4, 5, 8, 9]    // None → None, returns -2

Structurally the two SwitchInt terminators create 2 × 2 = 4 combinations. Incremental constraint filtering via check_transition (see Section 5.1.2.3) prunes the crossed branches (None → Some and Some → None), leaving only the 2 consistent paths.

5.1.3.2 Example 2: Nested SCCs with Constraint Filtering (path_5)

The test at rapx/tests/analyze/path_5/src/lib.rs has two nested loops with boolean guards that the constraint system can track:

#![allow(unused)]
fn main() {
fn read2(x: bool) -> Option<u32> {
    let mut outer_retry = true;
    loop {
        let mut inner_retry = true;
        loop {
            if x { return Some(42); }          // bb2 → bb3 (exit via return)
            else if inner_retry { inner_retry = false; continue; }  // bb4 → bb5 → bb2
            else { break; }                    // bb4 → bb6 (break inner loop)
        }
        if outer_retry { outer_retry = false; continue; }  // bb6 → bb7 → bb1
        return None;                           // bb6 → bb8 → bb9 (exit via return)
    }
}
}

The MIR has 10 basic blocks:

bb0: _2 = const true;       goto bb1   // outer_retry = true
bb1: _3 = const true;       goto bb2   // inner_retry = true
bb2: switchInt(_1) → [0: bb4, otherwise: bb3]   // test x
bb3: return Some(42);       goto bb9   // → exit
bb4: switchInt(copy _3) → [0: bb6, otherwise: bb5]  // test inner_retry
bb5: _3 = const false;      goto bb2   // inner_retry = false; continue inner
bb6: switchInt(copy _2) → [0: bb8, otherwise: bb7]  // test outer_retry
bb7: _2 = const false;      goto bb1   // outer_retry = false; continue outer
bb8: return None;           goto bb9   // → exit
bb9: return

SCC structure:

• Inner SCC: {bb2, bb4, bb5}, dominator bb2, back edge bb5 → bb2. Exit: bb2 → bb3 (x = true), bb4 → bb6 (inner break).
• Outer SCC: {bb1, bb2, bb4, bb5, bb6, bb7}, dominator bb1, back edge bb7 → bb1. bb2 is a child SCC of the outer SCC.

Inner SCC Structural Paths

At postfix_repeat = 0, the inner SCC DFS from bb2 enumerates four structurally distinct paths:

The postfix segment [4, 5] appears once in C and D. A second occurrence would repeat the segment and is pruned by check_postfix_segment, so no paths with two inner retries (e.g., 2 → 4 → 5 → 2 → 4 → 5 → 2) are generated.

Combining Across Outer Iterations

The outer SCC DFS splices inner SCC paths as atomic building blocks at each visit to bb2. Each outer iteration picks one inner path (A, B, C, or D), then proceeds through bb6:

• If the inner path exits to bb3 (A or C), the path goes to bb9 via a return — this ends the function.
• If the inner path exits to bb6 (B or D), the path reaches bb6. At bb6, outer_retry is tested: switchInt(copy _2) → [0: bb8, otherwise: bb7].
  • If outer_retry = true (otherwise branch): → bb7 (set outer_retry = false) → bb1 (continue outer loop). The outer postfix segment from bb1 back to bb1 is either [2, 4, 6, 7] (B path) or [2, 4, 5, 2, 4, 6, 7] (D path).
  • If outer_retry = false (0 branch): → bb8 → bb9 (return None). The outer loop ends.

At postfix_repeat = 0, each distinct outer postfix segment appears at most once, so at most three outer iterations are possible (initial entry + two distinct returns to bb1). Structurally, the full CFG paths are all ordered selections of inner SCC paths, terminated by a path whose exit reaches bb9 (A or C for Some, B or D for None). Representative combinations:

Reachability Filtering

Discriminant-based filtering combined with constant propagation (see Section 5.1.2.3) eliminates all but two of the 20 structural paths. The filtering exploits that x is an immutable boolean (SwitchInt discriminant), and inner_retry/outer_retry are assigned constants at well-defined points:

Path [0, 1, 2, 3, 9]                              // x = true
Path [0, 1, 2, 4, 5, 2, 4, 6, 7, 1, 2, 4, 5, 2, 4, 6, 8, 9]  // x = false

5.1.3.3 Example 3: Nested SCCs with Structural Pruning (path_7)

For contrast, this example has two nested loops where the constraint system cannot prune structurally possible but semantically impossible paths. The test lives at rapx/tests/analyze/path_7/src/lib.rs:

#![allow(unused)]
fn main() {
fn walk(rows: i32, cols: i32) -> i32 {
    let mut total = 0;
    let mut r = 0;
    loop {
        if r >= rows { break; }
        let mut c = 0;
        loop {
            if c >= cols { break; }
            total += 1;
            c += 1;
        }
        r += 1;
    }
    total
}
}

The CFG has two back edges, bb8 → bb4 and bb9 → bb1, creating two nested SCCs:

Each SCC can produce two configurations at repeat = 0:

• Inner SCC: skip 4 → 5 (postfix: none), or one body iteration 4 → 6 → 7 → 8 → 4 (postfix: [6, 7, 8]), then exits via 5. A second iteration would repeat [6, 7, 8], which is pruned.
• Outer SCC: the postfix segment between successive visits to 1 is either [3, 4, 5, 9] (inner skip) or [3, 4, 6, 7, 8, 4, 5, 9] (inner body).

Structurally, combining these gives 5 possible paths:

Paths 1–4 all appear in the output; Path 5 never does. The divergence is driven by the visited_sccs cache (see Section 5.1.2.3). Here is what happens during DFS enumeration:

• Path 4 (body then skip): The DFS first reaches bb4 from bb3, enters the inner SCC, and explores the body child (bb4 → bb6 → bb7 → bb8 → bb4 → bb5). Along this path, c and total are mutated — their constant-tracking state is invalidated. The outer SCC loops back to bb1 → bb3 → bb4. At this second visit, the constraint hash differs from the first entry because the body path altered local state. visited_sccs misses, the inner SCC is re-expanded, and this time the skip child (bb4 → bb5) is spliced in, producing body-then-skip.

• Path 5 (skip then body): If the DFS first takes the skip child (bb4 → bb5), no locals are mutated — c remains the constant 0 assigned at bb3. The outer SCC loops back to bb4 with an identical constraint hash. visited_sccs hits and blocks re-expansion, so the body child is never spliced in — skip-then-body is suppressed.

5.1.4 Usage

CLI:

# Default: postfix_repeat = 0
cargo rapx analyze paths

# With controlled SCC segment repetition
cargo rapx analyze paths --postfix-repeat 1

In code:

#![allow(unused)]
fn main() {
use analysis::path_analysis::default::PathAnalyzer;

let mut analyzer = PathAnalyzer::new(tcx, false);  // false = no debug output
analyzer.analyze_all();                        // postfix_repeat = 0
// or: analyzer.analyze_all_repeat(1);         // postfix_repeat = 1
let all_paths = analyzer.get_all_paths();      // FxHashMap<DefId, PathTree>
let fn_paths = analyzer.analyze(def_id);       // single function
}

Paths are stored in a PathTree (prefix-tree), keyed by DefId. See the source for the full API — PathGraph for CFG+SCC+constraint checking, PathEnumerator for DFS enumeration with SCC caching.

5.1.5 Relationship to Other Modules

• Alias Analysis: The MOP-based AliasGraph wraps a PathGraph for path-sensitive alias checking. SCC decomposition, top-down traversal, and incremental constraint filtering are all shared.
• SafeDrop: Reuses PathGraph for path-sensitive dangling pointer detection with per-block alias facts tracked along enumerated paths.
• Verification: PathExtractor wraps PathGraph and uses PathEnumerator to find paths reaching specific unsafe callsites. The postfix_repeat parameter controls SCC postfix repetition.
• Range Analysis: PathAnalyzer::analyze(def_id) is used to obtain per-function PathTrees for path-constraint extraction in RangeAnalyzer.