rapx/utils/
scc.rs

1//! Shared strongly-connected-component utilities.
2//!
3//! This module provides the small Tarjan SCC abstraction used by RAP analyses
4//! and by the verification path extractor.  The trait is intentionally graph
5//! agnostic: clients provide successor queries and receive each discovered SCC
6//! through `on_scc_found`.
7
8use rustc_data_structures::fx::FxHashSet;
9use std::cmp;
10
11/// An outgoing edge from an SCC body to a block outside the SCC.
12#[derive(Debug, Clone, Eq, Hash, PartialEq)]
13pub struct SccExit {
14    pub exit: usize,
15    pub to: usize,
16}
17
18impl SccExit {
19    /// Create an SCC exit edge from `exit` to `to`.
20    pub fn new(exit: usize, to: usize) -> Self {
21        SccExit { exit, to }
22    }
23}
24
25/// Per-header SCC metadata used by loop-aware analyses.
26#[derive(Debug, Clone)]
27pub struct SccInfo {
28    /// Representative entry block of the SCC.
29    pub enter: usize,
30    /// Other blocks in the SCC, excluding `enter`.
31    pub nodes: FxHashSet<usize>,
32    /// Edges leaving the SCC.
33    pub exits: FxHashSet<SccExit>,
34    /// Blocks with back edges to the SCC representative.
35    pub backnodes: FxHashSet<usize>,
36}
37
38impl SccInfo {
39    /// Create empty SCC metadata for `enter`.
40    pub fn new(enter: usize) -> Self {
41        SccInfo {
42            enter,
43            nodes: FxHashSet::default(),
44            exits: FxHashSet::default(),
45            backnodes: FxHashSet::default(),
46        }
47    }
48}
49
50/// Tarjan SCC callback trait.
51pub trait Scc {
52    /// Run SCC discovery from CFG entry block 0.
53    fn find_scc(&mut self) {
54        if self.get_size() == 0 {
55            return;
56        }
57        self.find_scc_from(0);
58    }
59
60    /// Run SCC discovery from a specific start node.
61    fn find_scc_from(&mut self, start: usize) {
62        if start >= self.get_size() {
63            return;
64        }
65        let mut stack = Vec::new();
66        let mut instack = FxHashSet::<usize>::default();
67        let mut dfn = vec![0; self.get_size()];
68        let mut low = vec![0; self.get_size()];
69        let mut time = 1;
70        self.tarjan(
71            start,
72            &mut stack,
73            &mut instack,
74            &mut dfn,
75            &mut low,
76            &mut time,
77        );
78    }
79
80    /// Callback invoked for each discovered SCC.
81    fn on_scc_found(&mut self, root: usize, scc_components: &[usize]);
82
83    /// Return outgoing successors of `root`.
84    fn get_next(&mut self, root: usize) -> FxHashSet<usize>;
85
86    /// Return the number of graph nodes.
87    fn get_size(&mut self) -> usize;
88
89    /// Recursive Tarjan traversal.
90    fn tarjan(
91        &mut self,
92        index: usize,
93        stack: &mut Vec<usize>,
94        instack: &mut FxHashSet<usize>,
95        dfn: &mut Vec<usize>,
96        low: &mut Vec<usize>,
97        time: &mut usize,
98    ) {
99        dfn[index] = *time;
100        low[index] = *time;
101        *time += 1;
102        stack.push(index);
103        instack.insert(index);
104
105        let size = self.get_size();
106        let nexts = self.get_next(index);
107        for next in nexts {
108            if next >= size {
109                continue;
110            }
111            if dfn[next] == 0 {
112                self.tarjan(next, stack, instack, dfn, low, time);
113                low[index] = cmp::min(low[index], low[next]);
114            } else if instack.contains(&next) {
115                low[index] = cmp::min(low[index], dfn[next]);
116            }
117        }
118
119        if dfn[index] == low[index] {
120            let mut component = vec![index];
121            while let Some(top) = stack.pop() {
122                instack.remove(&top);
123                if top == index {
124                    break;
125                }
126                component.push(top);
127            }
128            self.on_scc_found(index, &component);
129        }
130    }
131}
132
133/// Tree representation for nested SCC metadata.
134#[derive(Debug)]
135pub struct SccTree {
136    pub scc: SccInfo,
137    pub children: Vec<SccTree>,
138}