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