diff --git a/axiom-profiler-GUI/assets/html/perfetto.css b/axiom-profiler-GUI/assets/html/perfetto.css index 2773a72d..d1d39ab7 100644 --- a/axiom-profiler-GUI/assets/html/perfetto.css +++ b/axiom-profiler-GUI/assets/html/perfetto.css @@ -265,7 +265,9 @@ table { } .flags-page { + height: 100%; overflow-y: scroll; + z-index: 1; } .flags-content { max-width: 100ch; @@ -282,7 +284,7 @@ table { background: none; border: 1px solid rgb(218, 220, 224); border-radius: 2px; - color: rgb(25, 103, 210); + color: var(--flags-accent-color); font-size: 0.8125rem; padding: 8px 12px; cursor: pointer; @@ -305,8 +307,8 @@ table { .flag-widget select { grid-area: control; background: white; - border: 1px solid rgb(25, 103, 210); - color: rgb(25, 103, 210); + border: 1px solid var(--flags-accent-color); + color: var(--flags-accent-color); font-size: 0.8125rem; height: 1.625rem; letter-spacing: 0.01em; @@ -473,6 +475,7 @@ table { --section-background: hsl(213, 26%, 87%); --hover-background: hsl(216, 15%, 75%); --topbar-background: hsl(215, 1%, 95%); + --flags-accent-color: rgb(10, 75, 165); } * { diff --git a/axiom-profiler-GUI/assets/html/style.css b/axiom-profiler-GUI/assets/html/style.css index b36e3172..95435934 100644 --- a/axiom-profiler-GUI/assets/html/style.css +++ b/axiom-profiler-GUI/assets/html/style.css @@ -232,3 +232,61 @@ mwc-dialog { vertical-align: baseline; padding: 2px 3px; } + +.flags-content button:disabled { + cursor: default; + opacity: 0.5; +} +.flag-widget.term-display { + display: block; +} + +ul.td { + padding: 0; + margin-bottom: 6px; +} +li.td-row { + display: flex; + padding: 2px 0; +} + +li .td-matcher { + flex: 1 2 auto; + margin-right: 2px; +} +li.td-row.error .td-matcher, li .td-matcher.error { + border-color: red; +} +li .td-formatter { + flex: 2 1 auto; + margin-left: 2px; +} +li.td-row.error .td-formatter, li .td-formatter.error { + border-color: red; +} +li .td-error { + width: 1.8em; + margin-left: 4px; + display: flex; + justify-content: right; + align-items: center; +} +li .td-error.error { + cursor: help; +} + +li .td-matcher, li .td-formatter { + width: 100%; + padding: 3px 2px; +} +li input.td-matcher, li input.td-formatter { + background: white; + border: 1px solid var(--flags-accent-color); + color: var(--flags-accent-color); + font-size: 0.8125rem; + height: 1.625rem; + letter-spacing: 0.01em; +} +.td-buttons { + float: right; +} diff --git a/axiom-profiler-GUI/src/configuration/data.rs b/axiom-profiler-GUI/src/configuration/data.rs new file mode 100644 index 00000000..90170492 --- /dev/null +++ b/axiom-profiler-GUI/src/configuration/data.rs @@ -0,0 +1,80 @@ +use fxhash::FxHashMap; +use smt_log_parser::{display_with::{DisplayConfiguration, SymbolReplacement}, formatter::TermDisplayContext}; + +use crate::state::FileInfo; + +use super::ConfigurationProvider; + +impl ConfigurationProvider { + pub fn reset(&self) { + self.update.reset(); + } + pub fn update_display(&self, f: impl FnOnce(&mut DisplayConfiguration) -> bool + 'static) { + self.update.update(|cfg| f(&mut cfg.display)); + } + pub fn update_term_display(&self, file: Option, new: TermDisplayContext) { + self.update.update(move |cfg| { + if let Some(file) = file { + if new.is_empty() { + cfg.term_display.per_file.remove(&file.name).is_some() + } else { + let is_same = cfg.term_display.per_file.get(&file.name).is_some_and(|old| old == &new); + if !is_same { + cfg.term_display.per_file.insert(file.name, new); + } + !is_same + } + } else { + let is_same = cfg.term_display.general == new; + if !is_same { + cfg.term_display.general = new; + } + !is_same + } + }); + } +} + +#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct Configuration { + pub display: DisplayConfiguration, + pub term_display: TermDisplayContextFiles, +} +impl Configuration { + pub const fn default_display() -> DisplayConfiguration { + DisplayConfiguration { + display_term_ids: false, + display_quantifier_name: false, + replace_symbols: SymbolReplacement::Code, + html: true, + // Set manually elsewhere + enode_char_limit: None, + ast_depth_limit: None, + } + } +} + +impl Default for Configuration { + fn default() -> Self { + Self { + display: Self::default_display(), + term_display: TermDisplayContextFiles::default(), + } + } +} + +/// A grouping of general TermDisplayContext and per file ones. +#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)] +pub struct TermDisplayContextFiles { + pub general: TermDisplayContext, + pub per_file: FxHashMap, +} + +impl Default for TermDisplayContextFiles { + fn default() -> Self { + Self { + general: TermDisplayContext::basic(), + per_file: FxHashMap::default(), + } + } +} diff --git a/axiom-profiler-GUI/src/configuration/mod.rs b/axiom-profiler-GUI/src/configuration/mod.rs index f85626ac..61134e75 100644 --- a/axiom-profiler-GUI/src/configuration/mod.rs +++ b/axiom-profiler-GUI/src/configuration/mod.rs @@ -1,5 +1,7 @@ mod provider; mod page; +mod data; pub use provider::*; pub use page::*; +pub use data::*; diff --git a/axiom-profiler-GUI/src/configuration/page.rs b/axiom-profiler-GUI/src/configuration/page.rs index 2c3db76c..86ea13a9 100644 --- a/axiom-profiler-GUI/src/configuration/page.rs +++ b/axiom-profiler-GUI/src/configuration/page.rs @@ -1,15 +1,18 @@ -use std::rc::Rc; +use core::fmt; +use std::{borrow::Cow, rc::Rc}; +use smt_log_parser::{display_with::SymbolReplacement, formatter::{ConversionError, DeParseTrait, FallbackFormatter, FallbackParseError, Formatter, FormatterParseError, Matcher, TdcError, TermDisplay, TermDisplayContext}, NonMaxUsize}; use wasm_bindgen::JsCast; -use yew::{function_component, use_context, Callback, Html, Event, use_effect_with_deps}; +use web_sys::HtmlInputElement; +use yew::{function_component, prelude::Context, use_context, use_effect_with_deps, Callback, Component, Event, Html, NodeRef, Properties}; -use crate::configuration::{ConfigurationProvider, PersistentConfiguration}; +use crate::{configuration::{Configuration, ConfigurationProvider, TermDisplayContextFiles}, state::{FileInfo, StateProvider}}; macro_rules! flag_widget { - ($cfg:ident, $($access:ident).+, $($from:literal => $to:literal),+; $title:expr, $description:expr) => { + ($cfg:ident, $default:ident, $($access:ident).+, $title:expr, $description:expr, $($from:ident => $to:literal),+$(,)?) => { { let id = stringify!(cfg.$($access).+); - let curr = &(($cfg).config.persistent.$($access).+); + let curr = &(($cfg).config.$($access).+); let curr_to = match curr { $($from => $to,)+ }; @@ -22,7 +25,7 @@ macro_rules! flag_widget { || {} }; let deps = curr_to; - let default = PersistentConfiguration::default_const().$($access).+; + let default = $default.$($access).+; let default_to = match &default { $($from => $to,)+ }; @@ -37,7 +40,7 @@ macro_rules! flag_widget { $($to => $from,)+ _ => unreachable!(), }; - let old_value = &mut cfg.persistent.$($access).*; + let old_value = &mut cfg.$($access).*; if old_value != &new_value { *old_value = new_value; true @@ -63,22 +66,28 @@ macro_rules! flag_widget { pub fn Flags(_props: &()) -> Html { let cfg = use_context::>().unwrap(); let cfg_update = cfg.update.clone(); - let reset = Callback::from(move |_| cfg_update.update(|cfg| { - let new = PersistentConfiguration::default(); - if cfg.persistent != new { - cfg.persistent = new; - true - } else { - false - } - })); + let reset = Callback::from(move |_| cfg_update.reset()); + let default = Configuration::default(); let (display_term_ids, effect, deps) = flag_widget!( cfg, + default, display.display_term_ids, - true => "Enabled", - false => "Disabled"; "Display term IDs", - "Display the IDs (e.g. `#123`) of the terms as they appear in the log file in the UI." + "Display the IDs (e.g. `#123`) of the terms as they appear in the log file in the UI.", + true => "Enabled", + false => "Disabled" + ); + use_effect_with_deps(move |deps| effect(deps), deps); + use SymbolReplacement::*; + let (replace_symbols, effect, deps) = flag_widget!( + cfg, + default, + display.replace_symbols, + "Symbol replacement", + "Replace some symbols (e.g. \"not\", \"and\", \"<=\") in the UI with their corresponding mathematical or code representation.", + Math => "Mathematical", + Code => "Code", + None => "Disabled", ); use_effect_with_deps(move |deps| effect(deps), deps); @@ -87,6 +96,398 @@ pub fn Flags(_props: &()) -> Html {

{"Configuration flags"}

{display_term_ids} + {replace_symbols} + } } + +#[derive(Properties, Clone)] +pub struct TermDisplayFlagProps { + pub cfg: Rc, +} + +impl PartialEq for TermDisplayFlagProps { + fn eq(&self, other: &Self) -> bool { + self.cfg.config.term_display == other.cfg.config.term_display + } +} + +#[function_component] +pub fn TermDisplayFlag(props: &TermDisplayFlagProps) -> Html { + let term_display = &props.cfg.config.term_display; + let mut default = TermDisplayContextFiles::default(); + let data = use_context::>().unwrap(); + let file = data.state.file_info.as_ref(); + + let term_display_general = &term_display.general; + let cfg = props.cfg.clone(); + let apply = Callback::from(move |new| cfg.update_term_display(None, new)); + let cfg = props.cfg.clone(); + let reset = Callback::from(move |_| cfg.update_term_display(None, default.general.clone())); + let general = term_display_file_to_html((term_display_general, apply, reset, None)); + + let term_display_file = file.map(|f| term_display.per_file.get(&f.name).map(Cow::Borrowed).unwrap_or_default()); + let term_display_file = term_display_file.as_ref().map(|td| { + let f = file.unwrap(); + let cfg = props.cfg.clone(); + let file = f.clone(); + let default = default.per_file.remove(&file.name).unwrap_or_default(); + let reset = Callback::from(move |_| cfg.update_term_display(Some(file.clone()), default.clone())); + let cfg = props.cfg.clone(); + let file = f.clone(); + let apply = Callback::from(move |new| cfg.update_term_display(Some(file.clone()), new)); + (td.as_ref(), apply, reset, Some(f)) + }); + let file = term_display_file.map(term_display_file_to_html); + yew::html! { + <>{general}{file} + } +} + +fn term_display_file_to_html((td_ctx, apply, reset, file): (&TermDisplayContext, Callback, Callback<()>, Option<&FileInfo>)) -> Html { + let title = if let Some(file) = file { + format!("Term Formatting ({})", file.name) + } else { + "Term Formatting (Global)".to_string() + }; + let description = if file.is_some() { + "Formatting rules for the specified file. Replaces any global rules which match identically." + } else { + "Configure how to pretty print terms in the UI. If no matching formatting rule is found for a term, it is printed as a function application." + }; + yew::html! { +
+ +
{description}
+ +
+ } +} + +struct TermDisplayComponent { + fallback: String, + fallback_ref: NodeRef, + fallback_parsed: Result, + tds: Vec, + parsed: Option>, + modified: bool, + focused: Option<(NonMaxUsize, bool)>, +} + +pub enum TdcMsg { + ChangedRow(NonMaxUsize, bool, Event), + ChangedFallback(Event), + Revert, + Apply, + OnFocus(NonMaxUsize, bool), + OnBlur(NonMaxUsize, bool), +} + +#[derive(Properties, PartialEq)] +struct TermDisplayComponentProps { + pub td_ctx: TermDisplayContext, + pub apply: Callback, + pub reset: Callback<()>, +} + +#[derive(Debug)] +struct TermDisplayRow { + matcher: String, + matcher_ref: NodeRef, + matcher_err: Option, + formatter: String, + formatter_ref: NodeRef, + formatter_err: Option, + parsed: Option>, +} + +impl TermDisplayRow { + pub fn cmp_key(&self) -> impl Ord + '_ { + match self.matcher.as_bytes() { + [b'/', ..] => Err(1), + [b'(', b'/', ..] => Err(0), + [b'(', ..] => Ok((0, &self.matcher)), + _ => Ok((1, &self.matcher)), + } + } +} + +impl Component for TermDisplayComponent { + type Message = TdcMsg; + type Properties = TermDisplayComponentProps; + + fn create(ctx: &Context) -> Self { + let mut tds: Vec<_> = ctx.props().td_ctx.all().map(|td| { + let (matcher, formatter) = td.deparse_string(); + TermDisplayRow { + matcher, + matcher_ref: NodeRef::default(), + matcher_err: None, + formatter, + formatter_ref: NodeRef::default(), + formatter_err: None, + parsed: Some(Ok(td.clone())), + } + }).collect(); + tds.sort_by(|a, b| a.cmp_key().cmp(&b.cmp_key())); + let fallback = ctx.props().td_ctx.fallback(); + let mut self_ = Self { + fallback: fallback.formatter().deparse_string(), + fallback_ref: NodeRef::default(), + fallback_parsed: Ok(fallback.clone()), + tds, + parsed: Some(Ok(ctx.props().td_ctx.clone())), + modified: false, + focused: None, + }; + self_.check_last_td(); + self_ + } + fn changed(&mut self, ctx: &Context, old_props: &Self::Properties) -> bool { + debug_assert!(ctx.props() != old_props); + *self = Self::create(ctx); + true + } + + fn update(&mut self, ctx: &Context, msg: Self::Message) -> bool { + match msg { + TdcMsg::ChangedRow(idx, _matcher, _e) => { + let td = &mut self.tds[idx.get()]; + td.try_parse(); + self.try_parse(); + self.modified = !self.parsed.as_ref().is_some_and(|p| p.as_ref().is_ok_and(|tdc| tdc == &ctx.props().td_ctx)); + + if idx.get() == self.tds.len() - 1 { + self.check_last_td(); + } + true + } + TdcMsg::ChangedFallback(_e) => { + let fallback = self.fallback_ref.cast::().unwrap(); + self.fallback = fallback.value(); + self.fallback_parsed = self.fallback.parse::(); + self.try_parse(); + self.modified = !self.parsed.as_ref().is_some_and(|p| p.as_ref().is_ok_and(|tdc| tdc == &ctx.props().td_ctx)); + true + } + TdcMsg::Revert => { + *self = Self::create(ctx); + true + } + TdcMsg::Apply => { + ctx.props().apply.emit(self.parsed.clone().unwrap().unwrap()); + false + } + TdcMsg::OnFocus(idx, matcher) => { + self.focused = Some((idx, matcher)); + false + } + TdcMsg::OnBlur(idx, matcher) => { + if self.focused == Some((idx, matcher)) { + self.focused = None; + } + false + } + } + } + + fn view(&self, ctx: &Context) -> Html { + let tds = self.tds.iter().enumerate().map(|(i, td)| { + let mut errors = Vec::new(); + let idx = NonMaxUsize::new(i).unwrap(); + let link = ctx.link().clone(); + let matcher_change = Callback::from(move |e: Event| { + let link = link.clone(); + gloo::timers::callback::Timeout::new(10, move || link.send_message(TdcMsg::ChangedRow(idx, true, e))).forget(); + }); + let link = ctx.link().clone(); + let matcher_focus = Callback::from(move |_| { + link.send_message(TdcMsg::OnFocus(idx, true)); + }); + let link = ctx.link().clone(); + let matcher_blur = Callback::from(move |_| { + link.send_message(TdcMsg::OnBlur(idx, true)); + }); + let matcher_class = if td.matcher_err.is_some() { "td-matcher error" } else { "td-matcher" }; + td.matcher_err.as_ref().map(AnyError::Matcher).map(|e| errors.push(e)); + + let link = ctx.link().clone(); + let formatter_change = Callback::from(move |e: Event| { + let link = link.clone(); + gloo::timers::callback::Timeout::new(10, move || link.send_message(TdcMsg::ChangedRow(idx, false, e))).forget(); + }); + let link = ctx.link().clone(); + let formatter_focus = Callback::from(move |_| { + link.send_message(TdcMsg::OnFocus(idx, false)); + }); + let link = ctx.link().clone(); + let formatter_blur = Callback::from(move |_| { + link.send_message(TdcMsg::OnBlur(idx, false)); + }); + let formatter_class = if td.formatter_err.is_some() { "td-formatter error" } else { "td-formatter" }; + td.formatter_err.as_ref().map(AnyError::Formatter).map(|e| errors.push(e)); + + let error = td.parsed.as_ref().is_some_and(|p| p.is_err()); + let class = if error { "td-row error" } else { "td-row" }; + td.parsed.as_ref().map(|p| p.as_ref().map_err(AnyError::TermDisplay).map_err(|e| errors.push(e))); + yew::html! { +
  • + + + {error_tooltip(errors)} +
  • + } + }); + let link = ctx.link().clone(); + let formatter_change = Callback::from(move |e: Event| { + link.send_message(TdcMsg::ChangedFallback(e)); + }); + let formatter_class = if self.fallback_parsed.is_err() { "td-formatter error" } else { "td-formatter" }; + let fallback = yew::html! { +
  • +
    {"Fallback:"}
    + + {error_tooltip(self.fallback_parsed.as_ref().err().into_iter().map(AnyError::Fallback).collect())} +
  • + }; + let tds = [fallback].into_iter().chain(tds); + let modified = self.modified; + let can_apply = modified && self.fallback_parsed.is_ok() && self.tds.iter().all(|td| + td.is_empty() || td.parsed.as_ref().is_some_and(|p| p.is_ok()) + ); + let link = ctx.link().clone(); + let apply = Callback::from(move |_| { + if !can_apply { + return; + } + link.send_message(TdcMsg::Apply); + }); + let link = ctx.link().clone(); + let revert = Callback::from(move |_| { + if !modified { + return; + } + link.send_message(TdcMsg::Revert); + }); + let reset = ctx.props().reset.clone(); + let reset = Callback::from(move |_| reset.emit(())); + yew::html! { + <>
      + {for tds} +
    +
    + + + +
    + + } + } + + fn rendered(&mut self, _ctx: &Context, _first_render: bool) { + if let Some((idx, matcher)) = self.focused { + let td = &self.tds[idx.get()]; + let ref_ = if matcher { &td.matcher_ref } else { &td.formatter_ref }; + if let Some(element) = ref_.cast::() { + element.focus().ok(); + } + } + } +} + +impl TermDisplayComponent { + pub fn try_parse(&mut self) { + self.parsed = None; + let Ok(fallback) = &self.fallback_parsed else { + return; + }; + let all_td_ok = self.tds.iter().all(|td| td.is_empty() || td.parsed.as_ref().is_some_and(|p| p.is_ok())); + if !all_td_ok { + return; + } + + let tds = self.tds.iter().flat_map(|td| &td.parsed).map(|p| p.as_ref().unwrap().clone()); + let mut tdc: Result = tds.collect(); + if let Ok(tdc) = &mut tdc { + tdc.set_fallback(fallback.clone()); + } + self.parsed = Some(tdc); + } + + pub fn check_last_td(&mut self) { + if !self.tds.last().is_some_and(|td| td.is_empty()) { + self.tds.push(TermDisplayRow { + matcher: String::new(), + matcher_ref: NodeRef::default(), + matcher_err: None, + formatter: String::new(), + formatter_ref: NodeRef::default(), + formatter_err: None, + parsed: None, + }); + } + } +} + +impl TermDisplayRow { + pub fn try_parse(&mut self) -> Option<()> { + let matcher = self.matcher_ref.cast::()?; + self.matcher = matcher.value(); + let formatter = self.formatter_ref.cast::()?; + self.formatter = formatter.value(); + + let matcher = self.matcher.parse::(); + let formatter = self.formatter.parse::(); + + self.matcher_err = None; + self.formatter_err = None; + self.parsed = None; + + match (matcher, formatter) { + (Ok(matcher), Ok(formatter)) => { + if !self.is_empty() { + self.parsed = Some(TermDisplay::new(matcher, formatter)); + } + } + (Err(matcher), Err(formatter)) => { + self.matcher_err = Some(matcher); + self.formatter_err = Some(formatter); + } + (Err(matcher), Ok(_)) => { + self.matcher_err = Some(matcher); + } + (Ok(_), Err(formatter)) => { + self.formatter_err = Some(formatter); + } + } + Some(()) + } + + pub fn is_empty(&self) -> bool { + self.matcher.is_empty() && self.formatter.is_empty() + } +} + +#[derive(Debug)] +pub enum AnyError<'a> { + Matcher(&'a ConversionError), + Formatter(&'a FormatterParseError), + TermDisplay(&'a ConversionError), + Fallback(&'a FallbackParseError), +} + +impl fmt::Display for AnyError<'_> { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + // TODO: add a proper display here + write!(f, "{self:?}") + } +} + +pub fn error_tooltip(errors: Vec>) -> Html { + let title = errors.iter().map(AnyError::to_string).collect::>().join("\n"); + let class = if errors.is_empty() { "td-error" } else { "td-error error" }; + yew::html! { +
    {if errors.is_empty() { "" } else { "❌" }}
    + } +} diff --git a/axiom-profiler-GUI/src/configuration/provider.rs b/axiom-profiler-GUI/src/configuration/provider.rs index 87f27abb..75f8384a 100644 --- a/axiom-profiler-GUI/src/configuration/provider.rs +++ b/axiom-profiler-GUI/src/configuration/provider.rs @@ -1,106 +1,26 @@ -use std::{cell::RefCell, rc::Rc}; +use std::rc::Rc; -use gloo::{console::log, storage::Storage}; -use smt_log_parser::display_with::DisplayConfiguration; +use gloo::storage::Storage; use yew::{html, prelude::{Context, Html}, Callback, Children, Component, ContextProvider, Properties}; -use crate::RcParser; +use crate::utils::updater::{Update, Updater}; -// Public +use super::Configuration; -pub trait ConfigurationContext { - fn get_configuration(&self) -> Option>; -} -impl ConfigurationContext for html::Scope { - fn get_configuration(&self) -> Option> { - self.context(Callback::noop()).map(|c| c.0) - } -} +// Public #[derive(Clone, PartialEq)] pub struct ConfigurationProvider { pub config: Configuration, - pub update: ConfigurationUpdater, -} -#[derive(Clone, PartialEq)] -pub struct ConfigurationUpdater(Callback); -impl ConfigurationUpdater { - pub fn update(&self, f: impl for<'a> FnOnce(&'a mut Configuration) -> bool + 'static) { - self.0.emit(ConfigurationUpdate::new(f)); - } -} -pub struct ConfigurationUpdate(Callback<&'static mut Configuration, bool>); -impl ConfigurationUpdate { - fn new(f: impl for<'a> FnOnce(&'a mut Configuration) -> bool + 'static) -> Self { - let f = RefCell::new(Some(f)); - let f = Callback::from(move |config| - f.borrow_mut().take().unwrap()(config) - ); - Self(f) - } - fn apply(self, config: &mut Configuration) -> bool { - // SAFETY: the callback can only have been created with a - // `impl for<'a> FnOnce(&'a mut Configuration) -> bool + 'static`, and thus - // it cannot make use of the `&'static mut Configuration` lifetime. - let config = unsafe { &mut *(config as *mut _) }; - self.0.emit(config) - } -} - -impl ConfigurationProvider { - pub fn reset_persistent(&self) { - self.update.update(|cfg| { - let new = Default::default(); - if cfg.persistent != new { - cfg.persistent = new; - true - } else { - false - } - }); - } - pub fn update_display(&self, f: impl FnOnce(&mut DisplayConfiguration) -> bool + 'static) { - self.update.update(|cfg| f(&mut cfg.persistent.display)); - }pub fn update_parser(&self, f: impl FnOnce(&mut Option) -> bool + 'static) { - self.update.update(|cfg| f(&mut cfg.parser)); - } - pub fn reset_ml_viewer_mode(&self) { - self.update.update(|cfg| {cfg.persistent.ml_viewer_mode = false; true}); - } + pub update: Updater, } -#[derive(Clone, Default, PartialEq, Eq)] -pub struct Configuration { - pub parser: Option, - pub persistent: PersistentConfiguration, -} - -#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)] -pub struct PersistentConfiguration { - pub display: DisplayConfiguration, - pub ml_viewer_mode: bool, -} -impl PersistentConfiguration { - pub const fn default_const() -> Self { - let display = DisplayConfiguration { - display_term_ids: false, - display_quantifier_name: false, - use_mathematical_symbols: true, - html: true, - // Set manually elsewhere - enode_char_limit: None, - ast_depth_limit: None, - }; - Self { - display, - ml_viewer_mode: false, - } - } +pub trait ConfigurationContext { + fn get_configuration(&self) -> Option>; } - -impl Default for PersistentConfiguration { - fn default() -> Self { - Self::default_const() +impl ConfigurationContext for html::Scope { + fn get_configuration(&self) -> Option> { + self.context(Callback::noop()).map(|c| c.0) } } @@ -112,39 +32,39 @@ pub struct ConfigurationProviderProps { } impl Component for ConfigurationProvider { - type Message = ConfigurationUpdate; + type Message = Update; type Properties = ConfigurationProviderProps; fn create(ctx: &Context) -> Self { - let link = ctx.link().clone(); - let mut config = Configuration::default(); - if let Ok(cached) = gloo::storage::LocalStorage::get::("config") { - // log::warn!("ConfigurationProvider loaded: {cached:?}"); - config.persistent = cached; - config.persistent.ml_viewer_mode = false; + let config = gloo::storage::LocalStorage::get::("config"); + match &config { + Ok(_) | Err(gloo::storage::errors::StorageError::KeyNotFound(_)) => {} + Err(result) => log::error!("Configuration load error: {result:?}"), } - let update = Callback::from(move |config| link.send_message(config)); + + let config = config.unwrap_or_default(); Self { config, - update: ConfigurationUpdater(update), + update: Updater::new_link(ctx.link().clone()), } } fn update(&mut self, _ctx: &Context, msg: Self::Message) -> bool { - // log::warn!("ConfigurationProvider update: {:?}/{:?}: {:?}", msg.parser.is_some(), msg.parser.as_ref().map(|p| p.graph.is_some()), msg.persistent); let changed = msg.apply(&mut self.config); if changed { - gloo::storage::LocalStorage::set::<&PersistentConfiguration>("config", &self.config.persistent).ok(); + let result = gloo::storage::LocalStorage::set::<&Configuration>("config", &self.config); + if let Err(result) = result { + log::error!("Configuration save error: {result:?}"); + } } changed } fn view(&self, ctx: &Context) -> Html { - // log::warn!("ConfigurationProvider view: {:?}/{:?}", self.config.parser.is_some(), self.config.parser.as_ref().map(|p| p.graph.is_some())); html! { - > context={Rc::new(self.clone())}> - {ctx.props().children.clone()} - >> + > context={Rc::new(self.clone())}> + {for ctx.props().children.iter()} + >> } } } diff --git a/axiom-profiler-GUI/src/file.rs b/axiom-profiler-GUI/src/file.rs index 186c8f12..a188a7e6 100644 --- a/axiom-profiler-GUI/src/file.rs +++ b/axiom-profiler-GUI/src/file.rs @@ -7,7 +7,7 @@ use wasm_bindgen::JsCast; use web_sys::DataTransfer; use yew::{html::Scope, Callback, DragEvent}; -use crate::{global_callbacks::GlobalCallbacks, infobars::OmnibarMessage, CallbackRef, FileDataComponent, LoadingState, Msg, ParseProgress, PREVENT_DEFAULT_DRAG_OVER}; +use crate::{global_callbacks::GlobalCallbacks, infobars::OmnibarMessage, state::{FileInfo, StateContext}, CallbackRef, FileDataComponent, LoadingState, Msg, ParseProgress, PREVENT_DEFAULT_DRAG_OVER}; impl FileDataComponent { pub fn file_drag(registerer: &GlobalCallbacks, link: &Scope) -> [CallbackRef; 3] { @@ -72,6 +72,12 @@ impl FileDataComponent { let file_name = file.name(); let file_size = file.size(); + let (name, size) = (file_name.clone(), file_size); + link.get_state().unwrap().update_file_info(move |info| { + *info = Some(FileInfo { name, size }); + true + }); + log::info!("Selected file \"{file_name}\""); *self.cancel.borrow_mut() = false; let cancel = self.cancel.clone(); @@ -119,7 +125,7 @@ impl FileDataComponent { _ => (), } link.send_message(Msg::LoadingState(LoadingState::DoneParsing(finished.is_timeout(), cancel))); - link.send_message(Msg::LoadedFile(file_name, file_size, parser.take_parser(), finished, cancel)) + link.send_message(Msg::LoadedFile(parser.take_parser(), finished, cancel)) }); } Err((_err, _stream)) => { @@ -170,7 +176,7 @@ impl FileDataComponent { _ => (), } link.send_message(Msg::LoadingState(LoadingState::DoneParsing(finished.is_timeout(), cancel))); - link.send_message(Msg::LoadedFile(file_name, file_size, parser.take_parser(), finished, cancel)) + link.send_message(Msg::LoadedFile(parser.take_parser(), finished, cancel)) }); }); self.reader = Some(reader); diff --git a/axiom-profiler-GUI/src/filters/add_filter.rs b/axiom-profiler-GUI/src/filters/add_filter.rs index c65eed17..69a98ab4 100644 --- a/axiom-profiler-GUI/src/filters/add_filter.rs +++ b/axiom-profiler-GUI/src/filters/add_filter.rs @@ -5,7 +5,7 @@ use petgraph::{visit::{Dfs, Walker}, Direction}; use smt_log_parser::parsers::z3::graph::{raw::NodeKind, RawNodeIndex}; use yew::{function_component, html, use_context, Callback, Html, MouseEvent, Properties}; -use crate::{configuration::ConfigurationProvider, results::{filters::Filter, svg_result::DEFAULT_NODE_COUNT}}; +use crate::{results::{filters::Filter, svg_result::DEFAULT_NODE_COUNT}, state::StateProvider, RcParser}; #[derive(PartialEq, Properties)] pub struct AddFilterSidebarProps { @@ -17,8 +17,8 @@ pub struct AddFilterSidebarProps { #[function_component] pub fn AddFilterSidebar(props: &AddFilterSidebarProps) -> Html { - let cfg = use_context::>().unwrap(); - let Some(parser) = &cfg.config.parser else { + let data = use_context::>().unwrap(); + let Some(parser) = &data.state.parser else { return html!{} }; diff --git a/axiom-profiler-GUI/src/filters/manage_filter.rs b/axiom-profiler-GUI/src/filters/manage_filter.rs index 51afdccf..6dc7add7 100644 --- a/axiom-profiler-GUI/src/filters/manage_filter.rs +++ b/axiom-profiler-GUI/src/filters/manage_filter.rs @@ -6,7 +6,7 @@ use smt_log_parser::items::QuantIdx; use web_sys::{Element, HtmlElement, HtmlInputElement}; use yew::{function_component, html, use_context, Callback, Children, Component, Context, Html, NodeRef, Properties}; -use crate::{configuration::ConfigurationProvider, mouse_position, results::filters::Filter, PREVENT_DEFAULT_DRAG_OVER}; +use crate::{mouse_position, results::filters::Filter, state::StateProvider, PREVENT_DEFAULT_DRAG_OVER}; pub enum Msg { OnDragStart(usize, usize), @@ -291,8 +291,8 @@ pub struct ExistingFilterProps { #[function_component] pub fn ExistingFilter(props: &ExistingFilterProps) -> Html { - let cfg = use_context::>().unwrap(); - let graph = cfg.config.parser.as_ref().and_then(|p| p.graph.as_ref()); + let data = use_context::>().unwrap(); + let graph = data.state.parser.as_ref().and_then(|p| p.graph.as_ref()); let fc = |i| graph.as_ref().map(|g| { *g.borrow().raw[i].kind() }).unwrap(); diff --git a/axiom-profiler-GUI/src/filters/mod.rs b/axiom-profiler-GUI/src/filters/mod.rs index 626ef669..7482007d 100644 --- a/axiom-profiler-GUI/src/filters/mod.rs +++ b/axiom-profiler-GUI/src/filters/mod.rs @@ -1,7 +1,7 @@ mod add_filter; mod manage_filter; -use std::fmt::Display; +use std::{borrow::Borrow, fmt::Display}; use gloo::console::log; use material_yew::icon::MatIcon; @@ -9,7 +9,7 @@ use petgraph::Direction; use smt_log_parser::parsers::{z3::graph::{raw::NodeKind, RawNodeIndex}, ParseState}; use yew::{html, Callback, Component, Context, Html, MouseEvent, NodeRef, Properties}; -use crate::{configuration::ConfigurationContext, filters::{add_filter::AddFilterSidebar, manage_filter::{DraggableList, ExistingFilter}}, infobars::SidebarSectionHeader, results::{filters::{Disabler, Filter, DEFAULT_DISABLER_CHAIN, DEFAULT_FILTER_CHAIN}, svg_result::Msg as SVGMsg}, utils::{indexer::Indexer, toggle_list::ToggleList}, OpenedFileInfo, SIZE_NAMES}; +use crate::{filters::{add_filter::AddFilterSidebar, manage_filter::{DraggableList, ExistingFilter}}, infobars::SidebarSectionHeader, results::{filters::{Disabler, Filter, DEFAULT_DISABLER_CHAIN, DEFAULT_FILTER_CHAIN}, svg_result::Msg as SVGMsg}, state::StateContext, utils::toggle_list::ToggleList, OpenedFileInfo, RcParser, SIZE_NAMES}; use self::manage_filter::DragState; use material_yew::WeakComponentLink; @@ -160,9 +160,9 @@ impl Component for FiltersState { modified = true; } if let Filter::SelectNthMatchingLoop(n) = &filter { - // TODO: re-add finding matching loops - let graph = &ctx.props().file.parser.graph; - if !graph.as_ref().is_some_and(|g| (& *g.borrow()).found_matching_loops().is_some_and(|mls| mls > *n)) { + let state = ctx.link().get_state().unwrap(); + let graph = &state.state.parser.as_ref().unwrap().graph; + if !graph.as_ref().is_some_and(|g| (**g).borrow().found_matching_loops().is_some_and(|mls| mls > *n)) { return modified; } } @@ -171,10 +171,10 @@ impl Component for FiltersState { } Msg::AddFilter(edit, filter) => { if let Filter::SelectNthMatchingLoop(n) = &filter { - // TODO: re-add finding matching loops - let graph = &ctx.props().file.parser.graph; + let state = ctx.link().get_state().unwrap(); + let graph = &state.state.parser.as_ref().unwrap().graph; // This relies on the fact that the graph is updated before the `AddFilter` is - if !graph.as_ref().is_some_and(|g| g.borrow().found_matching_loops().is_some_and(|mls| mls > *n)) { + if !graph.as_ref().is_some_and(|g| (**g).borrow().found_matching_loops().is_some_and(|mls| mls > *n)) { return false; } } @@ -193,30 +193,32 @@ impl Component for FiltersState { }, Msg::ToggleMlViewerMode => { let search_matching_loops = ctx.props().search_matching_loops.clone(); - let found_mls = ctx.props().file.parser.found_mls; + + let state = ctx.link().get_state().unwrap(); + let found_mls = &state.state.parser.as_ref().unwrap().found_mls; if let None = found_mls { search_matching_loops.emit(()); } - let link = ctx.link().clone(); - let cfg = link.get_configuration().unwrap(); - cfg.update.update(|cfg| { cfg.persistent.ml_viewer_mode = !cfg.persistent.ml_viewer_mode; true }); + state.set_ml_viewer_mode(!state.state.ml_viewer_mode); true } } } fn view(&self, ctx: &Context) -> Html { + let data = ctx.link().get_state().unwrap(); + let info = data.state.file_info.as_ref().unwrap(); let file = &ctx.props().file; - let (size, unit) = file_size_display(file.file_size); + let (size, unit) = file_size_display(info.size); let details = match &file.parser_state { ParseState::Paused(_, state) => { let (parse_size, parse_unit) = file_size_display(state.bytes_read as u64); - format!("{} ({parse_size} {parse_unit}/{size} {unit})", file.file_name) + format!("{} ({parse_size} {parse_unit}/{size} {unit})", info.name) } ParseState::Completed { .. } => - format!("{} ({size} {unit})", file.file_name), + format!("{} ({size} {unit})", info.name), ParseState::Error(err) => - format!("{} (error {err:?})", file.file_name), + format!("{} (error {err:?})", info.name), }; // Existing ops let elem_hashes: Vec<_> = self.filter_chain.iter().map(Filter::get_hash).collect(); @@ -231,13 +233,14 @@ impl Component for FiltersState { }).collect(); let drag = ctx.link().callback(Msg::Drag); let will_delete = ctx.link().callback(Msg::WillDelete); - // TODO: re-add finding matching loops - let found_mls = ctx.props().file.parser.found_mls; + + let state = ctx.link().get_state().unwrap(); + let found_mls = &state.state.parser.as_ref().unwrap().found_mls; 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 { + let ml_viewer_mode = if state.state.ml_viewer_mode { html! {
  • {"close"}
    {"Exit matching loop viewer"}
  • } @@ -292,8 +295,7 @@ impl Component for FiltersState { }; let graph_details = file.rendered.as_ref().map(|g| { let class = if self.dragging { "hidden" } else { "" }; - // TODO: re-add finding matching loops - let mls = ctx.props().file.parser.found_mls.map(|mls| format!(", {mls} mtch loops")).unwrap_or_default(); + let mls = found_mls.map(|mls| format!(", {mls} mtch loops")).unwrap_or_default(); let details = format!("{} nodes, {} edges{mls}", g.graph.graph.node_count(), g.graph.graph.edge_count()); html! {
  • {details}
  • } }); diff --git a/axiom-profiler-GUI/src/infobars/omnibox/mod.rs b/axiom-profiler-GUI/src/infobars/omnibox/mod.rs index 942c92dd..6889106e 100644 --- a/axiom-profiler-GUI/src/infobars/omnibox/mod.rs +++ b/axiom-profiler-GUI/src/infobars/omnibox/mod.rs @@ -113,9 +113,7 @@ impl Component for Omnibox { } } fn changed(&mut self, ctx: &Context, old_props: &Self::Properties) -> bool { - if ctx.props() == old_props { - return false; - } + debug_assert!(ctx.props() != old_props); if ctx.props().progress != old_props.progress { self.focused = false; self.command_mode = false; diff --git a/axiom-profiler-GUI/src/infobars/topbar.rs b/axiom-profiler-GUI/src/infobars/topbar.rs index 58582aaa..047d7fa8 100644 --- a/axiom-profiler-GUI/src/infobars/topbar.rs +++ b/axiom-profiler-GUI/src/infobars/topbar.rs @@ -2,7 +2,7 @@ use material_yew::linear_progress::MatLinearProgress; use smt_log_parser::parsers::z3::graph::RawNodeIndex; use yew::{function_component, html, use_context, Callback, Html, NodeRef, Properties}; -use crate::{configuration::ConfigurationProvider, infobars::{ml_omnibox::MlOmnibox, Omnibox, SearchActionResult}, utils::lookup::Kind, LoadingState}; +use crate::{configuration::ConfigurationProvider, infobars::{ml_omnibox::MlOmnibox, Omnibox, SearchActionResult}, state::StateProvider, utils::lookup::Kind, LoadingState}; #[derive(Debug, Clone, PartialEq)] pub struct OmnibarMessage { @@ -18,7 +18,6 @@ pub struct TopbarProps { pub search: Callback>, pub pick: Callback<(String, Kind), Option>>, pub select: Callback, - pub found_mls: Option, pub pick_nth_ml: Callback, } @@ -60,10 +59,11 @@ pub fn Topbar(props: &TopbarProps) -> Html { closed = false; indeterminate = false; } - let ml_viewer_mode = use_context:: >().expect("no ctx found"); - let omnibox = if ml_viewer_mode.config.persistent.ml_viewer_mode { + let state = use_context::>().expect("no ctx found"); + let omnibox = if state.state.ml_viewer_mode { + let found_mls = state.state.parser.as_ref().unwrap().found_mls.unwrap(); html! { - + } } else { html! { diff --git a/axiom-profiler-GUI/src/lib.rs b/axiom-profiler-GUI/src/lib.rs index 00621c1f..75fd21fa 100644 --- a/axiom-profiler-GUI/src/lib.rs +++ b/axiom-profiler-GUI/src/lib.rs @@ -22,6 +22,7 @@ use yew::prelude::*; use material_yew::{MatIcon, MatIconButton, MatDialog, WeakComponentLink}; use crate::commands::CommandsProvider; +use crate::state::{StateContext, StateProviderContext}; use crate::configuration::{ConfigurationContext, ConfigurationProvider, Flags}; use crate::filters::FiltersState; use crate::infobars::{OmnibarMessage, SearchActionResult, SidebarSectionHeader, Topbar}; @@ -43,6 +44,7 @@ pub mod homepage; pub mod shortcuts; pub mod commands; pub mod file; +pub mod state; pub const GIT_DESCRIBE: &str = env!("VERGEN_GIT_DESCRIBE"); pub fn version() -> Option { @@ -61,7 +63,7 @@ pub static PREVENT_DEFAULT_DRAG_OVER: OnceLock> = OnceLock::new(); pub enum Msg { File(Option), - LoadedFile(String, u64, Z3Parser, ParseState, bool), + LoadedFile(Z3Parser, ParseState, bool), LoadingState(LoadingState), RenderedGraph(RenderedGraph), FailedOpening(String), @@ -126,8 +128,6 @@ impl ParseProgress { #[derive(Clone)] pub struct OpenedFileInfo { - file_name: String, - file_size: u64, parser_state: ParseState, parser_cancelled: bool, update: Rc, Vec>>>, @@ -135,14 +135,11 @@ pub struct OpenedFileInfo { selected_nodes: Vec, selected_edges: Vec, rendered: Option, - parser: RcParser, } impl PartialEq for OpenedFileInfo { fn eq(&self, other: &Self) -> bool { - self.file_name == other.file_name - && self.file_size == other.file_size - && std::mem::discriminant(&self.parser_state) == std::mem::discriminant(&other.parser_state) + std::mem::discriminant(&self.parser_state) == std::mem::discriminant(&other.parser_state) && self.selected_nodes == other.selected_nodes && self.selected_edges == other.selected_edges && self.rendered.as_ref().map(|r| r.graph.generation) == other.rendered.as_ref().map(|r| r.graph.generation) @@ -304,10 +301,10 @@ impl Component for FileDataComponent { let Some(file) = file else { return false; }; - // remove any old parser in the configuration - let cfg = ctx.link().get_configuration().unwrap(); - cfg.update_parser(|p| p.take().is_some()); - cfg.reset_ml_viewer_mode(); + // remove any old parser in the state + let state = ctx.link().get_state().unwrap(); + state.update_parser(|p| p.take().is_some()); + state.set_ml_viewer_mode(false); // hide the flags page if shown self.flags_visible.borrow().emit(Some(false)); @@ -367,8 +364,9 @@ impl Component for FileDataComponent { self.progress = LoadingState::NoFileSelected; let file = self.file.take(); drop(file); - let cfg = ctx.link().get_configuration().unwrap(); - cfg.update_parser(|p| p.take().is_some()); + let state = ctx.link().get_state().unwrap(); + state.update_file_info(|fi| fi.take().is_some()); + state.update_parser(|p| p.take().is_some()); if let Some(navigation_section) = self.navigation_section.cast::() { let _ = navigation_section.class_list().add_1("expanded"); @@ -383,19 +381,15 @@ impl Component for FileDataComponent { self.message.take(); true } - Msg::LoadedFile(file_name, file_size, parser, parser_state, parser_cancelled) => { - log::info!("Processing \"{file_name}\""); + Msg::LoadedFile(parser, parser_state, parser_cancelled) => { drop(self.reader.take()); let parser = RcParser::new(parser); - let rc_parser = parser.clone(); - let cfg = ctx.link().get_configuration().unwrap(); - cfg.update_parser(move |p| { - *p = Some(rc_parser); + let state = ctx.link().get_state().unwrap(); + state.update_parser(move |p| { + *p = Some(parser); true }); let file = OpenedFileInfo { - file_name, - file_size, parser_state, parser_cancelled, filter: WeakComponentLink::default(), @@ -403,7 +397,6 @@ impl Component for FileDataComponent { selected_nodes: Vec::new(), selected_edges: Vec::new(), rendered: None, - parser, }; self.file = Some(file); if let Some(navigation_section) = self.navigation_section.cast::() { @@ -466,44 +459,17 @@ impl Component for FileDataComponent { Msg::SearchMatchingLoops => { log::info!("Searching matching loops"); if let Some(file) = &mut self.file { - // TODO: re-add finding matching loops - // assert!(file.parser.graph.is_some()); - // let parser = ctx.link().get_configuration().unwrap().config.parser.unwrap(); - // let tmp = ctx.link().get_configuration().unwrap().config.parser.unwrap().clone(); - // let mut parser = tmp.parser.borrow_mut(); - // file.parser = ctx.link().get_configuration().unwrap().config.parser.unwrap().clone(); - let cfg = ctx.link().get_configuration().unwrap(); - let parser = cfg.config.parser.as_ref().unwrap(); - file.parser = parser.clone(); - if let Some(g) = &file.parser.graph { - file.parser.found_mls = Some((&mut *g.borrow_mut()) - // .search_matching_loops(&mut *parser)) - .search_matching_loops(&mut *file.parser.parser.borrow_mut())) + let state = ctx.link().get_state().unwrap(); + let parser = state.state.parser.as_ref().unwrap(); + if let Some(g) = &parser.graph { + let found_mls = Some((&mut *g.borrow_mut()) + .search_matching_loops(&mut *parser.parser.borrow_mut())); + state.update_parser(move |p| { + p.as_mut().unwrap().found_mls = found_mls; + true + }); + return true; } - return true; - // file.parser.found_mls = Some( - // &file - // .parser - // .graph - // .unwrap() - // .borrow_mut() - // .deref_mut() - // .search_matching_loops() - // ); - // assert!(parser.graph.is_some()); - // if let Some(g) = &file - // .parser - // .graph - // // .borrow_mut() - // // .as_mut() - // { - // file.parser.found_mls = Some(g - // .borrow_mut() - // .deref_mut() - // .search_matching_loops()); - // log::info!("Returning true"); - // return true; - // } } log::info!("Returning false"); false @@ -539,8 +505,14 @@ impl Component for FileDataComponent { None => html!{}, }; - let cfg = ctx.link().get_configuration().unwrap(); - let parser = cfg.config.parser.clone(); + let link = ctx.link().clone(); + let flags_visible_changed = Callback::from(move |visible| { + let data = link.get_state().unwrap(); + data.set_overlay_visible(visible); + }); + + let data = ctx.link().get_state().unwrap(); + let parser = data.state.parser.clone(); let parser_ref = parser.clone(); let visible = self.file.as_ref().and_then(|f| f.rendered.as_ref().map(|r| r.graph.clone())); let visible_ref = visible.clone(); @@ -569,13 +541,12 @@ impl Component for FileDataComponent { let pick_nth_ml = Callback::from({ let file = self.file.clone(); move |n: usize| { - if let Some(found_mls) = file.as_ref().and_then(|file| file.parser.found_mls) { let Some(filters_state_link) = &*filters_state_link.borrow() else { return; }; filters_state_link.send_message(crate::filters::Msg::AddFilter(false, Filter::SelectNthMatchingLoop(n))); } - }}); + }); // Callbacks let file_select_ref = self.file_select.clone(); @@ -641,18 +612,18 @@ impl Component for FileDataComponent {
    - +
    {page} - +
    // Shortcuts dialog @@ -683,11 +654,9 @@ impl Component for FileDataComponent { #[function_component(App)] pub fn app() -> Html { html! { -
    - +
    - -
    +
    } } diff --git a/axiom-profiler-GUI/src/results/filters.rs b/axiom-profiler-GUI/src/results/filters.rs index f87406a9..e0db4d0f 100644 --- a/axiom-profiler-GUI/src/results/filters.rs +++ b/axiom-profiler-GUI/src/results/filters.rs @@ -34,7 +34,7 @@ pub enum Filter { } impl Filter { - pub fn apply(self, graph: &mut InstGraph, parser: &Z3Parser, config: &DisplayConfiguration) -> FilterOutput { + pub fn apply<'a>(self, graph: &mut InstGraph, parser: &'a Z3Parser, config: impl FnOnce(&'a Z3Parser) -> DisplayCtxt<'a>) -> FilterOutput { match self { Filter::MaxNodeIdx(max) => graph.raw.set_visibility_when(true, |idx: RawNodeIndex, _: &Node| idx.0.index() >= max), Filter::MinNodeIdx(min) => graph.raw.set_visibility_when(true, |idx: RawNodeIndex, _: &Node| idx.0.index() < min), @@ -63,7 +63,7 @@ impl Filter { Filter::ShowLongestPath(nidx) => return FilterOutput::LongestPath(graph.raw.show_longest_path_through(nidx)), Filter::ShowNamedQuantifier(name) => { - let ctxt = DisplayCtxt { parser, config: config.clone() }; + let ctxt = config(parser); graph.raw.set_visibility_when(false, |_: RawNodeIndex, node: &Node| node.kind().inst().is_some_and(|i| parser[parser[i].match_].kind.quant_idx().map(|q| parser[q].kind.with(&ctxt).to_string()).is_some_and(|s| s == name) )) diff --git a/axiom-profiler-GUI/src/results/graph/graph_container.rs b/axiom-profiler-GUI/src/results/graph/graph_container.rs index b73eafdf..822e4074 100644 --- a/axiom-profiler-GUI/src/results/graph/graph_container.rs +++ b/axiom-profiler-GUI/src/results/graph/graph_container.rs @@ -10,6 +10,7 @@ use material_yew::WeakComponentLink; use crate::commands::{Command, CommandRef, CommandsContext}; use crate::results::svg_result::RenderedGraph; +use crate::state::StateContext; use crate::{CallbackRef, GlobalCallbacksContext, PagePosition, PrecisePosition}; use super::svg_graph::{Graph, Svg}; @@ -183,9 +184,7 @@ impl Component for GraphContainer { Self { graph, mouse_closures: None, resize_observer: None, drag_start: None, window: GraphWindow::default(), zoom_factor: 1.0, zoom_factor_delta: 1.0, zoom_with_mouse: false, held_keys, timeout: None, _callback_refs, _command_selection, _command_refs } } fn changed(&mut self, ctx: &Context, old_props: &Self::Properties) -> bool { - if ctx.props() == old_props { - return false; - } + debug_assert!(ctx.props() != old_props); self.zoom_factor_delta = 1.0; if self.graph.as_ref().map(|g| g.1) != ctx.props().rendered.as_ref().map(|r| r.graph.generation) { self.graph = ctx.props().rendered.as_ref().map(|r| (Html::from_html_unchecked(r.svg_text.clone()), r.graph.generation)); @@ -280,6 +279,10 @@ impl Component for GraphContainer { false } Msg::KeyDown(ev) => { + if ctx.link().get_state().unwrap().state.overlay_visible { + return false; + } + let key = ev.key(); let plain = !ev.meta_key() && !ev.ctrl_key() && !ev.shift_key() && !ev.alt_key(); match key.as_str() { @@ -320,6 +323,10 @@ impl Component for GraphContainer { false } Msg::KeyHold(()) => { + if ctx.link().get_state().unwrap().state.overlay_visible { + return false; + } + let mut delta = PrecisePosition::default(); let mut dz = 0.0; self.held_keys.retain(|key, (time, moved, released)| { diff --git a/axiom-profiler-GUI/src/results/graph/svg_graph.rs b/axiom-profiler-GUI/src/results/graph/svg_graph.rs index dbcbfb40..f08d25fa 100644 --- a/axiom-profiler-GUI/src/results/graph/svg_graph.rs +++ b/axiom-profiler-GUI/src/results/graph/svg_graph.rs @@ -31,9 +31,7 @@ pub struct GraphProps { #[function_component] pub fn Graph(props: &GraphProps) -> Html { - let Some(rendered) = &props.rendered else { - return html! {} - }; + let generation = props.rendered.as_ref().map(|r| r.graph.generation); let div_ref = use_node_ref(); { @@ -46,7 +44,10 @@ pub fn Graph(props: &GraphProps) -> Html { let scroll_window = props.scroll_window.clone(); let set_scroll = props.set_scroll.clone(); use_effect_with_deps( - move |&(_, zoom_factor)| { + move |&(generation, zoom_factor)| { + if generation.is_none() { + return; + } let div = div_ref .cast::() .expect("div_ref not attached to div element"); @@ -104,7 +105,7 @@ pub fn Graph(props: &GraphProps) -> Html { set_scroll.emit((new_scroll, graph_dims)); } }, - (rendered.graph.generation, zoom_factor), + (generation, zoom_factor), ) } @@ -114,7 +115,10 @@ pub fn Graph(props: &GraphProps) -> Html { let selected_nodes: FxHashSet<_> = props.selected_nodes.iter().copied().collect(); use_effect_with_deps( - move |(_, selected_nodes)| { + move |(generation, selected_nodes)| { + if generation.is_none() { + return; + } let div = div_ref .cast::() .expect("div_ref not attached to div element"); @@ -131,7 +135,7 @@ pub fn Graph(props: &GraphProps) -> Html { } } }, - (rendered.graph.generation, selected_nodes), + (generation, selected_nodes), ); } @@ -141,7 +145,10 @@ pub fn Graph(props: &GraphProps) -> Html { let selected_edges: FxHashSet<_> = props.selected_edges.iter().copied().collect(); use_effect_with_deps( - move |(_, selected_edges)| { + move |(generation, selected_edges)| { + if generation.is_none() { + return; + } let div = div_ref .cast::() .expect("div_ref not attached to div element"); @@ -158,7 +165,7 @@ pub fn Graph(props: &GraphProps) -> Html { } } }, - (rendered.graph.generation, selected_edges), + (generation, selected_edges), ); } @@ -168,143 +175,151 @@ pub fn Graph(props: &GraphProps) -> Html { let div_ref = div_ref.clone(); use_effect_with_deps( - move |_| { - let div = div_ref - .cast::() - .expect("div_ref not attached to div element"); + move |generation| { + let (nodes, edges) = if generation.is_some() { + let div = div_ref + .cast::() + .expect("div_ref not attached to div element"); - // construct event_listeners that emit node indices (contained in title tags) - let descendant_nodes = div.get_elements_by_class_name("node"); - let node_closures: Vec<_> = (0..descendant_nodes.length()) - .map(|i| { - // extract node_index from node to construct callback that emits it - let node = descendant_nodes.item(i).unwrap(); - // Create a duplicate of the node which is transparent - // to make it more clickable, especially when it gets - // gets selected and the original node becomes larger. - let node_shape = node.get_elements_by_tag_name("polygon").item(0) - .or_else(|| node.get_elements_by_tag_name("ellipse").item(0)); - if let Some(node_shape) = node_shape { - if let Some(parent) = node_shape.parent_node() { - if let Some(duplicate) = node_shape.clone_node().ok().and_then(|e| e.dyn_into::().ok()) { - let _ = parent.append_child(&duplicate); - duplicate.set_attribute("stroke-width", "5").unwrap(); - duplicate.set_attribute("stroke", "transparent").unwrap(); - duplicate.set_attribute("fill", "transparent").unwrap(); + // construct event_listeners that emit node indices (contained in title tags) + let descendant_nodes = div.get_elements_by_class_name("node"); + let node_closures: Vec<_> = (0..descendant_nodes.length()) + .map(|i| { + // extract node_index from node to construct callback that emits it + let node = descendant_nodes.item(i).unwrap(); + // Create a duplicate of the node which is transparent + // to make it more clickable, especially when it gets + // gets selected and the original node becomes larger. + let node_shape = node.get_elements_by_tag_name("polygon").item(0) + .or_else(|| node.get_elements_by_tag_name("ellipse").item(0)); + if let Some(node_shape) = node_shape { + if let Some(parent) = node_shape.parent_node() { + if let Some(duplicate) = node_shape.clone_node().ok().and_then(|e| e.dyn_into::().ok()) { + let _ = parent.append_child(&duplicate); + duplicate.set_attribute("stroke-width", "5").unwrap(); + duplicate.set_attribute("stroke", "transparent").unwrap(); + duplicate.set_attribute("fill", "transparent").unwrap(); + } } } - } - let idx = node.id().strip_prefix("node_").unwrap().parse::(); - let idx = RawNodeIndex(NodeIndex::new(idx.unwrap())); - // attach event listener to node - let callback = nodes_callback.clone(); - let mousedown: Closure = Closure::new(move |e: Event| { - e.cancel_bubble(); e.stop_propagation(); - callback.emit(idx); - }); - node.add_event_listener_with_callback( - "mousedown", - mousedown.as_ref().unchecked_ref(), - ).unwrap(); - let callback = nodes_callback.clone(); - let mouseover: Closure = Closure::new(move |e: Event| { - if e.dyn_into::().is_ok_and(|e| e.buttons() == 1 && e.shift_key()) { - callback.emit(idx) - } - }); - node.add_event_listener_with_callback( - "mouseover", - mouseover.as_ref().unchecked_ref(), - ).unwrap(); - (mousedown, mouseover) - }) - .collect(); - let direct_edges = div.get_elements_by_class_name("edge"); - let edge_closures: Vec<_> = (0..direct_edges.length()) - .map(|i| { - // extract edge_index from edge to construct callback that emits it - let edge = direct_edges.item(i).unwrap(); - // Create a duplicate of the edge which is transparent - // to make it more clickable. - let mut edge_hover_select = edge.clone(); - if let Some(edge_path) = edge.get_elements_by_tag_name("path").item(0) { - if let Some(parent) = edge_path.parent_node() { - if let Some(duplicate) = edge_path.clone_node().ok().and_then(|e| e.dyn_into::().ok()) { - let _ = parent.append_child(&duplicate); - duplicate.set_attribute("stroke-width", "15").unwrap(); - duplicate.set_attribute("stroke", "transparent").unwrap(); - duplicate.remove_attribute("stroke-dasharray").ok(); - edge_hover_select = duplicate; - } - } - } - let idx = edge.id().strip_prefix("edge_").unwrap().parse::(); - let idx = VisibleEdgeIndex(EdgeIndex::new(idx.unwrap())); - // attach event listener to edge - let callback = edges_callback.clone(); - let mousedown: Closure = Closure::new(move |e: Event| { - e.cancel_bubble(); e.stop_propagation(); - callback.emit(idx); - }); - edge.add_event_listener_with_callback( - "mousedown", - mousedown.as_ref().unchecked_ref(), - ).unwrap(); - let callback = edges_callback.clone(); - let mouseover: Closure = Closure::new(move |e: Event| - if e.dyn_into::().is_ok_and(|e| e.buttons() == 1 && e.shift_key()) { - callback.emit(idx) - } - ); - // Attach this event only to the edge and not the whole - // `edge` (including the arrowhead) because then we get - // two mousover events when moving from path to arrowhead. - edge_hover_select.add_event_listener_with_callback( - "mouseover", - mouseover.as_ref().unchecked_ref(), - ).unwrap(); - (mousedown, mouseover, edge_hover_select) - }) - .collect(); - move || { - for i in 0..node_closures.len() { - if let Some(node) = descendant_nodes.item(i as u32) { - let (mousedown, mouseover) = &node_closures[i]; - node.remove_event_listener_with_callback( + let idx = node.id().strip_prefix("node_").unwrap().parse::(); + let idx = RawNodeIndex(NodeIndex::new(idx.unwrap())); + // attach event listener to node + let callback = nodes_callback.clone(); + let mousedown: Closure = Closure::new(move |e: Event| { + e.cancel_bubble(); e.stop_propagation(); + callback.emit(idx); + }); + node.add_event_listener_with_callback( "mousedown", mousedown.as_ref().unchecked_ref(), ).unwrap(); - node.remove_event_listener_with_callback( + let callback = nodes_callback.clone(); + let mouseover: Closure = Closure::new(move |e: Event| { + if e.dyn_into::().is_ok_and(|e| e.buttons() == 1 && e.shift_key()) { + callback.emit(idx) + } + }); + node.add_event_listener_with_callback( "mouseover", mouseover.as_ref().unchecked_ref(), ).unwrap(); - } - } - for i in 0..edge_closures.len() { - if let Some(edge) = direct_edges.item(i as u32) { - let (mousedown, mouseover, edge_hover_select) = &edge_closures[i]; - edge.remove_event_listener_with_callback( + (mousedown, mouseover) + }) + .collect(); + let direct_edges = div.get_elements_by_class_name("edge"); + let edge_closures: Vec<_> = (0..direct_edges.length()) + .map(|i| { + // extract edge_index from edge to construct callback that emits it + let edge = direct_edges.item(i).unwrap(); + // Create a duplicate of the edge which is transparent + // to make it more clickable. + let mut edge_hover_select = edge.clone(); + if let Some(edge_path) = edge.get_elements_by_tag_name("path").item(0) { + if let Some(parent) = edge_path.parent_node() { + if let Some(duplicate) = edge_path.clone_node().ok().and_then(|e| e.dyn_into::().ok()) { + let _ = parent.append_child(&duplicate); + duplicate.set_attribute("stroke-width", "15").unwrap(); + duplicate.set_attribute("stroke", "transparent").unwrap(); + duplicate.remove_attribute("stroke-dasharray").ok(); + edge_hover_select = duplicate; + } + } + } + let idx = edge.id().strip_prefix("edge_").unwrap().parse::(); + let idx = VisibleEdgeIndex(EdgeIndex::new(idx.unwrap())); + // attach event listener to edge + let callback = edges_callback.clone(); + let mousedown: Closure = Closure::new(move |e: Event| { + e.cancel_bubble(); e.stop_propagation(); + callback.emit(idx); + }); + edge.add_event_listener_with_callback( "mousedown", mousedown.as_ref().unchecked_ref(), ).unwrap(); - edge_hover_select.remove_event_listener_with_callback( + let callback = edges_callback.clone(); + let mouseover: Closure = Closure::new(move |e: Event| + if e.dyn_into::().is_ok_and(|e| e.buttons() == 1 && e.shift_key()) { + callback.emit(idx) + } + ); + // Attach this event only to the edge and not the whole + // `edge` (including the arrowhead) because then we get + // two mousover events when moving from path to arrowhead. + edge_hover_select.add_event_listener_with_callback( "mouseover", mouseover.as_ref().unchecked_ref(), ).unwrap(); + (mousedown, mouseover, edge_hover_select) + }) + .collect(); + (Some((descendant_nodes, node_closures)), Some((direct_edges, edge_closures))) + } else { + (None, None) + }; + move || { + if let Some((descendant_nodes, node_closures)) = nodes { + for i in 0..node_closures.len() { + if let Some(node) = descendant_nodes.item(i as u32) { + let (mousedown, mouseover) = &node_closures[i]; + node.remove_event_listener_with_callback( + "mousedown", + mousedown.as_ref().unchecked_ref(), + ).unwrap(); + node.remove_event_listener_with_callback( + "mouseover", + mouseover.as_ref().unchecked_ref(), + ).unwrap(); + } + } + } + if let Some((direct_edges, edge_closures)) = edges { + for i in 0..edge_closures.len() { + if let Some(edge) = direct_edges.item(i as u32) { + let (mousedown, mouseover, edge_hover_select) = &edge_closures[i]; + edge.remove_event_listener_with_callback( + "mousedown", + mousedown.as_ref().unchecked_ref(), + ).unwrap(); + edge_hover_select.remove_event_listener_with_callback( + "mouseover", + mouseover.as_ref().unchecked_ref(), + ).unwrap(); + } } } } }, - rendered.graph.generation, + generation, ); } - html! { - <> + + generation.map(|_| html! {
    {props.children.clone()}
    - - } + }).unwrap_or_default() } #[derive(Properties)] diff --git a/axiom-profiler-GUI/src/results/graph_info.rs b/axiom-profiler-GUI/src/results/graph_info.rs index aa4ea2a3..6abecfcc 100644 --- a/axiom-profiler-GUI/src/results/graph_info.rs +++ b/axiom-profiler-GUI/src/results/graph_info.rs @@ -1,6 +1,6 @@ use std::rc::Rc; -use crate::{configuration::{ConfigurationContext, ConfigurationProvider}, utils::split_div::SplitDiv}; +use crate::{configuration::{Configuration, ConfigurationContext, ConfigurationProvider}, state::StateProvider, utils::split_div::SplitDiv, RcParser}; use indexmap::map::{Entry, IndexMap}; use material_yew::WeakComponentLink; // use smt_log_parser::parsers::z3::inst_graph::{EdgeType, NodeInfo}; @@ -16,7 +16,7 @@ pub struct GraphInfo { graph_container: WeakComponentLink, displayed_matching_loop_graph: Option, in_ml_viewer_mode: bool, - _context_listener: ContextHandle>, + _context_listener: ContextHandle>, } fn toggle_selected(map: &mut IndexMap, entry: T) -> Vec { @@ -54,7 +54,7 @@ pub enum Msg { SelectAll, ShowGeneralizedTerms(Vec), ShowMatchingLoopGraph(AttrValue), - ContextUpdated(Rc), + ContextUpdated(Rc), } #[derive(Properties, PartialEq)] @@ -81,7 +81,7 @@ impl Component for GraphInfo { .weak_link .borrow_mut() .replace(ctx.link().clone()); - let (msg, context_listener) = ctx + let (state, context_listener) = ctx .link() .context(ctx.link().callback(Msg::ContextUpdated)) .expect("No message context provided"); @@ -91,7 +91,7 @@ impl Component for GraphInfo { generalized_terms: Vec::new(), graph_container: WeakComponentLink::default(), displayed_matching_loop_graph: None, - in_ml_viewer_mode: msg.config.persistent.ml_viewer_mode, + in_ml_viewer_mode: state.state.ml_viewer_mode, _context_listener: context_listener, } } @@ -172,8 +172,8 @@ impl Component for GraphInfo { false } Msg::ContextUpdated(msg) => { - if self.in_ml_viewer_mode != msg.config.persistent.ml_viewer_mode { - self.in_ml_viewer_mode = msg.config.persistent.ml_viewer_mode; + if self.in_ml_viewer_mode != msg.state.ml_viewer_mode { + self.in_ml_viewer_mode = msg.state.ml_viewer_mode; true } else { false @@ -191,7 +191,6 @@ impl Component for GraphInfo { let link = ctx.link().clone(); Callback::from(move |edge: VisibleEdgeIndex| link.send_message(Msg::ToggleOpenEdge(edge))) }; - let _ignore_term_ids = !ctx.link().get_configuration().unwrap().config.persistent.display.display_term_ids; let on_node_select = ctx.link().callback(Msg::UserSelectedNode); let on_edge_select = ctx.link().callback(Msg::UserSelectedEdge); let deselect_all = ctx.link().callback(|_| Msg::DeselectAll); diff --git a/axiom-profiler-GUI/src/results/node_info.rs b/axiom-profiler-GUI/src/results/node_info.rs index 854c2ef9..ad44218c 100644 --- a/axiom-profiler-GUI/src/results/node_info.rs +++ b/axiom-profiler-GUI/src/results/node_info.rs @@ -3,7 +3,7 @@ use std::rc::Rc; use smt_log_parser::{display_with::{DisplayCtxt, DisplayWithCtxt}, items::{MatchKind, VarNames}, parsers::z3::graph::{raw::{EdgeKind, Node, NodeKind}, visible::{VisibleEdge, VisibleEdgeKind}, InstGraph, RawNodeIndex, VisibleEdgeIndex}, NonMaxU32}; use yew::{function_component, html, use_context, AttrValue, Callback, Html, MouseEvent, Properties}; -use crate::configuration::ConfigurationProvider; +use crate::{configuration::ConfigurationProvider, state::StateProvider}; use super::svg_result::RenderedGraph; @@ -59,6 +59,7 @@ impl<'a, 'b> NodeInfo<'a, 'b> { pub fn tooltip(&self, html: bool, char_limit: Option) -> String { let mut ctxt = DisplayCtxt { parser: self.ctxt.parser, + term_display: self.ctxt.term_display, config: self.ctxt.config.clone(), }; ctxt.config.html = html; @@ -98,10 +99,11 @@ impl<'a, 'b> NodeInfo<'a, 'b> { return None }; let match_ = &self.ctxt.parser[self.ctxt.parser[inst].match_]; + let mut qidx = match_.kind.quant_idx(); let pattern = match_.kind.pattern()?; let trigger_matches = self.ctxt.parser[pattern].child_ids.iter().rev().zip(match_.trigger_matches()); let mut blame: Vec<_> = trigger_matches.map(|(trigger, matched)| { - let trigger = trigger.with(self.ctxt).to_string(); + let trigger = trigger.with_data(self.ctxt, &mut qidx).to_string(); let enode = matched.enode().with(self.ctxt).to_string(); let equalities = matched.equalities().map(|eq| eq.with(self.ctxt).to_string()).collect(); (trigger, enode, equalities) @@ -156,18 +158,20 @@ pub fn SelectedNodesInfo( on_click, }: &SelectedNodesInfoProps, ) -> Html { + let cfg = use_context::>().unwrap(); + let data = use_context::>().unwrap(); + if selected_nodes.is_empty() { return html! {} } - - let cfg = use_context::>().unwrap(); - let parser = cfg.config.parser.as_ref().unwrap(); + let parser = data.state.parser.as_ref().unwrap(); let graph = parser.graph.as_ref().unwrap(); let parser = &*parser.parser; let graph = graph.borrow(); let ctxt = &DisplayCtxt { parser: &parser.borrow(), - config: cfg.config.persistent.display.clone(), + term_display: &data.state.term_display, + config: cfg.config.display.clone(), }; let infos = selected_nodes @@ -329,21 +333,23 @@ pub fn SelectedEdgesInfo( on_click, }: &SelectedEdgesInfoProps, ) -> Html { + let cfg = use_context::>().unwrap(); + let data = use_context::>().unwrap(); + if selected_edges.is_empty() { return html! {} } let Some(rendered) = rendered else { return html! {} }; - - let cfg = use_context::>().unwrap(); - let parser = cfg.config.parser.as_ref().unwrap(); + let parser = data.state.parser.as_ref().unwrap(); let graph = parser.graph.as_ref().unwrap(); let parser = &*parser.parser; let graph = graph.borrow(); let ctxt = &DisplayCtxt { parser: &parser.borrow(), - config: cfg.config.persistent.display.clone(), + term_display: &data.state.term_display, + config: cfg.config.display.clone(), }; let infos = selected_edges diff --git a/axiom-profiler-GUI/src/results/svg_result.rs b/axiom-profiler-GUI/src/results/svg_result.rs index 8ca1f2e7..5479f311 100644 --- a/axiom-profiler-GUI/src/results/svg_result.rs +++ b/axiom-profiler-GUI/src/results/svg_result.rs @@ -1,5 +1,5 @@ use crate::{ - configuration::ConfigurationContext, filters, results::{filters::FilterOutput, graph_info::{GraphInfo, Msg as GraphInfoMsg}, node_info::{EdgeInfo, NodeInfo}}, OpenedFileInfo + configuration::{Configuration, ConfigurationContext}, filters, results::{filters::FilterOutput, graph_info::{GraphInfo, Msg as GraphInfoMsg}, node_info::{EdgeInfo, NodeInfo}}, state::StateContext, OpenedFileInfo, RcParser }; use super::{ @@ -121,8 +121,8 @@ impl Component for SVGResult { let link = ctx.link().clone(); wasm_bindgen_futures::spawn_local(async move { gloo::timers::future::TimeoutFuture::new(10).await; - let cfg = link.get_configuration().unwrap(); - let parser = cfg.config.parser.as_ref().unwrap(); + let data = link.get_state().unwrap(); + let parser = data.state.parser.as_ref().unwrap(); let inst_graph = match InstGraph::new(&parser.parser.borrow()) { Ok(inst_graph) => inst_graph, Err(err) => { @@ -139,10 +139,10 @@ impl Component for SVGResult { }; let inst_graph = Rc::new(RefCell::new(inst_graph)); let inst_graph_ref = inst_graph.clone(); - cfg.update.update(|cfg| cfg.parser.as_mut().map(|p| { + data.update_graph(|p| { p.graph = Some(inst_graph_ref); true - }).unwrap_or_default()); + }); link.send_message(Msg::ConstructedGraph(inst_graph)); }); Self { @@ -185,8 +185,8 @@ impl Component for SVGResult { self.queue.push(msg); return false; }; - let cfg = ctx.link().get_configuration().unwrap(); - let rc_parser = cfg.config.parser.as_ref().unwrap(); + let data = ctx.link().get_state().unwrap(); + let rc_parser = data.state.parser.as_ref().unwrap(); let parser = &rc_parser.parser; let mut inst_graph = (**inst_graph).borrow_mut(); let inst_graph = &mut *inst_graph; @@ -196,7 +196,15 @@ impl Component for SVGResult { Msg::WorkerOutput(_out) => false, Msg::ApplyFilter(filter) => { log::debug!("Applying filter {:?}", filter); - match filter.apply(inst_graph, &parser.borrow(), &cfg.config.persistent.display) { + let config = |parser| { + let cfg = ctx.link().get_configuration().unwrap(); + DisplayCtxt { + parser, + term_display: &data.state.term_display, + config: cfg.config.display.clone(), + } + }; + match filter.apply(inst_graph, &parser.borrow(), config) { FilterOutput::LongestPath(path) => { ctx.props().selected_nodes.emit(path); // self.insts_info_link @@ -272,9 +280,11 @@ impl Component for SVGResult { self.async_graph_and_filter_chain = false; ctx.props().progress.emit(GraphState::Rendering(RenderingState::GraphToDot)); let filtered_graph = &calculated.graph; + let cfg = ctx.link().get_configuration().unwrap(); let ctxt = &DisplayCtxt { parser: &parser.borrow(), - config: cfg.config.persistent.display.clone(), + term_display: &data.state.term_display, + config: cfg.config.display.clone(), }; // Performance observations (default value is in []) @@ -425,9 +435,11 @@ impl Component for SVGResult { } Msg::RenderMLGraph(graph) => { let _filtered_graph = &graph; + let cfg = ctx.link().get_configuration().unwrap(); let _ctxt = &DisplayCtxt { parser: &parser.borrow(), - config: cfg.config.persistent.display.clone(), + term_display: &data.state.term_display, + config: cfg.config.display.clone(), }; // Performance observations (default value is in []) diff --git a/axiom-profiler-GUI/src/state/mod.rs b/axiom-profiler-GUI/src/state/mod.rs new file mode 100644 index 00000000..59ba5f8f --- /dev/null +++ b/axiom-profiler-GUI/src/state/mod.rs @@ -0,0 +1,148 @@ +use std::rc::Rc; + +use smt_log_parser::formatter::TermDisplayContext; +use yew::{html, Callback, Children, Component, Context, ContextHandle, ContextProvider, Html, Properties}; + +use crate::{configuration::{ConfigurationContext, ConfigurationProvider, TermDisplayContextFiles}, utils::updater::{Update, Updater}, RcParser}; + +// Public + +#[derive(Clone, Default, PartialEq)] +pub struct State { + pub file_info: Option, + /// Calculated automatically based on the set file_info. + pub term_display: TermDisplayContext, + pub parser: Option, + pub ml_viewer_mode: bool, + pub overlay_visible: bool, +} + +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, serde::Serialize, serde::Deserialize)] +pub struct FileInfo { + pub name: String, + pub size: u64, +} + +#[derive(Clone, PartialEq)] +pub struct StateProvider { + pub state: State, + update: Updater>, +} + +impl StateProvider { + pub fn update_file_info(&self, f: impl FnOnce(&mut Option) -> bool + 'static) { + self.update.update(|state| f(&mut state.file_info).then(|| StateUpdateKind::FileInfo)); + } + pub fn update_parser(&self, f: impl FnOnce(&mut Option) -> bool + 'static) { + self.update.update(|state| f(&mut state.parser).then(|| StateUpdateKind::Parser)); + } + pub fn update_graph(&self, f: impl FnOnce(&mut RcParser) -> bool + 'static) { + self.update.update(|state| state.parser.as_mut().map(f).unwrap_or_default().then(|| StateUpdateKind::Parser)); + } + + pub fn set_ml_viewer_mode(&self, ml_viewer_mode: bool) { + self.update.update(move |state| + (state.ml_viewer_mode != ml_viewer_mode).then(|| { + state.ml_viewer_mode = ml_viewer_mode; + StateUpdateKind::Other + }) + ); + } + pub fn set_overlay_visible(&self, overlay_visible: bool) { + self.update.update(move |state| + (state.overlay_visible != overlay_visible).then(|| { + state.overlay_visible = overlay_visible; + StateUpdateKind::Other + }) + ); + } +} + +pub trait StateContext { + fn get_state(&self) -> Option>; +} +impl StateContext for html::Scope { + fn get_state(&self) -> Option> { + self.context(Callback::noop()).map(|c| c.0) + } +} + +// Private + +impl State { + pub fn recalculate_term_display(&mut self, term_display: &TermDisplayContextFiles) { + let mut general = term_display.general.clone(); + let per_file = self.file_info.as_ref().and_then(|info| term_display.per_file.get(&info.name)); + if let Some(per_file) = per_file { + general.extend(per_file); + } + self.term_display = general; + } +} + +mod private { + pub enum StateUpdateKind { + FileInfo, + Parser, + Other, + } +} +use private::StateUpdateKind; + +pub struct StateProviderContext { + state: StateProvider, + _handle: ContextHandle>, +} + +#[derive(Properties, PartialEq)] +pub struct StateProviderProps { + pub children: Children, +} + +pub enum Msg { + Update(Update>), + ConfigChanged(Rc), +} + +impl Component for StateProviderContext { + type Message = Msg; + type Properties = StateProviderProps; + + fn create(ctx: &Context) -> Self { + let mut state = State::default(); + let (cfg, _handle) = ctx.link().context(ctx.link().callback(Msg::ConfigChanged)).unwrap(); + state.recalculate_term_display(&cfg.config.term_display); + Self { + state: StateProvider { + state, + update: Updater::new(ctx.link().callback(Msg::Update)), + }, + _handle, + } + } + + fn update(&mut self, ctx: &Context, msg: Self::Message) -> bool { + match msg { + Msg::Update(update) => { + let update = update.apply(&mut self.state.state); + if let Some(StateUpdateKind::FileInfo) = update { + let cfg = ctx.link().get_configuration().unwrap(); + self.state.state.recalculate_term_display(&cfg.config.term_display); + } + update.is_some() + } + Msg::ConfigChanged(cfg) => { + self.state.state.recalculate_term_display(&cfg.config.term_display); + true + } + } + } + + fn view(&self, ctx: &Context) -> Html { + html! { + > context={Rc::new(self.state.clone())}> + {for ctx.props().children.iter()} + >> + } + } +} diff --git a/axiom-profiler-GUI/src/utils/mod.rs b/axiom-profiler-GUI/src/utils/mod.rs index 666c679d..1c1606ab 100644 --- a/axiom-profiler-GUI/src/utils/mod.rs +++ b/axiom-profiler-GUI/src/utils/mod.rs @@ -6,3 +6,4 @@ pub mod toggle_list; pub mod lookup; pub mod position; pub mod overlay_page; +pub mod updater; diff --git a/axiom-profiler-GUI/src/utils/overlay_page.rs b/axiom-profiler-GUI/src/utils/overlay_page.rs index e180d584..28405411 100644 --- a/axiom-profiler-GUI/src/utils/overlay_page.rs +++ b/axiom-profiler-GUI/src/utils/overlay_page.rs @@ -8,10 +8,11 @@ pub type SetVisibleCallback = Rc>>>; #[derive(Properties, PartialEq)] pub struct OverlayProps { pub set_visible: SetVisibleCallback, + pub visible_changed: Callback, pub children: Children, } -pub struct Overlay { +pub struct Overlay { visible: bool, } @@ -30,24 +31,24 @@ impl Component for Overlay { } } fn changed(&mut self, ctx: &Context, old_props: &Self::Properties) -> bool { - if ctx.props() == old_props { - return false - } + debug_assert!(ctx.props() != old_props); *ctx.props().set_visible.borrow_mut() = ctx.link().callback(Msg::SetVisible); true } - fn update(&mut self, _ctx: &Context, msg: Self::Message) -> bool { + fn update(&mut self, ctx: &Context, msg: Self::Message) -> bool { match msg { Msg::SetVisible(visible) => { let Some(visible) = visible else { self.visible = !self.visible; + ctx.props().visible_changed.emit(self.visible); return true; }; if self.visible == visible { return false; } self.visible = visible; + ctx.props().visible_changed.emit(self.visible); true } } diff --git a/axiom-profiler-GUI/src/utils/split_div.rs b/axiom-profiler-GUI/src/utils/split_div.rs index f796413b..f9910f8d 100644 --- a/axiom-profiler-GUI/src/utils/split_div.rs +++ b/axiom-profiler-GUI/src/utils/split_div.rs @@ -77,10 +77,8 @@ impl Component for SplitDiv { } } fn changed(&mut self, ctx: &Context, old_props: &Self::Properties) -> bool { + debug_assert!(ctx.props() != old_props); let new_pros = ctx.props(); - if new_pros == old_props { - return false; - } let new_disabled = ctx.props().left_bound == ctx.props().right_bound; let old_disabled = old_props.left_bound == old_props.right_bound; if new_disabled != old_disabled { diff --git a/axiom-profiler-GUI/src/utils/updater.rs b/axiom-profiler-GUI/src/utils/updater.rs new file mode 100644 index 00000000..6e44153a --- /dev/null +++ b/axiom-profiler-GUI/src/utils/updater.rs @@ -0,0 +1,67 @@ +use std::cell::RefCell; + +use yew::{html::Scope, Callback, Component}; + +pub struct Updater(Callback>); + +impl Updater { + /// Called by the global provider on creation, with a callback to update the + /// provider. + pub fn new(update: Callback>) -> Self { + Self(update) + } + + pub fn new_link>>(link: Scope) -> Self where { + Self(Callback::from(move |update| link.send_message(update))) + } + + /// Called by the client to update the provider. + pub fn update(&self, f: impl for<'a> FnOnce(&'a mut T) -> O + 'static) { + self.0.emit(Update::new(f)); + } + + pub fn reset(&self) where T: Default + PartialEq, O: From { + self.update(|data| { + let new = Default::default(); + if *data != new { + *data = new; + true.into() + } else { + false.into() + } + }); + } +} + +impl Clone for Updater { + fn clone(&self) -> Self { + Self(self.0.clone()) + } + +} +impl PartialEq for Updater { + fn eq(&self, other: &Self) -> bool { + self.0 == other.0 + } +} + +pub struct Update(Callback<&'static mut T, O>); + +impl Update { + fn new(f: impl for<'a> FnOnce(&'a mut T) -> O + 'static) -> Self { + let f = RefCell::new(Some(f)); + let f = Callback::from(move |data| + f.borrow_mut().take().unwrap()(data) + ); + Self(f) + } + + /// Called by the global provider to apply the update. + pub fn apply(self, data: &mut T) -> O { + // SAFETY: the callback can only have been created with a + // `impl for<'a> FnOnce(&'a mut T) -> O + 'static`, and thus + // it cannot make use of the `&'static mut T` lifetime. + let data = unsafe { &mut *(data as *mut _) }; + self.0.emit(data) + } +} diff --git a/smt-log-parser/Cargo.toml b/smt-log-parser/Cargo.toml index 734edd3c..457f5f66 100644 --- a/smt-log-parser/Cargo.toml +++ b/smt-log-parser/Cargo.toml @@ -20,6 +20,7 @@ lasso = "0.7" nonmax = "0.5" serde = { version = "1.0.183", features = ["derive"], optional = true } mem_dbg = { version = "0.1.8", features = ["std", "derive"], default-features = false, optional = true } +regex = { version = "1.10", optional = true } [dev-dependencies] memory-stats = "1.1.0" @@ -28,7 +29,7 @@ smt-log-parser = { path = ".", features = ["mem_dbg"] } [features] default = ["display"] -display = [] +display = ["dep:regex"] # Tries to catch memory allocation errors, in some cases spends some extra time with test allocations # when a crate doesn't support `try_reserve`. Currently some panics may still happen. never_panic = [] diff --git a/smt-log-parser/src/display_with.rs b/smt-log-parser/src/display_with.rs index 3e18cfa0..faf70e56 100644 --- a/smt-log-parser/src/display_with.rs +++ b/smt-log-parser/src/display_with.rs @@ -1,6 +1,6 @@ use std::{borrow::Cow, fmt}; -use crate::{items::*, parsers::z3::z3parser::Z3Parser, StringTable, NonMaxU32}; +use crate::{formatter::{BindPowerPair, ChildIndex, MatchResult, SubFormatter, TermDisplayContext, QUANT_BIND}, items::*, parsers::z3::z3parser::Z3Parser, NonMaxU32, StringTable}; //////////// // General @@ -73,15 +73,34 @@ impl<'a, 'b, Ctxt, Data, T: DisplayWithCtxt + Copy> fmt::Display pub struct DisplayCtxt<'a> { pub parser: &'a Z3Parser, + pub term_display: &'a TermDisplayContext, pub config: DisplayConfiguration, } +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum SymbolReplacement { + Math, + Code, + None, +} + +impl SymbolReplacement { + pub fn as_math(self) -> Option { + match self { + SymbolReplacement::Math => Some(true), + SymbolReplacement::Code => Some(false), + SymbolReplacement::None => None, + } + } +} + #[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] #[derive(Debug, Clone, PartialEq, Eq)] pub struct DisplayConfiguration { pub display_term_ids: bool, pub display_quantifier_name: bool, - pub use_mathematical_symbols: bool, + pub replace_symbols: SymbolReplacement, /// Use tags for formatting pub html: bool, @@ -92,6 +111,7 @@ pub struct DisplayConfiguration { } mod private { + use crate::formatter::DEFAULT_BIND_POWER; use super::*; @@ -100,7 +120,7 @@ mod private { pub(super) term: TermIdx, children: &'a [TermIdx], quant: Vec<&'a Quantifier>, - bind_power: u8, + bind_power: BindPowerPair, ast_depth: u32, } impl<'a> DisplayData<'a> { @@ -109,7 +129,7 @@ mod private { term, children: &[], quant: Vec::new(), - bind_power: super::NO_BIND, + bind_power: BindPowerPair::symmetric(DEFAULT_BIND_POWER), ast_depth: 0, } } @@ -133,13 +153,30 @@ mod private { self.quant.pop(); result } - pub(super) fn with_bind_power( + + pub(super) fn with_outer_bind_power<'b>( + &mut self, + f: &mut fmt::Formatter<'b>, + bind_power: BindPowerPair, + inner: impl FnOnce(&mut Self, &mut fmt::Formatter<'b>) -> fmt::Result, + ) -> fmt::Result { + let needs_brackets = bind_power.is_smaller(&self.bind_power); + if needs_brackets { + write!(f, "(")?; + } + inner(self, f)?; + if needs_brackets { + write!(f, ")")?; + } + Ok(()) + } + pub(super) fn with_inner_bind_power<'f, 'b, T>( &mut self, - bind_power: u8, - f: impl FnOnce(&mut Self, u8) -> T, + bind_power: BindPowerPair, + f: impl FnOnce(&mut Self) -> T, ) -> T { let old = std::mem::replace(&mut self.bind_power, bind_power); - let result = f(self, old); + let result = f(self); self.bind_power = old; result } @@ -182,26 +219,26 @@ mod private { } use private::*; -// lower inside higher needs brackets around the lower -const NO_BIND: u8 = 0; -const QUANT_BIND: u8 = 3; -const TERNARY_BIND: u8 = 7; -const INFIX_BIND: u8 = 15; -const PREFIX_BIND: u8 = 31; //////////// // Item Idx defs //////////// -impl DisplayWithCtxt, ()> for TermIdx { +impl DisplayWithCtxt, Option> for TermIdx { fn fmt_with( self, f: &mut fmt::Formatter<'_>, ctxt: &DisplayCtxt<'_>, - _data: &mut (), + quant: &mut Option, ) -> fmt::Result { let mut data = DisplayData::new(self); - write!(f, "{}", ctxt.parser[self].with_data(ctxt, &mut data)) + if let Some(quant) = quant { + data.with_quant(&ctxt.parser[*quant], |data| { + write!(f, "{}", ctxt.parser[self].with_data(ctxt, data)) + }) + } else { + write!(f, "{}", ctxt.parser[self].with_data(ctxt, &mut data)) + } } } @@ -210,17 +247,17 @@ impl DisplayWithCtxt, ()> for ENodeIdx { self, f: &mut fmt::Formatter<'_>, ctxt: &DisplayCtxt<'_>, - data: &mut (), + _data: &mut (), ) -> fmt::Result { if let Some(enode_char_limit) = ctxt.config.enode_char_limit { - let owner = ctxt.parser[self].owner.with_data(ctxt, data).to_string(); + let owner = ctxt.parser[self].owner.with_data(ctxt, &mut None).to_string(); if owner.len() <= enode_char_limit.get() as usize { write!(f, "{owner}") } else { write!(f, "{}...", &owner[..enode_char_limit.get() as usize - 3]) } } else { - ctxt.parser[self].owner.fmt_with(f, ctxt, data) + ctxt.parser[self].owner.fmt_with(f, ctxt, &mut None) } } } @@ -230,11 +267,11 @@ impl DisplayWithCtxt, ()> for QuantIdx { self, f: &mut fmt::Formatter<'_>, ctxt: &DisplayCtxt<'_>, - data: &mut (), + _data: &mut (), ) -> fmt::Result { let quant = &ctxt.parser[self]; if let Some(term) = quant.term { - term.fmt_with(f, ctxt, data) + term.fmt_with(f, ctxt, &mut None) } else { let QuantKind::Other(name) = quant.kind else { panic!() @@ -319,7 +356,7 @@ impl DisplayWithCtxt, ()> for &QuantKind { ) -> fmt::Result { match *self { QuantKind::Other(kind) => write!(f, "{}", &ctxt.parser[kind]), - QuantKind::Lambda => if ctxt.config.use_mathematical_symbols { + QuantKind::Lambda => if matches!(ctxt.config.replace_symbols, SymbolReplacement::Math) { write!(f, "λ") } else if ctxt.config.html { write!(f, "<null>") @@ -358,7 +395,13 @@ impl<'a: 'b, 'b> DisplayWithCtxt, DisplayData<'b>> for &'a Term } if let Some(meaning) = ctxt.parser.meaning(data.term) { + if ctxt.config.html { + write!(f, "")?; + } write!(f, "{}", meaning.with_data(ctxt, data))?; + if ctxt.config.html { + write!(f, "")?; + } } else { write!(f, "{}", self.kind.with_data(ctxt, data))?; } @@ -372,7 +415,7 @@ impl VarNames { pub fn get_name<'a>(strings: &'a StringTable, this: Option<&Self>, idx: usize, config: &DisplayConfiguration) -> Cow<'a, str> { let name = match this { Some(Self::NameAndType(names)) => Cow::Borrowed(&strings[*names[idx].0]), - None | Some(Self::TypeOnly(_)) => Cow::Owned(if config.use_mathematical_symbols { + None | Some(Self::TypeOnly(_)) => Cow::Owned(if matches!(config.replace_symbols, SymbolReplacement::Math) { format!("•{idx}") } else { format!("qvar_{idx}") @@ -381,7 +424,7 @@ impl VarNames { if config.html { const COLORS: [&str; 9] = ["blue", "green", "olive", "maroon", "teal", "purple", "red", "fuchsia", "navy"]; let color = COLORS[idx % COLORS.len()]; - let name = format!("
    {name}
    "); + let name = format!("{name}"); Cow::Owned(name) } else { name @@ -417,14 +460,6 @@ fn display_child<'a, 'b, 'c, 'd>(f: &mut fmt::Formatter<'_>, child: TermIdx, ctx }) } -enum ProofOrAppKind<'a> { - Unary(&'a str), - Inline(&'a str), - Ternary(&'a str, &'a str), - Pattern, - OtherApp(&'a str), - Proof(&'a str), -} impl<'a, 'b> DisplayWithCtxt, DisplayData<'b>> for &'a ProofOrApp { fn fmt_with( self, @@ -432,99 +467,110 @@ impl<'a, 'b> DisplayWithCtxt, DisplayData<'b>> for &'a ProofOrAp ctxt: &DisplayCtxt<'b>, data: &mut DisplayData<'b>, ) -> fmt::Result { - let math = ctxt.config.use_mathematical_symbols; - use ProofOrAppKind::*; let name = &ctxt.parser[self.name]; - let kind = match name { - name if self.is_proof => Proof(name), - "not" => Unary(if math { "¬" } else { "!" }), - "-" if data.children().len() == 1 => Unary("-"), - - "and" => Inline(if math { "∧" } else { "&&" }), - "or" => Inline(if math { "∨" } else { "||" }), - "<=" => Inline(if math { "≤" } else { "<=" }), - ">=" => Inline(if math { "≥" } else { ">=" }), - op @ ("=" | "+" | "-" | "*" | "/" | "<" | ">") => Inline(op), - - "if" => Ternary("?", ":"), - - "pattern" => Pattern, - - name => OtherApp(name), - }; - match kind { - Unary(op) => data.with_bind_power(PREFIX_BIND, |data, bind_power| { - assert!(bind_power <= PREFIX_BIND); - assert_eq!(data.children().len(), 1); - let child = data.children()[0]; - write!(f, "{op}")?; - display_child(f, child, ctxt, data) - - }), - Inline(op) => data.with_bind_power(INFIX_BIND, |data, bind_power| { - let need_brackets = bind_power >= INFIX_BIND; - if need_brackets { - write!(f, "(")?; - } - for (idx, child) in data.children().iter().enumerate() { - if idx != 0 { - write!(f, " {op} ")?; - } - display_child(f, *child, ctxt, data)?; - } - if need_brackets { - write!(f, ")")?; - } - Ok(()) - }), - // `if` -> `$[#0|7] ? $[#1|7] : $[#2|7]_7` - Ternary(op1, op2) => data.with_bind_power(TERNARY_BIND, |data, bind_power| { - let need_brackets = bind_power >= TERNARY_BIND; - if need_brackets { - write!(f, "(")?; - } - assert_eq!(data.children().len(), 3); - let cond = data.children()[0]; - display_child(f, cond, ctxt, data)?; - write!(f, " {op1} ")?; - let then = data.children()[1]; - display_child(f, then, ctxt, data)?; - write!(f, " {op2} ")?; - let else_ = data.children()[2]; - display_child(f, else_, ctxt, data)?; - if need_brackets { - write!(f, ")")?; - } - Ok(()) - }), - // `pattern` -> `{ $(#0:-0|0|, ) }_256` - Pattern => data.with_bind_power(NO_BIND, |data, _| { - // BIND_POWER is highest - write!(f, "{{")?; - for (idx, child) in data.children().iter().enumerate() { - if idx != 0 { - write!(f, ", ")?; - } - display_child(f, *child, ctxt, data)?; + let children = NonMaxU32::new(data.children().len() as u32).unwrap(); + let match_ = ctxt.term_display.match_str(name, children); + match_.fmt_with(f, ctxt, data) + } +} +impl<'a, 'b> DisplayWithCtxt, DisplayData<'b>> for &'a MatchResult<'a, 'a> { + fn fmt_with(self, f: &mut fmt::Formatter<'_>, ctxt: &DisplayCtxt<'b>, data: &mut DisplayData<'b>) -> fmt::Result { + data.with_outer_bind_power(f, self.formatter.bind_power, |data, f| { + let get_capture = |idx: NonMaxU32| { + if idx == NonMaxU32::ZERO { + Some(self.haystack) + } else { + self.captures.as_ref().and_then(|c| c.get(idx.get() as usize).map(|c| c.as_str())) } - write!(f, "}}") - }), - OtherApp(name) | Proof(name) => data.with_bind_power(NO_BIND, |data, _| { - // BIND_POWER is highest - write!(f, "{name}")?; - if data.children().is_empty() { - return Ok(()); + }; + fn get_child(index: ChildIndex, data: &DisplayData) -> Option { + if index.0.is_negative() { + data.children().len().checked_sub(index.0.wrapping_abs() as u32 as usize) + } else { + let index = index.0 as usize; + (index < data.children().len()).then(|| index) } - write!(f, "(")?; - for (idx, child) in data.children().iter().enumerate() { - if idx != 0 { - write!(f, ", ")?; + } + fn write_formatter<'b, 's>(formatter_outputs: &[SubFormatter], f: &mut fmt::Formatter<'_>, ctxt: &DisplayCtxt<'b>, data: &mut DisplayData<'b>, get_capture: &impl Fn(NonMaxU32) -> Option<&'s str>) -> fmt::Result { + for output in formatter_outputs { + match output { + SubFormatter::String(s) => + write!(f, "{s}")?, + SubFormatter::Capture(idx) => { + let Some(capture) = get_capture(*idx) else { + continue; + }; + if let Some(as_math) = ctxt.config.replace_symbols.as_math() { + match capture { + "and" if as_math => write!(f, "∧")?, + "and" if !as_math => write!(f, "&&")?, + "or" if as_math => write!(f, "∨")?, + "or" if !as_math => write!(f, "||")?, + "not" if as_math => write!(f, "¬")?, + "not" if !as_math => write!(f, "!")?, + "<=" if as_math => write!(f, "≤")?, + ">=" if as_math => write!(f, "≥")?, + _ => write!(f, "{capture}")?, + } + } else { + write!(f, "{capture}")? + } + } + SubFormatter::Single { index, bind_power } => { + let Some(child) = get_child(*index, data) else { + continue; + }; + let child = data.children()[child]; + data.with_inner_bind_power(*bind_power, |data| { + display_child(f, child, ctxt, data) + })?; + } + SubFormatter::Repeat(r) => { + let (Some(from), Some(to)) = (get_child(r.from, data), get_child(r.to, data)) else { + continue; + }; + if !r.from.0.is_negative() && r.to.0.is_negative() && from > to { + continue; + } + if r.from.0.is_negative() && !r.to.0.is_negative() && from < to { + continue; + } + let forwards = from <= to; + // The range is inclusive on both ends + let mut curr = if forwards { from.wrapping_sub(1) } else { from.wrapping_add(1) }; + let iter = std::iter::from_fn(move || { + if curr == to { + None + } else { + curr = if forwards { curr.wrapping_add(1) } else { curr.wrapping_sub(1) }; + Some(curr) + } + }); + write_formatter(&r.left_sep.outputs, f, ctxt, data, get_capture)?; + let mut bind_power = BindPowerPair::asymmetric(r.left, r.middle.left); + for child in iter { + let is_final = child == to; + if is_final { + bind_power.right = r.right; + } + let child = data.children()[child]; + data.with_inner_bind_power(bind_power, |data| { + display_child(f, child, ctxt, data) + })?; + if !is_final { + write_formatter(&r.middle_sep.outputs, f, ctxt, data, get_capture)?; + bind_power.left = r.middle.right; + } + } + write_formatter(&r.right_sep.outputs, f, ctxt, data, get_capture)?; + } } - display_child(f, *child, ctxt, data)?; } - write!(f, ")") - }), - } + Ok(()) + } + + write_formatter(&self.formatter.outputs, f, ctxt, data, &get_capture) + }) } } @@ -555,12 +601,8 @@ impl<'a> DisplayWithCtxt, DisplayData<'a>> for &'a Quantifier { // want to replace the quantified variables by their names // for this, we need to store the quantifier in the context data.with_quant(self, |data| { - data.with_bind_power(QUANT_BIND, |data, bind_power| { - let need_brackets = bind_power > QUANT_BIND; - if need_brackets { - write!(f, "(")?; - } - if ctxt.config.use_mathematical_symbols { + data.with_outer_bind_power(f, QUANT_BIND, |data, f| { + if matches!(ctxt.config.replace_symbols, SymbolReplacement::Math) { write!(f, "∀ ")?; } else { write!(f, "FORALL ")?; @@ -576,7 +618,7 @@ impl<'a> DisplayWithCtxt, DisplayData<'a>> for &'a Quantifier { } write!(f, "{name}{ty}")?; } - let sep = if ctxt.config.use_mathematical_symbols { + let sep = if matches!(ctxt.config.replace_symbols, SymbolReplacement::Math) { "." } else { " ::" @@ -584,11 +626,9 @@ impl<'a> DisplayWithCtxt, DisplayData<'a>> for &'a Quantifier { write!(f, "{sep}")?; for child in data.children() { write!(f, " ")?; + // TODO: binding power! display_child(f, *child, ctxt, data)?; } - if need_brackets { - write!(f, ")")?; - } Ok(()) }) }) diff --git a/smt-log-parser/src/formatter/defns.rs b/smt-log-parser/src/formatter/defns.rs new file mode 100644 index 00000000..a27fdb29 --- /dev/null +++ b/smt-log-parser/src/formatter/defns.rs @@ -0,0 +1,408 @@ +use std::borrow::Cow; + +use fxhash::FxHashMap; + +use crate::NonMaxU32; + +use super::{ConversionError, DeParseTrait, FallbackParseError, TdcError}; + +pub const CONTROL_CHARACTER: char = '$'; +pub const SEPARATOR_CHARACTER: char = '|'; +pub const DEFAULT_BIND_POWER: BindPower = 0; + +#[derive(Default, Debug, Clone)] +pub struct TermDisplayContext { + string_matchers: FxHashMap<(Cow<'static, str>, Option), TermDisplay>, + regex_matchers: Vec, + regex_set: regex::RegexSet, + fallback: FallbackFormatter, +} + +impl FromIterator for Result { + fn from_iter>(iter: T) -> Self { + let mut this = TermDisplayContext::default(); + this.append(iter.into_iter())?; + Ok(this) + } +} + +impl TermDisplayContext { + pub fn is_empty(&self) -> bool { + self.string_matchers.is_empty() && self.regex_matchers.is_empty() + } + pub fn all(&self) -> impl Iterator { + self.string_matchers.values().chain(&self.regex_matchers) + } + pub fn fallback(&self) -> &FallbackFormatter { + &self.fallback + } + + pub fn set_fallback(&mut self, formatter: FallbackFormatter) { + self.fallback = formatter + } + + /// Appends multiple `TermDisplay` at once. This is more efficient than + /// repeatedly calling `push` as matching set for all regexes is calculated + /// only once. + pub fn append(&mut self, terms: impl Iterator) -> Result<(), TdcError> { + let mut added_regex_matcher = false; + for term in terms { + added_regex_matcher |= self.push_inner(term)?; + } + if added_regex_matcher { + self.calculate_regex_set(); + } + Ok(()) + } + + pub fn push(&mut self, term: TermDisplay) -> Result<(), TdcError> { + if self.push_inner(term)? { + self.calculate_regex_set(); + } + Ok(()) + } + + pub fn remove(&mut self, matcher: &Matcher) -> Option { + match &matcher.kind { + MatcherKind::Exact(s) => { + // SAFETY: though the lifetime is 'static in terms of the + // compiler, the actual lifetime will end at the end of the + // block. + let s = unsafe { &*(s.as_str() as *const _) }; + self.string_matchers.remove(&(Cow::Borrowed(s), matcher.children)) + } + MatcherKind::Regex(r) => { + let idx = self.regex_matchers.iter().position(|t| { + let MatcherKind::Regex(r2) = &t.matcher.kind else { unreachable!() }; + r2.original() == r.original() + })?; + let removed = self.regex_matchers.remove(idx); + self.calculate_regex_set(); + Some(removed) + } + } + } + + /// Extends this context with another higher priority one. If there are any + /// conflicts, we drop the conflicting entries from the `self` context! + pub fn extend(&mut self, other: &Self) { + for (k, v) in &other.string_matchers { + self.string_matchers.insert(k.clone(), v.clone()); + } + let must_recalculate = !other.regex_matchers.is_empty(); + let mut regex_matchers = other.regex_matchers.clone(); + regex_matchers.extend(self.regex_matchers.drain(..)); + self.regex_matchers = regex_matchers; + if must_recalculate { + self.calculate_regex_set(); + } + } + + /// Returns the formatter for the given string, defaulting to the fallback + /// if none match. See [`Self::match_str_opt`] for more details. + pub fn match_str<'a, 'b>(&'b self, haystack: &'a str, children: NonMaxU32) -> MatchResult<'a, 'b> { + self.match_str_opt(haystack, children).unwrap_or_else(|| { + MatchResult { + haystack, + captures: None, + formatter: self.fallback().formatter(), + } + }) + } + + /// Returns the formatter for the given string, if one exists. If multiple + /// matchers match the string, then the first one is returned. The order is + /// determined as `Matcher::Exact` first and then the first `Matcher::Regex` + /// in the order provided when constructing `self`. + pub fn match_str_opt<'a, 'b>(&'b self, haystack: &'a str, children: NonMaxU32) -> Option> { + // SAFETY: though the lifetime is 'static in terms of the + // compiler, the actual lifetime will end at the end of the + // block. + let static_key = unsafe { + &*(haystack as *const _) + }; + let string_match = self.string_matchers.get(&(Cow::Borrowed(static_key), Some(children))); + let string_match = string_match.or_else(|| self.string_matchers.get(&(Cow::Borrowed(static_key), None))); + if let Some(td) = string_match { + Some(td.as_match_no_capture(haystack)) + } else { + let mut matches = self.regex_set + .matches(haystack) + .into_iter() + .map(|idx| &self.regex_matchers[idx]) + .filter(|td| + !td.matcher.children.is_some_and(|c| c != children) + ); + // Fallback match in case of no matches which specify exact children + let first = matches.next(); + let mut matches = first.iter().copied().chain(matches); + let specific = matches.find(|td| td.matcher.children.is_some()); + let match_ = specific.or(first)?; + Some(match_.as_match_capture(haystack)) + } + } + + pub(super) fn to_parts(&self) -> (&FxHashMap<(Cow<'static, str>, Option), TermDisplay>, &Vec, &FallbackFormatter) { + (&self.string_matchers, &self.regex_matchers, &self.fallback) + } + pub(super) fn from_parts(string_matchers: FxHashMap<(Cow<'static, str>, Option), TermDisplay>, regex_matchers: Vec, fallback: FallbackFormatter) -> Self { + let mut this = TermDisplayContext::default(); + this.string_matchers = string_matchers; + this.regex_matchers = regex_matchers; + this.calculate_regex_set(); + this.fallback = fallback; + this + } + + fn push_inner(&mut self, term: TermDisplay) -> Result { + match &term.matcher.kind { + MatcherKind::Exact(s) => { + let k = (Cow::Owned(s.to_string()), term.matcher.children); + let duplicate = self.string_matchers.insert(k, term); + if let Some(duplicate) = duplicate { + let MatcherKind::Exact(s) = duplicate.matcher.kind else { unreachable!() }; + Err(TdcError::DuplicateExactMatcher(s, duplicate.matcher.children)) + } else { + Ok(false) + } + } + MatcherKind::Regex(_) => { + self.regex_matchers.push(term); + Ok(true) + } + } + } + fn calculate_regex_set(&mut self) { + self.regex_set = regex::RegexSet::new(self.regex_matchers.iter().map(|t| { + let MatcherKind::Regex(r) = &t.matcher.kind else { unreachable!() }; + r.original() + })).unwrap(); + } +} + +impl PartialEq for TermDisplayContext { + fn eq(&self, other: &Self) -> bool { + self.string_matchers == other.string_matchers + && self.regex_matchers == other.regex_matchers + && self.fallback == other.fallback + } +} +impl Eq for TermDisplayContext {} + +pub struct MatchResult<'a, 'b> { + pub haystack: &'a str, + pub captures: Option>, + pub formatter: &'b Formatter, +} + +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct TermDisplay { + pub(crate) matcher: Matcher, + pub(crate) formatter: Formatter, +} + +impl TermDisplay { + pub const fn empty() -> Self { + Self { + matcher: Matcher { + children: None, + kind: MatcherKind::Exact(String::new()), + }, + formatter: Formatter { + bind_power: BindPowerPair::symmetric(DEFAULT_BIND_POWER), + outputs: Vec::new(), + max_capture: None, + }, + } + } + + pub fn new(matcher: Matcher, formatter: Formatter) -> Result { + if let Some(max_capture) = formatter.max_capture { + let MatcherKind::Regex(r) = &matcher.kind else { + return Err(ConversionError::FormatterExpectsRegex(matcher, formatter)) + }; + if max_capture.get() as usize >= r.regex().captures_len() { + return Err(ConversionError::RegexNotEnoughCaptures(matcher, formatter)) + } + } + Ok(Self { matcher, formatter }) + } + pub fn deparse_string(&self) -> (String, String) { + (self.matcher.deparse_string(), self.formatter.deparse_string()) + } + + pub fn is_empty(&self) -> bool { + self == &Self::empty() + } + + /// Call this when you already know that `self.matcher` matches `haystack`. + pub const fn as_match_no_capture<'a>(&self, haystack: &'a str) -> MatchResult<'a, '_> { + MatchResult { + haystack, + captures: None, + formatter: &self.formatter, + } + } + + /// Call this when you already know that `self.matcher` matches `haystack`. + pub fn as_match_capture<'a>(&self, haystack: &'a str) -> MatchResult<'a, '_> { + let MatcherKind::Regex(r) = &self.matcher.kind else { + unreachable!() + }; + let Some(max_capture) = self.formatter.max_capture else { + return self.as_match_no_capture(haystack) + }; + let captures = r.regex().captures(haystack).unwrap(); + debug_assert!(captures.len() > max_capture.get() as usize); + MatchResult { + haystack, + captures: Some(captures), + formatter: &self.formatter, + } + } +} + +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Matcher { + pub children: Option, + pub kind: MatcherKind, +} + +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum MatcherKind { + Exact(String), + Regex(RegexMatcher), +} + +#[derive(Debug, Clone)] +pub struct RegexMatcher { + original: String, + regex: regex::Regex, +} +impl RegexMatcher { + pub fn new(original: String) -> Result { + let regex = regex::Regex::new(&original)?; + Ok(Self { original, regex }) + } + pub fn original(&self) -> &String { + &self.original + } + pub fn regex(&self) -> ®ex::Regex { + &self.regex + } +} + +impl PartialEq for RegexMatcher { + fn eq(&self, other: &Self) -> bool { + self.original == other.original + } +} +impl Eq for RegexMatcher {} + +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct Formatter { + /// How strongly does the formatter bind its output from the left? Bracketed + /// outputs generally have a higher binding power than non-bracketed ones. + /// For example `{ ... }` can have a higher binding power, while `... + ...` + /// would typically have a lower binding power. + pub bind_power: BindPowerPair, + + /// The formatter's output + pub outputs: Vec, + + /// The maximum value of any stored `SubFormatter::Capture`. + pub max_capture: Option, +} + +impl Formatter { + pub fn calculate_max_capture(&mut self) { + self.max_capture = self.outputs.iter().flat_map(|o| match o { + SubFormatter::Capture(c) => Some(*c), + SubFormatter::Repeat(r) => + (r.left_sep.max_capture.is_some() || + r.middle_sep.max_capture.is_some() || + r.right_sep.max_capture.is_some() + ).then(|| { + r.left_sep.max_capture.unwrap_or_default().max( + r.middle_sep.max_capture.unwrap_or_default().max( + r.right_sep.max_capture.unwrap_or_default() + ) + ) + }), + _ => None, + }).max(); + } +} + +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Default, Debug, Clone, PartialEq, Eq)] +pub struct FallbackFormatter(Formatter); + +impl FallbackFormatter { + /// Creates the fallback formatter. Returns `Ok` if successful, `Err` + /// if the fallback formatter has a non-zero `max_capture`. + pub fn new(formatter: Formatter) -> Result { + if let Some(mc) = formatter.max_capture.filter(|mc| mc.get() > 0) { + Err(FallbackParseError::MaxCaptureTooLarge(mc)) + } else { + Ok(Self(formatter)) + } + } + pub fn formatter(&self) -> &Formatter { + &self.0 + } +} + +pub type BindPower = u32; + +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct BindPowerPair { + pub left: BindPower, + pub right: BindPower, +} +impl BindPowerPair { + pub const fn symmetric(power: BindPower) -> Self { + Self { left: power, right: power } + } + pub const fn asymmetric(left: BindPower, right: BindPower) -> Self { + Self { left, right } + } + pub const fn is_smaller(&self, other: &Self) -> bool { + self.left < other.left || self.right < other.right + } +} + +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum SubFormatter { + String(String), + Single { + index: ChildIndex, + /// How strongly does the surrounding context bind the child? + bind_power: BindPowerPair, + }, + Repeat(SubFormatterRepeat), + Capture(NonMaxU32), +} + +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct SubFormatterRepeat { + pub from: ChildIndex, + pub to: ChildIndex, + pub left_sep: Formatter, + pub middle_sep: Formatter, + pub right_sep: Formatter, + pub left: BindPower, + pub middle: BindPowerPair, + pub right: BindPower, +} + +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub struct ChildIndex(pub i32); diff --git a/smt-log-parser/src/formatter/defns_const.rs b/smt-log-parser/src/formatter/defns_const.rs new file mode 100644 index 00000000..121b9fc5 --- /dev/null +++ b/smt-log-parser/src/formatter/defns_const.rs @@ -0,0 +1,212 @@ +use crate::NonMaxU32; + +use super::{defns::*, ConversionError, FormatterParseError}; + +#[derive(Debug)] +pub struct TermDisplayConst<'a> { + pub matcher: MatcherConst<'a>, + pub formatter: FormatterConst<'a>, +} + +impl TryFrom> for TermDisplay { + type Error = ConversionError; + fn try_from(t: TermDisplayConst) -> Result { + let matcher = Matcher::try_from(t.matcher)?; + let formatter = Formatter::try_from(t.formatter)?; + Self::new(matcher, formatter) + } +} + +#[derive(Debug)] +pub struct MatcherConst<'a> { + pub data: &'a str, + pub children: Option, + pub kind: MatcherKindConst, +} + +#[derive(Debug)] +pub enum MatcherKindConst { + Exact, + Regex, +} + +impl TryFrom> for Matcher { + type Error = regex::Error; + fn try_from(m: MatcherConst<'_>) -> Result { + let kind = match m.kind { + MatcherKindConst::Exact => + MatcherKind::Exact(m.data.to_string()), + MatcherKindConst::Regex => { + MatcherKind::Regex(RegexMatcher::new(format!("^(?:{})$", m.data))?) + } + }; + Ok(Matcher { + children: m.children, + kind, + }) + } +} + +#[derive(Debug)] +pub struct FormatterConst<'a> { + /// How strongly does the formatter bind its output from the left? Bracketed + /// outputs generally have a higher binding power than non-bracketed ones. + /// For example `{ ... }` can have a higher binding power, while `... + ...` + /// would typically have a lower binding power. + pub bind_power: BindPowerPair, + + /// The formatter's output + pub outputs: [Option>; 64], +} + +impl TryFrom> for Formatter { + type Error = FormatterParseError; + fn try_from(f: FormatterConst<'_>) -> Result { + let outputs: Vec<_> = f.outputs.into_iter().map_while(|o| o).map(|o| SubFormatter::try_from(o)).collect::>()?; + let mut self_ = Self { + bind_power: f.bind_power, + outputs, + max_capture: None, + }; + self_.calculate_max_capture(); + Ok(self_) + } +} + +impl<'a> FormatterConst<'a> { + /// Shallow max capture calculation. + pub const fn max_capture(&self) -> Option { + let mut max_capture = None::; + let mut idx = 0; + while idx < self.outputs.len() { + let Some(output) = &self.outputs[idx] else { + break; + }; + if let SubFormatterConst::Capture(idx) = output { + max_capture = match max_capture { + Some(max) if max.get() >= idx.get() => Some(max), + _ => Some(*idx), + }; + } + idx += 1; + } + max_capture + } +} + +#[derive(Debug)] +pub enum SubFormatterConst<'a> { + /// A simple string output, will be printed literally. + String(SubFormatterString<'a>), + /// + Single(SubFormatterSingle), + Repeat(SubFormatterRepeatConst<'a>), + Capture(NonMaxU32), +} + +impl TryFrom> for SubFormatter { + type Error = FormatterParseError; + fn try_from(sub: SubFormatterConst<'_>) -> Result { + let sf = match sub { + SubFormatterConst::String(s) => { + let c = s.control_deduplicate.then(|| CONTROL_CHARACTER); + let data = deduplicate_character(s.data, c); + SubFormatter::String(data) + } + SubFormatterConst::Single(s) => SubFormatter::Single { + index: s.index, + bind_power: s.bind_power, + }, + SubFormatterConst::Repeat(s) => SubFormatter::Repeat(s.try_into()?), + SubFormatterConst::Capture(idx) => SubFormatter::Capture(idx), + }; + Ok(sf) + } +} + +#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))] +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct SubFormatterSingle { + pub index: ChildIndex, + /// How strongly does the surrounding context bind the child? + pub bind_power: BindPowerPair, +} + +#[derive(Debug)] +pub struct SubFormatterString<'a> { + pub data: &'a str, + pub control_deduplicate: bool, +} + +#[derive(Debug)] +pub struct SubFormatterRepeatConst<'a> { + pub range: ChildRange, + pub left_sep: SubFormatterRepeatSeparator<'a>, + pub middle_sep: SubFormatterRepeatSeparator<'a>, + pub right_sep: SubFormatterRepeatSeparator<'a>, + pub left: BindPower, + pub middle: BindPowerPair, + pub right: BindPower, +} + +impl TryFrom> for SubFormatterRepeat { + type Error = FormatterParseError; + fn try_from(sub: SubFormatterRepeatConst<'_>) -> Result { + let left_sep = String::from(sub.left_sep); + let left_sep = left_sep.parse::()?; + let middle_sep = String::from(sub.middle_sep); + let middle_sep = middle_sep.parse::()?; + let right_sep = String::from(sub.right_sep); + let right_sep = right_sep.parse::()?; + Ok(Self { + from: sub.range.from, + to: sub.range.to, + left_sep, + middle_sep, + right_sep, + left: sub.left, + middle: sub.middle, + right: sub.right, + }) + } +} + +#[derive(Debug)] +pub struct SubFormatterRepeatSeparator<'a> { + /// Does the separator contain `SEPARATOR_CHARACTER`s that should be + /// deduplicated? + pub separator_deduplicate: bool, + pub separator: &'a str, +} + +impl From> for String { + fn from(sep: SubFormatterRepeatSeparator<'_>) -> Self { + let c = sep.separator_deduplicate.then(|| SEPARATOR_CHARACTER); + deduplicate_character(sep.separator, c) + } +} + +impl SubFormatterRepeatSeparator<'static> { + pub const fn default() -> Self { + Self { + separator_deduplicate: false, + separator: "", + } + } +} + +#[derive(Debug)] +pub struct ChildRange { + pub from: ChildIndex, + pub to: ChildIndex, +} + +fn deduplicate_character(s: &str, c: Option) -> String { + if let Some(c) = c { + let mut to: [u8; 4] = [0; 4]; + let to = c.encode_utf8(&mut to); + s.replace([c, c], to) + } else { + s.to_string() + } +} diff --git a/smt-log-parser/src/formatter/deparse.rs b/smt-log-parser/src/formatter/deparse.rs new file mode 100644 index 00000000..4ef2773a --- /dev/null +++ b/smt-log-parser/src/formatter/deparse.rs @@ -0,0 +1,118 @@ +use core::fmt; + +use super::defns::*; + +pub struct DeParse(pub D); + +impl fmt::Display for DeParse { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + self.0.deparse(f) + } +} + +pub trait DeParseTrait: Copy { + fn deparse_string(self) -> String { + DeParse(self).to_string() + } + fn deparse(self, f: &mut fmt::Formatter) -> fmt::Result; +} + +impl DeParseTrait for &'_ Matcher { + fn deparse(self, f: &mut fmt::Formatter) -> fmt::Result { + if self.children.is_some() { + write!(f, "(")?; + } + self.kind.deparse(f)?; + if let Some(children) = &self.children { + for _ in 0..children.get() { + write!(f, " _")?; + } + write!(f, ")")?; + } + Ok(()) + } +} + +impl DeParseTrait for &'_ MatcherKind { + fn deparse(self, f: &mut fmt::Formatter) -> fmt::Result { + match self { + MatcherKind::Exact(s) => + write!(f, "{s}"), + MatcherKind::Regex(r) => { + write!(f, "/")?; + let original = r.original(); + let no_prefix = original.strip_prefix("^(?:").unwrap_or(original); + let no_suffix = no_prefix.strip_suffix(")$").unwrap_or(no_prefix); + write!(f, "{no_suffix}")?; + write!(f, "/") + } + } + } +} + +impl DeParseTrait for &'_ Formatter { + fn deparse(self, f: &mut fmt::Formatter) -> fmt::Result { + if self.bind_power.left != DEFAULT_BIND_POWER { + write!(f, "{CONTROL_CHARACTER}{}{CONTROL_CHARACTER}", self.bind_power.left as i32)?; + } + for o in &self.outputs { + o.deparse(f)?; + } + if self.bind_power.right != DEFAULT_BIND_POWER { + write!(f, "{CONTROL_CHARACTER}{}{CONTROL_CHARACTER}", self.bind_power.right as i32)?; + } + Ok(()) + } +} + +impl DeParseTrait for &'_ SubFormatter { + fn deparse(self, f: &mut fmt::Formatter) -> fmt::Result { + match self { + SubFormatter::String(s) => + write!(f, "{}", duplicate_character(s, CONTROL_CHARACTER)), + SubFormatter::Single { index, bind_power } => + write!(f, "{CONTROL_CHARACTER}[#{}{SEPARATOR_CHARACTER}{}]{CONTROL_CHARACTER}", index.0, DeParse(bind_power)), + SubFormatter::Repeat(r) => { + write!(f, "{CONTROL_CHARACTER}(")?; + r.deparse(f)?; + write!(f, "){CONTROL_CHARACTER}") + } + SubFormatter::Capture(c) => + write!(f, "{CONTROL_CHARACTER}{{{c}}}{CONTROL_CHARACTER}"), + } + } +} + +fn duplicate_character(s: &str, c: char) -> String { + s.replace(c, &String::from_iter([c, c].into_iter())) +} + +impl DeParseTrait for &'_ BindPowerPair { + fn deparse(self, f: &mut fmt::Formatter) -> fmt::Result { + if self.left == self.right { + write!(f, "{}", self.left as i32) + } else { + write!(f, "{},{}", self.left as i32, self.right as i32) + } + } +} + +impl DeParseTrait for &'_ SubFormatterRepeat { + fn deparse(self, f: &mut fmt::Formatter) -> fmt::Result { + let from = self.from.0; + let to = self.to.0; + let left = self.left as i32; + let middle = DeParse(&self.middle); + let right = self.right as i32; + write!(f, "#{from}:{to}{SEPARATOR_CHARACTER}{left}{SEPARATOR_CHARACTER}{middle}{SEPARATOR_CHARACTER}{right}{CONTROL_CHARACTER}")?; + let left_sep = duplicate_character(&DeParse(&self.left_sep).to_string(), SEPARATOR_CHARACTER); + write!(f, "{left_sep}")?; + write!(f, "{SEPARATOR_CHARACTER}")?; + let middle_sep = duplicate_character(&DeParse(&self.middle_sep).to_string(), SEPARATOR_CHARACTER); + write!(f, "{middle_sep}")?; + write!(f, "{SEPARATOR_CHARACTER}")?; + let right_sep = duplicate_character(&DeParse(&self.right_sep).to_string(), SEPARATOR_CHARACTER); + write!(f, "{right_sep}")?; + Ok(()) + } +} diff --git a/smt-log-parser/src/formatter/error.rs b/smt-log-parser/src/formatter/error.rs new file mode 100644 index 00000000..31e1900c --- /dev/null +++ b/smt-log-parser/src/formatter/error.rs @@ -0,0 +1,177 @@ +use crate::NonMaxU32; + +use super::{ConstSplit, Matcher, Formatter}; + +#[derive(Debug, Clone)] +pub enum TdcError { + DuplicateExactMatcher(String, Option), +} + +#[derive(Debug, Clone)] +pub enum FallbackParseError { + MaxCaptureTooLarge(NonMaxU32), + FormatterParseError(FormatterParseError), +} + +#[derive(Debug)] +pub enum ConversionError { + Regex(regex::Error), + FormatterExpectsRegex(Matcher, Formatter), + RegexNotEnoughCaptures(Matcher, Formatter), + MatcherError(MatcherParseError), + FormatterParseError(FormatterParseError), +} + +impl From for ConversionError { + fn from(err: regex::Error) -> Self { + Self::Regex(err) + } +} + +impl From for ConversionError { + fn from(err: MatcherParseError) -> Self { + Self::MatcherError(err) + } +} + +impl From for ConversionError { + fn from(err: FormatterParseError) -> Self { + Self::FormatterParseError(err) + } +} + +pub type FormatterParseError = ParseError; +pub type MatcherParseError = ParseError; + +#[derive(Debug, Clone)] +pub struct ParseError { + pub s: String, + pub kind: T, +} + +impl From> for ParseError { + fn from(err: ParseErrorConst<'_, T>) -> Self { + Self { s: err.s.to_owned(), kind: err.kind } + } +} + +pub type ResultFormatterConst<'a, T> = Result>; +pub type ResultMatcherConst<'a, T> = Result>; +pub type ResultConst<'a, T> = Result>; + +#[derive(Debug)] +pub struct ParseErrorConst<'a, T> { + pub s: &'a str, + pub kind: T, +} + +#[derive(Debug, Clone)] +pub enum FormatterError { + MissingHash, + MissingRange, + MissingControl(&'static str), + TooManyControl(char), + UnexpectedPair, + IncorrectControl, + InvalidNumber, + CaptureOverflow, +} + +impl FormatterError { + pub const fn const_error(&self, error: bool) -> T { + use FormatterError::*; + match self { + MissingHash => [()][error as usize], + MissingRange => [()][error as usize], + MissingControl(_) => [()][error as usize], + TooManyControl(_) => [()][error as usize], + UnexpectedPair => [()][error as usize], + IncorrectControl => [()][error as usize], + InvalidNumber => [()][error as usize], + CaptureOverflow => [()][error as usize], + }; + [()][!error as usize]; + loop {} + } +} + +impl<'a> ParseErrorConst<'a, FormatterError> { + pub(super) const fn missing_hash(s: &'a str) -> Self { + Self { s, kind: FormatterError::MissingHash } + } + pub(super) const fn invalid_number(s: &'a str) -> Self { + Self { s, kind: FormatterError::InvalidNumber } + } + pub(super) const fn missing_range(s: &'a str) -> Self { + Self { s, kind: FormatterError::MissingRange } + } + pub(super) const fn missing_control(s: &'a str, expected: &'static str) -> Self { + Self { s, kind: FormatterError::MissingControl(expected) } + } + pub(super) const fn too_many_control(split: ConstSplit<'a, 1>) -> Self { + Self { s: split.remainder(), kind: FormatterError::TooManyControl(split.control()) } + } + pub(super) const fn unexpected_pair(s: &'a str) -> Self { + Self { s, kind: FormatterError::UnexpectedPair } + } + pub(super) const fn incorrect_control(s: &'a str) -> Self { + Self { s, kind: FormatterError::IncorrectControl } + } + pub(super) const fn capture_overflow(s: &'a str) -> Self { + Self { s, kind: FormatterError::CaptureOverflow } + } +} + +#[derive(Debug, Clone)] +pub enum MatcherError { + InvalidChildrenSpec, +} + +impl MatcherError { + pub const fn const_error(&self, error: bool) -> T { + use MatcherError::*; + match self { + InvalidChildrenSpec => [()][error as usize], + }; + [()][!error as usize]; + loop {} + } +} + +impl<'a> ParseErrorConst<'a, MatcherError> { + pub(super) const fn invalid_children_spec(s: &'a str) -> Self { + Self { s, kind: MatcherError::InvalidChildrenSpec } + } +} + +pub enum EitherError { + Formatter(FormatterError), + Matcher(MatcherError), + InvalidCapture, +} + +impl EitherError { + pub const fn const_error(&self, error: bool) -> T { + use EitherError::*; + match self { + Formatter(err) => err.const_error(error), + Matcher(err) => err.const_error(error), + InvalidCapture => [()][error as usize], + }; + [()][!error as usize]; + loop {} + } +} + +impl<'a> ParseErrorConst<'a, EitherError> { + pub(super) const fn formatter(err: ParseErrorConst<'a, FormatterError>) -> Self { + Self { s: err.s, kind: EitherError::Formatter(err.kind) } + } + pub(super) const fn matcher(err: ParseErrorConst<'a, MatcherError>) -> Self { + Self { s: err.s, kind: EitherError::Matcher(err.kind) } + } + + pub(super) const fn invalid_capture(s: &'a str) -> Self { + Self { s, kind: EitherError::InvalidCapture } + } +} diff --git a/smt-log-parser/src/formatter/mod.rs b/smt-log-parser/src/formatter/mod.rs new file mode 100644 index 00000000..523b4dd9 --- /dev/null +++ b/smt-log-parser/src/formatter/mod.rs @@ -0,0 +1,54 @@ +mod defns; +mod error; +mod parse; +mod defns_const; +#[cfg(feature = "serde")] +mod serde; +mod deparse; + +pub use defns::*; +pub use error::*; +pub(self) use parse::*; +pub use defns_const::*; +pub use deparse::*; + +macro_rules! unwrap { + ($e:expr) => { + match $e { + Ok(v) => v, + Err(e) => e.kind.const_error(true), + } + }; +} + +pub const QUANT_BIND: BindPowerPair = unwrap!(BindPowerPair::parse("-6,12")).1; + +pub const DEFAULT_FORMATTER: FormatterConst<'static> = unwrap!(FormatterConst::parse("$-8$${0}$$(#0:-1|4|8|4$(|, |))$$-4$")); +// pub const DEFAULT: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse("/(?:.|\\n)*/", "$-8$${0}$$(#0:-1|4|8|4$(|, |))$$-4$")); + +pub const TRIGGER: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse("pattern", "$-8${ $(#0:-1|4|8|4$, )$ }$-8$")); + +pub const UNARY_OP: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse("(/(?:not)/ _)", "$-6$${0}$$[#0|-8,16]$$-16$")); +pub const NEG: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse("(- _)", "$-6$-$[#0|-8,16]$$-16$")); +/// I'm not sure all of these are necessary since z3 generally breaks up terms, +/// e.g. `(>= _ _)` into `(and (= _ _) (< _ _))`, or `(=> _ _)` into `(or (not _) _)`. +pub const BINARY_OP: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse("/=|\\+|-|\\*|/|<|>|(?:and)|(?:or)|(?:<=)|(?:>=)|(?:=>)/", "$10$$(#0:-1|9|-16|9$| ${0}$ |)$$10$")); +pub const IF: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse("if", "$-8$$[#0|9,-16]$ ? $[#1|4,4]$ : $[#2|4,4]$$-8$")); + +// pub const SLOT_TEST: TermDisplayConst<'static> = unwrap!(TermDisplayConst::parse("slot", "$-8$&$[#0|9,-16]$[$[#1|4,4]$]$-8$")); + +impl TermDisplayContext { + pub fn basic() -> Self { + let self_: Result = [TRIGGER, UNARY_OP, NEG, BINARY_OP, IF].into_iter().map(|td| + TermDisplay::try_from(td).unwrap() + ).collect(); + self_.unwrap() + } +} + +impl Default for Formatter { + fn default() -> Self { + static FMT: std::sync::OnceLock = std::sync::OnceLock::new(); + FMT.get_or_init(|| Formatter::try_from(DEFAULT_FORMATTER).unwrap()).clone() + } +} diff --git a/smt-log-parser/src/formatter/parse.rs b/smt-log-parser/src/formatter/parse.rs new file mode 100644 index 00000000..46202994 --- /dev/null +++ b/smt-log-parser/src/formatter/parse.rs @@ -0,0 +1,589 @@ +use std::str::FromStr; + +use crate::NonMaxU32; + +use super::{defns::*, defns_const::*, error::*}; + +macro_rules! map_opt { + ($e:expr, $s:pat => $t:expr) => { + match $e { + Some($s) => Some($t), + None => None, + } + }; + ($s:ident => $t:expr) => { + map_opt!($s, $s => $t) + }; + ($e:expr, $s:pat => $t:expr, $d:expr) => { + match $e { + Some($s) => $t, + None => $d, + } + }; + ($s:ident => $t:expr, $d:expr) => { + map_opt!($s, $s => $t, $d) + }; + ($e:expr, Err($d:expr)) => { + match $e { + Some(s) => s, + None => return Err($d), + } + }; +} + +macro_rules! map_res { + ($e:expr) => { + map_res!($e, s => s, err => return Err(err)) + }; + ($e:expr, $err:ident => $f:expr) => { + map_res!($e, s => s, $err => return Err($f)) + }; + ($e:expr, $s:pat => $t:expr, $err:ident => $f:expr) => { + match $e { + Ok($s) => $t, + Err($err) => $f, + } + }; +} + +// Const parsing + +impl ChildIndex { + pub const fn parse<'a>(s: &'a str, hash_prefix: bool) -> ResultFormatterConst<'a, Self> { + let s = if hash_prefix { + let tail = ConstOperations::strip_prefix(s, '#'); + map_opt!(tail, Err(ParseErrorConst::missing_hash(s))) + } else { + s + }; + let index = map_res!(ConstOperations::parse_i32(s)); + Ok(Self(index)) + } +} + +impl ChildRange { + pub const fn parse<'a>(s: &'a str) -> ResultFormatterConst<'a, Self> { + let split = ConstOperations::split_first(s, ':'); + let (from, to) = map_opt!(split, Err(ParseErrorConst::missing_range(s))); + let from = map_res!(ChildIndex::parse(from, true)); + let to = map_res!(ChildIndex::parse(to, false)); + Ok(ChildRange { from, to }) + } +} + +impl BindPowerPair { + pub const fn parse<'a>(s: &'a str) -> ResultFormatterConst<'a, (bool, Self)> { + let split = ConstOperations::split(s, ','); + let (_, first, split) = split.next::(); + let first = map_res!(ConstOperations::parse_u32(first)); + let (second, split) = ConstOperations::split_more(split); + let second = map_opt!(second => map_res!(ConstOperations::parse_u32(second))); + match (second, split) { + (.., Some(split)) => Err(ParseErrorConst::too_many_control(split)), + (None, ..) => Ok((false, BindPowerPair::symmetric(first))), + (Some(second), None) => Ok((true, BindPowerPair::asymmetric(first, second))), + } + } +} + +impl SubFormatterSingle { + pub const fn parse<'a>(s: &'a str) -> ResultFormatterConst<'a, Self> { + let split = ConstOperations::split(s, SEPARATOR_CHARACTER); + let (_, index, split) = split.next::(); + let index = map_res!(ChildIndex::parse(index, true)); + let bind_power = map_opt!( + split => map_res!(BindPowerPair::parse(split.remainder())).1, + BindPowerPair::symmetric(DEFAULT_BIND_POWER) + ); + Ok(Self { index, bind_power }) + } +} + +impl<'a> SubFormatterRepeatConst<'a> { + pub const fn parse(s: &'a str) -> ResultFormatterConst<'a, Self> { + let split = ConstOperations::split(s, CONTROL_CHARACTER); + let (_, left, sep) = split.next::(); + + // $(`a:b|n|m,o,|p`$ + let left = ConstOperations::split(left, SEPARATOR_CHARACTER); + let (_, range, split) = left.next::(); + let range = map_res!(ChildRange::parse(range)); + let (left, middle, right) = map_res!(Self::parse_triple(split)); + + // $`(|, |)`)$ + let mut left_sep = SubFormatterRepeatSeparator::default(); + let mut middle_sep = SubFormatterRepeatSeparator::default(); + let mut right_sep = SubFormatterRepeatSeparator::default(); + if let Some(sep) = sep { + let sep = ConstOperations::split(sep.remainder(), SEPARATOR_CHARACTER); + let (separator_deduplicate, separator, sep) = sep.next::(); + if let Some(sep_two) = sep { + left_sep.separator_deduplicate = separator_deduplicate; + left_sep.separator = separator; + let (separator_deduplicate, separator, sep) = sep_two.next::(); + let sep = map_opt!(sep => sep, return Err(ParseErrorConst::too_many_control(sep_two))); + middle_sep.separator_deduplicate = separator_deduplicate; + middle_sep.separator = separator; + let (separator_deduplicate, separator, sep) = sep.next::(); + #[allow(unreachable_code)] + { map_opt!(sep => return Err(ParseErrorConst::too_many_control(sep))); } + right_sep.separator_deduplicate = separator_deduplicate; + right_sep.separator = separator; + } else { + middle_sep.separator_deduplicate = separator_deduplicate; + middle_sep.separator = separator; + } + } + Ok(Self { + range, + left_sep, + middle_sep, + right_sep, + left, + middle, + right, + }) + } + /// Could have any of: ``, `n`, `n,n`, `n|n`, `n,n|n`, `n|n,n`, `n|n|n`, `n|n,n|n` + const fn parse_triple(split: Option>) -> ResultFormatterConst<'a, (BindPower, BindPowerPair, BindPower)> { + const DEFAULT: BindPowerPair = BindPowerPair::symmetric(DEFAULT_BIND_POWER); + let split = map_opt!(split => split, return Ok((DEFAULT_BIND_POWER, DEFAULT, DEFAULT_BIND_POWER))); + let (_, first, split) = split.next::(); + let (pair, fst) = map_res!(BindPowerPair::parse(first)); + if pair { + // `n,n` or `n,n|n` + let split = map_opt!(split => split, return Ok((DEFAULT_BIND_POWER, fst, DEFAULT_BIND_POWER))); + let (_, second, split) = split.next::(); + #[allow(unreachable_code)] + { map_opt!(split => return Err(ParseErrorConst::too_many_control(split))); } + let (pair, snd) = map_res!(BindPowerPair::parse(second)); + return if pair { + Err(ParseErrorConst::unexpected_pair(second)) + } else { + // snd.left == snd.right + let snd = snd.left; + Ok((DEFAULT_BIND_POWER, fst, snd)) + } + } + // fst.left == fst.right + let split = map_opt!(split => split, return Ok((fst.left, fst, fst.right))); + let fst = fst.left; + // `n|n`, `n|n,n`, `n|n|n` or `n|n,n|n` + let (_, second, split) = split.next::(); + let (pair, snd) = map_res!(BindPowerPair::parse(second)); + let split = map_opt!(split => split, return Ok(if pair { + (fst, snd, DEFAULT_BIND_POWER) + } else { + // snd.left == snd.right + let snd = snd.left; + (fst, DEFAULT, snd) + })); + // `n|n|n` or `n|n,n|n` + let (_, third, split) = split.next::(); + #[allow(unreachable_code)] + { map_opt!(split => return Err(ParseErrorConst::too_many_control(split))); } + let (pair, thrd) = map_res!(BindPowerPair::parse(third)); + if pair { + Err(ParseErrorConst::unexpected_pair(third)) + } else { + // thrd.left == thrd.right + let thrd = thrd.left; + Ok((fst, snd, thrd)) + } + } +} + +impl<'a> SubFormatterConst<'a> { + pub const fn parse_control(s: &'a str) -> ResultFormatterConst<'a, (Self, &'a str)> { + if let Some(s) = ConstOperations::strip_prefix(s, '[') { + let split = ConstOperations::split_2(s, ']', CONTROL_CHARACTER); + let (_, control, split) = split.next::(); + let split = map_opt!(split, Err(ParseErrorConst::missing_control(s, "]$"))); + let control = map_res!(SubFormatterSingle::parse(control)); + return Ok((Self::Single(control), split.remainder())) + } + if let Some(s) = ConstOperations::strip_prefix(s, '(') { + let split = ConstOperations::split_2(s, ')', CONTROL_CHARACTER); + let (_, control, split) = split.next::(); + let split = map_opt!(split, Err(ParseErrorConst::missing_control(s, ")$"))); + let control = map_res!(SubFormatterRepeatConst::parse(control)); + return Ok((Self::Repeat(control), split.remainder())) + } + if let Some(s) = ConstOperations::strip_prefix(s, '{') { + let split = ConstOperations::split_2(s, '}', CONTROL_CHARACTER); + let (_, inner, split) = split.next::(); + let split = map_opt!(split, Err(ParseErrorConst::missing_control(s, "}$"))); + let capture = map_res!(ConstOperations::parse_u32(inner)); + if capture >= i32::MIN as u32 { + return Err(ParseErrorConst::capture_overflow(inner)); + } + let capture = map_opt!(NonMaxU32::new(capture), s => s, loop {}); + return Ok((Self::Capture(capture), split.remainder())) + } + Err(ParseErrorConst::incorrect_control(s)) + } + pub const fn parse_one(s: &'a str) -> ResultFormatterConst<'a, (Option>, Option<(Self, &'a str)>)> { + let split = ConstOperations::split(s, CONTROL_CHARACTER); + let (control_deduplicate, first, rest) = split.next::(); + let first = if first.is_empty() { + None + } else { + Some(SubFormatterString { data: first, control_deduplicate }) + }; + let rest = map_opt!(rest => map_res!(Self::parse_control(rest.remainder()))); + Ok((first, rest)) + } +} + +impl<'a> FormatterConst<'a> { + const INIT: Option> = None; + pub const fn parse(full: &'a str) -> ResultFormatterConst<'a, Self> { + let mut s = full; + let mut bind_power = BindPowerPair::symmetric(DEFAULT_BIND_POWER); + if let Some(rest) = ConstOperations::strip_prefix(s, CONTROL_CHARACTER) { + let (left, rest) = map_opt!(ConstOperations::split_first(rest, CONTROL_CHARACTER), Err(ParseErrorConst::missing_control(rest, "$"))); + let left = map_res!(ConstOperations::parse_u32(left)); + bind_power.left = left; + s = rest; + } + if let Some(rest) = ConstOperations::strip_suffix(s, CONTROL_CHARACTER) { + let (right, rest) = map_opt!(ConstOperations::split_last(rest, CONTROL_CHARACTER), Err(ParseErrorConst::missing_control(rest, "$"))); + let right = map_res!(ConstOperations::parse_u32(right)); + bind_power.right = right; + s = rest; + } + + let mut outputs = [Self::INIT; 64]; + let mut idx = 0; + loop { + let (str, ctrl) = map_res!(SubFormatterConst::parse_one(s)); + if let Some(str) = str { + outputs[idx] = Some(SubFormatterConst::String(str)); + idx += 1; + } + let Some((ctrl, rest)) = ctrl else { + break; + }; + outputs[idx] = Some(ctrl); + idx += 1; + s = rest; + } + Ok(Self { bind_power, outputs }) + } +} + +impl<'a> MatcherConst<'a> { + pub const fn parse(s: &'a str) -> ResultMatcherConst<'a, Self> { + let (s, children) = map_res!(Self::parse_children(s)); + let regex = map_opt!(ConstOperations::strip_prefix(s, '/'), s => ConstOperations::strip_suffix(s, '/'), None); + let (data, kind) = if let Some(regex) = regex { + (regex, MatcherKindConst::Regex) + } else { + (s, MatcherKindConst::Exact) + }; + Ok(Self { data, children, kind }) + } + pub const fn parse_children(s: &'a str) -> ResultMatcherConst<'a, (&'a str, Option)> { + let mut has_bracket = true; + let s = map_opt!(ConstOperations::strip_prefix(s, '('), s => s, { has_bracket = false; s }); + let mut s = match ConstOperations::strip_suffix(s, ')') { + Some(s) if has_bracket => s, + None if !has_bracket => return Ok((s, None)), + Some(s) => + return Err(ParseErrorConst::invalid_children_spec(s)), + None => return Err(ParseErrorConst::invalid_children_spec(s)), + }; + let mut children = NonMaxU32::ZERO; + while let Some(rest) = ConstOperations::strip_suffix(s, '_') { + let Some(rest) = ConstOperations::strip_suffix(rest, ' ') else { break }; + let new = NonMaxU32::new(children.get() + 1); + children = map_opt!(new, Err(ParseErrorConst::invalid_children_spec(s))); + s = rest; + } + Ok((s, Some(children))) + } +} + +impl<'a> TermDisplayConst<'a> { + pub const fn parse(m: &'a str, f: &'a str) -> ResultConst<'a, Self> { + let matcher = map_res!(MatcherConst::parse(m), err => ParseErrorConst::matcher(err)); + let formatter = map_res!(FormatterConst::parse(f), err => ParseErrorConst::formatter(err)); + if matches!(matcher.kind, MatcherKindConst::Exact) && formatter.max_capture().is_some() { + return Err(ParseErrorConst::invalid_capture(m)); + } + Ok(Self { matcher, formatter }) + } +} + +// Non-const parsing + +impl FromStr for ChildIndex { + type Err = FormatterParseError; + fn from_str(s: &str) -> Result { + Ok(Self::parse(s, true)?) + } +} + +impl FromStr for ChildRange { + type Err = FormatterParseError; + fn from_str(s: &str) -> Result { + Ok(Self::parse(s)?) + } +} + +impl FromStr for SubFormatterSingle { + type Err = FormatterParseError; + fn from_str(s: &str) -> Result { + Ok(Self::parse(s)?) + } +} + +impl FromStr for SubFormatterRepeat { + type Err = FormatterParseError; + fn from_str<'a>(s: &'a str) -> Result { + let self_ = SubFormatterRepeatConst::parse(s)?; + self_.try_into() + } +} + +impl FromStr for Formatter { + type Err = FormatterParseError; + fn from_str(s: &str) -> Result { + FormatterConst::parse(s)?.try_into() + } +} + +impl FromStr for FallbackFormatter { + type Err = FallbackParseError; + fn from_str(s: &str) -> Result { + FallbackFormatter::new(s.parse().map_err(FallbackParseError::FormatterParseError)?) + } +} + +impl FromStr for Matcher { + type Err = ConversionError; + fn from_str(s: &str) -> Result { + Ok(MatcherConst::parse(s).map_err(ParseError::from)?.try_into()?) + } +} + +// Helpers for const parsing + +#[derive(Debug, Clone, Copy)] +pub(super) struct ConstSplit<'a, const N: usize>(&'a str, [u8; N]); + +struct Check; +impl Check { + const CHECK_N_SIZE: () = { + ["N must be 1 or 2"][!(N == 1 || N == 2) as usize]; + ["N must be 1 when SKIP_DOUBLE"][!(N == 1 || !SKIP_DOUBLE) as usize]; + }; +} + +impl<'a, const N: usize> ConstSplit<'a, N> { + const fn next(self) -> (bool, &'a str, Option) { + let _ = Check::::CHECK_N_SIZE; + + let full = self.0.as_bytes(); + let mut s = full; + let mut skipped = false; + let mut idx = 0; + let reached_sep = loop { + match s { + [] => break None, + [b, n, r @ ..] if N == 1 && SKIP_DOUBLE && *b == self.1[0] && *n == self.1[0] => { + skipped = true; + idx += 2; + s = r; + } + [b, r @ ..] if N == 1 => { + s = r; + if *b == self.1[0] { + break Some(idx); + } + idx += 1; + } + [_] if N >= 2 => break None, + [b1, r @ ..] if N >= 2 => { + s = r; + if *b1 == self.1[0] { + let [b2, r @ ..] = r else { loop {} }; + if *b2 == self.1[1] { + s = r; + break Some(idx); + } + } + idx += 1; + } + _ => loop {} + } + }; + match reached_sep { + Some(reached_sep) => { + let (part, _) = full.split_at(reached_sep); + let part = unsafe { + std::str::from_utf8_unchecked(part) + }; + let rest = unsafe { + std::str::from_utf8_unchecked(s) + }; + (skipped, part, Some(ConstSplit(rest, self.1))) + } + None => (skipped, self.0, None), + } + } + const fn prev(self) -> (bool, &'a str, Option) { + let _ = Check::::CHECK_N_SIZE; + + let full = self.0.as_bytes(); + let mut s = full; + let mut skipped = false; + let mut idx = s.len(); + let reached_sep = loop { + match s { + [] => break None, + [r @ .., b, n] if N == 1 && SKIP_DOUBLE && *b == self.1[0] && *n == self.1[0] => { + skipped = true; + idx -= 2; + s = r; + } + [r @ .., b] if N == 1 => { + s = r; + if *b == self.1[0] { + break Some(idx); + } + idx -= 1; + } + [_] if N >= 2 => break None, + [r @ .., b2] if N >= 2 => { + s = r; + if *b2 == self.1[1] { + let [r @ .., b1] = r else { loop {} }; + if *b1 == self.1[1] { + s = r; + break Some(idx); + } + } + idx -= 1; + } + _ => loop {} + } + }; + match reached_sep { + Some(reached_sep) => { + let (_, part) = full.split_at(reached_sep); + let part = unsafe { + std::str::from_utf8_unchecked(part) + }; + let rest = unsafe { + std::str::from_utf8_unchecked(s) + }; + (skipped, part, Some(ConstSplit(rest, self.1))) + } + None => (skipped, self.0, None), + } + } + pub(super) const fn remainder(self) -> &'a str { + self.0 + } +} +impl ConstSplit<'_, 1> { + pub(super) const fn control(self) -> char { + self.1[0] as char + } +} + +struct ConstOperations; +impl ConstOperations { + const fn char_as_ascii(c: char) -> u8 { + ["Character must be an ASCII byte"][!c.is_ascii() as usize]; + c as u8 + } + + const fn strip_prefix(s: &str, prefix: char) -> Option<&str> { + let prefix = Self::char_as_ascii(prefix); + match s.as_bytes() { + [b, s @ ..] if *b == prefix => + Some(unsafe { std::str::from_utf8_unchecked(s) }), + _ => None, + } + } + const fn strip_suffix(s: &str, suffix: char) -> Option<&str> { + let suffix = Self::char_as_ascii(suffix); + match s.as_bytes() { + [s @ .., b] if *b == suffix => + Some(unsafe { std::str::from_utf8_unchecked(s) }), + _ => None, + } + } + + const fn split<'a>(s: &'a str, sep: char) -> ConstSplit<'a, 1> { + let sep = Self::char_as_ascii(sep); + ConstSplit(s, [sep]) + } + const fn split_2<'a>(s: &'a str, sep1: char, sep2: char) -> ConstSplit<'a, 2> { + let sep1 = Self::char_as_ascii(sep1); + let sep2 = Self::char_as_ascii(sep2); + ConstSplit(s, [sep1, sep2]) + } + + const fn split_more<'a, const N: usize>(s: Option>) -> (Option<&'a str>, Option>) { + map_opt!(s => { + let (_, part, split) = s.next::(); + (Some(part), split) + }, (None, None)) + } + const fn split_first(s: &'_ str, sep: char) -> Option<(&'_ str, &'_ str)> { + let split = Self::split(s, sep); + let (_, first, split) = split.next::(); + map_opt!(split => (first, split.remainder())) + } + const fn split_last(s: &'_ str, sep: char) -> Option<(&'_ str, &'_ str)> { + let split = Self::split(s, sep); + let (_, last, split) = split.prev::(); + map_opt!(split => (last, split.remainder())) + } + + const fn parse_i32<'a>(full: &'a str) -> ResultFormatterConst<'a, i32> { + let neg = Self::strip_prefix(full, '-'); + let is_neg = neg.is_some(); + let s = map_opt!(neg => neg, full); + if s.is_empty() { + return Err(ParseErrorConst::invalid_number(full)) + } + let leading_zero = Self::strip_prefix(s, '0'); + if let Some(leading_zero) = leading_zero { + return if is_neg || !leading_zero.is_empty() { + Err(ParseErrorConst::invalid_number(s)) + } else { + Ok(0) + } + } + let mut s = s.as_bytes(); + + let mut num = 0; + while !s.is_empty() { + match s { + [b @ b'0'..=b'9', r @ ..] => { + num = num * 10; + let delta = (*b - b'0') as i32; + if is_neg { + num -= delta; + } else { + num += delta; + } + s = r; + } + _ => { + let s = unsafe { std::str::from_utf8_unchecked(s) }; + return Err(ParseErrorConst::invalid_number(s)) + } + } + }; + Ok(num) + } + const fn parse_u32<'a>(full: &'a str) -> ResultFormatterConst<'a, u32> { + let data = map_res!(Self::parse_i32(full)); + Ok(data as u32) + } +} diff --git a/smt-log-parser/src/formatter/serde.rs b/smt-log-parser/src/formatter/serde.rs new file mode 100644 index 00000000..26f54540 --- /dev/null +++ b/smt-log-parser/src/formatter/serde.rs @@ -0,0 +1,48 @@ +use std::borrow::Cow; + +use crate::NonMaxU32; + +use super::defns; + +#[derive(serde::Serialize, serde::Deserialize)] +struct TermDisplayContext<'a> { + string_matchers: Vec<(Cow<'a, (Cow<'static, str>, Option)>, Cow<'a, defns::TermDisplay>)>, + regex_matchers: Cow<'a, Vec>, + fallback: Cow<'a, defns::FallbackFormatter>, +} + +impl serde::Serialize for defns::TermDisplayContext { + fn serialize(&self, serializer: S) -> Result { + let (string_matchers, regex_matchers, fallback) = self.to_parts(); + let self_ = TermDisplayContext { + string_matchers: string_matchers.iter().map(|(k, v)| (Cow::Borrowed(k), Cow::Borrowed(v))).collect(), + regex_matchers: Cow::Borrowed(regex_matchers), + fallback: Cow::Borrowed(fallback), + }; + self_.serialize(serializer) + } +} +impl<'de> serde::Deserialize<'de> for defns::TermDisplayContext { + fn deserialize>(deserializer: D) -> Result { + let self_: TermDisplayContext = serde::Deserialize::deserialize(deserializer)?; + let string_matchers = self_.string_matchers.into_iter().map(|(k, v)| (k.into_owned(), v.into_owned())).collect(); + let regex_matchers = self_.regex_matchers.into_owned(); + let fallback = self_.fallback.into_owned(); + Ok(Self::from_parts(string_matchers, regex_matchers, fallback)) + } +} + +#[derive(serde::Serialize, serde::Deserialize)] +struct RegexMatcher<'a>(Cow<'a, String>); + +impl serde::Serialize for defns::RegexMatcher { + fn serialize(&self, serializer: S) -> Result { + RegexMatcher(Cow::Borrowed(self.original())).serialize(serializer) + } +} +impl<'de> serde::Deserialize<'de> for defns::RegexMatcher { + fn deserialize>(deserializer: D) -> Result { + let RegexMatcher(s) = serde::Deserialize::deserialize(deserializer)?; + Ok(defns::RegexMatcher::new(s.into_owned()).map_err(serde::de::Error::custom)?) + } +} diff --git a/smt-log-parser/src/lib.rs b/smt-log-parser/src/lib.rs index a2022254..d77a6a2a 100644 --- a/smt-log-parser/src/lib.rs +++ b/smt-log-parser/src/lib.rs @@ -7,6 +7,8 @@ pub mod parsers; /// Pretty printing for items. #[cfg(feature = "display")] pub mod display_with; +#[cfg(feature = "display")] +pub mod formatter; mod error; mod mem_dbg; diff --git a/smt-log-parser/src/mem_dbg/mod.rs b/smt-log-parser/src/mem_dbg/mod.rs index 73c421b8..b5bd29ef 100644 --- a/smt-log-parser/src/mem_dbg/mod.rs +++ b/smt-log-parser/src/mem_dbg/mod.rs @@ -71,7 +71,7 @@ macro_rules! derive_wrapper { macro_rules! derive_non_max { ($name:ident, $prim:ident) => { - derive_wrapper!(nonmax::$name: Copy + Eq + PartialEq + PartialOrd + Ord + Hash); + derive_wrapper!(nonmax::$name: Copy + Eq + PartialEq + PartialOrd + Ord + Hash + Default); impl $name { pub const ZERO: Self = Self(nonmax::$name::ZERO); pub const ONE: Self = Self(nonmax::$name::ONE); diff --git a/smt-log-parser/src/parsers/z3/graph/analysis/matching_loop.rs b/smt-log-parser/src/parsers/z3/graph/analysis/matching_loop.rs index ddd285a0..ab4ead06 100644 --- a/smt-log-parser/src/parsers/z3/graph/analysis/matching_loop.rs +++ b/smt-log-parser/src/parsers/z3/graph/analysis/matching_loop.rs @@ -4,7 +4,7 @@ use fxhash::{FxHashMap, FxHashSet}; use gloo_console::log; use petgraph::{graph::NodeIndex, visit::Dfs, Direction::{Incoming, Outgoing}}; -use crate::{display_with::{DisplayConfiguration, DisplayCtxt, DisplayWithCtxt}, items::{ENodeIdx, EqTransIdx, InstIdx, MatchKind, QuantIdx, TermIdx}, parsers::z3::graph::{raw::{Node, NodeKind, RawIx}, visible::VisibleEdge, InstGraph}, Graph, Z3Parser, NonMaxU32}; +use crate::{display_with::{DisplayConfiguration, DisplayCtxt, DisplayWithCtxt}, formatter::TermDisplayContext, items::{ENodeIdx, EqTransIdx, InstIdx, MatchKind, QuantIdx, TermIdx}, parsers::z3::graph::{raw::{Node, NodeKind, RawIx}, visible::VisibleEdge, InstGraph}, Graph, NonMaxU32, Z3Parser}; use super::RawNodeIndex; // use matching_loop_graph::*; @@ -47,17 +47,6 @@ impl MlMatchedTerm { // TODO: maybe only generalise the terms in the very end? Otherwise we are creating lots of unnecessary generalised // terms that we won't even make use of pub fn merge_with(&mut self, matched: TermIdx, quant: QuantIdx, pattern: TermIdx, parser: &mut Z3Parser) { - let _ctxt = DisplayCtxt { - parser: &parser, - config: DisplayConfiguration { - display_term_ids: false, - display_quantifier_name: false, - use_mathematical_symbols: true, - html: true, - enode_char_limit: None, - ast_depth_limit: None, - }, - }; if let Some(term) = parser.terms.generalise(&mut parser.strings, vec![self.matched, matched]) { self.matched = term; } @@ -99,13 +88,15 @@ impl AbstractInst { } } pub fn to_string(&self, compact: bool, parser: &mut Z3Parser) -> String { - let generalised_pattern = parser.terms.generalise_pattern(&mut parser.strings, self.id.1); + let generalised_pattern = parser.terms.generalise_pattern(&mut parser.strings, self.id.1); + // TODO: this should be passed from the outside let ctxt = DisplayCtxt { parser: &parser, + term_display: &TermDisplayContext::default(), config: DisplayConfiguration { display_term_ids: false, display_quantifier_name: false, - use_mathematical_symbols: true, + replace_symbols: crate::display_with::SymbolReplacement::Math, html: true, enode_char_limit: None, ast_depth_limit: None, @@ -232,7 +223,7 @@ impl InstGraph { }; } - pub fn compute_nth_matching_loop_graph(&mut self, n: usize, parser: &mut Z3Parser) -> Graph<(String, MLGraphNode), ()> { + pub fn compute_nth_matching_loop_graph(&self, n: usize, parser: &mut Z3Parser) -> Graph<(String, MLGraphNode), ()> { let nodes_of_nth_matching_loop = self.raw.graph.node_indices().filter(|nx| self.raw.graph[*nx].part_of_ml.contains(&n)).collect::>>(); // here we "fold" a potential matching loop into an abstract instantiation graph that represents the repeating pattern of the potential matching loop // an abstract instantiation is defined by the quantifier and the pattern used for the pattern match @@ -309,10 +300,11 @@ impl InstGraph { for matched_term in abstract_inst.matched_terms.values() { let ctxt = DisplayCtxt { parser: &parser, + term_display: &TermDisplayContext::default(), config: DisplayConfiguration { display_term_ids: false, display_quantifier_name: false, - use_mathematical_symbols: true, + replace_symbols: crate::display_with::SymbolReplacement::Math, html: true, enode_char_limit: None, ast_depth_limit: Some(AST_DEPTH_LIMIT), @@ -350,10 +342,11 @@ impl InstGraph { for eq in abstract_inst.equalities.values() { let ctxt = DisplayCtxt { parser: &parser, + term_display: &TermDisplayContext::default(), config: DisplayConfiguration { display_term_ids: false, display_quantifier_name: false, - use_mathematical_symbols: true, + replace_symbols: crate::display_with::SymbolReplacement::Math, html: true, enode_char_limit: None, ast_depth_limit: Some(AST_DEPTH_LIMIT),