rapx/graphs/
scc.rs

1//! Shared strongly-connected-component utilities.
2//!
3//! This module provides the small Tarjan SCC abstraction used by RAPx 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 crate::compat::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    /// Legacy alias for `from` used by existing analyses.
15    pub exit: usize,
16    /// Source node inside the SCC body.
17    pub from: usize,
18    /// Destination node outside the SCC body.
19    pub to: usize,
20}
21
22impl SccExit {
23    /// Create an SCC exit edge from `from` to `to`.
24    pub fn new(from: usize, to: usize) -> Self {
25        SccExit {
26            exit: from,
27            from,
28            to,
29        }
30    }
31}
32
33/// Per-header SCC metadata used by loop-aware analyses.
34#[derive(Debug, Clone)]
35pub struct SccInfo {
36    /// SCC entry / representative block.
37    pub enter: usize,
38    /// SCC member set excluding `enter`.
39    pub nodes: FxHashSet<usize>,
40    /// Edges leaving the SCC.
41    pub exits: FxHashSet<SccExit>,
42    /// Edges inside the SCC region that go back to an earlier block or the representative.
43    pub backedges: Vec<(usize, usize)>,
44    /// Representative nodes of nested child SCCs.
45    pub child_sccs: Vec<usize>,
46}
47
48impl SccInfo {
49    /// Create empty SCC metadata for `enter`.
50    pub fn new(enter: usize) -> Self {
51        SccInfo {
52            enter,
53            nodes: FxHashSet::default(),
54            exits: FxHashSet::default(),
55            backedges: Vec::new(),
56            child_sccs: Vec::new(),
57        }
58    }
59
60    /// Returns `true` when this SCC contains only its representative and has no self-loop.
61    pub fn is_trivial(&self) -> bool {
62        self.nodes.is_empty() && self.backedges.is_empty()
63    }
64
65    /// Compatibility accessor for older callers.
66    pub fn enter(&self) -> usize {
67        self.enter
68    }
69}
70
71/// Tarjan SCC callback trait.
72pub trait Scc {
73    /// Run SCC discovery from CFG entry block 0.
74    fn find_scc(&mut self) {
75        if self.get_size() == 0 {
76            return;
77        }
78        self.find_scc_from(0);
79    }
80
81    /// Run SCC discovery from a specific start node.
82    fn find_scc_from(&mut self, start: usize) {
83        if start >= self.get_size() {
84            return;
85        }
86        let mut stack = Vec::new();
87        let mut instack = FxHashSet::<usize>::default();
88        let mut dfn = vec![0; self.get_size()];
89        let mut low = vec![0; self.get_size()];
90        let mut time = 1;
91        self.tarjan(
92            start,
93            &mut stack,
94            &mut instack,
95            &mut dfn,
96            &mut low,
97            &mut time,
98        );
99    }
100
101    /// Callback invoked for each discovered SCC.
102    fn on_scc_found(&mut self, root: usize, scc_components: &[usize]);
103
104    /// Return outgoing successors of `root`.
105    fn get_next(&mut self, root: usize) -> FxHashSet<usize>;
106
107    /// Return the number of graph nodes.
108    fn get_size(&mut self) -> usize;
109
110    /// Recursive Tarjan traversal.
111    fn tarjan(
112        &mut self,
113        index: usize,
114        stack: &mut Vec<usize>,
115        instack: &mut FxHashSet<usize>,
116        dfn: &mut Vec<usize>,
117        low: &mut Vec<usize>,
118        time: &mut usize,
119    ) {
120        dfn[index] = *time;
121        low[index] = *time;
122        *time += 1;
123        stack.push(index);
124        instack.insert(index);
125
126        let size = self.get_size();
127        let nexts = self.get_next(index);
128        for next in nexts {
129            if next >= size {
130                continue;
131            }
132            if dfn[next] == 0 {
133                self.tarjan(next, stack, instack, dfn, low, time);
134                low[index] = cmp::min(low[index], low[next]);
135            } else if instack.contains(&next) {
136                low[index] = cmp::min(low[index], dfn[next]);
137            }
138        }
139
140        if dfn[index] == low[index] {
141            let mut component = vec![index];
142            while let Some(top) = stack.pop() {
143                instack.remove(&top);
144                if top == index {
145                    break;
146                }
147                component.push(top);
148            }
149            self.on_scc_found(index, &component);
150        }
151    }
152}
rapx/graphs/scc.rs

rapx/graphs/
scc.rs
