From e4a35a9ef1bd76cf2d2045f55bcbd27d825faaf3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= Date: Thu, 31 Oct 2024 17:42:52 +0100 Subject: [PATCH] Improve ML search performance --- .gitignore | 1 + axiom-profiler-GUI/src/results/filters.rs | 34 ++--- .../graph/analysis/matching_loop/analysis.rs | 137 ++++++++++++++++++ .../graph/analysis/matching_loop/mod.rs | 2 + .../graph/analysis/matching_loop/search.rs | 44 ++---- .../graph/analysis/matching_loop/signature.rs | 18 ++- .../src/analysis/graph/analysis/mod.rs | 30 ++-- smt-log-parser/src/analysis/graph/hide.rs | 23 ++- smt-log-parser/src/analysis/graph/mod.rs | 2 +- smt-log-parser/src/analysis/graph/subgraph.rs | 9 ++ smt-log-parser/src/analysis/graph/visible.rs | 76 +--------- smt-log-parser/src/parsers/z3/z3parser.rs | 10 ++ smt-log-parser/tests/parse_logs.rs | 11 +- 13 files changed, 248 insertions(+), 149 deletions(-) create mode 100644 smt-log-parser/src/analysis/graph/analysis/matching_loop/analysis.rs diff --git a/.gitignore b/.gitignore index 48409550..7e2309ec 100644 --- a/.gitignore +++ b/.gitignore @@ -2,3 +2,4 @@ Cargo.lock .DS_STORE /logs +*.log diff --git a/axiom-profiler-GUI/src/results/filters.rs b/axiom-profiler-GUI/src/results/filters.rs index 87669e80..3ca94657 100644 --- a/axiom-profiler-GUI/src/results/filters.rs +++ b/axiom-profiler-GUI/src/results/filters.rs @@ -5,7 +5,7 @@ use petgraph::{ use smt_log_parser::{ analysis::{ analysis::matching_loop::MLGraphNode, - raw::{Node, NodeKind, RawInstGraph}, + raw::{IndexesInstGraph, Node, NodeKind, RawInstGraph}, InstGraph, RawNodeIndex, }, display_with::{DisplayCtxt, DisplayWithCtxt}, @@ -151,26 +151,26 @@ impl Filter { } }) .collect::>(); - let relevant_non_qi_nodes: Vec<_> = - Dfs::new(&*graph.raw.graph, nth_ml_endnode.1[0].1 .0) - .iter(graph.raw.rev()) - .filter(|nx| graph.raw.graph[*nx].kind().inst().is_none()) - .filter(|nx| { - graph.raw.graph[*nx] - .inst_children + let start = nth_ml_endnode.1[0].1.index(&graph.raw).0; + let relevant_non_qi_nodes: Vec<_> = Dfs::new(&*graph.raw.graph, start) + .iter(graph.raw.rev()) + .filter(|nx| graph.raw.graph[*nx].kind().inst().is_none()) + .filter(|nx| { + graph.raw.graph[*nx] + .inst_children + .nodes + .intersection(&nodes_of_nth_matching_loop) + .count() + > 0 + && graph.raw.graph[*nx] + .inst_parents .nodes .intersection(&nodes_of_nth_matching_loop) .count() > 0 - && graph.raw.graph[*nx] - .inst_parents - .nodes - .intersection(&nodes_of_nth_matching_loop) - .count() - > 0 - }) - .map(RawNodeIndex) - .collect(); + }) + .map(RawNodeIndex) + .collect(); graph .raw .set_visibility_many(false, relevant_non_qi_nodes.into_iter()); diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/analysis.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/analysis.rs new file mode 100644 index 00000000..0d966126 --- /dev/null +++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/analysis.rs @@ -0,0 +1,137 @@ +use fxhash::FxHashSet; + +use crate::{ + analysis::{ + analysis::{MlEndNodes, TopoAnalysis}, + raw::Node, + InstGraph, RawNodeIndex, + }, + items::InstIdx, + FxHashMap, Z3Parser, +}; + +use super::MlSignature; + +pub struct MlAnalysis { + pub data: Vec, + pub node_to_ml: FxHashMap, +} + +impl MlAnalysis { + pub fn new(parser: &Z3Parser, signatures: Vec<(MlSignature, FxHashSet)>) -> Self { + let mut node_to_ml = FxHashMap::::default(); + let data = signatures + .into_iter() + .enumerate() + .map(|(i, (sig, iidxs))| { + node_to_ml.extend( + iidxs + .into_iter() + .map(|iidx| (iidx, MlNodeInfo::new(parser, iidx, i))), + ); + sig + }) + .collect(); + Self { data, node_to_ml } + } + + pub fn finalise(self, min_depth: u32) -> (MlEndNodes, FxHashSet) { + let mut ml_end_nodes: MlEndNodes = + self.data.into_iter().map(|sig| (sig, Vec::new())).collect(); + let mut ml_nodes = FxHashSet::default(); + for (iidx, data) in self.node_to_ml.iter() { + if !data.is_root || data.max_depth < min_depth { + continue; + } + ml_nodes.insert(*iidx); + Self::walk_tree(&self.node_to_ml, data, &mut ml_nodes); + ml_end_nodes[data.ml_sig].1.push((data.max_depth, *iidx)); + } + ml_end_nodes.retain_mut(|(_, v)| { + if v.is_empty() { + false + } else { + v.sort_unstable_by_key(|(len, idx)| (u32::MAX - *len, *idx)); + true + } + }); + (ml_end_nodes, ml_nodes) + } + + pub fn walk_tree( + node_to_ml: &FxHashMap, + data: &MlNodeInfo, + ml_nodes: &mut FxHashSet, + ) { + for &reachable in &data.tree_above { + if ml_nodes.insert(reachable) { + let data = &node_to_ml[&reachable]; + Self::walk_tree(node_to_ml, data, ml_nodes); + } + } + } +} + +#[derive(Clone, Debug)] +pub struct MlNodeInfo { + pub is_root: bool, + pub ml_sig: usize, + pub max_depth: u32, + pub ast_size: u32, + pub tree_above: FxHashSet, +} + +impl MlNodeInfo { + pub fn new(parser: &Z3Parser, iidx: InstIdx, ml_sig: usize) -> Self { + Self { + is_root: true, + ml_sig, + max_depth: 0, + ast_size: parser.inst_ast_size(iidx), + tree_above: FxHashSet::default(), + } + } +} + +impl TopoAnalysis for MlAnalysis { + type Value = FxHashSet; + + fn collect<'a, 'n, T: Iterator>( + &mut self, + graph: &'a InstGraph, + idx: RawNodeIndex, + _node: &'a Node, + from_all: impl Fn() -> T, + ) -> Self::Value + where + Self::Value: 'n, + { + let mut self_info = FxHashSet::default(); + for (_, info) in from_all() { + self_info.extend(info.iter().copied()); + } + + let Some(iidx) = graph.raw[idx].kind().inst() else { + return self_info; + }; + let Some(mut curr_info) = self.node_to_ml.remove(&iidx) else { + return self_info; + }; + + self_info.retain(|&prev_iidx| { + let prev_info = self.node_to_ml.get_mut(&prev_iidx).unwrap(); + if prev_info.ml_sig == curr_info.ml_sig && prev_info.ast_size <= curr_info.ast_size { + prev_info.is_root = false; + curr_info.max_depth = curr_info.max_depth.max(prev_info.max_depth + 1); + curr_info.tree_above.insert(prev_iidx); + false + } else { + true + } + }); + + self.node_to_ml.insert(iidx, curr_info); + self_info.insert(iidx); + self_info + } +} diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs index f9b3035c..43384aad 100644 --- a/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs +++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/mod.rs @@ -1,8 +1,10 @@ +mod analysis; mod generalise; mod node; mod search; mod signature; +pub use analysis::*; pub use node::*; pub use signature::*; diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/search.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/search.rs index e1c4f3c1..f0c8e00e 100644 --- a/smt-log-parser/src/analysis/graph/analysis/matching_loop/search.rs +++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/search.rs @@ -1,8 +1,12 @@ +use fxhash::FxHashSet; use petgraph::visit::{Dfs, Reversed}; use crate::{ analysis::{ - analysis::MlEndNodes, raw::NodeKind, visible::VisibleEdge, InstGraph, RawNodeIndex, + analysis::{matching_loop::MlAnalysis, MlEndNodes}, + raw::{IndexesInstGraph, NodeKind}, + visible::VisibleEdge, + InstGraph, }, items::{GraphIdx, InstIdx, TermIdx, TimeRange}, Z3Parser, @@ -29,7 +33,11 @@ impl InstGraph { let long_path_leaves_sub_idx: Vec<_> = long_path_leaves .iter() - .map(|(_, leaves)| long_paths_subgraph.reverse(leaves[0].1).unwrap()) + .map(|(_, leaves)| { + long_paths_subgraph + .reverse(leaves[0].1.index(&self.raw)) + .unwrap() + }) .collect(); // assign to each node in a matching loop which matching loops it belongs to, i.e., if a node is part of the @@ -93,8 +101,8 @@ impl InstGraph { /// Per each quantifier, finds the nodes that are part paths of length at /// least `MIN_MATCHING_LOOP_LENGTH`. Additionally, returns a list of the /// endpoints of these paths. - fn find_long_paths_per_quant(&mut self, parser: &Z3Parser) -> (MlEndNodes, Vec) { - let signatures = Self::collect_ml_signatures(parser); + fn find_long_paths_per_quant(&mut self, parser: &Z3Parser) -> (MlEndNodes, FxHashSet) { + let signatures = self.collect_ml_signatures(parser); // Collect all signatures instantiated at least `MIN_MATCHING_LOOP_LENGTH` times let mut signatures: Vec<_> = signatures .into_iter() @@ -107,32 +115,12 @@ impl InstGraph { .then_some((sig, insts)) }) .collect(); - signatures.sort_unstable_by(|a, b| a.0.cmp(&b.0)); // eprintln!("Found {} signatures", signatures.len()); + signatures.sort_unstable_by(|a, b| a.0.cmp(&b.0)); - let mut long_path_leaves = Vec::new(); - let mut long_path_nodes = Vec::new(); - for (sig, insts) in signatures { - // eprintln!("Checking signature: {}", sig.to_string(parser)); - self.raw.reset_visibility_to(true); - let to_raw = self.raw.inst_to_raw_idx(); - self.raw - .set_visibility_many(false, insts.iter().copied().map(to_raw)); - let mut single_quant_subgraph = self.to_visible_opt(); - - let max_depths = - single_quant_subgraph.compute_longest_distances_from_roots(self, parser); - let (leaves, nodes) = single_quant_subgraph - .collect_nodes_in_long_paths(&max_depths, MIN_MATCHING_LOOP_LENGTH); - let mut leaves: Vec<_> = leaves.collect(); - if leaves.is_empty() { - continue; - } - leaves.sort_unstable_by_key(|(len, idx)| (u32::MAX - *len, *idx)); - long_path_leaves.push((sig, leaves)); - long_path_nodes.extend(nodes); - } - (long_path_leaves, long_path_nodes) + let mut analysis = MlAnalysis::new(parser, signatures); + self.topo_analysis(&mut analysis); + analysis.finalise(MIN_MATCHING_LOOP_LENGTH) } pub fn found_matching_loops(&self) -> Option { diff --git a/smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs b/smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs index 9132208c..169543ba 100644 --- a/smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs +++ b/smt-log-parser/src/analysis/graph/analysis/matching_loop/signature.rs @@ -7,7 +7,7 @@ use crate::{ analysis::InstGraph, display_with::{DisplayCtxt, DisplayWithCtxt}, formatter::TermDisplayContext, - items::{ENodeIdx, InstIdx, Instantiation, QuantIdx, TermIdx}, + items::{ENodeIdx, GraphIdx, InstIdx, QuantIdx, TermIdx}, FxHashMap, Z3Parser, }; @@ -17,6 +17,7 @@ pub struct MlSignature { pub quantifier: QuantIdx, pub pattern: TermIdx, pub parents: Box<[InstParent]>, + pub subgraph: GraphIdx, } /// For each pattern in the matched pattern, where did the blamed term come @@ -33,8 +34,10 @@ pub enum InstParent { } impl MlSignature { - pub fn new(parser: &Z3Parser, inst: &Instantiation) -> Option { - let match_ = &parser[inst.match_]; + pub fn new(graph: &InstGraph, parser: &Z3Parser, inst: InstIdx) -> Option { + let subgraph = graph.raw[inst].subgraph?.0; + + let match_ = &parser[parser[inst].match_]; let pattern = match_.kind.pattern()?; // If it has a pattern then definitely also has a quant_idx let quant_idx = match_.kind.quant_idx().unwrap(); @@ -56,6 +59,7 @@ impl MlSignature { quantifier: quant_idx, pattern, parents, + subgraph, }) } @@ -76,20 +80,22 @@ impl MlSignature { .collect::>() .join(", "); format!( - "{} {} {parents:?}", + "{} {} {parents:?} {:?}", self.quantifier.with(&ctxt), self.pattern, + self.subgraph, ) } } impl InstGraph { pub(super) fn collect_ml_signatures( + &self, parser: &Z3Parser, ) -> FxHashMap> { let mut signatures = FxHashMap::<_, FxHashSet<_>>::default(); - for (iidx, inst) in parser.instantiations().iter_enumerated() { - let Some(ml_sig) = MlSignature::new(parser, inst) else { + for (iidx, _) in parser.instantiations().iter_enumerated() { + let Some(ml_sig) = MlSignature::new(self, parser, iidx) else { continue; }; signatures.entry(ml_sig).or_default().insert(iidx); diff --git a/smt-log-parser/src/analysis/graph/analysis/mod.rs b/smt-log-parser/src/analysis/graph/analysis/mod.rs index 7996ab9f..b6a5f72f 100644 --- a/smt-log-parser/src/analysis/graph/analysis/mod.rs +++ b/smt-log-parser/src/analysis/graph/analysis/mod.rs @@ -10,7 +10,7 @@ use std::mem::MaybeUninit; use mem_dbg::{MemDbg, MemSize}; use petgraph::Direction; -use crate::{Graph, Result, TiVec, Z3Parser}; +use crate::{items::InstIdx, Graph, Result, TiVec, Z3Parser}; use self::{ cost::DefaultCost, @@ -21,7 +21,7 @@ use self::{ use super::{raw::Node, InstGraph, RawNodeIndex}; -pub type MlEndNodes = Vec<(MlSignature, Vec<(u32, RawNodeIndex)>)>; +pub type MlEndNodes = Vec<(MlSignature, Vec<(u32, InstIdx)>)>; #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))] #[derive(Debug, Default)] @@ -39,19 +39,21 @@ pub struct Analysis { } impl Analysis { - pub fn new(nodes: impl ExactSizeIterator + Clone) -> Result { + pub fn new(nodes: impl Iterator) -> Result { // Alloc `children` vector let mut cost = Vec::new(); - cost.try_reserve_exact(nodes.len())?; - cost.extend(nodes.clone()); + for node in nodes { + cost.try_reserve(1)?; + cost.push(node); + } // Alloc `children` vector let mut children = Vec::new(); - children.try_reserve_exact(nodes.len())?; - children.extend(nodes.clone()); + children.try_reserve_exact(cost.len())?; + children.extend(cost.iter().copied()); // Alloc `fwd_depth_min` vector let mut fwd_depth_min = Vec::new(); - fwd_depth_min.try_reserve_exact(nodes.len())?; - fwd_depth_min.extend(nodes.clone()); + fwd_depth_min.try_reserve_exact(cost.len())?; + fwd_depth_min.extend(cost.iter().copied()); Ok(Self { cost, children, @@ -69,7 +71,7 @@ impl InstGraph { const SKIP_DISABLED: bool, >( &self, - mut initialiser: I, + analysis: &mut I, ) -> TiVec { let mut data = typed_index_collections::TiVec::>::with_capacity( @@ -83,7 +85,7 @@ impl InstGraph { let mut data = TiVec::from(data); for subgraph in self.subgraphs.iter() { - initialiser.reset(); + analysis.reset(); let dir = if FORWARD { Direction::Incoming @@ -93,7 +95,7 @@ impl InstGraph { let for_each = |curr: RawNodeIndex| { let node = &self.raw[curr]; let value = if node.disabled() && SKIP_DISABLED { - initialiser.collect(self, curr, node, core::iter::empty) + analysis.collect(self, curr, node, core::iter::empty) } else { let from_all = || { let ix_map = |i: RawNodeIndex| { @@ -115,7 +117,7 @@ impl InstGraph { }; iter.map(ix_map) }; - initialiser.collect(self, curr, node, from_all) + analysis.collect(self, curr, node, from_all) }; data[curr] = MaybeUninit::new(value); }; @@ -129,7 +131,7 @@ impl InstGraph { for &singleton in &self.subgraphs.singletons { let node = &self.raw[singleton]; - let value = initialiser.collect(self, singleton, node, core::iter::empty); + let value = analysis.collect(self, singleton, node, core::iter::empty); data[singleton] = MaybeUninit::new(value); } diff --git a/smt-log-parser/src/analysis/graph/hide.rs b/smt-log-parser/src/analysis/graph/hide.rs index 499a9baf..bb6b35b0 100644 --- a/smt-log-parser/src/analysis/graph/hide.rs +++ b/smt-log-parser/src/analysis/graph/hide.rs @@ -4,7 +4,7 @@ use petgraph::{ }; use super::{ - raw::{EdgeKind, Node, NodeState, RawInstGraph, RawIx}, + raw::{EdgeKind, IndexesInstGraph, Node, NodeState, RawInstGraph, RawIx}, InstGraph, RawNodeIndex, }; @@ -61,8 +61,13 @@ impl RawInstGraph { } } } - pub fn set_visibility_many(&mut self, hidden: bool, nodes: impl Iterator) { + pub fn set_visibility_many( + &mut self, + hidden: bool, + nodes: impl Iterator, + ) { for node in nodes { + let node = node.index(self); self.set_visibility(hidden, node); } } @@ -145,15 +150,19 @@ impl RawInstGraph { impl InstGraph { pub fn keep_first_n_cost(&mut self, n: usize) { - self.raw.keep_first_n(self.analysis.cost.iter().copied(), n) + let cost = self.analysis.cost.iter().copied(); + let cost = cost.chain(self.subgraphs.singletons()); + self.raw.keep_first_n(cost, n) } pub fn keep_first_n_children(&mut self, n: usize) { - self.raw - .keep_first_n(self.analysis.children.iter().copied(), n) + let children = self.analysis.children.iter().copied(); + let children = children.chain(self.subgraphs.singletons()); + self.raw.keep_first_n(children, n) } pub fn keep_first_n_fwd_depth_min(&mut self, n: usize) { - self.raw - .keep_first_n(self.analysis.fwd_depth_min.iter().copied(), n) + let fwd_depth_min = self.analysis.fwd_depth_min.iter().copied(); + let fwd_depth_min = fwd_depth_min.chain(self.subgraphs.singletons()); + self.raw.keep_first_n(fwd_depth_min, n) } // pub fn keep_first_n_max_depth(&mut self, n: usize) { // self.raw.keep_first_n(self.analysis.max_depth.iter().copied(), n) diff --git a/smt-log-parser/src/analysis/graph/mod.rs b/smt-log-parser/src/analysis/graph/mod.rs index 7de6f576..aac2cf77 100644 --- a/smt-log-parser/src/analysis/graph/mod.rs +++ b/smt-log-parser/src/analysis/graph/mod.rs @@ -31,7 +31,7 @@ impl InstGraph { pub fn new(parser: &Z3Parser) -> Result { let mut raw = RawInstGraph::new(parser)?; let subgraphs = raw.partition()?; - let analysis = Analysis::new(raw.graph.node_indices().map(RawNodeIndex))?; + let analysis = Analysis::new(subgraphs.in_subgraphs())?; let mut self_ = InstGraph { raw, subgraphs, diff --git a/smt-log-parser/src/analysis/graph/subgraph.rs b/smt-log-parser/src/analysis/graph/subgraph.rs index 32702a7a..902f0955 100644 --- a/smt-log-parser/src/analysis/graph/subgraph.rs +++ b/smt-log-parser/src/analysis/graph/subgraph.rs @@ -23,6 +23,15 @@ pub struct Subgraphs { pub singletons: Vec, } +impl Subgraphs { + pub fn in_subgraphs(&self) -> impl Iterator + '_ { + self.subgraphs.iter().flat_map(|s| s.nodes.iter().copied()) + } + pub fn singletons(&self) -> impl Iterator + '_ { + self.singletons.iter().copied() + } +} + impl Deref for Subgraphs { type Target = TiVec; fn deref(&self) -> &Self::Target { diff --git a/smt-log-parser/src/analysis/graph/visible.rs b/smt-log-parser/src/analysis/graph/visible.rs index 5fd85d30..56185fe0 100644 --- a/smt-log-parser/src/analysis/graph/visible.rs +++ b/smt-log-parser/src/analysis/graph/visible.rs @@ -3,14 +3,14 @@ use std::ops::{Index, IndexMut}; use fxhash::{FxHashMap, FxHashSet}; use petgraph::{ graph::{DiGraph, EdgeIndex, NodeIndex}, - visit::{Dfs, EdgeRef, IntoEdgeReferences, Reversed, Topo, Walker}, + visit::{EdgeRef, IntoEdgeReferences}, Direction::{self, Incoming, Outgoing}, }; use crate::{ graph_idx, items::{ENodeIdx, EqGivenIdx}, - NonMaxU32, TiVec, Z3Parser, + NonMaxU32, }; use super::{ @@ -30,8 +30,8 @@ pub struct VisibleInstGraph { impl InstGraph { pub fn to_visible_opt(&self) -> VisibleInstGraph { - let bwd_vis_reachable = self.topo_analysis(BwdReachableVisAnalysis); - let mut reconnect = self.topo_analysis(ReconnectAnalysis(bwd_vis_reachable)); + let bwd_vis_reachable = self.topo_analysis(&mut BwdReachableVisAnalysis); + let mut reconnect = self.topo_analysis(&mut ReconnectAnalysis(bwd_vis_reachable)); let (mut nodes, mut edges) = (0, 0); for (idx, data) in reconnect.iter_mut_enumerated() { let node = &self.raw[idx]; @@ -362,74 +362,6 @@ impl VisibleInstGraph { } } } - - /// Collect all nodes that are part of a path of at least `min_length` - /// nodes. Additionally, returns a list of all of the leaves of these long - /// paths along with their max depth. - pub(crate) fn collect_nodes_in_long_paths<'a>( - &'a mut self, - max_depths: &'a TiVec, - min_length: u32, - ) -> ( - impl Iterator + 'a, - impl Iterator + 'a, - ) { - // traverse this subtree in topological order to compute longest distances from root nodes - let long_path_leaves: Vec<_> = self - .graph - .node_indices() - // only want to keep end nodes of longest paths, i.e., nodes without any children - .filter(|nx| self.graph.neighbors(*nx).next().is_none()) - // only want to show matching loops of length at least 3, hence only keep nodes with depth at least 2 - .filter(|nx| max_depths[VisibleNodeIndex(*nx)] >= min_length - 1) - .collect(); - // Walk backwards from leaves to collect all nodes - let rev_graph = Reversed(&self.graph); - let mut dfs = Dfs::empty(rev_graph); - dfs.stack = long_path_leaves.clone(); - - let long_path_leaves = long_path_leaves - .into_iter() - .map(|nx| (max_depths[VisibleNodeIndex(nx)], self.graph[nx].idx)); - let long_path_nodes = dfs.iter(rev_graph).map(|nx| self.graph[nx].idx); - (long_path_leaves, long_path_nodes) - } - - pub fn compute_longest_distances_from_roots( - &self, - graph: &InstGraph, - parser: &Z3Parser, - ) -> TiVec { - let mut ast_sizes: TiVec = - self.graph.node_indices().map(|_| u32::MAX).collect(); - let mut max_depths: TiVec = - self.graph.node_indices().map(|_| 0).collect(); - let mut topo = Topo::new(&self.graph); - while let Some(nx) = topo.next(&self.graph) { - let ast_size = graph.raw[self.graph[nx].idx] - .kind() - .inst() - .map(|inst| { - let bound_terms = parser[parser[inst].match_] - .kind - .bound_terms(|e| parser[e].owner, |t| t); - bound_terms - .iter() - .map(|&tidx| parser.ast_size(tidx).unwrap()) - .sum() - }) - .unwrap_or_default(); - ast_sizes[VisibleNodeIndex(nx)] = ast_size; - - let parents = self.graph.neighbors_directed(nx, Incoming); - let max_parent_depth = parents - .map(VisibleNodeIndex) - .filter_map(|nx| (ast_size >= ast_sizes[nx]).then_some(max_depths[nx] + 1)) - .max(); - max_depths[VisibleNodeIndex(nx)] = max_parent_depth.unwrap_or_default(); - } - max_depths - } } impl Index for VisibleInstGraph { diff --git a/smt-log-parser/src/parsers/z3/z3parser.rs b/smt-log-parser/src/parsers/z3/z3parser.rs index 11791f58..ef4848f8 100644 --- a/smt-log-parser/src/parsers/z3/z3parser.rs +++ b/smt-log-parser/src/parsers/z3/z3parser.rs @@ -847,6 +847,16 @@ impl Z3Parser { }; Some(children_size? + 1) } + + pub fn inst_ast_size(&self, iidx: InstIdx) -> u32 { + let bound_terms = self[self[iidx].match_] + .kind + .bound_terms(|e| self[e].owner, |t| t); + bound_terms + .iter() + .map(|&tidx| self.ast_size(tidx).unwrap()) + .sum() + } } impl std::ops::Index for Z3Parser { diff --git a/smt-log-parser/tests/parse_logs.rs b/smt-log-parser/tests/parse_logs.rs index a17d7af8..4dc02a31 100644 --- a/smt-log-parser/tests/parse_logs.rs +++ b/smt-log-parser/tests/parse_logs.rs @@ -96,13 +96,16 @@ fn parse_all_logs() { let now = Instant::now(); let mut inst_graph = InstGraph::new(&parser).unwrap(); + let elapsed_ig = now.elapsed(); assert!( - now.elapsed() < timeout, + elapsed_ig < timeout, "Constructing inst graph took longer than timeout" ); + let now = Instant::now(); inst_graph.search_matching_loops(&mut parser); - let elapsed = now.elapsed(); + let elapsed_ml = now.elapsed(); + let elapsed= elapsed_ig + elapsed_ml; max_analysis_ovhd = f64::max( max_analysis_ovhd, @@ -117,8 +120,8 @@ fn parse_all_logs() { ALLOCATOR.limit() / mb as usize, ); assert!( - elapsed < 4 * timeout, - "ML search took longer than 4*timeout" + elapsed_ml < timeout, + "ML search took longer than timeout" ); inst_graph.mem_dbg(DbgFlags::default()).ok(); println!();