rapx/verify/
path_extractor.rs

1//! Path extraction for verification targets.
2//!
3//! This module builds finite, acyclic paths from a function CFG to each unsafe checkpoint
4//! so that the verifier can reason about pointer properties along concrete execution
5//! traces without unrolling loops or recursive cycles.
6//!
7//! # Path reachability
8//!
9//! Each path is validated against a `PathGraph` (an SCC-aware path enumeration
10//! structure) to ensure the computed block sequence is actually reachable. Paths
11//! that fail this check are silently discarded.
12//!
13//! # Path limit
14//!
15//! To prevent exponential blow-up, path enumeration is capped at
16//! [`crate::limit::path_limit`] (the `--path-limit` CLI value, or
17//! [`crate::limit::PATH_LIMIT`]). Enumeration stops producing new paths once
18//! the limit is reached and the tree is marked truncated.
19
20use crate::compat::FxHashMap;
21use rustc_hir::def_id::DefId;
22use rustc_middle::{mir::BasicBlock, ty::TyCtxt};
23
24use crate::analysis::path::{
25    PathTree,
26    graph::{PathEnumerator, PathGraph},
27};
28
29use crate::helpers::mir_scan::{Checkpoint, CheckpointLocation};
30
31/// Enumerates finite, SCC-aware verification paths from the function entry
32/// to each unsafe checkpoint in a single function body.
33///
34/// `PathExtractor` is the **first stage** of the verification pipeline.  It
35/// takes a function's MIR control-flow graph and a list of unsafe checkpoints,
36/// then produces a [`CheckpointPaths`] value that maps every checkpoint to a set
37/// of acyclic block-level paths reaching it.
38///
39/// # Pipeline role
40///
41/// ```text
42/// PathExtractor ──► BackwardSlicer ──► ForwardVerifier ──► SmtChecker
43///    (paths)          (relevant items)    (abstract facts)    (satisfiability)
44/// ```
45///
46/// The paths produced here determine *which* MIR instructions the slicer
47/// will inspect and in what order, so path quality directly affects
48/// verification precision.
49///
50/// # SCC handling
51///
52/// Loops (strongly connected components) are detected and collapsed by
53/// [`PathGraph`].  The `allow_repeat` parameter controls how many extra
54/// iterations of each SCC postfix are appended beyond the first — useful
55/// for modeling loop-carried effects without unrolling indefinitely.
56///
57/// # Path limit
58///
59/// Whole-CFG path enumeration is capped at
60/// [`crate::limit::path_limit`] (the `--path-limit` CLI value, or
61/// [`crate::limit::PATH_LIMIT`]) to prevent exponential blow-up in
62/// functions with many branches.
63pub(crate) struct PathExtractor<'tcx> {
64    /// Compiler type context used for MIR access and name resolution.
65    tcx: TyCtxt<'tcx>,
66    /// The function whose MIR body is being analyzed.
67    def_id: DefId,
68    /// Unsafe checkpoints (call terminators, raw-ptr derefs, static mut accesses)
69    /// discovered in the function's MIR body.
70    checkpoints: Vec<Checkpoint<'tcx>>,
71    /// Number of extra SCC postfix repetitions allowed (default 0).
72    allow_repeat: usize,
73}
74
75impl<'tcx> PathExtractor<'tcx> {
76    /// Create a path extractor for `def_id` and the checkpoints found in that body.
77    ///
78    /// Path extraction (SCC detection, enumeration, filtering) is deferred
79    /// until [`run`] is called.
80    ///
81    /// `allow_repeat` controls how many times a repeated SCC postfix segment
82    /// is allowed beyond the first occurrence. Default is 0 (no extra repeats).
83    pub(crate) fn new(
84        tcx: TyCtxt<'tcx>,
85        def_id: DefId,
86        checkpoints: Vec<Checkpoint<'tcx>>,
87        allow_repeat: usize,
88    ) -> Self {
89        Self {
90            tcx,
91            def_id,
92            checkpoints,
93            allow_repeat,
94        }
95    }
96
97    /// Run path extraction, consuming the extractor.
98    ///
99    /// Returns a `Vec<CallGroup>` — one entry per unique callee DefId.
100    /// Checkpoints that target the same callee share a single `PathTree`,
101    /// avoiding redundant subtree construction.
102    pub(crate) fn run(self) -> Vec<CallGroup<'tcx>> {
103        let mut graph = PathGraph::new(self.tcx, self.def_id);
104        graph.inline_callees();
105        graph.find_scc();
106        let mut tree = {
107            let mut enumerator = PathEnumerator::new(&graph);
108            enumerator.enumerate_paths_repeat(self.allow_repeat)
109        };
110        tree.set_block_fn(
111            graph
112                .cfg
113                .blocks
114                .iter()
115                .map(|b| (b.def_id, b.local_index))
116                .collect(),
117            graph.inline_bindings.clone(),
118            graph.inline_parents.clone(),
119            graph.inlined_call_blocks.clone(),
120        );
121        group_by_callee(self.checkpoints, &tree)
122    }
123}
124
125/// Checkpoints targeting the same callee, grouped for shared path analysis.
126///
127/// One `CallGroup` is produced per unique callee `DefId` in the function.
128/// All checkpoints in the group share the same `PathTree`; individual paths
129/// are filtered by `checkpoint.block` at query time.
130pub(crate) struct CallGroup<'tcx> {
131    /// Shared full-CFG prefix tree, built once for all checkpoints in the group.
132    pub tree: PathTree,
133    /// Checkpoints that target this callee.
134    pub checkpoints: Vec<Checkpoint<'tcx>>,
135}
136
137fn group_by_callee<'tcx>(
138    checkpoints: Vec<Checkpoint<'tcx>>,
139    tree: &PathTree,
140) -> Vec<CallGroup<'tcx>> {
141    let mut groups: FxHashMap<Option<DefId>, Vec<Checkpoint<'tcx>>> = FxHashMap::default();
142    for cs in checkpoints {
143        groups.entry(cs.callee).or_default().push(cs);
144    }
145    groups
146        .into_iter()
147        .map(|(_callee, checkpoints)| CallGroup {
148            tree: tree.clone(),
149            checkpoints,
150        })
151        .collect()
152}
153
154/// One finite, acyclic execution trace from the function entry to a target
155/// checkpoint, represented as an ordered sequence of MIR basic blocks.
156///
157/// A `Path` is the core currency flowing through the verification pipeline.
158/// It is produced by [`PathExtractor`], then consumed by the
159/// [`BackwardSlicer`](super::slicer::BackwardSlicer) to determine which MIR
160/// instructions are relevant to the safety property being checked.
161///
162/// # Structure
163///
164/// Each path consists of:
165/// - **`target`** — the [`CheckpointLocation`] identifying the specific call
166///   terminator (or synthetic checkpoint) this path reaches.  Redundant
167///   with the final step but stored separately for fast lookup.
168/// - **`steps`** — an ordered list of [`PathStep`] values.  Intermediate
169///   steps are MIR basic blocks; the final step is always
170///   `PathStep::Checkpoint(target)`.  The path always starts at function
171///   entry (block `bb0`).
172///
173/// # Reachability
174///
175/// Every `Path` returned by `PathExtractor` is guaranteed to be *reachable*
176/// in the function's CFG.  Paths that cannot be validated against the
177/// SCC-aware [`PathGraph`] are silently discarded during extraction.
178///
179/// # Example (compact notation)
180///
181/// ```text
182/// bb2 -> bb3 -> bb4 -> checkpoint@bb5::unsafe_fn
183/// ```
184///
185/// In the path above, blocks 2, 3, and 4 are intermediate MIR blocks;
186/// block 5 contains the unsafecall terminator that the path targets.
187#[derive(Clone, Debug)]
188pub(crate) struct Path {
189    /// The checkpoint location (function + basic block) reached by this path.
190    pub target: CheckpointLocation,
191    /// Ordered sequence of basic blocks from function entry to `target`,
192    /// terminated by a `PathStep::Checkpoint`.
193    pub steps: Vec<PathStep>,
194}
195
196impl Path {
197    /// Render this path as a compact array of block indices.
198    pub(crate) fn describe_indices(&self) -> String {
199        let mut indices: Vec<usize> = Vec::new();
200        for step in &self.steps {
201            match step {
202                PathStep::Block(b) => indices.push(b.as_usize()),
203                PathStep::Checkpoint(l) => {
204                    let bb = l.block.as_usize();
205                    if indices.last() != Some(&bb) {
206                        indices.push(bb);
207                    }
208                }
209            }
210        }
211        format!("{:?}", indices)
212    }
213
214    /// Whether this path re-enters a block it already visited (a loop-unrolled
215    /// iteration, not a genuinely distinct step).
216    pub(crate) fn reenters(&self) -> bool {
217        let mut seen = std::collections::HashSet::new();
218        self.steps.iter().any(|s| match s {
219            PathStep::Block(b) => !seen.insert(b.as_usize()),
220            _ => false,
221        })
222    }
223
224}
225
226/// One step in a finite verification path.
227#[derive(Clone, Debug)]
228pub(crate) enum PathStep {
229    /// A normal MIR basic block.
230    Block(BasicBlock),
231    /// The target checkpoint that terminates the path.
232    Checkpoint(CheckpointLocation),
233}
rapx/verify/path_extractor.rs

rapx/verify/
path_extractor.rs
