From 685e8346d4d292813fa930948197ea86e3cd0ec0 Mon Sep 17 00:00:00 2001 From: ojyrkinen Date: Thu, 14 Dec 2023 15:24:04 +0100 Subject: [PATCH] First attempt for matching loop detection --- .../src/results/filters/graph_filters.rs | 11 +++ axiom-profiler-GUI/src/results/svg_result.rs | 2 +- smt-log-parser/src/parsers/z3/inst_graph.rs | 78 ++++++++++++++++++- 3 files changed, 87 insertions(+), 4 deletions(-) diff --git a/axiom-profiler-GUI/src/results/filters/graph_filters.rs b/axiom-profiler-GUI/src/results/filters/graph_filters.rs index 99159603..f445bc3d 100644 --- a/axiom-profiler-GUI/src/results/filters/graph_filters.rs +++ b/axiom-profiler-GUI/src/results/filters/graph_filters.rs @@ -20,6 +20,7 @@ pub enum Filter { VisitSubTreeWithRoot(NodeIndex, bool), MaxDepth(usize), ShowLongestPath(NodeIndex), + ShowMatchingLoops, } impl Display for Filter { @@ -46,6 +47,7 @@ impl Display for Filter { }, Self::MaxDepth(depth) => write!(f, "Show nodes up to depth {}", depth), Self::ShowLongestPath(node) => write!(f, "Showing longest path through node {}", node.index()), + Self::ShowMatchingLoops => write!(f, "Showing matching loops (experimental)"), } } } @@ -68,6 +70,7 @@ impl Filter { Filter::VisitSourceTree(nidx, retain) => graph.visit_ancestors(nidx, retain), Filter::MaxDepth(depth) => graph.retain_nodes(|node: &NodeData| node.min_depth.unwrap() <= depth), Filter::ShowLongestPath(nidx) => return Some(graph.show_longest_path_through(nidx)), + Filter::ShowMatchingLoops => graph.show_matching_loops(), } None } @@ -111,6 +114,10 @@ pub fn graph_filter(props: &GraphFilterProps) -> Html { let callback = props.add_filters.clone(); Callback::from(move |_| callback.emit(vec![Filter::MaxDepth(max_depth.value)])) }; + let show_matching_loops = { + let callback = props.add_filters.clone(); + Callback::from(move |_| callback.emit(vec![Filter::ShowMatchingLoops])) + }; html! {

{"Add (optional) filters:"}

@@ -158,6 +165,10 @@ pub fn graph_filter(props: &GraphFilterProps) -> Html { />
+
+ + +
{if selected_insts.len() > 0 { html! { diff --git a/axiom-profiler-GUI/src/results/svg_result.rs b/axiom-profiler-GUI/src/results/svg_result.rs index 7d5d4efd..7f917acd 100644 --- a/axiom-profiler-GUI/src/results/svg_result.rs +++ b/axiom-profiler-GUI/src/results/svg_result.rs @@ -140,7 +140,7 @@ impl Component for SVGResult { } Msg::ResetGraph => { log::debug!("Resetting graph"); - self.inst_graph.reset(); + self.inst_graph.reset_visibility_to(true); false } Msg::RenderGraph(UserPermission { permission }) => { diff --git a/smt-log-parser/src/parsers/z3/inst_graph.rs b/smt-log-parser/src/parsers/z3/inst_graph.rs index 4b95b831..dc4d394d 100644 --- a/smt-log-parser/src/parsers/z3/inst_graph.rs +++ b/smt-log-parser/src/parsers/z3/inst_graph.rs @@ -1,4 +1,4 @@ -use fxhash::FxHashMap; +use fxhash::{FxHashMap, FxHashSet}; use gloo_console::log; use petgraph::graph::{Edge, NodeIndex}; use petgraph::stable_graph::StableGraph; @@ -17,6 +17,8 @@ use crate::items::{BlamedTermItem, InstIdx, QuantIdx, TermIdx, DepType, Dependen use super::z3parser::Z3Parser; +const MATCHING_LOOP_LOWER_BOUND: usize = 3; + #[derive(Clone, Copy, Default)] pub struct NodeData { pub line_nr: usize, @@ -99,6 +101,7 @@ pub struct InstGraph { cost_ranked_node_indices: Vec, branching_ranked_node_indices: Vec, tr_closure: Vec, + non_theory_quants: FxHashSet, } enum InstOrder { @@ -394,9 +397,74 @@ impl InstGraph { // } // } - pub fn reset(&mut self) { + pub fn show_matching_loops(&mut self) { + let mut matching_loops: Vec> = Vec::new(); + for quant in self.non_theory_quants.clone() { + // log!(format!("Processing quant {}", quant)); + self.reset_visibility_to(true); + self.retain_nodes(|node: &NodeData| !node.is_theory_inst && node.quant_idx == quant); + self.retain_visible_nodes_and_reconnect(); + let mut subgraph_of_quant: Graph = Graph::from(self.visible_graph.clone()); + let longest_path = Self::find_longest_path(&mut subgraph_of_quant); + matching_loops.push(longest_path); + } + self.reset_visibility_to(false); + for matching_loop in matching_loops { + if matching_loop.len() >= MATCHING_LOOP_LOWER_BOUND { + for node in matching_loop { + // log!(format!("Node {} is part of a matching loop", node.index())); + self.orig_graph[node].visible = true; + } + } + } + } + + fn find_longest_path(graph: &mut Graph) -> Vec { + // traverse this subtree in topological order to compute longest distances from node + let mut topo = Topo::new(&*graph); + while let Some(nx) = topo.next(&*graph) { + let parents = graph.neighbors_directed(nx, Incoming); + let max_parent_depth = parents + .map(|nx| graph.node_weight(nx).unwrap().max_depth) + .max(); + if let Some(depth) = max_parent_depth { + // log!(format!("Computing depth {} for node {}", depth + 1, nx.index())); + graph[nx].max_depth = depth + 1; + } else { + graph[nx].max_depth = 0; + // log!(format!("Computing depth {} for node {}", 0, nx.index())); + } + } + let furthest_away_node_idx = graph + .node_indices() + .max_by(|node_a, node_b| graph.node_weight(*node_a).unwrap().max_depth.cmp(&graph.node_weight(*node_b).unwrap().max_depth)) + .unwrap(); + // log!(format!("Furthest away node is {}", furthest_away_node_idx.index())); + // backtrack a longest path from furthest away node in subgraph until we reach a root + let mut longest_path: Vec = Vec::new(); + let mut visitor: Vec= Vec::new(); + visitor.push(furthest_away_node_idx); + while let Some(curr) = visitor.pop() { + // log!(format!("Backtracking. Currently at node {}", curr.index())); + longest_path.push(graph.node_weight(curr).unwrap().orig_graph_idx); + let curr_distance = graph.node_weight(curr).unwrap().max_depth; + let pred = graph + .neighbors_directed(curr, Incoming) + .filter(|pred| { + let pred_distance = graph.node_weight(*pred).unwrap().max_depth; + pred_distance == curr_distance - 1 + }) + .last(); + if let Some(node) = pred { + visitor.push(node); + } + } + longest_path + } + + pub fn reset_visibility_to(&mut self, visibility: bool) { for node in self.orig_graph.node_weights_mut() { - node.visible = true; + node.visible = visibility; } } @@ -536,6 +604,10 @@ impl InstGraph { max_depth: 0, topo_ord: 0, }); + if !dep.quant_discovered { + self.non_theory_quants.insert(quant_idx); + // log!(format!("Inserting quant {} into non_theory_quants", quant_idx)); + } } } // then add all edges between nodes