Variety of small fixes

README.md

@@ -32,6 +32,8 @@ NOTE: if this takes too long, it is possible to run the Axiom Profiler with a pr
 
 Similarly, if you have a log file which takes too long to load into the Axiom Profiler, hitting Cancel will cause the tool to work with the portion loaded so far.
 
+To correctly parse the log file, we impose a few [restrictions](smt-log-parser/design-docs/restrictions.md) on the smt2 file given to z3.
+
 ## Obtaining Z3 logs from various verification tools that use Z3 (feel free to add more)
 
 ### Boogie

axiom-profiler-GUI/assets/html/perfetto.css

@@ -938,6 +938,7 @@ input[type="file"] {
     display: grid;
     grid-template-columns: [left] auto [right] 1fr;
     row-gap: 5px;
+	overflow-x: scroll;
 }
 .pf-tree .pf-tree-node {
     display: contents;

axiom-profiler-GUI/assets/html/style.css

@@ -254,7 +254,13 @@ mwc-dialog {
     width: 0.5lh;
     height: 0.5lh;
     border: 1px solid #000;
-    margin: 0 0.25lh;
+    flex-shrink: 0;
+}
+.node-colour.ml {
+    margin-left: 0.25lh;
+}
+.node-colour.mr {
+    margin-right: 0.25lh;
 }
 .omnibox-dropdown .omnibox-options-container li .tag {
     border-radius: 10px;

axiom-profiler-GUI/src/configuration/data.rs

@@ -58,7 +58,7 @@ impl Configuration {
             input: None,
             html: true,
             font_tag: false,
-            ast_depth_limit: NonMaxU32::new(50),
+            ast_depth_limit: NonMaxU32::new(20),
             // Set manually elsewhere
             enode_char_limit: None,
         }

axiom-profiler-GUI/src/configuration/page.rs

@@ -122,7 +122,7 @@ pub fn Flags(props: &FlagsProps) -> Html {
         "Printing depth limit",
         "Stop printing terms once this AST depth has been reached. Only needed to avoid crashes with huge proof terms.", |
         if NonMaxU32::new(10) => "10",
-        if NonMaxU32::new(25) => "25",
+        if NonMaxU32::new(20) => "20",
         if NonMaxU32::new(50) => "50",
         if NonMaxU32::new(100) => "100",
         if None => "Disabled"

axiom-profiler-GUI/src/screen/file/summary.rs

@@ -70,10 +70,12 @@ pub fn Summary(props: &SummaryProps) -> Html {
             <MostQuants ..inner.clone() />
             <CostQuants ..inner.clone() />
             <MultQuants ..inner.clone() />
-        </DetailContainer><DetailContainer>
+        </DetailContainer>
+        <DetailContainer>
             <CostLemmas ..inner.clone() />
             <CostCdcl ..inner />
-        </DetailContainer></article>
+        </DetailContainer>
+        </article>
         {graph}
     </div>}
 }
@@ -149,7 +151,7 @@ pub fn MostQuants(props: &SummaryPropsInner) -> Html {
         .take_while(|(.., c)| *c > 0);
     let quants = quants.map(|(q, hue, (), c)| {
         let left = format_to_html(*c);
-        let right = html! { <div class="info-box-row">{ format!("{q}") }<QuantColourBox {hue} /></div> };
+        let right = html! { <div class="info-box-row"><QuantColourBox margin_right={true} {hue} />{ format!("{q}") }</div> };
         (left, right)
     }).collect::<Vec<_>>();
 
@@ -179,7 +181,7 @@ pub fn CostQuants(props: &SummaryPropsInner) -> Html {
         let costs = costs.iter().take(DISPLAY_TOP_N).take_while(|(.., c)| c.0 > 0.0);
         let costs = costs.map(|(q, hue, c, _)| {
             let left = html!{{ format!("{c:.1}") }};
-            let right = html! { <div class="info-box-row">{ format!("{q}") }<QuantColourBox {hue} /></div> };
+            let right = html! { <div class="info-box-row"><QuantColourBox margin_right={true} {hue} />{ format!("{q}") }</div> };
             (left, right)
         }).collect::<Vec<_>>();
         html! {<Detail title="Average cost" hover="The quantifiers upon which the most instantiations causally depend. See average weighing flag.">
@@ -209,7 +211,7 @@ pub fn MultQuants(props: &SummaryPropsInner) -> Html {
         let mults = mults.iter().take(DISPLAY_TOP_N).take_while(|(.., c)| c.0 > 0.0);
         let mults = mults.map(|(q, hue, c, _)| {
             let left = html!{{ format!("{c:.1}") }};
-            let right = html! { <div class="info-box-row">{ format!("{q}") }<QuantColourBox {hue} /></div> };
+            let right = html! { <div class="info-box-row"><QuantColourBox margin_right={true} {hue} />{ format!("{q}") }</div> };
             (left, right)
         }).collect::<Vec<_>>();
         html! {<Detail title="Average multiplicativity" hover="The quantifiers which the highest multiplicative factor, i.e. those that on average directly cause N other instantiations. See average weighing flag.">

axiom-profiler-GUI/src/screen/inst_graph/search.rs

@@ -133,7 +133,7 @@ impl Graph {
                 search_text: search_text.to_string(),
                 post_text: String::new(),
                 info: html! {<>
-                    <QuantColourBox {hue} />
+                    <QuantColourBox margin_right={true} {hue} />
                     {counter.visible.len().to_string()}{" shown / "}{counter.total().to_string()}
                 </>},
                 select_from: counter.visible.len(),

axiom-profiler-GUI/src/utils/colouring.rs

@@ -7,14 +7,22 @@ use yew::prelude::*;
 #[derive(Properties, Clone, PartialEq)]
 pub struct QuantColourBoxProps {
     pub hue: Option<f64>,
+    pub margin_left: Option<bool>,
+    pub margin_right: Option<bool>,
 }
 
 #[function_component]
 pub fn QuantColourBox(props: &QuantColourBoxProps) -> Html {
     let style = props
         .hue
         .map(|hue| format!("background-color: hsl({hue}, 79%, 76%)"));
-    html! { <div class="node-colour" {style}></div> }
+    let class = match (props.margin_left, props.margin_right) {
+        (Some(true), Some(true)) => "node-colour ml mr",
+        (Some(true), _) => "node-colour ml",
+        (_, Some(true)) => "node-colour mr",
+        (_, _) => "node-colour",
+    };
+    html! { <div {class} {style}></div> }
 }
 
 #[derive(Debug, Clone)]

smt-log-parser/Cargo.toml

@@ -36,7 +36,9 @@ clap = { version = "4.5.4", features = ["derive"] }
 [dev-dependencies]
 memory-stats = "1.1.0"
 cap = "0.1.2"
-smt-log-parser = { path = ".", features = ["mem_dbg"] }
+serde_json = "1.0"
+rand = "0.8"
+smt-log-parser = { path = ".", features = ["mem_dbg", "serde"] }
 
 [features]
 default = ["display", "analysis"]

smt-log-parser/design-docs/restrictions.md

@@ -0,0 +1,9 @@
+This document describes restrictions on the input smt2 files which our tool requires to be satisfied.
+These restrictions are due to z3 bugs/limitations which require workarounds in our tool.
+If these restrictions are not satisfied these workarounds might fail and lines in the log file might be ignored.
+
+## Names
+
+The following restrictions apply to choosing names for `declare-fun` and `declare-const`:
+
+- The names `string`, `indent`, `compose`, `choice` and `cr` are forbidden ([#100](https://github.com/viperproject/axiom-profiler-2/issues/100)).

smt-log-parser/src/analysis/generalise.rs

@@ -4,7 +4,7 @@ use crate::{
         synthetic::{AnyTerm, SynthIdx, SynthTermKind, SynthTerms},
         terms::Terms,
     },
-    Result,
+    FxHashMap, Result,
 };
 
 impl SynthTerms {
@@ -13,6 +13,7 @@ impl SynthTerms {
         table: &Terms,
         smaller: TermIdx,
         larger: TermIdx,
+        depth: usize,
     ) -> Result<Option<SynthIdx>> {
         if smaller == larger {
             // if terms are equal, no need to generalize
@@ -29,11 +30,15 @@ impl SynthTerms {
             && smaller_term.kind == larger_term.kind
             && smaller_term.child_ids.len() == larger_term.child_ids.len()
         {
+            // TODO: remove this depth restriction
+            if depth == 0 {
+                return Ok(None);
+            }
             let Some(child_ids) = smaller_term
                 .child_ids
                 .iter()
                 .zip(&*larger_term.child_ids)
-                .map(|(&sc, &lc)| self.generalise_first(table, sc, lc))
+                .map(|(&sc, &lc)| self.generalise_first(table, sc, lc, depth - 1))
                 .collect::<Result<Option<_>>>()?
             else {
                 return Ok(None);
@@ -60,19 +65,38 @@ impl SynthTerms {
     ) -> Result<Option<SynthIdx>> {
         assert_ne!(larger, smaller);
         let smaller_meaning = table.meaning(smaller);
+        let mut cache = FxHashMap::default();
         let (found_smaller, replaced) =
-            self.input_replace_inner(table, smaller, smaller_meaning, larger)?;
+            self.input_replace_inner(table, smaller, smaller_meaning, larger, &mut cache)?;
         // If we didn't find the smaller term in the bigger one, then it's
         // probably not a repeating pattern getting larger (so return `None`).
         Ok(found_smaller.then_some(replaced))
     }
 
+    fn input_replace_cached(
+        &mut self,
+        table: &Terms,
+        smaller: TermIdx,
+        smaller_meaning: Option<&Meaning>,
+        larger: TermIdx,
+        cache: &mut FxHashMap<TermIdx, (bool, SynthIdx)>,
+    ) -> Result<(bool, SynthIdx)> {
+        if let Some((found_smaller, replaced)) = cache.get(&larger) {
+            return Ok((*found_smaller, *replaced));
+        }
+        let (found_smaller, replaced) =
+            self.input_replace_inner(table, smaller, smaller_meaning, larger, cache)?;
+        cache.insert(larger, (found_smaller, replaced));
+        Ok((found_smaller, replaced))
+    }
+
     fn input_replace_inner(
         &mut self,
         table: &Terms,
         smaller: TermIdx,
         smaller_meaning: Option<&Meaning>,
         larger: TermIdx,
+        cache: &mut FxHashMap<TermIdx, (bool, SynthIdx)>,
     ) -> Result<(bool, SynthIdx)> {
         if larger == smaller {
             return Ok((true, self.new_input(None)?));
@@ -98,7 +122,7 @@ impl SynthTerms {
             .iter()
             .map(|&c| {
                 let (found, replaced) =
-                    self.input_replace_inner(table, smaller, smaller_meaning, c)?;
+                    self.input_replace_cached(table, smaller, smaller_meaning, c, cache)?;
                 found_smaller |= found;
                 Ok(replaced)
             })

smt-log-parser/src/analysis/graph/analysis/matching_loop/analysis.rs

@@ -2,13 +2,14 @@ use std::cmp::Reverse;
 
 #[cfg(feature = "mem_dbg")]
 use mem_dbg::{MemDbg, MemSize};
+use nonmax::NonMaxU64;
 
 use crate::{
     analysis::{analysis::run::TopoAnalysis, raw::Node, InstGraph, RawNodeIndex},
     idx,
     items::{Blame, ENodeIdx, EqTransIdx, InstIdx, TermIdx},
     mem_dbg::InternMap,
-    parsers::z3::synthetic::SynthIdx,
+    parsers::z3::{synthetic::SynthIdx, AstSize},
     FxHashMap, FxHashSet, TiVec, Z3Parser,
 };
 
@@ -118,6 +119,7 @@ impl<'a> MlAnalysis<'a> {
         parser: &'a mut Z3Parser,
         signatures: Vec<(MlSignature, FxHashSet<InstIdx>)>,
     ) -> Self {
+        let mut cached = FxHashMap::default();
         let mut node_to_ml = FxHashMap::<InstIdx, MlNodeInfo>::default();
         let data = signatures
             .into_iter()
@@ -127,7 +129,7 @@ impl<'a> MlAnalysis<'a> {
                 node_to_ml.extend(
                     iidxs
                         .into_iter()
-                        .map(|iidx| (iidx, MlNodeInfo::new(parser, iidx, i))),
+                        .map(|iidx| (iidx, MlNodeInfo::new(parser, iidx, i, &mut cached))),
                 );
                 sig
             })
@@ -238,7 +240,7 @@ impl<'a> MlAnalysis<'a> {
 #[derive(Debug)]
 pub struct MlNodeInfo {
     pub ml_sig: MlSigIdx,
-    pub ast_size: u32,
+    pub ast_size: Option<NonMaxU64>,
     pub blames: Box<[CollectedBlame]>,
 
     pub tree_above: Vec<MlLinkInfo>,
@@ -318,7 +320,7 @@ impl MlAnalysisInner<'_> {
                 let enode = self
                     .parser
                     .synth_terms
-                    .generalise_first(&self.parser.terms, smaller.owner, larger.owner)
+                    .generalise_first(&self.parser.terms, smaller.owner, larger.owner, 20)
                     .unwrap()?;
                 // println!("result  : {:?}", enode.debug(self.parser));
                 assert_eq!(smaller.equalities.len(), larger.equalities.len());
@@ -335,7 +337,7 @@ impl MlAnalysisInner<'_> {
                         let from = self
                             .parser
                             .synth_terms
-                            .generalise_first(&self.parser.terms, self_eq.1, other_eq.1)
+                            .generalise_first(&self.parser.terms, self_eq.1, other_eq.1, 20)
                             .unwrap()?;
                         // println!("result   : {:?}", from.debug(self.parser));
                         // println!(
@@ -346,7 +348,7 @@ impl MlAnalysisInner<'_> {
                         let to = self
                             .parser
                             .synth_terms
-                            .generalise_first(&self.parser.terms, self_eq.2, other_eq.2)
+                            .generalise_first(&self.parser.terms, self_eq.2, other_eq.2, 20)
                             .unwrap()?;
                         // println!("result   : {:?}", to.debug(self.parser));
                         Some((from, to))
@@ -412,10 +414,15 @@ impl MlNodeInfo {
         blames.map(|blame| CollectedBlame::new(parser, blame))
     }
 
-    pub fn new(parser: &Z3Parser, iidx: InstIdx, ml_sig: MlSigIdx) -> Self {
+    pub fn new(
+        parser: &Z3Parser,
+        iidx: InstIdx,
+        ml_sig: MlSigIdx,
+        cached: &mut FxHashMap<TermIdx, AstSize>,
+    ) -> Self {
         Self {
             ml_sig,
-            ast_size: parser.inst_ast_size(iidx),
+            ast_size: parser.inst_ast_size(iidx, cached),
             tree_above: Default::default(),
             blames: Self::blames(parser, iidx).collect(),
         }
@@ -492,6 +499,15 @@ impl MlNodeInfo {
             Some(above)
         })
     }
+
+    pub fn ge_ast_size(&self, other: &Self) -> bool {
+        match (self.ast_size, other.ast_size) {
+            (Some(ss), Some(os)) => ss >= os,
+            (Some(_), None) => false,
+            (None, Some(_)) => true,
+            (None, None) => true,
+        }
+    }
 }
 
 #[cfg_attr(feature = "mem_dbg", derive(MemSize, MemDbg))]
@@ -559,7 +575,7 @@ impl TopoAnalysis<true, false> for MlAnalysis<'_> {
 
         curr.filter(|prev_iidx| {
             let prev_info = self.node_to_ml.get_mut(&prev_iidx).unwrap();
-            if prev_info.ml_sig == curr_info.ml_sig && prev_info.ast_size <= curr_info.ast_size {
+            if prev_info.ml_sig == curr_info.ml_sig && curr_info.ge_ast_size(prev_info) {
                 let mut gen = None;
                 let mut max_ungen_depth = 0;
                 let mut max_depth = 0;

smt-log-parser/src/analysis/graph/analysis/matching_loop/explain.rs

@@ -426,8 +426,8 @@ impl MlExplainer {
                 self.ancestor_is_recurring = false;
 
                 let all = self.equalities().transitive[eq].all(forward);
-                for next in all {
-                    use TransitiveExplSegmentKind::*;
+                use TransitiveExplSegmentKind::*;
+                for next in all.clone() {
                     match next.kind {
                         Given(eq_use) => self.walk_given(eq_use, next.forward)?,
                         Transitive(eq) => self.walk_trans(eq, next.forward)?,
@@ -436,6 +436,13 @@ impl MlExplainer {
                     ancestor_is_recurring |= self.ancestor_is_recurring;
                     self.ancestor_is_recurring = false;
                 }
+                if !self.ancestor_is_recurring {
+                    for next in all {
+                        if let Transitive(eq) = next.kind {
+                            self.burned_eqs.insert(eq);
+                        }
+                    }
+                }
                 self.ancestor_is_recurring = ancestor_is_recurring;
                 Ok(())
             }
@@ -483,6 +490,9 @@ impl MlExplainer {
                 eq: EqTransIdx,
                 forward: bool,
             ) -> core::result::Result<(), Never> {
+                if self.burned_eqs.contains(&eq) {
+                    return Ok(());
+                }
                 self.super_walk_trans(eq, forward)?;
                 if self.ancestor_is_recurring && !self.add_mode {
                     self.burned_eqs.insert(eq);

smt-log-parser/src/analysis/graph/analysis/reconnect.rs

@@ -142,7 +142,8 @@ impl ReconnectEdge {
     }
 
     fn set_to_h(self, to_h: RawNodeIndex) -> Self {
-        assert_eq!(self.from.visible, self.to_h);
+        debug_assert_eq!(self.from.visible, self.to_h);
+        debug_assert_ne!(self.to_h, to_h);
         Self { to_h, ..self }
     }
 }