Struct PathEnumerator 

pub struct PathEnumerator<'g, 'tcx> {
    graph: &'g PathGraph<'tcx>,
    scc_paths: FxHashMap<SccKey, Vec<SccPath>>,
    visited_sccs: FxHashSet<SccKey>,
}

Builds a PathTree by depth-first enumeration of whole-CFG paths.

The enumerator holds a &PathGraph (which must have find_scc() called beforehand) and two caches:

The constraint hash used by visited_sccs is a ConstraintHash: it walks the current path prefix, accumulates (local → constant_value) bindings from each block’s BlockConstantInfo, sorts them, and hashes the result. Different constraint states (e.g. a loop variable changing from true to false) produce different hashes.

1. scc_paths — maps SccKey to a list of acyclic paths through that SCC. Reused across repeated enumerations of the same function with different repeat counts.

2. visited_sccs — set of SccKey entries already explored (matched by entry + constraint, ignoring repeat). When the same SCC is reached with the same constraint state, its sub-paths are identical, so the re-entry is skipped.

Constraint-based filtering runs incrementally during DFS via PathGraph::check_transition, so only feasible paths are inserted into the resulting tree.

Fields

graph: &'g PathGraph<'tcx>

scc_paths: FxHashMap<SccKey, Vec<SccPath>>

visited_sccs: FxHashSet<SccKey>

Implementations

impl<'g, 'tcx> PathEnumerator<'g, 'tcx>

pub fn new(graph: &'g PathGraph<'tcx>) -> Self

pub fn enumerate_paths(&mut self) -> PathTree

Enumerate all whole-CFG paths, pruning infeasible transitions via incremental constraint-based filtering during DFS.

SCC regions are flattened into a bounded set of acyclic paths.

pub fn enumerate_paths_repeat(&mut self, postfix_repeat: usize) -> PathTree

Enumerate whole-CFG paths allowing each SCC postfix segment to repeat up to postfix_repeat additional times. postfix_repeat = 0 gives the same result as enumerate_paths.

pub fn find_scc_paths_repeat( &mut self, start: usize, scc: &SccInfo, postfix_repeat: usize, ) -> Vec<SccPath>

Enumerate all acyclic paths through scc starting at start, allowing each postfix segment to repeat up to postfix_repeat additional times.

Results are cached per (def_id, scc_enter, postfix_repeat).

fn dfs_scc_tree( &mut self, scc: &SccInfo, cur: usize, path: &mut Vec<usize>, segment_counts: &mut FxHashMap<Vec<usize>, usize>, postfix_repeat: usize, out: &mut Vec<SccPath>, seen_paths: &mut FxHashSet<Vec<usize>>, depth: usize, )

Recursive DFS through one level of the SCC tree.

Enumerates structurally possible paths through the SCC to exit points. No constraint tracking — check_postfix_segment prunes repeated loop-body segments purely by block-id sequence.

When postfix_repeat > 0, allows the same postfix segment to repeat up to postfix_repeat additional times beyond the first occurrence.

Child SCC paths are pre-enumerated via find_scc_paths_repeat and treated as atomic building blocks (no recursive descent into child SCC internals).

fn constraint_context(&self, path: &[usize]) -> ConstraintHash

Build a ConstraintHash from the constraint state along path.

fn collect_whole_cfg_paths( &mut self, current: usize, path: &mut Vec<usize>, tree: &mut PathTree, depth: usize, postfix_repeat: usize, constraints: &FxHashMap<usize, usize>, )

Depth-first enumeration of all CFG paths from current to a terminator.

SCC nodes are flattened via find_scc_paths_repeat; non-SCC blocks are followed one by one. No cycle detection is needed because the post-SCC CFG is a DAG. Constraints are maintained incrementally — each transition is checked via PathGraph::check_transition before recursing, and infeasible branches are pruned early.

fn sort_scc_tree(&self, scc: &SccInfo) -> SccInfo

fn record_unique_path( &self, path: &[usize], scc: &SccInfo, out: &mut Vec<SccPath>, seen_paths: &mut FxHashSet<Vec<usize>>, )

fn compute_exit_successors(&self, path: &[usize], scc: &SccInfo) -> Vec<usize>