From ac5fea633c5b5a43aedb508b71244cabb6aa8d6e Mon Sep 17 00:00:00 2001 From: ojyrkinen Date: Sat, 20 Jan 2024 11:06:51 +0100 Subject: [PATCH] Added option to compute ML graph of currently visible inst graph --- .../src/results/filters/graph_filters.rs | 11 +++++++++++ smt-log-parser/src/parsers/z3/inst_graph.rs | 13 +++++++++++++ 2 files changed, 24 insertions(+) diff --git a/axiom-profiler-GUI/src/results/filters/graph_filters.rs b/axiom-profiler-GUI/src/results/filters/graph_filters.rs index 6e240d6c..6040daee 100644 --- a/axiom-profiler-GUI/src/results/filters/graph_filters.rs +++ b/axiom-profiler-GUI/src/results/filters/graph_filters.rs @@ -25,6 +25,7 @@ pub enum Filter { SelectNthMatchingLoop(usize), ShowMatchingLoopSubgraph, AnalyzeMatchingLoopWithEndNode(NodeIndex), + ShowMatchingLoopGraph, } impl Display for Filter { @@ -77,6 +78,7 @@ impl Display for Filter { write!(f, "Showing all potential matching loops") } Self::AnalyzeMatchingLoopWithEndNode(node) => write!(f, "Analyzing potential matching loop with end-node {}", node.index()), + Self::ShowMatchingLoopGraph => write!(f, "Showing matching loop graph of currently visible graph"), } } } @@ -105,6 +107,7 @@ impl Filter { Filter::SelectNthMatchingLoop(n) => return FilterOutput::MatchingLoopGraph(graph.show_nth_matching_loop(n, parser)), Filter::ShowMatchingLoopSubgraph => graph.show_matching_loop_subgraph(), Filter::AnalyzeMatchingLoopWithEndNode(endnode) => return FilterOutput::MatchingLoopGraph(graph.analyze_matching_loop_with_endnode(endnode, parser)), + Filter::ShowMatchingLoopGraph => return FilterOutput::MatchingLoopGraph(graph.show_matching_loop_graph_of_visible_graph(parser)), } FilterOutput::None } @@ -201,6 +204,10 @@ impl Component for GraphFilters { let max_depth = self.max_depth; Callback::from(move |_| callback.emit(vec![Filter::MaxDepth(max_depth)])) }; + let matching_loop_graph = { + let callback = ctx.props().add_filters.clone(); + Callback::from(move |_| callback.emit(vec![Filter::ShowMatchingLoopGraph])) + }; html! {

{"Add (optional) filters:"}

@@ -240,6 +247,10 @@ impl Component for GraphFilters { />
+
+ + +
{if !self.selected_insts.is_empty() { html! { diff --git a/smt-log-parser/src/parsers/z3/inst_graph.rs b/smt-log-parser/src/parsers/z3/inst_graph.rs index d021f98e..434a905e 100644 --- a/smt-log-parser/src/parsers/z3/inst_graph.rs +++ b/smt-log-parser/src/parsers/z3/inst_graph.rs @@ -547,6 +547,19 @@ impl InstGraph { } } + pub fn show_matching_loop_graph_of_visible_graph(&self, p: &mut Z3Parser) -> Graph { + let potential_matching_loop = self.orig_graph.filter_map( + |_, node| Some(node).filter(|node| node.visible).cloned(), + |orig_graph_idx, edge_data| { + Some(EdgeType::Direct { + kind: edge_data.clone(), + orig_graph_idx, + }) + }, + ); + MatchingLoopGraph::from_graph(&potential_matching_loop, &self.orig_graph, p) + } + pub fn show_nth_matching_loop(&mut self, n: usize, p: &mut Z3Parser) -> Graph { self.reset_visibility_to(false); // relies on the fact that we have previously sorted self.matching_loop_end_nodes by max_depth in descending order in