Fix high degree filter and improve reconnect

viperproject · May 27, 2024 · 107feda · 107feda
1 parent 3537d05
commit 107feda
Show file tree

Hide file tree

Showing 5 changed files with 126 additions and 87 deletions.
diff --git a/axiom-profiler-GUI/src/filters/manage_filter.rs b/axiom-profiler-GUI/src/filters/manage_filter.rs
@@ -432,6 +432,7 @@ impl Component for ExistingFilterText {
                 if self.focus.is_none() {
                     let (s, v): (Vec<_>, Vec<_>) = self.inputs.iter().partition(|(c, _)| *c == '"');
                     let v = v.into_iter().map(|(_, input)| {
+                        // FIXME: this unwrap can sometimes panic, why?
                         let input = input.cast::<HtmlInputElement>().unwrap();
                         input.value().chars().filter(|c| c.is_digit(10)).collect::<String>().parse::<usize>().ok()
                     }).collect::<Option<_>>();

diff --git a/axiom-profiler-GUI/src/results/node_info.rs b/axiom-profiler-GUI/src/results/node_info.rs
@@ -188,49 +188,53 @@ pub fn SelectedNodesInfo(
             let z3_gen = info.node.kind().inst().and_then(|i| (& *parser.borrow())[i].z3_generation).map(|g| format!(" (z3 gen {g})"));
 
             let quantifier_body = info.quantifier_body().map(|body| html! {
-                <><hr/>
-                <InfoLine header="Body" text={body} code=true /></>
+                <><InfoLine header="Body" text={body} code=true /><hr/></>
             });
             let blame: Option<Html> = info.blame().map(|blame| blame.into_iter().enumerate().map(|(idx, (trigger, enode, equalities))| {
                 let equalities: Html = equalities.into_iter().map(|equality| html! {
                     <InfoLine header="Equality" text={equality} code=true />
                 }).collect();
                 html! {
-                <><hr/>
+                <>
                     <InfoLine header={format!("Trigger #{idx}")} text={trigger} code=true />
                     <InfoLine header="Matched" text={enode} code=true />
                     {equalities}
-                </>
+                <hr/></>
                 }
             }).collect());
             let bound_terms = info.bound_terms().map(|terms| {
                 let bound: Html = terms.into_iter().map(|term| html! {
                     <InfoLine header="Bound" text={term} code=true />
                 }).collect();
-                html! { <><hr/>{bound}</> }
+                html! { <>{bound}<hr/></> }
             });
             let resulting_term = info.resulting_term().map(|term| html! {
-                <><hr/>
-                <InfoLine header="Resulting Term" text={term} code=true /></>
+                <><InfoLine header="Resulting Term" text={term} code=true /><hr/></>
             });
             let yield_terms = info.yield_terms().map(|terms| {
                 let yields: Html = terms.into_iter().map(|term| html! {
                     <InfoLine header="Yield" text={term} code=true />
                 }).collect();
-                html! { <><hr/>{yields}</> }
+                html! { <>{yields}<hr/></> }
             });
             html! {
                 <details {open}>
                 <summary {onclick}>{summary}{description}</summary>
                 <ul>
-                    <InfoLine header="Cost" text={format!("{:.1}{}", info.node.cost, z3_gen.unwrap_or_default())} code=false />
-                    <InfoLine header="To Root" text={format!("short {}, long {}", info.node.fwd_depth.min, info.node.fwd_depth.max)} code=false />
-                    <InfoLine header="To Leaf" text={format!("short {}, long {}", info.node.bwd_depth.min, info.node.bwd_depth.max)} code=false />
                     {quantifier_body}
                     {blame}
                     {bound_terms}
                     {resulting_term}
                     {yield_terms}
+                    <InfoLine header="Cost" text={format!("{:.1}{}", info.node.cost, z3_gen.unwrap_or_default())} code=false />
+                    <InfoLine header="To Root" text={format!("short {}, long {}", info.node.fwd_depth.min, info.node.fwd_depth.max)} code=false />
+                    <InfoLine header="To Leaf" text={format!("short {}, long {}", info.node.bwd_depth.min, info.node.bwd_depth.max)} code=false />
+                    <InfoLine header="Degree" text={
+                        format!("parents {}, children {}",
+                            graph.raw.neighbors_directed(node, petgraph::Direction::Incoming).len(),
+                            graph.raw.neighbors_directed(node, petgraph::Direction::Outgoing).len()
+                        )
+                    } code=false />
                 </ul>
                 </details>
             }
@@ -287,15 +291,15 @@ impl<'a, 'b> EdgeInfo<'a, 'b> {
                 "Yield Equality".to_string(),
             VisibleEdgeKind::YieldBlameEq { .. } =>
                 "Yield/Blame Equality".to_string(),
-            VisibleEdgeKind::YieldEqOther(_, _) =>
+            VisibleEdgeKind::YieldEqOther(_) =>
                 "Yield Equality Other".to_string(),
             VisibleEdgeKind::ENodeEq(_) =>
                 "ENode Equality".to_string(),
             VisibleEdgeKind::ENodeBlameEq { .. } =>
                 "ENode/Blame Equality".to_string(),
-            VisibleEdgeKind::ENodeEqOther(_, _) =>
+            VisibleEdgeKind::ENodeEqOther(_) =>
                 "ENode Equality Other".to_string(),
-            VisibleEdgeKind::Unknown(start, _, end) => {
+            VisibleEdgeKind::Unknown(start, end) => {
                 let ctxt = self.ctxt;
                 let hidden_from = self.graph.raw.graph.edge_endpoints(start.0).unwrap().1;
                 let hidden_to = self.graph.raw.graph.edge_endpoints(end.0).unwrap().0;

diff --git a/smt-log-parser/src/parsers/z3/graph/analysis/mod.rs b/smt-log-parser/src/parsers/z3/graph/analysis/mod.rs
@@ -114,8 +114,8 @@ impl InstGraph {
             self.raw.graph[a.0].cost.total_cmp(&self.raw.graph[b.0].cost).reverse().then_with(|| a.cmp(&b))
         );
         self.analysis.children.sort_by(|&a, &b| {
-            let ac = self.raw.graph.neighbors_directed(a.0, Direction::Outgoing).count();
-            let bc = self.raw.graph.neighbors_directed(b.0, Direction::Outgoing).count();
+            let ac = self.raw.neighbors_directed(a, Direction::Outgoing).len();
+            let bc = self.raw.neighbors_directed(b, Direction::Outgoing).len();
             ac.cmp(&bc).reverse().then_with(|| a.cmp(&b))
         });
         self.analysis.fwd_depth_min.sort_by(|&a, &b|

diff --git a/smt-log-parser/src/parsers/z3/graph/subgraph.rs b/smt-log-parser/src/parsers/z3/graph/subgraph.rs
@@ -4,7 +4,7 @@ use mem_dbg::{MemDbg, MemSize};
 use petgraph::{graph::{DiGraph, EdgeIndex, Neighbors, NodeIndex, IndexType}, Directed, Direction::{self, Incoming, Outgoing}, Undirected};
 use roaring::RoaringBitmap;
 
-use super::{raw::RawIx, RawNodeIndex};
+use super::{raw::RawIx, InstGraph, RawNodeIndex};
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
 #[derive(Debug)]
@@ -136,6 +136,54 @@ impl TransitiveClosure {
     }
 }
 
+impl InstGraph {
+    pub fn non_visible_paths_between(&self, from: RawNodeIndex, to: RawNodeIndex) -> Option<(FxHashSet<RawNodeIndex>, Option<Vec<RawNodeIndex>>)> {
+        if from == to {
+            return Some(([to].into_iter().collect(), Some(vec![to])));
+        }
+
+        let from_node = &self.raw[from];
+        let to_node = &self.raw[to];
+        let (from_subgraph, _) = from_node.subgraph?;
+        let (to_subgraph, to_idx) = to_node.subgraph?;
+        if from_subgraph != to_subgraph {
+            return None;
+        }
+
+        let filtered = NodeFiltered::from_fn(&*self.raw.graph, |n| {
+            let node = &self.raw.graph[n];
+            !node.visible() && node.subgraph.is_some_and(|(subgraph, idx)| {
+                subgraph == from_subgraph && self.subgraphs[subgraph].reach_fwd.in_transitive_closure(idx, to_idx)
+            })
+        });
+
+        let mut paths_between: FxHashSet<_> = [to].into_iter().collect();
+        let mut simple_path = None;
+
+        let mut path = vec![from];
+        let mut stack = vec![filtered.neighbors_directed(from.0, Outgoing).map(RawNodeIndex).collect::<Vec<_>>()];
+        while let Some(mut neighbours) = stack.pop() {
+            if let Some(next) = neighbours.pop() {
+                stack.push(neighbours);
+                if paths_between.contains(&next) {
+                    paths_between.extend(path.iter().copied());
+                    if simple_path.is_none() {
+                        path.push(next);
+                        simple_path = Some(path);
+                    }
+                    path = Vec::new();
+                } else {
+                    path.push(next);
+                    stack.push(filtered.neighbors_directed(next.0, Outgoing).map(RawNodeIndex).collect::<Vec<_>>());
+                }
+            } else {
+                path.pop();
+            }
+        }
+        Some((paths_between, simple_path))
+    }
+}
+
 // Graph wrapper for Topo walk
 
 pub(super) struct SubgraphStartNodes<'g, N, E, Ix: IndexType> {