From c7b7b2ff184491c10055b532f71ccf3380b59c6c Mon Sep 17 00:00:00 2001 From: ojyrkinen Date: Fri, 22 Dec 2023 09:11:42 +0100 Subject: [PATCH] Wrote basic code for term generalisation and refactored graph_filters.rs --- .../src/results/filters/filter_chain.rs | 4 +- .../src/results/filters/graph_filters.rs | 282 +++++++++++------- axiom-profiler-GUI/src/utils/mod.rs | 1 + axiom-profiler-GUI/src/utils/usize_input.rs | 77 +++++ smt-log-parser/src/display_with.rs | 5 +- smt-log-parser/src/items.rs | 5 +- smt-log-parser/src/parsers/z3/inst_graph.rs | 35 ++- smt-log-parser/src/parsers/z3/terms.rs | 30 +- smt-log-parser/src/parsers/z3/z3parser.rs | 7 +- 9 files changed, 330 insertions(+), 116 deletions(-) create mode 100644 axiom-profiler-GUI/src/utils/usize_input.rs diff --git a/axiom-profiler-GUI/src/results/filters/filter_chain.rs b/axiom-profiler-GUI/src/results/filters/filter_chain.rs index 8158d92c..2ab4e236 100644 --- a/axiom-profiler-GUI/src/results/filters/filter_chain.rs +++ b/axiom-profiler-GUI/src/results/filters/filter_chain.rs @@ -1,5 +1,5 @@ use super::super::svg_result::{UserPermission, DEFAULT_NODE_COUNT}; -use super::graph_filters::{Filter, GraphFilter}; +use super::graph_filters::{Filter, GraphFilters}; use gloo::console::log; use yew::prelude::*; // use gloo_console::log; @@ -114,7 +114,7 @@ impl yew::html::Component for FilterChain { let add_filters = ctx.link().callback(Msg::AddFilters); html!( <> - diff --git a/axiom-profiler-GUI/src/results/filters/graph_filters.rs b/axiom-profiler-GUI/src/results/filters/graph_filters.rs index 6e8f7cc5..85c8f0b0 100644 --- a/axiom-profiler-GUI/src/results/filters/graph_filters.rs +++ b/axiom-profiler-GUI/src/results/filters/graph_filters.rs @@ -1,5 +1,5 @@ use super::node_actions::NodeActions; -use crate::utils::input_state::{InputValue, UsizeInput}; +use crate::{utils::usize_input::UsizeInput, results::svg_result::DEFAULT_NODE_COUNT}; use petgraph::{stable_graph::NodeIndex, Direction}; use smt_log_parser::{ items::QuantIdx, @@ -21,7 +21,7 @@ pub enum Filter { VisitSubTreeWithRoot(NodeIndex, bool), MaxDepth(usize), ShowLongestPath(NodeIndex), - ShowMatchingLoops, + AnalyzeMatchingLoops(usize), } impl Display for Filter { @@ -61,7 +61,7 @@ impl Display for Filter { Self::ShowLongestPath(node) => { write!(f, "Showing longest path through node {}", node.index()) } - Self::ShowMatchingLoops => write!(f, "Showing matching loops"), + Self::AnalyzeMatchingLoops(loop_count) => write!(f, "Showing the {} longest matching loops", loop_count), } } } @@ -89,7 +89,7 @@ impl Filter { graph.retain_nodes(|node: &NodeData| node.min_depth.unwrap() <= depth) } Filter::ShowLongestPath(nidx) => return Some(graph.show_longest_path_through(nidx)), - Filter::ShowMatchingLoops => graph.show_matching_loops(), + Filter::AnalyzeMatchingLoops(n) => graph.show_n_longest_matching_loops(n), } None } @@ -101,107 +101,181 @@ pub struct GraphFilterProps { pub dependency: *const smt_log_parser::Z3Parser, } -#[function_component(GraphFilter)] -pub fn graph_filter(props: &GraphFilterProps) -> Html { - let max_node_idx = use_reducer(InputValue::default); - let max_instantiations = use_reducer(InputValue::default); - let max_branching = use_reducer(InputValue::default); - let max_depth = use_reducer(InputValue::default); - let selected_insts = use_context::>().expect("no ctx found"); +pub struct GraphFilters { + max_node_idx: usize, + max_instantiations: usize, + max_branching: usize, + max_depth: usize, + max_matching_loops: usize, + selected_insts: Vec, + context_listener: ContextHandle>, + // add additional bool field to store whether matching loops have + // already been analyzed + // analyzed_matching_loops + // in that case, display additional filters such as + // show n longest matching loops where n = +} - let add_max_line_nr_filter = { - let max_node_idx = max_node_idx.clone(); - let callback = props.add_filters.clone(); - Callback::from(move |_| callback.emit(vec![Filter::MaxNodeIdx(max_node_idx.value)])) - }; - let add_theory_filter = { - let callback = props.add_filters.clone(); - Callback::from(move |_| callback.emit(vec![Filter::IgnoreTheorySolving])) - }; - let add_max_insts_filter = { - let max_instantiations = max_instantiations.clone(); - let callback = props.add_filters.clone(); - Callback::from(move |_| callback.emit(vec![Filter::MaxInsts(max_instantiations.value)])) - }; - let add_max_branching_filter = { - let max_branching = max_branching.clone(); - let callback = props.add_filters.clone(); - Callback::from(move |_| callback.emit(vec![Filter::MaxBranching(max_branching.value)])) - }; - let add_max_depth_filter = { - let max_depth = max_depth.clone(); - let callback = props.add_filters.clone(); - Callback::from(move |_| callback.emit(vec![Filter::MaxDepth(max_depth.value)])) - }; - let show_matching_loops = { - let callback = props.add_filters.clone(); - Callback::from(move |_| callback.emit(vec![Filter::ShowMatchingLoops])) - }; - html! { -
-

{"Add (optional) filters:"}

-
- - -
-
- - -
-
- - -
-
- - -
-
- - -
+#[derive(Properties, PartialEq)] +pub struct GraphFiltersProps { + pub add_filters: Callback>, + pub dependency: *const smt_log_parser::Z3Parser, +} + +pub enum Msg { + SetMaxNodeIdx(usize), + SetMaxInsts(usize), + SetMaxBranching(usize), + SetMaxDepth(usize), + SetMaxMatchingLoops(usize), + SelectedInstsUpdated(Vec) +} + +impl Component for GraphFilters { + type Message = Msg; + type Properties = GraphFiltersProps; + + fn update(&mut self, ctx: &Context, msg: Self::Message) -> bool { + match msg { + Msg::SetMaxNodeIdx(to) => { + self.max_node_idx = to; + true + } + Msg::SetMaxInsts(to) => { + self.max_instantiations = to; + true + } + Msg::SetMaxBranching(to) => { + self.max_branching = to; + true + } + Msg::SetMaxDepth(to) => { + self.max_depth = to; + true + } + Msg::SetMaxMatchingLoops(to) => { + self.max_matching_loops = to; + true + } + Msg::SelectedInstsUpdated(selected_insts) => { + self.selected_insts = selected_insts; + true + } + } + } + + fn create(ctx: &Context) -> Self { + let (selected_insts, context_listener) = ctx + .link() + .context(ctx.link().callback(Msg::SelectedInstsUpdated)) + .expect("No context provided"); + Self { + max_node_idx: usize::MAX, + max_instantiations: DEFAULT_NODE_COUNT, + max_branching: usize::MAX, + max_depth: usize::MAX, + max_matching_loops: 1, + selected_insts, + context_listener, + } + } + fn view(&self, ctx: &Context) -> Html { + let add_max_line_nr_filter = { + let callback = ctx.props().add_filters.clone(); + let max_node_idx = self.max_node_idx; + Callback::from(move |_| callback.emit(vec![Filter::MaxNodeIdx(max_node_idx)])) + }; + let add_theory_filter = { + let callback = ctx.props().add_filters.clone(); + Callback::from(move |_| callback.emit(vec![Filter::IgnoreTheorySolving])) + }; + let add_max_insts_filter = { + let callback = ctx.props().add_filters.clone(); + let max_instantiations = self.max_instantiations; + Callback::from(move |_| callback.emit(vec![Filter::MaxInsts(max_instantiations)])) + }; + let add_max_branching_filter = { + let callback = ctx.props().add_filters.clone(); + let max_branching = self.max_branching; + Callback::from(move |_| callback.emit(vec![Filter::MaxBranching(max_branching)])) + }; + let add_max_depth_filter = { + let callback = ctx.props().add_filters.clone(); + let max_depth = self.max_depth; + Callback::from(move |_| callback.emit(vec![Filter::MaxDepth(max_depth)])) + }; + let analyze_matching_loops = { + let callback = ctx.props().add_filters.clone(); + let max_matching_loops = self.max_matching_loops; + Callback::from(move |_| callback.emit(vec![Filter::AnalyzeMatchingLoops(max_matching_loops)])) + }; + html! {
- - +

{"Add (optional) filters:"}

+
+ // pass a WeakComponentLink here as prop such that the UsizeInput can directly update the + // fields in the GraphFilters struct + + +
+
+ + +
+
+ + +
+
+ + +
+
+ + +
+ //
+ // + // + //
+
+ + +
+ {if !self.selected_insts.is_empty() { + html! { + + } + } else { + html! {} + }} + // + //
- {if !selected_insts.is_empty() { - html! { - - } - } else { - html! {} - }} - // - // -
- + } } -} +} \ No newline at end of file diff --git a/axiom-profiler-GUI/src/utils/mod.rs b/axiom-profiler-GUI/src/utils/mod.rs index 716bddac..5dbe046d 100644 --- a/axiom-profiler-GUI/src/utils/mod.rs +++ b/axiom-profiler-GUI/src/utils/mod.rs @@ -1,2 +1,3 @@ pub mod input_state; pub mod toggle_switch; +pub mod usize_input; \ No newline at end of file diff --git a/axiom-profiler-GUI/src/utils/usize_input.rs b/axiom-profiler-GUI/src/utils/usize_input.rs new file mode 100644 index 00000000..f9c3da88 --- /dev/null +++ b/axiom-profiler-GUI/src/utils/usize_input.rs @@ -0,0 +1,77 @@ +use wasm_bindgen::{JsCast, UnwrapThrowExt}; +use web_sys::HtmlInputElement; +use yew::prelude::*; + +#[derive(Properties, PartialEq)] +pub struct UsizeInputProps { + pub label: AttrValue, + pub placeholder: AttrValue, + pub set_value: Callback, +} + +#[function_component(UsizeInput)] +pub fn integer_input(props: &UsizeInputProps) -> Html { + let input_ref = use_node_ref(); + let set_value_to = { + let set_value = props.set_value.clone(); + move |input_event: Event| { + let target: HtmlInputElement = input_event + .target() + .unwrap_throw() + .dyn_into() + .unwrap_throw(); + if let Ok(value) = target.value().to_string().parse::() { + log::debug!("Setting the value to {}", value); + set_value.emit(value); + } + } + }; + + let set_value_on_enter = Callback::from({ + let set_value = set_value_to.clone(); + move |key_event: KeyboardEvent| { + if key_event.key() == "Enter" { + let event: Event = key_event.clone().into(); + set_value(event); + } + } + }); + + let set_value_on_blur = Callback::from({ + let set_value = set_value_to.clone(); + move |blur_event: FocusEvent| { + let event: Event = blur_event.clone().into(); + set_value(event); + } + }); + + // { + // // Whenever dependency changes, need to reset the state + // let dep = props.dependency; + // let input_value = input_value.clone(); + // let input_ref = input_ref.clone(); + // let default_value = props.default_value; + // use_effect_with_deps( + // { + // let input_value = input_value.clone(); + // move |_| { + // input_value.dispatch(InputAction::SetValueTo(default_value)); + // let input = input_ref + // .cast::() + // .expect("div_ref not attached to div element"); + // input.set_value(""); + // } + // }, + // dep, + // ); + // } + let placeholder = props.placeholder.to_string(); + + html! { + <> + + + + } +} + diff --git a/smt-log-parser/src/display_with.rs b/smt-log-parser/src/display_with.rs index 1e64a765..89282559 100644 --- a/smt-log-parser/src/display_with.rs +++ b/smt-log-parser/src/display_with.rs @@ -241,8 +241,8 @@ impl<'a> DisplayWithCtxt, DisplayData<'a>> for &'a Term { ) -> fmt::Result { data.with_children(&self.child_ids, |data| { if ctxt.display_term_ids { - let namespace = ctxt.parser.strings.resolve(&self.id.namespace); - let id = self.id.id.map(|id| id.to_string()).unwrap_or_default(); + let namespace = ctxt.parser.strings.resolve(&self.id.unwrap().namespace); + let id = self.id.unwrap().id.map(|id| id.to_string()).unwrap_or_default(); write!(f, "[{namespace}#{id}]")?; } if let Some(meaning) = &self.meaning { @@ -269,6 +269,7 @@ impl<'a> DisplayWithCtxt, DisplayData<'a>> for &'a TermKind { } TermKind::ProofOrApp(poa) => write!(f, "{}", poa.with_data(ctxt, data)), TermKind::Quant(idx) => write!(f, "{}", ctxt.parser[*idx].with_data(ctxt, data)), + TermKind::GeneralizedTerm => write!(f, "[generalized term]"), } } } diff --git a/smt-log-parser/src/items.rs b/smt-log-parser/src/items.rs index b0dd4fcb..9018217c 100644 --- a/smt-log-parser/src/items.rs +++ b/smt-log-parser/src/items.rs @@ -46,7 +46,7 @@ idx!(MatchIdx, "m{}"); /// A Z3 term and associated data. #[derive(Debug, Serialize, Deserialize)] pub struct Term { - pub id: TermId, + pub id: Option, pub kind: TermKind, pub meaning: Option, pub child_ids: Vec, @@ -57,6 +57,7 @@ pub enum TermKind { Var(usize), ProofOrApp(ProofOrApp), Quant(QuantIdx), + GeneralizedTerm, } #[derive(Debug, Clone, Serialize, Deserialize)] @@ -81,7 +82,7 @@ impl TermKind { } } -#[derive(Debug, Serialize, Deserialize, PartialEq, Eq)] +#[derive(Debug, Serialize, Deserialize, PartialEq, Eq, Clone, Copy)] pub struct Meaning { /// The theory in which the value should be interpreted (e.g. `bv`) pub theory: IString, diff --git a/smt-log-parser/src/parsers/z3/inst_graph.rs b/smt-log-parser/src/parsers/z3/inst_graph.rs index 0fc16682..d41b8930 100644 --- a/smt-log-parser/src/parsers/z3/inst_graph.rs +++ b/smt-log-parser/src/parsers/z3/inst_graph.rs @@ -1,3 +1,4 @@ +use futures::StreamExt; use fxhash::FxHashSet; use gloo_console::log; use itertools::Itertools; @@ -12,10 +13,11 @@ use petgraph::{ use petgraph::{Direction, Graph}; use roaring::bitmap::RoaringBitmap; use std::fmt; +use std::iter::zip; use typed_index_collections::TiVec; use crate::display_with::{DisplayCtxt, DisplayWithCtxt}; -use crate::items::{BlameKind, ENodeIdx, Fingerprint, InstIdx, MatchKind}; +use crate::items::{BlameKind, ENodeIdx, Fingerprint, InstIdx, MatchKind, Term, TermIdx}; use super::z3parser::Z3Parser; @@ -154,6 +156,35 @@ pub struct VisibleGraphInfo { pub edge_count_decreased: bool, } +pub fn generalize(t1: TermIdx, t2: TermIdx, p: &mut Z3Parser) -> TermIdx { + if t1 == t2 { + // if terms are equal, no need to generalize + t1 + } else if p.terms.is_general_term(t1) { + // if self is already generalized, no need to generalize further + t1 + } else { + // if neither term is generalized, check the meanings and recurse over children + if p[t1].meaning == p[t2].meaning { + let mut children: Vec = Vec::new(); + for (c1, c2) in zip(p[t1].child_ids.clone(), p[t2].child_ids.clone()) { + let child = generalize(c1, c2, p); + children.push(child) + } + if children.iter().any(|c| p.terms.is_general_term(*c)) { + // if term has any generalized children, need to crate new generalized term + p.terms.mk_generalized_term_with_children(p[t1].meaning, children) + } else { + // else, can just return t1 + t1 + } + } else { + // if not, generalize + p.terms.mk_generalized_term() + } + } +} + impl InstGraph { pub fn from(parser: &Z3Parser) -> Self { let mut inst_graph = Self::default(); @@ -427,7 +458,7 @@ impl InstGraph { // } // } - pub fn show_matching_loops(&mut self) { + pub fn show_n_longest_matching_loops(&mut self, n: usize) { let quants: FxHashSet<_> = self .orig_graph .node_weights() diff --git a/smt-log-parser/src/parsers/z3/terms.rs b/smt-log-parser/src/parsers/z3/terms.rs index 74505584..f693fe3f 100644 --- a/smt-log-parser/src/parsers/z3/terms.rs +++ b/smt-log-parser/src/parsers/z3/terms.rs @@ -1,6 +1,6 @@ use typed_index_collections::TiVec; -use crate::items::{StringTable, Term, TermId, TermIdToIdxMap, TermIdx}; +use crate::items::{StringTable, Term, TermId, TermIdToIdxMap, TermIdx, TermKind::GeneralizedTerm, Meaning}; #[derive(Debug)] pub struct Terms { @@ -36,6 +36,34 @@ impl Terms { pub(super) fn parse_existing_id(&self, strings: &mut StringTable, id: &str) -> Option { self.parse_id(strings, id).and_then(|r| r.ok()) } + + pub(super) fn mk_generalized_term(&mut self) -> TermIdx { + let idx = self.terms.next_key(); + let term = Term { + id: None, + kind: GeneralizedTerm, + meaning: None, + child_ids: Vec::new(), + }; + self.terms.push(term); + idx + } + + pub(super) fn is_general_term(&self, t: TermIdx) -> bool { + t == self.terms.last_key().unwrap() + } + + pub(super) fn mk_generalized_term_with_children(&mut self, meaning: Option, children: Vec) -> TermIdx { + let idx = self.terms.next_key(); + let term = Term { + id: None, + kind: GeneralizedTerm, + meaning, + child_ids: children, + }; + self.terms.push(term); + idx + } } impl std::ops::Index for Terms { diff --git a/smt-log-parser/src/parsers/z3/z3parser.rs b/smt-log-parser/src/parsers/z3/z3parser.rs index 632b2e6f..3604f737 100644 --- a/smt-log-parser/src/parsers/z3/z3parser.rs +++ b/smt-log-parser/src/parsers/z3/z3parser.rs @@ -213,7 +213,7 @@ impl Z3LogParser for Z3Parser { assert!(!children.is_empty()); let qidx = self.quantifiers.next_key(); let term = Term { - id: full_id, + id: Some(full_id), kind: TermKind::Quant(qidx), meaning: None, child_ids: children, @@ -240,7 +240,7 @@ impl Z3LogParser for Z3Parser { // Return if there is unexpectedly more data Self::expect_completed(l)?; let term = Term { - id: full_id, + id: Some(full_id), kind, meaning: None, child_ids: Vec::new(), @@ -261,7 +261,7 @@ impl Z3LogParser for Z3Parser { // TODO: add rewrite, monotonicity cases let children = self.gobble_children(l)?; let term = Term { - id: full_id, + id: Some(full_id), kind, meaning: None, child_ids: children, @@ -523,6 +523,7 @@ impl Z3LogParser for Z3Parser { fn eof(&mut self) { // TODO: this shouldn't be done here. self.compute_costs(); + self.terms.mk_generalized_term(); } fn push<'a>(&mut self, mut l: impl Iterator) -> Option<()> {