smt_scope/analysis/graph/
mod.rs

1#[cfg(feature = "mem_dbg")]
2use mem_dbg::{MemDbg, MemSize};
3use subgraph::Subgraphs;
4
5use crate::{Result, Z3Parser};
6
7use self::{analysis::Analysis, raw::RawInstGraph, visible::VisibleInstGraph};
8
9pub mod analysis;
10pub mod disable;
11pub mod hide;
12pub mod raw;
13pub mod subgraph;
14pub mod visible;
15
16pub use raw::{RawEdgeIndex, RawNodeIndex};
17pub use visible::{VisibleEdgeIndex, VisibleNodeIndex};
18
19const DEFAULT_N: usize = 10000;
20
21#[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
22#[derive(Debug)]
23pub struct InstGraph {
24    pub raw: RawInstGraph,
25    pub subgraphs: Subgraphs,
26    pub analysis: Analysis,
27}
28
29impl InstGraph {
30    pub fn new(parser: &Z3Parser) -> Result<Self> {
31        Self::new_with_analysis(parser, DEFAULT_N)
32    }
33    pub fn new_lite(parser: &Z3Parser) -> Result<Self> {
34        Self::new_with_analysis(parser, 0)
35    }
36
37    fn new_with_analysis(parser: &Z3Parser, n: usize) -> Result<Self> {
38        let mut raw = RawInstGraph::new(parser)?;
39        let subgraphs = raw.partition()?;
40        let analysis = Analysis::new(subgraphs.in_subgraphs())?;
41        let mut self_ = InstGraph {
42            raw,
43            subgraphs,
44            analysis,
45        };
46        self_.initialise_first(parser, n);
47        Ok(self_)
48    }
49
50    pub fn visible_unchanged(&self, old: &VisibleInstGraph) -> bool {
51        self.raw.stats.generation == old.generation
52    }
53}
54
55#[macro_export]
56macro_rules! graph_idx {
57    ($mod_name:ident, $node:ident, $edge:ident, $inner:ident) => {
58        mod $mod_name {
59            #[cfg(feature = "mem_dbg")]
60            use mem_dbg::*;
61            use petgraph::graph::IndexType;
62
63            use $crate::idx;
64
65            idx!($inner, "ix{}");
66            impl Default for $inner {
67                fn default() -> Self {
68                    Self::from(0)
69                }
70            }
71            unsafe impl IndexType for $inner {
72                fn new(x: usize) -> Self {
73                    Self::from(x)
74                }
75                fn index(&self) -> usize {
76                    usize::from(*self)
77                }
78                fn max() -> Self {
79                    Self::MAX
80                }
81            }
82            #[derive(Debug, Copy, Clone, Default, PartialEq, PartialOrd, Eq, Ord, Hash)]
83            pub struct $node(pub petgraph::graph::NodeIndex<$inner>);
84            #[derive(Debug, Copy, Clone, Default, PartialEq, PartialOrd, Eq, Ord, Hash)]
85            pub struct $edge(pub petgraph::graph::EdgeIndex<$inner>);
86
87            #[cfg(feature = "mem_dbg")]
88            impl MemDbgImpl for $node {}
89            #[cfg(feature = "mem_dbg")]
90            impl MemSize for $node {
91                fn mem_size(&self, _flags: SizeFlags) -> usize {
92                    std::mem::size_of::<Self>()
93                }
94            }
95            #[cfg(feature = "mem_dbg")]
96            impl CopyType for $node {
97                type Copy = True;
98            }
99            #[cfg(feature = "mem_dbg")]
100            impl MemDbgImpl for $edge {}
101            #[cfg(feature = "mem_dbg")]
102            impl MemSize for $edge {
103                fn mem_size(&self, _flags: SizeFlags) -> usize {
104                    std::mem::size_of::<Self>()
105                }
106            }
107            #[cfg(feature = "mem_dbg")]
108            impl CopyType for $edge {
109                type Copy = True;
110            }
111
112            impl From<usize> for $node {
113                fn from(x: usize) -> Self {
114                    Self(petgraph::graph::NodeIndex::new(x))
115                }
116            }
117            impl From<$node> for usize {
118                fn from(x: $node) -> Self {
119                    x.0.index()
120                }
121            }
122        }
123        pub use $mod_name::{$edge, $inner, $node};
124    };
125}
smt_scope/analysis/graph/mod.rs

smt_scope/analysis/graph/
mod.rs
