Struct PathExtractor 

pub struct PathExtractor<'tcx> {
    tcx: TyCtxt<'tcx>,
    def_id: DefId,
    checkpoints: Vec<Checkpoint<'tcx>>,
    allow_repeat: usize,
}

Enumerates finite, SCC-aware verification paths from the function entry to each unsafe checkpoint in a single function body.

PathExtractor is the first stage of the verification pipeline. It takes a function’s MIR control-flow graph and a list of unsafe checkpoints, then produces a [CheckpointPaths] value that maps every checkpoint to a set of acyclic block-level paths reaching it.

Pipeline role

PathExtractor ──► BackwardSlicer ──► ForwardVerifier ──► SmtChecker
   (paths)          (relevant items)    (abstract facts)    (satisfiability)

The paths produced here determine which MIR instructions the slicer will inspect and in what order, so path quality directly affects verification precision.

SCC handling

Loops (strongly connected components) are detected and collapsed by PathGraph. The allow_repeat parameter controls how many extra iterations of each SCC postfix are appended beyond the first — useful for modeling loop-carried effects without unrolling indefinitely.

Path limit

Per-checkpoint path count is capped at PATH_LIMIT (1024) to prevent exponential blow-up in functions with many branches.

Fields

tcx: TyCtxt<'tcx>

Compiler type context used for MIR access and name resolution.

def_id: DefId

The function whose MIR body is being analyzed.

checkpoints: Vec<Checkpoint<'tcx>>

Unsafe checkpoints (call terminators, raw-ptr derefs, static mut accesses) discovered in the function’s MIR body.

allow_repeat: usize

Number of extra SCC postfix repetitions allowed (default 0).

Implementations

impl<'tcx> PathExtractor<'tcx>

pub fn new( tcx: TyCtxt<'tcx>, def_id: DefId, checkpoints: Vec<Checkpoint<'tcx>>, allow_repeat: usize, ) -> Self

Create a path extractor for def_id and the checkpoints found in that body.

Path extraction (SCC detection, enumeration, filtering) is deferred until [run] is called.

allow_repeat controls how many times a repeated SCC postfix segment is allowed beyond the first occurrence. Default is 0 (no extra repeats).

pub fn run(self) -> Vec<CallGroup<'tcx>>

Run path extraction, consuming the extractor.

Returns a Vec<CallGroup> — one entry per unique callee DefId. Checkpoints that target the same callee share a single PathTree, avoiding redundant subtree construction.