Skip to content

Commit

Permalink
Fix high degree filter and improve reconnect (#44)
Browse files Browse the repository at this point in the history 
* Fix high degree filter and improve reconnect

* Hide ML graph outside of ml_viewer_mode

* Fix # url issue
  • Loading branch information
@JonasAlaif
JonasAlaif authored May 27, 2024
1 parent 8a07853 commit 7952445
Show file tree
Hide file tree
Showing 7 changed files with 139 additions and 93 deletions.
1 change: 1 addition & 0 deletions axiom-profiler-GUI/src/filters/manage_filter.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<_>>();
Expand Down
5 changes: 4 additions & 1 deletion axiom-profiler-GUI/src/filters/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -233,7 +233,10 @@ impl Component for FiltersState {
let will_delete = ctx.link().callback(Msg::WillDelete);
// TODO: re-add finding matching loops
let found_mls = ctx.props().file.parser.found_mls;
let toggle_ml_viewer_mode = ctx.link().callback(|_| Msg::ToggleMlViewerMode);
let toggle_ml_viewer_mode = ctx.link().callback(|ev: MouseEvent| {
ev.prevent_default();
Msg::ToggleMlViewerMode
});
let ml_viewer_mode = if ctx.link().get_configuration().unwrap().config.persistent.ml_viewer_mode {
html! {
<li><a draggable="false" href="#" onclick={toggle_ml_viewer_mode}><div class="material-icons"><MatIcon>{"close"}</MatIcon></div>{"Exit matching loop viewer"}</a></li>
Expand Down
14 changes: 9 additions & 5 deletions axiom-profiler-GUI/src/results/graph_info.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -220,11 +220,15 @@ impl Component for GraphInfo {
<SelectedNodesInfo selected_nodes={self.selected_nodes.iter().map(|(k, v)| (*k, *v)).collect::<Vec<_>>()} on_click={on_node_click} />
<SelectedEdgesInfo selected_edges={self.selected_edges.iter().map(|(k, v)| (*k, *v)).collect::<Vec<_>>()} rendered={ctx.props().rendered.clone()} on_click={on_edge_click} />
{ if let Some(graph) = &self.displayed_matching_loop_graph {
html!{
<>
<h2>{"Information on Displayed Matching Loop"}</h2>
<div style="overflow-x: auto;">{Html::from_html_unchecked(graph.clone())}</div>
</>
if self.in_ml_viewer_mode {
html!{
<>
<h2>{"Information on Displayed Matching Loop"}</h2>
<div style="overflow-x: auto;">{Html::from_html_unchecked(graph.clone())}</div>
</>
}
} else {
html!{}
}
} else {
html!{}
Expand Down
32 changes: 18 additions & 14 deletions axiom-profiler-GUI/src/results/node_info.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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>
}
Expand Down Expand Up @@ -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;
Expand Down
4 changes: 2 additions & 2 deletions smt-log-parser/src/parsers/z3/graph/analysis/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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|
Expand Down
50 changes: 49 additions & 1 deletion smt-log-parser/src/parsers/z3/graph/subgraph.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down Expand Up @@ -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> {
Expand Down
Loading

0 comments on commit 7952445

Please sign in to comment.