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 7be3d2bb..f9b3035c 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 @@ -6,4 +6,4 @@ mod signature; pub use node::*; pub use signature::*; -pub const MIN_MATCHING_LOOP_LENGTH: usize = 3; +pub const MIN_MATCHING_LOOP_LENGTH: u32 = 6; 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 56d0a686..e1c4f3c1 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 @@ -4,7 +4,7 @@ use crate::{ analysis::{ analysis::MlEndNodes, raw::NodeKind, visible::VisibleEdge, InstGraph, RawNodeIndex, }, - items::{InstIdx, TermIdx, TimeRange}, + items::{GraphIdx, InstIdx, TermIdx, TimeRange}, Z3Parser, }; @@ -56,23 +56,34 @@ impl InstGraph { } fn has_n_overlapping_stacks( + &self, parser: &Z3Parser, i: impl Iterator, - n: usize, + n: u32, ) -> bool { - let mut frames: Vec<_> = i.map(|inst| parser[parser[inst].frame].active).collect(); + let mut frames: Vec<_> = i + .map(|inst| { + ( + self.raw[inst].subgraph.map(|s| s.0), + parser[parser[inst].frame].active, + ) + }) + .collect(); frames.sort_unstable(); - let mut frame_stack = Vec::::new(); - for frame in frames { + let mut frame_stack = Vec::<(GraphIdx, TimeRange)>::new(); + for (subgraph, frame) in frames { + let Some(subgraph) = subgraph else { + continue; + }; while let Some(last) = frame_stack.last() { - if last.sorted_overlap(&frame) { + if subgraph == last.0 && last.1.sorted_overlap(&frame) { break; } else { frame_stack.pop(); } } - frame_stack.push(frame); - if frame_stack.len() >= n { + frame_stack.push((subgraph, frame)); + if frame_stack.len() >= n as usize { return true; } } @@ -88,7 +99,7 @@ impl InstGraph { let mut signatures: Vec<_> = signatures .into_iter() .filter_map(|(sig, insts)| { - Self::has_n_overlapping_stacks( + self.has_n_overlapping_stacks( parser, insts.iter().copied(), MIN_MATCHING_LOOP_LENGTH, @@ -109,13 +120,15 @@ impl InstGraph { .set_visibility_many(false, insts.iter().copied().map(to_raw)); let mut single_quant_subgraph = self.to_visible_opt(); - let (leaves, nodes) = - single_quant_subgraph.collect_nodes_in_long_paths(MIN_MATCHING_LOOP_LENGTH); + 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)| (usize::MAX - *len, *idx)); + leaves.sort_unstable_by_key(|(len, idx)| (u32::MAX - *len, *idx)); long_path_leaves.push((sig, leaves)); long_path_nodes.extend(nodes); } diff --git a/smt-log-parser/src/analysis/graph/analysis/mod.rs b/smt-log-parser/src/analysis/graph/analysis/mod.rs index a86f7b0a..7996ab9f 100644 --- a/smt-log-parser/src/analysis/graph/analysis/mod.rs +++ b/smt-log-parser/src/analysis/graph/analysis/mod.rs @@ -21,7 +21,7 @@ use self::{ use super::{raw::Node, InstGraph, RawNodeIndex}; -pub type MlEndNodes = Vec<(MlSignature, Vec<(usize, RawNodeIndex)>)>; +pub type MlEndNodes = Vec<(MlSignature, Vec<(u32, RawNodeIndex)>)>; #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))] #[derive(Debug, Default)] diff --git a/smt-log-parser/src/analysis/graph/visible.rs b/smt-log-parser/src/analysis/graph/visible.rs index a7fef575..5fd85d30 100644 --- a/smt-log-parser/src/analysis/graph/visible.rs +++ b/smt-log-parser/src/analysis/graph/visible.rs @@ -10,7 +10,7 @@ use petgraph::{ use crate::{ graph_idx, items::{ENodeIdx, EqGivenIdx}, - NonMaxU32, + NonMaxU32, TiVec, Z3Parser, }; use super::{ @@ -58,7 +58,6 @@ impl InstGraph { idx, hidden_parents: hidden_parents as u32, hidden_children: hidden_children as u32, - max_depth: 0, }; graph.add_node(v_node); } @@ -109,7 +108,6 @@ impl InstGraph { idx, hidden_parents: hidden_parents as u32, hidden_children: hidden_children as u32, - max_depth: 0, } }) }; @@ -172,7 +170,6 @@ impl InstGraph { .iter() .filter(|&n| self.raw[*n].hidden()) .count() as u32, - max_depth: 0, }; node_index_map[i] = graph.add_node(nw); } @@ -369,22 +366,22 @@ 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( - &mut self, - min_length: usize, + pub(crate) fn collect_nodes_in_long_paths<'a>( + &'a mut self, + max_depths: &'a TiVec, + min_length: u32, ) -> ( - impl Iterator + '_, - impl Iterator + '_, + impl Iterator + 'a, + impl Iterator + 'a, ) { // traverse this subtree in topological order to compute longest distances from root nodes - Self::compute_longest_distances_from_roots(self); 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| self.graph[*nx].max_depth >= min_length - 1) + .filter(|nx| max_depths[VisibleNodeIndex(*nx)] >= min_length - 1) .collect(); // Walk backwards from leaves to collect all nodes let rev_graph = Reversed(&self.graph); @@ -393,18 +390,45 @@ impl VisibleInstGraph { let long_path_leaves = long_path_leaves .into_iter() - .map(|nx| (self.graph[nx].max_depth, self.graph[nx].idx)); + .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(&mut self) { + 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(|nx| self.graph[nx].max_depth + 1).max(); - self.graph[nx].max_depth = max_parent_depth.unwrap_or_default(); + 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 } } @@ -436,7 +460,6 @@ pub struct VisibleNode { pub idx: RawNodeIndex, pub hidden_parents: u32, pub hidden_children: u32, - pub max_depth: usize, } #[derive(Clone, PartialEq, Eq, Hash)] diff --git a/smt-log-parser/tests/parse_logs.rs b/smt-log-parser/tests/parse_logs.rs index a2d72320..5ff2183f 100644 --- a/smt-log-parser/tests/parse_logs.rs +++ b/smt-log-parser/tests/parse_logs.rs @@ -93,21 +93,33 @@ fn parse_all_logs() { mem_limit / mb, ); ALLOCATOR.set_limit(mem_limit as usize).unwrap(); + + let now = Instant::now(); let mut inst_graph = InstGraph::new(&parser).unwrap(); + assert!( + now.elapsed() < timeout, + "Constructing inst graph took longer than timeout" + ); + inst_graph.search_matching_loops(&mut parser); let elapsed = now.elapsed(); + max_analysis_ovhd = f64::max( max_analysis_ovhd, (ALLOCATOR.allocated() as u64 - middle_alloc) as f64 / parse_bytes as f64, ); println!( - "Finished analysis in {elapsed:?} ({} kB/ms). {} nodes. Memory use {} MB / {} MB:", + "Finished analysis in {elapsed:?} ({} kB/ms). {} nodes, {} mls. Memory use {} MB / {} MB:", parse_bytes_kb / elapsed.as_millis() as u64, inst_graph.raw.graph.node_count(), + inst_graph.analysis.matching_loop_end_nodes.as_ref().map(|ml| ml.len()).unwrap_or_default(), ALLOCATOR.allocated() / mb as usize, ALLOCATOR.limit() / mb as usize, ); - assert!(elapsed < timeout, "Analysis took longer than timeout"); + assert!( + elapsed < 10 * timeout, + "ML search took longer than 10*timeout" + ); inst_graph.mem_dbg(DbgFlags::default()).ok(); println!(); println!("===");