Added option to compute ML graph of currently visible inst graph

viperproject · Jan 20, 2024 · ac5fea6 · ac5fea6
1 parent bd94e5f
commit ac5fea6
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 0 deletions.
diff --git 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! {
             <div>
                 <h2>{"Add (optional) filters:"}</h2>
@@ -240,6 +247,10 @@ impl Component for GraphFilters {
                     />
                     <button onclick={add_max_depth_filter}>{"Add"}</button>
                 </div>
+                <div>
+                    <label for="matching_loop_graph">{"Generate matching loop graph"}</label>
+                    <button onclick={matching_loop_graph} id="matching_loop_graph">{"Add"}</button>
+                </div>
                 {if !self.selected_insts.is_empty() {
                     html! {
                         <NodeActions selected_nodes={self.selected_insts.clone()} action={ctx.props().add_filters.clone()} />

diff --git 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<String, InstOrEquality> {
+        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<String, InstOrEquality> {
         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